Fatal assertions: also propagate to callers and other threads

regression/cbmc-concurrency/fatal_assertion_thread1/main.c

@@ -0,0 +1,28 @@
+int shared;
+int other;
+
+void worker(void)
+{
+  int divisor = shared;
+  // division by zero: undefined behaviour in this thread
+  shared = 10 / divisor;
+}
+
+void bystander(void)
+{
+  // may run after the undefined behaviour in the worker thread
+  __CPROVER_assert(other == 0, "bystander");
+}
+
+int main()
+{
+  __CPROVER_assert(other == 0, "before any thread");
+__CPROVER_ASYNC_1:
+  bystander();
+__CPROVER_ASYNC_2:
+  worker();
+  // not reachable from the worker thread, but may run after its undefined
+  // behaviour
+  __CPROVER_assert(other == 0, "after the spawn");
+  return 0;
+}

regression/cbmc-concurrency/fatal_assertion_thread1/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--div-by-zero-check
+^EXIT=10$
+^SIGNAL=0$
+^\[worker\.division-by-zero\.1\] line 8 division by zero in 10 / divisor: FAILURE$
+^\[main\.assertion\.1\] line 19 before any thread: SUCCESS$
+^\[main\.assertion\.2\] line 26 after the spawn: UNKNOWN$
+^\[bystander\.assertion\.1\] line 14 bystander: UNKNOWN$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+A refuted fatal assertion (here: undefined behaviour) in one thread makes
+proven properties in all threads UNKNOWN, including code that does not follow
+it in the control-flow graph: the bystander thread and the code of main after
+the spawn. Code that runs before any thread starts keeps its status.

regression/cbmc/Division4/main.c

@@ -0,0 +1,15 @@
+int other;
+
+void f(int divisor)
+{
+  // possible division by zero
+  int result = 10 / divisor;
+}
+
+int main()
+{
+  int divisor;
+  f(divisor);
+  __CPROVER_assert(other == 0, "after the return");
+  return 0;
+}

regression/cbmc/Division4/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[f\.division-by-zero\.1\] line 6 division by zero in 10 / divisor: FAILURE$
+^\[main\.assertion\.1\] line 13 after the return: UNKNOWN$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Code that runs after a return from the function holding a refuted fatal
+assertion is affected by it, too.

regression/cbmc/Memory_leak_abort/test.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 _Exit\.memory-leak\.1.*FAILURE
-__CPROVER__start\.memory-leak\.1.*SUCCESS
+__CPROVER__start\.memory-leak\.1.*UNKNOWN
 abort\.memory-leak\.1.*FAILURE
 exit\.memory-leak\.1.*FAILURE
 main\.memory-leak\.1.*FAILURE

src/goto-checker/fatal_assertions.cpp

@@ -16,7 +16,9 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <goto-programs/goto_functions.h>
 
 #include <stack>
+#include <unordered_map>
 #include <unordered_set>
+#include <vector>
 
 struct function_loc_pairt
 {
@@ -58,25 +60,64 @@ struct function_loc_pair_hasht
 using loc_sett =
   std::unordered_set<function_loc_pairt, function_loc_pair_hasht>;
 
+/// The call sites of each function that is called directly.
+static std::unordered_map<irep_idt, std::vector<function_loc_pairt>>
+call_sites(const goto_functionst &goto_functions)
+{
+  std::unordered_map<irep_idt, std::vector<function_loc_pairt>> result;
+
+  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_function_call() && target->call_function().id() == ID_symbol)
+      {
+        result[to_symbol_expr(target->call_function()).get_identifier()]
+          .emplace_back(function_it, target);
+      }
+    }
+  }
+
+  return result;
+}
+
+/// All locations that may execute after any of \p locs: their successors,
+/// the bodies of the functions they call, and, when the end of the function
+/// holding one of \p locs is reached, the continuations of all its call sites
+/// (and so on transitively). A callee entered through a call returns to that
+/// call only, whose continuation is added at the call.
 static loc_sett
 reachable_fixpoint(const loc_sett &locs, const goto_functionst &goto_functions)
 {
-  // frontier set
-  std::stack<function_loc_pairt> working;
+  const auto callers = call_sites(goto_functions);
+
+  // frontier set, with whether the calling context is unknown: if it is, the
+  // end of the function returns to any of its call sites
+  std::stack<std::pair<function_loc_pairt, bool>> working;
 
   for(auto loc : locs)
-    working.push(loc);
+    working.emplace(loc, true);
 
   loc_sett fixpoint;
+  loc_sett any_caller;
 
   while(!working.empty())
   {
-    auto loc = working.top();
+    auto loc = working.top().first;
+    const bool unknown_context = working.top().second;
     working.pop();
 
-    auto insertion_result = fixpoint.insert(loc);
-    if(!insertion_result.second)
-      continue; // seen already
+    bool seen = !fixpoint.insert(loc).second;
+    if(unknown_context)
+      seen = !any_caller.insert(loc).second;
+    if(seen)
+      continue;
 
     if(loc.target->is_function_call())
     {
@@ -89,20 +130,46 @@ reachable_fixpoint(const loc_sett &locs, const goto_functionst &goto_functions)
         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());
+        if(!function_iterator->second.body.instructions.empty())
+        {
+          working.emplace(
+            function_loc_pairt{
+              function_iterator,
+              function_iterator->second.body.instructions.begin()},
+            false);
+        }
       }
 
       // add the next location to the working set
-      working.emplace(loc.function_it, std::next(loc.target));
+      working.emplace(
+        function_loc_pairt{loc.function_it, std::next(loc.target)},
+        unknown_context);
+    }
+    else if(loc.target->is_end_function())
+    {
+      // with an unknown calling context, execution continues after any call
+      // site of this function
+      auto callers_it = callers.find(loc.function_it->first);
+      if(unknown_context && callers_it != callers.end())
+      {
+        for(const auto &call_site : callers_it->second)
+        {
+          working.emplace(
+            function_loc_pairt{
+              call_site.function_it, std::next(call_site.target)},
+            true);
+        }
+      }
     }
     else
     {
       auto &body = loc.function_it->second.body;
 
       for(auto successor : body.get_successors(loc.target))
-        working.emplace(loc.function_it, successor);
+      {
+        working.emplace(
+          function_loc_pairt{loc.function_it, successor}, unknown_context);
+      }
     }
   }
 
@@ -111,13 +178,20 @@ reachable_fixpoint(const loc_sett &locs, const goto_functionst &goto_functions)
 
 /// Proven assertions after refuted fatal assertions
 /// are marked as UNKNOWN.
+///
+/// In a multi-threaded program, code that does not follow a refuted fatal
+/// assertion in the control-flow graph can still run after it: the code of
+/// other threads. Any such code is reachable from some START_THREAD
+/// instruction, because at least two threads exist at that point. We then
+/// also start from every START_THREAD instruction.
 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;
+  loc_sett thread_starts;
 
   for(auto function_it = goto_functions.function_map.begin();
       function_it != goto_functions.function_map.end();
@@ -140,9 +214,14 @@ void propagate_fatal_to_proven(
           fatal_locs.emplace(function_it, target);
         }
       }
+      else if(target->is_start_thread())
+        thread_starts.emplace(function_it, target);
     }
   }
 
+  if(!fatal_locs.empty())
+    fatal_locs.insert(thread_starts.begin(), thread_starts.end());
+
   // Saturate fixpoint.
   auto fixpoint = reachable_fixpoint(fatal_locs, goto_functions);
 

src/goto-checker/fatal_assertions.h

@@ -17,7 +17,9 @@ Author: Daniel Kroening, dkr@amazon.com
 class goto_functionst;
 
 /// Proven assertions after refuted fatal assertions
-/// are marked as UNKNOWN.
+/// are marked as UNKNOWN. This includes code that runs after a return from
+/// the function holding a refuted fatal assertion, and, in multi-threaded
+/// programs, the code of all threads.
 void propagate_fatal_assertions(propertiest &, const goto_functionst &);
 
 #endif // CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H