[sledge] Change: Rely on llvm size computation for global initializers

Summary:
Rather than compute the size of the llair type of the llair
initializer expression, compute the size of the llvm initializer
directly.

Reviewed By: ngorogiannis

Differential Revision: D21720982

fbshipit-source-id: 4364baf38

sledge/bin/frontend.ml

@@ -671,19 +671,18 @@ and xlate_global stk : x -> Llvm.llvalue -> Global.t =
       [%Trace.call fun {pf} -> pf "%a" pp_llvalue llg]
       ;
       let g = xlate_name x ~global:() llg in
-      let llt = Llvm.type_of llg in
-      let typ = xlate_type x llt in
       let loc = find_loc llg in
       (* add to tbl without initializer in case of recursive occurrences in
          its own initializer *)
-      Hashtbl.set memo_global ~key:llg ~data:(Global.mk g typ loc) ;
+      Hashtbl.set memo_global ~key:llg ~data:(Global.mk g loc) ;
       let init =
         match Llvm.classify_value llg with
         | GlobalVariable ->
-            Option.map ~f:(xlate_value stk x) (Llvm.global_initializer llg)
+            Option.map (Llvm.global_initializer llg) ~f:(fun llv ->
+                (xlate_value stk x llv, size_of x (Llvm.type_of llv)) )
         | _ -> None
       in
-      Global.mk ?init g typ loc
+      Global.mk ?init g loc
       |>
       [%Trace.retn fun {pf} -> pf "%a" Global.pp_defn] )
 
@@ -1335,7 +1334,7 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
       [] llf
   in
   let freturn =
-    match name.typ with
+    match Reg.typ name.reg with
     | Pointer {elt= Function {return= Some typ; _}} ->
         Some (Reg.program typ "freturn")
     | _ -> None

sledge/src/domain_sh.ml

@@ -18,9 +18,9 @@ let simplify q = if !simplify_states then Sh.simplify q else q
 
 let init globals =
   IArray.fold globals ~init:Sh.emp ~f:(fun q -> function
-    | {Global.reg; init= Some arr} ->
+    | {Global.reg; init= Some (arr, siz)} ->
         let loc = Term.var (Reg.var reg) in
-        let len = Term.integer (Z.of_int (Typ.size_of (Exp.typ arr))) in
+        let len = Term.integer (Z.of_int siz) in
         let arr = arr.term in
         Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
     | _ -> q )

sledge/src/exp.ml

@@ -279,7 +279,6 @@ and typ_of exp =
       typ
   [@@warning "-9"]
 
-let typ = typ_of
 let pp_exp = pp
 
 (** Registers are the expressions constructed by [Reg] *)

sledge/src/exp.mli

@@ -194,6 +194,5 @@ val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a
 (** Query *)
 
 val term : t -> Term.t
-val typ : t -> Typ.t
 val is_true : t -> bool
 val is_false : t -> bool

sledge/src/global.ml

@@ -7,7 +7,7 @@
 
 (** Global variables *)
 
-type t = {reg: Reg.t; init: Exp.t option; typ: Typ.t; loc: Loc.t}
+type t = {reg: Reg.t; init: (Exp.t * int) option; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
 let pp fs {reg} =
@@ -18,16 +18,17 @@ let pp fs {reg} =
   in
   pf "@%s%a" name Reg.pp_demangled reg
 
-let pp_defn fs {reg; init; typ; loc} =
+let pp_defn fs {reg; init; loc} =
-  Format.fprintf fs "@[<2>%a %a%a%a@]" Typ.pp typ Reg.pp reg Loc.pp loc
+  Format.fprintf fs "@[<2>%a %a%a%a@]" Typ.pp (Reg.typ reg) Reg.pp reg
+    Loc.pp loc
     (Option.pp "@ = @[%a@]" Exp.pp)
-    init
+    (Option.map ~f:fst init)
 
 let invariant g =
   Invariant.invariant [%here] g [%sexp_of: t]
   @@ fun () ->
-  let {reg; typ} = g in
+  let {reg} = g in
-  assert (Typ.is_sized typ) ;
+  assert (Typ.is_sized (Reg.typ reg)) ;
   assert (Var.is_global (Reg.var reg))
 
-let mk ?init reg typ loc = {reg; init; typ; loc} |> check invariant
+let mk ?init reg loc = {reg; init; loc} |> check invariant

sledge/src/global.mli

@@ -7,7 +7,7 @@
 
 (** Global variables *)
 
-type t = private {reg: Reg.t; init: Exp.t option; typ: Typ.t; loc: Loc.t}
+type t = private {reg: Reg.t; init: (Exp.t * int) option; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
 val pp : t pp
@@ -15,4 +15,4 @@ val pp_defn : t pp
 
 include Invariant.S with type t := t
 
-val mk : ?init:Exp.t -> Reg.t -> Typ.t -> Loc.t -> t
+val mk : ?init:Exp.t * int -> Reg.t -> Loc.t -> t

sledge/src/llair.ml

@@ -214,7 +214,7 @@ let rec dummy_block =
 
 and dummy_func =
   let dummy_reg = Reg.program ~global:() Typ.ptr "dummy" in
-  { name= Global.mk dummy_reg Typ.ptr Loc.none
+  { name= Global.mk dummy_reg Loc.none
   ; formals= []
   ; freturn= None
   ; fthrow= dummy_reg
@@ -436,7 +436,7 @@ module Func = struct
     let pp_if cnd str fs = if cnd then Format.fprintf fs str in
     Format.fprintf fs "@[<v>@[<v>%a%a@[<2>%a%a@]%t@]"
       (Option.pp "%a " Typ.pp)
-      ( match name.typ with
+      ( match Reg.typ name.reg with
       | Pointer {elt= Function {return; _}} -> return
       | _ -> None )
       (Option.pp " %a := " Reg.pp)
@@ -457,7 +457,7 @@ module Func = struct
     Invariant.invariant [%here] func [%sexp_of: t]
     @@ fun () ->
     assert (func == func.entry.parent) ;
-    match func.name.typ with
+    match Reg.typ func.name.reg with
     | Pointer {elt= Function {return; _}; _} ->
         assert (
           not