Skip to content

Commit

Permalink
Add symbiotic submodule
Browse files Browse the repository at this point in the history
  • Loading branch information
filipeom committed Aug 29, 2024
1 parent b581e5d commit 0fb3e69
Show file tree
Hide file tree
Showing 5 changed files with 35 additions and 2 deletions.
3 changes: 3 additions & 0 deletions .gitmodules
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion bench/dune
Original file line number Diff line number Diff line change
@@ -1 +1 @@
(dirs :standard \ klee pie results-*)
(dirs :standard \ klee symbiotic pie results-*)
1 change: 1 addition & 0 deletions bench/symbiotic
Submodule symbiotic added at 787214
29 changes: 28 additions & 1 deletion bench/tool/tool.ml
Original file line number Diff line number Diff line change
Expand Up @@ -8,23 +8,30 @@ 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 wait_pid =
Expand Down Expand Up @@ -96,6 +103,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)
Expand Down Expand Up @@ -131,6 +149,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
Expand Down
2 changes: 2 additions & 0 deletions bench/tool/tool.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 0fb3e69

Please sign in to comment.