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 #6985 from ethereum/smt_refactor_bmc

Browse Source 
[SMTChecker] Collect assertions in EncodingContext
This commit is contained in:
chriseth 2019-06-24 16:09:09 +02:00 committed by GitHub
commit 3d5e2b40c5
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 104 additions and 73 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

54
libsolidity/formal/EncodingContext.cpp
View File

@ -23,15 +23,15 @@ using namespace std;
using namespace dev; using namespace dev;
using namespace dev::solidity::smt; using namespace dev::solidity::smt;
EncodingContext::EncodingContext(SolverInterface& _solver): EncodingContext::EncodingContext(std::shared_ptr<SolverInterface> _solver):
m_solver(_solver), m_thisAddress(make_unique<SymbolicAddressVariable>("this", *_solver)),
m_thisAddress(make_unique<SymbolicAddressVariable>("this", m_solver)) m_solver(_solver)
{ {
auto sort = make_shared<ArraySort>( auto sort = make_shared<ArraySort>(
make_shared<Sort>(Kind::Int), make_shared<Sort>(Kind::Int),
make_shared<Sort>(Kind::Int) make_shared<Sort>(Kind::Int)
); );
m_balances = make_unique<SymbolicVariable>(sort, "balances", m_solver); m_balances = make_unique<SymbolicVariable>(sort, "balances", *m_solver);
} }
void EncodingContext::reset() void EncodingContext::reset()
@ -41,6 +41,7 @@ void EncodingContext::reset()
m_globalContext.clear(); m_globalContext.clear();
m_thisAddress->increaseIndex(); m_thisAddress->increaseIndex();
m_balances->increaseIndex(); m_balances->increaseIndex();
m_assertions.clear();
} }
/// Variables. /// Variables.
@ -55,7 +56,7 @@ bool EncodingContext::createVariable(solidity::VariableDeclaration const& _varDe
{ {
solAssert(!knownVariable(_varDecl), ""); solAssert(!knownVariable(_varDecl), "");
auto const& type = _varDecl.type(); auto const& type = _varDecl.type();
auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), m_solver); auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_solver);
m_variables.emplace(&_varDecl, result.second); m_variables.emplace(&_varDecl, result.second);
return result.first; return result.first;
} }
@ -105,7 +106,7 @@ void EncodingContext::setZeroValue(solidity::VariableDeclaration const& _decl)
void EncodingContext::setZeroValue(SymbolicVariable& _variable) void EncodingContext::setZeroValue(SymbolicVariable& _variable)
{ {
setSymbolicZeroValue(_variable, m_solver); setSymbolicZeroValue(_variable, *m_solver);
} }
void EncodingContext::setUnknownValue(solidity::VariableDeclaration const& _decl) void EncodingContext::setUnknownValue(solidity::VariableDeclaration const& _decl)
@ -116,7 +117,7 @@ void EncodingContext::setUnknownValue(solidity::VariableDeclaration const& _decl
void EncodingContext::setUnknownValue(SymbolicVariable& _variable) void EncodingContext::setUnknownValue(SymbolicVariable& _variable)
{ {
setSymbolicUnknownValue(_variable, m_solver); setSymbolicUnknownValue(_variable, *m_solver);
} }
/// Expressions /// Expressions
@ -143,7 +144,7 @@ bool EncodingContext::createExpression(solidity::Expression const& _e, shared_pt
} }
else else
{ {
auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), m_solver); auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_solver);
m_expressions.emplace(&_e, result.second); m_expressions.emplace(&_e, result.second);
return result.first; return result.first;
} }
@ -165,7 +166,7 @@ shared_ptr<SymbolicVariable> EncodingContext::globalSymbol(string const& _name)
bool EncodingContext::createGlobalSymbol(string const& _name, solidity::Expression const& _expr) bool EncodingContext::createGlobalSymbol(string const& _name, solidity::Expression const& _expr)
{ {
solAssert(!knownGlobalSymbol(_name), ""); solAssert(!knownGlobalSymbol(_name), "");
auto result = newSymbolicVariable(*_expr.annotation().type, _name, m_solver); auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_solver);
m_globalContext.emplace(_name, result.second); m_globalContext.emplace(_name, result.second);
setUnknownValue(*result.second); setUnknownValue(*result.second);
return result.first; return result.first;
@ -207,9 +208,40 @@ void EncodingContext::transfer(Expression _from, Expression _to, Expression _val
m_balances->valueAtIndex(indexBefore), m_balances->valueAtIndex(indexBefore),
m_balances->valueAtIndex(indexAfter) m_balances->valueAtIndex(indexAfter)
); );
m_solver.addAssertion(m_balances->currentValue() == newBalances); m_solver->addAssertion(m_balances->currentValue() == newBalances);
} }
/// Solver.
Expression EncodingContext::assertions()
{
if (m_assertions.empty())
return Expression(true);
return m_assertions.back();
}
void EncodingContext::pushSolver()
{
m_assertions.push_back(assertions());
}
void EncodingContext::popSolver()
{
solAssert(!m_assertions.empty(), "");
m_assertions.pop_back();
}
void EncodingContext::addAssertion(Expression const& _expr)
{
if (m_assertions.empty())
m_assertions.push_back(_expr);
else
m_assertions.back() = _expr && move(m_assertions.back());
}
/// Private helpers.
void EncodingContext::addBalance(Expression _address, Expression _value) void EncodingContext::addBalance(Expression _address, Expression _value)
{ {
auto newBalances = Expression::store( auto newBalances = Expression::store(
@ -218,5 +250,5 @@ void EncodingContext::addBalance(Expression _address, Expression _value)
balance(_address) + move(_value) balance(_address) + move(_value)
); );
m_balances->increaseIndex(); m_balances->increaseIndex();
m_solver.addAssertion(newBalances == m_balances->currentValue()); m_solver->addAssertion(newBalances == m_balances->currentValue());
} }

37
libsolidity/formal/EncodingContext.h
View File

@ -36,12 +36,12 @@ namespace smt
class EncodingContext class EncodingContext
{ {
public: public:
EncodingContext(SolverInterface& _solver); EncodingContext(std::shared_ptr<SolverInterface> _solver);
/// Resets the entire context. /// Resets the entire context.
void reset(); void reset();
/// Methods related to variables. /// Variables.
//@{ //@{
/// @returns the symbolic representation of a program variable. /// @returns the symbolic representation of a program variable.
std::shared_ptr<SymbolicVariable> variable(solidity::VariableDeclaration const& _varDecl); std::shared_ptr<SymbolicVariable> variable(solidity::VariableDeclaration const& _varDecl);
@ -74,7 +74,7 @@ public:
void setUnknownValue(SymbolicVariable& _variable); void setUnknownValue(SymbolicVariable& _variable);
//@} //@}
/// Methods related to expressions. /// Expressions.
////@{ ////@{
/// @returns the symbolic representation of an AST node expression. /// @returns the symbolic representation of an AST node expression.
std::shared_ptr<SymbolicVariable> expression(solidity::Expression const& _e); std::shared_ptr<SymbolicVariable> expression(solidity::Expression const& _e);
@ -88,12 +88,13 @@ public:
bool knownExpression(solidity::Expression const& _e) const; bool knownExpression(solidity::Expression const& _e) const;
//@} //@}
/// Methods related to global variables and functions. /// Global variables and functions.
//@{ //@{
/// Global variables and functions. /// Global variables and functions.
std::shared_ptr<SymbolicVariable> globalSymbol(std::string const& _name); std::shared_ptr<SymbolicVariable> globalSymbol(std::string const& _name);
/// @returns all symbolic variables. /// @returns all symbolic globals.
std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> const& globalSymbols() const { return m_globalContext; } std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> const& globalSymbols() const { return m_globalContext; }
/// Defines a new global variable or function /// Defines a new global variable or function
/// and @returns true if type was abstracted. /// and @returns true if type was abstracted.
bool createGlobalSymbol(std::string const& _name, solidity::Expression const& _expr); bool createGlobalSymbol(std::string const& _name, solidity::Expression const& _expr);
@ -101,7 +102,7 @@ public:
bool knownGlobalSymbol(std::string const& _var) const; bool knownGlobalSymbol(std::string const& _var) const;
//@} //@}
/// Blockchain related methods. /// Blockchain.
//@{ //@{
/// Value of `this` address. /// Value of `this` address.
Expression thisAddress(); Expression thisAddress();
@ -113,12 +114,22 @@ public:
void transfer(Expression _from, Expression _to, Expression _value); void transfer(Expression _from, Expression _to, Expression _value);
//@} //@}
/// Solver.
//@{
/// @returns conjunction of all added assertions.
Expression assertions();
void pushSolver();
void popSolver();
void addAssertion(Expression const& _e);
std::shared_ptr<SolverInterface> solver() { return m_solver; }
//@}
private: private:
/// Adds _value to _account's balance. /// Adds _value to _account's balance.
void addBalance(Expression _account, Expression _value); void addBalance(Expression _account, Expression _value);
SolverInterface& m_solver; /// Symbolic expressions.
//{@
/// Symbolic variables. /// Symbolic variables.
std::unordered_map<solidity::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables; std::unordered_map<solidity::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
@ -134,6 +145,16 @@ private:
/// Symbolic balances. /// Symbolic balances.
std::unique_ptr<SymbolicVariable> m_balances; std::unique_ptr<SymbolicVariable> m_balances;
//@}
/// Solver related.
//@{
/// Solver can be SMT solver or Horn solver in the future.
std::shared_ptr<SolverInterface> m_solver;
/// Assertion stack.
std::vector<Expression> m_assertions;
//@}
}; };
} }

60
libsolidity/formal/SMTChecker.cpp
View File

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

8
libsolidity/formal/SMTChecker.h
View File

@ -53,7 +53,7 @@ public:
/// This is used if the SMT solver is not directly linked into this binary. /// 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 /// @returns a list of inputs to the SMT solver that were not part of the argument to
/// the constructor. /// 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, /// @returns the FunctionDefinition of a called function if possible and should inline,
/// otherwise nullptr. /// otherwise nullptr.
@ -91,10 +91,6 @@ private:
void endVisit(IndexAccess const& _node) override; void endVisit(IndexAccess const& _node) override;
bool visit(InlineAssembly 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. /// Do not visit subtree if node is a RationalNumber.
/// Symbolic _expr is the rational literal. /// Symbolic _expr is the rational literal.
bool shortcutRationalNumber(Expression const& _expr); bool shortcutRationalNumber(Expression const& _expr);
@ -274,7 +270,7 @@ private:
/// @returns the VariableDeclaration referenced by an Identifier or nullptr. /// @returns the VariableDeclaration referenced by an Identifier or nullptr.
VariableDeclaration const* identifierToVariable(Expression const& _expr); VariableDeclaration const* identifierToVariable(Expression const& _expr);
smt::SMTPortfolio m_interface; std::shared_ptr<smt::SolverInterface> m_interface;
smt::VariableUsage m_variableUsage; smt::VariableUsage m_variableUsage;
bool m_loopExecutionHappened = false; bool m_loopExecutionHappened = false;
bool m_arrayAssignmentHappened = false; bool m_arrayAssignmentHappened = false;

16
libsolidity/formal/SMTPortfolio.cpp
View File

@ -43,21 +43,18 @@ SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
void SMTPortfolio::reset() void SMTPortfolio::reset()
{ {
m_assertions.clear();
for (auto const& s: m_solvers) for (auto const& s: m_solvers)
s->reset(); s->reset();
} }
void SMTPortfolio::push() void SMTPortfolio::push()
{ {
m_assertions.push_back(Expression(true));
for (auto const& s: m_solvers) for (auto const& s: m_solvers)
s->push(); s->push();
} }
void SMTPortfolio::pop() void SMTPortfolio::pop()
{ {
m_assertions.pop_back();
for (auto const& s: m_solvers) for (auto const& s: m_solvers)
s->pop(); s->pop();
} }
@ -70,23 +67,10 @@ void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort)
void SMTPortfolio::addAssertion(Expression const& _expr) void SMTPortfolio::addAssertion(Expression const& _expr)
{ {
if (m_assertions.empty())
m_assertions.push_back(_expr);
else
m_assertions.back() = _expr && move(m_assertions.back());
for (auto const& s: m_solvers) for (auto const& s: m_solvers)
s->addAssertion(_expr); s->addAssertion(_expr);
} }
Expression SMTPortfolio::assertions()
{
if (m_assertions.empty())
return Expression(true);
return m_assertions.back();
}
/* /*
* Broadcasts the SMT query to all solvers and returns a single result. * Broadcasts the SMT query to all solvers and returns a single result.
* This comment explains how this result is decided. * This comment explains how this result is decided.

2
libsolidity/formal/SMTPortfolio.h
View File

@ -53,8 +53,6 @@ public:
void addAssertion(Expression const& _expr) override; void addAssertion(Expression const& _expr) override;
Expression assertions();
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
std::vector<std::string> unhandledQueries() override; std::vector<std::string> unhandledQueries() override;