[sledge] Error reporting improvements

Summary:
Improve Trace.fail to log the error and raise informative exceptions.
Eliminate the confusion between Import.fail and Trace.fail by removing
Import.fail.

Reviewed By: bennostein

Differential Revision: D17725608

fbshipit-source-id: 79fdfbd86

sledge/src/config/dune.in

@@ -6,7 +6,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-let deps = ["import"]
+let deps = ["import"; "trace"]
 
 ;;
 Jbuild_plugin.V1.send

sledge/src/dune.in

@@ -6,7 +6,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-let deps = ["import"; "llair_"; "symbheap"; "config"; "domain"]
+let deps = ["import"; "trace"; "llair_"; "symbheap"; "config"; "domain"]
 
 ;;
 Jbuild_plugin.V1.send

sledge/src/import/import.ml

@@ -117,8 +117,8 @@ module Invariant = struct
             Error.to_exn
               (Error.create_s
                  (Base.Sexp.message "invariant failed"
-                    [ ("", Source_code_position.sexp_of_t here)
-                    ; ("exn", sexp_of_exn exn)
+                    [ ("", sexp_of_exn exn)
+                    ; ("", Source_code_position.sexp_of_t here)
                     ; ("", sexp_of_t t) ]))
           in
           Caml.Printexc.raise_with_backtrace exn bt ) ;

sledge/src/import/import.mli

@@ -77,6 +77,11 @@ type ('a, 'b) fmt = ('a, Formatter.t, unit, 'b) format4
 
 exception Unimplemented of string
 
+val raisef : (string -> exn) -> ('a, unit -> _) fmt -> 'a
+(** Take a function from a string message to an exception, and a format
+    string with the additional arguments it specifies, and then call the
+    function on the formatted string and raise the returned exception. *)
+
 val warn : ('a, unit -> unit) fmt -> 'a
 (** Issue a warning for a survivable problem. *)
 
@@ -91,10 +96,6 @@ val assertf : bool -> ('a, unit -> unit) fmt -> 'a
 val checkf : bool -> ('a, unit -> bool) fmt -> 'a
 (** As [assertf] but returns the argument bool. *)
 
-val fail : ('a, unit -> _) fmt -> 'a
-(** Raise a [Failure] exception indicating a fatal error not covered by
-    [assertf], [checkf], or [todo]. *)
-
 val check : ('a -> unit) -> 'a -> 'a
 (** Assert that function does not raise on argument, and return argument. *)
 

sledge/src/llair/frontend.ml

@@ -608,7 +608,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
       match (exp_typ, mask_typ) with
       | Array {len= m}, Array {len= n} when m = n && Llvm.is_null llmask ->
           exp
-      | _ -> fail "xlate_opcode: %a" pp_llvalue llv () )
+      | _ -> todo "vector operations: %a" pp_llvalue llv () )
   | Invalid | Ret | Br | Switch | IndirectBr | Invoke | Invalid2
    |Unreachable | Alloca | Load | Store | PHI | Call | UserOp1 | UserOp2
    |Fence | AtomicCmpXchg | AtomicRMW | Resume | LandingPad | CleanupRet
@@ -785,7 +785,7 @@ let rec xlate_func_name x llv =
   | GlobalIFunc -> todo "ifunc: %a" pp_llvalue llv ()
   | InlineAsm -> todo "inline asm: %a" pp_llvalue llv ()
   | ConstantPointerNull -> todo "call null: %a" pp_llvalue llv ()
-  | _ -> fail "unknown function: %a" pp_llvalue llv ()
+  | k -> todo "function kind %a in %a" pp_llvaluekind k pp_llvalue llv ()
 
 let ignored_callees = Hash_set.create (module String)
 
@@ -860,13 +860,12 @@ let xlate_instr :
         | ConstantExpr -> (
           match Llvm.constexpr_opcode maybe_llfunc with
           | BitCast -> Llvm.operand maybe_llfunc 0
-          | IntToPtr -> todo "calls with inttoptr" ()
           | _ ->
-              fail "Unknown value in a call instruction %a" pp_llvalue
+              todo "opcode kind in call instruction %a" pp_llvalue
                 maybe_llfunc () )
         | _ ->
-            fail "Unhandled operand type in a call instruction %a"
-              pp_llvaluekind llfunc_valuekind ()
+            todo "operand kind in call instruction %a" pp_llvaluekind
+              llfunc_valuekind ()
       in
       let lltyp = Llvm.type_of llfunc in
       assert (Poly.(Llvm.classify_type lltyp = Pointer)) ;

sledge/src/llair/term.ml

@@ -990,7 +990,7 @@ let map e ~f =
   | RecN (_, xs) ->
       assert (
         xs == Vector.map_preserving_phys_equal ~f xs
-        || fail "Term.map does not support updating subterms of RecN." ) ;
+        || fail "Term.map does not support updating subterms of RecN." () ) ;
       e
   | _ -> e
 

sledge/src/symbheap/equality.ml

@@ -99,8 +99,8 @@ let invariant r =
       iter_max_solvables a ~f:(fun b ->
           assert (
             in_car r b
-            || Trace.fail "@[subterm %a of %a not in carrier of@ %a@]"
-                 Term.pp b Term.pp a pp r ) ) )
+            || fail "@[subterm %a of %a not in carrier of@ %a@]" Term.pp b
+                 Term.pp a pp r () ) ) )
 
 (** Core operations *)
 

sledge/src/symbheap/exec.ml

@@ -662,10 +662,10 @@ let exec_spec pre {xs; foot; sub; ms; post} =
       ms Sh.pp post ;
     assert (
       let vs = Set.diff (Set.diff foot.us xs) pre.us in
-      Set.is_empty vs || Trace.fail "unbound foot: {%a}" Var.Set.pp vs ) ;
+      Set.is_empty vs || fail "unbound foot: {%a}" Var.Set.pp vs () ) ;
     assert (
       let vs = Set.diff (Set.diff post.us xs) pre.us in
-      Set.is_empty vs || Trace.fail "unbound post: {%a}" Var.Set.pp vs )]
+      Set.is_empty vs || fail "unbound post: {%a}" Var.Set.pp vs () )]
   ;
   let foot = Sh.extend_us xs foot in
   let zs, pre = Sh.bind_exists pre ~wrt:xs in
@@ -698,7 +698,7 @@ let kill pre reg = Sh.exists (Set.add Var.Set.empty reg) pre
 
 let move pre reg_exps =
   exec_spec pre (move_spec pre.us reg_exps)
-  |> function Some post -> post | _ -> fail "Exec.move failed"
+  |> function Some post -> post | _ -> fail "Exec.move failed" ()
 
 let load pre ~reg ~ptr ~len = exec_spec pre (load_spec pre.us reg ptr len)
 let store pre ~ptr ~exp ~len = exec_spec pre (store_spec pre.us ptr exp len)

sledge/src/symbheap/sh.ml

@@ -145,12 +145,11 @@ let rec invariant q =
   try
     assert (
       Set.disjoint us xs
-      || Trace.fail "inter: @[%a@]@\nq: @[%a@]" Var.Set.pp (Set.inter us xs)
-           pp q ) ;
+      || fail "inter: @[%a@]@\nq: @[%a@]" Var.Set.pp (Set.inter us xs) pp q
+           () ) ;
     assert (
       Set.is_subset (fv q) ~of_:us
-      || Trace.fail "unbound but free: %a" Var.Set.pp (Set.diff (fv q) us)
-    ) ;
+      || fail "unbound but free: %a" Var.Set.pp (Set.diff (fv q) us) () ) ;
     Equality.invariant cong ;
     ( match djns with
     | [[]] ->
@@ -274,8 +273,8 @@ let exists xs q =
   ;
   assert (
     Set.is_subset xs ~of_:q.us
-    || Trace.fail "Sh.exists fail xs - q.us:%a" Var.Set.pp
-         (Set.diff xs q.us) ) ;
+    || fail "Sh.exists fail xs - q.us:%a" Var.Set.pp (Set.diff xs q.us) ()
+  ) ;
   {q with us= Set.diff q.us xs; xs= Set.union q.xs xs} |> check invariant
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]

sledge/src/symbheap/solver.ml

@@ -626,6 +626,6 @@ let infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
     Option.iter r ~f:(fun frame ->
         let lost = Set.diff (Set.union minuend.us xs) frame.us in
         let gain = Set.diff frame.us (Set.union minuend.us xs) in
-        assert (Set.is_empty lost || Trace.fail "lost: %a" Var.Set.pp lost) ;
-        assert (Set.is_empty gain || Trace.fail "gained: %a" Var.Set.pp gain)
+        assert (Set.is_empty lost || fail "lost: %a" Var.Set.pp lost ()) ;
+        assert (Set.is_empty gain || fail "gained: %a" Var.Set.pp gain ())
     )]

sledge/src/trace/trace.ml

@@ -167,12 +167,11 @@ let retn mod_name fun_name k result =
   result
 
 let fail fmt =
-  Format.fprintf fs "@\n@[<2>| " ;
-  Format.kfprintf
-    (fun fs ->
-      Format.fprintf fs "@]@." ;
-      assert false )
-    fs fmt
+  raisef
+    (fun msg ->
+      Format.fprintf fs "@\n@[<2>| %s@]@." msg ;
+      Failure msg )
+    fmt
 
 let%test_module _ =
   (module struct let () = init ~margin:70 ~config:!config () end)

sledge/src/trace/trace.mli

@@ -60,5 +60,6 @@ val retn : string -> string -> (pf -> 'b -> unit) -> 'b -> 'b
 val flush : unit -> unit
 (** Flush the internal buffers. *)
 
-val fail : ('a, Formatter.t, unit, _) format4 -> 'a
-(** Emit a message at the current indentation level, and [assert false]. *)
+val fail : ('a, unit -> _) fmt -> 'a
+(** Emit a message at the current indentation level, and raise a [Failure]
+    exception indicating a fatal error. *)