[sledge] Fix size in translation of global variables

Summary:
Global variables have pointer type. The size needed by the backend is
of the element type, not of the pointer itself. This diff corrects
this.

Reviewed By: kren1

Differential Revision: D15577756

fbshipit-source-id: 948ecf3cd

sledge/src/llair/frontend.ml

@@ -573,21 +573,21 @@ and xlate_global : x -> Llvm.llvalue -> Global.t =
       let g = xlate_name llg in
       let llt = Llvm.type_of llg in
       let typ = xlate_type x llt in
-      let siz = size_of 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 siz typ loc) ;
+      Hashtbl.set memo_global ~key:llg ~data:(Global.mk g typ loc) ;
       let init =
         match (Llvm.classify_value llg, Llvm.linkage llg) with
         | _, (External | External_weak) -> None
         | GlobalVariable, _ ->
-            Some (xlate_value x (Llvm.global_initializer llg))
+            let siz = size_of x (Llvm.element_type llt) in
+            Some (xlate_value x (Llvm.global_initializer llg), siz)
         | _ -> None
       in
-      Global.mk ?init g siz typ loc
+      Global.mk ?init g typ loc
       |>
-      [%Trace.retn fun {pf} -> pf "%a" Global.pp] )
+      [%Trace.retn fun {pf} -> pf "%a" Global.pp_defn] )
 
 type pop_thunk = Loc.t -> Llair.inst list
 

sledge/src/llair/global.ml

@@ -7,7 +7,7 @@
 
 (** Global variables *)
 
-type t = {var: Var.t; init: Exp.t option; siz: int; typ: Typ.t; loc: Loc.t}
+type t = {var: Var.t; init: (Exp.t * int) option; typ: Typ.t; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
 let pp fs {var} =
@@ -20,7 +20,7 @@ let pp fs {var} =
 
 let pp_defn fs {var; init; typ} =
   Format.fprintf fs "@[<2>%a %a%a@]" Typ.pp typ Var.pp var
-    (Option.pp " =@ @[%a@]" Exp.pp)
+    (Option.pp " =@ @[%a@]" (fun fs (init, _) -> Exp.pp fs init))
     init
 
 let invariant g =
@@ -29,4 +29,4 @@ let invariant g =
   let {typ} = g in
   assert (Typ.is_sized typ)
 
-let mk ?init var siz typ loc = {var; init; siz; typ; loc} |> check invariant
+let mk ?init var typ loc = {var; init; typ; loc} |> check invariant

sledge/src/llair/global.mli

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

sledge/src/llair/llair.ml

@@ -202,7 +202,7 @@ let rec dummy_block =
 
 and dummy_func =
   let dummy_ptr_typ = Typ.pointer ~elt:(Typ.opaque ~name:"dummy") in
-  { name= Global.mk (Var.program "dummy") 0 dummy_ptr_typ Loc.none
+  { name= Global.mk (Var.program "dummy") dummy_ptr_typ Loc.none
   ; entry= dummy_block
   ; cfg= Vector.empty }
 

sledge/src/symbheap/domain.ml

@@ -13,7 +13,7 @@ let pp = Sh.pp
 
 let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
-    | {Global.var; init= Some arr; siz} ->
+    | {Global.var; init= Some (arr, siz)} ->
         let loc = Exp.var var in
         let len = Exp.integer (Z.of_int siz) Typ.siz in
         Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})