Add symbiotic runner

.gitmodules

@@ -14,3 +14,6 @@
 	path = test/c/collections-c/files
 	url = https://github.com/zapashcanon/Collections-C.git
 	shallow = true
+[submodule "bench/symbiotic"]
+	path = bench/symbiotic
+	url = https://github.com/filipeom/symbiotic-testcomp.git

bench/dune

@@ -1 +1 @@
-(dirs :standard \ klee pie results-*)
+(dirs :standard \ klee symbiotic pie results-*)

bench/tool/tool.ml

@@ -8,25 +8,36 @@ type t =
       ; solver : S.solver_type
       }
   | Klee
+  | Symbiotic
 
 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_short_name = function
+  | Owi _ -> "owi"
+  | Klee -> "klee"
+  | Symbiotic -> "symbiotic"
 
 let to_reference_name = function
   | Owi { concolic; workers; optimisation_level; solver } ->
     Format.asprintf "owi_w%d_O%d_s%a%s" workers optimisation_level
       S.pp_solver_type solver
       (if concolic then "_concolic" else "")
   | Klee -> "klee"
+  | Symbiotic -> "symbiotic"
 
 let mk_owi ~concolic ~workers ~optimisation_level ~solver =
   Owi { concolic; workers; optimisation_level; solver }
 
 let mk_klee () = Klee
 
+let mk_symbiotic () = Symbiotic
+
 exception Sigchld
 
+let kill_klee_descendants () =
+  let _ = Format.ksprintf Sys.command "pkill klee" in
+  ()
+
 let wait_pid =
   let last_utime = ref 0. in
   let last_stime = ref 0. in
@@ -46,6 +57,8 @@ let wait_pid =
     end;
     Sys.set_signal Sys.sigchld Signal_default;
     let waited_pid, status = Unix.waitpid [] (-pid) in
+    (* Because symbiotic is leaking klee processes *)
+    kill_klee_descendants ();
     let end_time = Unix.gettimeofday () in
     let { Rusage.utime; stime; _ } = Rusage.get Rusage.Children in
     assert (waited_pid = pid);
@@ -96,6 +109,17 @@ let wait_pid =
             if !has_found_error then Reached rusage else Nothing rusage
           end
           else Other (rusage, code)
+        | Symbiotic ->
+          if code = 0 then begin
+            match Bos.OS.File.read dst_stderr with
+            | Error (`Msg err) -> failwith err
+            | Ok data -> (
+              let error = Astring.String.find_sub ~sub:"Found ERROR!" data in
+              match error with
+              | Some _ -> Reached rusage
+              | None -> Nothing rusage )
+          end
+          else Other (rusage, code)
       end
       | WSIGNALED n -> Signaled (rusage, n)
       | WSTOPPED n -> Stopped (rusage, n)
@@ -131,6 +155,15 @@ let execvp ~output_dir tool file timeout =
         ; timeout
         ; file
         ] )
+    | Symbiotic ->
+      let path_to_symbiotic = "symbiotic/bin/symbiotic" in
+      ( path_to_symbiotic
+      , [ path_to_symbiotic
+        ; "--test-comp"
+        ; Format.sprintf "--timeout=%s" timeout
+        ; "--prp=testcomp/sv-benchmarks/c/properties/coverage-error-call.prp"
+        ; file
+        ] )
   in
   let args = Array.of_list args in
   Unix.execvp bin args

bench/tool/tool.mli

@@ -13,6 +13,8 @@ val mk_owi :
 
 val mk_klee : unit -> t
 
+val mk_symbiotic : unit -> t
+
 val fork_and_run_on_file :
      i:int
   -> fmt:Format.formatter