From 33e702cd8b2136d085c3eb997561693d573655c6 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 2 Mar 2020 08:43:48 -0800 Subject: [PATCH] [sledge] Improve Sh printing for Sh-internal tracing Summary: Add `Sh.pp_raw` which is closer to the representation, for use when tracing `Sh` operations. Reviewed By: ngorogiannis Differential Revision: D20120281 fbshipit-source-id: e3b1b531a --- sledge/src/import/import.ml | 6 ++++++ sledge/src/import/import.mli | 1 + sledge/src/symbheap/exec.ml | 2 +- sledge/src/symbheap/sh.ml | 25 +++++++++++++++++-------- sledge/src/symbheap/sh.mli | 3 ++- sledge/src/symbheap/sh_test.ml | 12 ++++++------ 6 files changed, 33 insertions(+), 16 deletions(-) diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml index 12be86106..d9a5be4d0 100644 --- a/sledge/src/import/import.ml +++ b/sledge/src/import/import.ml @@ -333,6 +333,12 @@ module Set = struct let equal_m__t (module Elt : Compare_m) = equal let pp pp_elt fs x = List.pp ",@ " pp_elt fs (to_list x) + + let pp_diff pp_elt fs (xs, ys) = + let lose = diff xs ys and gain = diff ys xs in + if not (is_empty lose) then Format.fprintf fs "-- %a" (pp pp_elt) lose ; + if not (is_empty gain) then Format.fprintf fs "++ %a" (pp pp_elt) gain + let disjoint x y = is_empty (inter x y) let add_option yo x = Option.fold ~f:add ~init:x yo let add_list ys x = List.fold ~f:add ~init:x ys diff --git a/sledge/src/import/import.mli b/sledge/src/import/import.mli index ca256ba94..57e6c5d87 100644 --- a/sledge/src/import/import.mli +++ b/sledge/src/import/import.mli @@ -248,6 +248,7 @@ module Set : sig (module Compare_m) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> bool val pp : 'e pp -> ('e, 'c) t pp + val pp_diff : 'e pp -> (('e, 'c) t * ('e, 'c) t) pp val disjoint : ('e, 'c) t -> ('e, 'c) t -> bool val add_option : 'e option -> ('e, 'c) t -> ('e, 'c) t val add_list : 'e list -> ('e, 'c) t -> ('e, 'c) t diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index e3c2d8f10..0f549b264 100644 --- a/sledge/src/symbheap/exec.ml +++ b/sledge/src/symbheap/exec.ml @@ -610,7 +610,7 @@ let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) = let exec_spec pre0 {xs; foot; sub; ms; post} = ([%Trace.call fun {pf} -> pf "@[%a@]@ @[<2>%a@,@[{%a %a}@;<1 -1>%a--@ {%a }@]@]" Sh.pp pre0 - (Sh.pp_us ~pre:"@<2>∀ ") + (Sh.pp_us ~pre:"@<2>∀ " ()) xs Sh.pp foot (fun fs sub -> if not (Var.Subst.is_empty sub) then diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 1bd117897..5c028ca27 100644 --- a/sledge/src/symbheap/sh.ml +++ b/sledge/src/symbheap/sh.ml @@ -177,15 +177,21 @@ let pp_heap x ?pre cong fs heap = let blocks = List.group ~break (List.sort ~compare heap) in List.pp ?pre "@ * " (pp_block x) fs blocks -let pp_us ?(pre = ("" : _ fmt)) fs us = - if not (Set.is_empty us) then - [%Trace.fprintf fs "%( %)@[%a@] .@ " pre Var.Set.pp us] +let pp_us ?(pre = ("" : _ fmt)) ?vs () fs us = + match vs with + | None -> + if not (Set.is_empty us) then + [%Trace.fprintf fs "%( %)@[%a@] .@ " pre Var.Set.pp us] + | Some vs -> + if not (Set.equal vs us) then + [%Trace.fprintf + fs "%( %)@[%a@] .@ " pre (Set.pp_diff Var.pp) (vs, us)] let rec pp_ ?var_strength vs parent_xs parent_cong fs {us; xs; cong; pure; heap; djns} = Format.pp_open_hvbox fs 0 ; let x v = Option.bind ~f:(fun (_, m) -> Map.find m v) var_strength in - pp_us fs us ; + pp_us ~vs () fs us ; let xs_d_vs, xs_i_vs = Set.diff_inter (Set.filter xs ~f:(fun v -> Poly.(x v <> Some `Anonymous))) @@ -200,9 +206,11 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs if not first then Format.fprintf fs " " ; Equality.ppx_classes_diff x fs (parent_cong, cong) ; let pure = - List.filter_map pure ~f:(fun e -> - let e' = Equality.normalize cong e in - if Term.is_true e' then None else Some e' ) + if Option.is_none var_strength then pure + else + List.filter_map pure ~f:(fun e -> + let e' = Equality.normalize cong e in + if Term.is_true e' then None else Some e' ) in List.pp ~pre:(if first then "@[ " else "@ @[@<2>∧ ") @@ -236,7 +244,7 @@ and pp_djn ?var_strength vs xs cong fs = function in Format.fprintf fs "@[(%a)@]" (pp_ ?var_strength vs (Set.union xs sjn.xs) cong) - {sjn with us= Set.diff sjn.us vs} )) + sjn )) djn let pp_diff_eq cong fs q = @@ -245,6 +253,7 @@ let pp_diff_eq cong fs q = let pp fs q = pp_diff_eq Equality.true_ fs q let pp_djn fs d = pp_djn Var.Set.empty Var.Set.empty Equality.true_ fs d +let pp_raw fs q = pp_ Var.Set.empty Var.Set.empty Equality.true_ fs q let fv_seg seg = fold_vars_seg seg ~f:Set.add ~init:Var.Set.empty let fv ?ignore_cong q = diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli index c7a28f006..4b104c3f6 100644 --- a/sledge/src/symbheap/sh.mli +++ b/sledge/src/symbheap/sh.mli @@ -26,8 +26,9 @@ and disjunction = starjunction list type t = starjunction [@@deriving equal, compare, sexp] val pp_seg_norm : Equality.t -> seg pp -val pp_us : ?pre:('a, 'a) fmt -> Var.Set.t pp +val pp_us : ?pre:('a, 'a) fmt -> ?vs:Var.Set.t -> unit -> Var.Set.t pp val pp : t pp +val pp_raw : t pp val pp_diff_eq : Equality.t -> t pp val pp_djn : disjunction pp val simplify : t -> t diff --git a/sledge/src/symbheap/sh_test.ml b/sledge/src/symbheap/sh_test.ml index b34452934..97219d7f1 100644 --- a/sledge/src/symbheap/sh_test.ml +++ b/sledge/src/symbheap/sh_test.ml @@ -55,9 +55,9 @@ let%test_module _ = ∨ ( ( ( 1 = _ = %y_2 ∧ emp) ∨ ( 2 = _ ∧ emp) )) ) - ( (∃ %x_1, %x_2 . 2 = %x_2 ∧ emp) - ∨ (∃ %x_1 . 1 = %x_1 = %y_2 ∧ emp) - ∨ ( 0 = %x_1 ∧ emp) + ( (∃ %x_1, %x_2 . 2 = %x_2 ∧ (%x_2 = 2) ∧ emp) + ∨ (∃ %x_1 . 1 = %x_1 = %y_2 ∧ (%x_1 = 1) ∧ (%y_2 = 1) ∧ emp) + ∨ ( 0 = %x_1 ∧ (%x_1 = 0) ∧ emp) ) |}] let%expect_test _ = @@ -81,9 +81,9 @@ let%test_module _ = ∨ ( ( ( 1 = _ = %y_2 ∧ emp) ∨ ( 2 = _ ∧ emp) )) ) - ( (∃ %x_1, %x_3, %x_4 . 2 = %x_4 ∧ emp) - ∨ (∃ %x_1, %x_3 . 1 = %y_2 = %x_3 ∧ emp) - ∨ (∃ %x_1 . 0 = %x_1 ∧ emp) + ( (∃ %x_1, %x_3, %x_4 . 2 = %x_4 ∧ (%x_4 = 2) ∧ emp) + ∨ (∃ %x_1, %x_3 . 1 = %y_2 = %x_3 ∧ (%y_2 = 1) ∧ (%x_3 = 1) ∧ emp) + ∨ (∃ %x_1 . 0 = %x_1 ∧ (%x_1 = 0) ∧ emp) ) |}] let%expect_test _ =