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 ;