diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index eee9988ed..2676dffaa 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -60,7 +60,7 @@ BMC::BMC( #endif } -void BMC::analyze(SourceUnit const& _source, map> _solvedTargets) +void BMC::analyze(SourceUnit const& _source, map, smt::EncodingContext::IdCompare> _solvedTargets) { if (m_interface->solvers() == 0) { @@ -84,8 +84,21 @@ void BMC::analyze(SourceUnit const& _source, map 0 && !m_settings.showUnproved) + m_errorReporter.warning( + 2788_error, + {}, + "BMC: " + + to_string(m_unprovedAmt) + + " verification condition(s) could not be proved." + + " Enable the model checker option \"show unproved\" to see all of them." + + " Consider choosing a specific contract to be verified in order to reduce the solving problems." + + " Consider increasing the timeout per query." + ); } // If this check is true, Z3 and CVC4 are not available @@ -961,8 +974,12 @@ void BMC::checkCondition( case smtutil::CheckResult::UNSATISFIABLE: break; case smtutil::CheckResult::UNKNOWN: - m_errorReporter.warning(_errorMightHappen, _location, "BMC: " + _description + " might happen here.", secondaryLocation); + { + ++m_unprovedAmt; + if (m_settings.showUnproved) + m_errorReporter.warning(_errorMightHappen, _location, "BMC: " + _description + " might happen here.", secondaryLocation); break; + } case smtutil::CheckResult::CONFLICTING: m_errorReporter.warning(1584_error, _location, "BMC: At least two SMT solvers provided conflicting answers. Results might not be sound."); break; diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index c1b89347c..a256dbf09 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -66,7 +66,7 @@ public: langutil::CharStreamProvider const& _charStreamProvider ); - void analyze(SourceUnit const& _sources, std::map> _solvedTargets); + void analyze(SourceUnit const& _sources, std::map, smt::EncodingContext::IdCompare> _solvedTargets); /// This is used if the SMT solver is not directly linked into this binary. /// @returns a list of inputs to the SMT solver that were not part of the argument to @@ -192,7 +192,10 @@ private: std::vector m_verificationTargets; /// Targets that were already proven. - std::map> m_solvedTargets; + std::map, smt::EncodingContext::IdCompare> m_solvedTargets; + + /// Number of verification conditions that could not be proved. + size_t m_unprovedAmt = 0; }; } diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 00657922d..7cc963956 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -933,6 +933,7 @@ void CHC::resetSourceAnalysis() { m_safeTargets.clear(); m_unsafeTargets.clear(); + m_unprovedTargets.clear(); m_functionTargetIds.clear(); m_verificationTargets.clear(); m_queryPlaceholders.clear(); @@ -1594,6 +1595,32 @@ void CHC::checkVerificationTargets() checkedErrorIds.insert(target.errorId); } + auto toReport = m_unsafeTargets; + if (m_settings.showUnproved) + for (auto const& [node, targets]: m_unprovedTargets) + for (auto const& [target, info]: targets) + toReport[node].emplace(target, info); + + for (auto const& [node, targets]: toReport) + for (auto const& [target, info]: targets) + m_errorReporter.warning( + info.error, + info.location, + info.message + ); + + if (!m_settings.showUnproved && !m_unprovedTargets.empty()) + m_errorReporter.warning( + 5840_error, + {}, + "CHC: " + + to_string(m_unprovedTargets.size()) + + " verification condition(s) could not be proved." + + " Enable the model checker option \"show unproved\" to see all of them." + + " Consider choosing a specific contract to be verified in order to reduce the solving problems." + + " Consider increasing the timeout per query." + ); + // There can be targets in internal functions that are not reachable from the external interface. // These are safe by definition and are not even checked by the CHC engine, but this information // must still be reported safe by the BMC engine. @@ -1633,27 +1660,26 @@ void CHC::checkAndReportTarget( else if (result == CheckResult::SATISFIABLE) { solAssert(!_satMsg.empty(), ""); - m_unsafeTargets[_target.errorNode].insert(_target.type); auto cex = generateCounterexample(model, error().name); if (cex) - m_errorReporter.warning( + m_unsafeTargets[_target.errorNode][_target.type] = { _errorReporterId, location, "CHC: " + _satMsg + "\nCounterexample:\n" + *cex - ); + }; else - m_errorReporter.warning( + m_unsafeTargets[_target.errorNode][_target.type] = { _errorReporterId, location, "CHC: " + _satMsg - ); + }; } else if (!_unknownMsg.empty()) - m_errorReporter.warning( + m_unprovedTargets[_target.errorNode][_target.type] = { _errorReporterId, location, "CHC: " + _unknownMsg - ); + }; } /** diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 3aab9268d..f2e8f62a1 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -39,6 +39,8 @@ #include +#include + #include #include @@ -62,8 +64,14 @@ public: void analyze(SourceUnit const& _sources); - std::map> const& safeTargets() const { return m_safeTargets; } - std::map> const& unsafeTargets() const { return m_unsafeTargets; } + struct ReportTargetInfo + { + langutil::ErrorId error; + langutil::SourceLocation location; + std::string message; + }; + std::map, smt::EncodingContext::IdCompare> const& safeTargets() const { return m_safeTargets; } + std::map, smt::EncodingContext::IdCompare> const& unsafeTargets() const { return m_unsafeTargets; } /// This is used if the Horn solver is not directly linked into this binary. /// @returns a list of inputs to the Horn solver that were not part of the argument to @@ -347,10 +355,12 @@ private: /// Helper mapping unique IDs to actual verification targets. std::map m_verificationTargets; - /// Targets proven safe. - std::map> m_safeTargets; - /// Targets proven unsafe. - std::map> m_unsafeTargets; + /// Targets proved safe. + std::map, smt::EncodingContext::IdCompare> m_safeTargets; + /// Targets proved unsafe. + std::map, smt::EncodingContext::IdCompare> m_unsafeTargets; + /// Targets not proved. + std::map, smt::EncodingContext::IdCompare> m_unprovedTargets; //@} /// Control-flow. diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index 1aac80248..9b304f8ea 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -120,8 +120,8 @@ void ModelChecker::analyze(SourceUnit const& _source) m_chc.analyze(_source); auto solvedTargets = m_chc.safeTargets(); - for (auto const& target: m_chc.unsafeTargets()) - solvedTargets[target.first] += target.second; + for (auto const& [node, targets]: m_chc.unsafeTargets()) + solvedTargets[node] += targets | ranges::views::keys; if (m_settings.engine.bmc) m_bmc.analyze(_source, solvedTargets); diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h index edd8f0800..ff39ddc9f 100644 --- a/libsolidity/formal/ModelCheckerSettings.h +++ b/libsolidity/formal/ModelCheckerSettings.h @@ -113,6 +113,7 @@ struct ModelCheckerSettings { ModelCheckerContracts contracts = ModelCheckerContracts::Default(); ModelCheckerEngine engine = ModelCheckerEngine::None(); + bool showUnproved = false; smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All(); ModelCheckerTargets targets = ModelCheckerTargets::Default(); std::optional timeout; @@ -123,6 +124,7 @@ struct ModelCheckerSettings return contracts == _other.contracts && engine == _other.engine && + showUnproved == _other.showUnproved && solvers == _other.solvers && targets == _other.targets && timeout == _other.timeout; diff --git a/test/tools/fuzzer_common.cpp b/test/tools/fuzzer_common.cpp index ef85288b0..65749a009 100644 --- a/test/tools/fuzzer_common.cpp +++ b/test/tools/fuzzer_common.cpp @@ -20,6 +20,7 @@ #include #include +#include #include @@ -104,6 +105,7 @@ void FuzzerUtil::testCompiler( compiler.setModelCheckerSettings({ frontend::ModelCheckerContracts::Default(), frontend::ModelCheckerEngine::All(), + /*showUnproved=*/false, smtutil::SMTSolverChoice::All(), frontend::ModelCheckerTargets::Default(), /*timeout=*/1