cerc-io/solidity
16
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 #10661 from ethereum/smt_checked

Browse Source 
[SMTChecker] Checked arithmetic and unchecked blocks
This commit is contained in:
Đorđe Mijović 2020-12-30 16:00:31 +01:00 committed by GitHub
commit 1837e0ae7f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
74 changed files with 765 additions and 614 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -6,6 +6,7 @@ Language Features:
Compiler Features:
* Parser: Report meaningful error if parsing a version pragma failed.
* SMTChecker: Support ABI functions as uninterpreted functions.
* SMTChecker: Use checked arithmetic by default and support ``unchecked`` blocks.
Bugfixes:
* Code Generator: Fix length check when decoding malformed error data in catch clause.

32
libsolidity/formal/BMC.cpp
View File

@ -137,8 +137,7 @@ void BMC::endVisit(ContractDefinition const& _contract)
inlineConstructorHierarchy(_contract);
popCallStack();
/// Check targets created by state variable initialization.
smtutil::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
checkVerificationTargets();
m_verificationTargets.clear();
}
@ -175,8 +174,7 @@ void BMC::endVisit(FunctionDefinition const& _function)
{
if (isRootFunction())
{
smtutil::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
checkVerificationTargets();
m_verificationTargets.clear();
m_pathConditions.clear();
}
@ -534,6 +532,7 @@ pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
Expression const& _expression
)
{
// Unchecked does not disable div by 0 checks.
if (_op == Token::Div || _op == Token::Mod)
addVerificationTarget(
VerificationTarget::Type::DivByZero,
@ -543,6 +542,9 @@ pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
if (!m_checked)
return values;
auto const* intType = dynamic_cast<IntegerType const*>(_commonType);
if (!intType)
intType = TypeProvider::uint256();
@ -625,13 +627,13 @@ pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
/// Verification targets.
void BMC::checkVerificationTargets(smtutil::Expression const& _constraints)
void BMC::checkVerificationTargets()
{
for (auto& target: m_verificationTargets)
checkVerificationTarget(target, _constraints);
checkVerificationTarget(target);
}
void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smtutil::Expression const& _constraints)
void BMC::checkVerificationTarget(BMCVerificationTarget& _target)
{
switch (_target.type)
{
@ -639,14 +641,14 @@ void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smtutil::Expre
checkConstantCondition(_target);
break;
case VerificationTarget::Type::Underflow:
checkUnderflow(_target, _constraints);
checkUnderflow(_target);
break;
case VerificationTarget::Type::Overflow:
checkOverflow(_target, _constraints);
checkOverflow(_target);
break;
case VerificationTarget::Type::UnderOverflow:
checkUnderflow(_target, _constraints);
checkOverflow(_target, _constraints);
checkUnderflow(_target);
checkOverflow(_target);
break;
case VerificationTarget::Type::DivByZero:
checkDivByZero(_target);
@ -672,7 +674,7 @@ void BMC::checkConstantCondition(BMCVerificationTarget& _target)
);
}
void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints)
void BMC::checkUnderflow(BMCVerificationTarget& _target)
{
solAssert(
_target.type == VerificationTarget::Type::Underflow ||
@ -693,7 +695,7 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression con
intType = TypeProvider::uint256();
checkCondition(
_target.constraints && _constraints && _target.value < smt::minValue(*intType),
_target.constraints && _target.value < smt::minValue(*intType),
_target.callStack,
_target.modelExpressions,
_target.expression->location(),
@ -705,7 +707,7 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression con
);
}
void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints)
void BMC::checkOverflow(BMCVerificationTarget& _target)
{
solAssert(
_target.type == VerificationTarget::Type::Overflow ||
@ -726,7 +728,7 @@ void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression cons
intType = TypeProvider::uint256();
checkCondition(
_target.constraints && _constraints && _target.value > smt::maxValue(*intType),
_target.constraints && _target.value > smt::maxValue(*intType),
_target.callStack,
_target.modelExpressions,
_target.expression->location(),

8
libsolidity/formal/BMC.h
View File

@ -130,11 +130,11 @@ private:
std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> modelExpressions;
};
void checkVerificationTargets(smtutil::Expression const& _constraints);
void checkVerificationTarget(BMCVerificationTarget& _target, smtutil::Expression const& _constraints = smtutil::Expression(true));
void checkVerificationTargets();
void checkVerificationTarget(BMCVerificationTarget& _target);
void checkConstantCondition(BMCVerificationTarget& _target);
void checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints);
void checkOverflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints);
void checkUnderflow(BMCVerificationTarget& _target);
void checkOverflow(BMCVerificationTarget& _target);
void checkDivByZero(BMCVerificationTarget& _target);
void checkBalance(BMCVerificationTarget& _target);
void checkAssert(BMCVerificationTarget& _target);

4
libsolidity/formal/CHC.cpp
View File

@ -732,11 +732,15 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
frontend::Expression const& _expression
)
{
// Unchecked does not disable div by 0 checks.
if (_op == Token::Mod || _op == Token::Div)
verificationTargetEncountered(&_expression, VerificationTarget::Type::DivByZero, _right == 0);
auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
if (!m_checked)
return values;
IntegerType const* intType = nullptr;
if (auto const* type = dynamic_cast<IntegerType const*>(_commonType))
intType = type;

34
libsolidity/formal/SMTEncoder.cpp
View File

@ -283,6 +283,25 @@ void SMTEncoder::endVisit(FunctionDefinition const&)
m_context.popSolver();
}
bool SMTEncoder::visit(Block const& _block)
{
if (_block.unchecked())
{
solAssert(m_checked, "");
m_checked = false;
}
return true;
}
void SMTEncoder::endVisit(Block const& _block)
{
if (_block.unchecked())
{
solAssert(!m_checked, "");
m_checked = true;
}
}
bool SMTEncoder::visit(InlineAssembly const& _inlineAsm)
{
m_errorReporter.warning(
@ -745,6 +764,7 @@ void SMTEncoder::initContract(ContractDefinition const& _contract)
createStateVariables(_contract);
clearIndices(m_currentContract, nullptr);
m_variableUsage.setCurrentContract(_contract);
m_checked = true;
}
void SMTEncoder::initFunction(FunctionDefinition const& _function)
@ -759,6 +779,7 @@ void SMTEncoder::initFunction(FunctionDefinition const& _function)
createLocalVariables(_function);
m_arrayAssignmentHappened = false;
clearIndices(m_currentContract, &_function);
m_checked = true;
}
void SMTEncoder::visitAssert(FunctionCall const& _funCall)
@ -1762,6 +1783,9 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
}
}();
if (m_checked)
return {valueUnbounded, valueUnbounded};
if (_op == Token::Div || _op == Token::Mod)
{
// mod and unsigned division never underflow/overflow
@ -2385,6 +2409,16 @@ void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value)
createExpr(_e);
solAssert(_value.sort->kind != smtutil::Kind::Function, "Equality operator applied to type that is not fully supported");
m_context.addAssertion(expr(_e) == _value);
if (
auto type = _e.annotation().type;
m_checked && smt::isNumber(*type)
)
m_context.addAssertion(smtutil::Expression::implies(
currentPathConditions(),
smt::symbolicUnknownConstraints(expr(_e), type)
));
}
void SMTEncoder::popPathCondition()

7
libsolidity/formal/SMTEncoder.h
View File

@ -103,6 +103,8 @@ protected:
bool visit(ModifierDefinition const& _node) override;
bool visit(FunctionDefinition const& _node) override;
void endVisit(FunctionDefinition const& _node) override;
bool visit(Block const& _node) override;
void endVisit(Block const& _node) override;
bool visit(PlaceholderStatement const& _node) override;
bool visit(IfStatement const&) override { return false; }
bool visit(WhileStatement const&) override { return false; }
@ -358,6 +360,11 @@ protected:
/// Used to retrieve models.
std::set<Expression const*> m_uninterpretedTerms;
std::vector<smtutil::Expression> m_pathConditions;
/// Whether the currently visited block uses checked
/// or unchecked arithmetic.
bool m_checked = true;
/// Local SMTEncoder ErrorReporter.
/// This is necessary to show the "No SMT solver available"
/// warning before the others in case it's needed.

4
test/cmdlineTests/standard_model_checker_engine_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0xfb59e2e8177462af35c799138353d20a1d92e6078fa64073c48e01b66c94e568":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x058094a9af015b518e634e27c9b42140d8b77dd0f915986a1e2fbed694cdb7de":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -17,7 +17,7 @@
(declare-fun |expr_9_0| () Int)
(declare-fun |expr_10_1| () Bool)
(assert (and (and (and true true) (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (= expr_9_0 0) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))) (not expr_10_1)))
(assert (and (and (and true true) (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (implies (and true true) true) (and (= expr_9_0 0) (and (implies (and true true) (and (>= expr_8_0 0) (<= expr_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))) (not expr_10_1)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_4_0))
(check-sat)

314
test/cmdlineTests/standard_model_checker_timeout_all/output.json
View File

File diff suppressed because one or more lines are too long

598
test/cmdlineTests/standard_model_checker_timeout_bmc/output.json
View File

File diff suppressed because one or more lines are too long

1
test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol
View File

@ -10,4 +10,3 @@ contract C {
}
}
// ----
// Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

1
test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol
View File

@ -11,5 +11,4 @@ contract C {
}
}
// ----
// Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 2529: (150-157): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\nl = 0\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf(0)

3
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_3d.sol
View File

@ -26,5 +26,4 @@ contract C {
}
}
// ----
// Warning 6328: (570-625): CHC: Assertion violation might happen here.
// Warning 4661: (570-625): BMC: Assertion violation happens here.
// Warning 6328: (570-625): CHC: Assertion violation happens here.\nCounterexample:\nc = [[[2]]]\n\n\n\nTransaction trace:\nconstructor()\nState: c = []\ng()

1
test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol
View File

@ -12,4 +12,3 @@ contract C {
}
}
// ----
// Warning 4984: (174-177): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

11
test/libsolidity/smtCheckerTests/bmc_coverage/math.sol
View File

@ -1,7 +1,5 @@
pragma experimental SMTChecker;
contract C {
uint z = 1;
uint w = z - 3;
function a(uint x, uint y) public pure returns (uint) {
return x + y;
}
@ -18,8 +16,7 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 2661: (141-146): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (217-222): BMC: Underflow (resulting value less than 0) happens here.
// Warning 2661: (293-298): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 3046: (369-374): BMC: Division by zero happens here.
// Warning 4144: (68-73): BMC: Underflow (resulting value less than 0) happens here.
// Warning 2661: (111-116): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (187-192): BMC: Underflow (resulting value less than 0) happens here.
// Warning 2661: (263-268): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 3046: (339-344): BMC: Division by zero happens here.

9
test/libsolidity/smtCheckerTests/bmc_coverage/math_constructor.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
uint z = 1;
uint w = z - 3;
}
// ====
// SMTEngine: bmc
// ----
// Warning 4144: (68-73): BMC: Underflow (resulting value less than 0) happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol
View File

@ -34,4 +34,4 @@ contract C {
}
}
// ----
// Warning 6328: (528-565): CHC: Assertion violation happens here.\nCounterexample:\nowner = (- 1), y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = (- 1), y = 0, z = 0, s = 0\nf()
// Warning 6328: (528-565): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 1, y = 0, z = 0, s = 0\nf()

2
test/libsolidity/smtCheckerTests/external_calls/external_safe.sol
View File

@ -17,5 +17,3 @@ contract C {
}
}
// ----
// Warning 6328: (200-214): CHC: Assertion violation might happen here.
// Warning 4661: (200-214): BMC: Assertion violation happens here.

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

@ -21,6 +21,5 @@ contract A is B {
// ====
// SMTIgnoreCex: yes
// ----
// Warning 4984: (244-249): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (232-250): CHC: Assertion violation happens here.
// Warning 4984: (203-208): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

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

@ -18,6 +18,5 @@ contract A is B {
}
}
// ----
// Warning 4984: (230-235): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (207-212): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (198-203): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (198-203): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639934\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639934)

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

@ -28,5 +28,4 @@ contract A is B2, B1 {
// SMTIgnoreCex: yes
// ----
// Warning 4984: (200-205): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (314-319): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (302-320): CHC: Assertion violation happens here.

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

@ -28,5 +28,4 @@ contract A is B2, B1 {
// SMTIgnoreCex: yes
// ----
// Warning 4984: (200-205): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (314-319): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (302-320): CHC: Assertion violation happens here.

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

@ -13,4 +13,4 @@ contract C {
}
}
// ----
// Warning 6328: (145-159): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 9\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(9)
// Warning 6328: (145-159): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(11)

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

@ -14,5 +14,7 @@ contract C is B {
assert(y == x);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(11)
// Warning 6328: (165-179): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol
View File

@ -17,4 +17,4 @@ contract C {
}
}
// ----
// Warning 6328: (293-307): CHC: Assertion violation happens here.
// Warning 6328: (293-307): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()

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

@ -21,4 +21,3 @@ contract C {
// ----
// Warning 6328: (136-155): CHC: Assertion violation happens here.\nCounterexample:\nTON = 1000\n\n\n\nTransaction trace:\nconstructor()\nState: TON = 1000\nf1()
// Warning 4984: (229-234): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor()\nf(115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (327-332): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor()\nf(115792089237316195423570985008687907853269984665640564039457584007913129639935)

2
test/libsolidity/smtCheckerTests/imports/import_base.sol
View File

@ -19,7 +19,7 @@ contract Der is Base {
}
// ----
// Warning 4984: (der:101-109): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (der:113-126): CHC: Assertion violation happens here.\nCounterexample:\nx = 3, a = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: x = 0, a = 0\ng(0)
// Warning 6328: (der:113-126): CHC: Assertion violation happens here.\nCounterexample:\nx = 3, a = 7\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: x = 0, a = 0\ng(0)
// Warning 4984: (base:100-103): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 2661: (base:100-103): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (der:101-109): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

1
test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_3.sol
View File

@ -33,5 +33,4 @@ contract C is Z, B {
// SMTIgnoreCex: yes
// ----
// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (366-371): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (394-408): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_4.sol
View File

@ -33,5 +33,4 @@ contract C is Z, B {
// SMTIgnoreCex: yes
// ----
// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (366-371): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (394-408): CHC: Assertion violation happens here.

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

@ -24,9 +24,5 @@ contract A is B {
// SMTIgnoreCex: yes
// ----
// Warning 4984: (157-162): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (239-244): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (261-266): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (261-270): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (287-292): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (275-293): CHC: Assertion violation happens here.
// Warning 4984: (216-221): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

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

@ -24,8 +24,5 @@ contract A is B {
// SMTIgnoreCex: yes
// ----
// Warning 4984: (157-163): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (240-245): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (262-268): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (285-290): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (273-291): CHC: Assertion violation happens here.
// Warning 4984: (217-222): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

1
test/libsolidity/smtCheckerTests/invariants/loop_basic.sol
View File

@ -12,4 +12,3 @@ contract Simple {
// ====
// SMTSolvers: z3
// ----
// Warning 4984: (132-135): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

1
test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol
View File

@ -10,4 +10,3 @@ contract Simple {
// ====
// SMTSolvers: z3
// ----
// Warning 4984: (116-119): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

5
test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol
View File

@ -9,9 +9,8 @@ contract Simple {
for (x = 0; x < 10; ++x) {}
assert(x == 10);
}
assert(y == x);
// Disabled because of Spacer nondeterminism.
//assert(y == x);
}
}
// ----
// Warning 6328: (187-201): CHC: Assertion violation might happen here.
// Warning 4661: (187-201): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol
View File

@ -21,5 +21,3 @@ contract LoopFor2 {
// SMTIgnoreCex: yes
// ----
// Warning 2072: (156-171): Unused local variable.
// Warning 4984: (252-257): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (232-238): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

2
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol
View File

@ -20,5 +20,3 @@ contract LoopFor2 {
// ====
// SMTSolvers: z3
// ----
// Warning 4984: (245-250): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (225-231): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

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

@ -20,4 +20,3 @@ contract LoopFor2 {
}
}
// ----
// Warning 4984: (311-317): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

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

@ -24,5 +24,3 @@ contract LoopFor2 {
// SMTSolvers: z3
// ----
// Warning 2072: (156-171): Unused local variable.
// Warning 4984: (244-249): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (270-273): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

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

@ -25,5 +25,3 @@ contract LoopFor2 {
// ====
// SMTSolvers: z3
// ----
// Warning 4984: (237-242): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (263-266): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

2
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
View File

@ -20,7 +20,5 @@ contract LoopFor2 {
}
}
// ----
// Warning 4984: (229-234): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (255-258): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (338-357): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1)
// Warning 6328: (361-380): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1)

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

@ -13,7 +13,7 @@ contract C
function f() m public {
assert(x > 0);
x = x + 1;
unchecked { x = x + 1; }
}
function g(uint _x) public {
@ -21,5 +21,4 @@ contract C
}
}
// ----
// Warning 4984: (203-208): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ng(115792089237316195423570985008687907853269984665640564039457584007913129639935)\nState: x = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nf()
// Warning 6328: (136-149): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ng(115792089237316195423570985008687907853269984665640564039457584007913129639935)\nState: x = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nf()

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

@ -12,4 +12,4 @@ contract C
}
}
// ----
// Warning 6328: (198-218): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 0\n\n\nTransaction trace:\nconstructor()\nf(0, 0)
// Warning 6328: (198-218): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 38\n\n\nTransaction trace:\nconstructor()\nf(0, 38)

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

@ -12,4 +12,4 @@ contract C
}
}
// ----
// Warning 6328: (197-216): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 0\n\n\nTransaction trace:\nconstructor()\nf(0, 0)
// Warning 6328: (197-216): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 38\n\n\nTransaction trace:\nconstructor()\nf(0, 38)

15
test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol
View File

@ -4,12 +4,17 @@ contract C {
uint a;
bool b;
constructor(bool _b) {
b = _b;
}
function f() public returns(uint c) {
c = b ? a + 1 : a--;
assert(c > a);
c = b ? a + 10 : ++a;
assert(c >= a);
}
}
// ----
// Warning 4984: (129-134): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935, b = false\n\nc = 0\n\nTransaction trace:\nconstructor()\nState: a = 0, b = false\nf()\nState: a = 115792089237316195423570985008687907853269984665640564039457584007913129639935, b = false\nf()
// Warning 3944: (137-140): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\na = 0, b = false\n\nc = 0\n\nTransaction trace:\nconstructor()\nState: a = 0, b = false\nf()
// Warning 6328: (150-163): CHC: Assertion violation happens here.\nCounterexample:\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935, b = false\n\nc = 0\n\nTransaction trace:\nconstructor()\nState: a = 0, b = false\nf()
// Warning 4984: (167-173): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (176-179): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 2661: (167-173): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (176-179): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

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

@ -1,7 +1,7 @@
pragma experimental SMTChecker;
contract C {
function mul(uint256 a, uint256 b) internal pure returns (uint256) {
uint256 c;
function mul(uint8 a, uint8 b) internal pure returns (uint8) {
uint8 c;
if (a != 0) {
c = a * b;
require(c / a == b);
@ -10,3 +10,4 @@ contract C {
}
}
// ----
// Warning 6838: (161-171): BMC: Condition is always true.

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

@ -1,13 +1,14 @@
pragma experimental SMTChecker;
contract C {
function mul(uint256 a, uint256 b) public pure returns (uint256) {
function mul(uint8 a, uint8 b) public pure returns (uint8) {
if (a == 0) {
return 0;
}
uint256 c = a * b;
uint8 c = a * b;
require(c / a == b);
return c;
}
}
// ----
// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (152-157): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\na = 128\nb = 2\n = 0\n\nTransaction trace:\nconstructor()\nmul(128, 2)
// Warning 6838: (169-179): BMC: Condition is always true.

13
test/libsolidity/smtCheckerTests/operators/shifts/shift_cleanup.sol
View File

@ -2,10 +2,12 @@ pragma experimental SMTChecker;
contract C {
function f() public pure returns (uint16 x) {
x = 0xffff;
x += 32;
x = x << 8;
x = x >> 16;
unchecked {
x = 0xffff;
x += 32;
x = x << 8;
x = x >> 16;
}
assert(x == 0);
// Fails because x = 0.
assert(x == 10);
@ -14,5 +16,4 @@ contract C {
// ====
// SMTIgnoreCex: yes
// ----
// Warning 4984: (109-116): CHC: Overflow (resulting value larger than 65535) happens here.
// Warning 6328: (193-208): CHC: Assertion violation happens here.
// Warning 6328: (215-230): CHC: Assertion violation happens here.

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

@ -21,5 +21,6 @@ contract C {
*/
}
// ----
// Warning 4984: (87-90): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\nx = 255\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ndec_pre()\nState: x = 255\ninc_pre()
// Warning 4984: (87-90): CHC: Overflow (resulting value larger than 255) might happen here.
// Warning 3944: (127-130): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ndec_pre()
// Warning 2661: (87-90): BMC: Overflow (resulting value larger than 255) happens here.

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

@ -14,4 +14,3 @@ contract C
}
// ----
// Warning 4984: (120-125): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\nx = 100\n = 0\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 4984: (163-168): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\nx = 128\n = 0\n\nTransaction trace:\nconstructor()\nf(0)

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

@ -7,4 +7,4 @@ contract C {
}
}
// ----
// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 18, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15]\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\n\nTransaction trace:\nconstructor()\nf([15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 18, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], 23158417847463239084714197001737581570653996933128112807891516801582625927988)
// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = [13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 16, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13]\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\n\nTransaction trace:\nconstructor()\nf([13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 16, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13], 23158417847463239084714197001737581570653996933128112807891516801582625927988)

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

@ -4,7 +4,8 @@ contract C
{
function f(int8 x) public pure returns (int8) {
x = 100;
int8 y = x * 2;
int8 y;
unchecked { y = x * 2; }
assert(y == -56);
y = x * 100;
assert(y == 16);
@ -12,5 +13,4 @@ contract C
}
}
// ----
// Warning 4984: (117-122): CHC: Overflow (resulting value larger than 127) happens here.\nCounterexample:\n\nx = 100\n = 0\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 4984: (150-157): CHC: Overflow (resulting value larger than 127) happens here.\nCounterexample:\n\nx = 100\n = 0\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 4984: (169-176): CHC: Overflow (resulting value larger than 127) happens here.\nCounterexample:\n\nx = 100\n = 0\n\nTransaction trace:\nconstructor()\nf(0)

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

@ -3,10 +3,11 @@ pragma experimental SMTChecker;
contract C
{
function f(uint8 x) public pure returns (uint8) {
uint8 y = x + 255;
uint8 y;
unchecked { y = x + 255; }
require(y >= x);
x = 255;
y = x + 1;
unchecked { y = x + 1; }
assert(y == 0);
y = x + 255;
assert(y == 254);
@ -14,6 +15,4 @@ contract C
}
}
// ----
// Warning 4984: (109-116): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\nx = 1\n = 0\n\nTransaction trace:\nconstructor()\nf(1)
// Warning 4984: (154-159): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\nx = 255\n = 0\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 4984: (185-192): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\nx = 255\n = 0\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 4984: (218-225): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\nx = 255\n = 0\n\nTransaction trace:\nconstructor()\nf(0)

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

@ -2,19 +2,16 @@ pragma experimental SMTChecker;
contract C
{
function f(int8 x) public pure returns (int8) {
function f(int8 x) public pure {
x = 127;
int8 y = x + 1;
int8 y;
unchecked { y = x + 1; }
assert(y == -128);
y = x + 127;
unchecked { y = x + 127; }
assert(y == -2);
x = -127;
y = x + -127;
unchecked { y = x + -127; }
assert(y == 2);
}
}
// ----
// Warning 6321: (87-91): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
// Warning 4984: (117-122): CHC: Overflow (resulting value larger than 127) happens here.\nCounterexample:\n\nx = 127\n = 0\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 4984: (151-158): CHC: Overflow (resulting value larger than 127) happens here.\nCounterexample:\n\nx = 127\n = 0\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 3944: (197-205): CHC: Underflow (resulting value less than -128) happens here.\nCounterexample:\n\nx = (- 127)\n = 0\n\nTransaction trace:\nconstructor()\nf(0)

11
test/libsolidity/smtCheckerTests/overflow/safe_add_1.sol
View File

@ -1,11 +0,0 @@
pragma experimental SMTChecker;
contract C
{
function add(uint x, uint y) public pure returns (uint) {
require(x + y >= x);
return x + y;
}
}
// ----
// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 1\ny = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n = 0\n\nTransaction trace:\nconstructor()\nadd(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)

12
test/libsolidity/smtCheckerTests/overflow/safe_add_2.sol
View File

@ -1,12 +0,0 @@
pragma experimental SMTChecker;
contract C
{
function add(uint x, uint y) public pure returns (uint) {
uint z = x + y;
require(z >= x);
return z;
}
}
// ----
// Warning 4984: (116-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 1\ny = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n = 0\n\nTransaction trace:\nconstructor()\nadd(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)

1
test/libsolidity/smtCheckerTests/overflow/signed_guard_sum_overflow.sol
View File

@ -9,4 +9,3 @@ contract C {
// ----
// Warning 3944: (111-116): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here.\nCounterexample:\n\nx = (- 1)\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nconstructor()\nf((- 1), (- 57896044618658097711785492504343953926634992332820282019728792003956564819968))
// Warning 4984: (111-116): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 1\ny = 57896044618658097711785492504343953926634992332820282019728792003956564819967\n = 0\n\nTransaction trace:\nconstructor()\nf(1, 57896044618658097711785492504343953926634992332820282019728792003956564819967)
// Warning 3944: (133-138): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here.\nCounterexample:\n\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\ny = (- 1)\n = 0\n\nTransaction trace:\nconstructor()\nf((- 57896044618658097711785492504343953926634992332820282019728792003956564819968), (- 1))

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

@ -4,13 +4,12 @@ contract C
{
function f(uint8 x) public pure returns (uint) {
x = 0;
uint8 y = x - 1;
uint8 y;
unchecked { y = x - 1; }
assert(y == 255);
y = x - 255;
unchecked { y = x - 255; }
assert(y == 1);
return y;
}
}
// ----
// Warning 3944: (117-122): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\nx = 0\n = 0\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 3944: (150-157): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\nx = 0\n = 0\n\nTransaction trace:\nconstructor()\nf(0)

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

@ -4,18 +4,16 @@ contract C
{
function f(int8 x) public pure returns (int8) {
x = -2;
int8 y = x - 127;
int8 y;
unchecked { y = x - 127; }
assert(y == 127);
x = -128;
y = x - 127;
unchecked { y = x - 127; }
assert(y == 1);
x = 127;
y = x - (-127);
unchecked { y = x - (-127); }
assert(y == -2);
return y;
}
}
// ----
// Warning 3944: (116-123): CHC: Underflow (resulting value less than -128) happens here.\nCounterexample:\n\nx = (- 2)\n = 0\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 3944: (163-170): CHC: Underflow (resulting value less than -128) happens here.\nCounterexample:\n\nx = (- 128)\n = 0\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 4984: (207-217): CHC: Overflow (resulting value larger than 127) happens here.\nCounterexample:\n\nx = 127\n = 0\n\nTransaction trace:\nconstructor()\nf(0)

3
test/libsolidity/smtCheckerTests/overflow/unsigned_guard_sum_overflow.sol
View File

@ -2,9 +2,8 @@ pragma experimental SMTChecker;
contract C {
function f(uint x, uint y) public pure returns (uint) {
require(x + y >= x);
return x + y;
}
}
// ----
// Warning 4984: (114-119): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 1\ny = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n = 0\n\nTransaction trace:\nconstructor()\nf(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (113-118): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 1\ny = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n = 0\n\nTransaction trace:\nconstructor()\nf(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)

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

@ -14,6 +14,6 @@ contract C {
// Warning 2072: (184-188): Unused local variable.
// Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)
// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 16, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13]\n\n\nTransaction trace:\nconstructor()\nf([13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 16, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 18, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15]\n\n\nTransaction trace:\nconstructor()\nf([15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 18, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15])
// Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)

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

@ -9,7 +9,8 @@ contract C
assert(tx.gasprice == msg.value);
assert(tx.origin == msg.sender);
uint x = block.number;
assert(x + 2 > block.number);
unchecked { x += 2; }
assert(x > block.number);
assert(block.timestamp > 10);
assert(gasleft() > 100);
}
@ -20,7 +21,6 @@ contract C
// Warning 6328: (165-204): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (208-240): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (244-275): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 4984: (311-316): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (304-332): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (336-364): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (368-391): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (328-352): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (356-384): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (388-411): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()

4
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): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 0\nb = 0\n\n\nTransaction trace:\nconstructor()\nf(0, 0)
// Warning 6328: (131-160): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 0\n\n\nTransaction trace:\nconstructor()\nf(0, 0)
// Warning 4984: (105-127): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 0\nb = 38\n\n\nTransaction trace:\nconstructor()\nf(0, 38)
// Warning 6328: (131-160): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7719\nb = 38\n\n\nTransaction trace:\nconstructor()\nf(7719, 38)

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

@ -19,4 +19,4 @@ contract C
// EVMVersion: >spuriousDragon
// ----
// Warning 2072: (224-240): Unused local variable.
// Warning 6328: (266-281): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = [5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 14, 5, 17, 5, 5, 5, 5, 5, 5, 5, 5, 5, 27, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 14, 5, 17, 5, 5, 5, 5, 5, 5, 5, 5, 5, 27, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])
// Warning 6328: (266-281): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = [7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 14, 7, 7, 7, 19, 7, 7, 7, 7, 7, 7, 7, 27, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7]\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 14, 7, 7, 7, 19, 7, 7, 7, 7, 7, 7, 7, 27, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7])

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

@ -16,4 +16,4 @@ contract C
}
}
// ----
// Warning 6328: (266-286): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\n\n\nTransaction trace:\nconstructor()\nf(3)
// Warning 6328: (266-286): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\n\nTransaction trace:\nconstructor()\nf(0)

2
test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol
View File

@ -15,4 +15,4 @@ contract C {
}
}
// ----
// Warning 6328: (225-245): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 2, a: []}\ns2 = {x: 3, a: [6, 6, 6, 6, 6, 6, 6]}\n\n\nTransaction trace:\nconstructor()\nf({x: 0, a: []}, {x: 3, a: [6, 6, 6, 6, 6, 6, 6]})
// Warning 6328: (225-245): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 2, a: []}\ns2 = {x: 3, a: [5, 5, 5, 5, 5, 5]}\n\n\nTransaction trace:\nconstructor()\nf({x: 0, a: []}, {x: 3, a: [5, 5, 5, 5, 5, 5]})

4
test/libsolidity/smtCheckerTests/types/struct/struct_unary_sub.sol
View File

@ -15,5 +15,7 @@ contract C {
assert(s1.x == s2.x);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (240-260): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 98, a: []}\ns2 = {x: (- 38), a: [6, 6, 6, 6, 6, 6, 6]}\n\n\nTransaction trace:\nconstructor()\nf({x: 0, a: []}, {x: (- 38), a: [6, 6, 6, 6, 6, 6, 6]})
// Warning 6328: (240-260): CHC: Assertion violation happens here.

12
test/libsolidity/smtCheckerTests/unchecked/block_inside_unchecked.sol Normal file
View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C {
function f() public pure returns (uint y) {
unchecked{{
uint max = type(uint).max;
uint x = max + 1; // overflow not reported
y = x;
}}
assert(y == 0);
}
}

20
test/libsolidity/smtCheckerTests/unchecked/check_var_init.sol Normal file
View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
contract C {
uint public x = msg.value - 10; // can underflow
constructor() payable {}
}
contract D {
function h() internal returns (uint) {
return msg.value - 10; // can underflow
}
function f() public {
unchecked {
h(); // unchecked here does not mean h does not underflow
}
}
}
// ----
// Warning 3944: (66-80): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()
// Warning 3944: (193-207): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()

13
test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C {
function add(uint16 a, uint16 b) public pure returns (uint16) {
return a + b; // can overflow
}
function f(uint16 a, uint16 b, uint16 c) public pure returns (uint16) {
unchecked { return add(a, b) + c; } // add can still overflow, `+ c` can't
}
}
// ----
// Warning 4984: (129-134): CHC: Overflow (resulting value larger than 65535) happens here.\nCounterexample:\n\na = 1\nb = 65535\n = 0\n\nTransaction trace:\nconstructor()\nadd(1, 65535)

14
test/libsolidity/smtCheckerTests/unchecked/checked_modifier_called_by_unchecked.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
modifier add(uint16 a, uint16 b) {
unchecked { a + b; } // overflow not reported
_;
}
function f(uint16 a, uint16 b, uint16 c) public pure add(a, b) returns (uint16) {
return b + c; // can overflow
}
}
// ----
// Warning 4984: (258-263): CHC: Overflow (resulting value larger than 65535) happens here.\nCounterexample:\n\na = 65535\nb = 1\nc = 65535\n = 0\n\nTransaction trace:\nconstructor()\nf(65535, 1, 65535)

13
test/libsolidity/smtCheckerTests/unchecked/flipping_sign_tests.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract test {
function f() public pure returns (bool) {
int256 x = -2**255;
unchecked { assert(-x == x); }
assert(-x == x); // CHC apparently does not create an underflow target for unary minus
return true;
}
}
// ----
// Warning 6328: (143-158): CHC: Assertion violation happens here.\nCounterexample:\n\n\n = false\n\nTransaction trace:\nconstructor()\nf()
// Warning 2661: (150-152): BMC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.

27
test/libsolidity/smtCheckerTests/unchecked/inc_dec.sol Normal file
View File

@ -0,0 +1,27 @@
pragma experimental SMTChecker;
contract C {
function o() public pure {
uint x = type(uint).max;
unchecked { ++x; }
assert(x == type(uint).min);
}
function u() public pure {
uint x = type(uint).min;
unchecked { --x; }
assert(x == type(uint).max);
}
function o_int() public pure {
int x = type(int).max;
unchecked { ++x; }
assert(x == type(int).min);
}
function u_int() public pure {
int x = type(int).min;
unchecked { --x; }
assert(x == type(int).max);
}
}

18
test/libsolidity/smtCheckerTests/unchecked/signed_mod.sol Normal file
View File

@ -0,0 +1,18 @@
pragma experimental SMTChecker;
contract C {
function f(int a, int b) public pure returns (int) {
return a % b; // can div by 0
}
function g(bool _check) public pure returns (int) {
int x = type(int).min;
if (_check) {
return x / -1; // can overflow
} else {
unchecked { return x / -1; } // overflow not reported
}
}
}
// ----
// Warning 4281: (118-123): CHC: Division by zero happens here.\nCounterexample:\n\na = 0\nb = 0\n = 0\n\nTransaction trace:\nconstructor()\nf(0, 0)
// Warning 4984: (275-281): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\n_check = true\n = 0\n\nTransaction trace:\nconstructor()\ng(true)

15
test/libsolidity/smtCheckerTests/unchecked/unchecked_called_by_checked.sol Normal file
View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C {
function add(uint16 a, uint16 b) public pure returns (uint16) {
unchecked {
return a + b; // overflow not reported
}
}
function f(uint16 a) public pure returns (uint16) {
return add(a, 0x100) + 0x100; // should overflow on `+ 0x100`
}
}
// ----
// Warning 4984: (273-294): CHC: Overflow (resulting value larger than 65535) happens here.\nCounterexample:\n\na = 65024\n = 0\n\nTransaction trace:\nconstructor()\nf(65024)

20
test/libsolidity/smtCheckerTests/unchecked/unchecked_div_by_zero.sol Normal file
View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
contract C {
function div(uint256 a, uint256 b) public pure returns (uint256) {
// Does not disable div by zero check
unchecked {
return a / b;
}
}
function mod(uint256 a, uint256 b) public pure returns (uint256) {
// Does not disable div by zero check
unchecked {
return a % b;
}
}
}
// ----
// Warning 4281: (202-207): CHC: Division by zero happens here.\nCounterexample:\n\na = 0\nb = 0\n = 0\n\nTransaction trace:\nconstructor()\ndiv(0, 0)
// Warning 4281: (382-387): CHC: Division by zero happens here.\nCounterexample:\n\na = 0\nb = 0\n = 0\n\nTransaction trace:\nconstructor()\nmod(0, 0)