diff --git a/regression/cbmc-concurrency/fatal_assertion_thread1/main.c b/regression/cbmc-concurrency/fatal_assertion_thread1/main.c new file mode 100644 index 000000000000..7d3f9a43949a --- /dev/null +++ b/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; +} diff --git a/regression/cbmc-concurrency/fatal_assertion_thread1/test.desc b/regression/cbmc-concurrency/fatal_assertion_thread1/test.desc new file mode 100644 index 000000000000..80534c1bb10c --- /dev/null +++ b/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. diff --git a/regression/cbmc/Division4/main.c b/regression/cbmc/Division4/main.c new file mode 100644 index 000000000000..ba78a836ee6a --- /dev/null +++ b/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; +} diff --git a/regression/cbmc/Division4/test.desc b/regression/cbmc/Division4/test.desc new file mode 100644 index 000000000000..fc7242f9f731 --- /dev/null +++ b/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. diff --git a/regression/cbmc/Memory_leak_abort/test.desc b/regression/cbmc/Memory_leak_abort/test.desc index 7c77b3769c13..20b258da7e31 100644 --- a/regression/cbmc/Memory_leak_abort/test.desc +++ b/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 diff --git a/src/goto-checker/fatal_assertions.cpp b/src/goto-checker/fatal_assertions.cpp index ddc9e3af869f..f5930f428194 100644 --- a/src/goto-checker/fatal_assertions.cpp +++ b/src/goto-checker/fatal_assertions.cpp @@ -16,7 +16,9 @@ Author: Daniel Kroening, dkr@amazon.com #include #include +#include #include +#include struct function_loc_pairt { @@ -58,25 +60,64 @@ struct function_loc_pair_hasht using loc_sett = std::unordered_set; +/// The call sites of each function that is called directly. +static std::unordered_map> +call_sites(const goto_functionst &goto_functions) +{ + std::unordered_map> 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 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> 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,6 +178,12 @@ 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) @@ -118,6 +191,7 @@ void propagate_fatal_to_proven( // 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); diff --git a/src/goto-checker/fatal_assertions.h b/src/goto-checker/fatal_assertions.h index 89baf01263be..25b7850c902f 100644 --- a/src/goto-checker/fatal_assertions.h +++ b/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