[sledge] Do not store size of globals separately

Summary:
Now that expression types and type sizes can be computed, it is not
necessary to store the sizes of globals separately.

Reviewed By: ngorogiannis

Differential Revision: D17801932

fbshipit-source-id: f746e506b

sledge/src/llair/exp.mli

@@ -205,5 +205,6 @@ 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/llair/frontend.ml

@@ -654,13 +654,8 @@ and xlate_global : x -> Llvm.llvalue -> Global.t =
       Hashtbl.set memo_global ~key:llg ~data:(Global.mk g typ loc) ;
       let init =
         match Llvm.classify_value llg with
-        | GlobalVariable -> (
+        | GlobalVariable ->
-          match Llvm.global_initializer llg with
+            Option.map ~f:(xlate_value x) (Llvm.global_initializer llg)
-          | Some llinit ->
-              let siz = size_of x (Llvm.element_type llt) in
-              let init = xlate_value x llinit in
-              Some (init, siz)
-          | _ -> None )
         | _ -> None
       in
       Global.mk ?init g typ loc

sledge/src/llair/global.ml

@@ -7,7 +7,7 @@
 
 (** Global variables *)
 
-type t = {reg: Reg.t; init: (Exp.t * int) option; typ: Typ.t; loc: Loc.t}
+type t = {reg: Reg.t; init: Exp.t option; typ: Typ.t; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
 let pp fs {reg} =
@@ -20,7 +20,7 @@ let pp fs {reg} =
 
 let pp_defn fs {reg; init; typ; loc} =
   Format.fprintf fs "@[<2>%a %a%a%a@]" Typ.pp typ Reg.pp reg Loc.pp loc
-    (Option.pp "@ = @[%a@]" (fun fs (init, _) -> Exp.pp fs init))
+    (Option.pp "@ = @[%a@]" Exp.pp)
     init
 
 let invariant g =

sledge/src/llair/global.mli

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

sledge/src/symbheap/sh_domain.ml

@@ -19,9 +19,9 @@ let report_fmt_thunk = Fn.flip pp
 
 let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
-    | {Global.reg; init= Some (arr, siz)} ->
+    | {Global.reg; init= Some arr} ->
         let loc = Term.var (Reg.var reg) in
-        let len = Term.integer (Z.of_int siz) in
+        let len = Term.size_of (Exp.typ arr) in
         let arr = arr.term in
         Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
     | _ -> q )