[sledge] Refactor: Add global flag to Reg representation

Summary:
The term representing an exp should not rely on more info than is
carried by the exp.

Reviewed By: jvillard

Differential Revision: D21720989

fbshipit-source-id: b65bf3678

sledge/src/exp.ml

@@ -64,7 +64,7 @@ module T = struct
   type t = {desc: desc; term: Term.t}
 
   and desc =
-    | Reg of {name: string; typ: Typ.t}
+    | Reg of {name: string; global: bool; typ: Typ.t}
     | Nondet of {msg: string; typ: Typ.t}
     | Label of {parent: string; name: string}
     | Integer of {data: Z.t; typ: Typ.t}
@@ -325,7 +325,8 @@ module Reg = struct
     match e.desc with Reg _ -> Some (e |> check invariant) | _ -> None
 
   let program ?global typ name =
-    {desc= Reg {name; typ}; term= Term.var (Var.program ?global name)}
+    { desc= Reg {name; global= Option.is_some global; typ}
+    ; term= Term.var (Var.program ?global name) }
     |> check invariant
 end
 

sledge/src/exp.mli

@@ -74,7 +74,7 @@ type opN = Record  (** Record (array / struct) constant *)
 type t = private {desc: desc; term: Term.t}
 
 and desc = private
-  | Reg of {name: string; typ: Typ.t}  (** Virtual register *)
+  | Reg of {name: string; global: bool; typ: Typ.t}  (** Virtual register *)
   | Nondet of {msg: string; typ: Typ.t}
       (** Anonymous register with arbitrary value, representing
           non-deterministic approximation of value described by [msg] *)