[sledge] Add LLAIR expression form for globals

Summary:
Distinguish expressions that name globals from registers. This leads
to clearer code, and globals are semantically distinct from general
registers. In particular, they are constant, so any machinery for
handling assignment does not need to consider them. This diff only
adds the distinction to LLAIR, it is not pushed through to FOL, which
will come later.

Reviewed By: jvillard

Differential Revision: D24846676

fbshipit-source-id: 3aca025bf

sledge/cli/domain_itv.ml

@@ -65,7 +65,7 @@ let rec apron_typ_of_llair_typ : Llair.Typ.t -> Texpr1.typ option = function
 
 let rec apron_texpr_of_llair_exp exp q =
   match (exp : Llair.Exp.t) with
-  | Reg {name} | Function {name} ->
+  | Reg {name} | Global {name} | Function {name} ->
       Some (Texpr1.Var (apron_var_of_name name))
   | Integer {data} -> Some (Texpr1.Cst (Coeff.s_of_int (Z.to_int data)))
   | Float {data} -> (
@@ -278,7 +278,7 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
     todo "Summaries not yet implemented for interval analysis" ()
   else
     let mangle r =
-      Llair.Reg.program (Llair.Reg.typ r) ("__tmp__" ^ Llair.Reg.name r)
+      Llair.Reg.mk (Llair.Reg.typ r) ("__tmp__" ^ Llair.Reg.name r)
     in
     let args = List.combine_exn formals actuals in
     let q' = List.fold ~f:(fun (f, a) q -> assign (mangle f) a q) args q in
@@ -311,4 +311,4 @@ type summary = t
 
 let pp_summary = pp
 let apply_summary _ _ = None
-let create_summary ~locals:_ ~formals:_ q = (q, q)
+let create_summary ~globals:_ ~locals:_ ~formals:_ q = (q, q)

sledge/cli/frontend.ml

@@ -343,10 +343,10 @@ let xlate_float : x -> Llvm.llvalue -> Exp.t =
   let data = suffix_after_last_space (Llvm.string_of_llvalue llv) in
   Exp.float typ data
 
-let xlate_name x ?global : Llvm.llvalue -> Reg.t =
+let xlate_name x : Llvm.llvalue -> Reg.t =
  fun llv ->
   let typ = xlate_type x (Llvm.type_of llv) in
-  Reg.program ?global typ (find_name llv)
+  Reg.mk typ (find_name llv)
 
 let xlate_name_opt : x -> Llvm.llvalue -> Reg.t option =
  fun x instr ->
@@ -457,7 +457,7 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
         , Exp.function_
             (Function.mk (xlate_type x (Llvm.type_of llv)) (find_name llv))
         )
-    | GlobalVariable -> ([], Exp.reg (xlate_global x llv).reg)
+    | GlobalVariable -> ([], Exp.global (xlate_global x llv).name)
     | GlobalAlias -> xlate_value x (Llvm.operand llv 0)
     | ConstantInt -> ([], xlate_int x llv)
     | ConstantFP -> ([], xlate_float x llv)
@@ -501,7 +501,7 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
           todo "types with undetermined size: %a" pp_lltype llt () ;
         let name = Printf.sprintf "undef_%i" !undef_count in
         let loc = Loc.none in
-        let reg = Reg.program typ name in
+        let reg = Reg.mk typ name in
         let msg = Llvm.string_of_llvalue llv in
         ([Inst.nondet ~reg:(Some reg) ~msg ~loc], Exp.reg reg)
     | Instruction
@@ -751,7 +751,7 @@ and xlate_global : x -> Llvm.llvalue -> GlobalDefn.t =
   GlobTbl.find_or_add memo_global llg ~default:(fun () ->
       [%Trace.call fun {pf} -> pf "%a" pp_llvalue llg]
       ;
-      let g = xlate_name x ~global:() llg in
+      let g = Global.mk (xlate_type x (Llvm.type_of llg)) (find_name llg) in
       let loc = find_loc llg in
       (* add to tbl without initializer in case of recursive occurrences in
          its own initializer *)
@@ -772,7 +772,7 @@ and xlate_global : x -> Llvm.llvalue -> GlobalDefn.t =
       in
       GlobalDefn.mk ?init g loc
       |>
-      [%Trace.retn fun {pf} -> pf "%a" GlobalDefn.pp_defn] )
+      [%Trace.retn fun {pf} -> pf "%a" GlobalDefn.pp] )
 
 type pop_thunk = Loc.t -> Llair.inst list
 
@@ -925,7 +925,7 @@ let rec xlate_func_name x llv =
       ( []
       , Exp.function_
           (Function.mk (xlate_type x (Llvm.type_of llv)) (find_name llv)) )
-  | GlobalVariable -> ([], Exp.reg (xlate_name x ~global:() llv))
+  | GlobalVariable -> ([], Exp.global (xlate_global x llv).name)
   | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
   | Argument | Instruction _ -> xlate_value x llv
   | GlobalAlias -> xlate_func_name x (Llvm.operand llv 0)
@@ -1147,7 +1147,7 @@ let xlate_instr :
             && not (Llvm.is_declaration llfunc)
           then
             warn "ignoring variable arguments to variadic function: %a"
-              GlobalDefn.pp (xlate_global x llfunc) () ;
+              Global.pp (xlate_global x llfunc).name () ;
           assert (Poly.(Llvm.classify_type lltyp = Pointer)) ;
           Array.length (Llvm.param_types (Llvm.element_type lltyp)) )
       in
@@ -1264,8 +1264,8 @@ let xlate_instr :
          e.g. either cleanup or rethrow. *)
       let i32, tip, cxa_exception = landingpad_typs x instr in
       let pi8, _, exc_typ = exception_typs in
-      let exc = Exp.reg (Reg.program pi8 (find_name instr ^ ".exc")) in
-      let ti = Reg.program tip (name ^ ".ti") in
+      let exc = Exp.reg (Reg.mk pi8 (find_name instr ^ ".exc")) in
+      let ti = Reg.mk tip (name ^ ".ti") in
       (* std::type_info* ti = ((__cxa_exception* )exc - 1)->exceptionType *)
       let load_ti =
         let typ = cxa_exception in
@@ -1451,11 +1451,11 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
   let freturn =
     match typ with
     | Pointer {elt= Function {return= Some typ; _}} ->
-        Some (Reg.program typ "freturn")
+        Some (Reg.mk typ "freturn")
     | _ -> None
   in
   let _, _, exc_typ = exception_typs in
-  let fthrow = Reg.program exc_typ "fthrow" in
+  let fthrow = Reg.mk exc_typ "fthrow" in
   ( match Llvm.block_begin llf with
   | Before entry_blk ->
       let pop = pop_stack_frame_of_function x llf entry_blk in

sledge/cli/sledge_cli.ml

@@ -91,15 +91,15 @@ let used_globals pgm preanalyze : Domain_used_globals.r =
         ; skip_throw= false
         ; function_summaries= true
         ; entry_points
-        ; globals= Declared Llair.Reg.Set.empty }
+        ; globals= Declared Llair.Global.Set.empty }
         pgm
     in
     Per_function
-      (Llair.Function.Map.map summary_table ~f:Llair.Reg.Set.union_list)
+      (Llair.Function.Map.map summary_table ~f:Llair.Global.Set.union_list)
   else
     Declared
-      (Llair.Reg.Set.of_iter
-         (Iter.map ~f:(fun g -> g.reg) (IArray.to_iter pgm.globals)))
+      (Llair.Global.Set.of_iter
+         (Iter.map ~f:(fun g -> g.name) (IArray.to_iter pgm.globals)))
 
 let analyze =
   let%map_open bound =

sledge/src/control.ml

@@ -322,9 +322,7 @@ module Make (Dom : Domain_intf.Dom) = struct
       else
         let globals = Domain_used_globals.by_function opts.globals name in
         let function_summary, post_state =
-          Dom.create_summary ~locals post_state
-            ~formals:
-              (Llair.Reg.Set.union (Llair.Reg.Set.of_list formals) globals)
+          Dom.create_summary ~globals ~locals ~formals post_state
         in
         Llair.Function.Tbl.add_multi ~key:name ~data:function_summary
           summary_table ;

sledge/src/domain_intf.ml

@@ -32,7 +32,7 @@ module type Dom = sig
 
   val call :
        summaries:bool
-    -> globals:Llair.Reg.Set.t
+    -> globals:Llair.Global.Set.t
     -> actuals:Llair.Exp.t list
     -> areturn:Llair.Reg.t option
     -> formals:Llair.Reg.t list
@@ -57,7 +57,11 @@ module type Dom = sig
   val pp_summary : summary pp
 
   val create_summary :
-    locals:Llair.Reg.Set.t -> formals:Llair.Reg.Set.t -> t -> summary * t
+       globals:Llair.Global.Set.t
+    -> locals:Llair.Reg.Set.t
+    -> formals:Llair.Reg.t list
+    -> t
+    -> summary * t
 
   val apply_summary : t -> summary -> t option
 end

sledge/src/domain_relation.ml

@@ -12,8 +12,9 @@ module type State_domain_sig = sig
   include Domain_intf.Dom
 
   val create_summary :
-       locals:Llair.Reg.Set.t
-    -> formals:Llair.Reg.Set.t
+       globals:Llair.Global.Set.t
+    -> locals:Llair.Reg.Set.t
+    -> formals:Llair.Reg.t list
     -> entry:t
     -> current:t
     -> summary * t
@@ -79,8 +80,8 @@ module Make (State_domain : State_domain_sig) = struct
         (List.pp ",@ " Llair.Exp.pp)
         (List.rev actuals)
         (List.pp ",@ " Llair.Reg.pp)
-        (List.rev formals) Llair.Reg.Set.pp locals Llair.Reg.Set.pp globals
-        State_domain.pp current]
+        (List.rev formals) Llair.Reg.Set.pp locals Llair.Global.Set.pp
+        globals State_domain.pp current]
     ;
     let caller_current, state_from_call =
       State_domain.call ~summaries ~globals ~actuals ~areturn ~formals
@@ -116,9 +117,9 @@ module Make (State_domain : State_domain_sig) = struct
 
   let pp_summary = State_domain.pp_summary
 
-  let create_summary ~locals ~formals (entry, current) =
+  let create_summary ~globals ~locals ~formals (entry, current) =
     let fs, next =
-      State_domain.create_summary ~locals ~formals ~entry ~current
+      State_domain.create_summary ~globals ~locals ~formals ~entry ~current
     in
     (fs, (entry, next))
 

sledge/src/domain_relation.mli

@@ -12,8 +12,9 @@ module type State_domain_sig = sig
   include Domain_intf.Dom
 
   val create_summary :
-       locals:Llair.Reg.Set.t
-    -> formals:Llair.Reg.Set.t
+       globals:Llair.Global.Set.t
+    -> locals:Llair.Reg.Set.t
+    -> formals:Llair.Reg.t list
     -> entry:t
     -> current:t
     -> summary * t

sledge/src/domain_sh.ml

@@ -22,8 +22,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 : Llair.GlobalDefn.t) with
-      | {reg; init= Some (seq, siz)} ->
-          let loc = Term.var (X.reg reg) in
+      | {name; init= Some (seq, siz)} ->
+          let loc = Term.var (X.global name) 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})
@@ -121,7 +121,8 @@ let localize_entry globals actuals formals freturn locals shadow pre entry =
   let formals_set = Var.Set.of_list formals in
   let freturn_locals = X.regs (Llair.Reg.Set.add_option freturn locals) in
   let function_summary_pre =
-    garbage_collect entry ~wrt:(Var.Set.union formals_set (X.regs globals))
+    garbage_collect entry
+      ~wrt:(Var.Set.union formals_set (X.globals globals))
   in
   [%Trace.info "function summary pre %a" pp function_summary_pre] ;
   let foot = Sh.exists formals_set function_summary_pre in
@@ -150,8 +151,8 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
       (List.pp ",@ " Llair.Exp.pp)
       (List.rev actuals)
       (List.pp ",@ " Llair.Reg.pp)
-      (List.rev formals) Llair.Reg.Set.pp locals Llair.Reg.Set.pp globals pp
-      q]
+      (List.rev formals) Llair.Reg.Set.pp locals Llair.Global.Set.pp globals
+      pp q]
   ;
   let actuals = List.map ~f:X.term actuals in
   let areturn = Option.map ~f:X.reg areturn in
@@ -248,13 +249,18 @@ let pp_summary fs {xs; foot; post} =
   Format.fprintf fs "@[<v>xs: @[%a@]@ foot: %a@ post: %a @]" Var.Set.pp xs
     pp foot pp post
 
-let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
+let create_summary ~globals ~locals ~formals ~entry ~current:(post : Sh.t) =
   [%Trace.call fun {pf} ->
-    pf "formals %a@ entry: %a@ current: %a" Llair.Reg.Set.pp formals pp
-      entry pp post]
+    pf "formals %a@ entry: %a@ current: %a"
+      (List.pp ",@ " Llair.Reg.pp)
+      formals pp entry pp post]
   ;
+  let globals = X.globals globals in
+  let formals =
+    Var.Set.of_iter (Iter.map ~f:X.reg (List.to_iter formals))
+  in
+  let formals = Var.Set.union formals globals in
   let locals = X.regs locals in
-  let formals = X.regs formals in
   let foot = Sh.exists locals entry in
   let foot, subst = Sh.freshen ~wrt:(Var.Set.union foot.us post.us) foot in
   let restore_formals q =

sledge/src/domain_sh.mli

@@ -9,11 +9,10 @@
 
 include Domain_intf.Dom
 
-(* formals should include all the parameters of the summary. That is both
-   formals and globals. *)
 val create_summary :
-     locals:Llair.Reg.Set.t
-  -> formals:Llair.Reg.Set.t
+     globals:Llair.Global.Set.t
+  -> locals:Llair.Reg.Set.t
+  -> formals:Llair.Reg.t list
   -> entry:t
   -> current:t
   -> summary * t

sledge/src/domain_unit.ml

@@ -39,5 +39,5 @@ let resolve_callee lookup ptr _ =
 type summary = unit
 
 let pp_summary fs () = Format.pp_print_string fs "()"
-let create_summary ~locals:_ ~formals:_ _ = ((), ())
+let create_summary ~globals:_ ~locals:_ ~formals:_ _ = ((), ())
 let apply_summary _ _ = Some ()

sledge/src/domain_used_globals.ml

@@ -7,28 +7,30 @@
 
 (** Used-globals abstract domain *)
 
-type t = Llair.Reg.Set.t [@@deriving equal, sexp]
+type t = Llair.Global.Set.t [@@deriving equal, sexp]
 
-let pp = Llair.Reg.Set.pp
+let pp = Llair.Global.Set.pp
 let report_fmt_thunk = Fun.flip pp
-let empty = Llair.Reg.Set.empty
+let empty = Llair.Global.Set.empty
 
 let init globals =
   [%Trace.info
     "pgm globals: {%a}" (IArray.pp ", " Llair.GlobalDefn.pp) globals] ;
   empty
 
-let join l r = Some (Llair.Reg.Set.union l r)
+let join l r = Some (Llair.Global.Set.union l r)
 let recursion_beyond_bound = `skip
 let is_false _ = false
 let post _ _ state = state
-let retn _ _ from_call post = Llair.Reg.Set.union from_call post
+let retn _ _ from_call post = Llair.Global.Set.union from_call post
 let dnf t = [t]
 
-let add_if_global v gs =
-  if Llair.Reg.is_global v then Llair.Reg.Set.add v gs else gs
+let used_globals exp s =
+  Llair.Exp.fold_exps exp s ~f:(fun e s ->
+      match Llair.Global.of_exp e with
+      | Some g -> Llair.Global.Set.add g s
+      | None -> s )
 
-let used_globals exp s = Llair.Exp.fold_regs ~f:add_if_global exp s
 let exec_assume st exp = Some (used_globals exp st)
 let exec_kill _ st = st
 
@@ -89,14 +91,14 @@ let resolve_callee lookup ptr st =
 type summary = t
 
 let pp_summary = pp
-let create_summary ~locals:_ ~formals:_ state = (state, state)
-let apply_summary st summ = Some (Llair.Reg.Set.union st summ)
+let create_summary ~globals:_ ~locals:_ ~formals:_ state = (state, state)
+let apply_summary st summ = Some (Llair.Global.Set.union st summ)
 
 (** Query *)
 
 type r =
-  | Per_function of Llair.Reg.Set.t Llair.Function.Map.t
-  | Declared of Llair.Reg.Set.t
+  | Per_function of Llair.Global.Set.t Llair.Function.Map.t
+  | Declared of Llair.Global.Set.t
 
 let by_function : r -> Llair.Function.t -> t =
  fun s fn ->
@@ -113,4 +115,4 @@ let by_function : r -> Llair.Function.t -> t =
            used-globals pre-analysis "
           Llair.Function.pp fn () ) )
   |>
-  [%Trace.retn fun {pf} r -> pf "%a" Llair.Reg.Set.pp r]
+  [%Trace.retn fun {pf} r -> pf "%a" Llair.Global.Set.pp r]

sledge/src/domain_used_globals.mli

@@ -7,11 +7,11 @@
 
 (** Used-globals abstract domain *)
 
-include Domain_intf.Dom with type summary = Llair.Reg.Set.t
+include Domain_intf.Dom with type summary = Llair.Global.Set.t
 
 type r =
-  | Per_function of Llair.Reg.Set.t Llair.Function.Map.t
+  | Per_function of Llair.Global.Set.t Llair.Function.Map.t
       (** per-function used-globals map *)
-  | Declared of Llair.Reg.Set.t  (** program-wide set *)
+  | Declared of Llair.Global.Set.t  (** program-wide set *)
 
 val by_function : r -> Llair.Function.t -> summary

sledge/src/llair/exp.ml

@@ -62,7 +62,8 @@ module T = struct
   [@@deriving compare, equal, hash, sexp]
 
   type t =
-    | Reg of {name: string; global: bool; typ: Typ.t}
+    | Reg of {name: string; typ: Typ.t}
+    | Global of {name: string; typ: Typ.t [@ignore]}
     | Function of {name: string; typ: Typ.t [@ignore]}
     | Label of {parent: string; name: string}
     | Integer of {data: Z.t; typ: Typ.t}
@@ -128,8 +129,8 @@ let rec pp fs exp =
     Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
   in
   match exp with
-  | Reg {name; global= true} -> pf "%@%s" name
-  | Reg {name; global= false} -> pf "%%%s" name
+  | Reg {name} -> pf "%%%s" name
+  | Global {name} -> pf "%@%s%a" name pp_demangled name
   | Function {name} -> pf "&%s%a" name pp_demangled name
   | Label {name} -> pf "%s" name
   | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
@@ -172,7 +173,7 @@ let valid_idx idx elts = 0 <= idx && idx < IArray.length elts
 let rec invariant exp =
   let@ () = Invariant.invariant [%here] exp [%sexp_of: t] in
   match exp with
-  | Reg {typ} -> assert (Typ.is_sized typ)
+  | Reg {typ} | Global {typ} -> assert (Typ.is_sized typ)
   | Function {typ= Pointer {elt= Function _}} -> ()
   | Function _ -> assert false
   | Integer {data; typ} -> (
@@ -251,7 +252,9 @@ let rec invariant exp =
 
 and typ_of exp =
   match exp with
-  | Reg {typ} | Function {typ} | Integer {typ} | Float {typ} -> typ
+  | Reg {typ} | Global {typ} | Function {typ} | Integer {typ} | Float {typ}
+    ->
+      typ
   | Label _ -> Typ.ptr
   | Ap1 ((Signed _ | Unsigned _ | Convert _ | Splat), dst, _) -> dst
   | Ap1 (Select idx, typ, _) -> (
@@ -296,15 +299,38 @@ module Reg = struct
 
   let name = function Reg x -> x.name | r -> violates invariant r
   let typ = function Reg x -> x.typ | r -> violates invariant r
-  let is_global = function Reg x -> x.global | r -> violates invariant r
-  let pp_demangled ppf r = pp_demangled ppf (name r)
 
   let of_exp = function
     | Reg _ as e -> Some (e |> check invariant)
     | _ -> None
 
-  let program ?global typ name =
-    Reg {name; global= Option.is_some global; typ} |> check invariant
+  let mk typ name = Reg {name; typ} |> check invariant
+end
+
+(** Globals are the expressions constructed by [Global] *)
+module Global = struct
+  include T
+
+  let pp = pp
+
+  module Set = struct
+    include Set
+
+    let pp = Set.pp pp_exp
+  end
+
+  let invariant x =
+    let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
+    match x with Global _ -> invariant x | _ -> assert false
+
+  let name = function Global x -> x.name | r -> violates invariant r
+  let typ = function Global x -> x.typ | r -> violates invariant r
+
+  let of_exp = function
+    | Global _ as e -> Some (e |> check invariant)
+    | _ -> None
+
+  let mk typ name = Global {name; typ} |> check invariant
 end
 
 (** Function names are the expressions constructed by [Function] *)
@@ -338,6 +364,7 @@ let reg x = x
 (* constants *)
 
 let function_ f = f
+let global g = g
 let label ~parent ~name = Label {parent; name} |> check invariant
 let integer typ data = Integer {data; typ} |> check invariant
 let null = integer Typ.ptr Z.zero

sledge/src/llair/exp.mli

@@ -72,7 +72,8 @@ type opN = Record  (** Record (array / struct) constant *)
 [@@deriving compare, equal, hash, sexp]
 
 type t = private
-  | Reg of {name: string; global: bool; typ: Typ.t}  (** Virtual register *)
+  | Reg of {name: string; typ: Typ.t}  (** Virtual register *)
+  | Global of {name: string; typ: Typ.t [@ignore]}  (** Global constant *)
   | Function of {name: string; typ: Typ.t [@ignore]}  (** Function name *)
   | Label of {parent: string; name: string}
       (** Address of named code block within parent function *)
@@ -104,15 +105,36 @@ module Reg : sig
   end
 
   val pp : t pp
-  val pp_demangled : t pp
 
   include Invariant.S with type t := t
 
   val of_exp : exp -> t option
-  val program : ?global:unit -> Typ.t -> string -> t
+  val mk : Typ.t -> string -> t
+  val name : t -> string
+  val typ : t -> Typ.t
+end
+
+(** Exp.Global is re-exported as Global *)
+module Global : sig
+  type exp := t
+  type t = private exp [@@deriving compare, equal, hash, sexp]
+
+  module Set : sig
+    include Set.S with type elt := t
+
+    val sexp_of_t : t -> Sexp.t
+    val t_of_sexp : Sexp.t -> t
+    val pp : t pp
+  end
+
+  val pp : t pp
+
+  include Invariant.S with type t := t
+
+  val of_exp : exp -> t option
+  val mk : Typ.t -> string -> t
   val name : t -> string
   val typ : t -> Typ.t
-  val is_global : t -> bool
 end
 
 (** Exp.Function is re-exported as Function *)
@@ -140,6 +162,7 @@ val reg : Reg.t -> t
 
 (* constants *)
 val function_ : Function.t -> t
+val global : Global.t -> t
 val label : parent:string -> name:string -> t
 val null : t
 val bool : bool -> t
@@ -199,6 +222,7 @@ val update : Typ.t -> rcd:t -> int -> elt:t -> t
 
 (** Traverse *)
 
+val fold_exps : t -> 's -> f:(t -> 's -> 's) -> 's
 val fold_regs : t -> 's -> f:(Reg.t -> 's -> 's) -> 's
 
 (** Query *)

sledge/src/llair/global.ml

@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Globals *)
+
+include Exp.Global

sledge/src/llair/global.mli

@@ -0,0 +1,12 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Globals *)
+
+include module type of struct
+  include Exp.Global
+end

sledge/src/llair/globalDefn.ml

@@ -7,26 +7,18 @@
 
 (** Global variables *)
 
-type t = {reg: Reg.t; init: (Exp.t * int) option; loc: Loc.t}
+type t = {name: Global.t; init: (Exp.t * int) option; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
-let pp fs {reg} =
-  let name = Reg.name reg in
-  let pf pp =
-    Format.pp_open_box fs 2 ;
-    Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs pp
-  in
-  pf "@%s%a" name Reg.pp_demangled reg
-
-let pp_defn fs {reg; init; loc} =
-  Format.fprintf fs "@[<2>%a %a%a %a@]" Typ.pp (Reg.typ reg) Reg.pp reg
+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
 
 let invariant g =
   let@ () = Invariant.invariant [%here] g [%sexp_of: t] in
-  let {reg} = g in
-  assert (Typ.is_sized (Reg.typ reg)) ;
-  assert (Reg.is_global reg)
+  let {name} = g in
+  assert (Typ.is_sized (Global.typ name))
 
-let mk ?init reg loc = {reg; init; loc} |> check invariant
+let mk ?init name loc = {name; init; loc} |> check invariant

sledge/src/llair/globalDefn.mli

@@ -7,12 +7,11 @@
 
 (** Global variables *)
 
-type t = private {reg: Reg.t; init: (Exp.t * int) option; loc: Loc.t}
+type t = private {name: Global.t; init: (Exp.t * int) option; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
 val pp : t pp
-val pp_defn : t pp
 
 include Invariant.S with type t := t
 
-val mk : ?init:Exp.t * int -> Reg.t -> Loc.t -> t
+val mk : ?init:Exp.t * int -> Global.t -> Loc.t -> t

sledge/src/llair/llair.ml

@@ -14,6 +14,7 @@ module Typ = Typ
 module Reg = Reg
 module Exp = Exp
 module Function = Function
+module Global = Global
 module GlobalDefn = GlobalDefn
 
 type inst =
@@ -228,7 +229,7 @@ and dummy_func =
         "dummy"
   ; formals= []
   ; freturn= None
-  ; fthrow= Reg.program Typ.ptr "dummy"
+  ; fthrow= Reg.mk Typ.ptr "dummy"
   ; locals= Reg.Set.empty
   ; entry= dummy_block
   ; loc= Loc.none }
@@ -601,7 +602,7 @@ module Program = struct
     assert (
       not
         (Iter.contains_dup (IArray.to_iter pgm.globals) ~cmp:(fun g1 g2 ->
-             Reg.compare g1.GlobalDefn.reg g2.GlobalDefn.reg )) )
+             Global.compare g1.name g2.name )) )
 
   let mk ~globals ~functions =
     { globals= IArray.of_list_rev globals
@@ -610,7 +611,7 @@ module Program = struct
 
   let pp fs {globals; functions} =
     Format.fprintf fs "@[<v>@[%a@]@ @ @ @[%a@]@]"
-      (IArray.pp "@\n@\n" GlobalDefn.pp_defn)
+      (IArray.pp "@\n@\n" GlobalDefn.pp)
       globals
       (List.pp "@\n@\n" Func.pp)
       ( Function.Map.values functions

sledge/src/llair/llair.mli

@@ -13,6 +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. *)

sledge/src/llair_to_Fol.ml

@@ -13,10 +13,16 @@ let func f =
   let name = Llair.Function.name f in
   Var.program ~name ~global:true
 
+let global g =
+  let name = Llair.Global.name g in
+  Var.program ~name ~global:true
+
+let globals gs =
+  Var.Set.of_iter (Iter.map ~f:global (Llair.Global.Set.to_iter gs))
+
 let reg r =
   let name = Llair.Reg.name r in
-  let global = Llair.Reg.is_global r in
-  Var.program ~name ~global
+  Var.program ~name ~global:false
 
 let regs rs = Var.Set.of_iter (Iter.map ~f:reg (Llair.Reg.Set.to_iter rs))
 let uap0 f = T.apply f [||]
@@ -67,7 +73,8 @@ and term : Llair.Exp.t -> T.t =
       F.inject
         (F.cond ~cnd:(formula cnd) ~pos:(formula pos) ~neg:(formula neg))
   (* terms *)
-  | Reg {name; global; typ= _} -> T.var (Var.program ~name ~global)
+  | Reg {name; typ= _} -> T.var (Var.program ~name ~global:false)
+  | Global {name; typ= _} -> T.var (Var.program ~name ~global:true)
   | Function {name; typ= _} -> T.var (Var.program ~name ~global:true)
   | Label {parent; name} ->
       uap0 (Funsym.uninterp ("label_" ^ parent ^ "_" ^ name))

sledge/src/llair_to_Fol.mli

@@ -8,6 +8,8 @@
 open Fol
 
 val func : Llair.Function.t -> Var.t
+val global : Llair.Global.t -> Var.t
+val globals : Llair.Global.Set.t -> Var.Set.t
 val reg : Llair.Reg.t -> Var.t
 val regs : Llair.Reg.Set.t -> Var.Set.t
 val term : Llair.Exp.t -> Term.t