From 88030c65683f1f425d6d577609f09691a27d7429 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 10 Jul 2020 10:28:49 +0200 Subject: [PATCH] [SMTChecker] Refactor verification targets --- libsolidity/formal/BMC.cpp | 30 +++--- libsolidity/formal/BMC.h | 6 +- libsolidity/formal/CHC.cpp | 141 +++++++++++++++++-------- libsolidity/formal/CHC.h | 31 +++++- libsolidity/formal/EncodingContext.cpp | 10 +- libsolidity/formal/EncodingContext.h | 8 +- libsolidity/formal/ModelChecker.cpp | 7 +- libsolidity/formal/SMTEncoder.cpp | 2 +- 8 files changed, 160 insertions(+), 75 deletions(-) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 8f74dbb3e..921c71ccf 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -52,11 +52,11 @@ BMC::BMC( #endif } -void BMC::analyze(SourceUnit const& _source, set _safeAssertions) +void BMC::analyze(SourceUnit const& _source, map> _solvedTargets) { solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), ""); - m_safeAssertions += move(_safeAssertions); + m_solvedTargets = move(_solvedTargets); m_context.setSolver(m_interface.get()); m_context.clear(); m_context.setAssertionAccumulation(true); @@ -684,16 +684,22 @@ void BMC::checkBalance(BMCVerificationTarget& _target) void BMC::checkAssert(BMCVerificationTarget& _target) { solAssert(_target.type == VerificationTarget::Type::Assert, ""); - if (!m_safeAssertions.count(_target.expression)) - checkCondition( - _target.constraints && !_target.value, - _target.callStack, - _target.modelExpressions, - _target.expression->location(), - 4661_error, - 7812_error, - "Assertion violation" - ); + + if ( + m_solvedTargets.count(_target.expression) && + m_solvedTargets.at(_target.expression).count(_target.type) + ) + return; + + checkCondition( + _target.constraints && !_target.value, + _target.callStack, + _target.modelExpressions, + _target.expression->location(), + 4661_error, + 7812_error, + "Assertion violation" + ); } void BMC::addVerificationTarget( diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 4f0a98023..2eed58101 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -63,7 +63,7 @@ public: smtutil::SMTSolverChoice _enabledSolvers ); - void analyze(SourceUnit const& _sources, std::set _safeAssertions); + void analyze(SourceUnit const& _sources, std::map> _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 @@ -180,8 +180,8 @@ private: std::vector m_verificationTargets; - /// Assertions that are known to be safe. - std::set m_safeAssertions; + /// Targets that were already proven. + std::map> m_solvedTargets; }; } diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index c3e9d6cb4..336dfaa37 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -96,48 +96,7 @@ void CHC::analyze(SourceUnit const& _source) for (auto const* source: sources) source->accept(*this); - for (auto const& [scope, target]: m_verificationTargets) - { - if (target.type == VerificationTarget::Type::Assert) - { - auto assertions = transactionAssertions(scope); - for (auto const* assertion: assertions) - { - createErrorBlock(); - connectBlocks(target.value, error(), target.constraints && (target.errorId == static_cast(assertion->id()))); - auto [result, model] = query(error(), assertion->location()); - // This should be fine but it's a bug in the old compiler - (void)model; - if (result == smtutil::CheckResult::UNSATISFIABLE) - m_safeAssertions.insert(assertion); - } - } - else if (target.type == VerificationTarget::Type::PopEmptyArray) - { - solAssert(dynamic_cast(scope), ""); - createErrorBlock(); - connectBlocks(target.value, error(), target.constraints && (target.errorId == static_cast(scope->id()))); - auto [result, model] = query(error(), scope->location()); - // This should be fine but it's a bug in the old compiler - (void)model; - if (result != smtutil::CheckResult::UNSATISFIABLE) - { - string msg = "Empty array \"pop\" "; - if (result == smtutil::CheckResult::SATISFIABLE) - msg += "detected here."; - else - msg += "might happen here."; - m_unsafeTargets.insert(scope); - m_outerErrorReporter.warning( - 2529_error, - scope->location(), - msg - ); - } - } - else - solAssert(false, ""); - } + checkVerificationTargets(); } vector CHC::unhandledQueries() const @@ -540,7 +499,7 @@ void CHC::visitAssert(FunctionCall const& _funCall) m_currentBlock, m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction), currentPathConditions() && !m_context.expression(*args.front())->currentValue() && ( - m_error.currentValue() == static_cast(_funCall.id()) + m_error.currentValue() == newErrorId(_funCall) ) ); @@ -638,7 +597,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) connectBlocks( m_currentBlock, m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction), - currentPathConditions() && symbArray->length() <= 0 && m_error.currentValue() == static_cast(_arrayPop.id()) + currentPathConditions() && symbArray->length() <= 0 && m_error.currentValue() == newErrorId(_arrayPop) ); m_context.addAssertion(m_error.currentValue() == previousError); @@ -647,9 +606,10 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) void CHC::resetSourceAnalysis() { m_verificationTargets.clear(); - m_safeAssertions.clear(); + m_safeTargets.clear(); m_unsafeTargets.clear(); m_functionAssertions.clear(); + m_errorIds.clear(); m_callGraph.clear(); m_summaries.clear(); } @@ -1167,7 +1127,98 @@ void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smtutil::Expressi } } +void CHC::checkVerificationTargets() +{ + for (auto const& [scope, target]: m_verificationTargets) + { + if (target.type == VerificationTarget::Type::Assert) + checkAssertTarget(scope, target); + else + { + string satMsg; + string unknownMsg; + + if (target.type == VerificationTarget::Type::PopEmptyArray) + { + solAssert(dynamic_cast(scope), ""); + satMsg = "Empty array \"pop\" detected here."; + unknownMsg = "Empty array \"pop\" might happen here."; + } + else + solAssert(false, ""); + + auto it = m_errorIds.find(scope->id()); + solAssert(it != m_errorIds.end(), ""); + checkAndReportTarget(scope, target, it->second, satMsg, unknownMsg); + } + } +} + +void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const& _target) +{ + solAssert(_target.type == VerificationTarget::Type::Assert, ""); + auto assertions = transactionAssertions(_scope); + for (auto const* assertion: assertions) + { + auto it = m_errorIds.find(assertion->id()); + solAssert(it != m_errorIds.end(), ""); + unsigned errorId = it->second; + + createErrorBlock(); + connectBlocks(_target.value, error(), _target.constraints && (_target.errorId == errorId)); + auto [result, model] = query(error(), assertion->location()); + // This should be fine but it's a bug in the old compiler + (void)model; + if (result == smtutil::CheckResult::UNSATISFIABLE) + m_safeTargets[assertion].insert(_target.type); + } +} + +void CHC::checkAndReportTarget( + ASTNode const* _scope, + CHCVerificationTarget const& _target, + unsigned _errorId, + string _satMsg, + string _unknownMsg +) +{ + createErrorBlock(); + connectBlocks(_target.value, error(), _target.constraints && (_target.errorId == _errorId)); + auto [result, model] = query(error(), _scope->location()); + // This should be fine but it's a bug in the old compiler + (void)model; + if (result == smtutil::CheckResult::UNSATISFIABLE) + m_safeTargets[_scope].insert(_target.type); + else if (result == smtutil::CheckResult::SATISFIABLE) + { + solAssert(!_satMsg.empty(), ""); + m_unsafeTargets[_scope].insert(_target.type); + m_outerErrorReporter.warning( + 2529_error, + _scope->location(), + _satMsg + ); + } + else if (!_unknownMsg.empty()) + m_outerErrorReporter.warning( + 1147_error, + _scope->location(), + _unknownMsg + ); +} + string CHC::uniquePrefix() { return to_string(m_blockCounter++); } + +unsigned CHC::newErrorId(frontend::Expression const& _expr) +{ + unsigned errorId = m_context.newUniqueId(); + // We need to make sure the error id is not zero, + // because error id zero actually means no error in the CHC encoding. + if (errorId == 0) + errorId = m_context.newUniqueId(); + m_errorIds.emplace(_expr.id(), errorId); + return errorId; +} diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index dcba90606..07af4c76b 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -36,6 +36,7 @@ #include +#include #include namespace solidity::frontend @@ -54,7 +55,8 @@ public: void analyze(SourceUnit const& _sources); - std::set const& safeAssertions() const { return m_safeAssertions; } + std::map> const& safeTargets() const { return m_safeTargets; } + std::map> 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 @@ -191,6 +193,18 @@ private: void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId); void addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId); void addArrayPopVerificationTarget(ASTNode const* _scope, smtutil::Expression _errorId); + + void checkVerificationTargets(); + // Forward declaration. Definition is below. + struct CHCVerificationTarget; + void checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const& _target); + void checkAndReportTarget( + ASTNode const* _scope, + CHCVerificationTarget const& _target, + unsigned _errorId, + std::string _satMsg, + std::string _unknownMsg + ); //@} /// Misc. @@ -198,6 +212,10 @@ private: /// Returns a prefix to be used in a new unique block name /// and increases the block counter. std::string uniquePrefix(); + + /// @returns a new unique error id associated with _expr and stores + /// it into m_errorIds. + unsigned newErrorId(Expression const& _expr); //@} /// Predicates. @@ -257,10 +275,10 @@ private: std::map m_verificationTargets; - /// Assertions proven safe. - std::set m_safeAssertions; + /// Targets proven safe. + std::map> m_safeTargets; /// Targets proven unsafe. - std::set m_unsafeTargets; + std::map> m_unsafeTargets; //@} /// Control-flow. @@ -271,6 +289,11 @@ private: std::map, IdCompare> m_functionAssertions; + /// Maps ASTNode ids to error ids. + /// A multimap is used instead of map anticipating the UnderOverflow + /// target which has 2 error ids. + std::multimap m_errorIds; + /// The current block. smtutil::Expression m_currentBlock = smtutil::Expression(true); diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp index 57686ace4..b58160230 100644 --- a/libsolidity/formal/EncodingContext.cpp +++ b/libsolidity/formal/EncodingContext.cpp @@ -32,21 +32,21 @@ EncodingContext::EncodingContext(): void EncodingContext::reset() { resetAllVariables(); - resetSlackId(); + resetUniqueId(); m_expressions.clear(); m_globalContext.clear(); m_state.reset(); m_assertions.clear(); } -void EncodingContext::resetSlackId() +void EncodingContext::resetUniqueId() { - m_nextSlackId = 0; + m_nextUniqueId = 0; } -unsigned EncodingContext::newSlackId() +unsigned EncodingContext::newUniqueId() { - return m_nextSlackId++; + return m_nextUniqueId++; } void EncodingContext::clear() diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h index fcfd5e149..09316709a 100644 --- a/libsolidity/formal/EncodingContext.h +++ b/libsolidity/formal/EncodingContext.h @@ -41,9 +41,9 @@ public: /// To be used in the beginning of a root function visit. void reset(); /// Resets the fresh id for slack variables. - void resetSlackId(); + void resetUniqueId(); /// Returns the current fresh slack id and increments it. - unsigned newSlackId(); + unsigned newUniqueId(); /// Clears the entire context, erasing everything. /// To be used before a model checking engine starts. void clear(); @@ -173,8 +173,8 @@ private: bool m_accumulateAssertions = true; //@} - /// Fresh ids for slack variables to be created deterministically. - unsigned m_nextSlackId = 0; + /// Central source of unique ids. + unsigned m_nextUniqueId = 0; }; } diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index f74e1327d..718a41ae1 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -41,7 +41,12 @@ void ModelChecker::analyze(SourceUnit const& _source) return; m_chc.analyze(_source); - m_bmc.analyze(_source, m_chc.safeAssertions()); + + auto solvedTargets = m_chc.safeTargets(); + for (auto const& target: m_chc.unsafeTargets()) + solvedTargets[target.first] += target.second; + + m_bmc.analyze(_source, solvedTargets); } vector ModelChecker::unhandledQueries() diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 6faaaf600..bd2a9a754 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1262,7 +1262,7 @@ pair SMTEncoder::arithmeticOperation( auto symbMax = smt::maxValue(*intType); smtutil::Expression intValueRange = (0 - symbMin) + symbMax + 1; - string suffix = to_string(_operation.id()) + "_" + to_string(m_context.newSlackId()); + string suffix = to_string(_operation.id()) + "_" + to_string(m_context.newUniqueId()); smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context); smt::SymbolicIntVariable m(intType, intType, "m_" + suffix, m_context);