diff options
author | chriseth <chris@ethereum.org> | 2018-10-24 20:34:17 +0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-24 20:34:17 +0800 |
commit | 01566c2e1af5b7f655fd593e5e1019e103d739a0 (patch) | |
tree | aaa2f597e4d4cb2a48e3bd5197c9222646953979 /libsolidity | |
parent | 8d01db7c2d74cbf245b995e6d13e563aff5cef65 (diff) | |
parent | e2cf5f6ed94c571c7478b9a313f8e4fceee2aec3 (diff) | |
download | dexon-solidity-01566c2e1af5b7f655fd593e5e1019e103d739a0.tar dexon-solidity-01566c2e1af5b7f655fd593e5e1019e103d739a0.tar.gz dexon-solidity-01566c2e1af5b7f655fd593e5e1019e103d739a0.tar.bz2 dexon-solidity-01566c2e1af5b7f655fd593e5e1019e103d739a0.tar.lz dexon-solidity-01566c2e1af5b7f655fd593e5e1019e103d739a0.tar.xz dexon-solidity-01566c2e1af5b7f655fd593e5e1019e103d739a0.tar.zst dexon-solidity-01566c2e1af5b7f655fd593e5e1019e103d739a0.zip |
Merge pull request #5272 from ethereum/smt_special_vars
[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash
Diffstat (limited to 'libsolidity')
-rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 115 | ||||
-rw-r--r-- | libsolidity/formal/SMTChecker.h | 16 | ||||
-rw-r--r-- | libsolidity/formal/SSAVariable.cpp | 2 | ||||
-rw-r--r-- | libsolidity/formal/SSAVariable.h | 10 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicAddressVariable.cpp | 11 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicAddressVariable.h | 1 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicBoolVariable.cpp | 6 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicBoolVariable.h | 2 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicIntVariable.cpp | 8 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicIntVariable.h | 2 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicTypes.cpp | 15 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicVariable.cpp | 6 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicVariable.h | 11 |
13 files changed, 144 insertions, 61 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 99ab2cb5..631a9eee 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -363,6 +363,10 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) visitAssert(_funCall); else if (funType.kind() == FunctionType::Kind::Require) visitRequire(_funCall); + else if (funType.kind() == FunctionType::Kind::GasLeft) + visitGasLeft(_funCall); + else if (funType.kind() == FunctionType::Kind::BlockHash) + visitBlockHash(_funCall); else if (funType.kind() == FunctionType::Kind::Internal) inlineFunctionCall(_funCall); else @@ -393,6 +397,27 @@ void SMTChecker::visitRequire(FunctionCall const& _funCall) addPathImpliedExpression(expr(*args[0])); } +void SMTChecker::visitGasLeft(FunctionCall const& _funCall) +{ + string gasLeft = "gasleft()"; + // We increase the variable index since gasleft changes + // inside a tx. + defineSpecialVariable(gasLeft, _funCall, true); + auto const& symbolicVar = m_specialVariables.at(gasLeft); + unsigned index = symbolicVar->index(); + // We set the current value to unknown anyway to add type constraints. + symbolicVar->setUnknownValue(); + if (index > 0) + m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); +} + +void SMTChecker::visitBlockHash(FunctionCall const& _funCall) +{ + string blockHash = "blockhash()"; + // TODO Define blockhash as an uninterpreted function + defineSpecialVariable(blockHash, _funCall); +} + void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) { FunctionDefinition const* _funDef = nullptr; @@ -460,7 +485,12 @@ void SMTChecker::endVisit(Identifier const& _identifier) } else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get())) { - if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require) + if ( + fun->kind() == FunctionType::Kind::Assert || + fun->kind() == FunctionType::Kind::Require || + fun->kind() == FunctionType::Kind::GasLeft || + fun->kind() == FunctionType::Kind::BlockHash + ) return; createExpr(_identifier); } @@ -468,6 +498,8 @@ void SMTChecker::endVisit(Identifier const& _identifier) { if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration)) defineExpr(_identifier, currentValue(*decl)); + else if (_identifier.name() == "now") + defineSpecialVariable(_identifier.name(), _identifier); else // TODO: handle MagicVariableDeclaration here m_errorReporter.warning( @@ -496,7 +528,7 @@ void SMTChecker::endVisit(Literal const& _literal) void SMTChecker::endVisit(Return const& _return) { - if (hasExpr(*_return.expression())) + if (knownExpr(*_return.expression())) { auto returnParams = m_functionPath.back()->returnParameters(); if (returnParams.size() > 1) @@ -509,6 +541,54 @@ void SMTChecker::endVisit(Return const& _return) } } +bool SMTChecker::visit(MemberAccess const& _memberAccess) +{ + auto const& exprType = _memberAccess.expression().annotation().type; + solAssert(exprType, ""); + if (exprType->category() == Type::Category::Magic) + { + auto identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression()); + string accessedName; + if (identifier) + accessedName = identifier->name(); + else + m_errorReporter.warning( + _memberAccess.location(), + "Assertion checker does not yet support this expression." + ); + defineSpecialVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess); + return false; + } + else + m_errorReporter.warning( + _memberAccess.location(), + "Assertion checker does not yet support this expression." + ); + + return true; +} + +void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _expr, bool _increaseIndex) +{ + if (!knownSpecialVariable(_name)) + { + auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); + m_specialVariables.emplace(_name, result.second); + result.second->setUnknownValue(); + if (result.first) + m_errorReporter.warning( + _expr.location(), + "Assertion checker does not yet support this special variable." + ); + } + else if (_increaseIndex) + m_specialVariables.at(_name)->increaseIndex(); + // The default behavior is not to increase the index since + // most of the special values stay the same throughout a tx. + defineExpr(_expr, m_specialVariables.at(_name)->currentValue()); +} + + void SMTChecker::arithmeticOperation(BinaryOperation const& _op) { switch (_op.getOperator()) @@ -681,11 +761,15 @@ void SMTChecker::checkCondition( expressionNames.push_back(_additionalValueName); } for (auto const& var: m_variables) - if (knownVariable(*var.first)) - { - expressionsToEvaluate.emplace_back(currentValue(*var.first)); - expressionNames.push_back(var.first->name()); - } + { + expressionsToEvaluate.emplace_back(currentValue(*var.first)); + expressionNames.push_back(var.first->name()); + } + for (auto const& var: m_specialVariables) + { + expressionsToEvaluate.emplace_back(var.second->currentValue()); + expressionNames.push_back(var.first); + } } smt::CheckResult result; vector<string> values; @@ -910,7 +994,7 @@ void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _varia bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { // This might be the case for multiple calls to the same function. - if (hasVariable(_varDecl)) + if (knownVariable(_varDecl)) return true; auto const& type = _varDecl.type(); solAssert(m_variables.count(&_varDecl) == 0, ""); @@ -927,11 +1011,6 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) return true; } -string SMTChecker::uniqueSymbol(Expression const& _expr) -{ - return "expr_" + to_string(_expr.id()); -} - bool SMTChecker::knownVariable(VariableDeclaration const& _decl) { return m_variables.count(&_decl); @@ -969,7 +1048,7 @@ void SMTChecker::setUnknownValue(VariableDeclaration const& _decl) smt::Expression SMTChecker::expr(Expression const& _e) { - if (!hasExpr(_e)) + if (!knownExpr(_e)) { m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." ); createExpr(_e); @@ -977,20 +1056,20 @@ smt::Expression SMTChecker::expr(Expression const& _e) return m_expressions.at(&_e)->currentValue(); } -bool SMTChecker::hasExpr(Expression const& _e) const +bool SMTChecker::knownExpr(Expression const& _e) const { return m_expressions.count(&_e); } -bool SMTChecker::hasVariable(VariableDeclaration const& _var) const +bool SMTChecker::knownSpecialVariable(string const& _var) const { - return m_variables.count(&_var); + return m_specialVariables.count(_var); } void SMTChecker::createExpr(Expression const& _e) { solAssert(_e.annotation().type, ""); - if (hasExpr(_e)) + if (knownExpr(_e)) m_expressions.at(&_e)->increaseIndex(); else { diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index f66693d2..95e01708 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -66,6 +66,7 @@ private: virtual void endVisit(Identifier const& _node) override; virtual void endVisit(Literal const& _node) override; virtual void endVisit(Return const& _node) override; + virtual bool visit(MemberAccess const& _node) override; void arithmeticOperation(BinaryOperation const& _op); void compareOperation(BinaryOperation const& _op); @@ -73,10 +74,14 @@ private: void visitAssert(FunctionCall const&); void visitRequire(FunctionCall const&); + void visitGasLeft(FunctionCall const&); + void visitBlockHash(FunctionCall const&); /// Visits the FunctionDefinition of the called function /// if available and inlines the return value. void inlineFunctionCall(FunctionCall const&); + void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false); + /// Division expression in the given type. Requires special treatment because /// of rounding for signed division. smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type); @@ -129,8 +134,6 @@ private: /// This fails if the type is not supported. bool createVariable(VariableDeclaration const& _varDecl); - static std::string uniqueSymbol(Expression const& _expr); - /// @returns true if _delc is a variable that is known at the current point, i.e. /// has a valid index bool knownVariable(VariableDeclaration const& _decl); @@ -154,10 +157,13 @@ private: /// Creates the expression (value can be arbitrary) void createExpr(Expression const& _e); /// Checks if expression was created - bool hasExpr(Expression const& _e) const; + bool knownExpr(Expression const& _e) const; /// Creates the expression and sets its value. void defineExpr(Expression const& _e, smt::Expression _value); + /// Checks if special variable was seen. + bool knownSpecialVariable(std::string const& _var) const; + /// Adds a new path condition void pushPathCondition(smt::Expression const& _e); /// Remove the last path condition @@ -172,9 +178,6 @@ private: /// Removes local variables from the context. void removeLocalVariables(); - /// Checks if VariableDeclaration was seen. - bool hasVariable(VariableDeclaration const& _e) const; - /// Copy the SSA indices of m_variables. VariableIndices copyVariableIndices(); /// Resets the variable indices. @@ -187,6 +190,7 @@ private: /// repeated calls to the same function. std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions; std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables; + std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables; std::vector<smt::Expression> m_pathConditions; ErrorReporter& m_errorReporter; diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index dbc58664..36e15508 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -28,6 +28,6 @@ SSAVariable::SSAVariable() void SSAVariable::resetIndex() { m_currentIndex = 0; - m_nextFreeIndex.reset (new int); + m_nextFreeIndex.reset (new unsigned); *m_nextFreeIndex = 1; } diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h index d357740d..46935472 100644 --- a/libsolidity/formal/SSAVariable.h +++ b/libsolidity/formal/SSAVariable.h @@ -34,19 +34,19 @@ public: void resetIndex(); /// This function returns the current index of this SSA variable. - int index() const { return m_currentIndex; } - int& index() { return m_currentIndex; } + unsigned index() const { return m_currentIndex; } + unsigned& index() { return m_currentIndex; } - int operator++() + unsigned operator++() { return m_currentIndex = (*m_nextFreeIndex)++; } private: - int m_currentIndex; + unsigned m_currentIndex; /// The next free index is a shared pointer because we want /// the copy and the copied to share it. - std::shared_ptr<int> m_nextFreeIndex; + std::shared_ptr<unsigned> m_nextFreeIndex; }; } diff --git a/libsolidity/formal/SymbolicAddressVariable.cpp b/libsolidity/formal/SymbolicAddressVariable.cpp index 68b95080..67a18540 100644 --- a/libsolidity/formal/SymbolicAddressVariable.cpp +++ b/libsolidity/formal/SymbolicAddressVariable.cpp @@ -24,18 +24,17 @@ using namespace dev; using namespace dev::solidity; SymbolicAddressVariable::SymbolicAddressVariable( - Type const& _type, string const& _uniqueName, smt::SolverInterface& _interface ): - SymbolicIntVariable(_type, _uniqueName, _interface) + SymbolicIntVariable(make_shared<IntegerType>(160), _uniqueName, _interface) { - solAssert(isAddress(_type.category()), ""); } void SymbolicAddressVariable::setUnknownValue() { - IntegerType intType{160}; - m_interface.addAssertion(currentValue() >= minValue(intType)); - m_interface.addAssertion(currentValue() <= maxValue(intType)); + auto intType = dynamic_cast<IntegerType const*>(m_type.get()); + solAssert(intType, ""); + m_interface.addAssertion(currentValue() >= minValue(*intType)); + m_interface.addAssertion(currentValue() <= maxValue(*intType)); } diff --git a/libsolidity/formal/SymbolicAddressVariable.h b/libsolidity/formal/SymbolicAddressVariable.h index 4a0f2361..3c9c379a 100644 --- a/libsolidity/formal/SymbolicAddressVariable.h +++ b/libsolidity/formal/SymbolicAddressVariable.h @@ -31,7 +31,6 @@ class SymbolicAddressVariable: public SymbolicIntVariable { public: SymbolicAddressVariable( - Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _interface ); diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp index 9c41ca9d..4d753c5c 100644 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ b/libsolidity/formal/SymbolicBoolVariable.cpp @@ -22,13 +22,13 @@ using namespace dev; using namespace dev::solidity; SymbolicBoolVariable::SymbolicBoolVariable( - Type const& _type, + TypePointer _type, string const& _uniqueName, smt::SolverInterface&_interface ): - SymbolicVariable(_type, _uniqueName, _interface) + SymbolicVariable(move(_type), _uniqueName, _interface) { - solAssert(_type.category() == Type::Category::Bool, ""); + solAssert(m_type->category() == Type::Category::Bool, ""); } smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h index 85e41b3b..438af2c6 100644 --- a/libsolidity/formal/SymbolicBoolVariable.h +++ b/libsolidity/formal/SymbolicBoolVariable.h @@ -31,7 +31,7 @@ class SymbolicBoolVariable: public SymbolicVariable { public: SymbolicBoolVariable( - Type const& _type, + TypePointer _type, std::string const& _uniqueName, smt::SolverInterface& _interface ); diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp index cf1a7486..a5939842 100644 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -24,13 +24,13 @@ using namespace dev; using namespace dev::solidity; SymbolicIntVariable::SymbolicIntVariable( - Type const& _type, + TypePointer _type, string const& _uniqueName, smt::SolverInterface& _interface ): - SymbolicVariable(_type, _uniqueName, _interface) + SymbolicVariable(move(_type), _uniqueName, _interface) { - solAssert(isNumber(_type.category()), ""); + solAssert(isNumber(m_type->category()), ""); } smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const @@ -45,7 +45,7 @@ void SymbolicIntVariable::setZeroValue() void SymbolicIntVariable::setUnknownValue() { - auto intType = dynamic_cast<IntegerType const*>(&m_type); + auto intType = dynamic_cast<IntegerType const*>(m_type.get()); solAssert(intType, ""); m_interface.addAssertion(currentValue() >= minValue(*intType)); m_interface.addAssertion(currentValue() <= maxValue(*intType)); diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h index 110ebb09..a9e51b1b 100644 --- a/libsolidity/formal/SymbolicIntVariable.h +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -31,7 +31,7 @@ class SymbolicIntVariable: public SymbolicVariable { public: SymbolicIntVariable( - Type const& _type, + TypePointer _type, std::string const& _uniqueName, smt::SolverInterface& _interface ); diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index d47869db..7e5db7bd 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -43,27 +43,28 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable( { bool abstract = false; shared_ptr<SymbolicVariable> var; + TypePointer type = _type.shared_from_this(); if (!isSupportedType(_type)) { abstract = true; - var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver); + var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver); } else if (isBool(_type.category())) - var = make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver); + var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _solver); else if (isFunction(_type.category())) - var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver); + var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver); else if (isInteger(_type.category())) - var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver); + var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver); else if (isAddress(_type.category())) - var = make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver); + var = make_shared<SymbolicAddressVariable>(_uniqueName, _solver); else if (isRational(_type.category())) { auto rational = dynamic_cast<RationalNumberType const*>(&_type); solAssert(rational, ""); if (rational->isFractional()) - var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver); + var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver); else - var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver); + var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver); } else solAssert(false, ""); diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp index c042ec48..530564d2 100644 --- a/libsolidity/formal/SymbolicVariable.cpp +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -24,18 +24,18 @@ using namespace dev; using namespace dev::solidity; SymbolicVariable::SymbolicVariable( - Type const& _type, + TypePointer _type, string const& _uniqueName, smt::SolverInterface& _interface ): - m_type(_type), + m_type(move(_type)), m_uniqueName(_uniqueName), m_interface(_interface), m_ssa(make_shared<SSAVariable>()) { } -string SymbolicVariable::uniqueSymbol(int _index) const +string SymbolicVariable::uniqueSymbol(unsigned _index) const { return m_uniqueName + "_" + to_string(_index); } diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h index 417e1f92..e554139f 100644 --- a/libsolidity/formal/SymbolicVariable.h +++ b/libsolidity/formal/SymbolicVariable.h @@ -39,10 +39,11 @@ class SymbolicVariable { public: SymbolicVariable( - Type const& _type, + TypePointer _type, std::string const& _uniqueName, smt::SolverInterface& _interface ); + virtual ~SymbolicVariable() = default; smt::Expression currentValue() const @@ -58,8 +59,8 @@ public: return currentValue(); } - int index() const { return m_ssa->index(); } - int& index() { return m_ssa->index(); } + unsigned index() const { return m_ssa->index(); } + unsigned& index() { return m_ssa->index(); } /// Sets the var to the default value of its type. /// Inherited types must implement. @@ -69,9 +70,9 @@ public: virtual void setUnknownValue() {} protected: - std::string uniqueSymbol(int _index) const; + std::string uniqueSymbol(unsigned _index) const; - Type const& m_type; + TypePointer m_type = nullptr; std::string m_uniqueName; smt::SolverInterface& m_interface; std::shared_ptr<SSAVariable> m_ssa = nullptr; |