From 8be5dbec0b1f69b34fe62b50f0810a976ac51dab Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 1 Jul 2019 07:16:21 -0700 Subject: [PATCH] [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 | 4 ++-- sledge/src/report.ml | 8 +++----- sledge/src/report.mli | 4 ++-- sledge/src/symbheap/domain.ml | 7 ++++--- sledge/src/symbheap/domain.mli | 1 + sledge/src/symbheap/sh.ml | 9 +++++++-- sledge/src/symbheap/sh_test.ml | 28 ++++++++++++++-------------- sledge/src/symbheap/solver_test.ml | 19 +++++++++---------- sledge/src/symbheap/state_domain.ml | 9 ++++++--- sledge/src/trace/trace.ml | 2 +- 10 files changed, 49 insertions(+), 42 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 25dfeeb84..96d579f7b 100644 --- a/sledge/src/control.ml +++ b/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 = diff --git a/sledge/src/report.ml b/sledge/src/report.ml index 6f5656c2a..f5e135cd0 100644 --- a/sledge/src/report.ml +++ b/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@[%a Invalid memory access executing@;<1 2>@[%a@]@]@." Loc.pp + Format.printf "@\n@[%a Invalid memory access@;<1 2>@[%a@]@]@." Loc.pp (loc access) pp access ; [%Trace.kprintf (fun _ -> assert false) "@\n\ - @[%a Invalid memory access executing@;<1 2>@[%a@]@ from \ - symbolic state@;<1 2>@[{ %a@ }@]@]@." - Loc.pp (loc access) pp access Domain.pp state] + @[%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 diff --git a/sledge/src/report.mli b/sledge/src/report.mli index 596f9f336..8daccdb58 100644 --- a/sledge/src/report.mli +++ b/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 diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml index 4f25bbf9e..364e09205 100644 --- a/sledge/src/symbheap/domain.ml +++ b/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 "@[ 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) ; diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli index e7c48a83a..346cbd824 100644 --- a/sledge/src/symbheap/domain.mli +++ b/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 diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 3fae3dd4f..010c224e8 100644 --- a/sledge/src/symbheap/sh.ml +++ b/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 () diff --git a/sledge/src/symbheap/sh_test.ml b/sledge/src/symbheap/sh_test.ml index cd5ce0c18..3cb8be62d 100644 --- a/sledge/src/symbheap/sh_test.ml +++ b/sledge/src/symbheap/sh_test.ml @@ -29,7 +29,7 @@ let%test_module _ = pp (Sh.star p q) ; [%expect {| - ∃ %x_1 . emp + ∃ %x_1 . emp 0 = %x_1 ∧ emp @@ -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 ) diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml index 29a3523f6..21a0a3f79 100644 --- a/sledge/src/symbheap/solver_test.ml +++ b/sledge/src/symbheap/solver_test.ml @@ -50,22 +50,22 @@ let%test_module _ = check_frame Sh.emp [] Sh.emp ; [%expect {| - ( infer_frame: emp \- emp - ) infer_frame: emp |}] + ( infer_frame: emp \- emp + ) infer_frame: emp |}] let%expect_test _ = 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) ; [%expect {| - ( infer_frame: emp \- ∃ %m_8, %n_9 . %m_8 = %n_9 ∧ emp - ) infer_frame: emp |}] + ( infer_frame: emp \- ∃ %m_8, %n_9 . %m_8 = %n_9 ∧ emp + ) infer_frame: emp |}] let%expect_test _ = check_frame @@ -73,7 +73,7 @@ let%test_module _ = [] Sh.emp ; [%expect {| - ( infer_frame: %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ \- emp + ( infer_frame: %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ \- emp ) infer_frame: %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ |}] let%expect_test _ = @@ -86,7 +86,7 @@ let%test_module _ = ( infer_frame: %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ \- %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ - ) infer_frame: emp |}] + ) infer_frame: emp |}] let%expect_test _ = check_frame @@ -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⟩) diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index af5a984b0..9fdc5e93a 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/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 diff --git a/sledge/src/trace/trace.ml b/sledge/src/trace/trace.ml index 6f421d142..0130df972 100644 --- a/sledge/src/trace/trace.ml +++ b/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 ;