cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #9113 from ethereum/smt_chc_overflow

Browse Source 
[SMTChecker] Add underflow/overflow target to CHC
This commit is contained in:
chriseth 2020-08-20 13:17:00 +02:00 committed by GitHub
commit 4dc63875f9
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
74 changed files with 395 additions and 124 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -5,6 +5,7 @@ Language Features:
Compiler Features:
* SMTChecker: Add underflow and overflow as verification conditions in the CHC engine.
* Standard JSON Interface: Do not run EVM bytecode code generation, if only Yul IR or EWasm output is requested.
* Yul: Report error when using non-string literals for ``datasize()``, ``dataoffset()``, ``linkersymbol()``, ``loadimmutable()``, ``setimmutable()``.
* Yul Optimizer: LoopInvariantCodeMotion can move reading operations outside for-loops as long as the affected area is not modified inside the loop.

64
libsolidity/formal/BMC.cpp
View File

@ -499,8 +499,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
);
@ -606,12 +635,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,
@ -632,13 +668,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,

145
libsolidity/formal/CHC.cpp
View File

@ -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);
}
}
}
}

10
libsolidity/formal/CHC.h
View File

@ -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.

1
libsolidity/formal/SMTEncoder.cpp
View File

@ -1084,7 +1084,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);

2
test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
View File

@ -9,4 +9,4 @@ contract C {
}
}
// ----
// Warning 2529: (111-121): Empty array "pop" detected here
// Warning 2529: (111-121): Empty array "pop" detected here.

2
test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
View File

@ -10,5 +10,5 @@ contract C {
}
}
// ----
// Warning 3944: (162-177): Underflow (resulting value less than 0) happens here
// Warning 6328: (150-184): Assertion violation happens here
// Warning 4144: (162-177): Underflow (resulting value less than 0) happens here

2
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol
View File

@ -12,5 +12,5 @@ contract C {
}
}
// ----
// Warning 3944: (217-232): Underflow (resulting value less than 0) happens here
// Warning 6328: (205-239): Assertion violation happens here
// Warning 4144: (217-232): Underflow (resulting value less than 0) happens here

3
test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol
View File

@ -53,5 +53,4 @@ contract MyConc{
// ----
// Warning 2519: (773-792): This declaration shadows an existing declaration.
// Warning 2018: (1009-1086): Function state mutability can be restricted to view
// Warning 6084: (985-1002): Underflow (resulting value less than 0) happens here.
// Warning 6084: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/control_flow/short_circuit_and.sol
View File

@ -15,4 +15,3 @@ contract c {
}
}
// ----
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol
View File

@ -16,4 +16,3 @@ contract c {
}
// ----
// Warning 6328: (227-236): Assertion violation happens here
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol
View File

@ -19,4 +19,3 @@ contract c {
// ----
// Warning 6328: (202-218): Assertion violation happens here
// Warning 6328: (242-252): Assertion violation happens here
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both.sol
View File

@ -15,4 +15,3 @@ contract c {
}
}
// ----
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol
View File

@ -16,4 +16,3 @@ contract c {
}
// ----
// Warning 6328: (225-235): Assertion violation happens here
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/control_flow/short_circuit_or.sol
View File

@ -15,4 +15,3 @@ contract c {
}
}
// ----
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol
View File

@ -16,4 +16,3 @@ contract c {
}
// ----
// Warning 6328: (225-235): Assertion violation happens here
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol
View File

@ -25,4 +25,3 @@ contract c {
}
// ----
// Warning 6328: (360-370): Assertion violation happens here
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both.sol
View File

@ -15,4 +15,3 @@ contract c {
}
}
// ----
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol
View File

@ -16,4 +16,3 @@ contract c {
}
// ----
// Warning 6328: (225-235): Assertion violation happens here
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

4
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol
View File

@ -19,6 +19,6 @@ contract A is B {
}
}
// ----
// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (244-249): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (232-250): Assertion violation happens here
// Warning 2661: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (244-249): Overflow (resulting value larger than 2**256 - 1) happens here

6
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
View File

@ -18,6 +18,6 @@ contract A is B {
}
}
// ----
// Warning 2661: (207-212): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (198-203): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (230-235): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (198-203): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (207-212): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (230-235): Overflow (resulting value larger than 2**256 - 1) happens here

5
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol
View File

@ -25,7 +25,6 @@ contract A is B2, B1 {
}
}
// ----
// Warning 4984: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (302-320): Assertion violation happens here
// Warning 2661: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here

5
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol
View File

@ -25,7 +25,6 @@ contract A is B2, B1 {
}
}
// ----
// Warning 4984: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (302-320): Assertion violation happens here
// Warning 2661: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here

10
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
View File

@ -27,11 +27,7 @@ contract A is B2, B1 {
}
}
// ----
// Warning 4984: (160-165): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (225-230): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (241-246): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (334-350): Assertion violation happens here
// Warning 4144: (160-165): Underflow (resulting value less than 0) happens here
// Warning 2661: (160-165): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (225-230): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (241-246): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (225-230): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (241-246): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (160-165): Overflow (resulting value larger than 2**256 - 1) happens here

3
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol
View File

@ -25,6 +25,5 @@ contract A is B {
}
}
// ----
// Warning 4984: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (328-342): Assertion violation happens here
// Warning 2661: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here

2
test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
View File

@ -13,5 +13,5 @@ contract C {
}
}
// ----
// Warning 4984: (115-120): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (162-176): Assertion violation happens here
// Warning 2661: (115-120): Overflow (resulting value larger than 2**256 - 1) happens here

3
test/libsolidity/smtCheckerTests/functions/internal_call_state_var_init_2.sol
View File

@ -7,6 +7,3 @@ contract c {
bool b = (f() > 0) || (f() > 0);
}
// ----
// Warning 2661: (100-105): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4144: (100-105): Underflow (resulting value less than 0) happens here
// Warning 2661: (100-105): Overflow (resulting value larger than 2**256 - 1) happens here

5
test/libsolidity/smtCheckerTests/functions/library_constant.sol
View File

@ -20,7 +20,6 @@ contract C {
}
// ----
// Warning 6328: (136-155): Assertion violation happens here
// Warning 2661: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (327-332): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 8364: (300-302): Assertion checker does not yet implement type type(library l1)
// Warning 2661: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (327-332): Overflow (resulting value larger than 2**256 - 1) happens here

3
test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_mixed_chain_with_params.sol
View File

@ -25,6 +25,5 @@ contract A is B {
}
}
// ----
// Warning 4984: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (328-342): Assertion violation happens here
// Warning 2661: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here

14
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol
View File

@ -22,12 +22,10 @@ contract A is B {
}
// ----
// Warning 4984: (157-162): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (216-221): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (261-270): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (287-292): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (275-293): Assertion violation happens here
// Warning 4144: (157-162): Underflow (resulting value less than 0) happens here
// Warning 2661: (157-162): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (216-221): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (157-162): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (261-270): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (287-292): Overflow (resulting value larger than 2**256 - 1) happens here

11
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol
View File

@ -22,10 +22,9 @@ contract A is B {
}
// ----
// Warning 4984: (157-163): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (217-222): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (240-245): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (262-268): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (285-290): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (273-291): Assertion violation happens here
// Warning 2661: (157-163): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (217-222): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (157-163): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (240-245): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (262-268): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 2661: (285-290): Overflow (resulting value larger than 2**256 - 1) happens here

4
test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol
View File

@ -5,7 +5,6 @@ contract C
function f(uint x) public pure {
require(x < 100);
do {
// Overflows due to resetting x.
x = x + 1;
} while (x < 10);
assert(x < 14);
@ -14,5 +13,4 @@ contract C
// ====
// SMTSolvers: z3
// ----
// Warning 6328: (179-193): Assertion violation happens here
// Warning 2661: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (143-157): Assertion violation happens here

5
test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol
View File

@ -5,15 +5,10 @@ contract C
function f(uint x) public pure {
require(x < 100);
do {
// Overflows due to resetting x.
x = x + 1;
} while (x < 1000);
// The assertion is true but we can't infer so
// because x is touched in the loop.
assert(x > 0);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning 2661: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
View File

@ -14,5 +14,6 @@ contract C
// ====
// SMTSolvers: z3
// ----
// Warning 1218: (176-181): Error trying to invoke SMT solver.
// Warning 6328: (189-203): Assertion violation happens here
// Warning 2661: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
View File

@ -19,6 +19,7 @@ contract LoopFor2 {
// ====
// SMTSolvers: z3
// ----
// Warning 1218: (244-249): Error trying to invoke SMT solver.
// Warning 6328: (281-301): Assertion violation happens here
// Warning 6328: (305-324): Assertion violation happens here
// Warning 6328: (328-347): Assertion violation happens here

1
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
View File

@ -23,5 +23,6 @@ contract LoopFor2 {
// ====
// SMTSolvers: z3
// ----
// Warning 1218: (237-242): Error trying to invoke SMT solver.
// Warning 6328: (362-382): Assertion violation happens here
// Warning 6328: (409-428): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol
View File

@ -21,5 +21,5 @@ contract C
}
}
// ----
// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (136-149): Assertion violation happens here
// Warning 2661: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol
View File

@ -15,4 +15,3 @@ contract C
}
}
// ----
// Warning 2661: (145-150): Overflow (resulting value larger than 2**256 - 1) happens here

8
test/libsolidity/smtCheckerTests/operators/div_zero.sol Normal file
View File

@ -0,0 +1,8 @@
pragma experimental SMTChecker;
contract C {
uint z = 0;
uint x = 2 / z;
}
// ----
// Warning 6084: (69-74): Division by zero happens here.

1
test/libsolidity/smtCheckerTests/operators/division_3.sol
View File

@ -6,4 +6,5 @@ contract C {
}
}
// ----
// Warning 1218: (127-132): Error trying to invoke SMT solver.
// Warning 2661: (127-132): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here

2
test/libsolidity/smtCheckerTests/operators/division_4.sol
View File

@ -6,3 +6,5 @@ contract C {
return x / y;
}
}
// ----
// Warning 1218: (147-152): Error trying to invoke SMT solver.

2
test/libsolidity/smtCheckerTests/operators/division_5.sol
View File

@ -9,3 +9,5 @@ contract C {
return c;
}
}
// ----
// Warning 1218: (151-156): Error trying to invoke SMT solver.

2
test/libsolidity/smtCheckerTests/operators/division_6.sol
View File

@ -11,3 +11,5 @@ contract C {
return c;
}
}
// ----
// Warning 1218: (265-270): Error trying to invoke SMT solver.

1
test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol
View File

@ -7,4 +7,5 @@ contract C {
}
}
// ----
// Warning 1218: (112-117): Error trying to invoke SMT solver.
// Warning 1218: (105-123): Error trying to invoke SMT solver.

1
test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol
View File

@ -7,4 +7,5 @@ contract C {
}
}
// ----
// Warning 1218: (113-118): Error trying to invoke SMT solver.
// Warning 1218: (106-125): Error trying to invoke SMT solver.

1
test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol
View File

@ -7,4 +7,5 @@ contract C {
}
}
// ----
// Warning 1218: (113-118): Error trying to invoke SMT solver.
// Warning 1218: (106-125): Error trying to invoke SMT solver.

1
test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol
View File

@ -7,4 +7,5 @@ contract C {
}
}
// ----
// Warning 1218: (114-119): Error trying to invoke SMT solver.
// Warning 1218: (107-125): Error trying to invoke SMT solver.

3
test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol
View File

@ -6,7 +6,6 @@ contract test {
}
// ----
// Warning 2072: (80-88): Unused local variable.
// Warning 4984: (91-112): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 5084: (91-100): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (103-112): Type conversion is not yet fully supported and might yield false positives.
// Warning 4144: (91-112): Underflow (resulting value less than 0) happens here
// Warning 2661: (91-112): Overflow (resulting value larger than 2**256 - 1) happens here

2
test/libsolidity/smtCheckerTests/operators/fixed_point_compound_add.sol
View File

@ -4,5 +4,3 @@ contract C {
function f() internal { b[0] += 1; }
}
// ----
// Warning 4144: (84-93): Underflow (resulting value less than 0) happens here
// Warning 2661: (84-93): Overflow (resulting value larger than 2**256 - 1) happens here

1
test/libsolidity/smtCheckerTests/operators/mod_even.sol
View File

@ -9,4 +9,5 @@ contract C
}
}
// ----
// Warning 1218: (113-118): Error trying to invoke SMT solver.
// Warning 1218: (122-142): Error trying to invoke SMT solver.

4
test/libsolidity/smtCheckerTests/overflow/overflow_mul.sol
View File

@ -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

4
test/libsolidity/smtCheckerTests/overflow/overflow_mul_signed.sol
View File

@ -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

4
test/libsolidity/smtCheckerTests/overflow/overflow_sum.sol
View File

@ -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

6
test/libsolidity/smtCheckerTests/overflow/overflow_sum_signed.sol
View File

@ -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

11
test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
function f(int x, int y) public pure returns (int) {
return x / y;
}
}
// ----
// Warning 1218: (110-115): Error trying to invoke SMT solver.
// Warning 3046: (110-115): Division by zero happens here
// Warning 2661: (110-115): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here

10
test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
function f(int x, int y) public pure returns (int) {
require(x >= y);
return x - y;
}
}
// ----
// Warning 4984: (129-134): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here

11
test/libsolidity/smtCheckerTests/overflow/signed_guard_sum_overflow.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
function f(int x, int y) public pure returns (int) {
require(x + y >= x);
return x + y;
}
}
// ----
// Warning 3944: (111-116): Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here
// Warning 3944: (133-138): Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here

9
test/libsolidity/smtCheckerTests/overflow/signed_mod_overflow.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f(int x, int y) public pure returns (int) {
return x % y;
}
}
// ----
// Warning 3046: (110-115): Division by zero happens here

10
test/libsolidity/smtCheckerTests/overflow/signed_mul_overflow.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
function f(int x, int y) public pure returns (int) {
return x * y;
}
}
// ----
// Warning 3944: (110-115): Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here
// Warning 4984: (110-115): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here

10
test/libsolidity/smtCheckerTests/overflow/signed_sub_overflow.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
function f(int x, int y) public pure returns (int) {
return x - y;
}
}
// ----
// Warning 3944: (110-115): Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here
// Warning 4984: (110-115): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here

10
test/libsolidity/smtCheckerTests/overflow/signed_sum_overflow.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
function f(int x, int y) public pure returns (int) {
return x + y;
}
}
// ----
// Warning 3944: (110-115): Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here
// Warning 4984: (110-115): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here

2
test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol
View File

@ -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

4
test/libsolidity/smtCheckerTests/overflow/underflow_sub.sol
View File

@ -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

6
test/libsolidity/smtCheckerTests/overflow/underflow_sub_signed.sol
View File

@ -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

9
test/libsolidity/smtCheckerTests/overflow/unsigned_div_overflow.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f(uint x, uint y) public pure returns (uint) {
return x / y;
}
}
// ----
// Warning 3046: (113-118): Division by zero happens here

8
test/libsolidity/smtCheckerTests/overflow/unsigned_guard_sub_overflow.sol Normal file
View File

@ -0,0 +1,8 @@
pragma experimental SMTChecker;
contract C {
function f(uint x, uint y) public pure returns (uint) {
require(x >= y);
return x - y;
}
}

8
test/libsolidity/smtCheckerTests/overflow/unsigned_guard_sum_overflow.sol Normal file
View File

@ -0,0 +1,8 @@
pragma experimental SMTChecker;
contract C {
function f(uint x, uint y) public pure returns (uint) {
require(x + y >= x);
return x + y;
}
}

9
test/libsolidity/smtCheckerTests/overflow/unsigned_mod_overflow.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f(uint x, uint y) public pure returns (uint) {
return x % y;
}
}
// ----
// Warning 3046: (113-118): Division by zero happens here

9
test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f(uint x, uint y) public pure returns (uint) {
return x * y;
}
}
// ----
// Warning 4984: (113-118): Overflow (resulting value larger than 2**256 - 1) happens here

9
test/libsolidity/smtCheckerTests/overflow/unsigned_sub_overflow.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f(uint x, uint y) public pure returns (uint) {
return x - y;
}
}
// ----
// Warning 3944: (113-118): Underflow (resulting value less than 0) happens here

9
test/libsolidity/smtCheckerTests/overflow/unsigned_sum_overflow.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f(uint x, uint y) public pure returns (uint) {
return x + y;
}
}
// ----
// Warning 4984: (113-118): Overflow (resulting value larger than 2**256 - 1) happens here

2
test/libsolidity/smtCheckerTests/special/many.sol
View File

@ -15,6 +15,7 @@ contract C
}
}
// ----
// Warning 4984: (311-316): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (79-115): Assertion violation happens here
// Warning 6328: (119-161): Assertion violation happens here
// Warning 6328: (165-204): Assertion violation happens here
@ -23,4 +24,3 @@ contract C
// Warning 6328: (304-332): Assertion violation happens here
// Warning 6328: (336-364): Assertion violation happens here
// Warning 6328: (368-391): Assertion violation happens here
// Warning 2661: (311-316): Overflow (resulting value larger than 2**256 - 1) happens here

2
test/libsolidity/smtCheckerTests/types/address_balance.sol
View File

@ -9,5 +9,5 @@ contract C
}
// ----
// Warning 2072: (96-102): Unused local variable.
// Warning 4984: (105-127): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 6328: (131-160): Assertion violation happens here
// Warning 2661: (105-127): Overflow (resulting value larger than 2**256 - 1) happens here

2
test/libsolidity/smtCheckerTests/types/tuple_declarations_function_2.sol
View File

@ -15,4 +15,4 @@ contract C
}
}
// ----
// Warning 2661: (152-157): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4984: (152-157): Overflow (resulting value larger than 2**256 - 1) happens here