diff options
23 files changed, 272 insertions, 78 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; diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index c7e60256..195004cb 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -133,23 +133,6 @@ BOOST_AUTO_TEST_CASE(assignment_in_declaration) CHECK_SUCCESS_NO_WARNINGS(text); } -BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars) -{ - string text = R"( - contract C { - function g() public pure {} - function f() public view { - uint a = 3; - this.g(); - assert(a == 3); - g(); - assert(a == 3); - } - } - )"; - CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call"); -} - BOOST_AUTO_TEST_CASE(branches_merge_variables) { // Branch does not touch variable a diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol new file mode 100644 index 00000000..d0f263eb --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public payable { + assert(blockhash(2) > 0); + } +} +// ---- +// Warning: (86-98): Assertion checker does not yet support this special variable. +// Warning: (86-98): Assertion checker does not yet implement this type. +// Warning: (86-102): Assertion checker does not yet implement the type bytes32 for comparisons +// Warning: (86-102): Internal error: Expression undefined for SMT solver. +// Warning: (79-103): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/difficulty.sol b/test/libsolidity/smtCheckerTests/special/difficulty.sol new file mode 100644 index 00000000..4469d4e5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/difficulty.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint difficulty) public view { + assert(block.difficulty == difficulty); + } +} +// ---- +// Warning: (91-129): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/gasleft.sol b/test/libsolidity/smtCheckerTests/special/gasleft.sol new file mode 100644 index 00000000..857230fe --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/gasleft.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public view { + assert(gasleft() > 0); + uint g = gasleft(); + assert(g < gasleft()); + assert(g >= gasleft()); + } +} +// ---- +// Warning: (76-97): Assertion violation happens here +// Warning: (123-144): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/many.sol b/test/libsolidity/smtCheckerTests/special/many.sol new file mode 100644 index 00000000..40e5d987 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/many.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public payable { + assert(msg.sender == block.coinbase); + assert(block.difficulty == block.gaslimit); + assert(block.number == block.timestamp); + assert(tx.gasprice == msg.value); + assert(tx.origin == msg.sender); + uint x = block.number; + assert(x + 2 > block.number); + assert(now > 10); + assert(gasleft() > 100); + } +} +// ---- +// Warning: (79-115): Assertion violation happens here +// Warning: (119-161): Assertion violation happens here +// Warning: (165-204): Assertion violation happens here +// Warning: (208-240): Assertion violation happens here +// Warning: (244-275): Assertion violation happens here +// Warning: (311-316): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (336-352): Assertion violation happens here +// Warning: (356-379): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/msg_data.sol b/test/libsolidity/smtCheckerTests/special/msg_data.sol new file mode 100644 index 00000000..7e748f09 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_data.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public payable { + assert(msg.data.length > 0); + } +} +// ---- +// Warning: (86-101): Assertion checker does not yet support this expression. +// Warning: (86-94): Assertion checker does not yet support this special variable. +// Warning: (86-94): Assertion checker does not yet implement this type. +// Warning: (86-101): Internal error: Expression undefined for SMT solver. +// Warning: (79-106): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol new file mode 100644 index 00000000..dd2366e2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public view { + address a = msg.sender; + address b = msg.sender; + assert(a == b); + } +} diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol new file mode 100644 index 00000000..ad45d076 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public view { + require(msg.sender != address(0)); + address a = msg.sender; + address b = msg.sender; + assert(a == b); + } +} +// ---- +// Warning: (98-108): Assertion checker does not yet implement this expression. +// Warning: (98-108): Internal error: Expression undefined for SMT solver. diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol new file mode 100644 index 00000000..9a4eefd5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(address c) public view { + address a = msg.sender; + address b = msg.sender; + assert(a == b); + assert(c == msg.sender); + } +} +// ---- +// Warning: (155-178): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/msg_sig.sol b/test/libsolidity/smtCheckerTests/special/msg_sig.sol new file mode 100644 index 00000000..6f832179 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_sig.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public payable { + assert(msg.sig == 0x00000000); + } +} +// ---- +// Warning: (86-93): Assertion checker does not yet support this special variable. +// Warning: (86-93): Assertion checker does not yet implement this type. +// Warning: (86-107): Assertion checker does not yet implement the type bytes4 for comparisons +// Warning: (86-107): Internal error: Expression undefined for SMT solver. +// Warning: (79-108): Assertion violation happens here |