From 4c6ad4a2e2c28be3babb64b4d52180df45c304d1 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 10 Jun 2020 07:04:39 -0700
Subject: [PATCH] [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  | 5 +++--
 sledge/src/exp.mli | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/sledge/src/exp.ml b/sledge/src/exp.ml
index 6c8d42273..f714b6f47 100644
--- a/sledge/src/exp.ml
+++ b/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
 
diff --git a/sledge/src/exp.mli b/sledge/src/exp.mli
index e29477791..5a1d8fe45 100644
--- a/sledge/src/exp.mli
+++ b/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] *)