[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

@@ -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

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

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

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 *)
 

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