From e32bc55fb0b01ca01103ab20010b11c2e5f96446 Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Mon, 3 Jun 2024 13:27:47 +0200 Subject: [PATCH] clean solver interface --- src/interpret/choice_intf.ml | 2 +- src/symbolic/solver.ml | 18 +++++--- src/symbolic/solver.mli | 21 +++++++++ src/symbolic/symbolic_choice.ml | 80 +++++++++++++++++---------------- 4 files changed, 76 insertions(+), 45 deletions(-) create mode 100644 src/symbolic/solver.mli diff --git a/src/interpret/choice_intf.ml b/src/interpret/choice_intf.ml index 9aa17a38b..41d8ca52a 100644 --- a/src/interpret/choice_intf.ml +++ b/src/interpret/choice_intf.ml @@ -35,7 +35,7 @@ module type Complete = sig val with_thread : (thread -> 'b) -> 'b t - val solver : Solver.solver t + val solver : Solver.t t val thread : thread t diff --git a/src/symbolic/solver.ml b/src/symbolic/solver.ml index 52a876f20..9a8e35b24 100644 --- a/src/symbolic/solver.ml +++ b/src/symbolic/solver.ml @@ -2,16 +2,22 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -type 'a solver_module = (module Smtml.Solver_intf.S with type t = 'a) - -type solver = S : ('a solver_module * 'a) -> solver [@@unboxed] - module Z3Batch = Smtml.Solver.Batch (Smtml.Z3_mappings) -let solver_mod : Z3Batch.t solver_module = (module Z3Batch) +type 'a solver_module = (module Smtml.Solver_intf.S with type t = 'a) -let fresh_solver () = +type t = S : ('a solver_module * 'a) -> t [@@unboxed] + +let fresh () = let module Mapping = Smtml.Z3_mappings.Fresh.Make () in let module Batch = Smtml.Solver.Batch (Mapping) in let solver = Batch.create ~logic:QF_BVFP () in S ((module Batch), solver) + +let check (S (solver_module, s)) pc = + let module Solver = (val solver_module) in + Solver.check s pc + +let model (S (solver_module, s)) ~symbols = + let module Solver = (val solver_module) in + Solver.model ~symbols s diff --git a/src/symbolic/solver.mli b/src/symbolic/solver.mli new file mode 100644 index 000000000..880dd6406 --- /dev/null +++ b/src/symbolic/solver.mli @@ -0,0 +1,21 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + +module Z3Batch : sig + type t + + val create : ?params:Smtml.Params.t -> ?logic:Smtml.Ty.logic -> unit -> t + + val check : t -> Smtml.Expr.t list -> Smtml.Solver_intf.satisfiability + + val model : ?symbols:Smtml.Symbol.t list -> t -> Smtml.Model.t option +end + +type t + +val fresh : unit -> t + +val check : t -> Smtml.Expr.t list -> Smtml.Solver_intf.satisfiability + +val model : t -> symbols:Smtml.Symbol.t list -> Smtml.Model.t option diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index 1a55075bc..0a72b34b0 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -2,18 +2,17 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -open Solver -open Smtml open Symbolic_value -exception Assertion of Expr.t * Thread.t +exception Assertion of Smtml.Expr.t * Thread.t module Minimalist = struct type err = | Assert_fail | Trap of Trap.t - type 'a t = M of (Thread.t -> solver -> ('a, err) Stdlib.Result.t * Thread.t) + type 'a t = + | M of (Thread.t -> Solver.t -> ('a, err) Stdlib.Result.t * Thread.t) [@@unboxed] type 'a run_result = ('a, err) Stdlib.Result.t * Thread.t @@ -39,21 +38,23 @@ module Minimalist = struct let ( let+ ) = map let select (vb : vbool) = - let v = Expr.simplify vb in - match Expr.view v with + let v = Smtml.Expr.simplify vb in + match Smtml.Expr.view v with | Val True -> return true | Val False -> return false - | _ -> Format.kasprintf failwith "%a" Expr.pp v + | _ -> Format.kasprintf failwith "%a" Smtml.Expr.pp v let select_i32 (i : int32) = - let v = Expr.simplify i in - match Expr.view v with Val (Num (I32 i)) -> return i | _ -> assert false + let v = Smtml.Expr.simplify i in + match Smtml.Expr.view v with + | Val (Num (I32 i)) -> return i + | _ -> assert false let trap t = M (fun th _sol -> (Error (Trap t), th)) let assertion (vb : vbool) = - let v = Expr.simplify vb in - match Expr.view v with + let v = Smtml.Expr.simplify vb in + match Smtml.Expr.view v with | Val True -> return () | Val False -> M (fun th _sol -> (Error Assert_fail, th)) | _ -> assert false @@ -66,7 +67,7 @@ module Minimalist = struct let add_pc (_vb : vbool) = return () - let run ~workers:_ t thread = run t thread (fresh_solver ()) + let run ~workers:_ t thread = run t thread (Solver.fresh ()) end module WQ = struct @@ -172,7 +173,7 @@ module Multicore = struct val stop : 'a t - val assertion_fail : Expr.t -> 'a t + val assertion_fail : Smtml.Expr.t -> 'a t val trap : Trap.t -> 'a t @@ -180,7 +181,7 @@ module Multicore = struct val yield : unit t - val solver : solver t + val solver : Solver.t t val with_thread : (Thread.t -> 'a) -> 'a t @@ -197,7 +198,7 @@ module Multicore = struct type 'a eval = | EVal of 'a | ETrap of Trap.t - | EAssert of Expr.t + | EAssert of Smtml.Expr.t type 'a run_result = ('a eval * Thread.t) Seq.t @@ -314,7 +315,8 @@ module Multicore = struct *) module M = Schedulable - type 'a t = St of (Thread.t -> ('a * Thread.t, solver) M.t) [@@unboxed] + type 'a t = St of (Thread.t -> ('a * Thread.t, Solver.t) M.t) + [@@unboxed] let run (St mxf) st = mxf st @@ -359,7 +361,7 @@ module Multicore = struct type 'a eval = | EVal of 'a | ETrap of Trap.t - | EAssert of Expr.t + | EAssert of Smtml.Expr.t type 'a t = 'a eval M.t @@ -436,7 +438,7 @@ module Multicore = struct add_init_task sched (State.run t thread); let join_handles = Array.map - (fun () -> spawn_worker sched fresh_solver) + (fun () -> spawn_worker sched Solver.fresh) (Array.init workers (Fun.const ())) in WQ.read_as_seq sched.res_writer ~finalizer:(fun () -> @@ -455,7 +457,7 @@ module Multicore = struct include CoreImpl let add_pc (c : vbool) = - match Expr.view c with + match Smtml.Expr.view c with | Val True -> return () | Val False -> stop | _ -> @@ -473,27 +475,25 @@ module Multicore = struct *) let check_reachability = let* () = yield in - let* (S (solver_module, s)) = solver in - let module Solver = (val solver_module) in let* thread in - match Solver.check s thread.pc with + let* solver in + match Solver.check solver thread.pc with | `Sat -> return () | `Unsat | `Unknown -> stop let get_model symbol = let* () = yield in - let* (S (solver_module, s)) = solver in - let module Solver = (val solver_module) in + let* solver in let+ thread in - match Solver.check s thread.pc with + match Solver.check solver thread.pc with | `Unsat | `Unknown -> None | `Sat -> begin - let model = Solver.model ~symbols:[ symbol ] s in + let model = Solver.model solver ~symbols:[ symbol ] in match model with | None -> failwith "Unreachable: The problem is sat so a model should exist" | Some model -> begin - match Model.evaluate model symbol with + match Smtml.Model.evaluate model symbol with | None -> failwith "Unreachable: The model exists so this symbol should evaluate" @@ -506,8 +506,8 @@ module Multicore = struct match model with Some v -> return v | None -> stop let select (cond : Symbolic_value.vbool) = - let v = Expr.simplify cond in - match Expr.view v with + let v = Smtml.Expr.simplify cond in + match Smtml.Expr.view v with | Val True -> return true | Val False -> return false | Val (Num (I32 _)) -> failwith "unreachable (type error)" @@ -527,21 +527,21 @@ module Multicore = struct choose true_branch false_branch [@@inline] - let summary_symbol (e : Expr.t) = + let summary_symbol (e : Smtml.Expr.t) = let* thread in - match Expr.view e with + match Smtml.Expr.view e with | Symbol sym -> return (None, sym) | _ -> let choices = thread.choices in let symbol_name = Format.sprintf "choice_i32_%i" choices in let+ () = modify_thread (fun t -> { t with choices = choices + 1 }) in - let sym = Symbol.(symbol_name @: Ty_bitv 32) in - let assign = Expr.(relop Ty_bool Eq (mk_symbol sym) e) in + let sym = Smtml.Symbol.(symbol_name @: Ty_bitv 32) in + let assign = Smtml.Expr.(relop Ty_bool Eq (mk_symbol sym) e) in (Some assign, sym) let select_i32 (i : Symbolic_value.int32) = - let sym_int = Expr.simplify i in - match Expr.view sym_int with + let sym_int = Smtml.Expr.simplify i in + match Smtml.Expr.view sym_int with | Val (Num (I32 i)) -> return i | _ -> let* assign, symbol = summary_symbol sym_int in @@ -555,10 +555,14 @@ module Multicore = struct | Num (I32 i) -> i | _ -> failwith "Unreachable: found symbol must be a value" in - let this_value_cond = Expr.Bitv.I32.(Expr.mk_symbol symbol = v i) in + let this_value_cond = + let open Smtml.Expr in + Bitv.I32.(mk_symbol symbol = v i) + in let not_this_value_cond = - (* != is **not** the physical equality here *) - Expr.Bitv.I32.(Expr.mk_symbol symbol != v i) + let open Smtml.Expr in + (* != is **not** the physical inequality here *) + Bitv.I32.(Smtml.Expr.mk_symbol symbol != v i) in let this_val_branch = let* () = add_breadcrumb i in