From adb1e484673cdfa7c9afc05fd1d8ba7fdb877149 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 8 Jan 2020 09:09:47 -0800 Subject: [PATCH] [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 | 1 + sledge/src/symbheap/sh.ml | 73 ++++++++++++++++++++++++------ sledge/src/symbheap/sh.mli | 1 - sledge/src/symbheap/solver_test.ml | 15 +++--- 4 files changed, 65 insertions(+), 25 deletions(-) diff --git a/sledge/src/llair/term.mli b/sledge/src/llair/term.mli index 7e2e0833e..3c7318e44 100644 --- a/sledge/src/llair/term.mli +++ b/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 diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 449c8959d..167ad640a 100644 --- a/sledge/src/symbheap/sh.ml +++ b/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 - ~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) )) ; + pp_heap ~is_x ~pre:(if first then " " else "@ @<2>∧ ") cong fs heap ; let first = first && List.is_empty heap in List.pp ~pre:(if first then " " else "@ * ") diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli index d288efe24..874d65bed 100644 --- a/sledge/src/symbheap/sh.mli +++ b/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 diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml index aadf44a93..edc1bb65c 100644 --- a/sledge/src/symbheap/solver_test.ml +++ b/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) -[ %l_6, 16 )-> ⟨8,%a_2⟩ + %l_6 -[)-> ⟨8,%a_1⟩^⟨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) -[ %l_6, 16 )-> ⟨8,%a_2⟩ + %l_6 -[)-> ⟨8,%a_1⟩^⟨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) -[ %l_6, 16 )-> ⟨8,%a_2⟩ + %l_6 -[)-> ⟨8,%a_1⟩^⟨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 )