From 55540d35008f456d00bc64041a9400eb7f218a98 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 28 Feb 2019 06:45:30 -0800 Subject: [PATCH] [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 | 4 ++-- sledge/src/symbheap/congruence.ml | 30 ++++++++++++++---------------- sledge/src/symbheap/exec.ml | 4 ++-- sledge/src/symbheap/sh.ml | 8 ++++---- sledge/src/symbheap/solver.ml | 5 ++--- sledge/src/trace/trace.ml | 4 ---- sledge/src/trace/trace.mli | 3 --- 7 files changed, 24 insertions(+), 34 deletions(-) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 837922495..83ec1cf4e 100644 --- a/sledge/src/llair/exp.ml +++ b/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 - "simplifying %a %a yields %a with new subexp %a" + || Trace.fail + "simplifying %a %a@ yields %a@ with new subexp %a" pp op pp arg pp e pp a ) | _ -> () ) ) diff --git a/sledge/src/symbheap/congruence.ml b/sledge/src/symbheap/congruence.ml index 81029dd21..6095740e4 100644 --- a/sledge/src/symbheap/congruence.ml +++ b/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@]" - Exp.pp bj Exp.pp a pp r ) ) ; + || Trace.fail "@[subexp %a of %a not in carrier of@ %a@]" Exp.pp + 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 - "every app rep should be its own rep: %a @<2>↦ %a" Exp.pp a - Exp.pp a' ) ; + || Trace.fail "every app rep should be its own rep: %a @<2>↦ %a" + Exp.pp a Exp.pp a' ) ; match Map.find r.cls a' with | None -> (* every rep in dom of cls *) - assert ( - Trace.report "rep not in dom of cls: %a@\n%a" Exp.pp a' pp r ) + assert (Trace.fail "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 - Exp.pp c_' Exp.pp a ) ; + || Trace.fail "%a sub-normalizes to %a @<2>≠ %a" Exp.pp c Exp.pp + 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) -> diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index 0005295b1..f17cc30ec 100644 --- a/sledge/src/symbheap/exec.ml +++ b/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 diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 4d8df9839..a2f85a9f0 100644 --- a/sledge/src/symbheap/sh.ml +++ b/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 - (Set.inter us xs) pp q ) ; + || Trace.fail "inter: @[%a@]@\nq: @[%a@]" Var.Set.pp (Set.inter us xs) + 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] diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml index b0b7c3ba2..86e8a20b1 100644 --- a/sledge/src/symbheap/solver.ml +++ b/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 gain || Trace.report "gained: %a" Var.Set.pp gain ) + 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) )] diff --git a/sledge/src/trace/trace.ml b/sledge/src/trace/trace.ml index 3990ad6a7..b90460686 100644 --- a/sledge/src/trace/trace.ml +++ b/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 diff --git a/sledge/src/trace/trace.mli b/sledge/src/trace/trace.mli index 389d2edc5..8fd32d7a3 100644 --- a/sledge/src/trace/trace.mli +++ b/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]. *)