allow to run concolic bench

bench/testcomp/testcomp.ml

@@ -3,9 +3,9 @@ module Unix = struct
   include Bos.OS.U
 end
 
-let _tool = Tool.mk_owi ~workers:4 ~optimisation_level:1
+let tool = Tool.mk_owi ~concolic:false ~workers:24 ~optimisation_level:3
 
-let tool = Tool.mk_klee ()
+let _tool = Tool.mk_klee ()
 
 let reference_name = Tool.to_reference_name tool
 

bench/tool/tool.ml

@@ -1,7 +1,8 @@
 type t =
   | Owi of
-      { workers : int
+      { concolic : bool
       ; optimisation_level : int
+      ; workers : int
       }
   | Klee
 
@@ -10,11 +11,13 @@ let ( let+ ) o f = match o with Ok v -> Ok (f v) | Error _ as e -> e
 let to_short_name = function Owi _ -> "owi" | Klee -> "klee"
 
 let to_reference_name = function
-  | Owi { workers; optimisation_level } ->
-    Format.sprintf "owi_w%d_O%d" workers optimisation_level
+  | Owi { concolic; workers; optimisation_level } ->
+    Format.sprintf "owi_w%d_O%d%s" workers optimisation_level
+      (if concolic then "_concolic" else "")
   | Klee -> "klee"
 
-let mk_owi ~workers ~optimisation_level = Owi { workers; optimisation_level }
+let mk_owi ~concolic ~workers ~optimisation_level =
+  Owi { concolic; workers; optimisation_level }
 
 let mk_klee () = Klee
 
@@ -94,29 +97,30 @@ let execvp ~output_dir tool file timeout =
   let timeout = string_of_int timeout in
   let bin, args =
     match tool with
-    | Owi { workers; optimisation_level } ->
+    | Owi { workers; optimisation_level; concolic } ->
       ( "owi"
-      , [| "owi"
-         ; "c"
-         ; "--unsafe"
-         ; Format.sprintf "-O%d" optimisation_level
-         ; Format.sprintf "-w%d" workers
-         ; "-o"
-         ; output_dir
-         ; file
-        |] )
+      , [ "owi"; "c" ]
+        @ (if concolic then [ "--concolic" ] else [])
+        @ [ "--unsafe"
+          ; Format.sprintf "-O%d" optimisation_level
+          ; Format.sprintf "-w%d" workers
+          ; "-o"
+          ; output_dir
+          ; file
+          ] )
     | Klee ->
       let path_to_klee = "klee/bin/klee" in
       ( path_to_klee
-      , [| path_to_klee
-         ; "--error-only"
-         ; "--max-time"
-         ; timeout
-         ; "--max-walltime"
-         ; timeout
-         ; file
-        |] )
+      , [ path_to_klee
+        ; "--error-only"
+        ; "--max-time"
+        ; timeout
+        ; "--max-walltime"
+        ; timeout
+        ; file
+        ] )
   in
+  let args = Array.of_list args in
   Unix.execvp bin args
 
 let dup ~src ~dst =

bench/tool/tool.mli

@@ -4,7 +4,7 @@ val to_short_name : t -> string
 
 val to_reference_name : t -> string
 
-val mk_owi : workers:int -> optimisation_level:int -> t
+val mk_owi : concolic:bool -> workers:int -> optimisation_level:int -> t
 
 val mk_klee : unit -> t
 

src/cmd/cmd_conc.ml

@@ -542,16 +542,17 @@ let find_model_to_run solver tree =
 
 let launch solver tree link_state modules_to_run =
   let rec find_model n =
-    if n = 0 then
-      let () = Format.pp_std "Failed to find something to run@." in
+    if n = 0 then begin
+      Format.pp_std "Failed to find something to run@\n";
       None
+    end
     else
       match find_model_to_run solver tree with
       | None -> find_model (n - 1)
       | Some m ->
         if debug then begin
-          Format.pp_std "Found something to run %a@."
-            (fun ppf v -> Smtml.Model.pp ppf v)
+          Format.pp_std "Found something to run %a@\n"
+            (Smtml.Model.pp ~no_values:false)
             m
         end;
         Some m
@@ -577,7 +578,7 @@ let launch solver tree link_state modules_to_run =
       | None ->
         Format.pp_err "Can't satisfy assume !@\n";
         loop (count - 1)
-      | Some model -> run_model (Some model) (count - 1)
+      | Some _model as model -> run_model model (count - 1)
     end
     | Error (Trap trap) -> Some (`Trap trap, thread)
     | Error Assert_fail -> Some (`Assert_fail, thread)