[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

@@ -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

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

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@,@[<hv>{%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

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 =
+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,6 +206,8 @@ 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 =
+    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' )
@@ -236,7 +244,7 @@ and pp_djn ?var_strength vs xs cong fs = function
              in
              Format.fprintf fs "@[<hv 1>(%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 =

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

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, %x_2 .   2 = %x_2 ∧ (%x_2 = 2) ∧ emp)
-        ∨ (∃ %x_1 .   1 = %x_1 = %y_2 ∧ emp)
+        ∨ (∃ %x_1 .   1 = %x_1 = %y_2 ∧ (%x_1 = 1) ∧ (%y_2 = 1) ∧ emp)
-        ∨ (  0 = %x_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, %x_4 .   2 = %x_4 ∧ (%x_4 = 2) ∧ emp)
-        ∨ (∃ %x_1, %x_3 .   1 = %y_2 = %x_3 ∧ emp)
+        ∨ (∃ %x_1, %x_3 .   1 = %y_2 = %x_3 ∧ (%y_2 = 1) ∧ (%x_3 = 1) ∧ emp)
-        ∨ (∃ %x_1 .   0 = %x_1 ∧ emp)
+        ∨ (∃ %x_1 .   0 = %x_1 ∧ (%x_1 = 0) ∧ emp)
         ) |}]
 
     let%expect_test _ =