introduce 'fatal assertions'

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: 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$
 ^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.

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"
@@ -62,6 +64,8 @@ class all_properties_verifier_with_trace_storaget : public goto_verifiert
       ++iterations;
     }
 
+    propagate_fatal_assertions(properties, goto_model.get_goto_functions());
+
     return determine_result(properties);
   }
 

src/goto-checker/fatal_assertions.cpp

@@ -0,0 +1,172 @@
+/*******************************************************************\
+
+Module: Fatal Assertions
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Fatal Assertions
+
+#include "fatal_assertions.h"
+
+#include <util/irep_hash.h>
+
+#include <goto-programs/goto_functions.h>
+
+#include <stack>
+#include <unordered_set>
+
+struct function_loc_pairt
+{
+  using function_itt = goto_functionst::function_mapt::const_iterator;
+  function_loc_pairt(
+    function_itt __function_it,
+    goto_programt::const_targett __target)
+    : function_it(__function_it), target(__target)
+  {
+  }
+  function_itt function_it;
+  goto_programt::const_targett target;
+  bool operator==(const function_loc_pairt &other) const
+  {
+    return function_it->first == other.function_it->first &&
+           target == other.target;
+  }
+};
+
+struct function_itt_hasht
+{
+  using function_itt = goto_functionst::function_mapt::const_iterator;
+  std::size_t operator()(const function_itt &function_it) const
+  {
+    return function_it->first.hash();
+  }
+};
+
+struct function_loc_pair_hasht
+{
+  std::size_t operator()(const function_loc_pairt &p) const
+  {
+    auto h1 = p.function_it->first.hash();
+    auto h2 = const_target_hash{}(p.target);
+    return hash_combine(h1, h2);
+  }
+};
+
+using loc_sett =
+  std::unordered_set<function_loc_pairt, function_loc_pair_hasht>;
+
+static loc_sett
+reachable_fixpoint(const loc_sett &locs, const goto_functionst &goto_functions)
+{
+  // frontier set
+  std::stack<function_loc_pairt> working;
+
+  for(auto loc : locs)
+    working.push(loc);
+
+  loc_sett fixpoint;
+
+  while(!working.empty())
+  {
+    auto loc = working.top();
+    working.pop();
+
+    auto insertion_result = fixpoint.insert(loc);
+    if(!insertion_result.second)
+      continue; // seen already
+
+    if(loc.target->is_function_call())
+    {
+      // get the callee
+      auto &function = loc.target->call_function();
+      if(function.id() == ID_symbol)
+      {
+        // add the callee to the working set
+        auto &function_identifier = to_symbol_expr(function).get_identifier();
+        auto function_iterator =
+          goto_functions.function_map.find(function_identifier);
+        CHECK_RETURN(function_iterator != goto_functions.function_map.end());
+        working.emplace(
+          function_iterator,
+          function_iterator->second.body.instructions.begin());
+      }
+
+      // add the next location to the working set
+      working.emplace(loc.function_it, std::next(loc.target));
+    }
+    else
+    {
+      auto &body = loc.function_it->second.body;
+
+      for(auto successor : body.get_successors(loc.target))
+        working.emplace(loc.function_it, successor);
+    }
+  }
+
+  return fixpoint;
+}
+
+/// Proven assertions after refuted fatal assertions
+/// are marked as UNKNOWN.
+void propagate_fatal_to_proven(
+  propertiest &properties,
+  const goto_functionst &goto_functions)
+{
+  // Iterate to find refuted fatal assertions. Anything reachalble
+  // from there is a 'fatal loc'.
+  loc_sett fatal_locs;
+
+  for(auto function_it = goto_functions.function_map.begin();
+      function_it != goto_functions.function_map.end();
+      function_it++)
+  {
+    auto &body = function_it->second.body;
+    for(auto target = body.instructions.begin();
+        target != body.instructions.end();
+        target++)
+    {
+      if(target->is_assert() && target->source_location().property_fatal())
+      {
+        auto id = target->source_location().get_property_id();
+        auto property = properties.find(id);
+        CHECK_RETURN(property != properties.end());
+
+        // Status?
+        if(property->second.status == property_statust::FAIL)
+        {
+          fatal_locs.emplace(function_it, target);
+        }
+      }
+    }
+  }
+
+  // Saturate fixpoint.
+  auto fixpoint = reachable_fixpoint(fatal_locs, goto_functions);
+
+  // Now mark PASS assertions as UNKNOWN.
+  for(auto &loc : fixpoint)
+  {
+    if(loc.target->is_assert())
+    {
+      auto id = loc.target->source_location().get_property_id();
+      auto property = properties.find(id);
+      CHECK_RETURN(property != properties.end());
+
+      // Status?
+      if(property->second.status == property_statust::PASS)
+      {
+        property->second.status = property_statust::UNKNOWN;
+      }
+    }
+  }
+}
+
+void propagate_fatal_assertions(
+  propertiest &properties,
+  const goto_functionst &goto_functions)
+{
+  propagate_fatal_to_proven(properties, goto_functions);
+}

src/goto-checker/fatal_assertions.h

@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: Fatal Assertions
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Fatal Assertions
+
+#ifndef CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H
+#define CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H
+
+#include "properties.h"
+
+class goto_functionst;
+
+/// Proven assertions after refuted fatal assertions
+/// are marked as UNKNOWN.
+void propagate_fatal_assertions(propertiest &, const goto_functionst &);
+
+#endif // CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H

src/util/irep_ids.def

@@ -26,6 +26,7 @@ IREP_ID_ONE(line)
 IREP_ID_ONE(column)
 IREP_ID_ONE(comment)
 IREP_ID_ONE(property_class)
+IREP_ID_ONE(property_fatal)
 IREP_ID_ONE(property_id)
 IREP_ID_ONE(function)
 IREP_ID_ONE(mathematical_function)

src/util/source_location.h

@@ -96,6 +96,11 @@ class source_locationt:public irept
     return find(ID_basic_block_source_lines);
   }
 
+  bool property_fatal() const
+  {
+    return get_bool(ID_property_fatal);
+  }
+
   void set_file(const irep_idt &file)
   {
     set(ID_file, file);
@@ -163,6 +168,14 @@ class source_locationt:public irept
     add(ID_basic_block_source_lines, std::move(source_lines));
   }
 
+  void property_fatal(bool _property_fatal)
+  {
+    if(_property_fatal)
+      set(ID_property_fatal, true);
+    else
+      remove(ID_property_fatal);
+  }
+
   void set_hide()
   {
     set(ID_hide, true);