[sledge] Rename Global to GlobalDefn

Summary:
This module represents the definition of a global constant, rather
than the global itself.

Reviewed By: jvillard

Differential Revision: D24846673

fbshipit-source-id: d47e67984

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

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

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

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)

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 "@[<v>@[%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

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