diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 484a3afaf..cb17aab41 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -96,7 +96,7 @@ void SMTChecker::endVisit(ContractDefinition const&) void SMTChecker::endVisit(VariableDeclaration const& _varDecl) { if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value()) - assignment(_varDecl, *_varDecl.value(), _varDecl.location()); + assignment(_varDecl, *_varDecl.value()); } bool SMTChecker::visit(ModifierDefinition const&) @@ -346,14 +346,14 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl) declarations.at(i) && m_context.knownVariable(*declarations.at(i)) ) - assignment(*declarations.at(i), components.at(i)->currentValue(), declarations.at(i)->location()); + assignment(*declarations.at(i), components.at(i)->currentValue()); } } } else if (m_context.knownVariable(*_varDecl.declarations().front())) { if (_varDecl.initialValue()) - assignment(*_varDecl.declarations().front(), *_varDecl.initialValue(), _varDecl.location()); + assignment(*_varDecl.declarations().front(), *_varDecl.initialValue()); } else m_errorReporter.warning( @@ -540,7 +540,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op) auto innerValue = currentValue(*decl); auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1; defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue); - assignment(*decl, newValue, _op.location()); + assignment(*decl, newValue); } else if (dynamic_cast(&_op.subExpression())) { @@ -554,6 +554,14 @@ void SMTChecker::endVisit(UnaryOperation const& _op) _op.location(), "Assertion checker does not yet implement such increments / decrements." ); + + addOverflowTarget( + _op.getOperator() == Token::Inc ? OverflowTarget::Type::Overflow : OverflowTarget::Type::Underflow, + _op.annotation().type, + expr(_op), + _op.location() + ); + break; } case Token::Sub: // - @@ -1336,7 +1344,7 @@ void SMTChecker::assignment( else if (auto varDecl = identifierToVariable(_left)) { solAssert(_right.size() == 1, ""); - assignment(*varDecl, _right.front(), _location); + assignment(*varDecl, _right.front()); } else if (dynamic_cast(&_left)) { @@ -1382,19 +1390,15 @@ smt::Expression SMTChecker::compoundAssignment(Assignment const& _assignment) ); } -void SMTChecker::assignment(VariableDeclaration const& _variable, Expression const& _value, SourceLocation const& _location) +void SMTChecker::assignment(VariableDeclaration const& _variable, Expression const& _value) { - assignment(_variable, expr(_value), _location); + assignment(_variable, expr(_value)); } -void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location) +void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expression const& _value) { TypePointer type = _variable.type(); - if (type->category() == Type::Category::Integer) - addOverflowTarget(OverflowTarget::Type::All, type, _value, _location); - else if (type->category() == Type::Category::Address) - addOverflowTarget(OverflowTarget::Type::All, TypeProvider::uint(160), _value, _location); - else if (type->category() == Type::Category::Mapping) + if (type->category() == Type::Category::Mapping) arrayAssignment(); m_interface->addAssertion(m_context.newValue(_variable) == _value); } diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index c3e973528..14fa4f4d6 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -140,9 +140,9 @@ private: /// of rounding for signed division. smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type); - void assignment(VariableDeclaration const& _variable, Expression const& _value, langutil::SourceLocation const& _location); + void assignment(VariableDeclaration const& _variable, Expression const& _value); /// Handles assignments to variables of different types. - void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, langutil::SourceLocation const& _location); + void assignment(VariableDeclaration const& _variable, smt::Expression const& _value); /// Handles assignments between generic expressions. /// Will also be used for assignments of tuple components. void assignment( diff --git a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol index dc9c9c846..ece92ee0c 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol @@ -87,8 +87,6 @@ contract InternalCall { // Warning: (782-813): Type conversion is not yet fully supported and might yield false positives. // Warning: (771-814): Assertion checker does not yet implement this type of function call. // Warning: (825-830): Assertion checker does not yet support the type of this variable. -// Warning: (690-750): Underflow (resulting value less than 0) happens here -// Warning: (690-750): Overflow (resulting value larger than 2**160 - 1) happens here // Warning: (1057-1068): Assertion checker does not yet implement type function () returns (uint256) // Warning: (1120-1131): Assertion checker does not yet implement type function () returns (uint256) // Warning: (1403-1408): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol index 6293aa58b..54a9465c9 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol @@ -15,6 +15,4 @@ contract C // Warning: (189-203): Assertion violation happens here // Warning: (176-181): Underflow (resulting value less than 0) happens here // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here -// Warning: (172-181): Underflow (resulting value less than 0) happens here -// Warning: (172-181): Overflow (resulting value larger than 2**256 - 1) happens here // Warning: (126-129): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol index 8ee1fa32e..2562effaa 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol @@ -16,6 +16,4 @@ contract C // Warning: (244-257): Assertion violation happens here // Warning: (176-181): Underflow (resulting value less than 0) happens here // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here -// Warning: (172-181): Underflow (resulting value less than 0) happens here -// Warning: (172-181): Overflow (resulting value larger than 2**256 - 1) happens here // Warning: (126-129): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol index aa4ae6e85..4d082026d 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol @@ -8,5 +8,3 @@ contract C { } // ---- // Warning: (136-150): Assertion violation happens here -// Warning: (115-120): Underflow (resulting value less than 0) happens here -// Warning: (115-120): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol index cdd70b9a6..eb62d36ed 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol @@ -10,5 +10,3 @@ contract C { } // ---- // Warning: (167-181): Assertion violation happens here -// Warning: (142-147): Underflow (resulting value less than 0) happens here -// Warning: (142-147): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol index 73ade8c20..b0c3cae4c 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol @@ -11,5 +11,3 @@ contract C { } // ---- // Warning: (213-226): Assertion violation happens here -// Warning: (142-147): Underflow (resulting value less than 0) happens here -// Warning: (142-147): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol index 5e8119a72..6184c441f 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol @@ -11,5 +11,3 @@ contract C { } // ---- // Warning: (138-144): For loop condition is always true. -// Warning: (161-166): Underflow (resulting value less than 0) happens here -// Warning: (161-166): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol index af5747dcc..eec59ded8 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol @@ -16,5 +16,3 @@ contract C { // ---- // Warning: (115-121): Unused local variable. // Warning: (356-370): Assertion violation happens here -// Warning: (285-290): Underflow (resulting value less than 0) happens here -// Warning: (285-290): Overflow (resulting value larger than 2**256 - 1) happens here