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)