From 539b4a0b46da116c170ff831f876a78dcaed7860 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 27 Jan 2020 08:19:41 -0800 Subject: [PATCH] [sledge] Add term to Extract a slice out of an aggregate value MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Summary: The byte-array theory used for the contents of memory is strong enough to express all the constraints arising during symbolic execution without the ability to extract a slice out of a byte-array. However, without Extract, it is not possible to solve some equations for some variables, for example solving ⟨n,α⟩^⟨m,β⟩ = ⟨l,γ⟩ for α. Solving such equations is needed for quantifier elimination and to formulate the byte-array theory as a Shostak theory. Reviewed By: ngorogiannis Differential Revision: D19286632 fbshipit-source-id: 07dc112d0 --- sledge/src/llair/term.ml | 13 ++++++++++--- sledge/src/llair/term.mli | 5 ++++- sledge/src/symbheap/solver_test.ml | 12 ++++++------ 3 files changed, 20 insertions(+), 10 deletions(-) diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index 62ad271d6..3f3874328 100644 --- a/sledge/src/llair/term.ml +++ b/sledge/src/llair/term.ml @@ -36,7 +36,7 @@ type op2 = | Update of int [@@deriving compare, equal, hash, sexp] -type op3 = Conditional [@@deriving compare, equal, hash, sexp] +type op3 = Conditional | Extract [@@deriving compare, equal, hash, sexp] type opN = Concat | Record [@@deriving compare, equal, hash, sexp] type recN = Record [@@deriving compare, equal, hash, sexp] @@ -196,9 +196,11 @@ let rec ppx strength fs term = | Ap2 (Ashr, x, y) -> pf "(%a@ ashr %a)" pp x pp y | Ap3 (Conditional, cnd, thn, els) -> pf "(%a@ ? %a@ : %a)" pp cnd pp thn pp els + | Ap3 (Extract, agg, off, len) -> pf "%a[%a,%a)" pp agg pp off pp len | Ap1 (Splat, byt) -> pf "%a^" pp byt | Ap2 (Memory, siz, arr) -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr - | ApN (Concat, args) -> pf "%a" (Vector.pp "@,^" pp) args + | ApN (Concat, args) when Vector.is_empty args -> pf "@<2>⟨⟩" + | ApN (Concat, args) -> pf "(%a)" (Vector.pp "@,^" pp) args | ApN (Record, elts) -> pf "{%a}" (pp_record strength) elts | RecN (Record, elts) -> pf "{|%a|}" (Vector.pp ",@ " pp) elts | Ap1 (Select idx, rcd) -> pf "%a[%i]" pp rcd idx @@ -789,6 +791,7 @@ let simp_concat xs = let simp_splat byt = Ap1 (Splat, byt) let simp_memory siz arr = Ap2 (Memory, siz, arr) +let simp_extract agg off len = Ap3 (Extract, agg, off, len) (* records *) @@ -850,7 +853,10 @@ let norm2 op x y = |> check invariant let norm3 op x y z = - (match op with Conditional -> simp_cond x y z) |> check invariant + ( match op with + | Conditional -> simp_cond x y z + | Extract -> simp_extract x y z ) + |> check invariant let normN op xs = (match op with Concat -> simp_concat xs | Record -> simp_record xs) @@ -885,6 +891,7 @@ let ashr = norm2 Ashr let conditional ~cnd ~thn ~els = norm3 Conditional cnd thn els let splat byt = norm1 Splat byt let memory ~siz ~arr = norm2 Memory siz arr +let extract ~agg ~off ~len = norm3 Extract agg off len let concat xs = normN Concat (Vector.of_array xs) let record elts = normN Record elts let select ~rcd ~idx = norm1 (Select idx) rcd diff --git a/sledge/src/llair/term.mli b/sledge/src/llair/term.mli index 12a6ded07..01995622f 100644 --- a/sledge/src/llair/term.mli +++ b/sledge/src/llair/term.mli @@ -49,7 +49,9 @@ type op2 = | Update of int (** Constant record with updated index *) [@@deriving compare, equal, hash, sexp] -type op3 = Conditional (** If-then-else *) +type op3 = + | Conditional (** If-then-else *) + | Extract (** Extract a slice of an aggregate value *) [@@deriving compare, equal, hash, sexp] type opN = @@ -214,6 +216,7 @@ val conditional : cnd:t -> thn:t -> els:t -> t (* memory contents *) val splat : t -> t +val extract : agg:t -> off:t -> len:t -> t val eq_concat : t * t -> (t * t) array -> t (* records (struct / array values) *) diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml index 376c41d65..42e717535 100644 --- a/sledge/src/symbheap/solver_test.ml +++ b/sledge/src/symbheap/solver_test.ml @@ -133,7 +133,7 @@ let%test_module _ = {| ( infer_frame: %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3 . %l_6 -[)-> ⟨16,%a_3⟩ - ) infer_frame: %a_2 = _ ∧ ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a_2⟩ ∧ emp |}] + ) infer_frame: %a_2 = _ ∧ ⟨16,%a_3⟩ = (⟨8,%a_1⟩^⟨8,%a_2⟩) ∧ emp |}] let%expect_test _ = check_frame @@ -149,7 +149,7 @@ let%test_module _ = \- ∃ %a_3, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩ ) infer_frame: - %a_2 = _ ∧ ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a_2⟩ ∧ 16 = %m_8 ∧ emp |}] + %a_2 = _ ∧ ⟨16,%a_3⟩ = (⟨8,%a_1⟩^⟨8,%a_2⟩) ∧ 16 = %m_8 ∧ emp |}] let%expect_test _ = check_frame @@ -165,7 +165,7 @@ let%test_module _ = \- ∃ %a_3, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩ ) infer_frame: - %a_2 = _ ∧ ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a_2⟩ ∧ 16 = %m_8 ∧ emp |}] + %a_2 = _ ∧ ⟨16,%a_3⟩ = (⟨8,%a_1⟩^⟨8,%a_2⟩) ∧ 16 = %m_8 ∧ emp |}] let%expect_test _ = check_frame @@ -185,7 +185,7 @@ let%test_module _ = ) infer_frame: ∃ %a0_10, %a1_11 . %a_2 = %a0_10 - ∧ ⟨32,%a_1⟩ = ⟨16,%a_2⟩^⟨16,%a1_11⟩ + ∧ ⟨32,%a_1⟩ = (⟨16,%a_2⟩^⟨16,%a1_11⟩) ∧ 16 = %m_8 = %n_9 ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}] @@ -242,12 +242,12 @@ let%test_module _ = ∧ 16 = %m_8 ∧ (%l_6 + 16) -[ %l_6, 16 )-> ⟨0,%a_3⟩) ∨ ( %a_3 = _ - ∧ ⟨16,%a_1⟩ = ⟨8,%a_2⟩^⟨8,%a_3⟩ + ∧ ⟨16,%a_1⟩ = (⟨8,%a_2⟩^⟨8,%a_3⟩) ∧ 1 = %n_9 ∧ 16 = %m_8 ∧ emp) ∨ ( %a_3 = _ - ∧ ⟨16,%a_1⟩ = ⟨0,%a_2⟩^⟨16,%a_3⟩ + ∧ ⟨16,%a_1⟩ = (⟨0,%a_2⟩^⟨16,%a_3⟩) ∧ 0 = %n_9 ∧ 16 = %m_8 ∧ emp)