diff --git a/CHANGES.md b/CHANGES.md index 3cbb9677f..7ff67c406 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,6 @@ ## unreleased +- adds flags `--fail-on-trap-only` and `fail-on-assertion-only` - parameterize the `Thread` module on the symbolic memory and the `Choice_monad` module on a Thread - adds a `owi_char` function to create char symbolic value - adds a `Mem` argument to external function to allow direct manipulation of the memory. diff --git a/bench/tool/tool.ml b/bench/tool/tool.ml index f5d993c36..82ae1842f 100644 --- a/bench/tool/tool.ml +++ b/bench/tool/tool.ml @@ -107,6 +107,7 @@ let execvp ~output_dir tool file timeout = , [ "owi"; "c" ] @ (if concolic then [ "--concolic" ] else []) @ [ "--unsafe" + ; "--fail-on-assertion-only" ; Format.sprintf "-O%d" optimisation_level ; Format.sprintf "-w%d" workers ; "-o" diff --git a/example/c/README.md b/example/c/README.md index b4ce0e395..26e19f94d 100644 --- a/example/c/README.md +++ b/example/c/README.md @@ -297,6 +297,12 @@ OPTIONS Guarantee a fixed deterministic order of found failures. This implies --no-stop-at-failure. + --fail-on-assertion-only + ignore traps and only report assertion violations + + --fail-on-trap-only + ignore assertion violations and only report traps + -I VAL headers path diff --git a/example/conc/README.md b/example/conc/README.md index 62f8cbd78..25f8db645 100644 --- a/example/conc/README.md +++ b/example/conc/README.md @@ -53,6 +53,12 @@ OPTIONS Guarantee a fixed deterministic order of found failures. This implies --no-stop-at-failure. + --fail-on-assertion-only + ignore traps and only report assertion violations + + --fail-on-trap-only + ignore assertion violations and only report traps + --no-stop-at-failure do not stop when a program failure is encountered diff --git a/example/sym/README.md b/example/sym/README.md index bafaef1fb..40b9c9ca5 100644 --- a/example/sym/README.md +++ b/example/sym/README.md @@ -57,6 +57,12 @@ OPTIONS Guarantee a fixed deterministic order of found failures. This implies --no-stop-at-failure. + --fail-on-assertion-only + ignore traps and only report assertion violations + + --fail-on-trap-only + ignore assertion violations and only report traps + --no-stop-at-failure do not stop when a program failure is encountered diff --git a/src/bin/owi.ml b/src/bin/owi.ml index 588730178..a05686f3b 100644 --- a/src/bin/owi.ml +++ b/src/bin/owi.ml @@ -51,6 +51,16 @@ let no_values = let doc = "do not display a value for each symbol" in Cmdliner.Arg.(value & flag & info [ "no-value" ] ~doc) +let fail_mode = + let trap_doc = "ignore assertion violations and only report traps" in + let assert_doc = "ignore traps and only report assertion violations" in + Cmdliner.Arg.( + value + & vflag `Both + [ (`Trap_only, info [ "fail-on-trap-only" ] ~doc:trap_doc) + ; (`Assertion_only, info [ "fail-on-assertion-only" ] ~doc:assert_doc) + ] ) + let optimize = let doc = "optimize mode" in Cmdliner.Arg.(value & flag & info [ "optimize" ] ~doc) @@ -135,8 +145,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 - $ solver ) + $ no_stop_at_failure $ no_values $ deterministic_result_order $ fail_mode + $ concolic $ solver ) let fmt_cmd = let open Cmdliner in @@ -201,8 +211,8 @@ let sym_cmd = Cmd.v info Term.( const Cmd_sym.cmd $ profiling $ debug $ unsafe $ optimize $ workers - $ no_stop_at_failure $ no_values $ deterministic_result_order $ workspace - $ solver $ files ) + $ no_stop_at_failure $ no_values $ deterministic_result_order $ fail_mode + $ workspace $ solver $ files ) let conc_cmd = let open Cmdliner in @@ -214,8 +224,8 @@ let conc_cmd = Cmd.v info Term.( const Cmd_conc.cmd $ profiling $ debug $ unsafe $ optimize $ workers - $ no_stop_at_failure $ no_values $ deterministic_result_order $ workspace - $ solver $ files ) + $ no_stop_at_failure $ no_values $ deterministic_result_order $ fail_mode + $ workspace $ solver $ files ) let wasm2wat_cmd = let open Cmdliner in diff --git a/src/cmd/cmd_c.ml b/src/cmd/cmd_c.ml index 703d70b07..1805b7f8b 100644 --- a/src/cmd/cmd_c.ml +++ b/src/cmd/cmd_c.ml @@ -120,7 +120,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 solver : unit Result.t = + deterministic_result_order fail_mode concolic solver : unit Result.t = if debug then Logs.set_level (Some Debug); let workspace = Fpath.v workspace in let includes = libc_location @ includes in @@ -131,4 +131,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 solver files + deterministic_result_order fail_mode workspace solver files diff --git a/src/cmd/cmd_c.mli b/src/cmd/cmd_c.mli index 2a2b73d17..d87ca1344 100644 --- a/src/cmd/cmd_c.mli +++ b/src/cmd/cmd_c.mli @@ -18,6 +18,7 @@ val cmd : -> bool -> bool -> bool + -> Cmd_sym.fail_mode -> bool -> Smtml.Solver_dispatcher.solver_type -> unit Result.t diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index e114280f9..64a721c4e 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -401,7 +401,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) solver files = + _deterministic_result_order _fail_mode (workspace : Fpath.t) solver files = if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; diff --git a/src/cmd/cmd_conc.mli b/src/cmd/cmd_conc.mli index 2a258b383..5d841000a 100644 --- a/src/cmd/cmd_conc.mli +++ b/src/cmd/cmd_conc.mli @@ -11,6 +11,7 @@ val cmd : -> bool -> bool -> bool + -> Cmd_sym.fail_mode -> Fpath.t -> Smtml.Solver_dispatcher.solver_type -> Fpath.t list diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index f61287521..de0305963 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -6,6 +6,12 @@ open Syntax module Expr = Smtml.Expr module Choice = Symbolic_choice_with_memory +type fail_mode = + [ `Trap_only + | `Assertion_only + | `Both + ] + let ( let*/ ) (t : 'a Result.t) (f : 'a -> 'b Result.t Choice.t) : 'b Result.t Choice.t = match t with Error e -> Choice.return (Error e) | Ok x -> f x @@ -38,7 +44,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) solver files = + deterministic_result_order fail_mode (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 *) @@ -49,9 +55,15 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values let thread = Thread_with_memory.init () in let res_queue = Wq.init () in let callback v = - match v with - | Symbolic_choice_intf.EVal (Ok ()), _ -> () - | v -> Wq.push v res_queue + let open Symbolic_choice_intf in + match (fail_mode, v) with + | _, (EVal (Ok ()), _) -> () + | _, (EVal (Error e), thread) -> Wq.push (`Error e, thread) res_queue + | (`Both | `Trap_only), (ETrap (t, m), thread) -> + Wq.push (`ETrap (t, m), thread) res_queue + | (`Both | `Assertion_only), (EAssert (e, m), thread) -> + Wq.push (`EAssert (e, m), thread) res_queue + | (`Trap_only | `Assertion_only), _ -> () in let join_handles = Symbolic_choice_with_memory.run ~workers solver result thread ~callback @@ -75,17 +87,11 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values | Seq.Nil -> Ok count_acc | Seq.Cons ((result, _thread), tl) -> let* model = - let open Symbolic_choice_intf in match result with - | EAssert (assertion, model) -> - print_bug (`EAssert (assertion, model)); - Ok model - | ETrap (tr, model) -> - print_bug (`ETrap (tr, model)); + | (`EAssert (_, model) | `ETrap (_, model)) as bug -> + print_bug bug; Ok model - | EVal (Ok ()) -> - Fmt.failwith "unreachable: callback should have filtered eval ok out." - | EVal (Error e) -> Error e + | `Error e -> Error e in let count_acc = succ count_acc in let* () = diff --git a/src/cmd/cmd_sym.mli b/src/cmd/cmd_sym.mli index 2a258b383..938f1e343 100644 --- a/src/cmd/cmd_sym.mli +++ b/src/cmd/cmd_sym.mli @@ -2,6 +2,12 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) +type fail_mode = + [ `Trap_only + | `Assertion_only + | `Both + ] + val cmd : bool -> bool @@ -11,6 +17,7 @@ val cmd : -> bool -> bool -> bool + -> fail_mode -> Fpath.t -> Smtml.Solver_dispatcher.solver_type -> Fpath.t list