diff --git a/Changelog.md b/Changelog.md index fbaddb36f..3a0456855 100644 --- a/Changelog.md +++ b/Changelog.md @@ -4,6 +4,7 @@ Language Features: Compiler Features: + * SMTChecker: Do not report underflow/overflow if they always revert. This removes false positives when using ``SafeMath``. * Static Analyzer: Warn about expressions with custom types when they have no effect. diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 78591ad69..a9e3c171f 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -21,7 +21,6 @@ #include #include -#include #include #include @@ -109,6 +108,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function) m_expressions.clear(); m_globalContext.clear(); m_uninterpretedTerms.clear(); + m_overflowTargets.clear(); resetStateVariables(); initializeLocalVariables(_function); m_loopExecutionHappened = false; @@ -126,7 +126,10 @@ void SMTChecker::endVisit(FunctionDefinition const&) // Otherwise we remove any local variables from the context and // keep the state variables. if (isRootFunction()) + { + checkUnderOverflow(); removeLocalVariables(); + } m_functionPath.pop_back(); } @@ -316,21 +319,56 @@ void SMTChecker::endVisit(TupleExpression const& _tuple) defineExpr(_tuple, expr(*_tuple.components()[0])); } -void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location) +void SMTChecker::addOverflowTarget( + OverflowTarget::Type _type, + TypePointer _intType, + smt::Expression _value, + SourceLocation const& _location +) { - checkCondition( - _value < minValue(_type), - _location, - "Underflow (resulting value less than " + formatNumberReadable(_type.minValue()) + ")", - "", - &_value + m_overflowTargets.emplace_back( + _type, + std::move(_intType), + std::move(_value), + currentPathConditions(), + _location ); +} + +void SMTChecker::checkUnderOverflow() +{ + for (auto& target: m_overflowTargets) + { + if (target.type != OverflowTarget::Type::Overflow) + checkUnderflow(target); + if (target.type != OverflowTarget::Type::Underflow) + checkOverflow(target); + } +} + +void SMTChecker::checkUnderflow(OverflowTarget& _target) +{ + solAssert(_target.type != OverflowTarget::Type::Overflow, ""); + auto intType = dynamic_cast(_target.intType.get()); checkCondition( - _value > maxValue(_type), - _location, - "Overflow (resulting value larger than " + formatNumberReadable(_type.maxValue()) + ")", + _target.path && _target.value < minValue(*intType), + _target.location, + "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")", "", - &_value + &_target.value + ); +} + +void SMTChecker::checkOverflow(OverflowTarget& _target) +{ + solAssert(_target.type != OverflowTarget::Type::Underflow, ""); + auto intType = dynamic_cast(_target.intType.get()); + checkCondition( + _target.path && _target.value > maxValue(*intType), + _target.location, + "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")", + "", + &_target.value ); } @@ -376,8 +414,13 @@ void SMTChecker::endVisit(UnaryOperation const& _op) case Token::Sub: // - { defineExpr(_op, 0 - expr(_op.subExpression())); - if (auto intType = dynamic_cast(_op.annotation().type.get())) - checkUnderOverflow(expr(_op), *intType, _op.location()); + if (dynamic_cast(_op.annotation().type.get())) + addOverflowTarget( + OverflowTarget::Type::All, + _op.annotation().type, + expr(_op), + _op.location() + ); break; } default: @@ -853,9 +896,28 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) m_interface->addAssertion(right != 0); } - checkUnderOverflow(value, intType, _op.location()); + addOverflowTarget( + OverflowTarget::Type::All, + _op.annotation().commonType, + value, + _op.location() + ); + + smt::Expression intValueRange = (0 - minValue(intType)) + maxValue(intType) + 1; + defineExpr(_op, smt::Expression::ite( + value > maxValue(intType) || value < minValue(intType), + value % intValueRange, + value + )); + if (intType.isSigned()) + { + defineExpr(_op, smt::Expression::ite( + expr(_op) > maxValue(intType), + expr(_op) - intValueRange, + expr(_op) + )); + } - defineExpr(_op, value); break; } default: @@ -944,10 +1006,10 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, Expression con void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location) { TypePointer type = _variable.type(); - if (auto const* intType = dynamic_cast(type.get())) - checkUnderOverflow(_value, *intType, _location); + if (dynamic_cast(type.get())) + addOverflowTarget(OverflowTarget::Type::All, type, _value, _location); else if (dynamic_cast(type.get())) - checkUnderOverflow(_value, IntegerType(160), _location); + addOverflowTarget(OverflowTarget::Type::All, make_shared(160), _value, _location); else if (dynamic_cast(type.get())) arrayAssignment(); m_interface->addAssertion(newValue(_variable) == _value); diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 1521c613b..ccb7e1e4d 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -137,9 +137,33 @@ private: Expression const& _condition, std::string const& _description ); - /// Checks that the value is in the range given by the type. - void checkUnderOverflow(smt::Expression _value, IntegerType const& _Type, langutil::SourceLocation const& _location); + struct OverflowTarget + { + enum class Type { Underflow, Overflow, All } type; + TypePointer intType; + smt::Expression value; + smt::Expression path; + langutil::SourceLocation const& location; + + OverflowTarget(Type _type, TypePointer _intType, smt::Expression _value, smt::Expression _path, langutil::SourceLocation const& _location): + type(_type), + intType(_intType), + value(_value), + path(_path), + location(_location) + { + solAssert(dynamic_cast(intType.get()), ""); + } + }; + + /// Checks that the value is in the range given by the type. + void checkUnderflow(OverflowTarget& _target); + void checkOverflow(OverflowTarget& _target); + /// Calls the functions above for all elements in m_overflowTargets accordingly. + void checkUnderOverflow(); + /// Adds an overflow target for lazy check at the end of the function. + void addOverflowTarget(OverflowTarget::Type _type, TypePointer _intType, smt::Expression _value, langutil::SourceLocation const& _location); std::pair> checkSatisfiableAndGenerateModel(std::vector const& _expressionsToEvaluate); @@ -244,6 +268,8 @@ private: bool isRootFunction(); /// Returns true if _funDef was already visited. bool visitedFunction(FunctionDefinition const* _funDef); + + std::vector m_overflowTargets; }; } diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol index df6eaaa7e..747f4b37a 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol @@ -12,6 +12,5 @@ contract C } } // ---- -// Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here -// Warning: (146-155): Overflow (resulting value larger than 2**256 - 1) happens here // Warning: (179-193): Assertion violation happens here +// Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol index 49a1e0a58..1710d0af2 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol +++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol @@ -14,6 +14,5 @@ contract C } } // ---- -// Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here -// Warning: (146-155): Overflow (resulting value larger than 2**256 - 1) happens here // Warning: (269-282): Assertion violation happens here +// Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol index 2be01c2d5..6293aa58b 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol @@ -12,6 +12,9 @@ contract C } } // ---- -// Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here -// Warning: (172-181): Overflow (resulting value larger than 2**256 - 1) happens here // 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 c8232ab63..8ee1fa32e 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol @@ -13,6 +13,9 @@ contract C } } // ---- -// Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here -// Warning: (172-181): Overflow (resulting value larger than 2**256 - 1) happens here // 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 4d082026d..aa4ae6e85 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol @@ -8,3 +8,5 @@ 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 eb62d36ed..cdd70b9a6 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol @@ -10,3 +10,5 @@ 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 b0c3cae4c..73ade8c20 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol @@ -11,3 +11,5 @@ 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 6184c441f..5e8119a72 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol @@ -11,3 +11,5 @@ 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 eec59ded8..af5747dcc 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol @@ -16,3 +16,5 @@ 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 diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_mul.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_mul.sol new file mode 100644 index 000000000..4d9177180 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_mul.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint8 x) public pure returns (uint8) { + x = 100; + uint8 y = x * 3; + assert(y == 44); + x = 128; + y = x * 4; + assert(y == 0); + return y; + } +} +// ---- +// Warning: (120-125): Overflow (resulting value larger than 255) happens here +// Warning: (163-168): Overflow (resulting value larger than 255) happens here diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_mul_signed.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_mul_signed.sol new file mode 100644 index 000000000..5dc11647e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_mul_signed.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(int8 x) public pure returns (int8) { + x = 100; + int8 y = x * 2; + assert(y == -56); + y = x * 100; + assert(y == 16); + return y; + } +} +// ---- +// Warning: (117-122): Overflow (resulting value larger than 127) happens here +// Warning: (150-157): Overflow (resulting value larger than 127) happens here diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_sum.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_sum.sol new file mode 100644 index 000000000..1f19f56fa --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_sum.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint8 x) public pure returns (uint8) { + uint8 y = x + 255; + require(y >= x); + x = 255; + y = x + 1; + assert(y == 0); + y = x + 255; + assert(y == 254); + return y; + } +} +// ---- +// Warning: (154-159): Overflow (resulting value larger than 255) happens here +// Warning: (185-192): Overflow (resulting value larger than 255) happens here diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_sum_signed.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_sum_signed.sol new file mode 100644 index 000000000..09ebb5944 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_sum_signed.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(int8 x) public pure returns (int8) { + x = 127; + int8 y = x + 1; + assert(y == -128); + y = x + 127; + assert(y == -2); + x = -127; + y = x + -127; + assert(y == 2); + } +} +// ---- +// Warning: (117-122): Overflow (resulting value larger than 127) happens here +// Warning: (151-158): Overflow (resulting value larger than 127) happens here +// Warning: (197-205): Underflow (resulting value less than -128) happens here diff --git a/test/libsolidity/smtCheckerTests/overflow/safe_add_1.sol b/test/libsolidity/smtCheckerTests/overflow/safe_add_1.sol new file mode 100644 index 000000000..97e7ea343 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/safe_add_1.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; + +contract C +{ + function add(uint x, uint y) public pure returns (uint) { + require(x + y >= x); + return x + y; + } +} diff --git a/test/libsolidity/smtCheckerTests/overflow/safe_add_2.sol b/test/libsolidity/smtCheckerTests/overflow/safe_add_2.sol new file mode 100644 index 000000000..9b64a8885 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/safe_add_2.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function add(uint x, uint y) public pure returns (uint) { + uint z = x + y; + require(z >= x); + return z; + } +} diff --git a/test/libsolidity/smtCheckerTests/overflow/safe_div_1.sol b/test/libsolidity/smtCheckerTests/overflow/safe_div_1.sol new file mode 100644 index 000000000..42a0324a4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/safe_div_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function div(uint256 a, uint256 b) internal pure returns (uint256) { + require(b > 0); + uint256 c = a / b; + return c; + } +} diff --git a/test/libsolidity/smtCheckerTests/overflow/safe_mul_1.sol b/test/libsolidity/smtCheckerTests/overflow/safe_mul_1.sol new file mode 100644 index 000000000..c93108304 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/safe_mul_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + function mul(uint256 a, uint256 b) internal pure returns (uint256) { + uint256 c; + if (a != 0) { + c = a * b; + require(c / a == b); + } + return c; + } +} diff --git a/test/libsolidity/smtCheckerTests/overflow/safe_mul_2.sol b/test/libsolidity/smtCheckerTests/overflow/safe_mul_2.sol new file mode 100644 index 000000000..b85d368c2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/safe_mul_2.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C +{ + function mul(uint256 a, uint256 b) internal pure returns (uint256) { + if (a == 0) { + return 0; + } + uint256 c = a * b; + require(c / a == b); + return c; + } +} +// ---- +// Warning: (180-185): Division by zero happens here diff --git a/test/libsolidity/smtCheckerTests/overflow/safe_sub_1.sol b/test/libsolidity/smtCheckerTests/overflow/safe_sub_1.sol new file mode 100644 index 000000000..d618aa136 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/safe_sub_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function sub(uint256 a, uint256 b) internal pure returns (uint256) { + require(b <= a); + uint256 c = a - b; + return c; + } +} diff --git a/test/libsolidity/smtCheckerTests/overflow/underflow_sub.sol b/test/libsolidity/smtCheckerTests/overflow/underflow_sub.sol new file mode 100644 index 000000000..d41cfaa71 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/underflow_sub.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint8 x) public pure returns (uint) { + x = 0; + uint8 y = x - 1; + assert(y == 255); + y = x - 255; + assert(y == 1); + return y; + } +} +// ---- +// Warning: (117-122): Underflow (resulting value less than 0) happens here +// Warning: (150-157): Underflow (resulting value less than 0) happens here diff --git a/test/libsolidity/smtCheckerTests/overflow/underflow_sub_signed.sol b/test/libsolidity/smtCheckerTests/overflow/underflow_sub_signed.sol new file mode 100644 index 000000000..40416498d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/underflow_sub_signed.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(int8 x) public pure returns (int8) { + x = -2; + int8 y = x - 127; + assert(y == 127); + x = -128; + y = x - 127; + assert(y == 1); + x = 127; + y = x - (-127); + assert(y == -2); + return y; + } +} +// ---- +// Warning: (116-123): Underflow (resulting value less than -128) happens here +// Warning: (163-170): Underflow (resulting value less than -128) happens here +// Warning: (207-217): Overflow (resulting value larger than 127) happens here diff --git a/test/libsolidity/smtCheckerTests/special/many.sol b/test/libsolidity/smtCheckerTests/special/many.sol index ae60b1e5b..e9ef98b26 100644 --- a/test/libsolidity/smtCheckerTests/special/many.sol +++ b/test/libsolidity/smtCheckerTests/special/many.sol @@ -20,6 +20,6 @@ contract C // 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 2**256 - 1) happens here +// Warning: (304-332): Assertion violation happens here // Warning: (336-352): Assertion violation happens here // Warning: (356-379): Assertion violation happens here