From 2118ebd92353b9999c778d4749e488e441515ff5 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 13 Nov 2020 07:32:48 -0800 Subject: [PATCH] [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 | 2 +- sledge/src/domain_sh.ml | 7 ++++++- sledge/src/llair/globalDefn.ml | 9 +++++---- sledge/src/llair/globalDefn.mli | 4 ++-- 4 files changed, 14 insertions(+), 8 deletions(-) diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml index 675a3c81e..49f9058bc 100644 --- a/sledge/cli/frontend.ml +++ b/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 diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 93bcdbc41..2c8f10cf0 100644 --- a/sledge/src/domain_sh.ml +++ b/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}) diff --git a/sledge/src/llair/globalDefn.ml b/sledge/src/llair/globalDefn.ml index f10b8539c..a29a02624 100644 --- a/sledge/src/llair/globalDefn.ml +++ b/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 diff --git a/sledge/src/llair/globalDefn.mli b/sledge/src/llair/globalDefn.mli index 5eaa1e489..55641a9b9 100644 --- a/sledge/src/llair/globalDefn.mli +++ b/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