Add flags --fail-on-trap-only and fail-on-assertion-only

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"

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

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

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

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;
 

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

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* () =

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