introduce 'fatal assertions'

This introduces a variant of ASSERT instructions that are fatal when they
are refuted.  Execution paths through fatal assertions that are refuted are
undefined.  Assertions that (otherwise) pass and that are reachable from a
refuted fatal assertion are now reported as UNKNOWN.

The motivating use-case for fatal assertions is undefined behavior in
languages such as C/C++ or Rust.

Author: kroening

jbmc/regression/jbmc-strings/StringFormatString/test-string1-length.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test
 --function Test.string1Length --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$

jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test
 --function Test.checkMinLength --string-non-empty --max-nondet-string-length 2147483647
 ^EXIT=10$

regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc

@@ -2,7 +2,7 @@ CORE
 div_by_zero.c
 --div-by-zero-check --trace
 \[main\.division-by-zero\.1\] line \d division by zero in x / y: FAILURE
-\[main\.division-by-zero\.2\] line \d+ division by zero in x / z: SUCCESS
+\[main\.division-by-zero\.2\] line \d+ division by zero in x / z: UNKNOWN
 y=0
 ^VERIFICATION FAILED$
 ^EXIT=10$

regression/cbmc/Division3/main.c

@@ -0,0 +1,18 @@
+_Bool nondet_bool();
+
+void main()
+{
+  __CPROVER_assert(0, "non-fatal assertion");
+
+  if(nondet_bool())
+  {
+    int divisor = nondet_bool() ? 2 : 0;
+
+    // possible division by zero
+    int result = 10 / divisor;
+
+    __CPROVER_assert(divisor == 2 || divisor == 0, "divisor value");
+  }
+  else
+    __CPROVER_assert(0, "independent assertion");
+}

regression/cbmc/Division3/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line 5 non-fatal assertion: FAILURE$
+^\[main\.division-by-zero\.1\] line 12 division by zero in 10 / divisor: FAILURE$
+^\[main\.assertion\.2\] line 14 divisor value: UNKNOWN$
+^\[main\.assertion\.3\] line 17 independent assertion: FAILURE$
+^\*\* 3 of 4 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/pragma_cprover_enable_all/test.desc

@@ -8,22 +8,22 @@ main.c
 ^\[main\.float-division-by-zero\.\d+\] line 87 floating-point division by zero in x / den: FAILURE
 ^\[main\.overflow\.\d+\] line 87 arithmetic overflow on floating-point division in x / den: FAILURE
 ^\[main\.division-by-zero\.\d+\] line 88 division by zero in 10 / 0: FAILURE$
-^\[main\.enum-range-check\.\d+\] line 89 enum range check in \(ABC\)10: FAILURE
-^\[main\.overflow\.\d+\] line 90 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
-^\[main\.overflow\.\d+\] line 91 arithmetic overflow on signed \+ in k \+ 1: FAILURE
+^\[main\.enum-range-check\.\d+\] line 89 enum range check in \(ABC\)10: UNKNOWN$
+^\[main\.overflow\.\d+\] line 90 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): UNKNOWN$
+^\[main\.overflow\.\d+\] line 91 arithmetic overflow on signed \+ in k \+ 1: UNKNOWN$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
-^\[main\.pointer_primitives\.\d+\] line 41 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
-^\[main\.pointer_primitives\.\d+\] line 41 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
-^\[main\.pointer_arithmetic\.\d+\] line 42 pointer arithmetic: pointer outside object bounds in p \+ .*2000000000000(l|ll): FAILURE
-^\[main\.NaN\.\d+\] line 48 NaN on / in x / den: FAILURE
-^\[main\.float-division-by-zero\.\d+\] line 49 floating-point division by zero in x / den: FAILURE
-^\[main\.overflow\.\d+\] line 48 arithmetic overflow on floating-point division in x / den: FAILURE
-^\[main\.division-by-zero\.\d+\] line 48 division by zero in 10 / 0: FAILURE$
-^\[main\.enum-range-check\.\d+\] line 49 enum range check in \(ABC\)10: FAILURE
-^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE
-^\[main\.overflow\.\d+\] line 51 arithmetic overflow on signed \+ in k \+ 1: FAILURE
+^\[main\.pointer_primitives\.\d+\] line 41 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\):
+^\[main\.pointer_primitives\.\d+\] line 41 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\):
+^\[main\.pointer_arithmetic\.\d+\] line 42 pointer arithmetic: pointer outside object bounds in p \+ .*2000000000000(l|ll):
+^\[main\.NaN\.\d+\] line 48 NaN on / in x / den:
+^\[main\.float-division-by-zero\.\d+\] line 49 floating-point division by zero in x / den:
+^\[main\.overflow\.\d+\] line 48 arithmetic overflow on floating-point division in x / den:
+^\[main\.division-by-zero\.\d+\] line 48 division by zero in 10 / 0:
+^\[main\.enum-range-check\.\d+\] line 49 enum range check in \(ABC\)10:
+^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\):
+^\[main\.overflow\.\d+\] line 51 arithmetic overflow on signed \+ in k \+ 1:
 --
 This test uses all possible named-checks to maximize coverage.

regression/contracts-dfcc/assigns-slice-targets/test-replace.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main-replace.c
 --dfcc main --replace-call-with-contract foo
 ^\[main.assertion.\d+\].*assertion s.a == 0: SUCCESS$

regression/contracts-dfcc/loop_assigns-slice-from/test.desc

@@ -1,4 +1,4 @@
-CORE dfcc-only
+KNOWNBUG
 main.c
 --no-malloc-may-fail --dfcc main --apply-loop-contracts
 ^EXIT=10$

regression/contracts/loop_assigns-slice-from/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$

regression/symtab2gb/multiple_symtabs/test.desc

@@ -7,4 +7,3 @@ user.json_symtab library.json_symtab
 ^\[2\] file library.adb line \d+ assertion: FAILURE$
 ^VERIFICATION FAILED$
 --
-error

regression/symtab2gb/single_symtab/test.desc

@@ -7,4 +7,3 @@ entry_point.json_symtab
 ^\[2\] file entry_point.adb line \d+ assertion: SUCCESS$
 ^VERIFICATION FAILED$
 --
-error

src/ansi-c/goto_check_c.cpp

@@ -1752,6 +1752,9 @@ void goto_check_ct::add_guarded_property(
     }
     else
     {
+      if(property_class == "division-by-zero")
+        annotated_location.property_fatal(true);
+
       new_code.add(goto_programt::make_assertion(
         std::move(guarded_expr), annotated_location));
     }

src/goto-checker/Makefile

@@ -1,11 +1,12 @@
 SRC = bmc_util.cpp \
       counterexample_beautification.cpp \
       cover_goals_report_util.cpp \
-      incremental_goto_checker.cpp \
+      fatal_assertions.cpp \
       goto_symex_fault_localizer.cpp \
       goto_symex_property_decider.cpp \
       goto_trace_storage.cpp \
       goto_verifier.cpp \
+      incremental_goto_checker.cpp \
       multi_path_symex_checker.cpp \
       multi_path_symex_only_checker.cpp \
       properties.cpp \

src/goto-checker/all_properties_verifier_with_trace_storage.h

@@ -12,10 +12,12 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_TRACE_STORAGE_H
 #define CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_TRACE_STORAGE_H
 
-#include "goto_verifier.h"
+#include <goto-programs/abstract_goto_model.h>
 
 #include "bmc_util.h"
+#include "fatal_assertions.h"
 #include "goto_trace_storage.h"
+#include "goto_verifier.h"
 #include "incremental_goto_checker.h"
 #include "properties.h"
 #include "report_util.h"
@@ -44,24 +46,23 @@ class all_properties_verifier_with_trace_storaget : public goto_verifiert
       if(result.progress == incremental_goto_checkert::resultt::progresst::DONE)
         break;
 
-      // we've got an error trace
-      if(options.get_bool_option("trace"))
+      message_building_error_trace(log);
+      for(const auto &property_id : result.updated_properties)
       {
-        message_building_error_trace(log);
-        for(const auto &property_id : result.updated_properties)
+        if(properties.at(property_id).status == property_statust::FAIL)
         {
-          if(properties.at(property_id).status == property_statust::FAIL)
-          {
-            // get correctly truncated error trace for property and store it
-            (void)traces.insert(
-              incremental_goto_checker.build_trace(property_id));
-          }
+          // get correctly truncated error trace for property and store it
+          (void)traces.insert(
+            incremental_goto_checker.build_trace(property_id));
         }
       }
 
       ++iterations;
     }
 
+    propagate_fatal_assertions(
+      properties, traces, goto_model.get_goto_functions());
+
     return determine_result(properties);
   }