cerc-io/solidity
10
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 #6896 from ethereum/smt_use_portfolio

Browse Source 
[SMTChecker] Use SMTPortfolio directly
This commit is contained in:
Leonardo 2019-06-05 10:26:05 +02:00 committed by GitHub
commit c39ea56f93
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 38 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

62
libsolidity/formal/SMTChecker.cpp
View File

@ -34,10 +34,10 @@ using namespace langutil;
using namespace dev::solidity;
SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
m_interface(make_unique<smt::SMTPortfolio>(_smtlib2Responses)),
m_interface(_smtlib2Responses),
m_errorReporterReference(_errorReporter),
m_errorReporter(m_smtErrors),
m_context(*m_interface)
m_context(m_interface)
{
#if defined (HAVE_Z3) || defined (HAVE_CVC4)
if (!_smtlib2Responses.empty())
@ -56,11 +56,11 @@ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _
if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
_source.accept(*this);
solAssert(m_interface->solvers() > 0, "");
solAssert(m_interface.solvers() > 0, "");
// If this check is true, Z3 and CVC4 are not available
// and the query answers were not provided, since SMTPortfolio
// guarantees that SmtLib2Interface is the first solver.
if (!m_interface->unhandledQueries().empty() && m_interface->solvers() == 1)
if (!m_interface.unhandledQueries().empty() && m_interface.solvers() == 1)
{
if (!m_noSolverWarning)
{
@ -106,7 +106,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
// Not visited by a function call
if (m_callStack.empty())
{
m_interface->reset();
m_interface.reset();
m_context.reset();
m_pathConditions.clear();
m_callStack.clear();
@ -302,13 +302,13 @@ bool SMTChecker::visit(ForStatement const& _node)
checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
}
m_interface->push();
m_interface.push();
if (_node.condition())
m_interface->addAssertion(expr(*_node.condition()));
m_interface.addAssertion(expr(*_node.condition()));
_node.body().accept(*this);
if (_node.loopExpression())
_node.loopExpression()->accept(*this);
m_interface->pop();
m_interface.pop();
auto indicesAfterLoop = copyVariableIndices();
// We reset the execution to before the loop
@ -693,7 +693,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
solAssert(value, "");
smt::Expression thisBalance = m_context.balance();
setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_interface);
setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_interface);
checkCondition(thisBalance < expr(*value), _funCall.location(), "Insufficient funds", "address(this).balance", &thisBalance);
m_context.transfer(m_context.thisAddress(), expr(address), expr(*value));
@ -737,7 +737,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
// We set the current value to unknown anyway to add type constraints.
m_context.setUnknownValue(*symbolicVar);
if (index > 0)
m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
m_interface.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
}
void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
@ -819,7 +819,7 @@ void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
smtArguments.push_back(expr(*arg));
defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments));
m_uninterpretedTerms.insert(&_funCall);
setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_interface);
setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, m_interface);
}
void SMTChecker::endVisit(Identifier const& _identifier)
@ -911,7 +911,7 @@ void SMTChecker::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_interface);
m_context.createExpression(_literal, result.second);
}
m_errorReporter.warning(
@ -936,10 +936,10 @@ void SMTChecker::endVisit(Return const& _return)
solAssert(components.size() == returnParams.size(), "");
for (unsigned i = 0; i < returnParams.size(); ++i)
if (components.at(i))
m_interface->addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i)));
m_interface.addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i)));
}
else if (returnParams.size() == 1)
m_interface->addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
m_interface.addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
}
}
@ -981,7 +981,7 @@ bool SMTChecker::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_interface);
m_uninterpretedTerms.insert(&_memberAccess);
return false;
}
@ -1028,7 +1028,7 @@ void SMTChecker::endVisit(IndexAccess const& _indexAccess)
setSymbolicUnknownValue(
expr(_indexAccess),
_indexAccess.annotation().type,
*m_interface
m_interface
);
m_uninterpretedTerms.insert(&_indexAccess);
}
@ -1080,7 +1080,7 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c
expr(*indexAccess.indexExpression()),
_rightHandSide
);
m_interface->addAssertion(m_context.newValue(*varDecl) == store);
m_interface.addAssertion(m_context.newValue(*varDecl) == store);
// Update the SMT select value after the assignment,
// necessary for sound models.
defineExpr(indexAccess, smt::Expression::select(
@ -1211,7 +1211,7 @@ smt::Expression SMTChecker::arithmeticOperation(
if (_op == Token::Div || _op == Token::Mod)
{
checkCondition(_right == 0, _location, "Division by zero", "<result>", &_right);
m_interface->addAssertion(_right != 0);
m_interface.addAssertion(_right != 0);
}
addOverflowTarget(
@ -1393,7 +1393,7 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio
addOverflowTarget(OverflowTarget::Type::All, TypeProvider::uint(160), _value, _location);
else if (type->category() == Type::Category::Mapping)
arrayAssignment();
m_interface->addAssertion(m_context.newValue(_variable) == _value);
m_interface.addAssertion(m_context.newValue(_variable) == _value);
}
SMTChecker::VariableIndices SMTChecker::visitBranch(ASTNode const* _statement, smt::Expression _condition)
@ -1422,7 +1422,7 @@ void SMTChecker::checkCondition(
smt::Expression const* _additionalValue
)
{
m_interface->push();
m_interface.push();
addPathConjoinedExpression(_condition);
vector<smt::Expression> expressionsToEvaluate;
@ -1534,7 +1534,7 @@ void SMTChecker::checkCondition(
m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
break;
}
m_interface->pop();
m_interface.pop();
}
void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string const& _description)
@ -1543,15 +1543,15 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
if (dynamic_cast<Literal const*>(&_condition))
return;
m_interface->push();
m_interface.push();
addPathConjoinedExpression(expr(_condition));
auto positiveResult = checkSatisfiable();
m_interface->pop();
m_interface.pop();
m_interface->push();
m_interface.push();
addPathConjoinedExpression(!expr(_condition));
auto negatedResult = checkSatisfiable();
m_interface->pop();
m_interface.pop();
if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver.");
@ -1596,7 +1596,7 @@ SMTChecker::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _exp
vector<string> values;
try
{
tie(result, values) = m_interface->check(_expressionsToEvaluate);
tie(result, values) = m_interface.check(_expressionsToEvaluate);
}
catch (smt::SolverError const& _e)
{
@ -1632,7 +1632,7 @@ void SMTChecker::initializeFunctionCallParameters(CallableDeclaration const& _fu
for (unsigned i = 0; i < funParams.size(); ++i)
if (createVariable(*funParams[i]))
{
m_interface->addAssertion(_callArgs[i] == m_context.newValue(*funParams[i]));
m_interface.addAssertion(_callArgs[i] == m_context.newValue(*funParams[i]));
if (funParams[i]->annotation().type->category() == Type::Category::Mapping)
m_arrayAssignmentHappened = true;
}
@ -1698,7 +1698,7 @@ void SMTChecker::mergeVariables(set<VariableDeclaration const*> const& _variable
int trueIndex = _indicesEndTrue.at(decl);
int falseIndex = _indicesEndFalse.at(decl);
solAssert(trueIndex != falseIndex, "");
m_interface->addAssertion(m_context.newValue(*decl) == smt::Expression::ite(
m_interface.addAssertion(m_context.newValue(*decl) == smt::Expression::ite(
_condition,
valueAtIndex(*decl, trueIndex),
valueAtIndex(*decl, falseIndex))
@ -1758,7 +1758,7 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
{
createExpr(_e);
solAssert(smt::smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported");
m_interface->addAssertion(expr(_e) == _value);
m_interface.addAssertion(expr(_e) == _value);
}
void SMTChecker::popPathCondition()
@ -1807,12 +1807,12 @@ void SMTChecker::pushCallStack(CallStackEntry _entry)
void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e)
{
m_interface->addAssertion(currentPathConditions() && _e);
m_interface.addAssertion(currentPathConditions() && _e);
}
void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
{
m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
m_interface.addAssertion(smt::Expression::implies(currentPathConditions(), _e));
}
bool SMTChecker::isRootFunction()

10
libsolidity/formal/SMTChecker.h
View File

@ -19,7 +19,7 @@
#include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/formal/SMTPortfolio.h>
#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/formal/VariableUsage.h>
@ -53,7 +53,7 @@ public:
/// 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
/// the constructor.
std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
std::vector<std::string> unhandledQueries() { return m_interface.unhandledQueries(); }
/// @returns the FunctionDefinition of a called function if possible and should inline,
/// otherwise nullptr.
@ -91,6 +91,10 @@ private:
void endVisit(IndexAccess const& _node) override;
bool visit(InlineAssembly const& _node) override;
smt::Expression assertions() { return m_interface.assertions(); }
void push() { m_interface.push(); }
void pop() { m_interface.pop(); }
/// Do not visit subtree if node is a RationalNumber.
/// Symbolic _expr is the rational literal.
bool shortcutRationalNumber(Expression const& _expr);
@ -270,7 +274,7 @@ private:
/// @returns the VariableDeclaration referenced by an Identifier or nullptr.
VariableDeclaration const* identifierToVariable(Expression const& _expr);
std::unique_ptr<smt::SolverInterface> m_interface;
smt::SMTPortfolio m_interface;
smt::VariableUsage m_variableUsage;
bool m_loopExecutionHappened = false;
bool m_arrayAssignmentHappened = false;