[sledge] Add term to Extract a slice out of an aggregate value

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

@@ -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

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) *)

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)