From fa9256fce68654ecbdf86ce5c46c8dc0c7b268c5 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 3 Mar 2024 11:25:28 -0800 Subject: [PATCH] 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. --- src/goto-checker/Makefile | 3 +- src/goto-checker/fatal_assertions.cpp | 130 ++++++++++++++++++++++++++ src/goto-checker/fatal_assertions.h | 27 ++++++ src/util/irep_ids.def | 1 + src/util/source_location.h | 13 +++ 5 files changed, 173 insertions(+), 1 deletion(-) create mode 100644 src/goto-checker/fatal_assertions.cpp create mode 100644 src/goto-checker/fatal_assertions.h diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index cb8243ecbc1f..0750b9d22749 100644 --- a/src/goto-checker/Makefile +++ b/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 \ diff --git a/src/goto-checker/fatal_assertions.cpp b/src/goto-checker/fatal_assertions.cpp new file mode 100644 index 000000000000..a6e3b2756e8c --- /dev/null +++ b/src/goto-checker/fatal_assertions.cpp @@ -0,0 +1,130 @@ +/*******************************************************************\ + +Module: Fatal Assertions + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +/// \file +/// Fatal Assertions + +#include "fatal_assertions.h" + +#include + +#include + +#include +#include + +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_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; + +static void +reachable_fixpoint(loc_sett &locs, const goto_functionst &goto_functions) +{ + std::stack working; + + for(auto loc : locs) + working.push(loc); + + while(!working.empty()) + { + auto loc = working.top(); + working.pop(); + locs.insert(loc); + + if(loc.target->is_function_call()) + { + } + else + { + auto &body = loc.function_it->second.body; + + for(auto successor : body.get_successors(loc.target)) + working.emplace(loc.function_it, successor); + } + } +} + +void propagate_fatal_assertions( + 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. + reachable_fixpoint(fatal_locs, goto_functions); + + // Now mark PASS assertions as UNKNOWN. + for(auto &loc : fatal_locs) + { + 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; + } + } + } +} diff --git a/src/goto-checker/fatal_assertions.h b/src/goto-checker/fatal_assertions.h new file mode 100644 index 000000000000..b8017ba208b9 --- /dev/null +++ b/src/goto-checker/fatal_assertions.h @@ -0,0 +1,27 @@ +/*******************************************************************\ + +Module: Fatal Assertions + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +/// \file +/// Fatal Assertions + +#ifndef CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H +#define CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H + +#include "properties.h" + +/// Assertions after fatal assertions that are +/// refuted do not have meaning, and passing ones +/// are marked as UNKNOWN. +/// Assertions that are independently refuted are left +/// in that state, even though the counterexample +/// might be invalid. +/// This avoids ambiguity if two refuted fatal asserions +/// may reach each other. +void propagate_fatal_assertions(propertiest &, const abstract_goto_modelt &); + +#endif // CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index eea285397a5c..8773149eb2a9 100644 --- a/src/util/irep_ids.def +++ b/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) diff --git a/src/util/source_location.h b/src/util/source_location.h index fe99c578fb3a..1f4373f14f9b 100644 --- a/src/util/source_location.h +++ b/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);