From aacdbc060af96068044c6059e2fa88f5e33e520a Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 12 Nov 2020 16:37:37 -0800 Subject: [PATCH] [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 | 2 +- sledge/src/fol/exp.ml | 9 ----- sledge/src/fol/exp.mli | 10 ------ sledge/src/fol/trm.ml | 71 ++++++++------------------------------ sledge/src/fol/trm.mli | 9 ----- sledge/src/llair/exp.ml | 22 +++++------- sledge/src/llair/typ.ml | 14 ++++++++ sledge/src/llair/typ.mli | 5 +++ sledge/src/llair_to_Fol.ml | 30 +++++++++++++--- 9 files changed, 68 insertions(+), 104 deletions(-) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index aca3ed63f..27a3d321d 100644 --- a/sledge/src/fol/context.ml +++ b/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) diff --git a/sledge/src/fol/exp.ml b/sledge/src/fol/exp.ml index 1b23b252b..a2bc3dde5 100644 --- a/sledge/src/fol/exp.ml +++ b/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 diff --git a/sledge/src/fol/exp.mli b/sledge/src/fol/exp.mli index 7f9345f8f..a394a949f 100644 --- a/sledge/src/fol/exp.mli +++ b/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 diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index b0524829f..f39d98eb0 100644 --- a/sledge/src/fol/trm.ml +++ b/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 "@[%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) diff --git a/sledge/src/fol/trm.mli b/sledge/src/fol/trm.mli index 4c873974a..1ed83df66 100644 --- a/sledge/src/fol/trm.mli +++ b/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 diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 29878d32e..7cd7d92b8 100644 --- a/sledge/src/llair/exp.ml +++ b/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 "@[%s@]" (String.escaped s) - | exception _ -> - Format.fprintf fs "@[%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 "@[%s@]" (String.escaped s) + | exception _ -> Format.fprintf fs "@[%a@]" (IArray.pp ",@ " pp) elts (** Invariant *) diff --git a/sledge/src/llair/typ.ml b/sledge/src/llair/typ.ml index e8b480104..0b0f11f3a 100644 --- a/sledge/src/llair/typ.ml +++ b/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 _) -> diff --git a/sledge/src/llair/typ.mli b/sledge/src/llair/typ.mli index 1944b25e2..d00127039 100644 --- a/sledge/src/llair/typ.mli +++ b/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. *) diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml index 58ba7fc05..dd26b2375 100644 --- a/sledge/src/llair_to_Fol.ml +++ b/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)