diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml index 2b8fc867c..1c500160a 100644 --- a/sledge/cli/frontend.ml +++ b/sledge/cli/frontend.ml @@ -374,7 +374,7 @@ let memo_value : (Inst.t list * Exp.t) ValTbl.t = ValTbl.create () module GlobTbl = LlvalueTbl -let memo_global : Global.t GlobTbl.t = GlobTbl.create () +let memo_global : GlobalDefn.t GlobTbl.t = GlobTbl.create () let should_inline : Llvm.llvalue -> bool = fun llv -> @@ -746,7 +746,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Inst.t list * Exp.t |> [%Trace.retn fun {pf} -> pf "%a" pp_prefix_exp] -and xlate_global : x -> Llvm.llvalue -> Global.t = +and xlate_global : x -> Llvm.llvalue -> GlobalDefn.t = fun x llg -> GlobTbl.find_or_add memo_global llg ~default:(fun () -> [%Trace.call fun {pf} -> pf "%a" pp_llvalue llg] @@ -755,7 +755,7 @@ and xlate_global : x -> Llvm.llvalue -> Global.t = let loc = find_loc llg in (* add to tbl without initializer in case of recursive occurrences in its own initializer *) - GlobTbl.set memo_global ~key:llg ~data:(Global.mk g loc) ; + GlobTbl.set memo_global ~key:llg ~data:(GlobalDefn.mk g loc) ; let init = match Llvm.classify_value llg with | GlobalVariable -> @@ -770,9 +770,9 @@ and xlate_global : x -> Llvm.llvalue -> Global.t = (init, size_of x (Llvm.type_of llv)) ) | _ -> None in - Global.mk ?init g loc + GlobalDefn.mk ?init g loc |> - [%Trace.retn fun {pf} -> pf "%a" Global.pp_defn] ) + [%Trace.retn fun {pf} -> pf "%a" GlobalDefn.pp_defn] ) type pop_thunk = Loc.t -> Llair.inst list @@ -1147,7 +1147,7 @@ let xlate_instr : && not (Llvm.is_declaration llfunc) then warn "ignoring variable arguments to variadic function: %a" - Global.pp (xlate_global x llfunc) () ; + GlobalDefn.pp (xlate_global x llfunc) () ; assert (Poly.(Llvm.classify_type lltyp = Pointer)) ; Array.length (Llvm.param_types (Llvm.element_type lltyp)) ) in diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml index 57688cccd..e18605ddc 100644 --- a/sledge/src/domain_intf.ml +++ b/sledge/src/domain_intf.ml @@ -11,7 +11,7 @@ module type Dom = sig val pp : t pp val report_fmt_thunk : t -> Format.formatter -> unit - val init : Llair.Global.t iarray -> t + val init : Llair.GlobalDefn.t iarray -> t val join : t -> t -> t option val is_false : t -> bool val dnf : t -> t list diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index fc61d8612..4ff5c8c29 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -21,8 +21,8 @@ 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 with - | {Llair.Global.reg; init= Some (seq, siz)} -> + match (global : Llair.GlobalDefn.t) with + | {reg; init= Some (seq, siz)} -> let loc = Term.var (X.reg reg) in let len = Term.integer (Z.of_int siz) in let seq = X.term seq in diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml index 9b2c57c42..4267087c9 100644 --- a/sledge/src/domain_used_globals.ml +++ b/sledge/src/domain_used_globals.ml @@ -14,7 +14,8 @@ let report_fmt_thunk = Fun.flip pp let empty = Llair.Reg.Set.empty let init globals = - [%Trace.info "pgm globals: {%a}" (IArray.pp ", " Llair.Global.pp) globals] ; + [%Trace.info + "pgm globals: {%a}" (IArray.pp ", " Llair.GlobalDefn.pp) globals] ; empty let join l r = Some (Llair.Reg.Set.union l r) diff --git a/sledge/src/llair/global.ml b/sledge/src/llair/globalDefn.ml similarity index 100% rename from sledge/src/llair/global.ml rename to sledge/src/llair/globalDefn.ml diff --git a/sledge/src/llair/global.mli b/sledge/src/llair/globalDefn.mli similarity index 100% rename from sledge/src/llair/global.mli rename to sledge/src/llair/globalDefn.mli diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index 0f13731cd..6d3bacc5a 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -14,7 +14,7 @@ module Typ = Typ module Reg = Reg module Exp = Exp module Function = Function -module Global = Global +module GlobalDefn = GlobalDefn type inst = | Move of {reg_exps: (Reg.t * Exp.t) iarray; loc: Loc.t} @@ -125,7 +125,7 @@ let equal_block x y = Int.equal x.sort_index y.sort_index type functions = func Function.Map.t [@@deriving sexp_of] -type program = {globals: Global.t iarray; functions: functions} +type program = {globals: GlobalDefn.t iarray; functions: functions} [@@deriving sexp_of] let pp_inst fs inst = @@ -601,7 +601,7 @@ module Program = struct assert ( not (Iter.contains_dup (IArray.to_iter pgm.globals) ~cmp:(fun g1 g2 -> - Reg.compare g1.Global.reg g2.Global.reg )) ) + Reg.compare g1.GlobalDefn.reg g2.GlobalDefn.reg )) ) let mk ~globals ~functions = { globals= IArray.of_list_rev globals @@ -610,7 +610,7 @@ module Program = struct let pp fs {globals; functions} = Format.fprintf fs "@[@[%a@]@ @ @ @[%a@]@]" - (IArray.pp "@\n@\n" Global.pp_defn) + (IArray.pp "@\n@\n" GlobalDefn.pp_defn) globals (List.pp "@\n@\n" Func.pp) ( Function.Map.values functions diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index 640012fd1..f4679c3e8 100644 --- a/sledge/src/llair/llair.mli +++ b/sledge/src/llair/llair.mli @@ -13,7 +13,7 @@ module Typ = Typ module Reg = Reg module Exp = Exp module Function = Function -module Global = Global +module GlobalDefn = GlobalDefn (** Instructions for memory manipulation or other non-control effects. *) type inst = private @@ -104,7 +104,7 @@ and func = private type functions type program = private - { globals: Global.t iarray (** Global variable definitions. *) + { globals: GlobalDefn.t iarray (** Global definitions. *) ; functions: functions (** (Global) function definitions. *) } module Inst : sig @@ -213,5 +213,5 @@ module Program : sig include Invariant.S with type t := t - val mk : globals:Global.t list -> functions:func list -> t + val mk : globals:GlobalDefn.t list -> functions:func list -> t end