[sledge] Add sizes to types

Summary:
In order to type-check casts, it is necessary to have the size of each
sized type. This size information is also useful in a few other places.

Reviewed By: bennostein

Differential Revision: D17801931

fbshipit-source-id: f8ef53276

sledge/src/llair/exp.ml

@@ -223,7 +223,7 @@ let rec invariant exp =
   | Ap2 (Splat, typ, byt, siz) -> (
       assert (Typ.convertible Typ.byt (typ_of byt)) ;
       assert (Typ.convertible Typ.siz (typ_of siz)) ;
-      match (Typ.prim_bit_size_of typ, siz.desc) with
+      match (Typ.size_of typ, siz.desc) with
       | Some n, Integer {data} -> assert (Z.equal (Z.of_int n) data)
       | None, Integer {data} -> assert (not (Z.equal Z.zero data))
       | _ -> () )
@@ -545,10 +545,10 @@ let fold_regs e ~init ~f =
 
 let is_true e =
   match e.desc with
-  | Integer {data; typ= Integer {bits= 1}} -> Z.is_true data
+  | Integer {data; typ= Integer {bits= 1; _}} -> Z.is_true data
   | _ -> false
 
 let is_false e =
   match e.desc with
-  | Integer {data; typ= Integer {bits= 1}} -> Z.is_false data
+  | Integer {data; typ= Integer {bits= 1; _}} -> Z.is_false data
   | _ -> false

sledge/src/llair/frontend.ml

@@ -206,14 +206,15 @@ let rec xlate_type : x -> Llvm.lltype -> Typ.t =
  fun x llt ->
   let xlate_type_ llt =
     match Llvm.classify_type llt with
-    | Half -> Typ.float ~bits:16 ~enc:`IEEE
+    | Half -> Typ.float ~bits:16 ~siz:(size_of x llt) ~enc:`IEEE
-    | Float -> Typ.float ~bits:32 ~enc:`IEEE
+    | Float -> Typ.float ~bits:32 ~siz:(size_of x llt) ~enc:`IEEE
-    | Double -> Typ.float ~bits:64 ~enc:`IEEE
+    | Double -> Typ.float ~bits:64 ~siz:(size_of x llt) ~enc:`IEEE
-    | X86fp80 -> Typ.float ~bits:80 ~enc:`Extended
+    | X86fp80 -> Typ.float ~bits:80 ~siz:(size_of x llt) ~enc:`Extended
-    | Fp128 -> Typ.float ~bits:128 ~enc:`IEEE
+    | Fp128 -> Typ.float ~bits:128 ~siz:(size_of x llt) ~enc:`IEEE
-    | Ppc_fp128 -> Typ.float ~bits:128 ~enc:`Pair
+    | Ppc_fp128 -> Typ.float ~bits:128 ~siz:(size_of x llt) ~enc:`Pair
-    | Integer -> Typ.integer ~bits:(Llvm.integer_bitwidth llt)
+    | Integer ->
-    | X86_mmx -> Typ.integer ~bits:64
+        Typ.integer ~bits:(Llvm.integer_bitwidth llt) ~siz:(size_of x llt)
+    | X86_mmx -> Typ.integer ~bits:64 ~siz:(size_of x llt)
     | Function ->
         let return = xlate_type_opt x (Llvm.return_type llt) in
         let llargs = Llvm.param_types llt in
@@ -228,11 +229,11 @@ let rec xlate_type : x -> Llvm.lltype -> Typ.t =
     | Vector ->
         let elt = xlate_type x (Llvm.element_type llt) in
         let len = Llvm.vector_size llt in
-        Typ.array ~elt ~len
+        Typ.array ~elt ~len ~siz:(size_of x llt)
     | Array ->
         let elt = xlate_type x (Llvm.element_type llt) in
         let len = Llvm.array_length llt in
-        Typ.array ~elt ~len
+        Typ.array ~elt ~len ~siz:(size_of x llt)
     | Struct ->
         let llelts = Llvm.struct_element_types llt in
         let len = Array.length llelts in
@@ -241,16 +242,16 @@ let rec xlate_type : x -> Llvm.lltype -> Typ.t =
           let elts =
             Vector.map ~f:(xlate_type x) (Vector.of_array llelts)
           in
-          Typ.tuple elts ~packed
+          Typ.tuple elts ~siz:(size_of x llt) ~packed
         else
           let name = struct_name llt in
-          if Llvm.is_opaque llt then Typ.opaque ~name
+          if Llvm.is_opaque llt then Typ.opaque ~name ~siz:(size_of x llt)
           else
             let elts =
               Vector.init len ~f:(fun i -> lazy (xlate_type x llelts.(i)))
             in
-            Typ.struct_ ~name elts ~packed
+            Typ.struct_ ~name elts ~siz:(size_of x llt) ~packed
-    | Token -> Typ.opaque ~name:"token"
+    | Token -> Typ.opaque ~name:"token" ~siz:(size_of x llt)
     | Void | Label | Metadata -> assert false
   in
   Hashtbl.find_or_add memo_type llt ~default:(fun () ->
@@ -379,9 +380,11 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
         | Integer _ -> Exp.integer typ Z.zero
         | Pointer _ -> Exp.null
         | Array _ | Tuple _ | Struct _ ->
+            let llsiz = size_of x llt in
+            if llsiz = 0 then todo "ConstantAggregateZero of size 0" () ;
             Exp.splat typ
               ~byt:(Exp.integer Typ.byt Z.zero)
-              ~siz:(Exp.integer Typ.siz (Z.of_int (size_of x llt)))
+              ~siz:(Exp.integer Typ.siz (Z.of_int llsiz))
         | _ -> fail "ConstantAggregateZero of type %a" Typ.pp typ () )
     | ConstantVector | ConstantArray ->
         let typ = xlate_type x (Llvm.type_of llv) in
@@ -716,9 +719,11 @@ let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Typ.t * Llvm.lltype =
   (i32, xlate_type x tip, cxa_exception)
 
 let exception_typs =
-  let pi8 = Typ.pointer ~elt:(Typ.integer ~bits:8) in
+  let pi8 = Typ.pointer ~elt:Typ.byt in
-  let i32 = Typ.integer ~bits:32 in
+  let i32 = Typ.integer ~bits:32 ~siz:4 in
-  let exc = Typ.tuple ~packed:false (Vector.of_array [|pi8; i32|]) in
+  let exc =
+    Typ.tuple ~packed:false (Vector.of_array [|pi8; i32|]) ~siz:12
+  in
   (pi8, i32, exc)
 
 (** Translate a control transfer from instruction [instr] to block [dst] to

sledge/src/llair/llair.ml

@@ -219,9 +219,8 @@ let rec dummy_block =
   ; sort_index= 0 }
 
 and dummy_func =
-  let dummy_ptr_typ = Typ.pointer ~elt:(Typ.opaque ~name:"dummy") in
+  let dummy_reg = Reg.program ~global:() Typ.ptr "dummy" in
-  let dummy_reg = Reg.program ~global:() dummy_ptr_typ "dummy" in
+  { name= Global.mk dummy_reg Typ.ptr Loc.none
-  { name= Global.mk dummy_reg dummy_ptr_typ Loc.none
   ; params= []
   ; freturn= None
   ; fthrow= dummy_reg
@@ -432,7 +431,7 @@ module Func = struct
     assert (func == func.entry.parent) ;
     let {name= {typ; _}; cfg; _} = func in
     match typ with
-    | Pointer {elt= Function {return; _}} ->
+    | Pointer {elt= Function {return; _}; _} ->
         assert (
           not
             (Vector.contains_dup cfg ~compare:(fun b1 b2 ->

sledge/src/llair/term.ml

@@ -500,7 +500,7 @@ let simp_convert ~unsigned dst src arg =
   if (not unsigned) && Typ.equivalent dst src then arg
   else
     match (dst, src, arg) with
-    | Integer {bits= m}, Integer {bits= n}, Integer {data} ->
+    | Integer {bits= m; _}, Integer {bits= n; _}, Integer {data} ->
         integer (Z.extract ~unsigned (min m n) data)
     | _ -> Ap1 (Convert {unsigned; dst; src}, arg)
 
@@ -951,8 +951,7 @@ let select ~rcd ~idx = norm1 (Select idx) rcd
 let update ~rcd ~idx ~elt = norm2 (Update idx) rcd elt
 
 let size_of t =
-  Option.bind (Typ.prim_bit_size_of t) ~f:(fun n ->
+  Option.map ~f:(fun n -> integer (Z.of_int n)) (Typ.size_of t)
-      if n % 8 = 0 then Some (integer (Z.of_int (n / 8))) else None )
 
 (** Transform *)
 

sledge/src/llair/typ.ml

@@ -9,17 +9,18 @@
 
 type t =
   | Function of {return: t option; args: t vector}
-  | Integer of {bits: int}
+  | Integer of {bits: int; siz: int}
-  | Float of {bits: int; enc: [`IEEE | `Extended | `Pair]}
+  | Float of {bits: int; siz: int; enc: [`IEEE | `Extended | `Pair]}
   | Pointer of {elt: t}
-  | Array of {elt: t; len: int}
+  | Array of {elt: t; len: int; siz: int}
-  | Tuple of {elts: t vector; packed: bool}
+  | Tuple of {elts: t vector; siz: int; packed: bool}
   | Struct of
       { name: string
       ; elts: t vector (* possibly cyclic, name unique *)
             [@compare.ignore] [@equal.ignore] [@sexp_drop_if fun _ -> true]
+      ; siz: int
       ; packed: bool }
-  | Opaque of {name: string}
+  | Opaque of {name: string; siz: int}
 [@@deriving compare, equal, hash, sexp]
 
 let rec pp fs typ =
@@ -77,34 +78,34 @@ let invariant t =
 (** Constructors *)
 
 let function_ ~return ~args = Function {return; args} |> check invariant
-let integer ~bits = Integer {bits} |> check invariant
+let integer ~bits ~siz = Integer {bits; siz} |> check invariant
-let float ~bits ~enc = Float {bits; enc} |> check invariant
+let float ~bits ~siz ~enc = Float {bits; siz; enc} |> check invariant
 let pointer ~elt = Pointer {elt} |> check invariant
-let array ~elt ~len = Array {elt; len} |> check invariant
+let array ~elt ~len ~siz = Array {elt; len; siz} |> check invariant
-let tuple elts ~packed = Tuple {elts; packed} |> check invariant
+let tuple elts ~siz ~packed = Tuple {elts; siz; packed} |> check invariant
-let opaque ~name = Opaque {name} |> check invariant
+let opaque ~name ~siz = Opaque {name; siz} |> check invariant
 
 let struct_ =
   let defns : (string, t) Hashtbl.t = Hashtbl.create (module String) in
-  let dummy_typ = Opaque {name= "dummy"} in
+  let dummy_typ = Opaque {name= "dummy"; siz= 0} in
-  fun ~name ~packed elt_thks ->
+  fun ~name ~siz ~packed elt_thks ->
     match Hashtbl.find defns name with
     | Some typ -> typ
     | None ->
         (* Add placeholder defn to prevent computing [elts] in calls to
            [struct] from [elts] for recursive occurrences of [name]. *)
         let elts = Array.create ~len:(Vector.length elt_thks) dummy_typ in
-        let typ = Struct {name; elts= Vector.of_array elts; packed} in
+        let typ = Struct {name; elts= Vector.of_array elts; siz; packed} in
         Hashtbl.set defns ~key:name ~data:typ ;
         Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elts.(i) <- elt) ;
         typ |> check invariant
 
 (** Constants *)
 
-let bool = integer ~bits:1
+let bool = integer ~bits:1 ~siz:1
-let byt = integer ~bits:8
+let byt = integer ~bits:8 ~siz:1
-let int = integer ~bits:32
+let int = integer ~bits:32 ~siz:4
-let siz = integer ~bits:64
+let siz = integer ~bits:64 ~siz:8
 
 (** [ptr] is semantically equivalent to [siz], but has a distinct
     representation because the element type is important for [Global]s *)
@@ -112,6 +113,17 @@ let ptr = pointer ~elt:byt
 
 (** Queries *)
 
+let size_of = function
+  | Function _ -> None
+  | Integer {siz}
+   |Float {siz}
+   |Array {siz}
+   |Tuple {siz}
+   |Struct {siz}
+   |Opaque {siz} ->
+      Some siz
+  | Pointer _ -> Some 8
+
 let rec prim_bit_size_of = function
   | Integer {bits} | Float {bits} -> Some bits
   | Pointer _ -> prim_bit_size_of siz
@@ -130,12 +142,8 @@ let rec equivalent t0 t1 =
   | _ -> equal t0 t1
 
 let castable t0 t1 =
-  match (t0, t1) with
+  match (size_of t0, size_of t1) with
-  | ( (Pointer _ | Integer _ | Float _ | Array _)
+  | Some m, Some n -> m = n
-    , (Pointer _ | Integer _ | Float _ | Array _) ) -> (
-    match (prim_bit_size_of t0, prim_bit_size_of t1) with
-    | Some n0, Some n1 -> n0 = n1
-    | _ -> false )
   | _ -> equal t0 t1
 
 let rec convertible t0 t1 =

sledge/src/llair/typ.mli

@@ -10,19 +10,19 @@
 type t = private
   | Function of {return: t option; args: t vector}
       (** (Global) function names have type Pointer to Function. *)
-  | Integer of {bits: int}  (** Integer of given bitwidth. *)
+  | Integer of {bits: int; siz: int}  (** Integer of given bitwidth. *)
-  | Float of {bits: int; enc: [`IEEE | `Extended | `Pair]}
+  | Float of {bits: int; siz: int; enc: [`IEEE | `Extended | `Pair]}
       (** Floating-point numbers of given bitwidth and encoding. *)
   | Pointer of {elt: t}  (** Pointer to element type. *)
-  | Array of {elt: t; len: int}
+  | Array of {elt: t; len: int; siz: int}
       (** Statically-sized array of [len] elements of type [elt]. *)
-  | Tuple of {elts: t vector; packed: bool}
+  | Tuple of {elts: t vector; siz: int; packed: bool}
       (** Anonymous aggregate of heterogeneous types. *)
-  | Struct of {name: string; elts: t vector; packed: bool}
+  | Struct of {name: string; elts: t vector; siz: int; packed: bool}
       (** Uniquely named aggregate of heterogeneous types. Every cycle of
           recursive types contains a [Struct]. NOTE: recursive [Struct]
           types are represented by cyclic values. *)
-  | Opaque of {name: string}
+  | Opaque of {name: string; siz: int}
       (** Uniquely named aggregate type whose definition is hidden. *)
 [@@deriving compare, equal, hash, sexp]
 
@@ -39,16 +39,17 @@ val int : t
 val siz : t
 val ptr : t
 val function_ : return:t option -> args:t vector -> t
-val integer : bits:int -> t
+val integer : bits:int -> siz:int -> t
-val float : bits:int -> enc:[`Extended | `IEEE | `Pair] -> t
+val float : bits:int -> siz:int -> enc:[`Extended | `IEEE | `Pair] -> t
 val pointer : elt:t -> t
-val array : elt:t -> len:int -> t
+val array : elt:t -> len:int -> siz:int -> t
-val tuple : t vector -> packed:bool -> t
+val tuple : t vector -> siz:int -> packed:bool -> t
-val struct_ : name:string -> packed:bool -> t lazy_t vector -> t
+val struct_ : name:string -> siz:int -> packed:bool -> t lazy_t vector -> t
-val opaque : name:string -> t
+val opaque : name:string -> siz:int -> t
 
 (** Queries *)
 
+val size_of : t -> int option
 val prim_bit_size_of : t -> int option
 
 val is_sized : t -> bool

sledge/src/symbheap/equality_test.ml

@@ -16,8 +16,8 @@ let%test_module _ =
     let pp = printf pp
     let pp_classes = printf pp_classes
     let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r)
-    let i8 = Typ.integer ~bits:8
+    let i8 = Typ.int
-    let i64 = Typ.integer ~bits:64
+    let i64 = Typ.siz
     let ( ! ) i = Term.integer (Z.of_int i)
     let ( + ) = Term.add
     let ( - ) = Term.sub
@@ -99,10 +99,10 @@ let%test_module _ =
       pp r2 ;
       [%expect
         {|
-          %x_5 = %y_6 = %z_7 = ((i64)(i8) %x_5)
+          %x_5 = %y_6 = %z_7 = ((i64)(i32) %x_5)
 
           {sat= true;
-           rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [((i64)(i8) %x_5) ↦ %x_5]]} |}]
+           rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [((i64)(i32) %x_5) ↦ %x_5]]} |}]
 
     let%test _ = entails_eq r2 x z
     let%test _ = entails_eq (or_ r1 r2) x y