diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 69165841b..255f7c2ac 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -498,8 +498,37 @@ pair BMC::arithmeticOperation( auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression); + auto const* intType = dynamic_cast(_commonType); + if (!intType) + intType = TypeProvider::uint256(); + + // Mod does not need underflow/overflow checks. + if (_op == Token::Mod) + return values; + + VerificationTarget::Type type; + // The order matters here: + // If _op is Div and intType is signed, we only care about overflow. + if (_op == Token::Div) + { + if (intType->isSigned()) + // Signed division can only overflow. + type = VerificationTarget::Type::Overflow; + else + // Unsigned division cannot underflow/overflow. + return values; + } + else if (intType->isSigned()) + type = VerificationTarget::Type::UnderOverflow; + else if (_op == Token::Sub) + type = VerificationTarget::Type::Underflow; + else if (_op == Token::Add || _op == Token::Mul) + type = VerificationTarget::Type::Overflow; + else + solAssert(false, ""); + addVerificationTarget( - VerificationTarget::Type::UnderOverflow, + type, values.second, &_expression ); @@ -605,12 +634,19 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression con _target.type == VerificationTarget::Type::UnderOverflow, "" ); - IntegerType const* intType = nullptr; - if (auto const* type = dynamic_cast(_target.expression->annotation().type)) - intType = type; - else + + if ( + m_solvedTargets.count(_target.expression) && ( + m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::Underflow) || + m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::UnderOverflow) + ) + ) + return; + + auto const* intType = dynamic_cast(_target.expression->annotation().type); + if (!intType) intType = TypeProvider::uint256(); - solAssert(intType, ""); + checkCondition( _target.constraints && _constraints && _target.value < smt::minValue(*intType), _target.callStack, @@ -631,13 +667,19 @@ void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression cons _target.type == VerificationTarget::Type::UnderOverflow, "" ); - IntegerType const* intType = nullptr; - if (auto const* type = dynamic_cast(_target.expression->annotation().type)) - intType = type; - else + + if ( + m_solvedTargets.count(_target.expression) && ( + m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::Overflow) || + m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::UnderOverflow) + ) + ) + return; + + auto const* intType = dynamic_cast(_target.expression->annotation().type); + if (!intType) intType = TypeProvider::uint256(); - solAssert(intType, ""); checkCondition( _target.constraints && _constraints && _target.value > smt::maxValue(*intType), _target.callStack, diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 304754529..b69306727 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -147,7 +147,7 @@ void CHC::endVisit(ContractDefinition const& _contract) else inlineConstructorHierarchy(_contract); - connectBlocks(m_currentBlock, summary(_contract), m_error.currentValue() == 0); + connectBlocks(m_currentBlock, summary(_contract)); clearIndices(m_currentContract, nullptr); vector symbArgs = currentFunctionVariables(*m_currentContract); @@ -452,6 +452,9 @@ void CHC::endVisit(FunctionCall const& _funCall) case FunctionType::Kind::BareCallCode: case FunctionType::Kind::BareDelegateCall: case FunctionType::Kind::Creation: + SMTEncoder::endVisit(_funCall); + unknownFunctionCall(_funCall); + break; case FunctionType::Kind::KECCAK256: case FunctionType::Kind::ECRecover: case FunctionType::Kind::SHA256: @@ -459,9 +462,7 @@ void CHC::endVisit(FunctionCall const& _funCall) case FunctionType::Kind::BlockHash: case FunctionType::Kind::AddMod: case FunctionType::Kind::MulMod: - SMTEncoder::endVisit(_funCall); - unknownFunctionCall(_funCall); - break; + [[fallthrough]]; default: SMTEncoder::endVisit(_funCall); break; @@ -601,14 +602,74 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) auto previousError = m_error.currentValue(); m_error.increaseIndex(); - addArrayPopVerificationTarget(&_arrayPop, m_error.currentValue()); - connectBlocks( - m_currentBlock, - m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction), - currentPathConditions() && symbArray->length() <= 0 && m_error.currentValue() == newErrorId(_arrayPop) + addVerificationTarget(&_arrayPop, VerificationTarget::Type::PopEmptyArray, m_error.currentValue()); + + smtutil::Expression target = (symbArray->length() <= 0) && (m_error.currentValue() == newErrorId(_arrayPop)); + m_context.addAssertion((m_error.currentValue() == previousError) || target); +} + +pair CHC::arithmeticOperation( + Token _op, + smtutil::Expression const& _left, + smtutil::Expression const& _right, + TypePointer const& _commonType, + frontend::Expression const& _expression +) +{ + auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression); + + IntegerType const* intType = nullptr; + if (auto const* type = dynamic_cast(_commonType)) + intType = type; + else + intType = TypeProvider::uint256(); + + // Mod does not need underflow/overflow checks. + // Div only needs overflow check for signed types. + if (_op == Token::Mod || (_op == Token::Div && !intType->isSigned())) + return values; + + auto previousError = m_error.currentValue(); + m_error.increaseIndex(); + + VerificationTarget::Type targetType; + unsigned errorId = newErrorId(_expression); + + optional target; + if (_op == Token::Div) + { + targetType = VerificationTarget::Type::Overflow; + target = values.second > intType->maxValue() && m_error.currentValue() == errorId; + } + else if (intType->isSigned()) + { + unsigned secondErrorId = newErrorId(_expression); + targetType = VerificationTarget::Type::UnderOverflow; + target = (values.second < intType->minValue() && m_error.currentValue() == errorId) || + (values.second > intType->maxValue() && m_error.currentValue() == secondErrorId); + } + else if (_op == Token::Sub) + { + targetType = VerificationTarget::Type::Underflow; + target = values.second < intType->minValue() && m_error.currentValue() == errorId; + } + else if (_op == Token::Add || _op == Token::Mul) + { + targetType = VerificationTarget::Type::Overflow; + target = values.second > intType->maxValue() && m_error.currentValue() == errorId; + } + else + solAssert(false, ""); + + addVerificationTarget( + &_expression, + targetType, + m_error.currentValue() ); - m_context.addAssertion(m_error.currentValue() == previousError); + m_context.addAssertion((m_error.currentValue() == previousError) || *target); + + return values; } void CHC::resetSourceAnalysis() @@ -1174,26 +1235,25 @@ void CHC::addVerificationTarget( m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId}); } -void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId) -{ - addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId); -} - -void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smtutil::Expression _errorId) +void CHC::addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _errorId) { solAssert(m_currentContract, ""); - solAssert(m_currentFunction, ""); - if (m_currentFunction->isConstructor()) - addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, summary(*m_currentContract), smtutil::Expression(true), _errorId); + if (!m_currentFunction || m_currentFunction->isConstructor()) + addVerificationTarget(_scope, _type, summary(*m_currentContract), smtutil::Expression(true), _errorId); else { auto iface = (*m_interfaces.at(m_currentContract))(initialStateVariables()); auto sum = summary(*m_currentFunction); - addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, iface, sum, _errorId); + addVerificationTarget(_scope, _type, iface, sum, _errorId); } } +void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId) +{ + addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId); +} + void CHC::checkVerificationTargets() { for (auto const& [scope, target]: m_verificationTargets) @@ -1203,8 +1263,12 @@ void CHC::checkVerificationTargets() else { string satMsg; + string satMsgUnderflow; + string satMsgOverflow; string unknownMsg; ErrorId errorReporterId; + ErrorId underflowErrorId = 3944_error; + ErrorId overflowErrorId = 4984_error; if (target.type == VerificationTarget::Type::PopEmptyArray) { @@ -1213,12 +1277,51 @@ void CHC::checkVerificationTargets() unknownMsg = "Empty array \"pop\" might happen here."; errorReporterId = 2529_error; } + else if ( + target.type == VerificationTarget::Type::Underflow || + target.type == VerificationTarget::Type::Overflow || + target.type == VerificationTarget::Type::UnderOverflow + ) + { + auto const* expr = dynamic_cast(scope); + solAssert(expr, ""); + auto const* intType = dynamic_cast(expr->annotation().type); + if (!intType) + intType = TypeProvider::uint256(); + + satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ") happens here"; + satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ") happens here"; + if (target.type == VerificationTarget::Type::Underflow) + { + satMsg = satMsgUnderflow; + errorReporterId = underflowErrorId; + } + else if (target.type == VerificationTarget::Type::Overflow) + { + satMsg = satMsgOverflow; + errorReporterId = overflowErrorId; + } + } else solAssert(false, ""); auto it = m_errorIds.find(scope->id()); solAssert(it != m_errorIds.end(), ""); - checkAndReportTarget(scope, target, it->second, errorReporterId, satMsg, unknownMsg); + unsigned errorId = it->second; + + if (target.type != VerificationTarget::Type::UnderOverflow) + checkAndReportTarget(scope, target, errorId, errorReporterId, satMsg, unknownMsg); + else + { + auto specificTarget = target; + specificTarget.type = VerificationTarget::Type::Underflow; + checkAndReportTarget(scope, specificTarget, errorId, underflowErrorId, satMsgUnderflow, unknownMsg); + + ++it; + solAssert(it != m_errorIds.end(), ""); + specificTarget.type = VerificationTarget::Type::Overflow; + checkAndReportTarget(scope, specificTarget, it->second, overflowErrorId, satMsgOverflow, unknownMsg); + } } } } diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 8342524bb..ac1315317 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -84,6 +84,14 @@ private: void externalFunctionCall(FunctionCall const& _funCall); void unknownFunctionCall(FunctionCall const& _funCall); void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override; + /// Creates underflow/overflow verification targets. + std::pair arithmeticOperation( + Token _op, + smtutil::Expression const& _left, + smtutil::Expression const& _right, + TypePointer const& _commonType, + Expression const& _expression + ) override; //@} struct IdCompare @@ -197,8 +205,8 @@ private: std::pair query(smtutil::Expression const& _query, langutil::SourceLocation const& _location); void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId); + void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _errorId); void addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId); - void addArrayPopVerificationTarget(ASTNode const* _scope, smtutil::Expression _errorId); void checkVerificationTargets(); // Forward declaration. Definition is below. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 50ede6d13..78711c52f 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1083,7 +1083,6 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall) auto oldElements = symbArray->elements(); auto oldLength = symbArray->length(); - m_context.addAssertion(oldLength > 0); symbArray->increaseIndex(); m_context.addAssertion(symbArray->elements() == oldElements); diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_mul.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_mul.sol index 86697dea0..05b15987f 100644 --- a/test/libsolidity/smtCheckerTests/overflow/overflow_mul.sol +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_mul.sol @@ -13,5 +13,5 @@ contract C } } // ---- -// Warning 2661: (120-125): Overflow (resulting value larger than 255) happens here -// Warning 2661: (163-168): Overflow (resulting value larger than 255) happens here +// Warning 4984: (120-125): Overflow (resulting value larger than 255) happens here +// Warning 4984: (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 index 7663fa34e..7a71a7d2f 100644 --- a/test/libsolidity/smtCheckerTests/overflow/overflow_mul_signed.sol +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_mul_signed.sol @@ -12,5 +12,5 @@ contract C } } // ---- -// Warning 2661: (117-122): Overflow (resulting value larger than 127) happens here -// Warning 2661: (150-157): Overflow (resulting value larger than 127) happens here +// Warning 4984: (117-122): Overflow (resulting value larger than 127) happens here +// Warning 4984: (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 index 3eb3fd13f..c94b09b97 100644 --- a/test/libsolidity/smtCheckerTests/overflow/overflow_sum.sol +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_sum.sol @@ -14,5 +14,5 @@ contract C } } // ---- -// Warning 2661: (154-159): Overflow (resulting value larger than 255) happens here -// Warning 2661: (185-192): Overflow (resulting value larger than 255) happens here +// Warning 4984: (154-159): Overflow (resulting value larger than 255) happens here +// Warning 4984: (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 index 7e9938c74..8fc6b4997 100644 --- a/test/libsolidity/smtCheckerTests/overflow/overflow_sum_signed.sol +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_sum_signed.sol @@ -14,6 +14,6 @@ contract C } } // ---- -// Warning 2661: (117-122): Overflow (resulting value larger than 127) happens here -// Warning 2661: (151-158): Overflow (resulting value larger than 127) happens here -// Warning 4144: (197-205): Underflow (resulting value less than -128) happens here +// Warning 4984: (117-122): Overflow (resulting value larger than 127) happens here +// Warning 4984: (151-158): Overflow (resulting value larger than 127) happens here +// Warning 3944: (197-205): Underflow (resulting value less than -128) happens here diff --git a/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol index 117554eca..41ba3d0d5 100644 --- a/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol @@ -3,4 +3,4 @@ contract C { function f(uint a, uint b) public pure returns (uint) { return a + b; } } // ---- -// Warning 2661: (112-117): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning 4984: (112-117): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/overflow/underflow_sub.sol b/test/libsolidity/smtCheckerTests/overflow/underflow_sub.sol index 1029e90a5..1ecf1e870 100644 --- a/test/libsolidity/smtCheckerTests/overflow/underflow_sub.sol +++ b/test/libsolidity/smtCheckerTests/overflow/underflow_sub.sol @@ -12,5 +12,5 @@ contract C } } // ---- -// Warning 4144: (117-122): Underflow (resulting value less than 0) happens here -// Warning 4144: (150-157): Underflow (resulting value less than 0) happens here +// Warning 3944: (117-122): Underflow (resulting value less than 0) happens here +// Warning 3944: (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 index 84634a213..6dab43c79 100644 --- a/test/libsolidity/smtCheckerTests/overflow/underflow_sub_signed.sol +++ b/test/libsolidity/smtCheckerTests/overflow/underflow_sub_signed.sol @@ -16,6 +16,6 @@ contract C } } // ---- -// Warning 4144: (116-123): Underflow (resulting value less than -128) happens here -// Warning 4144: (163-170): Underflow (resulting value less than -128) happens here -// Warning 2661: (207-217): Overflow (resulting value larger than 127) happens here +// Warning 3944: (116-123): Underflow (resulting value less than -128) happens here +// Warning 3944: (163-170): Underflow (resulting value less than -128) happens here +// Warning 4984: (207-217): Overflow (resulting value larger than 127) happens here