Built-in checks can optionally be fatal

With a new option --assert-then-assume each built-in check (assertion) is followed by an assumption. For Kani, this will enable more consistent behaviour, and it may give us an additional way to produce "fatal assertions" as proposed in diffblue#8226.
tautschnig · Mar 15, 2024 · eb48d8b · eb48d8b
1 parent 689c552
commit eb48d8b
Show file tree

Hide file tree

Showing 10 changed files with 63 additions and 9 deletions.
diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1
@@ -304,6 +304,9 @@ ignore user assumptions
 \fB\-\-assert\-to\-assume\fR
 convert user assertions to assumptions
 .TP
+\fB\-\-assert\-then\-assume\fR
+follow each inserted check by an assumption
+.TP
 \fB\-\-cover\fR CC
 create test\-suite with coverage criterion CC,
 where CC is one of assertion[s], assume[s],

diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1
@@ -568,6 +568,9 @@ ignore user assumptions
 \fB\-\-assert\-to\-assume\fR
 convert user assertions to assumptions
 .TP
+\fB\-\-assert\-then\-assume\fR
+follow each inserted check by an assumption
+.TP
 \fB\-\-malloc\-may\-fail\fR
 allow malloc calls to return a null pointer
 .TP

diff --git a/doc/man/goto-diff.1 b/doc/man/goto-diff.1
@@ -99,6 +99,9 @@ ignore user assumptions
 \fB\-\-assert\-to\-assume\fR
 convert user assertions to assumptions
 .TP
+\fB\-\-assert\-then\-assume\fR
+follow each inserted check by an assumption
+.TP
 \fB\-\-cover\fR CC
 create test\-suite with coverage criterion CC,
 where CC is one of assertion[s], assume[s],

diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1
@@ -239,6 +239,9 @@ ignore user assumptions
 \fB\-\-assert\-to\-assume\fR
 convert user assertions to assumptions
 .TP
+\fB\-\-assert\-then\-assume\fR
+follow each inserted check by an assumption
+.TP
 \fB\-\-uninitialized\-check\fR
 add checks for uninitialized locals (experimental)
 .TP

diff --git a/regression/cbmc/assert-then-assume/main.c b/regression/cbmc/assert-then-assume/main.c
@@ -0,0 +1,9 @@
+int nondet_int();
+
+int main()
+{
+  int x;
+  int *p = nondet_int() ? (int *)0 : &x;
+  *p = 42;
+  __CPROVER_assert(x == 42, "cannot fail with assert-to-assume");
+}
diff --git a/regression/cbmc/assert-then-assume/test.desc b/regression/cbmc/assert-then-assume/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--assert-then-assume
+^\[main.pointer_dereference.1\] line 7 dereference failure: pointer NULL in \*p: FAILURE$
+^\[main.assertion.1\] line 8 cannot fail with assert-to-assume: SUCCESS$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
diff --git a/regression/cbmc/assert-to-assume/main.c b/regression/cbmc/assert-to-assume/main.c
@@ -0,0 +1,9 @@
+int nondet_int();
+
+int main()
+{
+  int x;
+  int *p = nondet_int() ? (int *)0 : &x;
+  *p = 42;
+  __CPROVER_assert(x == 42, "cannot fail with assert-to-assume");
+}
diff --git a/regression/cbmc/assert-to-assume/test.desc b/regression/cbmc/assert-to-assume/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--assert-to-assume
+^\[main.assertion.1\] line 8 cannot fail with assert-to-assume: SUCCESS$
+^\*\* 0 of 1 failed
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp
@@ -74,6 +74,7 @@ class goto_check_ct
     enable_nan_check = _options.get_bool_option("nan-check");
     retain_trivial = _options.get_bool_option("retain-trivial-checks");
     enable_assert_to_assume = _options.get_bool_option("assert-to-assume");
+    enable_assert_then_assume = _options.get_bool_option("assert-then-assume");
     error_labels = _options.get_list_option("error-label");
     enable_pointer_primitive_check =
       _options.get_bool_option("pointer-primitive-check");
@@ -273,6 +274,7 @@ class goto_check_ct
   bool enable_nan_check;
   bool retain_trivial;
   bool enable_assert_to_assume;
+  bool enable_assert_then_assume;
   bool enable_pointer_primitive_check;
 
   /// Maps a named-check name to the corresponding boolean flag.
@@ -1719,14 +1721,14 @@ void goto_check_ct::add_guarded_property(
 
     add_all_checked_named_check_pragmas(annotated_location);
 
-    if(enable_assert_to_assume)
+    if(!enable_assert_to_assume)
     {
-      new_code.add(goto_programt::make_assumption(
+      new_code.add(goto_programt::make_assertion(
         std::move(guarded_expr), annotated_location));
     }
-    else
+    if(enable_assert_to_assume || enable_assert_then_assume)
     {
-      new_code.add(goto_programt::make_assertion(
+      new_code.add(goto_programt::make_assumption(
         std::move(guarded_expr), annotated_location));
     }
   }
@@ -2082,15 +2084,15 @@ void goto_check_ct::goto_check(
         annotated_location.set_comment("error label " + label);
         annotated_location.set("user-provided", true);
 
-        if(enable_assert_to_assume)
+        if(!enable_assert_to_assume)
         {
           new_code.add(
-            goto_programt::make_assumption(false_exprt{}, annotated_location));
+            goto_programt::make_assertion(false_exprt{}, annotated_location));
         }
-        else
+        if(enable_assert_to_assume || enable_assert_then_assume)
         {
           new_code.add(
-            goto_programt::make_assertion(false_exprt{}, annotated_location));
+            goto_programt::make_assumption(false_exprt{}, annotated_location));
         }
       }
     }

diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h
@@ -48,6 +48,7 @@ void goto_check_c(
   "(error-label):"                                                             \
   "(no-assertions)(no-assumptions)"                                            \
   "(assert-to-assume)"                                                         \
+  "(assert-then-assume)"                                                       \
   "(no-bounds-check)(no-pointer-check)(no-signed-overflow-check)"              \
   "(no-pointer-primitive-check)(no-undefined-shift-check)"                     \
   "(no-div-by-zero-check)"
@@ -91,7 +92,8 @@ void goto_check_c(
   " {y--no-built-in-assertions} \t ignore assertions in built-in library\n"    \
   " {y--no-assertions} \t ignore user assertions\n"                            \
   " {y--no-assumptions} \t ignore user assumptions\n"                          \
-  " {y--assert-to-assume} \t convert user assertions to assumptions\n"
+  " {y--assert-to-assume} \t convert user assertions to assumptions\n"         \
+  " {y--assert-then-assume} \t follow each inserted check by an assumption\n"
 // clang-format on
 
 #define PARSE_OPTION_OVERRIDE(cmdline, options, option)                        \
@@ -117,6 +119,7 @@ void goto_check_c(
   options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("assumptions", !cmdline.isset("no-assumptions")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("assert-then-assume", cmdline.isset("assert-then-assume")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \
   if(cmdline.isset("error-label")) \
     options.set_option("error-label", cmdline.get_values("error-label"));      \