From 639bda69e7dea02199d5f869503c567949e7a60d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 12 Nov 2020 16:37:11 -0800 Subject: [PATCH] [sledge] Add byte-offsets of struct fields to Llair.Typ.t Summary: This information is needed to mediate between index-based operations (such as on records) and offset-based operations (such as load/store). Since it is fragile to recompute, the approach here is to query llvm during translation and store the result. Reviewed By: jvillard Differential Revision: D24772954 fbshipit-source-id: ad22c3ecf --- sledge/cli/frontend.ml | 22 ++++++++++++++++++---- sledge/nonstdlib/array.ml | 1 + sledge/nonstdlib/array.mli | 1 + sledge/nonstdlib/iArray.mli | 1 + sledge/src/llair/exp.ml | 6 +++--- sledge/src/llair/typ.ml | 14 ++++++++------ sledge/src/llair/typ.mli | 14 +++++++++----- 7 files changed, 41 insertions(+), 18 deletions(-) diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml index e730d9405..e427dac58 100644 --- a/sledge/cli/frontend.ml +++ b/sledge/cli/frontend.ml @@ -256,15 +256,27 @@ let rec xlate_type : x -> Llvm.lltype -> Typ.t = | Struct -> let llelts = Llvm.struct_element_types llt in let len = Array.length llelts in + let fld_off i = + match + Int64.unsigned_to_int + (Llvm_target.DataLayout.offset_of_element llt i + x.lldatalayout) + with + | Some i -> i + | None -> todo "offset too large: %a" pp_lltype llt () + in if Llvm.is_literal llt then let elts = - IArray.map ~f:(xlate_type x) (IArray.of_array llelts) + IArray.mapi + ~f:(fun i elt -> (fld_off i, xlate_type x elt)) + (IArray.of_array llelts) in Typ.tuple elts ~bits ~byts else let name = struct_name llt in let elts = - IArray.init len ~f:(fun i -> lazy (xlate_type x llelts.(i))) + IArray.init len ~f:(fun i -> + lazy (fld_off i, xlate_type x llelts.(i)) ) in Typ.struct_ ~name elts ~bits ~byts | Function -> fail "expected to be unsized: %a" pp_lltype llt () @@ -633,7 +645,7 @@ and xlate_opcode stk : match (typ : Typ.t) with | Tuple {elts} | Struct {elts} -> ( Exp.select typ rcd indices.(i) - , IArray.get elts indices.(i) + , snd (IArray.get elts indices.(i)) , Exp.update typ ~rcd indices.(i) ) | Array {elt} -> ( Exp.select typ rcd indices.(i) @@ -822,7 +834,9 @@ let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Typ.t * Llvm.lltype = let exception_typs = let pi8 = Typ.pointer ~elt:Typ.byt in let i32 = Typ.integer ~bits:32 ~byts:4 in - let exc = Typ.tuple (IArray.of_array [|pi8; i32|]) ~bits:96 ~byts:12 in + let exc = + Typ.tuple (IArray.of_array [|(0, pi8); (8, i32)|]) ~bits:96 ~byts:12 + in (pi8, i32, exc) (** Translate a control transfer from instruction [instr] to block [dst] to diff --git a/sledge/nonstdlib/array.ml b/sledge/nonstdlib/array.ml index 4966a71a7..57be2e838 100644 --- a/sledge/nonstdlib/array.ml +++ b/sledge/nonstdlib/array.ml @@ -28,6 +28,7 @@ let of_list_rev = function let is_empty = function [||] -> true | _ -> false let map xs ~f = map ~f xs +let mapi xs ~f = mapi ~f xs let map_endo xs ~f = map_endo map xs ~f let reduce_adjacent xs ~f = diff --git a/sledge/nonstdlib/array.mli b/sledge/nonstdlib/array.mli index f449ddf1d..dfeb69667 100644 --- a/sledge/nonstdlib/array.mli +++ b/sledge/nonstdlib/array.mli @@ -13,6 +13,7 @@ type 'a t = 'a array [@@deriving compare, equal, sexp] val of_ : 'a -> 'a t val of_list_rev : 'a list -> 'a t val map : 'a t -> f:('a -> 'b) -> 'b t +val mapi : 'a t -> f:(int -> 'a -> 'b) -> 'b t val map_endo : 'a t -> f:('a -> 'a) -> 'a t (** Like [map], but specialized to require [f] to be an endofunction, which diff --git a/sledge/nonstdlib/iArray.mli b/sledge/nonstdlib/iArray.mli index 94ad7576c..f08db3781 100644 --- a/sledge/nonstdlib/iArray.mli +++ b/sledge/nonstdlib/iArray.mli @@ -41,6 +41,7 @@ val init : int -> f:(int -> 'a) -> 'a t val sub : 'a t -> pos:int -> len:int -> 'a t val concat : 'a t list -> 'a t val map : 'a t -> f:('a -> 'b) -> 'b t +val mapi : 'a t -> f:(int -> 'a -> 'b) -> 'b t val map_endo : 'a t -> f:('a -> 'a) -> 'a t (** Like map, but specialized to require [f] to be an endofunction, which diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 6f2adc27b..3af26601c 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -208,7 +208,7 @@ let rec invariant exp = match typ with | Tuple {elts} | Struct {elts} -> assert (valid_idx idx elts) ; - assert (Typ.castable (IArray.get elts idx) (typ_of elt)) + assert (Typ.castable (snd (IArray.get elts idx)) (typ_of elt)) | Array {elt= typ_elt} -> assert (Typ.castable typ_elt (typ_of elt)) | _ -> assert false ) | Ap2 (op, typ, x, y) -> ( @@ -237,7 +237,7 @@ let rec invariant exp = | Tuple {elts} | Struct {elts} -> assert (IArray.length elts = IArray.length args) ; assert ( - IArray.for_all2_exn elts args ~f:(fun typ arg -> + IArray.for_all2_exn elts args ~f:(fun (_, typ) arg -> Typ.castable typ (typ_of arg) ) ) | _ -> assert false ) | RecRecord _ -> () @@ -253,7 +253,7 @@ and typ_of exp = | Ap1 (Select idx, typ, _) -> ( match typ with | Array {elt} -> elt - | Tuple {elts} | Struct {elts} -> IArray.get elts idx + | Tuple {elts} | Struct {elts} -> snd (IArray.get elts idx) | _ -> violates invariant exp ) | Ap2 ( (Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge | Ult | Ule | Ord | Uno) diff --git a/sledge/src/llair/typ.ml b/sledge/src/llair/typ.ml index 9e2f800c4..3a6adffc0 100644 --- a/sledge/src/llair/typ.ml +++ b/sledge/src/llair/typ.ml @@ -13,10 +13,10 @@ type t = | Float of {bits: int; byts: int; enc: [`IEEE | `Extended | `Pair]} | Pointer of {elt: t} | Array of {elt: t; len: int; bits: int; byts: int} - | Tuple of {elts: t iarray; bits: int; byts: int} + | Tuple of {elts: (int * t) iarray; bits: int; byts: int} | Struct of { name: string - ; elts: t iarray (* possibly cyclic, name unique *) + ; elts: (int * t) iarray (* possibly cyclic, name unique *) [@compare.ignore] [@equal.ignore] [@sexp_drop_if fun _ -> true] ; bits: int ; byts: int } @@ -42,14 +42,15 @@ let rec pp fs typ = pf "f%i%s" bits enc_str | Pointer {elt} -> pf "%a*" pp elt | Array {elt; len} -> pf "[%i x %a]" len pp elt - | Tuple {elts} -> pf "{ @[%a@] }" pps elts + | Tuple {elts} -> pf "{ @[%a@] }" pp_flds elts | Struct {name} | Opaque {name} -> pf "%%%s" name and pps fs typs = IArray.pp ",@ " pp fs typs +and pp_flds fs flds = IArray.pp ",@ " (fun fs (_, fld) -> pp fs fld) fs flds let pp_defn fs = function | Struct {name; elts} -> - Format.fprintf fs "@[<2>%%%s =@ @[{ %a@] }@]" name pps elts + Format.fprintf fs "@[<2>%%%s =@ @[{ %a@] }@]" name pp_flds elts | Opaque {name} -> Format.fprintf fs "@[<2>%%%s =@ opaque@]" name | typ -> pp fs typ @@ -67,7 +68,8 @@ let invariant t = assert (Option.for_all ~f:is_sized return) ; assert (IArray.for_all ~f:is_sized args) | Array {elt} -> assert (is_sized elt) - | Tuple {elts} | Struct {elts} -> assert (IArray.for_all ~f:is_sized elts) + | Tuple {elts} | Struct {elts} -> + assert (IArray.for_all ~f:(fun (_, t) -> is_sized t) elts) | Integer {bits} | Float {bits} -> assert (bits > 0) | Pointer _ | Opaque _ -> assert true @@ -93,7 +95,7 @@ let struct_ = | None -> (* Add placeholder defn to prevent computing [elts] in calls to [struct] from [elts] for recursive occurrences of [name]. *) - let elts = Array.make (IArray.length elt_thks) dummy_typ in + let elts = Array.make (IArray.length elt_thks) (0, dummy_typ) in let typ = Struct {name; elts= IArray.of_array elts; bits; byts} in String.Tbl.set defns ~key:name ~data:typ ; IArray.iteri elt_thks ~f:(fun i (lazy elt) -> elts.(i) <- elt) ; diff --git a/sledge/src/llair/typ.mli b/sledge/src/llair/typ.mli index c25f0601a..1944b25e2 100644 --- a/sledge/src/llair/typ.mli +++ b/sledge/src/llair/typ.mli @@ -16,10 +16,11 @@ type t = private | Pointer of {elt: t} (** Pointer to element type. *) | Array of {elt: t; len: int; bits: int; byts: int} (** Statically-sized array of [len] elements of type [elt]. *) - | Tuple of {elts: t iarray; bits: int; byts: int} + | Tuple of {elts: (int * t) iarray; bits: int; byts: int} (** Anonymous aggregate of heterogeneous types. *) - | Struct of {name: string; elts: t iarray; bits: int; byts: int} - (** Uniquely named aggregate of heterogeneous types. Every cycle of + | Struct of {name: string; elts: (int * t) iarray; bits: int; byts: int} + (** Uniquely named aggregate of heterogeneous types. Elements are + specified by their byte offset and their type. Every cycle of recursive types contains a [Struct]. NOTE: recursive [Struct] types are represented by cyclic values. *) | Opaque of {name: string} @@ -43,8 +44,11 @@ val integer : bits:int -> byts:int -> t val float : bits:int -> byts:int -> enc:[`Extended | `IEEE | `Pair] -> t val pointer : elt:t -> t val array : elt:t -> len:int -> bits:int -> byts:int -> t -val tuple : t iarray -> bits:int -> byts:int -> t -val struct_ : name:string -> bits:int -> byts:int -> t lazy_t iarray -> t +val tuple : (int * t) iarray -> bits:int -> byts:int -> t + +val struct_ : + name:string -> bits:int -> byts:int -> (int * t) lazy_t iarray -> t + val opaque : name:string -> t (** Queries *)