From 934e00d235caa56348f662cf01e29f5ab52e3ca9 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 3 Jul 2019 16:05:56 +0200 Subject: [PATCH] [SMTChecker] SymbolicVariables use EncodingContext to declare SMT vars --- libsolidity/formal/BMC.cpp | 2 +- libsolidity/formal/EncodingContext.cpp | 14 +++--- libsolidity/formal/EncodingContext.h | 7 +++ libsolidity/formal/SMTEncoder.cpp | 8 +-- libsolidity/formal/SymbolicTypes.cpp | 50 +++++++++---------- libsolidity/formal/SymbolicTypes.h | 12 ++--- libsolidity/formal/SymbolicVariables.cpp | 50 +++++++++---------- libsolidity/formal/SymbolicVariables.h | 25 +++++----- .../smtCheckerTestsJSON/multi.json | 6 +-- .../smtCheckerTestsJSON/simple.json | 2 +- 10 files changed, 92 insertions(+), 84 deletions(-) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index f3556e7da..279ed8e74 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -459,7 +459,7 @@ void BMC::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_context.solver()); + setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, m_context); } void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall) diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp index 2442c7df7..5170773a6 100644 --- a/libsolidity/formal/EncodingContext.cpp +++ b/libsolidity/formal/EncodingContext.cpp @@ -24,14 +24,14 @@ using namespace dev; using namespace dev::solidity::smt; EncodingContext::EncodingContext(std::shared_ptr _solver): - m_thisAddress(make_unique("this", *_solver)), + m_thisAddress(make_unique("this", *this)), m_solver(_solver) { auto sort = make_shared( make_shared(Kind::Int), make_shared(Kind::Int) ); - m_balances = make_unique(sort, "balances", *m_solver); + m_balances = make_unique(sort, "balances", *this); } void EncodingContext::reset() @@ -56,7 +56,7 @@ bool EncodingContext::createVariable(solidity::VariableDeclaration const& _varDe { solAssert(!knownVariable(_varDecl), ""); 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()), *this); m_variables.emplace(&_varDecl, result.second); return result.first; } @@ -106,7 +106,7 @@ void EncodingContext::setZeroValue(solidity::VariableDeclaration const& _decl) void EncodingContext::setZeroValue(SymbolicVariable& _variable) { - setSymbolicZeroValue(_variable, *m_solver); + setSymbolicZeroValue(_variable, *this); } void EncodingContext::setUnknownValue(solidity::VariableDeclaration const& _decl) @@ -117,7 +117,7 @@ void EncodingContext::setUnknownValue(solidity::VariableDeclaration const& _decl void EncodingContext::setUnknownValue(SymbolicVariable& _variable) { - setSymbolicUnknownValue(_variable, *m_solver); + setSymbolicUnknownValue(_variable, *this); } /// Expressions @@ -144,7 +144,7 @@ bool EncodingContext::createExpression(solidity::Expression const& _e, shared_pt } 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()), *this); m_expressions.emplace(&_e, result.second); return result.first; } @@ -166,7 +166,7 @@ shared_ptr EncodingContext::globalSymbol(string const& _name) bool EncodingContext::createGlobalSymbol(string const& _name, solidity::Expression const& _expr) { solAssert(!knownGlobalSymbol(_name), ""); - auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_solver); + auto result = newSymbolicVariable(*_expr.annotation().type, _name, *this); m_globalContext.emplace(_name, result.second); setUnknownValue(*result.second); return result.first; diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h index 4532d6fb4..3bce9b6e4 100644 --- a/libsolidity/formal/EncodingContext.h +++ b/libsolidity/formal/EncodingContext.h @@ -41,6 +41,13 @@ public: /// Resets the entire context. void reset(); + /// Forwards variable creation to the solver. + Expression newVariable(std::string _name, SortPointer _sort) + { + solAssert(m_solver, ""); + return m_solver->newVariable(move(_name), move(_sort)); + } + /// Variables. //@{ /// @returns the symbolic representation of a program variable. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index b7735a5f3..45694c187 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -473,7 +473,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) solAssert(value, ""); smt::Expression thisBalance = m_context.balance(); - setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_context.solver()); + setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context); m_context.transfer(m_context.thisAddress(), expr(address), expr(*value)); break; @@ -615,7 +615,7 @@ void SMTEncoder::endVisit(Literal const& _literal) auto stringType = TypeProvider::stringMemory(); auto stringLit = dynamic_cast(_literal.annotation().type); solAssert(stringLit, ""); - auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_context.solver()); + auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), m_context); m_context.createExpression(_literal, result.second); } m_errorReporter.warning( @@ -687,7 +687,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_context.solver()); + setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_context); m_uninterpretedTerms.insert(&_memberAccess); return false; } @@ -734,7 +734,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) setSymbolicUnknownValue( expr(_indexAccess), _indexAccess.annotation().type, - *m_context.solver() + m_context ); m_uninterpretedTerms.insert(&_indexAccess); } diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 7f0cb21ea..269fd1601 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -118,7 +118,7 @@ bool isSupportedTypeDeclaration(solidity::Type::Category _category) pair> newSymbolicVariable( solidity::Type const& _type, std::string const& _uniqueName, - SolverInterface& _solver + EncodingContext& _context ) { bool abstract = false; @@ -127,39 +127,39 @@ pair> newSymbolicVariable( if (!isSupportedTypeDeclaration(_type)) { abstract = true; - var = make_shared(solidity::TypeProvider::uint256(), _uniqueName, _solver); + var = make_shared(solidity::TypeProvider::uint256(), _uniqueName, _context); } else if (isBool(_type.category())) - var = make_shared(type, _uniqueName, _solver); + var = make_shared(type, _uniqueName, _context); else if (isFunction(_type.category())) - var = make_shared(type, _uniqueName, _solver); + var = make_shared(type, _uniqueName, _context); else if (isInteger(_type.category())) - var = make_shared(type, _uniqueName, _solver); + var = make_shared(type, _uniqueName, _context); else if (isFixedBytes(_type.category())) { auto fixedBytesType = dynamic_cast(type); solAssert(fixedBytesType, ""); - var = make_shared(fixedBytesType->numBytes(), _uniqueName, _solver); + var = make_shared(fixedBytesType->numBytes(), _uniqueName, _context); } else if (isAddress(_type.category()) || isContract(_type.category())) - var = make_shared(_uniqueName, _solver); + var = make_shared(_uniqueName, _context); else if (isEnum(_type.category())) - var = make_shared(type, _uniqueName, _solver); + var = make_shared(type, _uniqueName, _context); else if (isRational(_type.category())) { auto rational = dynamic_cast(&_type); solAssert(rational, ""); if (rational->isFractional()) - var = make_shared(solidity::TypeProvider::uint256(), _uniqueName, _solver); + var = make_shared(solidity::TypeProvider::uint256(), _uniqueName, _context); else - var = make_shared(type, _uniqueName, _solver); + var = make_shared(type, _uniqueName, _context); } else if (isMapping(_type.category())) - var = make_shared(type, _uniqueName, _solver); + var = make_shared(type, _uniqueName, _context); else if (isArray(_type.category())) - var = make_shared(type, _uniqueName, _solver); + var = make_shared(type, _uniqueName, _context); else if (isTuple(_type.category())) - var = make_shared(type, _uniqueName, _solver); + var = make_shared(type, _uniqueName, _context); else solAssert(false, ""); return make_pair(abstract, var); @@ -250,41 +250,41 @@ Expression maxValue(solidity::IntegerType const& _type) return Expression(_type.maxValue()); } -void setSymbolicZeroValue(SymbolicVariable const& _variable, SolverInterface& _interface) +void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context) { - setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _interface); + setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _context); } -void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface) +void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context) { solAssert(_type, ""); if (isInteger(_type->category())) - _interface.addAssertion(_expr == 0); + _context.addAssertion(_expr == 0); else if (isBool(_type->category())) - _interface.addAssertion(_expr == Expression(false)); + _context.addAssertion(_expr == Expression(false)); } -void setSymbolicUnknownValue(SymbolicVariable const& _variable, SolverInterface& _interface) +void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context) { - setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _interface); + setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _context); } -void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface) +void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context) { solAssert(_type, ""); if (isEnum(_type->category())) { auto enumType = dynamic_cast(_type); solAssert(enumType, ""); - _interface.addAssertion(_expr >= 0); - _interface.addAssertion(_expr < enumType->numberOfMembers()); + _context.addAssertion(_expr >= 0); + _context.addAssertion(_expr < enumType->numberOfMembers()); } else if (isInteger(_type->category())) { auto intType = dynamic_cast(_type); solAssert(intType, ""); - _interface.addAssertion(_expr >= minValue(*intType)); - _interface.addAssertion(_expr <= maxValue(*intType)); + _context.addAssertion(_expr >= minValue(*intType)); + _context.addAssertion(_expr <= maxValue(*intType)); } } diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 8993575e3..666cc0f38 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -17,7 +17,7 @@ #pragma once -#include +#include #include #include #include @@ -58,15 +58,15 @@ bool isTuple(solidity::Type::Category _category); /// Returns a new symbolic variable, according to _type. /// Also returns whether the type is abstract or not, /// which is true for unsupported types. -std::pair> newSymbolicVariable(solidity::Type const& _type, std::string const& _uniqueName, SolverInterface& _solver); +std::pair> newSymbolicVariable(solidity::Type const& _type, std::string const& _uniqueName, EncodingContext& _context); Expression minValue(solidity::IntegerType const& _type); Expression maxValue(solidity::IntegerType const& _type); -void setSymbolicZeroValue(SymbolicVariable const& _variable, SolverInterface& _interface); -void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface); -void setSymbolicUnknownValue(SymbolicVariable const& _variable, SolverInterface& _interface); -void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface); +void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context); +void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context); +void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context); +void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context); } } diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 398924b5d..aa02e3b24 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -28,11 +28,11 @@ using namespace dev::solidity::smt; SymbolicVariable::SymbolicVariable( solidity::TypePointer _type, string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ): m_type(move(_type)), m_uniqueName(move(_uniqueName)), - m_interface(_interface), + m_context(_context), m_ssa(make_unique()) { solAssert(m_type, ""); @@ -43,11 +43,11 @@ SymbolicVariable::SymbolicVariable( SymbolicVariable::SymbolicVariable( SortPointer _sort, string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ): m_sort(move(_sort)), m_uniqueName(move(_uniqueName)), - m_interface(_interface), + m_context(_context), m_ssa(make_unique()) { solAssert(m_sort, ""); @@ -65,7 +65,7 @@ string SymbolicVariable::currentName() const Expression SymbolicVariable::valueAtIndex(int _index) const { - return m_interface.newVariable(uniqueSymbol(_index), m_sort); + return m_context.newVariable(uniqueSymbol(_index), m_sort); } string SymbolicVariable::uniqueSymbol(unsigned _index) const @@ -82,9 +82,9 @@ Expression SymbolicVariable::increaseIndex() SymbolicBoolVariable::SymbolicBoolVariable( solidity::TypePointer _type, string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _interface) + SymbolicVariable(move(_type), move(_uniqueName), _context) { solAssert(m_type->category() == solidity::Type::Category::Bool, ""); } @@ -92,44 +92,44 @@ SymbolicBoolVariable::SymbolicBoolVariable( SymbolicIntVariable::SymbolicIntVariable( solidity::TypePointer _type, string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _interface) + SymbolicVariable(move(_type), move(_uniqueName), _context) { solAssert(isNumber(m_type->category()), ""); } SymbolicAddressVariable::SymbolicAddressVariable( string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ): - SymbolicIntVariable(TypeProvider::uint(160), move(_uniqueName), _interface) + SymbolicIntVariable(TypeProvider::uint(160), move(_uniqueName), _context) { } SymbolicFixedBytesVariable::SymbolicFixedBytesVariable( unsigned _numBytes, string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ): - SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), move(_uniqueName), _interface) + SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), move(_uniqueName), _context) { } SymbolicFunctionVariable::SymbolicFunctionVariable( solidity::TypePointer _type, string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _interface), - m_declaration(m_interface.newVariable(currentName(), m_sort)) + SymbolicVariable(move(_type), move(_uniqueName), _context), + m_declaration(m_context.newVariable(currentName(), m_sort)) { solAssert(m_type->category() == solidity::Type::Category::Function, ""); } void SymbolicFunctionVariable::resetDeclaration() { - m_declaration = m_interface.newVariable(currentName(), m_sort); + m_declaration = m_context.newVariable(currentName(), m_sort); } Expression SymbolicFunctionVariable::increaseIndex() @@ -147,9 +147,9 @@ Expression SymbolicFunctionVariable::operator()(vector _arguments) c SymbolicMappingVariable::SymbolicMappingVariable( solidity::TypePointer _type, string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _interface) + SymbolicVariable(move(_type), move(_uniqueName), _context) { solAssert(isMapping(m_type->category()), ""); } @@ -157,9 +157,9 @@ SymbolicMappingVariable::SymbolicMappingVariable( SymbolicArrayVariable::SymbolicArrayVariable( solidity::TypePointer _type, string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _interface) + SymbolicVariable(move(_type), move(_uniqueName), _context) { solAssert(isArray(m_type->category()), ""); } @@ -167,9 +167,9 @@ SymbolicArrayVariable::SymbolicArrayVariable( SymbolicEnumVariable::SymbolicEnumVariable( solidity::TypePointer _type, string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _interface) + SymbolicVariable(move(_type), move(_uniqueName), _context) { solAssert(isEnum(m_type->category()), ""); } @@ -177,9 +177,9 @@ SymbolicEnumVariable::SymbolicEnumVariable( SymbolicTupleVariable::SymbolicTupleVariable( solidity::TypePointer _type, string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _interface) + SymbolicVariable(move(_type), move(_uniqueName), _context) { solAssert(isTuple(m_type->category()), ""); } diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 42e3beb1e..f83936e47 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -29,6 +29,7 @@ namespace solidity namespace smt { +class EncodingContext; class Type; /** @@ -40,12 +41,12 @@ public: SymbolicVariable( solidity::TypePointer _type, std::string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ); SymbolicVariable( SortPointer _sort, std::string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ); virtual ~SymbolicVariable() = default; @@ -72,7 +73,7 @@ protected: /// Solidity type, used for size and range in number types. solidity::TypePointer m_type; std::string m_uniqueName; - SolverInterface& m_interface; + EncodingContext& m_context; std::unique_ptr m_ssa; }; @@ -85,7 +86,7 @@ public: SymbolicBoolVariable( solidity::TypePointer _type, std::string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ); }; @@ -98,7 +99,7 @@ public: SymbolicIntVariable( solidity::TypePointer _type, std::string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ); }; @@ -110,7 +111,7 @@ class SymbolicAddressVariable: public SymbolicIntVariable public: SymbolicAddressVariable( std::string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ); }; @@ -123,7 +124,7 @@ public: SymbolicFixedBytesVariable( unsigned _numBytes, std::string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ); }; @@ -136,7 +137,7 @@ public: SymbolicFunctionVariable( solidity::TypePointer _type, std::string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ); Expression increaseIndex(); @@ -159,7 +160,7 @@ public: SymbolicMappingVariable( solidity::TypePointer _type, std::string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ); }; @@ -172,7 +173,7 @@ public: SymbolicArrayVariable( solidity::TypePointer _type, std::string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ); }; @@ -185,7 +186,7 @@ public: SymbolicEnumVariable( solidity::TypePointer _type, std::string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ); }; @@ -198,7 +199,7 @@ public: SymbolicTupleVariable( solidity::TypePointer _type, std::string _uniqueName, - SolverInterface& _interface + EncodingContext& _context ); std::vector> const& components() diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json index a5e1990f5..6d85039e5 100644 --- a/test/libsolidity/smtCheckerTestsJSON/multi.json +++ b/test/libsolidity/smtCheckerTestsJSON/multi.json @@ -3,9 +3,9 @@ { "smtlib2responses": { - "0x399638a49c613bd393612f518a0bc22e9c7801791f0fa10a760b53c88686763c": "unsat\n", - "0x91c1bd0064608eae1120536e6e62864766bc370782e162d70f05d94a9f184ffc": "sat\n((|EVALEXPR_0| 1))\n", - "0x980a3db3305233a5417ea16e6253211d98818fcaa2ce7d0858f95080160092ef": "sat\n((|EVALEXPR_0| 0))\n" + "0x68fa399769cf119cbe46d5ae578164d39ea67e06eee08eeb37042d08a13a0cd8": "unsat\n", + "0xd78cd71ff120c5b5ecc5020146952f62de0506c4baef7ba499239a2ce2b14343": "sat\n((|EVALEXPR_0| 0))\n", + "0xf74672131cc6b7b3d6b82ed2fa0da2b75d01c9bc32f15d2f77e8e39e174f5a37": "sat\n((|EVALEXPR_0| 1))\n" } } } diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json index c085044c6..f390e4840 100644 --- a/test/libsolidity/smtCheckerTestsJSON/simple.json +++ b/test/libsolidity/smtCheckerTestsJSON/simple.json @@ -3,7 +3,7 @@ { "smtlib2responses": { - "0xc1ec66473d8e3b43cd320f847166c54f779e5e905085a837418d211233144dab": "sat\n((|EVALEXPR_0| 0))\n" + "0x9e377366ae857502a72974bd4e563258a29fa84dd4358cc053057544409da0ea": "sat\n((|EVALEXPR_0| 0))\n" } } }