mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #9067 from ethereum/smt_fix_fp_again
[SMTChecker] Fix BMC targets with FP
This commit is contained in:
commit
731e6466a0
@ -604,7 +604,11 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression con
|
||||
_target.type == VerificationTarget::Type::UnderOverflow,
|
||||
""
|
||||
);
|
||||
auto intType = dynamic_cast<IntegerType const*>(_target.expression->annotation().type);
|
||||
IntegerType const* intType = nullptr;
|
||||
if (auto const* type = dynamic_cast<IntegerType const*>(_target.expression->annotation().type))
|
||||
intType = type;
|
||||
else
|
||||
intType = TypeProvider::uint256();
|
||||
solAssert(intType, "");
|
||||
checkCondition(
|
||||
_target.constraints && _constraints && _target.value < smt::minValue(*intType),
|
||||
@ -626,7 +630,12 @@ void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression cons
|
||||
_target.type == VerificationTarget::Type::UnderOverflow,
|
||||
""
|
||||
);
|
||||
auto intType = dynamic_cast<IntegerType const*>(_target.expression->annotation().type);
|
||||
IntegerType const* intType = nullptr;
|
||||
if (auto const* type = dynamic_cast<IntegerType const*>(_target.expression->annotation().type))
|
||||
intType = type;
|
||||
else
|
||||
intType = TypeProvider::uint256();
|
||||
|
||||
solAssert(intType, "");
|
||||
checkCondition(
|
||||
_target.constraints && _constraints && _target.value > smt::maxValue(*intType),
|
||||
|
@ -1213,7 +1213,7 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
|
||||
{
|
||||
auto type = _op.annotation().commonType;
|
||||
solAssert(type, "");
|
||||
if (type->category() == Type::Category::Integer)
|
||||
if (type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint)
|
||||
{
|
||||
switch (_op.getOperator())
|
||||
{
|
||||
@ -1266,13 +1266,21 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
|
||||
};
|
||||
solAssert(validOperators.count(_op), "");
|
||||
solAssert(_commonType, "");
|
||||
solAssert(_commonType->category() == Type::Category::Integer, "");
|
||||
solAssert(
|
||||
_commonType->category() == Type::Category::Integer || _commonType->category() == Type::Category::FixedPoint,
|
||||
""
|
||||
);
|
||||
|
||||
IntegerType const* intType = nullptr;
|
||||
if (auto type = dynamic_cast<IntegerType const*>(_commonType))
|
||||
intType = type;
|
||||
else
|
||||
intType = TypeProvider::uint256();
|
||||
|
||||
auto const& intType = dynamic_cast<IntegerType const&>(*_commonType);
|
||||
smtutil::Expression valueNoMod(
|
||||
_op == Token::Add ? _left + _right :
|
||||
_op == Token::Sub ? _left - _right :
|
||||
_op == Token::Div ? division(_left, _right, intType) :
|
||||
_op == Token::Div ? division(_left, _right, *intType) :
|
||||
_op == Token::Mul ? _left * _right :
|
||||
/*_op == Token::Mod*/ _left % _right
|
||||
);
|
||||
@ -1280,20 +1288,23 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
|
||||
if (_op == Token::Div || _op == Token::Mod)
|
||||
m_context.addAssertion(_right != 0);
|
||||
|
||||
smtutil::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1;
|
||||
auto symbMin = smt::minValue(*intType);
|
||||
auto symbMax = smt::maxValue(*intType);
|
||||
|
||||
smtutil::Expression intValueRange = (0 - symbMin) + symbMax + 1;
|
||||
auto value = smtutil::Expression::ite(
|
||||
valueNoMod > smt::maxValue(intType),
|
||||
valueNoMod > symbMax,
|
||||
valueNoMod % intValueRange,
|
||||
smtutil::Expression::ite(
|
||||
valueNoMod < smt::minValue(intType),
|
||||
valueNoMod < symbMin,
|
||||
valueNoMod % intValueRange,
|
||||
valueNoMod
|
||||
)
|
||||
);
|
||||
|
||||
if (intType.isSigned())
|
||||
if (intType->isSigned())
|
||||
value = smtutil::Expression::ite(
|
||||
value > smt::maxValue(intType),
|
||||
value > symbMax,
|
||||
value - intValueRange,
|
||||
value
|
||||
);
|
||||
|
@ -0,0 +1,12 @@
|
||||
pragma experimental SMTChecker;
|
||||
contract test {
|
||||
function f() internal pure {
|
||||
ufixed a = uint64(1) + ufixed(2);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning: (80-88): Unused local variable.
|
||||
// Warning: (91-100): Type conversion is not yet fully supported and might yield false positives.
|
||||
// Warning: (103-112): Type conversion is not yet fully supported and might yield false positives.
|
||||
// Warning: (91-112): Underflow (resulting value less than 0) happens here
|
||||
// Warning: (91-112): Overflow (resulting value larger than 2**256 - 1) happens here
|
@ -0,0 +1,8 @@
|
||||
pragma experimental SMTChecker;
|
||||
contract C {
|
||||
fixed[] b;
|
||||
function f() internal { b[0] += 1; }
|
||||
}
|
||||
// ----
|
||||
// Warning: (84-93): Underflow (resulting value less than 0) happens here
|
||||
// Warning: (84-93): Overflow (resulting value larger than 2**256 - 1) happens here
|
Loading…
Reference in New Issue
Block a user