From 967a9e1c5814fa3142bc9806073066acce85e13a Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 7 Jun 2020 04:59:25 -0700 Subject: [PATCH] [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 | 11 +++++------ sledge/src/domain_sh.ml | 4 ++-- sledge/src/exp.ml | 1 - sledge/src/exp.mli | 1 - sledge/src/global.ml | 15 ++++++++------- sledge/src/global.mli | 4 ++-- sledge/src/llair.ml | 6 +++--- 7 files changed, 20 insertions(+), 22 deletions(-) diff --git a/sledge/bin/frontend.ml b/sledge/bin/frontend.ml index 339ff8b0b..c874cf146 100644 --- a/sledge/bin/frontend.ml +++ b/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 diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 7ca98248a..7d64b9e37 100644 --- a/sledge/src/domain_sh.ml +++ b/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 ) diff --git a/sledge/src/exp.ml b/sledge/src/exp.ml index 6a22228a9..384d37fe0 100644 --- a/sledge/src/exp.ml +++ b/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] *) diff --git a/sledge/src/exp.mli b/sledge/src/exp.mli index a27411904..e29477791 100644 --- a/sledge/src/exp.mli +++ b/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 diff --git a/sledge/src/global.ml b/sledge/src/global.ml index 966314600..c88e0d092 100644 --- a/sledge/src/global.ml +++ b/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} = - Format.fprintf fs "@[<2>%a %a%a%a@]" Typ.pp typ Reg.pp reg Loc.pp loc +let pp_defn fs {reg; init; 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 - assert (Typ.is_sized typ) ; + let {reg} = g in + 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 diff --git a/sledge/src/global.mli b/sledge/src/global.mli index 5f6200005..d6550daf0 100644 --- a/sledge/src/global.mli +++ b/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 diff --git a/sledge/src/llair.ml b/sledge/src/llair.ml index 3b6e00d7c..a285692b3 100644 --- a/sledge/src/llair.ml +++ b/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 "@[@[%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