From 52dec5f4da67048343f69bdb324f1c2c0bb9639b Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 15 Jun 2020 15:41:55 -0700 Subject: [PATCH] [sledge] Refactor: Move eq_concat out of Term Summary: `Term.eq_concat` is not primitive and complicates the `Term` interface. Move it to a couple clients as a convenience wrapper. Reviewed By: jvillard Differential Revision: D21721026 fbshipit-source-id: 0d74aa251 --- sledge/src/exec.ml | 11 ++++++++--- sledge/src/sh_test.ml | 9 +++++++-- sledge/src/solver.ml | 25 +++++++++++++++---------- sledge/src/term.ml | 4 ---- sledge/src/term.mli | 1 - 5 files changed, 30 insertions(+), 20 deletions(-) diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml index 490607365..7ec93c083 100644 --- a/sledge/src/exec.ml +++ b/sledge/src/exec.ml @@ -33,6 +33,11 @@ let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us = let null_eq ptr = Sh.pure (Term.eq Term.zero ptr) +let eq_concat (siz, arr) ms = + Term.( + eq (memory ~siz ~arr) + (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms))) + (* Overwritten variables renaming and remaining modified variables. [ws] are the written variables; [rs] are the variables read or in the precondition; [us] are the variables to which ghosts must be chosen @@ -167,7 +172,7 @@ let memmov_foot us dst src len = let siz_dst_mid_src, us, xs = fresh_var "m" us xs in let arr_dst_mid_src, us, xs = fresh_var "a" us xs in let eq_mem_dst_mid_src = - Term.eq_concat (siz_dst_mid_src, arr_dst_mid_src) mem_dst_mid_src + eq_concat (siz_dst_mid_src, arr_dst_mid_src) mem_dst_mid_src in let seg = Sh.seg @@ -192,7 +197,7 @@ let memmov_dn_spec us dst src len = 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_concat (siz_mid_src_src, arr_mid_src_src) mem_mid_src_src + eq_concat (siz_mid_src_src, arr_mid_src_src) mem_mid_src_src in let post = Sh.and_ eq_mem_mid_src_src @@ -217,7 +222,7 @@ let memmov_up_spec us dst src len = 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_concat (siz_src_src_mid, arr_src_src_mid) mem_src_src_mid + eq_concat (siz_src_src_mid, arr_src_src_mid) mem_src_src_mid in let post = Sh.and_ eq_mem_src_src_mid diff --git a/sledge/src/sh_test.ml b/sledge/src/sh_test.ml index 3ec54ce27..5b2f7435a 100644 --- a/sledge/src/sh_test.ml +++ b/sledge/src/sh_test.ml @@ -41,6 +41,11 @@ let%test_module _ = let x = Term.var x_ let y = Term.var y_ + let eq_concat (siz, arr) ms = + Term.( + eq (memory ~siz ~arr) + (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms))) + let of_eqs l = List.fold ~init:emp ~f:(fun q (a, b) -> and_ (Term.eq a b) q) l @@ -147,12 +152,12 @@ let%test_module _ = exists ~$[a_; c_; d_; e_] (star - (pure (Term.eq_concat (!16, e) [|(!8, a); (!8, d)|])) + (pure (eq_concat (!16, e) [|(!8, a); (!8, d)|])) (or_ (pure (Term.dq x !0)) (exists (Var.Set.of_list [b_]) - (pure (Term.eq_concat (!8, a) [|(!4, c); (!4, b)|]))))) + (pure (eq_concat (!8, a) [|(!4, c); (!4, b)|]))))) in pp_raw q ; let q' = simplify q in diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml index a6a7af5be..9f28e25f5 100644 --- a/sledge/src/solver.ml +++ b/sledge/src/solver.ml @@ -132,6 +132,11 @@ end open Goal +let eq_concat (siz, arr) ms = + Term.( + eq (memory ~siz ~arr) + (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms))) + let fresh_var name vs zs ~wrt = let v, wrt = Var.fresh name ~wrt in let vs = Var.Set.add vs v in @@ -244,7 +249,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_concat (o, a) [|(n, a0); (o_n, a1)|]) + (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)) @@ -285,7 +290,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_concat (n, a') [|(o, a); (n_o, a1')|]) + (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'}) @@ -322,7 +327,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_concat (o, a) [|(l_k, a0); (n, a1)|]) + (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)) @@ -367,7 +372,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_concat (o, a) [|(l_k, a0); (n, a1); (ko_ln, a2)|]) + (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 @@ -415,7 +420,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_concat (o, a) [|(l_k, a0); (ko_l, a1)|]) + (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)) @@ -424,7 +429,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_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|]) + (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)))) @@ -460,7 +465,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_concat (n, a') [|(k_l, a0'); (o, a)|]) + (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)))) @@ -500,7 +505,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_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|]) + (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 @@ -542,7 +547,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_concat (o, a) [|(ln_k, a1); (ko_ln, a2)|]) + (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)) @@ -551,7 +556,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_concat (n, a') [|(k_l, a0'); (ln_k, a1)|]) + (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)))) diff --git a/sledge/src/term.ml b/sledge/src/term.ml index c031aec51..3cd7e98e1 100644 --- a/sledge/src/term.ml +++ b/sledge/src/term.ml @@ -973,10 +973,6 @@ let select ~rcd ~idx = norm1 (Select idx) rcd let update ~rcd ~idx ~elt = norm2 (Update idx) rcd elt let rec_record i = simp_rec_record i |> check invariant -let eq_concat (siz, arr) ms = - eq (memory ~siz ~arr) - (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms)) - let rec binary mk x y = mk (of_exp x) (of_exp y) and ubinary mk typ x y = diff --git a/sledge/src/term.mli b/sledge/src/term.mli index c9501cb02..8043f3acf 100644 --- a/sledge/src/term.mli +++ b/sledge/src/term.mli @@ -226,7 +226,6 @@ val splat : t -> t val memory : siz:t -> arr:t -> t val extract : agg:t -> off:t -> len:t -> t val concat : t array -> t -val eq_concat : t * t -> (t * t) array -> t (* records (struct / array values) *) val record : t iarray -> t