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

Do not create VCs for underoverflow by default for Sol >=0.8

Browse Source
This commit is contained in:
Leo Alt 2021-07-07 12:31:09 +02:00
parent 6ec711b2f0
commit ee6285d6d7
28 changed files with 341 additions and 329 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -11,6 +11,7 @@ Compiler Features:
* Commandline Interface: option ``--pretty-json`` works also with ``--standard--json``.
* SMTChecker: Unproved targets are hidden by default, and the SMTChecker only states how many unproved targets there are. They can be listed using the command line option ``--model-checker-show-unproved`` or the JSON option ``settings.modelChecker.showUnproved``.
* SMTChecker: new setting to enable/disable encoding of division and modulo with slack variables. The command line option is ``--model-checker-div-mod-slacks`` and the JSON option is ``settings.modelChecker.divModWithSlacks``.
* SMTChecker: Do not check underflow and overflow by default.
Bugfixes:

13
docs/smtchecker.rst
View File

@ -34,6 +34,9 @@ The other verification targets that the SMTChecker checks at compile time are:
- Out of bounds index access.
- Insufficient funds for a transfer.
All the targets above are automatically checked by default if all engines are
enabled, except underflow and overflow for Solidity >=0.8.7.
The potential warnings that the SMTChecker reports are:
- ``<failing property> happens here.``. This means that the SMTChecker proved that a certain property fails. A counterexample may be given, however in complex situations it may also not show a counterexample. This result may also be a false positive in certain cases, when the SMT encoding adds abstractions for Solidity code that is either hard or impossible to express.
@ -93,8 +96,10 @@ Overflow
}
The contract above shows an overflow check example.
The SMTChecker will, by default, check every reachable arithmetic operation
in the contract for potential underflow and overflow.
The SMTChecker does not check underflow and overflow by default for Solidity >=0.8.7,
so we need to use the command line option ``--model-checker-targets "underflow,overflow"``
or the JSON option ``settings.modelChecker.targets = ["underflow", "overflow"]``.
See :ref:`this section for targets configuration<smtchecker_targets>`.
Here, it reports the following:
.. code-block:: text
@ -447,6 +452,8 @@ If the SMTChecker does not manage to solve the contract properties with the defa
a timeout can be given in milliseconds via the CLI option ``--model-checker-timeout <time>`` or
the JSON option ``settings.modelChecker.timeout=<time>``, where 0 means no timeout.
.. _smtchecker_targets:
Verification Targets
====================
@ -471,6 +478,8 @@ The keywords that represent the targets are:
A common subset of targets might be, for example:
``--model-checker-targets assert,overflow``.
All targets are checked by default, except underflow and overflow for Solidity >=0.8.7.
There is no precise heuristic on how and when to split verification targets,
but it can be useful especially when dealing with large contracts.

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

@ -415,7 +415,8 @@ Input Description
"solvers": ["cvc4", "smtlib2", "z3"],
// Choose which targets should be checked: constantCondition,
// underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds.
// If the option is not given all targets are checked by default.
// If the option is not given all targets are checked by default,
// except underflow/overflow for Solidity >=0.8.7.
// See the Formal Verification section for the targets description.
"targets": ["underflow", "overflow", "assert"],
// Timeout for each SMT query in milliseconds.

9
libsolidity/formal/ModelCheckerSettings.cpp
View File

@ -40,9 +40,16 @@ map<string, TargetType> const ModelCheckerTargets::targetStrings{
std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets)
{
set<TargetType> chosenTargets;
if (_targets == "default")
if (_targets == "default" || _targets == "all")
{
bool all = _targets == "all";
for (auto&& v: targetStrings | ranges::views::values)
{
if (!all && (v == TargetType::Underflow || v == TargetType::Overflow))
continue;
chosenTargets.insert(v);
}
}
else
for (auto&& t: _targets | ranges::views::split(',') | ranges::to<vector<string>>())
{

3
libsolidity/formal/ModelCheckerSettings.h
View File

@ -91,7 +91,10 @@ enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, Unde
struct ModelCheckerTargets
{
/// Adds the default targets, that is, all except underflow and overflow.
static ModelCheckerTargets Default() { return *fromString("default"); }
/// Adds all targets, including underflow and overflow.
static ModelCheckerTargets All() { return *fromString("all"); }
static std::optional<ModelCheckerTargets> fromString(std::string const& _targets);

6
solc/CommandLineParser.cpp
View File

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

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

@ -0,0 +1 @@
--model-checker-engine all --model-checker-targets all

16
test/cmdlineTests/model_checker_targets_all/err → test/cmdlineTests/model_checker_targets_all_all_engines/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> model_checker_targets_all/input.sol:7:3:
--> model_checker_targets_all_all_engines/input.sol:7:3:
|
7 | --x;
| ^^^
@ -23,7 +23,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> model_checker_targets_all/input.sol:8:3:
--> model_checker_targets_all_all_engines/input.sol:8:3:
|
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
@ -38,7 +38,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:9:3:
--> model_checker_targets_all_all_engines/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
@ -53,7 +53,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:11:3:
--> model_checker_targets_all_all_engines/input.sol:11:3:
|
11 | assert(x > 0);
| ^^^^^^^^^^^^^
@ -68,7 +68,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:12:3:
--> model_checker_targets_all_all_engines/input.sol:12:3:
|
12 | arr.pop();
| ^^^^^^^^^
@ -83,20 +83,20 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:13:3:
--> model_checker_targets_all_all_engines/input.sol:13:3:
|
13 | arr[x];
| ^^^^^^
Warning: BMC: Condition is always true.
--> model_checker_targets_all/input.sol:6:11:
--> model_checker_targets_all_all_engines/input.sol:6:11:
|
6 | require(x >= 0);
| ^^^^^^
Note: Callstack:
Warning: BMC: Insufficient funds happens here.
--> model_checker_targets_all/input.sol:10:3:
--> model_checker_targets_all_all_engines/input.sol:10:3:
|
10 | a.transfer(x);
| ^^^^^^^^^^^^^

0
test/cmdlineTests/model_checker_targets_all/input.sol → test/cmdlineTests/model_checker_targets_all_all_engines/input.sol
View File

2
test/cmdlineTests/model_checker_targets_all_bmc/args
View File

@ -1 +1 @@
--model-checker-engine bmc --model-checker-targets default
--model-checker-engine bmc --model-checker-targets all

2
test/cmdlineTests/model_checker_targets_all_chc/args
View File

@ -1 +1 @@
--model-checker-engine chc --model-checker-targets default
--model-checker-engine chc --model-checker-targets all

0
test/cmdlineTests/model_checker_targets_all/args → test/cmdlineTests/model_checker_targets_default_all_engines/args
View File

78
test/cmdlineTests/model_checker_targets_default_all_engines/err Normal file
View File

@ -0,0 +1,78 @@
Warning: CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_default_all_engines/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Warning: CHC: Assertion violation happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_default_all_engines/input.sol:11:3:
|
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Warning: CHC: Empty array "pop" happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_default_all_engines/input.sol:12:3:
|
12 | 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_default_all_engines/input.sol:13:3:
|
13 | arr[x];
| ^^^^^^
Warning: BMC: Condition is always true.
--> model_checker_targets_default_all_engines/input.sol:6:11:
|
6 | require(x >= 0);
| ^^^^^^
Note: Callstack:
Warning: BMC: Insufficient funds happens here.
--> model_checker_targets_default_all_engines/input.sol:10:3:
|
10 | a.transfer(x);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0
x = 0
Note: Callstack:
Note:

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

@ -0,0 +1,15 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
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_default_bmc/args Normal file
View File

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

43
test/cmdlineTests/model_checker_targets_default_bmc/err Normal file
View File

@ -0,0 +1,43 @@
Warning: BMC: Condition is always true.
--> model_checker_targets_default_bmc/input.sol:6:11:
|
6 | require(x >= 0);
| ^^^^^^
Note: Callstack:
Warning: BMC: Division by zero happens here.
--> model_checker_targets_default_bmc/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Note: Counterexample:
<result> = 0
a = 0
x = 0
Note: Callstack:
Note:
Warning: BMC: Insufficient funds happens here.
--> model_checker_targets_default_bmc/input.sol:10:3:
|
10 | a.transfer(x);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0
x = 0
Note: Callstack:
Note:
Warning: BMC: Assertion violation happens here.
--> model_checker_targets_default_bmc/input.sol:11:3:
|
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0
x = 0
Note: Callstack:
Note:

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

@ -0,0 +1,15 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
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_default_chc/args Normal file
View File

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

59
test/cmdlineTests/model_checker_targets_default_chc/err Normal file
View File

@ -0,0 +1,59 @@
Warning: CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_default_chc/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Warning: CHC: Assertion violation happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_default_chc/input.sol:11:3:
|
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Warning: CHC: Empty array "pop" happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_default_chc/input.sol:12:3:
|
12 | 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_default_chc/input.sol:13:3:
|
13 | arr[x];
| ^^^^^^

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

@ -0,0 +1,15 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
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];
}
}

0
test/cmdlineTests/standard_model_checker_targets_all/input.json → test/cmdlineTests/standard_model_checker_targets_default_all_engines/input.json
View File

162
test/cmdlineTests/standard_model_checker_targets_all/output.json → test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json
View File

@ -1,4 +1,59 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x8a1785699211e91e2593e2568d4240af6ec3b4ba113087fcb6f42bc764040d83":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x196770bc73875d44bb894706d45e41767470fb493b21a0b476d2d94ba750f250":"(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_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |d_div_mod_10_0| () Int)
(declare-fun |r_div_mod_10_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint_array_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint_array_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint_array_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (=> (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (=> (and true true) (and (>= expr_30_1 0) (<= expr_30_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_1 (ite (= expr_29_0 0) 0 d_div_mod_10_0)) (and (and (<= 0 r_div_mod_10_0) (or (= expr_29_0 0) (< r_div_mod_10_0 expr_29_0))) (and (= (+ (* d_div_mod_10_0 expr_29_0) r_div_mod_10_0) expr_28_0) (and (=> (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (=> (and true true) true) (and (= expr_28_0 2) (and (=> (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (=> (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (=> (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (=> (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_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_35_0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_8_1))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
","0x8a1785699211e91e2593e2568d4240af6ec3b4ba113087fcb6f42bc764040d83":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -48,110 +103,7 @@
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_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)))))))))) (not expr_14_1)))
(check-sat)
","0xf74fc530d5dd4498f4ad9eeb32a713af6cc6966efcd3e58083b97f864fdc7cbb":"(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_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |d_div_mod_14_0| () Int)
(declare-fun |r_div_mod_14_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint_array_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint_array_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint_array_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (=> (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (=> (and true true) (and (>= expr_30_1 0) (<= expr_30_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_1 (ite (= expr_29_0 0) 0 d_div_mod_14_0)) (and (and (<= 0 r_div_mod_14_0) (or (= expr_29_0 0) (< r_div_mod_14_0 expr_29_0))) (and (= (+ (* d_div_mod_14_0 expr_29_0) r_div_mod_14_0) expr_28_0) (and (=> (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (=> (and true true) true) (and (= expr_28_0 2) (and (=> (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (=> (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (=> (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (=> (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_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_35_0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_8_1))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
"}},"errors":[{"component":"general","errorCode":"3944","formattedMessage":"Warning: CHC: Underflow (resulting value less than 0) happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> A:8:7:
|
8 | \t\t\t\t\t\t--x;
| \t\t\t\t\t\t^^^
","message":"CHC: Underflow (resulting value less than 0) happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
arr = []
a = 0
x = 1
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> A:9:7:
|
9 | \t\t\t\t\t\tx + type(uint).max;
| \t\t\t\t\t\t^^^^^^^^^^^^^^^^^^
","message":"CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
arr = []
a = 0
x = 1
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"},{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
"}},"errors":[{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0

0
test/cmdlineTests/standard_model_checker_targets_all_bmc/input.json → test/cmdlineTests/standard_model_checker_targets_default_bmc/input.json
View File

150
test/cmdlineTests/standard_model_checker_targets_all_bmc/output.json → test/cmdlineTests/standard_model_checker_targets_default_bmc/output.json
View File

@ -190,63 +190,6 @@
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_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_14_1))
(check-sat)
","0xc4955111313d5bc83a8e7aece746156804afbd102ec8a78c06b2a284470deebc":"(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_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint_array_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint_array_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint_array_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (=> (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (=> (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_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_20_0 expr_25_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_8_1))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| (+ expr_20_0 expr_25_1)))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
","0xd5b9836c53d2b59d5215cfe646b8a2d6702aed014aae55a9512896c876117d01":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
@ -272,63 +215,6 @@
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_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)))))))))) (not expr_14_1)))
(check-sat)
","0xf8a9e6ce3d09ef3b2a597297e00abd8e9cdfee9d2491deb6cb8349f0ee53fc61":"(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_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint_array_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint_array_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint_array_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_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_17_0 1) 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_8_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| (- expr_17_0 1)))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
"}},"errors":[{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
--> A:7:15:
|
@ -336,41 +222,7 @@
| \t\t\t\t\t\t ^^^^^^
Note: Callstack:
","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":165,"file":"A","start":159},"type":"Warning"},{"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":177,"file":"A","start":174},"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":203,"file":"A","start":185},"type":"Warning"},{"component":"general","errorCode":"3046","formattedMessage":"Warning: BMC: Division by zero happens here.
","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":165,"file":"A","start":159},"type":"Warning"},{"component":"general","errorCode":"3046","formattedMessage":"Warning: BMC: Division by zero happens here.
--> A:10:7:
|
10 | \t\t\t\t\t\t2 / x;

0
test/cmdlineTests/standard_model_checker_targets_all_chc/input.json → test/cmdlineTests/standard_model_checker_targets_default_chc/input.json
View File

50
test/cmdlineTests/standard_model_checker_targets_all_chc/output.json → test/cmdlineTests/standard_model_checker_targets_default_chc/output.json
View File

@ -1,52 +1,4 @@
{"errors":[{"component":"general","errorCode":"3944","formattedMessage":"Warning: CHC: Underflow (resulting value less than 0) happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> A:8:7:
|
8 | \t\t\t\t\t\t--x;
| \t\t\t\t\t\t^^^
","message":"CHC: Underflow (resulting value less than 0) happens here.
Counterexample:
arr = []
a = 0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
arr = []
a = 0
x = 1
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> A:9:7:
|
9 | \t\t\t\t\t\tx + type(uint).max;
| \t\t\t\t\t\t^^^^^^^^^^^^^^^^^^
","message":"CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
arr = []
a = 0
x = 1
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"},{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
{"errors":[{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0

4
test/libsolidity/SMTCheckerTest.cpp
View File

@ -45,6 +45,10 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
m_modelCheckerSettings.solvers &= ModelChecker::availableSolvers();
/// Underflow and Overflow are not enabled by default for Solidity >=0.8.7,
/// so we explicitly enable all targets for the tests.
m_modelCheckerSettings.targets = ModelCheckerTargets::All();
auto engine = ModelCheckerEngine::fromString(m_reader.stringSetting("SMTEngine", "all"));
if (engine)
m_modelCheckerSettings.engine = *engine;

21
test/libsolidity/SMTCheckerTest.h
View File

@ -43,16 +43,19 @@ public:
void filterObtainedErrors() override;
protected:
/// This contains engine and timeout.
/// The engine can be set via option SMTEngine in the test.
/// The possible options are `all`, `chc`, `bmc`, `none`,
/// where the default is `all`.
ModelCheckerSettings m_modelCheckerSettings;
/*
Options that can be set in the test:
SMTEngine: `all`, `chc`, `bmc`, `none`, where the default is `all`.
Set in m_modelCheckerSettings.
SMTIgnoreCex: `yes`, `no`, where the default is `no`.
Set in m_ignoreCex.
SMTShowUnproved: `yes`, `no`, where the default is `yes`.
Set in m_modelCheckerSettings.
SMTSolvers: `all`, `cvc4`, `z3`, `none`, where the default is `all`.
Set in m_modelCheckerSettings.
*/
/// This is set via option SMTSolvers in the test.
/// The possible options are `all`, `z3`, `cvc4`, `none`,
/// where if none is given the default used option is `all`.
smtutil::SMTSolverChoice m_enabledSolvers;
ModelCheckerSettings m_modelCheckerSettings;
bool m_ignoreCex = false;
};