Existential quantifiers as symbolic values

soteria/lib/bv_values/encoding.ml

@@ -87,8 +87,9 @@ let smt_of_binop : Svalue.Binop.t -> sexp -> sexp -> sexp = function
   | BvConcat -> bv_concat
 
 let rec encode_value (v : Svalue.t) =
+  let var v = atom (Svalue.Var.to_string v) in
   match v.node.kind with
-  | Var v -> atom (Svalue.Var.to_string v)
+  | Var v -> var v
   | Float f -> (
       match Svalue.precision_of_f v.node.ty with
       | F16 -> f16_k @@ Float.of_string f
@@ -107,6 +108,10 @@ let rec encode_value (v : Svalue.t) =
           List.map (fun v -> seq_singl (encode_value_memo v)) vs |> seq_concat)
   | Ite (c, t, e) ->
       ite (encode_value_memo c) (encode_value_memo t) (encode_value_memo e)
+  | Exists (vs, sv) ->
+      let exists l x = list [ atom "exists"; list l; x ] in
+      let encode_var_memo (v, ty) = list [ var v; sort_of_ty ty ] in
+      exists (List.map encode_var_memo vs) (encode_value_memo sv)
   | Unop (unop, v1) ->
       let v1 = encode_value_memo v1 in
       smt_of_unop unop v1

soteria/lib/bv_values/eval.ml

@@ -48,6 +48,14 @@ let eval_unop : Unop.t -> t -> t = function
   | FRound rm -> Float.round rm
 
 let rec eval ~eval_var (x : t) : t =
+  let eval_without_vars vs =
+    let eval_var v ty =
+      match List.find_opt (fun (v', _) -> Var.equal v v') vs with
+      | Some (v, ty) -> mk_var v ty
+      | None -> eval_var v ty
+    in
+    eval ~eval_var
+  in
   let eval = eval ~eval_var in
   match x.node.kind with
   | Var v -> eval_var v x.node.ty
@@ -75,6 +83,9 @@ let rec eval ~eval_var (x : t) : t =
       if equal guard Bool.v_true then eval then_
       else if equal guard Bool.v_false then eval else_
       else Bool.ite guard (eval then_) (eval else_)
+  | Exists (vs, sv) ->
+      let sv = eval_without_vars vs sv in
+      Bool.exists vs sv
   | Seq l ->
       let l, changed = List.map_changed eval l in
       if Stdlib.not changed then x else Svalue.SSeq.mk ~seq_ty:x.node.ty l

soteria/lib/bv_values/svalue.ml

@@ -196,6 +196,7 @@ type t_kind =
   | Binop of Binop.t * t * t
   | Nop of Nop.t * t list
   | Ite of t * t * t
+  | Exists of (Var.t * ty) list * t
 
 and t_node = { kind : t_kind; ty : ty }
 and t = t_node hash_consed [@@deriving show { with_path = false }, eq, ord]
@@ -217,6 +218,15 @@ let iter =
         aux f c;
         aux f t;
         aux f e
+    | Exists (vs, sv) ->
+        let f sv =
+          match sv.node.kind with
+          | Var v ->
+              if List.exists (fun (v', _) -> Var.equal v v') vs then ()
+              else f sv
+          | _ -> f sv
+        in
+        aux f sv
   in
   Fun.flip aux
 
@@ -240,6 +250,9 @@ let rec pp ft t =
   | Ptr (l, o) -> pf ft "&(%a, %a)" pp l pp o
   | Seq l -> pf ft "%a" (brackets (list ~sep:comma pp)) l
   | Ite (c, t, e) -> pf ft "(%a ? %a : %a)" pp c pp t pp e
+  | Exists (vs, v) ->
+      let var_pp ft (v, ty) = pf ft "V%a:%a" Var.pp v pp_ty ty in
+      pf ft "∃ %a. %a" (list ~sep:comma var_pp) vs pp v
   | Unop (Not, { node = { kind = Binop (Eq, v1, v2); _ }; _ }) ->
       pf ft "(%a != %a)" pp v1 pp v2
   | Unop (op, v) -> pf ft "%a(%a)" Unop.pp op pp v
@@ -292,6 +305,7 @@ module Hcons = Hc.Make (struct
     | Binop (op, l, r) -> Hashtbl.hash (op, l.tag, r.tag, hty)
     | Nop (op, l) -> Hashtbl.hash (op, List.map (fun sv -> sv.tag) l, hty)
     | Ite (c, t, e) -> Hashtbl.hash (c.tag, t.tag, e.tag, hty)
+    | Exists (vs, sv) -> Hashtbl.hash (vs, sv.tag, hty)
 end)
 
 let ( <| ) kind ty : t = Hcons.hashcons { kind; ty }
@@ -346,6 +360,14 @@ let rec subst subst_var sv =
       let e' = subst subst_var e in
       if equal c c' && equal t t' && equal e e' then sv
       else Ite (c', t', e') <| sv.node.ty
+  | Exists (vs, v) ->
+      let subst_var v =
+        match List.find_opt (fun (v', _) -> Var.equal v v') vs with
+        | Some (v, _) -> v
+        | None -> subst_var v
+      in
+      let v' = subst subst_var v in
+      if equal v v' then sv else Exists (vs, v') <| sv.node.ty
 
 (** {2 Operator declarations} *)
 
@@ -361,6 +383,7 @@ module type Bool = sig
   val split_ands : t -> t Iter.t
   val distinct : t list -> t
   val ite : t -> t -> t -> t
+  val exists : (Var.t * ty) list -> t -> t
   val sem_eq : t -> t -> t
   val sem_eq_untyped : t -> t -> t
 end
@@ -538,6 +561,8 @@ module rec Bool : Bool = struct
     | _ when equal if_ else_ -> if_
     | _ -> Ite (guard, if_, else_) <| if_.node.ty
 
+  let exists vs body = Exists (vs, body) <| TBool
+
   let rec sem_eq v1 v2 =
     match (v1.node.kind, v2.node.kind) with
     | _ when equal v1 v2 -> v_true

soteria/tests/symex/dune

@@ -1,9 +1,9 @@
 (executables
- (names run_twice deep_give_up if_sure)
+ (names run_twice deep_give_up if_sure exists)
  (libraries soteria soteria_c_lib)
  (flags :standard -open Soteria.C_values)
  (preprocess
   (pps soteria.ppx)))
 
 (cram
- (deps ./run_twice.exe ./deep_give_up.exe ./if_sure.exe))
+ (deps ./run_twice.exe ./deep_give_up.exe ./if_sure.exe ./exists.exe))

soteria/tests/symex/exists.ml

@@ -0,0 +1,14 @@
+open Soteria.Bv_values
+open Soteria.Symex.Make (Soteria.Symex.Meta.Dummy) (Bv_solver.Z3_solver)
+open Syntax
+
+let test =
+  let v = Svalue.Var.of_int 42 in
+  let ty = Svalue.t_bool in
+  let sv = Svalue.mk_var v ty in
+  let exists = Svalue.Bool.exists [ (v, ty) ] sv in
+  if%sat Typed.type_ exists then return 42 else return (-1)
+
+let () =
+  let pp = Fmt.(Dump.list int) in
+  Fmt.pr "exists: %a@\n" pp (List.map fst @@ run ~mode:OX test)

soteria/tests/symex/symex.t

@@ -31,3 +31,6 @@ This test is considered successful if the out of each process is a single branch
   if_false: [42]
   if_maybe: [42]
   if_guranteed: [42]
+
+  $ ./exists.exe
+  exists: [42]