From 2f0a0cf28834e538aa951d80bcb4891b26257b22 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 10 Jan 2020 15:46:36 -0800 Subject: [PATCH] [sledge] Replace Memory and Concat Term constructors with eq_concat Summary: The exposed constructors for Memory and Concat Terms are only used in a very special idiom: to construct an equality between a single Memory chunk and the Concat of multiple Memory chunks. This diff specializes and simplifies by exposing a Term.eq_concat constructor for this idiom, and removes the underlying Term.memory and Term.concat constructors. Reviewed By: ngorogiannis Differential Revision: D19221866 fbshipit-source-id: 4842737d2 --- sledge/src/llair/term.ml | 4 +++ sledge/src/llair/term.mli | 3 +- sledge/src/symbheap/exec.ml | 57 +++++++++-------------------------- sledge/src/symbheap/sh.ml | 9 ++++-- sledge/src/symbheap/solver.ml | 56 ++++++---------------------------- 5 files changed, 36 insertions(+), 93 deletions(-) diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index 679b96932..7bac1c42e 100644 --- a/sledge/src/llair/term.ml +++ b/sledge/src/llair/term.ml @@ -895,6 +895,10 @@ let select ~rcd ~idx = norm1 (Select idx) rcd let update ~rcd ~idx ~elt = norm2 (Update idx) rcd elt let size_of t = integer (Z.of_int (Typ.size_of t)) +let eq_concat (siz, arr) ms = + eq (memory ~siz ~arr) + (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms)) + (** Transform *) let map e ~f = diff --git a/sledge/src/llair/term.mli b/sledge/src/llair/term.mli index b2148f646..bdc28fcf6 100644 --- a/sledge/src/llair/term.mli +++ b/sledge/src/llair/term.mli @@ -213,8 +213,7 @@ val conditional : cnd:t -> thn:t -> els:t -> t (* memory contents *) val splat : t -> t -val memory : siz:t -> arr:t -> t -val concat : t array -> t +val eq_concat : t * t -> (t * t) array -> t (* records (struct / array values) *) val record : t vector -> t diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index d8166ba0b..e3c2d8f10 100644 --- a/sledge/src/symbheap/exec.ml +++ b/sledge/src/symbheap/exec.ml @@ -159,16 +159,15 @@ let memmov_foot us dst src len = let arr_mid, us, xs = fresh_var "a" us xs in let arr_src, us, xs = fresh_var "a" us xs in let src_dst = Term.sub src dst in - let mem_dst = Term.memory ~siz:src_dst ~arr:arr_dst in + let mem_dst = (src_dst, arr_dst) in let siz_mid = Term.sub len src_dst in - let mem_mid = Term.memory ~siz:siz_mid ~arr:arr_mid in - let mem_src = Term.memory ~siz:src_dst ~arr:arr_src in - let mem_dst_mid_src = Term.concat [|mem_dst; mem_mid; mem_src|] in + let mem_mid = (siz_mid, arr_mid) in + let mem_src = (src_dst, arr_src) in + let mem_dst_mid_src = [|mem_dst; mem_mid; mem_src|] in let siz_dst_mid_src, us, xs = fresh_var "m" us xs in let arr_dst_mid_src, _, xs = fresh_var "a" us xs in let eq_mem_dst_mid_src = - Term.eq mem_dst_mid_src - (Term.memory ~siz:siz_dst_mid_src ~arr:arr_dst_mid_src) + Term.eq_concat (siz_dst_mid_src, arr_dst_mid_src) mem_dst_mid_src in let seg = Sh.seg @@ -189,12 +188,11 @@ let memmov_dn_spec us dst src len = let xs, bas, siz, _, mem_mid, mem_src, foot = memmov_foot us dst src len in - let mem_mid_src_src = Term.concat [|mem_mid; mem_src; mem_src|] in + let mem_mid_src_src = [|mem_mid; mem_src; mem_src|] in let siz_mid_src_src, us, xs = fresh_var "m" us xs in let arr_mid_src_src, _, xs = fresh_var "a" us xs in let eq_mem_mid_src_src = - Term.eq mem_mid_src_src - (Term.memory ~siz:siz_mid_src_src ~arr:arr_mid_src_src) + Term.eq_concat (siz_mid_src_src, arr_mid_src_src) mem_mid_src_src in let post = Sh.and_ eq_mem_mid_src_src @@ -215,12 +213,11 @@ let memmov_up_spec us dst src len = let xs, bas, siz, mem_src, mem_mid, _, foot = memmov_foot us src dst len in - let mem_src_src_mid = Term.concat [|mem_src; mem_src; mem_mid|] in + let mem_src_src_mid = [|mem_src; mem_src; mem_mid|] in let siz_src_src_mid, us, xs = fresh_var "m" us xs in let arr_src_src_mid, _, xs = fresh_var "a" us xs in let eq_mem_src_src_mid = - Term.eq mem_src_src_mid - (Term.memory ~siz:siz_src_src_mid ~arr:arr_src_src_mid) + Term.eq_concat (siz_src_src_mid, arr_src_src_mid) mem_src_src_mid in let post = Sh.and_ eq_mem_src_src_mid @@ -375,16 +372,8 @@ let realloc_spec us reg ptr siz = (Sh.and_ Term.( conditional ~cnd:(le len siz) - ~thn: - (eq (memory ~siz ~arr:a1) - (concat - [| memory ~siz:len ~arr:a0 - ; memory ~siz:(sub siz len) ~arr:a2 |])) - ~els: - (eq (memory ~siz:len ~arr:a0) - (concat - [| memory ~siz ~arr:a1 - ; memory ~siz:(sub len siz) ~arr:a2 |]))) + ~thn:(eq_concat (siz, a1) [|(len, a0); (sub siz len, a2)|]) + ~els:(eq_concat (len, a0) [|(siz, a1); (sub len siz, a2)|])) (Sh.seg rseg)) in {xs; foot; sub; ms; post} @@ -415,16 +404,8 @@ let rallocx_spec us reg ptr siz = (Sh.and_ Term.( conditional ~cnd:(le len siz) - ~thn: - (eq (memory ~siz ~arr:a1) - (concat - [| memory ~siz:len ~arr:a0 - ; memory ~siz:(sub siz len) ~arr:a2 |])) - ~els: - (eq (memory ~siz:len ~arr:a0) - (concat - [| memory ~siz ~arr:a1 - ; memory ~siz:(sub len siz) ~arr:a2 |]))) + ~thn:(eq_concat (siz, a1) [|(len, a0); (sub siz len, a2)|]) + ~els:(eq_concat (len, a0) [|(siz, a1); (sub len siz, a2)|])) (Sh.seg rseg)) in {xs; foot; sub; ms; post} @@ -458,16 +439,8 @@ let xallocx_spec us reg ptr siz ext = Term.( and_ (conditional ~cnd:(le len siz) - ~thn: - (eq (memory ~siz ~arr:a1) - (concat - [| memory ~siz:len ~arr:a0 - ; memory ~siz:(sub siz len) ~arr:a2 |])) - ~els: - (eq (memory ~siz:len ~arr:a0) - (concat - [| memory ~siz ~arr:a1 - ; memory ~siz:(sub len siz) ~arr:a2 |]))) + ~thn:(eq_concat (siz, a1) [|(len, a0); (sub siz len, a2)|]) + ~els:(eq_concat (len, a0) [|(siz, a1); (sub len siz, a2)|])) (and_ (le siz reg) (le reg (add siz ext)))) (Sh.seg seg') in diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index ae5d51c3f..5283aa168 100644 --- a/sledge/src/symbheap/sh.ml +++ b/sledge/src/symbheap/sh.ml @@ -58,13 +58,17 @@ let var_strength q = in var_strength_ Var.Set.empty Var.Map.empty q +let pp_memory x fs (siz, arr) = + let term_pp = Term.ppx x in + Format.fprintf fs "@<1>⟨%a,%a@<1>⟩" term_pp siz term_pp arr + let pp_seg x fs {loc; bas; len; siz; arr} = let term_pp = Term.ppx x in Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" term_pp loc (fun fs (bas, len) -> if (not (Term.equal loc bas)) || not (Term.equal len siz) then Format.fprintf fs " %a, %a " term_pp bas term_pp len ) - (bas, len) term_pp (Term.memory ~siz ~arr) + (bas, len) (pp_memory x) (siz, arr) let pp_seg_norm cong fs seg = let x _ = None in @@ -91,8 +95,7 @@ let pp_block x fs segs = in let term_pp = Term.ppx x in let pp_mems = - List.pp "@,^" (fun fs seg -> - term_pp fs (Term.memory ~siz:seg.siz ~arr:seg.arr) ) + List.pp "@,^" (fun fs seg -> pp_memory x fs (seg.siz, seg.arr)) in match segs with | {loc; bas; len; _} :: _ -> diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml index 6fce56473..083527b26 100644 --- a/sledge/src/symbheap/solver.ml +++ b/sledge/src/symbheap/solver.ml @@ -140,10 +140,7 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in let min = Sh.and_ - (Term.eq - (Term.memory ~siz:o ~arr:a) - (Term.concat - [|Term.memory ~siz:n ~arr:a0; Term.memory ~siz:o_n ~arr:a1|])) + (Term.eq_concat (o, a) [|(n, a0); (o_n, a1)|]) (Sh.star (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; arr= a1}) (Sh.rem_seg msg min)) @@ -184,11 +181,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o Sh.and_ (Term.eq b b') (Sh.and_ (Term.eq m m') (Sh.and_ - (Term.eq - (Term.concat - [| Term.memory ~siz:o ~arr:a - ; Term.memory ~siz:n_o ~arr:a1' |]) - (Term.memory ~siz:n ~arr:a')) + (Term.eq_concat (n, a') [|(o, a); (n_o, a1')|]) (Sh.star (Sh.seg {loc= Term.add l o; bas= b'; len= m'; siz= n_o; arr= a1'}) @@ -224,10 +217,7 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k in let min = Sh.and_ - (Term.eq - (Term.memory ~siz:o ~arr:a) - (Term.concat - [|Term.memory ~siz:l_k ~arr:a0; Term.memory ~siz:n ~arr:a1|])) + (Term.eq_concat (o, a) [|(l_k, a0); (n, a1)|]) (Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0}) (Sh.rem_seg msg min)) @@ -271,11 +261,7 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k in let min = Sh.and_ - (Term.eq - (Term.memory ~siz:o ~arr:a) - (Term.concat - [| Term.memory ~siz:l_k ~arr:a0; Term.memory ~siz:n ~arr:a1 - ; Term.memory ~siz:ko_ln ~arr:a2 |])) + (Term.eq_concat (o, a) [|(l_k, a0); (n, a1); (ko_ln, a2)|]) (Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0}) (Sh.star @@ -322,10 +308,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k in let min = Sh.and_ - (Term.eq - (Term.memory ~siz:o ~arr:a) - (Term.concat - [|Term.memory ~siz:l_k ~arr:a0; Term.memory ~siz:ko_l ~arr:a1|])) + (Term.eq_concat (o, a) [|(l_k, a0); (ko_l, a1)|]) (Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0}) (Sh.rem_seg msg min)) @@ -334,11 +317,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k Sh.and_ (Term.eq b b') (Sh.and_ (Term.eq m m') (Sh.and_ - (Term.eq - (Term.concat - [| Term.memory ~siz:ko_l ~arr:a1 - ; Term.memory ~siz:ln_ko ~arr:a2' |]) - (Term.memory ~siz:n ~arr:a')) + (Term.eq_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|]) (Sh.star (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; arr= a2'}) (Sh.rem_seg ssg sub)))) @@ -374,11 +353,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l Sh.and_ (Term.eq b b') (Sh.and_ (Term.eq m m') (Sh.and_ - (Term.eq - (Term.concat - [| Term.memory ~siz:k_l ~arr:a0' - ; Term.memory ~siz:o ~arr:a |]) - (Term.memory ~siz:n ~arr:a')) + (Term.eq_concat (n, a') [|(k_l, a0'); (o, a)|]) (Sh.star (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'}) (Sh.rem_seg ssg sub)))) @@ -418,11 +393,7 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l Sh.and_ (Term.eq b b') (Sh.and_ (Term.eq m m') (Sh.and_ - (Term.eq - (Term.concat - [| Term.memory ~siz:k_l ~arr:a0'; Term.memory ~siz:o ~arr:a - ; Term.memory ~siz:ln_ko ~arr:a2' |]) - (Term.memory ~siz:n ~arr:a')) + (Term.eq_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|]) (Sh.star (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'}) (Sh.star @@ -464,10 +435,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l in let min = Sh.and_ - (Term.eq - (Term.memory ~siz:o ~arr:a) - (Term.concat - [|Term.memory ~siz:ln_k ~arr:a1; Term.memory ~siz:ko_ln ~arr:a2|])) + (Term.eq_concat (o, a) [|(ln_k, a1); (ko_ln, a2)|]) (Sh.star (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; arr= a2}) (Sh.rem_seg msg min)) @@ -476,11 +444,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l Sh.and_ (Term.eq b b') (Sh.and_ (Term.eq m m') (Sh.and_ - (Term.eq - (Term.concat - [| Term.memory ~siz:k_l ~arr:a0' - ; Term.memory ~siz:ln_k ~arr:a1 |]) - (Term.memory ~siz:n ~arr:a')) + (Term.eq_concat (n, a') [|(k_l, a0'); (ln_k, a1)|]) (Sh.star (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'}) (Sh.rem_seg ssg sub))))