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

[SMTChecker] Move solver pointer from SMTEncoder to BMC

Browse Source
This commit is contained in:
Leonardo Alt 2019-07-02 12:06:52 +02:00
parent 7de18b37c2
commit b0818bd002
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;
BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
SMTEncoder(_context, _smtlib2Responses),
m_outerErrorReporter(_errorReporter)
SMTEncoder(_context),
m_outerErrorReporter(_errorReporter),
m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses))
{
#if defined (HAVE_Z3) || defined (HAVE_CVC4)
if (!_smtlib2Responses.empty())

4
libsolidity/formal/BMC.h
View File

@ -30,7 +30,7 @@
#include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SMTEncoder.h>
#include <libsolidity/formal/SMTPortfolio.h>
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h>
@ -174,6 +174,8 @@ private:
langutil::ErrorReporter& m_outerErrorReporter;
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 dev::solidity;
SMTEncoder::SMTEncoder(smt::EncodingContext& _context, map<h256, string> const& _smtlib2Responses):
m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
m_errorReporter(m_smtErrors),
m_context(_context)
{
@ -471,7 +470,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
solAssert(value, "");
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));
break;
@ -616,7 +615,7 @@ void SMTEncoder::endVisit(Literal const& _literal)
auto stringType = TypeProvider::stringMemory();
auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type);
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_errorReporter.warning(
@ -686,7 +685,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
if (_memberAccess.memberName() == "balance")
{
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);
return false;
}
@ -733,7 +732,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
setSymbolicUnknownValue(
expr(_indexAccess),
_indexAccess.annotation().type,
*m_interface
*m_context.solver()
);
m_uninterpretedTerms.insert(&_indexAccess);
}

4
libsolidity/formal/SMTEncoder.h
View File

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