From 37d1904bd3d0cf2e3b9790c87d499001deeee04e Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 9 Oct 2019 08:36:53 -0700 Subject: [PATCH] [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 | 2 +- sledge/src/llair/exp.ml | 14 ++++++-------- sledge/src/llair/exp.mli | 3 +-- sledge/src/llair/global.ml | 2 +- sledge/src/llair/term.ml | 6 +++++- sledge/src/llair/term.mli | 3 ++- 6 files changed, 16 insertions(+), 14 deletions(-) diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml index 99e2f9e47..f2af11554 100644 --- a/sledge/src/domain/used_globals.ml +++ b/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 diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index e3d228d68..2af9baf6c 100644 --- a/sledge/src/llair/exp.ml +++ b/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 diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index 99c35ba29..3c93ce484 100644 --- a/sledge/src/llair/exp.mli +++ b/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 *) diff --git a/sledge/src/llair/global.ml b/sledge/src/llair/global.ml index 634a847c7..fcbd41c52 100644 --- a/sledge/src/llair/global.ml +++ b/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 diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index 1d25009c1..cdd339519 100644 --- a/sledge/src/llair/term.ml +++ b/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 diff --git a/sledge/src/llair/term.mli b/sledge/src/llair/term.mli index f91714cd0..e25e2b777 100644 --- a/sledge/src/llair/term.mli +++ b/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]