[sledge] Revise Report printing

Summary:
The report output got disturbed by the change from predicate to
relational Domain, and the tricky control of printing simplified
states. After this diff by default states are printed in full, and in
simplified form with `-t State_domain.pp_simp`.

Also includes some minor output improvements.

Reviewed By: kren1

Differential Revision: D16059780

fbshipit-source-id: b33289887

sledge/src/control.ml

@@ -405,7 +405,7 @@ let exec_term :
                   callee.name.var args
               with
             | Some (Error ()) ->
-                Report.invalid_access_term state block.term ;
+                Report.invalid_access_term (Domain.project state) block.term ;
                 Work.skip
             | Some (Ok state) -> exec_goto stk state block return
             | None when Llair.Func.is_undefined callee ->
@@ -438,7 +438,7 @@ let exec_block :
   match Vector.fold_result ~f:exec_inst ~init:state block.cmnd with
   | Ok state -> exec_term ~opts pgm stk state block
   | Error (state, inst) ->
-      Report.invalid_access_inst state inst ;
+      Report.invalid_access_inst (Domain.project state) inst ;
       Work.skip
 
 let harness : opts:exec_opts -> Llair.t -> (int -> Work.t) option =

sledge/src/report.ml

@@ -25,15 +25,13 @@ let unknown_call call =
       call Llair.Term.pp call]
 
 let invalid_access state pp access loc =
-  Format.printf
-    "@\n@[<v 2>%a Invalid memory access executing@;<1 2>@[%a@]@]@." Loc.pp
+  Format.printf "@\n@[<v 2>%a Invalid memory access@;<1 2>@[%a@]@]@." Loc.pp
     (loc access) pp access ;
   [%Trace.kprintf
     (fun _ -> assert false)
       "@\n\
-       @[<v 2>%a Invalid memory access executing@;<1 2>@[%a@]@ from \
-       symbolic state@;<1 2>@[{ %a@ }@]@]@."
-      Loc.pp (loc access) pp access Domain.pp state]
+       @[<v 2>%a Invalid memory access@;<1 2>@[%a@]@;<1 2>@[{ %a@ }@]@]@."
+      Loc.pp (loc access) pp access State_domain.pp state]
 
 let invalid_access_inst state inst =
   invalid_access state Llair.Inst.pp inst Llair.Inst.loc

sledge/src/report.mli

@@ -8,5 +8,5 @@
 (** Issue reporting *)
 
 val unknown_call : Llair.term -> unit
-val invalid_access_inst : Domain.t -> Llair.inst -> unit
-val invalid_access_term : Domain.t -> Llair.term -> unit
+val invalid_access_inst : State_domain.t -> Llair.inst -> unit
+val invalid_access_term : State_domain.t -> Llair.term -> unit

sledge/src/symbheap/domain.ml

@@ -9,13 +9,14 @@
 
 type t = State_domain.t * State_domain.t
 
+let embed q = (q, q)
+let project (_, curr) = curr
+
 let pp fs (entry, current) =
   Format.fprintf fs "@[<v 1> entry: %a@;current: %a@]" State_domain.pp entry
     State_domain.pp current
 
-let init globals =
-  let init_state = State_domain.init globals in
-  (init_state, init_state)
+let init globals = embed (State_domain.init globals)
 
 let join (entry_a, current_a) (entry_b, current_b) =
   assert (State_domain.equal entry_b entry_a) ;

sledge/src/symbheap/domain.mli

@@ -9,6 +9,7 @@
 
 type t
 
+val project : t -> State_domain.t
 val pp : t pp
 val init : Global.t vector -> t
 val join : t -> t -> t

sledge/src/symbheap/sh.ml

@@ -64,7 +64,9 @@ let rec pp vs fs {us; xs; cong; pure; heap; djns} =
     "@ @<2>∧ " Exp.pp fs pure_exps ;
   let first = first && List.is_empty pure_exps in
   if List.is_empty heap then
-    Format.fprintf fs (if first then "emp" else "@ @<5>∧ emp")
+    Format.fprintf fs
+      ( if first then if List.is_empty djns then "  emp" else ""
+      else "@ @<5>∧ emp" )
   else
     List.pp
       ~pre:(if first then "  " else "@ @<2>∧ ")
@@ -80,7 +82,10 @@ let rec pp vs fs {us; xs; cong; pure; heap; djns} =
            [%compare: Exp.t * (Exp.t * Z.t)]
              (s1.bas, b_o s1.loc)
              (s2.bas, b_o s2.loc) )) ;
-  List.pp ~pre:"@ * " "@ * "
+  let first = first && List.is_empty heap in
+  List.pp
+    ~pre:(if first then "  " else "@ * ")
+    "@ * "
     (pp_djn (Set.union vs (Set.union us xs)))
     fs djns ;
   Format.pp_close_box fs ()

sledge/src/symbheap/sh_test.ml

@@ -50,10 +50,10 @@ let%test_module _ =
       pp_djn (Sh.dnf q) ;
       [%expect
         {|
-        emp
-        * ( (  0 = %x_1 ∧ emp)
-          ∨ (∃ %x_1 .emp
-             * ( (  1 = %x_1 = %y_2 ∧ emp) ∨ (∃ %x_1 .  2 = %x_1 ∧ emp) ))
+          ( (  0 = %x_1 ∧ emp)
+          ∨ (∃ %x_1 .  ( (  1 = %x_1 = %y_2 ∧ emp)
+                       ∨ (∃ %x_1 .  2 = %x_1 ∧ emp)
+                       ))
           )
 
         ( (∃ %x_1, %x_2 .   2 = %x_2 ∧ emp)
@@ -79,10 +79,10 @@ let%test_module _ =
       [%expect
         {|
         ∃ %x_1 .
-        emp
-        * ( (  0 = %x_1 ∧ emp)
-          ∨ (∃ %x_1 .emp
-             * ( (  1 = %x_1 = %y_2 ∧ emp) ∨ (∃ %x_1 .  2 = %x_1 ∧ emp) ))
+          ( (  0 = %x_1 ∧ emp)
+          ∨ (∃ %x_1 .  ( (  1 = %x_1 = %y_2 ∧ emp)
+                       ∨ (∃ %x_1 .  2 = %x_1 ∧ emp)
+                       ))
           )
 
         ( (∃ %x_1, %x_3, %x_4 .   2 = %x_4 ∧ emp)
@@ -108,11 +108,11 @@ let%test_module _ =
       [%expect
         {|
         ∃ %x_1 .
-        emp
-        * ( (  0 = %x_1 ∧ emp)
-          ∨ (∃ %x_1 .emp
-             * ( (  1 = %x_1 = %y_2 ∧ emp) ∨ (∃ %x_1 .  2 = %x_1 ∧ emp) ))
+          ( (  0 = %x_1 ∧ emp)
+          ∨ (∃ %x_1 .  ( (  1 = %x_1 = %y_2 ∧ emp)
+                       ∨ (∃ %x_1 .  2 = %x_1 ∧ emp)
+                       ))
           )
 
-        emp * ( (emp) ∨ (emp * ( (emp) ∨ (emp) )) ) |}]
+          ( (  emp) ∨ (  ( (  emp) ∨ (  emp) )) ) |}]
   end )

sledge/src/symbheap/solver_test.ml

@@ -57,8 +57,8 @@ let%test_module _ =
       check_frame (Sh.false_ Var.Set.empty) [] Sh.emp ;
       [%expect
         {|
-        ( infer_frame: emp * false \- emp
-        ) infer_frame: emp * false |}]
+        ( infer_frame:   false \-   emp
+        ) infer_frame:   false |}]
 
     let%expect_test _ =
       check_frame Sh.emp [n_; m_] (Sh.and_ (Exp.eq m n) Sh.emp) ;
@@ -232,8 +232,7 @@ let%test_module _ =
           \- ∃ %a_1, %m_8 .
               %l_6 -[)-> ⟨%m_8,%a_1⟩
         ) infer_frame:
-          emp
-          * ( (  %a_1 = %a_2
+            ( (  %a_1 = %a_2
                ∧ 2 = %n_9
                ∧ 16 = %m_8
                ∧ (%l_6 + 16) -[ %l_6, 16 )-> ⟨0,%a_3⟩)

sledge/src/symbheap/state_domain.ml

@@ -9,9 +9,12 @@
 
 type t = Sh.t [@@deriving equal, sexp_of]
 
-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
+let pp_simp fs q =
+  let q' = ref q in
+  [%Trace.printf "%a" (fun _ q -> q' := Sh.simplify q) q] ;
+  Sh.pp fs !q'
+
+let pp = pp_simp
 
 let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function

sledge/src/trace/trace.ml

@@ -77,7 +77,7 @@ let parse s =
       Ok {none with trace_mods_funs}
   with Assert_failure _ as exn -> Error exn
 
-let init ?(margin = 300) ~config:c () =
+let init ?(margin = 240) ~config:c () =
   Format.set_margin margin ;
   Format.set_max_indent (margin - 1) ;
   Format.pp_set_margin fs margin ;