cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #7030 from ethereum/smt_move_solver

Browse Source 
[SMTChecker] Move solver from SMTEncoder to BMC
This commit is contained in:
chriseth 2019-07-02 14:08:55 +02:00 committed by GitHub
commit 817852c650
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 12 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsolidity/formal/BMC.cpp
View File

@ -28,8 +28,9 @@ using namespace langutil;
using namespace dev::solidity; using namespace dev::solidity;
BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses): BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
SMTEncoder(_context, _smtlib2Responses), SMTEncoder(_context),
m_outerErrorReporter(_errorReporter) m_outerErrorReporter(_errorReporter),
m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses))
{ {
#if defined (HAVE_Z3) || defined (HAVE_CVC4) #if defined (HAVE_Z3) || defined (HAVE_CVC4)
if (!_smtlib2Responses.empty()) if (!_smtlib2Responses.empty())

4
libsolidity/formal/BMC.h
View File

@ -30,7 +30,7 @@
#include <libsolidity/formal/EncodingContext.h> #include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SMTEncoder.h> #include <libsolidity/formal/SMTEncoder.h>
#include <libsolidity/formal/SMTPortfolio.h> #include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/interface/ReadFile.h> #include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h> #include <liblangutil/ErrorReporter.h>
@ -174,6 +174,8 @@ private:
langutil::ErrorReporter& m_outerErrorReporter; langutil::ErrorReporter& m_outerErrorReporter;
std::vector<VerificationTarget> m_verificationTargets; std::vector<VerificationTarget> m_verificationTargets;
std::shared_ptr<smt::SolverInterface> m_interface;
}; };
} }

11
libsolidity/formal/SMTEncoder.cpp
View File

@ -28,8 +28,7 @@ using namespace dev;
using namespace langutil; using namespace langutil;
using namespace dev::solidity; using namespace dev::solidity;
SMTEncoder::SMTEncoder(smt::EncodingContext& _context, map<h256, string> const& _smtlib2Responses): SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
m_errorReporter(m_smtErrors), m_errorReporter(m_smtErrors),
m_context(_context) m_context(_context)
{ {
@ -474,7 +473,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
solAssert(value, ""); solAssert(value, "");
smt::Expression thisBalance = m_context.balance(); smt::Expression thisBalance = m_context.balance();
setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_interface); setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_context.solver());
m_context.transfer(m_context.thisAddress(), expr(address), expr(*value)); m_context.transfer(m_context.thisAddress(), expr(address), expr(*value));
break; break;
@ -616,7 +615,7 @@ void SMTEncoder::endVisit(Literal const& _literal)
auto stringType = TypeProvider::stringMemory(); auto stringType = TypeProvider::stringMemory();
auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type); auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type);
solAssert(stringLit, ""); solAssert(stringLit, "");
auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface); auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_context.solver());
m_context.createExpression(_literal, result.second); m_context.createExpression(_literal, result.second);
} }
m_errorReporter.warning( m_errorReporter.warning(
@ -688,7 +687,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
if (_memberAccess.memberName() == "balance") if (_memberAccess.memberName() == "balance")
{ {
defineExpr(_memberAccess, m_context.balance(expr(_memberAccess.expression()))); defineExpr(_memberAccess, m_context.balance(expr(_memberAccess.expression())));
setSymbolicUnknownValue(*m_context.expression(_memberAccess), *m_interface); setSymbolicUnknownValue(*m_context.expression(_memberAccess), *m_context.solver());
m_uninterpretedTerms.insert(&_memberAccess); m_uninterpretedTerms.insert(&_memberAccess);
return false; return false;
} }
@ -735,7 +734,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
setSymbolicUnknownValue( setSymbolicUnknownValue(
expr(_indexAccess), expr(_indexAccess),
_indexAccess.annotation().type, _indexAccess.annotation().type,
*m_interface *m_context.solver()
); );
m_uninterpretedTerms.insert(&_indexAccess); m_uninterpretedTerms.insert(&_indexAccess);
} }

4
libsolidity/formal/SMTEncoder.h
View File

@ -24,7 +24,6 @@
#include <libsolidity/formal/EncodingContext.h> #include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SMTPortfolio.h>
#include <libsolidity/formal/SymbolicVariables.h> #include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/formal/VariableUsage.h> #include <libsolidity/formal/VariableUsage.h>
@ -51,7 +50,7 @@ namespace solidity
class SMTEncoder: public ASTConstVisitor class SMTEncoder: public ASTConstVisitor
{ {
public: public:
SMTEncoder(smt::EncodingContext& _context, std::map<h256, std::string> const& _smtlib2Responses); SMTEncoder(smt::EncodingContext& _context);
/// @returns the leftmost identifier in a multi-d IndexAccess. /// @returns the leftmost identifier in a multi-d IndexAccess.
static Expression const* leftmostBase(IndexAccess const& _indexAccess); static Expression const* leftmostBase(IndexAccess const& _indexAccess);
@ -208,7 +207,6 @@ protected:
/// @returns a note to be added to warnings. /// @returns a note to be added to warnings.
std::string extraComment(); std::string extraComment();
std::shared_ptr<smt::SolverInterface> m_interface;
smt::VariableUsage m_variableUsage; smt::VariableUsage m_variableUsage;
bool m_arrayAssignmentHappened = false; bool m_arrayAssignmentHappened = false;
// True if the "No SMT solver available" warning was already created. // True if the "No SMT solver available" warning was already created.