[sledge] Use the size of a global's type instead of maintaining separately

Summary:
Global constants have reliable types, and their sizes can be used
instead of storing the size of the initializer separately.

Reviewed By: jvillard

Differential Revision: D24934114

fbshipit-source-id: 2426ab5be

sledge/cli/frontend.ml

@@ -769,7 +769,7 @@ and xlate_global : x -> Llvm.llvalue -> GlobalDefn.t =
                 let is_nondet = function Nondet _ -> true | _ -> false in
                 if not (List.for_all ~f:is_nondet pre) then
                   todo "global initializer instructions" () ;
-                (init, size_of x (Llvm.type_of llv)) )
+                init )
         | _ -> None
       in
       GlobalDefn.mk ?init g loc

sledge/src/domain_sh.ml

@@ -22,8 +22,13 @@ let simplify q = if !simplify_states then Sh.simplify q else q
 let init globals =
   IArray.fold globals Sh.emp ~f:(fun global q ->
       match (global : Llair.GlobalDefn.t) with
-      | {name; init= Some (seq, siz)} ->
+      | {name; init= Some seq} ->
           let loc = X.global name in
+          let siz =
+            match Llair.Global.typ name with
+            | Pointer {elt} -> Llair.Typ.size_of elt
+            | _ -> violates Llair.GlobalDefn.invariant global
+          in
           let len = Term.integer (Z.of_int siz) in
           let seq = X.term seq in
           Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; seq})

sledge/src/llair/globalDefn.ml

@@ -7,18 +7,19 @@
 
 (** Global variables *)
 
-type t = {name: Global.t; init: (Exp.t * int) option; loc: Loc.t}
+type t = {name: Global.t; init: Exp.t option; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
 let pp ppf {name; init; loc} =
   Format.fprintf ppf "@[<2>%a %a%a %a@]" Typ.pp (Global.typ name) Global.pp
     name
     (Option.pp "@ = @[%a@]" Exp.pp)
-    (Option.map ~f:fst init) Loc.pp loc
+    init Loc.pp loc
 
 let invariant g =
   let@ () = Invariant.invariant [%here] g [%sexp_of: t] in
-  let {name} = g in
-  assert (Typ.is_sized (Global.typ name))
+  match Global.typ g.name with
+  | Pointer {elt} -> assert (Option.is_none g.init || Typ.is_sized elt)
+  | _ -> assert false
 
 let mk ?init name loc = {name; init; loc} |> check invariant

sledge/src/llair/globalDefn.mli

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