[sledge] Move check for whether a variable is global from Reg to Var

Summary:
Extend the encoding using `id` from 0 indicating a program variable to
also -1 indicating a global program variable.

Reviewed By: bennostein

Differential Revision: D17665229

fbshipit-source-id: 848b8a31e

sledge/src/domain/used_globals.ml

@@ -23,7 +23,7 @@ let is_false _ = false
 let post _ _ state = state
 let retn _ _ from_call post = Set.union from_call post
 let dnf t = [t]
-let add_if_global gs v = if Reg.global v then Set.add gs v else gs
+let add_if_global gs v = if Var.global (Reg.var v) then Set.add gs v else gs
 
 let used_globals ?(init = empty) exp =
   Exp.fold_regs exp ~init ~f:add_if_global

sledge/src/llair/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; global: bool}
+      | Reg of {name: string; typ: Typ.t}
       | Nondet of {msg: string; typ: Typ.t}
       | Label of {parent: string; name: string}
       | Integer of {data: Z.t; typ: Typ.t}
@@ -139,8 +139,10 @@ let rec pp fs exp =
       Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
     in
     match exp.desc with
-    | Reg {name; global= true} -> pf "%@%s" name
-    | Reg {name; global= false} -> pf "%%%s" name
+    | Reg {name} -> (
+      match Var.of_term exp.term with
+      | Some v when Var.global v -> pf "%@%s" name
+      | _ -> pf "%%%s" name )
     | Nondet {msg} -> pf "nondet \"%s\"" msg
     | Label {name} -> pf "%s" name
     | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
@@ -359,15 +361,11 @@ module Reg = struct
   let name r =
     match r.desc with Reg x -> x.name | _ -> violates invariant r
 
-  let global r =
-    match r.desc with Reg x -> x.global | _ -> violates invariant r
-
   let of_exp e =
     match e.desc with Reg _ -> Some (e |> check invariant) | _ -> None
 
   let program ?global typ name =
-    { desc= Reg {name; typ; global= Option.is_some global}
-    ; term= Term.var (Var.program name) }
+    {desc= Reg {name; typ}; term= Term.var (Var.program ?global name)}
     |> check invariant
 end
 

sledge/src/llair/exp.mli

@@ -64,7 +64,7 @@ type opN =
 type t = private {desc: desc; term: Term.t}
 
 and desc = private
-  | Reg of {name: string; typ: Typ.t; global: bool}  (** Virtual register *)
+  | Reg of {name: string; 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] *)
@@ -120,7 +120,6 @@ module Reg : sig
   val program : ?global:unit -> Typ.t -> string -> t
   val var : t -> Var.t
   val name : t -> string
-  val global : t -> bool
 end
 
 (** Construct *)

sledge/src/llair/global.ml

@@ -28,6 +28,6 @@ let invariant g =
   @@ fun () ->
   let {reg; typ} = g in
   assert (Typ.is_sized typ) ;
-  assert (Reg.global reg)
+  assert (Var.global (Reg.var reg))
 
 let mk ?init reg typ loc = {reg; init; typ; loc} |> check invariant

sledge/src/llair/term.ml

@@ -209,6 +209,8 @@ let rec pp ?is_x fs term =
       Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
     in
     match term with
+    | Var {name; id= -1} as var ->
+        Trace.pp_styled (get_var_style var) "%@%s" fs name
     | Var {name; id= 0} as var ->
         Trace.pp_styled (get_var_style var) "%%%s" fs name
     | Var {name; id} as var ->
@@ -392,12 +394,14 @@ module Var = struct
 
   let id = function Var v -> v.id | x -> violates invariant x
   let name = function Var v -> v.name | x -> violates invariant x
+  let global = function Var v -> v.id = -1 | x -> violates invariant x
 
   let of_term = function
     | Var _ as v -> Some (v |> check invariant)
     | _ -> None
 
-  let program name = Var {name; id= 0}
+  let program ?global name =
+    Var {name; id= (if Option.is_some global then -1 else 0)}
 
   let fresh name ~(wrt : Set.t) =
     let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in

sledge/src/llair/term.mli

@@ -109,9 +109,10 @@ module Var : sig
   include Invariant.S with type t := t
 
   val of_term : term -> t option
-  val program : string -> t
+  val program : ?global:unit -> string -> t
   val fresh : string -> wrt:Set.t -> t * Set.t
   val name : t -> string
+  val global : t -> bool
 
   module Subst : sig
     type t [@@deriving compare, equal, sexp]