add a no-assert-failure-expression-printing

CHANGES.md

@@ -20,6 +20,7 @@
 - start benchmarking against test-comp
 - fix handling of `select` and `call_indirect` in the text format
 - add `owi wat2wasm` subcommand
+- add a `no-assert-failure-expression-printing` flag to `owi c`, `owi sym` and `owi conc`
 
 ## 0.2 - 2024-04-24
 

example/c/README.md

@@ -464,6 +464,9 @@ OPTIONS
        -m VAL, --arch=VAL (absent=32)
            data model
 
+       --no-assert-failure-expression-printing
+           do not display the expression in the assert failure
+
        --no-stop-at-failure
            do not stop when a program failure is encountered
 

example/conc/README.md

@@ -59,6 +59,9 @@ OPTIONS
        --fail-on-trap-only
            ignore assertion violations and only report traps
 
+       --no-assert-failure-expression-printing
+           do not display the expression in the assert failure
+
        --no-stop-at-failure
            do not stop when a program failure is encountered
 

example/sym/README.md

@@ -63,6 +63,9 @@ OPTIONS
        --fail-on-trap-only
            ignore assertion violations and only report traps
 
+       --no-assert-failure-expression-printing
+           do not display the expression in the assert failure
+
        --no-stop-at-failure
            do not stop when a program failure is encountered
 

src/bin/owi.ml

@@ -70,6 +70,11 @@ let no_values =
   let doc = "do not display a value for each symbol" in
   Cmdliner.Arg.(value & flag & info [ "no-value" ] ~doc)
 
+let no_assert_failure_expression_printing =
+  let doc = "do not display the expression in the assert failure" in
+  Cmdliner.Arg.(
+    value & flag & info [ "no-assert-failure-expression-printing" ] ~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
@@ -185,8 +190,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 $ fail_mode
-      $ concolic $ eacsl $ solver )
+      $ no_stop_at_failure $ no_values $ no_assert_failure_expression_printing
+      $ deterministic_result_order $ fail_mode $ concolic $ eacsl $ solver )
 
 let fmt_cmd =
   let open Cmdliner in
@@ -264,7 +269,8 @@ let sym_cmd =
   Cmd.v info
     Term.(
       const Cmd_sym.cmd $ profiling $ debug $ unsafe $ rac $ srac $ optimize
-      $ workers $ no_stop_at_failure $ no_values $ deterministic_result_order
+      $ workers $ no_stop_at_failure $ no_values
+      $ no_assert_failure_expression_printing $ deterministic_result_order
       $ fail_mode $ workspace $ solver $ files )
 
 let conc_cmd =
@@ -277,7 +283,8 @@ let conc_cmd =
   Cmd.v info
     Term.(
       const Cmd_conc.cmd $ profiling $ debug $ unsafe $ rac $ srac $ optimize
-      $ workers $ no_stop_at_failure $ no_values $ deterministic_result_order
+      $ workers $ no_stop_at_failure $ no_values
+      $ no_assert_failure_expression_printing $ deterministic_result_order
       $ fail_mode $ workspace $ solver $ files )
 
 let wasm2wat_cmd =

src/cmd/cmd_c.ml

@@ -185,7 +185,8 @@ 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 fail_mode concolic eacsl solver : unit Result.t =
+  no_assert_failure_expression_printing deterministic_result_order fail_mode
+  concolic eacsl solver : unit Result.t =
   let workspace = Fpath.v workspace in
   let includes = libc_location @ includes in
   let* (_exists : bool) = OS.Dir.create ~path:true workspace in
@@ -196,4 +197,5 @@ 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 false false optimize workers no_stop_at_failure
-    no_values deterministic_result_order fail_mode workspace solver files
+    no_values no_assert_failure_expression_printing deterministic_result_order
+    fail_mode workspace solver files

src/cmd/cmd_c.mli

@@ -18,6 +18,7 @@ val cmd :
   -> bool
   -> bool
   -> bool
+  -> bool
   -> Cmd_sym.fail_mode
   -> bool
   -> bool

src/cmd/cmd_conc.ml

@@ -416,8 +416,8 @@ let run 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 rac srac optimize _workers _no_stop_at_failure
-  no_values _deterministic_result_order _fail_mode (workspace : Fpath.t) solver
-  files =
+  no_values no_assert_failure_expression_printing _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 *)
@@ -460,7 +460,13 @@ let cmd profiling debug unsafe rac srac optimize _workers _no_stop_at_failure
     Error (`Found_bug 1)
   | Some (`Assert_fail, { assignments; _ }) ->
     let assignments = List.rev assignments in
-    Fmt.pr "Assert failure@\n";
+    if no_assert_failure_expression_printing then begin
+      Fmt.pr "Assert failure@\n"
+    end
+    else begin
+      (* TODO: print the assert failure expression ! *)
+      Fmt.pr "Assert failure@\n"
+    end;
     Fmt.pr "Model:@\n  @[<v>%a@]@."
       (Concolic_choice.pp_assignments ~no_values)
       assignments;

src/cmd/cmd_conc.mli

@@ -13,6 +13,7 @@ val cmd :
   -> bool
   -> bool
   -> bool
+  -> bool
   -> Cmd_sym.fail_mode
   -> Fpath.t
   -> Smtml.Solver_dispatcher.solver_type

src/cmd/cmd_sym.ml

@@ -47,8 +47,8 @@ let run_file ~unsafe ~rac ~srac ~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 rac srac optimize workers no_stop_at_failure
-  no_values deterministic_result_order fail_mode (workspace : Fpath.t) solver
-  files =
+  no_values no_assert_failure_expression_printing 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 *)
@@ -87,7 +87,12 @@ let cmd profiling debug unsafe rac srac optimize workers no_stop_at_failure
       Fmt.pr "Trap: %s@\n" (Trap.to_string tr);
       Fmt.pr "Model:@\n  @[<v>%a@]@." (Smtml.Model.pp ~no_values) model
     | `EAssert (assertion, model) ->
-      Fmt.pr "Assert failure: %a@\n" Expr.pp assertion;
+      if no_assert_failure_expression_printing then begin
+        Fmt.pr "Assert failure@\n"
+      end
+      else begin
+        Fmt.pr "Assert failure: %a@\n" Expr.pp assertion
+      end;
       Fmt.pr "Model:@\n  @[<v>%a@]@." (Smtml.Model.pp ~no_values) model
   in
   let rec print_and_count_failures count_acc results =

src/cmd/cmd_sym.mli

@@ -19,6 +19,7 @@ val cmd :
   -> bool
   -> bool
   -> bool
+  -> bool
   -> fail_mode
   -> Fpath.t
   -> Smtml.Solver_dispatcher.solver_type

test/c/eacsl/ghost/else.t

@@ -1,4 +1,7 @@
-  $ owi c --e-acsl ./else.c --no-value 2>1 | grep -v "Assert failure"
+  $ owi c --e-acsl ./else.c --no-value --no-assert-failure-expression-printing
+  Assert failure
   Model:
     (model
       (symbol_0 i32))
+  Reached problem!
+  [13]