[sledge] Remove record theory from backend, encode using sequence theory

Summary:
LLVM and Llair use a form of records, in particular for values of
constant structs and arrays. In Llair, these use standard `select` and
`update` operations a la McCarthy's theory of functional arrays, with
a compact `record` operation for constructing complete records. This
is fine and logically well-understood. The issue is that once
constructed, these values are accessed using instructions that (may)
operate over byte-ranges, rather than struct member indices. The
backend uses a theory of sequences to represent such values (the
contents of memory). So some code depends on high fidelity
interoperation between these two views.

This diff resolves this by removing the record theory from the backend
and instead encoding them using the sequence theory. The approach
taken keeps records in Llair and translates them to sequences in
Llair_to_Fol. This choice is made since the encoding into the sequence
theory involves terms that do not have types that are expressible in
terms of the source types. In particular, `(update r i e)`, is encoded
as the concatenation of the prefix of `r` up to the offset of index
`i`, followed by `e` (possibly with padding), and then the suffix of
`r` from index `i+1` on. The prefix and suffix sequences do not
necessarily have source-expressible types.

Reviewed By: jvillard

Differential Revision: D24800866

fbshipit-source-id: e7238c558

sledge/src/fol/context.ml

@@ -24,7 +24,7 @@ let rec classify e =
     | Uninterpreted -> Uninterpreted )
   | Sized _ | Extract _ | Concat _ -> Interpreted
   | Var _ | Z _ | Q _ -> Atomic
-  | Splat _ | Select _ | Update _ | Record _ | Apply _ -> Uninterpreted
+  | Splat _ | Apply _ -> Uninterpreted
 
 let interpreted e = equal_kind (classify e) Interpreted
 let non_interpreted e = not (interpreted e)

sledge/src/fol/exp.ml

@@ -229,15 +229,6 @@ module Term = struct
 
   let concat elts = apNt Trm.concat elts
 
-  (* records *)
-
-  let select ~rcd ~idx = ap1t (fun rcd -> Trm.select ~rcd ~idx) rcd
-
-  let update ~rcd ~idx ~elt =
-    ap2t (fun rcd elt -> Trm.update ~rcd ~idx ~elt) rcd elt
-
-  let record elts = apNt Trm.record elts
-
   (* uninterpreted *)
 
   let apply sym args = apNt (Trm.apply sym) args

sledge/src/fol/exp.mli

@@ -46,16 +46,6 @@ module rec Term : sig
   val concat : t array -> t
   (** Concatenation of sequences *)
 
-  (* records (with fixed indices) *)
-  val select : rcd:t -> idx:int -> t
-  (** Select an index from a record *)
-
-  val update : rcd:t -> idx:int -> elt:t -> t
-  (** Record updated with element at index *)
-
-  val record : t array -> t
-  (** Record constant *)
-
   (* uninterpreted *)
   val apply : Funsym.t -> t array -> t
 

sledge/src/fol/trm.ml

@@ -82,10 +82,6 @@ and Trm : sig
     | Sized of {seq: t; siz: t}
     | Extract of {seq: t; off: t; len: t}
     | Concat of t array
-    (* records (with fixed indices) *)
-    | Select of {idx: int; rcd: t}
-    | Update of {idx: int; rcd: t; elt: t}
-    | Record of t array
     (* uninterpreted *)
     | Apply of Funsym.t * t array
   [@@deriving compare, equal, sexp]
@@ -100,9 +96,6 @@ and Trm : sig
   val _Sized : t -> t -> t
   val _Extract : t -> t -> t -> t
   val _Concat : t array -> t
-  val _Select : int -> t -> t
-  val _Update : int -> t -> t -> t
-  val _Record : t array -> t
   val _Apply : Funsym.t -> t array -> t
   val add : t -> t -> t
   val sub : t -> t -> t
@@ -121,9 +114,6 @@ end = struct
     | Sized of {seq: t; siz: t}
     | Extract of {seq: t; off: t; len: t}
     | Concat of t array
-    | Select of {idx: int; rcd: t}
-    | Update of {idx: int; rcd: t; elt: t}
-    | Record of t array
     | Apply of Funsym.t * t array
   [@@deriving compare, equal, sexp]
 
@@ -155,11 +145,15 @@ end = struct
       | Sized {seq; siz} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp seq
       | Extract {seq; off; len} -> pf "%a[%a,%a)" pp seq pp off pp len
       | Concat [||] -> pf "@<2>⟨⟩"
-      | Concat xs -> pf "(%a)" (Array.pp "@,^" pp) xs
-      | Select {idx; rcd} -> pf "%a[%i]" pp rcd idx
-      | Update {idx; rcd; elt} ->
-          pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
-      | Record xs -> pf "{%a}" (ppx_record strength) xs
+      | Concat xs -> (
+          let exception Not_a_string in
+          try
+            pf "%S"
+              (String.init (Array.length xs) ~f:(fun i ->
+                   match xs.(i) with
+                   | Sized {seq= Z c} -> Char.of_int_exn (Z.to_int c)
+                   | _ -> raise_notrace Not_a_string ))
+          with _ -> pf "(%a)" (Array.pp "@,^" pp) xs )
       | Apply (f, [||]) -> pf "%a" Funsym.pp f
       | Apply
           ( ( (Rem | BitAnd | BitOr | BitXor | BitShl | BitLshr | BitAshr)
@@ -171,24 +165,6 @@ end = struct
     in
     pp fs trm
 
-  and ppx_record strength fs elts =
-    [%Trace.fprintf
-      fs "%a"
-        (fun fs elts ->
-          let exception Not_a_string in
-          match
-            String.init (Array.length elts) ~f:(fun i ->
-                match elts.(i) with
-                | Z c -> Char.of_int_exn (Z.to_int c)
-                | _ -> raise_notrace Not_a_string )
-          with
-          | s -> Format.fprintf fs "%S" s
-          | exception (Not_a_string | Z.Overflow | Failure _) ->
-              Format.fprintf fs "@[<h>%a@]"
-                (Array.pp ",@ " (ppx strength))
-                elts )
-        elts]
-
   let pp = ppx (fun _ -> None)
 
   let invariant e =
@@ -354,10 +330,6 @@ end = struct
     let xs = Array.reduce_adjacent ~f:simp_adjacent xs in
     (if Array.length xs = 1 then xs.(0) else Concat xs) |> check invariant
 
-  let _Select idx rcd = Select {idx; rcd} |> check invariant
-  let _Update idx rcd elt = Update {idx; rcd; elt} |> check invariant
-  let _Record es = Record es |> check invariant
-
   let _Apply f es =
     ( match Funsym.eval ~equal ~get_z ~ret_z:_Z ~get_q ~ret_q:_Q f es with
     | Some c -> c
@@ -370,16 +342,15 @@ end = struct
     match e with
     | Var _ as v -> f (Var.of_ v)
     | Z _ | Q _ -> ()
-    | Splat x | Select {rcd= x} -> iter_vars ~f x
-    | Sized {seq= x; siz= y} | Update {rcd= x; elt= y} ->
+    | Splat x -> iter_vars ~f x
+    | Sized {seq= x; siz= y} ->
         iter_vars ~f x ;
         iter_vars ~f y
     | Extract {seq= x; off= y; len= z} ->
         iter_vars ~f x ;
         iter_vars ~f y ;
         iter_vars ~f z
-    | Concat xs | Record xs | Apply (_, xs) ->
-        Array.iter ~f:(iter_vars ~f) xs
+    | Concat xs | Apply (_, xs) -> Array.iter ~f:(iter_vars ~f) xs
     | Arith a -> Iter.iter ~f:(iter_vars ~f) (Arith.trms a)
 
   let vars e = Iter.from_labelled_iter (iter_vars e)
@@ -428,12 +399,6 @@ let sized ~seq ~siz = _Sized seq siz
 let extract ~seq ~off ~len = _Extract seq off len
 let concat elts = _Concat elts
 
-(* records *)
-
-let select ~rcd ~idx = _Select idx rcd
-let update ~rcd ~idx ~elt = _Update idx rcd elt
-let record elts = _Record elts
-
 (* uninterpreted *)
 
 let apply sym args = _Apply sym args
@@ -449,9 +414,6 @@ let rec map_vars e ~f =
   | Sized {seq; siz} -> map2 (map_vars ~f) e _Sized seq siz
   | Extract {seq; off; len} -> map3 (map_vars ~f) e _Extract seq off len
   | Concat xs -> mapN (map_vars ~f) e _Concat xs
-  | Select {idx; rcd} -> map1 (map_vars ~f) e (_Select idx) rcd
-  | Update {idx; rcd; elt} -> map2 (map_vars ~f) e (_Update idx) rcd elt
-  | Record xs -> mapN (map_vars ~f) e _Record xs
   | Apply (g, xs) -> mapN (map_vars ~f) e (_Apply g) xs
 
 let map e ~f =
@@ -462,9 +424,6 @@ let map e ~f =
   | Sized {seq; siz} -> map2 f e _Sized seq siz
   | Extract {seq; off; len} -> map3 f e _Extract seq off len
   | Concat xs -> mapN f e _Concat xs
-  | Select {idx; rcd} -> map1 f e (_Select idx) rcd
-  | Update {idx; rcd; elt} -> map2 f e (_Update idx) rcd elt
-  | Record xs -> mapN f e _Record xs
   | Apply (g, xs) -> mapN f e (_Apply g) xs
 
 (** Traverse *)
@@ -473,15 +432,15 @@ let iter_subtrms e ~f =
   match e with
   | Var _ | Z _ | Q _ -> ()
   | Arith a -> Iter.iter ~f (Arith.trms a)
-  | Splat x | Select {rcd= x} -> f x
-  | Sized {seq= x; siz= y} | Update {rcd= x; elt= y} ->
+  | Splat x -> f x
+  | Sized {seq= x; siz= y} ->
       f x ;
       f y
   | Extract {seq= x; off= y; len= z} ->
       f x ;
       f y ;
       f z
-  | Concat xs | Record xs | Apply (_, xs) -> Array.iter ~f xs
+  | Concat xs | Apply (_, xs) -> Array.iter ~f xs
 
 let subtrms e = Iter.from_labelled_iter (iter_subtrms e)
 

sledge/src/fol/trm.mli

@@ -21,10 +21,6 @@ type t = private
   | Sized of {seq: t; siz: t}
   | Extract of {seq: t; off: t; len: t}
   | Concat of t array
-  (* records (with fixed indices) *)
-  | Select of {idx: int; rcd: t}
-  | Update of {idx: int; rcd: t; elt: t}
-  | Record of t array
   (* uninterpreted *)
   | Apply of Funsym.t * t array
 [@@deriving compare, equal, sexp]
@@ -76,11 +72,6 @@ val sized : seq:t -> siz:t -> t
 val extract : seq:t -> off:t -> len:t -> t
 val concat : t array -> t
 
-(* records (with fixed indices) *)
-val select : rcd:t -> idx:int -> t
-val update : rcd:t -> idx:int -> elt:t -> t
-val record : t array -> t
-
 (* uninterpreted *)
 val apply : Funsym.t -> t array -> t
 

sledge/src/llair/exp.ml

@@ -145,20 +145,14 @@ let rec pp fs exp =
   [@@warning "-9"]
 
 and pp_record fs elts =
-  [%Trace.fprintf
-    fs "%a"
-      (fun fs elts ->
-        match
-          String.init (IArray.length elts) ~f:(fun i ->
-              match IArray.get elts i with
-              | Integer {data} -> Char.of_int_exn (Z.to_int data)
-              | _ -> raise_notrace (Invalid_argument "not a string") )
-        with
-        | s -> Format.fprintf fs "@[<h>%s@]" (String.escaped s)
-        | exception _ ->
-            Format.fprintf fs "@[<h>%a@]" (IArray.pp ",@ " pp) elts )
-      elts]
-  [@@warning "-9"]
+  match
+    String.init (IArray.length elts) ~f:(fun i ->
+        match IArray.get elts i with
+        | Integer {data; _} -> Char.of_int_exn (Z.to_int data)
+        | _ -> raise_notrace (Invalid_argument "not a string") )
+  with
+  | s -> Format.fprintf fs "@[<h>%s@]" (String.escaped s)
+  | exception _ -> Format.fprintf fs "@[<hv>%a@]" (IArray.pp ",@ " pp) elts
 
 (** Invariant *)
 

sledge/src/llair/typ.ml

@@ -135,6 +135,20 @@ let size_of = function
       byts
   | Pointer _ -> 8
 
+let offset_length_of_elt typ idx =
+  match typ with
+  | Array {elt} ->
+      let len = size_of elt in
+      (len * idx, len)
+  | Tuple {elts; byts} | Struct {elts; byts} ->
+      let oI, _ = IArray.get elts idx in
+      let oJ =
+        if idx = IArray.length elts - 1 then byts
+        else fst (IArray.get elts (idx + 1))
+      in
+      (oI, oJ - oI)
+  | _ -> fail "offset_length_of_elt: %a" pp typ ()
+
 let rec equivalent t0 t1 =
   match (t0, t1) with
   | (Pointer _ | Integer _), (Pointer _ | Integer _) ->

sledge/src/llair/typ.mli

@@ -64,6 +64,11 @@ val size_of : t -> int
 (** The number of bytes between adjacent values of the given type, including
     alignment padding. Raises unless is_sized holds. *)
 
+val offset_length_of_elt : t -> int -> int * int
+(** The offset in bytes to, and number of bytes occupied by, the given
+    element of an aggretage type. Raises if type is not an aggregate or
+    index is invalid. *)
+
 val equivalent : t -> t -> bool
 (** Equivalent types are those that denote the same sets of values in the
     semantic model. An equivalence relation. *)

sledge/src/llair_to_Fol.ml

@@ -120,11 +120,31 @@ and term : Llair.Exp.t -> T.t =
   | Ap2 (Ashr, _, d, e) -> ap_ttt (uap2 BitAshr) d e
   | Ap3 (Conditional, _, cnd, thn, els) ->
       T.ite ~cnd:(formula cnd) ~thn:(term thn) ~els:(term els)
-  | Ap1 (Select idx, _, rcd) -> T.select ~rcd:(term rcd) ~idx
-  | Ap2 (Update idx, _, rcd, elt) ->
-      T.update ~rcd:(term rcd) ~idx ~elt:(term elt)
-  | ApN (Record, _, elts) ->
-      T.record (Array.map ~f:term (IArray.to_array elts))
+  | Ap1 (Select idx, typ, rcd) ->
+      let off, len = Llair.Typ.offset_length_of_elt typ idx in
+      let off = T.integer (Z.of_int off) in
+      let len = T.integer (Z.of_int len) in
+      T.extract ~seq:(term rcd) ~off ~len
+  | Ap2 (Update idx, typ, rcd, elt) ->
+      let oI, lI = Llair.Typ.offset_length_of_elt typ idx in
+      let oJ = oI + lI in
+      let off0 = T.zero in
+      let len0 = T.integer (Z.of_int oI) in
+      let len1 = T.integer (Z.of_int lI) in
+      let off2 = T.integer (Z.of_int oJ) in
+      let len2 = T.integer (Z.of_int (Llair.Typ.size_of typ - oI - lI)) in
+      let seq = term rcd in
+      T.concat
+        [| T.extract ~seq ~off:off0 ~len:len0
+         ; T.sized ~seq:(term elt) ~siz:len1
+         ; T.extract ~seq ~off:off2 ~len:len2 |]
+  | ApN (Record, typ, elts) ->
+      let elt_siz i =
+        T.integer (Z.of_int (snd (Llair.Typ.offset_length_of_elt typ i)))
+      in
+      T.concat
+        (Array.mapi (IArray.to_array elts) ~f:(fun i elt ->
+             T.sized ~seq:(term elt) ~siz:(elt_siz i) ))
   | Ap1 (Splat, _, byt) -> T.splat (term byt)
 
 and formula e = F.dq0 (term e)