diff --git a/soteria/lib/bv_values/encoding.ml b/soteria/lib/bv_values/encoding.ml index e8c9b44a5..24326d300 100644 --- a/soteria/lib/bv_values/encoding.ml +++ b/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 diff --git a/soteria/lib/bv_values/eval.ml b/soteria/lib/bv_values/eval.ml index dd98547ba..88e29d624 100644 --- a/soteria/lib/bv_values/eval.ml +++ b/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 diff --git a/soteria/lib/bv_values/svalue.ml b/soteria/lib/bv_values/svalue.ml index 46d77d3da..63c827213 100644 --- a/soteria/lib/bv_values/svalue.ml +++ b/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 diff --git a/soteria/tests/symex/dune b/soteria/tests/symex/dune index 34ee741fc..32bbd8207 100644 --- a/soteria/tests/symex/dune +++ b/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)) diff --git a/soteria/tests/symex/exists.ml b/soteria/tests/symex/exists.ml new file mode 100644 index 000000000..ff6c5965e --- /dev/null +++ b/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) diff --git a/soteria/tests/symex/symex.t b/soteria/tests/symex/symex.t index e8cce56ac..2755acc8c 100644 --- a/soteria/tests/symex/symex.t +++ b/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]