do not use a global solver

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  @[<v>%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  @[<v>%a@]@." (Smtml.Model.pp ~no_values) model;
     let* () = testcase model in
     Error (`Found_bug 1)

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 )

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]

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

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

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