add a --solver CLI option :-)

src/bin/owi.ml

@@ -22,6 +22,18 @@ let dir_file =
   let parse s = `Ok (Fpath.v s) in
   (parse, Fpath.pp)
 
+let solver_conv =
+  Cmdliner.Arg.conv
+    ( Smtml.Solver_dispatcher.solver_type_of_string
+    , Smtml.Solver_dispatcher.pp_solver_type )
+
+let deterministic_result_order =
+  let doc =
+    "Guarantee a fixed deterministic order of found failures. This implies \
+     --no-stop-at-failure."
+  in
+  Cmdliner.Arg.(value & flag & info [ "deterministic-result-order" ] ~doc)
+
 let files =
   let doc = "source files" in
   let f = existing_non_dir_file in
@@ -39,13 +51,6 @@ let no_values =
   let doc = "do not display a value for each symbol" in
   Cmdliner.Arg.(value & flag & info [ "no-value" ] ~doc)
 
-let deterministic_result_order =
-  let doc =
-    "Guarantee a fixed deterministic order of found failures. This implies \
-     --no-stop-at-failure."
-  in
-  Cmdliner.Arg.(value & flag & info [ "deterministic-result-order" ] ~doc)
-
 let optimize =
   let doc = "optimize mode" in
   Cmdliner.Arg.(value & flag & info [ "optimize" ] ~doc)
@@ -54,6 +59,13 @@ let profiling =
   let doc = "profiling mode" in
   Cmdliner.Arg.(value & flag & info [ "profiling"; "p" ] ~doc)
 
+let solver =
+  let doc = "SMT solver to use" in
+  Cmdliner.Arg.(
+    value
+    & opt solver_conv Smtml.Solver_dispatcher.Z3_solver
+    & info [ "solver"; "s" ] ~doc )
+
 let unsafe =
   let doc = "skip typechecking pass" in
   Cmdliner.Arg.(value & flag & info [ "unsafe"; "u" ] ~doc)
@@ -123,7 +135,8 @@ let c_cmd =
     Term.(
       const Cmd_c.cmd $ debug $ arch $ property $ testcomp $ output $ workers
       $ opt_lvl $ includes $ files $ profiling $ unsafe $ optimize
-      $ no_stop_at_failure $ no_values $ deterministic_result_order $ concolic )
+      $ no_stop_at_failure $ no_values $ deterministic_result_order $ concolic
+      $ solver )
 
 let fmt_cmd =
   let open Cmdliner in
@@ -189,7 +202,7 @@ let sym_cmd =
     Term.(
       const Cmd_sym.cmd $ profiling $ debug $ unsafe $ optimize $ workers
       $ no_stop_at_failure $ no_values $ deterministic_result_order $ workspace
-      $ files )
+      $ solver $ files )
 
 let conc_cmd =
   let open Cmdliner in
@@ -202,7 +215,7 @@ let conc_cmd =
     Term.(
       const Cmd_conc.cmd $ profiling $ debug $ unsafe $ optimize $ workers
       $ no_stop_at_failure $ no_values $ deterministic_result_order $ workspace
-      $ files )
+      $ solver $ files )
 
 let wasm2wat_cmd =
   let open Cmdliner in

src/cmd/cmd_c.ml

@@ -95,7 +95,7 @@ let metadata ~workspace arch property files : unit Result.t =
 
 let cmd debug arch property _testcomp workspace workers opt_lvl includes files
   profiling unsafe optimize no_stop_at_failure no_values
-  deterministic_result_order concolic : unit Result.t =
+  deterministic_result_order concolic solver : unit Result.t =
   if debug then Logs.set_level (Some Debug);
   let workspace = Fpath.v workspace in
   let includes = C_share.lib_location @ includes in
@@ -106,4 +106,4 @@ let cmd debug arch property _testcomp workspace workers opt_lvl includes files
   let files = [ modul ] in
   (if concolic then Cmd_conc.cmd else Cmd_sym.cmd)
     profiling debug unsafe optimize workers no_stop_at_failure no_values
-    deterministic_result_order workspace files
+    deterministic_result_order workspace solver files

src/cmd/cmd_c.mli

@@ -19,4 +19,5 @@ val cmd :
   -> bool
   -> bool
   -> bool
+  -> Smtml.Solver_dispatcher.solver_type
   -> unit Result.t

src/cmd/cmd_conc.ml

@@ -590,7 +590,7 @@ let launch solver tree link_state modules_to_run =
    which are handled here. Most of the computations are done in the Result
    monad, hence the let*. *)
 let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
-  deterministic_result_order (workspace : Fpath.t) files =
+  deterministic_result_order (workspace : Fpath.t) solver files =
   ignore (workers, no_stop_at_failure, deterministic_result_order, workspace);
 
   if profiling then Log.profiling_on := true;
@@ -599,7 +599,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.fresh () in
+  let solver = Solver.fresh solver () in
   let* link_state, modules_to_run =
     simplify_then_link_files ~unsafe ~optimize files
   in

src/cmd/cmd_conc.mli

@@ -12,5 +12,6 @@ val cmd :
   -> bool
   -> bool
   -> Fpath.t
+  -> Smtml.Solver_dispatcher.solver_type
   -> Fpath.t list
   -> unit Result.t

src/cmd/cmd_sym.ml

@@ -235,7 +235,7 @@ let run_file ~unsafe ~optimize pc filename =
    which are handled here. Most of the computations are done in the Result
    monad, hence the let*. *)
 let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
-  deterministic_result_order (workspace : Fpath.t) files =
+  deterministic_result_order (workspace : Fpath.t) solver files =
   if profiling then Log.profiling_on := true;
   if debug then Log.debug_on := true;
   (* deterministic_result_order implies no_stop_at_failure *)
@@ -244,7 +244,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
   let pc = Choice.return (Ok ()) in
   let result = List.fold_left (run_file ~unsafe ~optimize) pc files in
   let thread : Thread.t = Thread.create () in
-  let results = Symbolic_choice.run ~workers result thread in
+  let results = Symbolic_choice.run ~workers solver result thread in
   let print_bug = function
     | `ETrap (tr, model) ->
       Format.pp_std "Trap: %s@\n" (Trap.to_string tr);

src/cmd/cmd_sym.mli

@@ -12,5 +12,6 @@ val cmd :
   -> bool
   -> bool
   -> Fpath.t
+  -> Smtml.Solver_dispatcher.solver_type
   -> Fpath.t list
   -> unit Result.t

src/symbolic/solver.ml

@@ -6,8 +6,10 @@ type 'a solver_module = (module Smtml.Solver_intf.S with type t = 'a)
 
 type t = S : ('a solver_module * 'a) -> t [@@unboxed]
 
-let fresh () =
-  let module Mapping = Smtml.Z3_mappings.Fresh.Make () in
+let fresh solver () =
+  let module Mapping = (val Smtml.Solver_dispatcher.mappings_of_solver solver)
+  in
+  let module Mapping = Mapping.Fresh.Make () in
   let module Batch = Smtml.Solver.Batch (Mapping) in
   let solver = Batch.create ~logic:QF_BVFP () in
   S ((module Batch), solver)

src/symbolic/solver.mli

@@ -4,7 +4,7 @@
 
 type t
 
-val fresh : unit -> t
+val fresh : Smtml.Solver_dispatcher.solver_type -> unit -> t
 
 val check : t -> Smtml.Expr.t list -> Smtml.Solver_intf.satisfiability
 

src/symbolic/symbolic_choice.ml

@@ -65,7 +65,12 @@ module CoreImpl : sig
 
   type 'a run_result = ('a eval * Thread.t) Seq.t
 
-  val run : workers:int -> 'a t -> Thread.t -> 'a run_result
+  val run :
+       workers:int
+    -> Smtml.Solver_dispatcher.solver_type
+    -> 'a t
+    -> Thread.t
+    -> 'a run_result
 end = struct
   module Schedulable = struct
     (*
@@ -162,15 +167,13 @@ end = struct
     let spawn_worker sched wls_init =
       Wq.make_pledge sched.res_writer;
       Domain.spawn (fun () ->
-          let wls = wls_init () in
           Fun.protect
-            ~finally:(fun () -> Wq.end_pledge sched.res_writer)
+            ~finally:(fun () ->
+              Wq.end_pledge sched.res_writer;
+              Wq.fail sched.work_queue )
             (fun () ->
-              try work wls sched
-              with e ->
-                let bt = Printexc.get_raw_backtrace () in
-                Wq.fail sched.work_queue;
-                Printexc.raise_with_backtrace e bt ) )
+              let wls = wls_init () in
+              work wls sched ) )
   end
 
   module State = struct
@@ -295,13 +298,13 @@ end = struct
 
   type 'a run_result = ('a eval * Thread.t) Seq.t
 
-  let run ~workers t thread =
+  let run ~workers solver t thread =
     let open Scheduler in
     let sched = init_scheduler () in
     add_init_task sched (State.run t thread);
     let join_handles =
       Array.map
-        (fun () -> spawn_worker sched Solver.fresh)
+        (fun () -> spawn_worker sched (Solver.fresh solver))
         (Array.init workers (Fun.const ()))
     in
     Wq.read_as_seq sched.res_writer ~finalizer:(fun () ->

src/symbolic/symbolic_choice.mli

@@ -13,4 +13,9 @@ include
      and type 'a run_result = ('a eval * Thread.t) Seq.t
      and module V := Symbolic_value
 
-val run : workers:int -> 'a t -> Thread.t -> 'a run_result
+val run :
+     workers:int
+  -> Smtml.Solver_dispatcher.solver_type
+  -> 'a t
+  -> Thread.t
+  -> 'a run_result

src/symbolic/symbolic_choice_minimalist.ml

@@ -63,4 +63,4 @@ let solver = M (fun st sol -> (Ok sol, st))
 
 let add_pc (_vb : vbool) = return ()
 
-let run ~workers:_ t thread = run t thread (Solver.fresh ())
+let run ~workers:_ solver t thread = run t thread (Solver.fresh solver ())

src/symbolic/symbolic_choice_minimalist.mli

@@ -12,4 +12,9 @@ include
      and type 'a run_result = ('a, err) Stdlib.Result.t * Thread.t
      and module V := Symbolic_value
 
-val run : workers:int -> 'a t -> Thread.t -> 'a run_result
+val run :
+     workers:int
+  -> Smtml.Solver_dispatcher.solver_type
+  -> 'a t
+  -> Thread.t
+  -> 'a run_result

test/fuzz/interprets.ml

@@ -84,8 +84,8 @@ module Owi_symbolic : INTERPRET = struct
         let c = Interpret.SymbolicM.modul link_state.envs regular in
         let init_thread : Thread.t = Thread.create () in
         let res, _ =
-          Symbolic_choice_minimalist.run ~workers:dummy_workers_count c
-            init_thread
+          Symbolic_choice_minimalist.run ~workers:dummy_workers_count
+            Smtml.Solver_dispatcher.Z3_solver c init_thread
         in
         match res with
         | Ok res -> res