From 6f4362fa5a46729d1f675018369e6c71ed15cdd8 Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Mon, 3 Jun 2024 18:39:53 +0200 Subject: [PATCH] do not use a global solver --- src/cmd/cmd_conc.ml | 16 +++++++------- src/cmd/cmd_sym.ml | 35 +++++++++++++------------------ src/symbolic/solver.ml | 2 -- src/symbolic/solver.mli | 10 --------- src/symbolic/symbolic_choice.ml | 36 +++++++++++++++++++++++--------- src/symbolic/symbolic_choice.mli | 6 ++---- 6 files changed, 50 insertions(+), 55 deletions(-) diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index 68b6b9d9b..bf051705e 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -256,10 +256,10 @@ let run_modules_to_run (link_state : _ Link.state) modules_to_run = (Interpret.Concolic.modul link_state.envs) to_run ) (Choice.return (Ok ())) modules_to_run -let get_model (* ~symbols *) solver pc = +let get_model ~symbols solver pc = let expr = Concolic_choice.pc_to_exprs pc in - assert (`Sat = Solver.Z3Batch.check solver expr); - match Solver.Z3Batch.model (* ~symbols *) solver with + assert (`Sat = Solver.check solver expr); + match Solver.model ~symbols solver with | None -> assert false | Some model -> model @@ -446,10 +446,10 @@ let rec find_node_to_run tree = let pc_model solver pc = let expr = Concolic_choice.pc_to_exprs pc in - match Solver.Z3Batch.check solver expr with + match Solver.check solver expr with | `Unsat | `Unknown -> None | `Sat -> ( - match Solver.Z3Batch.model solver with + match Solver.model ~symbols:[] solver with | None -> assert false | Some model -> Some model ) @@ -516,7 +516,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values (* deterministic_result_order implies no_stop_at_failure *) (* let no_stop_at_failure = deterministic_result_order || no_stop_at_failure in *) let* _created_dir = Bos.OS.Dir.create ~path:true ~mode:0o755 workspace in - let solver = Solver.Z3Batch.create () in + let solver = Solver.fresh () in let* link_state, modules_to_run = simplify_then_link_files ~unsafe ~optimize files in @@ -555,7 +555,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values print_pc thread.pc; print_values thread.symbols_value end; - let model = get_model solver thread.pc in + let model = get_model ~symbols:[] solver thread.pc in Format.pp_std "Model:@\n @[%a@]@." (Smtml.Model.pp ~no_values) model; let* () = testcase model in Error (`Found_bug 1) @@ -565,7 +565,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values print_pc thread.pc; print_values thread.symbols_value end; - let model = get_model solver thread.pc in + let model = get_model ~symbols:[] solver thread.pc in Format.pp_std "Model:@\n @[%a@]@." (Smtml.Model.pp ~no_values) model; let* () = testcase model in Error (`Found_bug 1) diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index 5d6e9295e..6f53a1e2e 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -72,14 +72,14 @@ let summaries_extern_module : | Val (Num (I32 v)) -> Choice.return v | _ -> Log.debug2 {|alloc: cannot allocate base pointer "%a"|} Expr.pp v; - Choice.bind (abort ()) (fun () -> Choice.return 666l) + Choice.bind (abort ()) (fun () -> assert false) in let ptr v : int32 Choice.t = match view v with | Ptr (b, _) -> Choice.return b | _ -> Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v; - Choice.bind (abort ()) (fun () -> Choice.return 667l) + Choice.bind (abort ()) (fun () -> assert false) in let alloc (base : Value.int32) (size : Value.int32) : Value.int32 Choice.t = Choice.bind (i32 base) (fun base -> @@ -230,12 +230,6 @@ let run_file ~unsafe ~optimize pc filename = in run_binary_modul ~unsafe ~optimize pc m -let get_model ~symbols solver pc = - assert (`Sat = Solver.Z3Batch.check solver pc); - match Solver.Z3Batch.model ~symbols solver with - | None -> assert false - | Some model -> model - (* NB: This function propagates potential errors (Result.err) occurring during evaluation (OS, syntax error, etc.), except for Trap and Assert, which are handled here. Most of the computations are done in the Result @@ -248,7 +242,6 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values let no_stop_at_failure = deterministic_result_order || no_stop_at_failure in let* _created_dir = Bos.OS.Dir.create ~path:true ~mode:0o755 workspace in let pc = Choice.return (Ok ()) in - let solver = Solver.Z3Batch.create () in let result = List.fold_left (run_file ~unsafe ~optimize) pc files in let thread : Thread.t = Thread.create () in let results = Choice.run ~workers result thread in @@ -263,25 +256,25 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values let rec print_and_count_failures count_acc results = match results () with | Seq.Nil -> Ok count_acc - | Seq.Cons ((result, thread), tl) -> - let pc = Thread.pc thread in - let symbols = thread.symbol_set in - let model = get_model ~symbols solver pc in - let* is_err = + | Seq.Cons ((result, _thread), tl) -> + let* is_err, model = let open Symbolic_choice.Multicore in match result with - | EAssert assertion -> + | EAssert (assertion, model) -> print_bug (`EAssert (assertion, model)); - Ok true - | ETrap tr -> + Ok (true, Some model) + | ETrap (tr, model) -> print_bug (`ETrap (tr, model)); - Ok true - | EVal (Ok ()) -> Ok false + Ok (true, Some model) + | EVal (Ok ()) -> Ok (false, None) | EVal (Error e) -> Error e in let count_acc = if is_err then succ count_acc else count_acc in let* () = if not no_values then + let model = + match model with None -> Hashtbl.create 16 | Some m -> m + in let testcase = List.sort compare (Smtml.Model.get_bindings model) |> List.map snd in @@ -295,8 +288,8 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values let results = if deterministic_result_order then results - |> Seq.map (function (_, th) as x -> - (x, List.rev @@ Thread.breadcrumbs th) ) + |> Seq.map (function (_, thread) as x -> + (x, List.rev @@ Thread.breadcrumbs thread) ) |> List.of_seq |> List.sort (fun (_, bc1) (_, bc2) -> List.compare Stdlib.Int32.compare bc1 bc2 ) diff --git a/src/symbolic/solver.ml b/src/symbolic/solver.ml index 9a8e35b24..92feb0b80 100644 --- a/src/symbolic/solver.ml +++ b/src/symbolic/solver.ml @@ -2,8 +2,6 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -module Z3Batch = Smtml.Solver.Batch (Smtml.Z3_mappings) - type 'a solver_module = (module Smtml.Solver_intf.S with type t = 'a) type t = S : ('a solver_module * 'a) -> t [@@unboxed] diff --git a/src/symbolic/solver.mli b/src/symbolic/solver.mli index 880dd6406..6e7dc682b 100644 --- a/src/symbolic/solver.mli +++ b/src/symbolic/solver.mli @@ -2,16 +2,6 @@ (* 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 diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index 9156d6c7a..a0743ab40 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -4,8 +4,6 @@ open Symbolic_value -exception Assertion of Smtml.Expr.t * Thread.t - module Minimalist = struct type err = | Assert_fail @@ -173,7 +171,7 @@ module Multicore = struct val stop : 'a t - val assertion_fail : Smtml.Expr.t -> 'a t + val assertion_fail : Smtml.Expr.t -> Smtml.Model.t -> 'a t val trap : Trap.t -> 'a t @@ -197,8 +195,8 @@ module Multicore = struct type 'a eval = | EVal of 'a - | ETrap of Trap.t - | EAssert of Smtml.Expr.t + | ETrap of Trap.t * Smtml.Model.t + | EAssert of Smtml.Expr.t * Smtml.Model.t type 'a run_result = ('a eval * Thread.t) Seq.t @@ -360,8 +358,8 @@ module Multicore = struct type 'a eval = | EVal of 'a - | ETrap of Trap.t - | EAssert of Smtml.Expr.t + | ETrap of Trap.t * Smtml.Model.t + | EAssert of Smtml.Expr.t * Smtml.Model.t type 'a t = 'a eval M.t @@ -444,9 +442,20 @@ module Multicore = struct WQ.read_as_seq sched.res_writer ~finalizer:(fun () -> Array.iter Domain.join join_handles ) - let trap t = State.return (ETrap t) + let trap t = + let* thread in + let* solver in + match Solver.check solver thread.pc with + | `Sat -> + let symbols = thread.symbol_set in + begin + match Solver.model ~symbols solver with + | None -> assert false + | Some model -> State.return (ETrap (t, model)) + end + | `Unsat | `Unknown -> stop - let assertion_fail c = State.return (EAssert c) + let assertion_fail c model = State.return (EAssert (c, model)) end (* @@ -579,5 +588,12 @@ module Multicore = struct let assertion c = let* assertion_true = select c in - if assertion_true then return () else assertion_fail c + if assertion_true then return () + else + let* thread in + let* solver in + let symbols = thread.symbol_set in + match Solver.model ~symbols solver with + | None -> assert false + | Some model -> assertion_fail c model end diff --git a/src/symbolic/symbolic_choice.mli b/src/symbolic/symbolic_choice.mli index 96505fd16..899157ec8 100644 --- a/src/symbolic/symbolic_choice.mli +++ b/src/symbolic/symbolic_choice.mli @@ -2,8 +2,6 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -exception Assertion of Smtml.Expr.t * Thread.t - module Minimalist : sig type err = private | Assert_fail @@ -19,8 +17,8 @@ end module Multicore : sig type 'a eval = | EVal of 'a - | ETrap of Trap.t - | EAssert of Smtml.Expr.t + | ETrap of Trap.t * Smtml.Model.t + | EAssert of Smtml.Expr.t * Smtml.Model.t include Choice_intf.Complete