From 551a03c4c93e332598547db08490a109df46650c Mon Sep 17 00:00:00 2001
From: Timotej Kapus <kapust@fb.com>
Date: Thu, 13 Jun 2019 01:58:29 -0700
Subject: [PATCH] [sledge] Simplify the printed symbolic heaps

Summary:
Currently printing symbolic heaps is unreadable, because there are too
many quantified variables, that are mostly just equal to other
variables.

This diff tries to replace all variables in an equivalence class with a
single variable and remove the unneccesary variables.

It also introduces two modes for printing state domains:
`-t +State_domain.pp_full` prints the state domain as is
`-t +State_domain.pp` uses the simplification before printing.

Reviewed By: jberdine

Differential Revision: D15738748

fbshipit-source-id: 7c85b580e
---
 sledge/src/symbheap/sh.ml           | 16 ++++++++++++++++
 sledge/src/symbheap/sh.mli          |  1 +
 sledge/src/symbheap/sh_test.ml      | 26 ++++++++++++++++++++++++++
 sledge/src/symbheap/state_domain.ml |  8 +++++++-
 4 files changed, 50 insertions(+), 1 deletion(-)

diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index 1e7bd30d1..7b1931bbb 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -159,6 +159,22 @@ let rec invariant q =
             invariant sjn ) )
   with exc -> [%Trace.info "%a" pp q] ; raise exc
 
+let rec simplify {us; xs; cong; pure; heap; djns} =
+  [%Trace.call fun {pf} -> pf "%a" pp {us; xs; cong; pure; heap; djns}]
+  ;
+  let heap = List.map heap ~f:(map_seg ~f:(Equality.normalize cong)) in
+  let pure = List.map pure ~f:(Equality.normalize cong) in
+  let cong = Equality.true_ in
+  let djns = List.map djns ~f:(List.map ~f:simplify) in
+  let all_vars =
+    fv {us= Set.union us xs; xs= Var.Set.empty; cong; pure; heap; djns}
+  in
+  let xs = Set.inter all_vars xs in
+  let us = Set.inter all_vars us in
+  {us; xs; cong; pure; heap; djns} |> check invariant
+  |>
+  [%Trace.retn fun {pf} s -> pf "%a" pp s]
+
 (** Quantification and Vocabulary *)
 
 let rename_seg sub ({loc; bas; len; siz; arr} as h) =
diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli
index 927e61482..da8b6ef9c 100644
--- a/sledge/src/symbheap/sh.mli
+++ b/sledge/src/symbheap/sh.mli
@@ -30,6 +30,7 @@ val pp_seg_norm : Equality.t -> seg pp
 val pp_us : ?pre:('a, 'a) fmt -> Var.Set.t pp
 val pp : t pp
 val pp_djn : disjunction pp
+val simplify : t -> t
 
 include Invariant.S with type t := t
 
diff --git a/sledge/src/symbheap/sh_test.ml b/sledge/src/symbheap/sh_test.ml
index 89c94b13a..cd5ce0c18 100644
--- a/sledge/src/symbheap/sh_test.ml
+++ b/sledge/src/symbheap/sh_test.ml
@@ -89,4 +89,30 @@ let%test_module _ =
         ∨ (∃ %x_1, %x_3 .   1 = %y_2 = %x_3 ∧ emp)
         ∨ (∃ %x_1 .   0 = %x_1 ∧ emp)
         ) |}]
+
+    let%expect_test _ =
+      let q =
+        Sh.(
+          exists
+            ~$[x_]
+            (or_
+               (pure (x = !0))
+               (exists
+                  ~$[x_]
+                  (or_
+                     (and_ (x = !1) (pure (y = !1)))
+                     (exists ~$[x_] (pure (x = !2)))))))
+      in
+      pp q ;
+      pp (Sh.simplify q) ;
+      [%expect
+        {|
+        ∃ %x_1 .
+        emp
+        * ( (  0 = %x_1 ∧ emp)
+          ∨ (∃ %x_1 .emp
+             * ( (  1 = %x_1 = %y_2 ∧ emp) ∨ (∃ %x_1 .  2 = %x_1 ∧ emp) ))
+          )
+
+        emp * ( (emp) ∨ (emp * ( (emp) ∨ (emp) )) ) |}]
   end )
diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml
index 5fddd5304..a58ff7c91 100644
--- a/sledge/src/symbheap/state_domain.ml
+++ b/sledge/src/symbheap/state_domain.ml
@@ -9,7 +9,13 @@
 
 type t = Sh.t [@@deriving equal, sexp_of]
 
-let pp = Sh.pp
+let pp_full fs s = [%Trace.fprintf fs "%a" Sh.pp s]
+let pp fs s = [%Trace.fprintf fs "%a" Sh.pp (Sh.simplify s)]
+let pp fs s = pp_full fs s ; pp fs s
+
+(* I think it would be nice if `-t State_domain.pp` enabled the simplified
+   printing, with `-t State_domain.pp_full` for the more verbose one. So how
+   about this renaming? *)
 
 let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function