From cfc25ab82521509144f0ef8532cb3c8f8444312d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 10 Jun 2020 07:05:35 -0700 Subject: [PATCH] [sledge] Refactor: Remove Nondet Llair.Exp and Term Summary: Now that the frontend translates LLVM's undef to nondet instructions, not expressions, Nondet in Exp and Term are not needed. Reviewed By: jvillard Differential Revision: D21720969 fbshipit-source-id: e8acaf432 --- sledge/src/equality.ml | 9 ++++----- sledge/src/llair/exp.ml | 8 +++----- sledge/src/llair/exp.mli | 5 +---- sledge/src/term.ml | 37 ++++++++++--------------------------- sledge/src/term.mli | 4 ---- 5 files changed, 18 insertions(+), 45 deletions(-) diff --git a/sledge/src/equality.ml b/sledge/src/equality.ml index d23562d58..aeb1a95e5 100644 --- a/sledge/src/equality.ml +++ b/sledge/src/equality.ml @@ -17,8 +17,7 @@ let classify e = | Add _ | Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) -> Interpreted | Mul _ | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ | And _ | Or _ -> Uninterpreted - | Var _ | Integer _ | Rational _ | Float _ | Nondet _ | Label _ - |RecRecord _ -> + | Var _ | Integer _ | Rational _ | Float _ | Label _ | RecRecord _ -> Atomic let interpreted e = equal_kind (classify e) Interpreted @@ -101,7 +100,7 @@ end = struct (** compose a substitution with a mapping *) let compose1 ~key ~data s = match (key : Term.t) with - | Integer _ | Rational _ | Float _ | Nondet _ | Label _ -> s + | Integer _ | Rational _ | Float _ | Label _ -> s | _ -> if Term.equal key data then s else compose s (Term.Map.singleton key data) @@ -134,7 +133,7 @@ end = struct else let s = Term.Map.remove s key in match (key : Term.t) with - | Integer _ | Rational _ | Float _ | Nondet _ | Label _ -> s + | Integer _ | Rational _ | Float _ | Label _ -> s | _ -> Term.Map.add_exn ~key:key' ~data:data' s ) (** Holds only if [true ⊢ ∃xs. e=f]. Clients assume @@ -475,7 +474,7 @@ let rec canon r a = let rec extend_ a r = match (a : Term.t) with - | Integer _ | Rational _ | Float _ | Nondet _ | Label _ -> r + | Integer _ | Rational _ | Float _ | Label _ -> r | _ -> ( if interpreted a then Term.fold ~f:extend_ a ~init:r else diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index a52525623..99ea77cd7 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -63,7 +63,6 @@ module T = struct type 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} | Float of {data: string; typ: Typ.t} @@ -117,7 +116,6 @@ let rec pp fs exp = match exp with | Reg {name; global= true} -> pf "%@%s" name | Reg {name; global= false} -> 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" | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data @@ -166,7 +164,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} | Nondet {typ} -> assert (Typ.is_sized typ) + | Reg {typ} -> assert (Typ.is_sized typ) | Integer {data; typ} -> ( match typ with | Integer {bits} -> @@ -244,7 +242,7 @@ let rec invariant exp = and typ_of exp = match exp with - | Reg {typ} | Nondet {typ} | Integer {typ} | Float {typ} -> typ + | Reg {typ} | Integer {typ} | Float {typ} -> typ | Label _ -> Typ.ptr | Ap1 ((Signed _ | Unsigned _ | Convert _ | Splat), dst, _) -> dst | Ap1 (Select idx, typ, _) -> ( @@ -304,6 +302,7 @@ 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 of_ = function Reg _ as r -> r | _ -> invalid_arg "Reg.of_" let of_exp = function | Reg _ as e -> Some (e |> check invariant) @@ -321,7 +320,6 @@ let reg x = x (* constants *) -let nondet typ msg = Nondet {msg; typ} |> check invariant 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 9ea6771b4..b203191bc 100644 --- a/sledge/src/llair/exp.mli +++ b/sledge/src/llair/exp.mli @@ -73,9 +73,6 @@ type opN = Record (** Record (array / struct) constant *) type t = private | 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] *) | Label of {parent: string; name: string} (** Address of named code block within parent function *) | Integer of {data: Z.t; typ: Typ.t} (** Integer constant *) @@ -112,6 +109,7 @@ module Reg : sig include Invariant.S with type t := t + val of_ : exp -> t val of_exp : exp -> t option val program : ?global:unit -> Typ.t -> string -> t val name : t -> string @@ -125,7 +123,6 @@ end val reg : Reg.t -> t (* constants *) -val nondet : Typ.t -> string -> t val label : parent:string -> name:string -> t val null : t val bool : bool -> t diff --git a/sledge/src/term.ml b/sledge/src/term.ml index c7547f843..b9b04c016 100644 --- a/sledge/src/term.ml +++ b/sledge/src/term.ml @@ -81,7 +81,6 @@ and T : sig | Add of qset | Mul of qset | Label of {parent: string; name: string} - | Nondet of {msg: string} | Float of {data: string} | Integer of {data: Z.t} | Rational of {data: Q.t} @@ -102,7 +101,6 @@ end = struct | Add of qset | Mul of qset | Label of {parent: string; name: string} - | Nondet of {msg: string} | Float of {data: string} | Integer of {data: Z.t} | Rational of {data: Q.t} @@ -150,7 +148,6 @@ let rec ppx strength fs term = | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data | Rational {data} -> Trace.pp_styled `Magenta "%a" fs Q.pp data | Float {data} -> pf "%s" data - | Nondet {msg} -> pf "nondet \"%s\"" msg | Label {name} -> pf "%s" name | Ap1 (Signed {bits}, arg) -> pf "((s%i)@ %a)" bits pp arg | Ap1 (Unsigned {bits}, arg) -> pf "((u%i)@ %a)" bits pp arg @@ -344,7 +341,6 @@ let bool b = integer (Z.of_bool b) let true_ = bool true let false_ = bool false let float data = Float {data} |> check invariant -let nondet msg = Nondet {msg} |> check invariant let label ~parent ~name = Label {parent; name} |> check invariant (* type conversions *) @@ -990,7 +986,6 @@ and ubinary mk typ x y = and of_exp e = match (e : Llair.Exp.t) with | Reg {name; global; typ= _} -> Var {name; id= (if global then -1 else 0)} - | Nondet {msg; typ= _} -> nondet msg | Label {parent; name} -> label ~parent ~name | Integer {data; typ= _} -> integer data | Float {data; typ= _} -> float data @@ -1184,9 +1179,7 @@ let map e ~f = | Ap2 (op, x, y) -> map2 op ~f x y | Ap3 (op, x, y, z) -> map3 op ~f x y z | ApN (op, xs) -> mapN op ~f xs - | Var _ | Label _ | Nondet _ | Float _ | Integer _ | Rational _ - |RecRecord _ -> - e + | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> e let fold_map e ~init ~f = let s = ref init in @@ -1226,9 +1219,7 @@ let iter e ~f = | ApN (_, xs) -> IArray.iter ~f xs | And args | Or args -> Set.iter ~f args | Add args | Mul args -> Qset.iter ~f:(fun arg _ -> f arg) args - | Var _ | Label _ | Nondet _ | Float _ | Integer _ | Rational _ - |RecRecord _ -> - () + | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> () let exists e ~f = match e with @@ -1238,8 +1229,7 @@ let exists e ~f = | ApN (_, xs) -> IArray.exists ~f xs | And args | Or args -> Set.exists ~f args | Add args | Mul args -> Qset.exists ~f:(fun arg _ -> f arg) args - | Var _ | Label _ | Nondet _ | Float _ | Integer _ | Rational _ - |RecRecord _ -> + | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> false let for_all e ~f = @@ -1250,9 +1240,7 @@ let for_all e ~f = | ApN (_, xs) -> IArray.for_all ~f xs | And args | Or args -> Set.for_all ~f args | Add args | Mul args -> Qset.for_all ~f:(fun arg _ -> f arg) args - | Var _ | Label _ | Nondet _ | Float _ | Integer _ | Rational _ - |RecRecord _ -> - true + | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> true let fold e ~init:s ~f = match e with @@ -1262,9 +1250,7 @@ let fold e ~init:s ~f = | ApN (_, xs) -> IArray.fold ~f:(fun s x -> f x s) xs ~init:s | And args | Or args -> Set.fold ~f:(fun s e -> f e s) args ~init:s | Add args | Mul args -> Qset.fold ~f:(fun e _ s -> f e s) args ~init:s - | Var _ | Label _ | Nondet _ | Float _ | Integer _ | Rational _ - |RecRecord _ -> - s + | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> s let rec iter_terms e ~f = ( match e with @@ -1280,9 +1266,8 @@ let rec iter_terms e ~f = | And args | Or args -> Set.iter args ~f:(iter_terms ~f) | Add args | Mul args -> Qset.iter args ~f:(fun arg _ -> iter_terms ~f arg) - | Var _ | Label _ | Nondet _ | Float _ | Integer _ | Rational _ - |RecRecord _ -> - () ) ; + | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> () + ) ; f e let rec fold_terms e ~init:s ~f = @@ -1297,9 +1282,7 @@ let rec fold_terms e ~init:s ~f = Set.fold args ~init:s ~f:(fun s x -> fold_terms f x s) | Add args | Mul args -> Qset.fold args ~init:s ~f:(fun arg _ s -> fold_terms f arg s) - | Var _ | Label _ | Nondet _ | Float _ | Integer _ | Rational _ - |RecRecord _ -> - s + | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> s in f s e @@ -1323,7 +1306,7 @@ let is_false = function Integer {data} -> Z.is_false data | _ -> false let rec is_constant = function | Var _ -> false - | Label _ | Nondet _ | Float _ | Integer _ | Rational _ -> true + | Label _ | Float _ | Integer _ | Rational _ -> true | a -> for_all ~f:is_constant a let rec height = function @@ -1336,7 +1319,7 @@ let rec height = function 1 + Set.fold bs ~init:0 ~f:(fun m a -> max m (height a)) | Add qs | Mul qs -> 1 + Qset.fold qs ~init:0 ~f:(fun a _ m -> max m (height a)) - | Label _ | Nondet _ | Float _ | Integer _ | Rational _ | RecRecord _ -> 0 + | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> 0 (** Solve *) diff --git a/sledge/src/term.mli b/sledge/src/term.mli index 5e78b963c..e5a1f6602 100644 --- a/sledge/src/term.mli +++ b/sledge/src/term.mli @@ -89,9 +89,6 @@ and T : sig | Mul of qset (** Product of terms with rational exponents *) | Label of {parent: string; name: string} (** Address of named code block within parent function *) - | Nondet of {msg: string} - (** Anonymous local variable with arbitrary value, representing - non-deterministic approximation of value described by [msg] *) | Float of {data: string} (** Floating-point constant *) | Integer of {data: Z.t} (** Integer constant *) | Rational of {data: Q.t} (** Rational constant *) @@ -173,7 +170,6 @@ val invariant : t -> unit val var : Var.t -> t (* constants *) -val nondet : string -> t val label : parent:string -> name:string -> t val null : t val bool : bool -> t