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 #11145 from ethereum/smt_out_of_bounds

Browse Source 
[SMTChecker] Add `out of bounds` verification target
This commit is contained in:
Leonardo 2021-03-30 14:24:50 +02:00 committed by GitHub
commit a7e2a8acb2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
208 changed files with 1619 additions and 608 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Changelog.md
View File

@ -4,7 +4,10 @@ Language Features:
* Possibility to use ``bytes.concat`` with variable number of ``bytes`` and ``bytesNN`` arguments which behaves as a restricted version of `abi.encodePacked` with a more descriptive name.
Compiler Features:
* Commandline Interface: Model checker option ``--model-checker-targets`` also accepts ``outOfBounds``.
* Low-Level Inliner: Inline ordinary jumps to small blocks and jumps to small blocks that terminate.
* SMTChecker: Report out of bounds index access for arrays and fixed bytes.
* Standard JSON: Model checker option ``settings.modelChecker.targets`` also accepts ``outOfBounds``.
* Yul Optimizer: Added a new step FunctionSpecializer, that specializes a function with its literal arguments.

2
docs/smtchecker.rst
View File

@ -31,6 +31,7 @@ The other verification targets that the SMTChecker checks at compile time are:
- Division by zero.
- Trivial conditions and unreachable code.
- Popping an empty array.
- Out of bounds index access.
- Insufficient funds for a transfer.
The potential warnings that the SMTChecker reports are:
@ -457,6 +458,7 @@ list of one or more verification targets. The keywords that represent the target
- Division by zero: ``divByZero``.
- Trivial conditions and unreachable code: ``constantCondition``.
- Popping an empty array: ``popEmptyArray``.
- Out of bounds array/fixed bytes index access: ``outOfBounds``.
- Insufficient funds for a transfer: ``balance``.
- All of the above: ``all``.
- None of the above: ``none``.

2
docs/using-the-compiler.rst
View File

@ -379,7 +379,7 @@ Input Description
// Choose which model checker engine to use: all (default), bmc, chc, none.
"engine": "chc",
// Choose which targets should be checked: all (default), constantCondition,
// underflow, overflow, divByZero, balance, assert, popEmptyArray.
// underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds.
// See the Formal Verification section for the targets description.
// Multiple targets can be selected at the same time, separated by a comma
// without spaces:

32
libsolidity/formal/CHC.cpp
View File

@ -788,6 +788,32 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
verificationTargetEncountered(&_arrayPop, VerificationTargetType::PopEmptyArray, symbArray->length() <= 0);
}
void CHC::makeOutOfBoundsVerificationTarget(IndexAccess const& _indexAccess)
{
if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
return;
auto baseType = _indexAccess.baseExpression().annotation().type;
optional<smtutil::Expression> length;
if (smt::isArray(*baseType))
length = dynamic_cast<smt::SymbolicArrayVariable const&>(
*m_context.expression(_indexAccess.baseExpression())
).length();
else if (auto const* type = dynamic_cast<FixedBytesType const*>(baseType))
length = smtutil::Expression(static_cast<size_t>(type->numBytes()));
optional<smtutil::Expression> target;
if (
auto index = _indexAccess.indexExpression();
index && length
)
target = expr(*index) < 0 || expr(*index) >= *length;
if (target)
verificationTargetEncountered(&_indexAccess, VerificationTargetType::OutOfBounds, *target);
}
pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
Token _op,
smtutil::Expression const& _left,
@ -1415,6 +1441,12 @@ void CHC::checkVerificationTargets()
errorType = "Empty array \"pop\"";
errorReporterId = 2529_error;
}
else if (target.type == VerificationTargetType::OutOfBounds)
{
solAssert(dynamic_cast<IndexAccess const*>(target.errorNode), "");
errorType = "Out of bounds access";
errorReporterId = 6368_error;
}
else if (
target.type == VerificationTargetType::Underflow ||
target.type == VerificationTargetType::Overflow

1
libsolidity/formal/CHC.h
View File

@ -97,6 +97,7 @@ private:
void externalFunctionCallToTrustedCode(FunctionCall const& _funCall);
void unknownFunctionCall(FunctionCall const& _funCall);
void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override;
void makeOutOfBoundsVerificationTarget(IndexAccess const& _access) override;
/// Creates underflow/overflow verification targets.
std::pair<smtutil::Expression, smtutil::Expression> arithmeticOperation(
Token _op,

3
libsolidity/formal/ModelCheckerSettings.cpp
View File

@ -36,7 +36,8 @@ std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const&
{"divByZero", TargetType::DivByZero},
{"balance", TargetType::Balance},
{"assert", TargetType::Assert},
{"popEmptyArray", TargetType::PopEmptyArray}
{"popEmptyArray", TargetType::PopEmptyArray},
{"outOfBounds", TargetType::OutOfBounds}
};
set<TargetType> chosenTargets;

2
libsolidity/formal/ModelCheckerSettings.h
View File

@ -54,7 +54,7 @@ struct ModelCheckerEngine
}
};
enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray };
enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray, OutOfBounds };
struct ModelCheckerTargets
{

4
libsolidity/formal/SMTEncoder.cpp
View File

@ -1382,6 +1382,9 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
return;
makeOutOfBoundsVerificationTarget(_indexAccess);
if (auto const* type = dynamic_cast<FixedBytesType const*>(_indexAccess.baseExpression().annotation().type))
{
smtutil::Expression base = expr(_indexAccess.baseExpression());
@ -1430,6 +1433,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
solAssert(arrayVar, "");
Type const* baseType = _indexAccess.baseExpression().annotation().type;
defineExpr(_indexAccess, smtutil::Expression::select(
arrayVar->elements(),

2
libsolidity/formal/SMTEncoder.h
View File

@ -224,6 +224,8 @@ protected:
/// Allows BMC and CHC to create verification targets for popping
/// an empty array.
virtual void makeArrayPopVerificationTarget(FunctionCall const&) {}
/// Allows BMC and CHC to create verification targets for out of bounds access.
virtual void makeOutOfBoundsVerificationTarget(IndexAccess const&) {}
void addArrayLiteralAssertions(
smt::SymbolicArrayVariable& _symArray,

2
solc/CommandLineInterface.cpp
View File

@ -1052,7 +1052,7 @@ General Information)").c_str(),
)
(
g_strModelCheckerTargets.c_str(),
po::value<string>()->value_name("all,constantCondition,underflow,overflow,divByZero,balance,assert,popEmptyArray")->default_value("all"),
po::value<string>()->value_name("all,constantCondition,underflow,overflow,divByZero,balance,assert,popEmptyArray,outOfBounds")->default_value("all"),
"Select model checker verification targets. "
"Multiple targets can be selected at the same time, separated by a comma "
"and no spaces."

15
test/cmdlineTests/model_checker_targets_all/err
View File

@ -73,6 +73,21 @@ test.f(0, 1)
13 | arr.pop();
| ^^^^^^^^^
Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:14:3:
|
14 | arr[x];
| ^^^^^^
Warning: BMC: Condition is always true.
--> model_checker_targets_all/input.sol:7:11:
|

1
test/cmdlineTests/model_checker_targets_all/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_all_bmc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

15
test/cmdlineTests/model_checker_targets_all_chc/err
View File

@ -72,3 +72,18 @@ test.f(0, 1)
|
13 | arr.pop();
| ^^^^^^^^^
Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all_chc/input.sol:14:3:
|
14 | arr[x];
| ^^^^^^

1
test/cmdlineTests/model_checker_targets_all_chc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_assert_bmc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_assert_chc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_balance_bmc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_balance_chc/input.sol
View File

@ -10,5 +10,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_constant_condition_bmc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol
View File

@ -10,5 +10,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_div_by_zero_bmc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_div_by_zero_chc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_error/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine bmc --model-checker-targets outOfBounds

2
test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/err Normal file
View File

@ -0,0 +1,2 @@
Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
--> model_checker_targets_out_of_bounds_bmc/input.sol

15
test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/input.sol Normal file
View File

@ -0,0 +1,15 @@
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);
--x;
x + type(uint).max;
2 / x;
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_out_of_bounds_chc/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine chc --model-checker-targets outOfBounds

14
test/cmdlineTests/model_checker_targets_out_of_bounds_chc/err Normal file
View File

@ -0,0 +1,14 @@
Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_out_of_bounds_chc/input.sol:14:3:
|
14 | arr[x];
| ^^^^^^

16
test/cmdlineTests/model_checker_targets_out_of_bounds_chc/input.sol Normal file
View File

@ -0,0 +1,16 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);
--x;
x + type(uint).max;
2 / x;
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_overflow_bmc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_overflow_chc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_pop_empty_bmc/input.sol
View File

@ -10,5 +10,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_pop_empty_chc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_underflow_bmc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_underflow_chc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_underflow_overflow_assert_bmc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_underflow_overflow_bmc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/model_checker_targets_underflow_overflow_chc/input.sol
View File

@ -11,5 +11,6 @@ contract test {
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}

1
test/cmdlineTests/standard_model_checker_targets_all/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

37
test/cmdlineTests/standard_model_checker_targets_all/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x46492b9840256a3adc6e233de45185cf257b5247111456ce53d32381cb716096":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x0ae37e2188bca4f05e5d380a139f98fa51f42155b282121332698f6b8e8a822a":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -28,8 +28,8 @@
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_12_0| () Int)
(declare-fun |r_div_mod_12_0| () Int)
(declare-fun |d_div_mod_14_0| () Int)
(declare-fun |r_div_mod_14_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
@ -44,8 +44,11 @@
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) (and (>= expr_33_0 0) (<= expr_33_0 1461501637330902918203684832716283019655932542975))) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_12_0)) (and (and (<= 0 r_div_mod_12_0) (or (= expr_30_0 0) (< r_div_mod_12_0 expr_30_0))) (and (= (+ (* d_div_mod_12_0 expr_30_0) r_div_mod_12_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (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 (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) (and (>= expr_33_0 0) (<= expr_33_0 1461501637330902918203684832716283019655932542975))) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_14_0)) (and (and (<= 0 r_div_mod_14_0) (or (= expr_30_0 0) (< r_div_mod_14_0 expr_30_0))) (and (= (+ (* d_div_mod_14_0 expr_30_0) r_div_mod_14_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (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 (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(declare-const |EVALEXPR_1| Int)
@ -222,7 +225,31 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":306,"file":"A","start":297},"type":"Warning"},{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":306,"file":"A","start":297},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> A:14:7:
|
14 | \t\t\t\t\t\tarr[x];
| \t\t\t\t\t\t^^^^^^
","message":"CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":320,"file":"A","start":314},"type":"Warning"},{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
--> A:7:15:
|
7 | \t\t\t\t\t\trequire(x >= 0);

1
test/cmdlineTests/standard_model_checker_targets_all_bmc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

131
test/cmdlineTests/standard_model_checker_targets_all_bmc/output.json
View File

File diff suppressed because one or more lines are too long

1
test/cmdlineTests/standard_model_checker_targets_all_chc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

26
test/cmdlineTests/standard_model_checker_targets_all_chc/output.json
View File

@ -118,4 +118,28 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":306,"file":"A","start":297},"type":"Warning"}],"sources":{"A":{"id":0}}}
test.f(0, 1)","severity":"warning","sourceLocation":{"end":306,"file":"A","start":297},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> A:14:7:
|
14 | \t\t\t\t\t\tarr[x];
| \t\t\t\t\t\t^^^^^^
","message":"CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":320,"file":"A","start":314},"type":"Warning"}],"sources":{"A":{"id":0}}}

1
test/cmdlineTests/standard_model_checker_targets_assert_bmc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

5
test/cmdlineTests/standard_model_checker_targets_assert_bmc/output.json
View File

File diff suppressed because one or more lines are too long

1
test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

1
test/cmdlineTests/standard_model_checker_targets_balance_bmc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

5
test/cmdlineTests/standard_model_checker_targets_balance_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x2471cb3319011ef1b50871792b380ba51753bfb7a34c5e3124effc051c2040b0":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x0b0abe50a463d83cc965e76d4d1972e45281d54eb73ae5aa8fc775e90abbf71c":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -44,6 +44,9 @@
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) (and (>= expr_33_0 0) (<= expr_33_0 1461501637330902918203684832716283019655932542975))) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_30_0 0) (< r_div_mod_0_0 expr_30_0))) (and (= (+ (* d_div_mod_0_0 expr_30_0) r_div_mod_0_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (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 (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
(declare-const |EVALEXPR_0| Int)

1
test/cmdlineTests/standard_model_checker_targets_balance_chc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

1
test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

1
test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

1
test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

5
test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0xa1088f3811326a268c2e66329bd025ca3b9a1efc2e88735a71e0d32f516e7aab":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0xb8b792833b9e11c3c041b12b2497f440f94a3d5ba4b1e5fea5c8951df8e8ae50":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -44,6 +44,9 @@
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (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 (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))) (= expr_30_0 0)))
(declare-const |EVALEXPR_0| Int)

1
test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

3
test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/standard_model_checker_targets_underflow_overflow_bmc/input.json → test/cmdlineTests/standard_model_checker_targets_out_of_bounds_bmc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}
@ -23,7 +24,7 @@
"modelChecker":
{
"engine": "bmc",
"targets": "underflow,overflow"
"targets": "outOfBounds"
}
}
}

1
test/cmdlineTests/standard_model_checker_targets_out_of_bounds_bmc/output.json Normal file
View File

@ -0,0 +1 @@
{"sources":{"A":{"id":0}}}

30
test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/input.json Normal file
View File

@ -0,0 +1,30 @@
{
"language": "Solidity",
"sources":
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);
--x;
x + type(uint).max;
2 / x;
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}
},
"settings":
{
"modelChecker":
{
"engine": "chc",
"targets": "outOfBounds"
}
}
}

25
test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/output.json Normal file
View File

@ -0,0 +1,25 @@
{"errors":[{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> A:14:7:
|
14 | \t\t\t\t\t\tarr[x];
| \t\t\t\t\t\t^^^^^^
","message":"CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":320,"file":"A","start":314},"type":"Warning"}],"sources":{"A":{"id":0}}}

1
test/cmdlineTests/standard_model_checker_targets_overflow_bmc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

5
test/cmdlineTests/standard_model_checker_targets_overflow_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x875aa24f3cbb5eccbb17860716fb684063051450f8e1c8e4291787d707c0d4f7":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0xa3996a5d47bc44faaf73323541afb4be072ec0895e8308f2f86b201ef24f1260":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -44,6 +44,9 @@
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (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 (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))) (> (+ expr_21_0 expr_26_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(declare-const |EVALEXPR_0| Int)

1
test/cmdlineTests/standard_model_checker_targets_overflow_chc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

1
test/cmdlineTests/standard_model_checker_targets_pop_empty_bmc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

1
test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

1
test/cmdlineTests/standard_model_checker_targets_underflow_bmc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

5
test/cmdlineTests/standard_model_checker_targets_underflow_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x7e28accf1c311d29f1ccd5181e3288c6797c18e950e88fc23336089c8ce8dc31":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x7361a6612f525ea38847be6633b65ad5aa7c9a136c3756ccd0f1922e5a68f7ef":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -44,6 +44,9 @@
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (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 (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))))) (< (- x_9_0 1) 0)))
(declare-const |EVALEXPR_0| Int)

1
test/cmdlineTests/standard_model_checker_targets_underflow_chc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

1
test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_bmc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

121
test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_bmc/output.json
View File

File diff suppressed because one or more lines are too long

1
test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

1
test/cmdlineTests/standard_model_checker_targets_underflow_overflow_bmc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

10
test/cmdlineTests/standard_model_checker_targets_underflow_overflow_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x7e28accf1c311d29f1ccd5181e3288c6797c18e950e88fc23336089c8ce8dc31":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x7361a6612f525ea38847be6633b65ad5aa7c9a136c3756ccd0f1922e5a68f7ef":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -44,6 +44,9 @@
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (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 (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))))) (< (- x_9_0 1) 0)))
(declare-const |EVALEXPR_0| Int)
@ -54,7 +57,7 @@
(assert (= |EVALEXPR_2| (- x_9_0 1)))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
","0x875aa24f3cbb5eccbb17860716fb684063051450f8e1c8e4291787d707c0d4f7":"(set-option :produce-models true)
","0xa3996a5d47bc44faaf73323541afb4be072ec0895e8308f2f86b201ef24f1260":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -100,6 +103,9 @@
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (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 (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))) (> (+ expr_21_0 expr_26_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(declare-const |EVALEXPR_0| Int)

1
test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

147
test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/standard_model_checker_targets_underflow_overflow_bmc/output.json
View File

@ -1,147 +0,0 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0xbff03f53a7de50d2b79369639ee478ab1b8df545104dc83d93aafae02dde855a":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(declare-fun |state_0| () |state_type|)
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
(declare-fun |tx_0| () |tx_type|)
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
(declare-fun |crypto_0| () |crypto_type|)
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true))))))))))))) (< (- x_9_0 1) 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| (- x_9_0 1)))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
","0xc23473f0d9042c91db2816923860cf271ed38d055bf0c0a61ef777a2d890a4a3":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(declare-fun |state_0| () |state_type|)
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
(declare-fun |tx_0| () |tx_type|)
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
(declare-fun |crypto_0| () |crypto_type|)
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))) (> (+ expr_21_0 expr_26_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_1))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| (+ expr_21_0 expr_26_1)))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
"}},"errors":[{"component":"general","errorCode":"4144","formattedMessage":"Warning: BMC: Underflow (resulting value less than 0) happens here.
--> A:8:7:
|
8 | \t\t\t\t\t\t--x;
| \t\t\t\t\t\t^^^
Note: Counterexample:
<result> = (- 1)
a = 0
x = 0
Note: Callstack:
Note:
","message":"BMC: Underflow (resulting value less than 0) happens here.","secondarySourceLocations":[{"message":"Counterexample:
<result> = (- 1)
a = 0
x = 0
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":208,"file":"A","start":205},"type":"Warning"},{"component":"general","errorCode":"2661","formattedMessage":"Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
--> A:9:7:
|
9 | \t\t\t\t\t\tx + type(uint).max;
| \t\t\t\t\t\t^^^^^^^^^^^^^^^^^^
Note: Counterexample:
<result> = 2**256
a = 0
x = 1
Note: Callstack:
Note:
","message":"BMC: Overflow (resulting value larger than 2**256 - 1) happens here.","secondarySourceLocations":[{"message":"Counterexample:
<result> = 2**256
a = 0
x = 1
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":234,"file":"A","start":216},"type":"Warning"}],"sources":{"A":{"id":0}}}

1
test/cmdlineTests/standard_model_checker_targets_wrong/input.json
View File

@ -14,6 +14,7 @@
a.transfer(x);
assert(x > 0);
arr.pop();
arr[x];
}
}"
}

19
test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol
View File

@ -18,6 +18,9 @@ contract C {
assert(e.length == g.length); // should fail
(uint[][] memory h, uint[][][] memory i, uint j) = abi.decode(b1, (uint[][], uint[][][], uint));
require(j < h.length);
require(j < i.length);
require(j < i[j].length);
assert(h[j].length == i[j][j].length); // should fail
(uint[] memory k, uint[] memory l) = abi.decode(b2, (uint[], uint[]));
@ -39,18 +42,18 @@ contract C {
// Warning 8364: (811-817): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (811-819): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (811-821): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (943-949): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (951-957): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (1021-1027): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (1029-1035): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 6328: (214-242): CHC: Assertion violation happens here.
// Warning 6328: (367-395): CHC: Assertion violation happens here.
// Warning 6328: (446-474): CHC: Assertion violation happens here.
// Warning 6328: (592-620): CHC: Assertion violation happens here.
// Warning 6328: (639-667): CHC: Assertion violation happens here.
// Warning 6328: (686-714): CHC: Assertion violation happens here.
// Warning 6328: (833-870): CHC: Assertion violation happens here.
// Warning 6328: (963-991): CHC: Assertion violation happens here.
// Warning 6328: (1010-1038): CHC: Assertion violation happens here.
// Warning 6328: (1057-1085): CHC: Assertion violation happens here.
// Warning 6328: (911-948): CHC: Assertion violation happens here.
// Warning 6328: (1041-1069): CHC: Assertion violation happens here.
// Warning 6328: (1088-1116): CHC: Assertion violation happens here.
// Warning 6328: (1135-1163): CHC: Assertion violation happens here.
// Warning 8364: (194-200): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (202-208): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (315-321): Assertion checker does not yet implement type type(uint256[] memory)
@ -63,5 +66,5 @@ contract C {
// Warning 8364: (811-817): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (811-819): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (811-821): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (943-949): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (951-957): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (1021-1027): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (1029-1035): Assertion checker does not yet implement type type(uint256[] memory)

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

@ -3,6 +3,7 @@ pragma abicoder v2;
contract C {
function f(uint[][] memory arr) public pure {
require(arr.length > 0);
uint[][] memory arr2 = arr;
assert(arr2[0].length == arr[0].length);
assert(arr.length == arr2.length);

6
test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol
View File

@ -4,6 +4,12 @@ pragma abicoder v2;
contract C {
uint[][] arr;
uint[][] arr2;
constructor() {
arr.push();
arr.push();
arr2.push();
arr2.push();
}
function f() public view {
assert(arr2[0].length == arr[0].length);
assert(arr2.length == arr.length);

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

@ -4,6 +4,7 @@ pragma abicoder v2;
contract C {
uint[][] arr;
function f(uint[][] memory arr2) public {
require(arr2.length > 0);
arr = arr2;
assert(arr2[0].length == arr[0].length);
assert(arr2.length == arr.length);

6
test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol
View File

@ -3,6 +3,12 @@ pragma abicoder v2;
contract C {
uint[][] arr;
constructor() {
arr.push();
arr.push();
arr.push();
arr.push();
}
function f() public view {
uint[][] memory arr2 = arr;
assert(arr2[0].length == arr[0].length);

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

@ -2,8 +2,9 @@ pragma experimental SMTChecker;
contract C {
mapping (uint => uint[][]) map;
function f(uint x, uint y) public view {
function f(uint x, uint y) public {
require(x == y);
map[x].push();
assert(map[x][0].length == map[y][0].length);
}
}

11
test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol
View File

@ -6,8 +6,17 @@ contract C {
}
S s1;
S s2;
constructor() {
s1.arr.push();
s2.arr.push();
s1.arr[0].push();
s1.arr[0].push();
s1.arr[0].push();
s2.arr[0].push();
s2.arr[0].push();
s2.arr[0].push();
}
function f() public view {
assert(s1.arr[0].length == s2.arr[0].length);
}
}
// ----

6
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol
View File

@ -2,6 +2,12 @@ pragma experimental SMTChecker;
contract C {
uint[] arr;
constructor() {
arr.push();
arr.push();
arr.push();
arr.push();
}
function f() public view {
uint[] memory arr2 = arr;
arr2[2] = 3;

13
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol
View File

@ -2,12 +2,21 @@ pragma experimental SMTChecker;
contract C {
uint[][] arr;
uint[][] arr2;
constructor() {
arr.push();
arr.push();
arr.push();
arr.push();
arr[2].push();
arr[2].push();
arr[2].push();
arr[2].push();
}
function f() public {
uint x = arr[2].length;
uint y = arr[3].length;
uint z = arr.length;
arr[2][333] = 444;
arr[2][3] = 444;
assert(arr[2].length == x);
assert(arr[3].length == y);
assert(arr.length == z);

21
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol
View File

@ -2,18 +2,29 @@ pragma experimental SMTChecker;
contract C {
uint[][] arr;
uint[][] arr2;
constructor() {
arr.push();
arr.push();
arr.push();
arr.push();
arr[2].push();
arr[2].push();
arr[2].push();
arr[2].push();
}
function f() public {
uint x = arr[2].length;
uint y = arr[3].length;
uint z = arr.length;
arr[2][333] = 444;
arr[2][3] = 444;
assert(arr[2].length != x);
assert(arr[3].length != y);
assert(arr.length != z);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (198-224): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\nTransaction trace:\nC.constructor()\nState: arr = [], arr2 = []\nC.f()
// Warning 6328: (228-254): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\nTransaction trace:\nC.constructor()\nState: arr = [], arr2 = []\nC.f()
// Warning 6328: (258-281): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\nTransaction trace:\nC.constructor()\nState: arr = [], arr2 = []\nC.f()
// Warning 6328: (324-350): CHC: Assertion violation happens here.
// Warning 6328: (354-380): CHC: Assertion violation happens here.
// Warning 6328: (384-407): CHC: Assertion violation happens here.

14
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol
View File

@ -2,7 +2,19 @@ pragma experimental SMTChecker;
contract C {
uint[][] arr;
uint[][] arr2;
constructor() {
arr.push();
arr.push();
arr.push();
arr.push();
arr.push();
arr.push();
arr.push();
arr.push();
arr.push();
}
function f() public {
uint x = arr[2].length;
uint y = arr[3].length;

20
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol
View File

@ -2,7 +2,17 @@ pragma experimental SMTChecker;
contract C {
uint[][] arr;
uint[][] arr2;
constructor() {
arr.push();
arr.push();
arr.push();
arr.push();
arr.push();
arr.push();
arr.push();
arr.push();
arr.push();
}
function f() public {
uint x = arr[2].length;
uint y = arr[3].length;
@ -16,7 +26,7 @@ contract C {
}
}
// ----
// Warning 6328: (222-248): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\nTransaction trace:\nC.constructor()\nState: arr = [], arr2 = []\nC.f()
// Warning 6328: (252-278): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\nTransaction trace:\nC.constructor()\nState: arr = [], arr2 = []\nC.f()
// Warning 6328: (282-305): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\nTransaction trace:\nC.constructor()\nState: arr = [], arr2 = []\nC.f()
// Warning 6328: (309-335): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\nTransaction trace:\nC.constructor()\nState: arr = [], arr2 = []\nC.f()
// Warning 6328: (352-378): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (382-408): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (412-435): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (439-465): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()

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

@ -3,10 +3,11 @@ pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
a.push();
a.push();
a[0].push();
a[1].pop();
}
}
// ----
// Warning 2529: (111-121): CHC: Empty array "pop" happens here.\nCounterexample:\na = [[0]]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (123-133): CHC: Empty array "pop" happens here.\nCounterexample:\na = [[0], []]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

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

@ -4,6 +4,6 @@ contract C {
function s() public returns (int[] memory) {
array2d.push() = array2d.push();
assert(array2d[array2d.length - 1].length == array2d[array2d.length - 2].length);
return array2d[2];
return array2d[1];
}
}

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

@ -16,4 +16,4 @@ contract C {
}
}
// ----
// Warning 6328: (317-343): CHC: Assertion violation happens here.\nCounterexample:\nb = [[0], [0]]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
// Warning 6328: (317-343): CHC: Assertion violation happens here.

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

@ -14,5 +14,7 @@ contract C {
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6368: (212-216): CHC: Out of bounds access happens here.
// Warning 6368: (217-221): CHC: Out of bounds access happens here.
// Warning 3944: (217-232): CHC: Underflow (resulting value less than 0) happens here.
// Warning 6328: (205-239): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
View File

@ -8,8 +8,11 @@ contract C {
a[0][0] = 16;
uint[] storage b = a[0];
b[0] = 32;
// Access is safe but fails due to aliasing.
assert(a[0][0] == 16);
}
}
// ----
// Warning 6328: (167-188): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6368: (221-225): CHC: Out of bounds access happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6368: (221-228): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15]]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6328: (214-235): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

23
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol
View File

@ -4,20 +4,35 @@ contract C {
uint[][] a;
uint[][][] c;
uint[] d;
constructor() {
c.push().push().push();
d.push(); d.push();
}
function f() public {
a.push();
uint[] storage b = a[0];
// Access is safe but oob reported due to aliasing.
c[0][0][0] = 12;
d[5] = 7;
// Access is safe but oob reported due to aliasing.
d[1] = 7;
b.push(8);
assert(a[0].length == 0);
// Safe but knowledge about `c` is erased because `b` could be pointing to `c[x][y]`.
// Access is safe but oob reported due to aliasing.
assert(c[0][0][0] == 12);
// Safe but knowledge about `d` is erased because `b` could be pointing to `d`.
// Removed assertion because current Spacer seg faults in cex generation.
//assert(d[5] == 7);
//assert(d[1] == 7);
}
}
// ----
// Warning 6328: (193-217): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nState: a = [], c = [], d = []\nC.f()
// Warning 6328: (309-333): CHC: Assertion violation happens here.
// Warning 6368: (271-275): CHC: Out of bounds access happens here.
// Warning 6368: (271-278): CHC: Out of bounds access might happen here.
// Warning 6368: (271-281): CHC: Out of bounds access might happen here.
// Warning 6368: (344-348): CHC: Out of bounds access happens here.
// Warning 6368: (376-380): CHC: Out of bounds access happens here.\nCounterexample:\na = [], d = [5, 5, 5, 5, 5, 5, 5, 5, 7, 5, 9, 5, 11, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n\nTransaction trace:\nC.constructor()\nState: a = [], c = [[[0]]], d = [0, 0]\nC.f()
// Warning 6328: (369-393): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nState: a = [], c = [[[0]]], d = [0, 0]\nC.f()
// Warning 6368: (546-550): CHC: Out of bounds access happens here.\nCounterexample:\nc = []\n\nTransaction trace:\nC.constructor()\nState: a = [], c = [[[0]]], d = [0, 0]\nC.f()
// Warning 6368: (546-553): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nState: a = [], c = [[[0]]], d = [0, 0]\nC.f()
// Warning 6368: (546-556): CHC: Out of bounds access happens here.
// Warning 6328: (539-563): CHC: Assertion violation happens here.

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

@ -4,7 +4,7 @@ contract C {
uint[][] a;
function f() public {
a.push();
a[0].push();
a[a.length - 1].push();
assert(a[a.length - 1][0] == 0);
}
}

4
test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol
View File

@ -4,9 +4,9 @@ contract C {
uint[][] a;
function f() public {
a.push();
a[0].push();
a[a.length - 1].push();
assert(a[a.length - 1][0] == 100);
}
}
// ----
// Warning 6328: (111-144): CHC: Assertion violation happens here.\nCounterexample:\na = [[0]]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6328: (122-155): CHC: Assertion violation happens here.\nCounterexample:\na = [[0]]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

9
test/libsolidity/smtCheckerTests/functions/getters/array_1.sol
View File

@ -2,7 +2,12 @@ pragma experimental SMTChecker;
contract C {
uint[] public a;
constructor() {
a.push();
a.push();
a.push();
a.push();
}
function f() public view {
uint y = this.a(2);
assert(y == a[2]); // should hold
@ -10,4 +15,4 @@ contract C {
}
}
// ----
// Warning 6328: (153-167): CHC: Assertion violation happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6328: (220-234): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0, 0, 0]\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0, 0, 0]\nC.f()

14
test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
View File

@ -2,12 +2,22 @@ pragma experimental SMTChecker;
contract C {
uint[][] public a;
constructor() {
a.push();
a.push();
a.push();
a[2].push();
a[2].push();
a[2].push();
a[2].push();
}
function f() public view {
uint y = this.a(2,3);
assert(y == a[2][3]); // should hold
assert(y == 1); // should fail
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (160-174): CHC: Assertion violation happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6328: (275-289): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol
View File

@ -17,5 +17,7 @@ contract C {
assert(y == 1); // should fail
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (289-303): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (289-303): CHC: Assertion violation happens here.

Some files were not shown because too many files have changed in this diff Show More