mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
[SMTChecker] Add underflow/overflow target to CHC
This commit is contained in:
parent
b1fb9da63a
commit
8a06041bbe
@ -498,8 +498,37 @@ pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
|
||||
|
||||
auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
|
||||
|
||||
auto const* intType = dynamic_cast<IntegerType const*>(_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<IntegerType const*>(_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<IntegerType const*>(_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<IntegerType const*>(_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<IntegerType const*>(_target.expression->annotation().type);
|
||||
if (!intType)
|
||||
intType = TypeProvider::uint256();
|
||||
|
||||
solAssert(intType, "");
|
||||
checkCondition(
|
||||
_target.constraints && _constraints && _target.value > smt::maxValue(*intType),
|
||||
_target.callStack,
|
||||
|
@ -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<smtutil::Expression> 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<smtutil::Expression, smtutil::Expression> 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<IntegerType const*>(_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<smtutil::Expression> 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<Expression const*>(scope);
|
||||
solAssert(expr, "");
|
||||
auto const* intType = dynamic_cast<IntegerType const*>(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);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -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<smtutil::Expression, smtutil::Expression> 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<smtutil::CheckResult, smtutil::CHCSolverInterface::CexGraph> 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.
|
||||
|
@ -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);
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
Loading…
Reference in New Issue
Block a user