[sledge] Remove Trace.report in favor of Trace.fail

Summary:
Trace.report is essentially redundant with Trace.fail, and does not
behave as well wrt flushing when raising exceptions.

Reviewed By: ngorogiannis

Differential Revision: D14251657

fbshipit-source-id: 69a61c915

sledge/src/llair/exp.ml

@@ -1088,8 +1088,8 @@ let app1 ?(partial = false) op arg =
                | App _ as a ->
                    assert (
                      equal a op || equal a arg
-                     || Trace.report
+                     || Trace.fail
-                          "simplifying %a %a yields %a with new subexp %a"
+                          "simplifying %a %a@ yields %a@ with new subexp %a"
                           pp op pp arg pp e pp a )
                | _ -> () ) )
 

sledge/src/symbheap/congruence.ml

@@ -284,8 +284,8 @@ let pre_invariant r =
       Exp.iter a ~f:(fun bj ->
           assert (
             in_car r (Exp.base bj)
-            || Trace.report "@[subexp %a of %a not in carrier of@ %a@]"
+            || Trace.fail "@[subexp %a of %a not in carrier of@ %a@]" Exp.pp
-                 Exp.pp bj Exp.pp a pp r ) ) ;
+                 bj Exp.pp a pp r ) ) ;
       let a', a_k = solve_for_base a'k a in
       (* carrier is closed under rep *)
       assert (in_car r a') ;
@@ -293,27 +293,25 @@ let pre_invariant r =
         (* rep is sparse for symbols *)
         assert (
           (not (Map.mem r.rep a'))
-          || Trace.report
+          || Trace.fail
                "no symbol rep should be in rep domain: %a @<2>↦ %a@\n%a"
                Exp.pp a Exp.pp a' pp r )
       else
         (* rep is idempotent for applications *)
         assert (
           is_rep r a'
-          || Trace.report
+          || Trace.fail "every app rep should be its own rep: %a @<2>↦ %a"
-               "every app rep should be its own rep: %a @<2>↦ %a" Exp.pp a
+               Exp.pp a Exp.pp a' ) ;
-               Exp.pp a' ) ;
       match Map.find r.cls a' with
       | None ->
           (* every rep in dom of cls *)
-          assert (
+          assert (Trace.fail "rep not in dom of cls: %a@\n%a" Exp.pp a' pp r)
-            Trace.report "rep not in dom of cls: %a@\n%a" Exp.pp a' pp r )
       | Some a_cls ->
           (* every exp is in class of its rep *)
           assert (
             (* rep a = a'+k so expect a-k in cls a' *)
             Cls.mem a_cls a_k
-            || Trace.report "%a = %a by rep but %a not in cls@\n%a" Exp.pp a
+            || Trace.fail "%a = %a by rep but %a not in cls@\n%a" Exp.pp a
                  Exp.pp a'k Exp.pp a_k pp r ) ) ;
   Map.iteri r.cls ~f:(fun ~key:a' ~data:a_cls ->
       (* domain of cls are reps *)
@@ -323,18 +321,18 @@ let pre_invariant r =
           let a, a'_k = solve_for_base ak a' in
           assert (
             in_car r a
-            || Trace.report "%a in cls of %a but not in carrier" Exp.pp a
+            || Trace.fail "%a in cls of %a but not in carrier" Exp.pp a
                  Exp.pp a' ) ;
           let a'' = norm_base r a in
           assert (
             (* a' = a+k in cls so expect rep a = a'-k *)
             Exp.equal a'' a'_k
-            || Trace.report "%a = %a by cls but @<2>≠ %a by rep" Exp.pp a'
+            || Trace.fail "%a = %a by cls but @<2>≠ %a by rep" Exp.pp a'
                  Exp.pp ak Exp.pp a'' ) ) ) ;
   Map.iteri r.use ~f:(fun ~key:a' ~data:a_use ->
       assert (
         (not (Use.is_empty a_use))
-        || Trace.report "empty use list should not have been added" ) ;
+        || Trace.fail "empty use list should not have been added" ) ;
       Use.iter a_use ~f:(fun u ->
           (* uses are applications *)
           assert (not (Exp.is_simple u)) ;
@@ -345,7 +343,7 @@ let pre_invariant r =
           (* every rep is a subexp-modulo-rep of each of its uses *)
           assert (
             Exp.exists u ~f:(fun bj -> Exp.equal a' (Exp.base (norm r bj)))
-            || Trace.report
+            || Trace.fail
                  "rep %a has use %a, but is not the rep of any immediate \
                   subexp of the use"
                  Exp.pp a' Exp.pp u ) ;
@@ -370,8 +368,8 @@ let pre_invariant r =
         (* lkp contains equalities provable modulo normalizing sub-exps *)
         assert (
           Exp.equal a c_'
-          || Trace.report "%a sub-normalizes to %a @<2>≠ %a" Exp.pp c
+          || Trace.fail "%a sub-normalizes to %a @<2>≠ %a" Exp.pp c Exp.pp
-               Exp.pp c_' Exp.pp a ) ;
+               c_' Exp.pp a ) ;
         let c' = norm_base r c in
         Exp.iter a ~f:(fun bj ->
             (* every subexp of an app in domain of lkp has an associated use *)
@@ -385,7 +383,7 @@ let pre_invariant r =
               Use.exists b_use ~f:(fun u ->
                   Exp.equal a (Exp.map ~f:(norm r) u)
                   && Exp.equal c' (norm_base r u) )
-              || Trace.report
+              || Trace.fail
                    "no corresponding use for subexp %a of lkp key %a" Exp.pp
                    bj Exp.pp a ) ) ) ) ;
   List.iter r.pnd ~f:(fun (ai, bj) ->

sledge/src/symbheap/exec.ml

@@ -266,10 +266,10 @@ let exec_spec pre {xs; foot; post} =
       xs Sh.pp foot Sh.pp post ;
     assert (
       let vs = Set.diff (Set.diff foot.Sh.us xs) pre.Sh.us in
-      Set.is_empty vs || Trace.report "unbound foot: {%a}" Var.Set.pp vs ) ;
+      Set.is_empty vs || Trace.fail "unbound foot: {%a}" Var.Set.pp vs ) ;
     assert (
       let vs = Set.diff (Set.diff post.Sh.us xs) pre.Sh.us in
-      Set.is_empty vs || Trace.report "unbound post: {%a}" Var.Set.pp vs )]
+      Set.is_empty vs || Trace.fail "unbound post: {%a}" Var.Set.pp vs )]
   ;
   let zs, pre = Sh.bind_exists pre ~wrt:xs in
   ( match Solver.infer_frame pre xs foot with

sledge/src/symbheap/sh.ml

@@ -131,11 +131,11 @@ let rec invariant q =
   try
     assert (
       Set.disjoint us xs
-      || Trace.report "inter: @[%a@]@\nq: @[%a@]" Var.Set.pp
+      || Trace.fail "inter: @[%a@]@\nq: @[%a@]" Var.Set.pp (Set.inter us xs)
-           (Set.inter us xs) pp q ) ;
+           pp q ) ;
     assert (
       Set.is_subset (fv q) ~of_:us
-      || Trace.report "unbound but free: %a" Var.Set.pp (Set.diff (fv q) us)
+      || Trace.fail "unbound but free: %a" Var.Set.pp (Set.diff (fv q) us)
     ) ;
     Congruence.invariant cong ;
     ( match djns with
@@ -241,7 +241,7 @@ let exists xs q =
   ;
   assert (
     Set.is_subset xs ~of_:q.us
-    || Trace.report "%a" Var.Set.pp (Set.diff xs q.us) ) ;
+    || Trace.fail "%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

@@ -617,7 +617,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.report "lost: %a" Var.Set.pp lost) ;
+        assert (Set.is_empty lost || Trace.fail "lost: %a" Var.Set.pp lost) ;
-        assert (
+        assert (Set.is_empty gain || Trace.fail "gained: %a" Var.Set.pp gain)
-          Set.is_empty gain || Trace.report "gained: %a" Var.Set.pp gain )
     )]

sledge/src/trace/trace.ml

@@ -144,10 +144,6 @@ let retn mod_name fun_name k result =
   k {pf= (fun fmt -> decf mod_name fun_name fmt)} result ;
   result
 
-let report fmt =
-  Format.fprintf fs "@\n@[<2>| " ;
-  Format.kfprintf (fun fs -> Format.fprintf fs "@]" ; false) fs fmt
-
 let fail fmt =
   Format.fprintf fs "@\n@[<2>| " ;
   Format.kfprintf

sledge/src/trace/trace.mli

@@ -52,8 +52,5 @@ val retn : string -> string -> (pf -> 'b -> unit) -> 'b -> 'b
 val flush : unit -> unit
 (** Flush the internal buffers. *)
 
-val report : ('a, Formatter.t, unit, bool) format4 -> 'a
-(** Emit a message at the current indentation level, and return [false]. *)
-
 val fail : ('a, Formatter.t, unit, _) format4 -> 'a
 (** Emit a message at the current indentation level, and [assert false]. *)