From fc2695ce88330b2ec389ce3683b66a25079879dd Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 12 Nov 2020 16:38:03 -0800
Subject: [PATCH] [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           |  6 ++--
 sledge/cli/frontend.ml             | 24 ++++++++--------
 sledge/cli/sledge_cli.ml           |  8 +++---
 sledge/src/control.ml              |  4 +--
 sledge/src/domain_intf.ml          |  8 ++++--
 sledge/src/domain_relation.ml      | 13 +++++----
 sledge/src/domain_relation.mli     |  5 ++--
 sledge/src/domain_sh.ml            | 24 ++++++++++------
 sledge/src/domain_sh.mli           |  7 ++---
 sledge/src/domain_unit.ml          |  2 +-
 sledge/src/domain_used_globals.ml  | 28 ++++++++++---------
 sledge/src/domain_used_globals.mli |  6 ++--
 sledge/src/llair/exp.ml            | 45 ++++++++++++++++++++++++------
 sledge/src/llair/exp.mli           | 32 ++++++++++++++++++---
 sledge/src/llair/global.ml         | 10 +++++++
 sledge/src/llair/global.mli        | 12 ++++++++
 sledge/src/llair/globalDefn.ml     | 22 +++++----------
 sledge/src/llair/globalDefn.mli    |  5 ++--
 sledge/src/llair/llair.ml          |  7 +++--
 sledge/src/llair/llair.mli         |  1 +
 sledge/src/llair_to_Fol.ml         | 13 +++++++--
 sledge/src/llair_to_Fol.mli        |  2 ++
 22 files changed, 185 insertions(+), 99 deletions(-)
 create mode 100644 sledge/src/llair/global.ml
 create mode 100644 sledge/src/llair/global.mli

diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index f3ebcfb78..e13e0a591 100644
--- a/sledge/cli/domain_itv.ml
+++ b/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)
diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml
index 1c500160a..c8a7c1521 100644
--- a/sledge/cli/frontend.ml
+++ b/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
diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml
index 5aeb3a79f..ad2fc4345 100644
--- a/sledge/cli/sledge_cli.ml
+++ b/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 =
diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 2de05504e..6adaa14ca 100644
--- a/sledge/src/control.ml
+++ b/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 ;
diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml
index e18605ddc..0e24692f7 100644
--- a/sledge/src/domain_intf.ml
+++ b/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
diff --git a/sledge/src/domain_relation.ml b/sledge/src/domain_relation.ml
index 7caad0b76..c28bcbf72 100644
--- a/sledge/src/domain_relation.ml
+++ b/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))
 
diff --git a/sledge/src/domain_relation.mli b/sledge/src/domain_relation.mli
index 957abc1ae..0f1af3326 100644
--- a/sledge/src/domain_relation.mli
+++ b/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
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 4ff5c8c29..60fed440c 100644
--- a/sledge/src/domain_sh.ml
+++ b/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 =
diff --git a/sledge/src/domain_sh.mli b/sledge/src/domain_sh.mli
index e832aa8e7..70249f754 100644
--- a/sledge/src/domain_sh.mli
+++ b/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
diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml
index 5d0ffb849..c8f6aeacd 100644
--- a/sledge/src/domain_unit.ml
+++ b/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 ()
diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml
index 4267087c9..58accca28 100644
--- a/sledge/src/domain_used_globals.ml
+++ b/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]
diff --git a/sledge/src/domain_used_globals.mli b/sledge/src/domain_used_globals.mli
index 2fe681252..c1a93a02e 100644
--- a/sledge/src/domain_used_globals.mli
+++ b/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
diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 896a65c9f..19695863b 100644
--- a/sledge/src/llair/exp.ml
+++ b/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
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 1f0b7a32c..d94b04b52 100644
--- a/sledge/src/llair/exp.mli
+++ b/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 *)
diff --git a/sledge/src/llair/global.ml b/sledge/src/llair/global.ml
new file mode 100644
index 000000000..185b20767
--- /dev/null
+++ b/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
diff --git a/sledge/src/llair/global.mli b/sledge/src/llair/global.mli
new file mode 100644
index 000000000..74f2f0418
--- /dev/null
+++ b/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
diff --git a/sledge/src/llair/globalDefn.ml b/sledge/src/llair/globalDefn.ml
index ca98b674e..f10b8539c 100644
--- a/sledge/src/llair/globalDefn.ml
+++ b/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
diff --git a/sledge/src/llair/globalDefn.mli b/sledge/src/llair/globalDefn.mli
index d6550daf0..5eaa1e489 100644
--- a/sledge/src/llair/globalDefn.mli
+++ b/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
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index 6d3bacc5a..f7a4a3516 100644
--- a/sledge/src/llair/llair.ml
+++ b/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
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index f4679c3e8..d65cadf11 100644
--- a/sledge/src/llair/llair.mli
+++ b/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. *)
diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
index a7de81324..cb80fcf8a 100644
--- a/sledge/src/llair_to_Fol.ml
+++ b/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))
diff --git a/sledge/src/llair_to_Fol.mli b/sledge/src/llair_to_Fol.mli
index 8ca00887c..ac1c3de82 100644
--- a/sledge/src/llair_to_Fol.mli
+++ b/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