[sledge] Simplify printing of symbolic heaps

Summary:
Reduce redundancy by printing adjacent segments as if they had been
concatenated together.

Reviewed By: ngorogiannis

Differential Revision: D19221881

fbshipit-source-id: 613105864

sledge/src/llair/term.mli

@@ -242,5 +242,6 @@ val fold_terms : t -> init:'a -> f:('a -> t -> 'a) -> 'a
 val fv : t -> Var.Set.t
 val is_true : t -> bool
 val is_false : t -> bool
+val is_constant : t -> bool
 val classify : t -> [> `Atomic | `Interpreted | `Simplified | `Uninterpreted]
 val solve : t -> t -> t Map.t option

sledge/src/symbheap/sh.ml

@@ -39,6 +39,63 @@ let pp_seg ?is_x fs {loc; bas; len; siz; arr} =
 let pp_seg_norm cong fs seg =
   pp_seg fs (map_seg seg ~f:(Equality.normalize cong))
 
+let pp_block ?is_x fs segs =
+  let is_full_alloc segs =
+    match segs with
+    | {loc; bas; len; _} :: _ -> (
+        Term.equal loc bas
+        &&
+        match len with
+        | Integer {data} -> (
+          match
+            List.fold segs ~init:(Some Z.zero) ~f:(fun len seg ->
+                match (len, seg.siz) with
+                | Some len, Integer {data} -> Some (Z.add len data)
+                | _ -> None )
+          with
+          | Some blk_len -> Z.equal data blk_len
+          | _ -> false )
+        | _ -> false )
+    | [] -> false
+  in
+  let term_pp = Term.pp_full ?is_x in
+  let pp_mems =
+    List.pp "@,^" (fun fs seg ->
+        term_pp fs (Term.memory ~siz:seg.siz ~arr:seg.arr) )
+  in
+  match segs with
+  | {loc; bas; len; _} :: _ ->
+      Format.fprintf fs "@[<2>%a@ @[@[-[%t)->@]@ @[%a@]@]@]" term_pp loc
+        (fun fs ->
+          if not (is_full_alloc segs) then
+            Format.fprintf fs " %a, %a " term_pp bas term_pp len )
+        pp_mems segs
+  | [] -> ()
+
+let pp_heap ?is_x ?pre cong fs heap =
+  let bas_off = function
+    | Term.Add poly as sum ->
+        let const = Qset.count poly Term.one in
+        (Term.sub sum (Term.rational const), const)
+    | e -> (e, Q.zero)
+  in
+  let compare s1 s2 =
+    [%compare: Term.t * (Term.t * Q.t)]
+      (s1.bas, bas_off s1.loc)
+      (s2.bas, bas_off s2.loc)
+  in
+  let break s1 s2 =
+    (not (Term.equal s1.bas s2.bas))
+    || (not (Term.equal s1.len s2.len))
+    || not (Term.is_constant (Term.sub s2.loc s1.loc))
+  in
+  let blocks =
+    List.group ~break
+      (List.sort ~compare
+         (List.map ~f:(map_seg ~f:(Equality.normalize cong)) heap))
+  in
+  List.pp ?pre "@ * " (pp_block ?is_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]
@@ -71,21 +128,7 @@ let rec pp vs all_xs fs {us; xs; cong; pure; heap; djns} =
       ( if first then if List.is_empty djns then "  emp" else ""
       else "@ @<5>∧ emp" )
   else
-    List.pp
+    pp_heap ~is_x ~pre:(if first then "  " else "@ @<2>∧ ") cong fs heap ;
-      ~pre:(if first then "  " else "@ @<2>∧ ")
-      "@ * " (pp_seg ~is_x) fs
-      (List.sort
-         (List.map ~f:(map_seg ~f:(Equality.normalize cong)) heap)
-         ~compare:(fun s1 s2 ->
-           let b_o = function
-             | Term.Add poly as sum ->
-                 let const = Qset.count poly Term.one in
-                 (Term.sub sum (Term.rational const), const)
-             | e -> (e, Q.zero)
-           in
-           [%compare: Term.t * (Term.t * Q.t)]
-             (s1.bas, b_o s1.loc)
-             (s2.bas, b_o s2.loc) )) ;
   let first = first && List.is_empty heap in
   List.pp
     ~pre:(if first then "  " else "@ * ")

sledge/src/symbheap/sh.mli

@@ -25,7 +25,6 @@ and disjunction = starjunction list
 
 type t = starjunction [@@deriving equal, compare, sexp]
 
-val pp_seg : ?is_x:(Term.t -> bool) -> seg pp
 val pp_seg_norm : Equality.t -> seg pp
 val pp_us : ?pre:('a, 'a) fmt -> Var.Set.t pp
 val pp : t pp

sledge/src/symbheap/solver_test.ml

@@ -132,8 +132,7 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            %l_6 -[ %l_6, 16 )-> ⟨8,%a_1⟩
+            %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩
-          * (%l_6 + 8) -[ %l_6, 16 )-> ⟨8,%a_2⟩
           \- ∃ %a_3 .
               %l_6 -[)-> ⟨16,%a_3⟩
         ) infer_frame:
@@ -149,8 +148,7 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            %l_6 -[ %l_6, 16 )-> ⟨8,%a_1⟩
+            %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩
-          * (%l_6 + 8) -[ %l_6, 16 )-> ⟨8,%a_2⟩
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩
         ) infer_frame:
@@ -170,10 +168,9 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            %l_6 -[ %l_6, 16 )-> ⟨8,%a_1⟩
+            %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩
-          * (%l_6 + 8) -[ %l_6, 16 )-> ⟨8,%a_2⟩
           \- ∃ %a_3, %m_8 .
-              %l_6 -[)-> ⟨%m_8,%a_3⟩
+              %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩
         ) infer_frame:
           ∃ %a1_9 .
             %a_2 = %a1_9
@@ -249,7 +246,7 @@ let%test_module _ =
             ∨ (  1 = %n_9 ∧ emp)
             )
           \- ∃ %a_1, %m_8 .
-              %l_6 -[)-> ⟨%m_8,%a_1⟩
+              %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame:
             ( (  %a_1 = %a_2
                ∧ 2 = %n_9
@@ -282,6 +279,6 @@ let%test_module _ =
           ∧ (%l_6 + 8 × %n_9) -[ %l_6, 16 )-> ⟨(-8 × %n_9 + 16),%a_3⟩
           * %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩
           \- ∃ %a_1, %m_8 .
-              %l_6 -[)-> ⟨%m_8,%a_1⟩
+              %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame: |}]
   end )