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

Add paris constraints to SMTChecker

Browse Source 
Co-authored-by: Daniel <daniel@ekpyron.org>
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
Co-authored-by: Leo <leo@ethereum.org>
This commit is contained in:
Rodrigo Q. Saramago 2023-01-19 13:06:23 +00:00
parent d9d9ab30a2
commit feba4de509
No known key found for this signature in database
GPG Key ID: 9B36B2525704A359
26 changed files with 183 additions and 102 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -173,7 +173,7 @@ at each version. Backward compatibility is not guaranteed between each version.
- ``london``
- The block's base fee (`EIP-3198 <https://eips.ethereum.org/EIPS/eip-3198>`_ and `EIP-1559 <https://eips.ethereum.org/EIPS/eip-1559>`_) can be accessed via the global ``block.basefee`` or ``basefee()`` in inline assembly.
- ``paris`` (**default**)
- Introduces ``prevrandao()`` and ``block.prevrandao``, and changes the semantics of the ``block.difficulty``, disallowing ``difficulty()`` in inline assembly (see `EIP-4399 <https://eips.ethereum.org/EIPS/eip-4399>`_).
- Introduces ``prevrandao()`` and ``block.prevrandao``, and changes the semantics of the now deprecated ``block.difficulty``, disallowing ``difficulty()`` in inline assembly (see `EIP-4399 <https://eips.ethereum.org/EIPS/eip-4399>`_).
.. index:: ! standard JSON, ! --standard-json
.. _compiler-api:

10
libsolidity/formal/Predicate.cpp
View File

@ -255,8 +255,14 @@ string Predicate::formatSummaryCall(
if (auto const* identifier = dynamic_cast<Identifier const*>(memberExpr))
{
ASTString const& name = identifier->name();
auto memberName = _memberAccess.memberName();
// TODO remove this for 0.9.0
if (name == "block" && memberName == "difficulty")
memberName = "prevrandao";
if (name == "block" || name == "msg" || name == "tx")
txVars.insert(name + "." + _memberAccess.memberName());
txVars.insert(name + "." + memberName);
}
return true;
@ -642,7 +648,7 @@ map<string, optional<string>> Predicate::readTxVars(smtutil::Expression const& _
{"block.basefee", TypeProvider::uint256()},
{"block.chainid", TypeProvider::uint256()},
{"block.coinbase", TypeProvider::address()},
{"block.difficulty", TypeProvider::uint256()},
{"block.prevrandao", TypeProvider::uint256()},
{"block.gaslimit", TypeProvider::uint256()},
{"block.number", TypeProvider::uint256()},
{"block.timestamp", TypeProvider::uint256()},

8
libsolidity/formal/SMTEncoder.cpp
View File

@ -1337,7 +1337,13 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
{
auto const& name = identifier->name();
solAssert(name == "block" || name == "msg" || name == "tx", "");
defineExpr(_memberAccess, state().txMember(name + "." + _memberAccess.memberName()));
auto memberName = _memberAccess.memberName();
// TODO remove this for 0.9.0
if (name == "block" && memberName == "difficulty")
memberName = "prevrandao";
defineExpr(_memberAccess, state().txMember(name + "." + memberName));
}
else if (auto magicType = dynamic_cast<MagicType const*>(exprType))
{

9
libsolidity/formal/SymbolicState.cpp
View File

@ -142,13 +142,20 @@ smtutil::Expression SymbolicState::txMember(string const& _member) const
return m_tx.member(_member);
}
smtutil::Expression SymbolicState::evmParisConstraints() const
{
// Ensure prevrandao range as defined by EIP-4399.
return txMember("block.prevrandao") > (u256(1) << 64);
}
smtutil::Expression SymbolicState::txTypeConstraints() const
{
return
evmParisConstraints() &&
smt::symbolicUnknownConstraints(m_tx.member("block.basefee"), TypeProvider::uint256()) &&
smt::symbolicUnknownConstraints(m_tx.member("block.chainid"), TypeProvider::uint256()) &&
smt::symbolicUnknownConstraints(m_tx.member("block.coinbase"), TypeProvider::address()) &&
smt::symbolicUnknownConstraints(m_tx.member("block.difficulty"), TypeProvider::uint256()) &&
smt::symbolicUnknownConstraints(m_tx.member("block.prevrandao"), TypeProvider::uint256()) &&
smt::symbolicUnknownConstraints(m_tx.member("block.gaslimit"), TypeProvider::uint256()) &&
smt::symbolicUnknownConstraints(m_tx.member("block.number"), TypeProvider::uint256()) &&
smt::symbolicUnknownConstraints(m_tx.member("block.timestamp"), TypeProvider::uint256()) &&

5
libsolidity/formal/SymbolicState.h
View File

@ -68,9 +68,9 @@ private:
* - block basefee
* - block chainid
* - block coinbase
* - block difficulty
* - block gaslimit
* - block number
* - block prevrandao
* - block timestamp
* - TODO gasleft
* - msg data
@ -136,6 +136,7 @@ public:
smtutil::Expression txTypeConstraints() const;
smtutil::Expression txNonPayableConstraint() const;
smtutil::Expression blockhash(smtutil::Expression _blockNumber) const;
smtutil::Expression evmParisConstraints() const;
//@}
/// Crypto functions.
@ -197,7 +198,7 @@ private:
{"block.basefee", smtutil::SortProvider::uintSort},
{"block.chainid", smtutil::SortProvider::uintSort},
{"block.coinbase", smt::smtSort(*TypeProvider::address())},
{"block.difficulty", smtutil::SortProvider::uintSort},
{"block.prevrandao", smtutil::SortProvider::uintSort},
{"block.gaslimit", smtutil::SortProvider::uintSort},
{"block.number", smtutil::SortProvider::uintSort},
{"block.timestamp", smtutil::SortProvider::uintSort},

64
test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json
View File

@ -3,38 +3,11 @@
{
"smtlib2queries":
{
"0x2bcd3328dc8d31e869efd5e0dfdb16a6fa26f0a9c2829ea55670262be485e401": "(set-option :produce-models true)
(set-logic ALL)
(declare-fun |x_3_3| () Int)
(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.basefee| Int) (|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-fun |x_3_4| () Int)
(declare-fun |x_3_0| () Int)
(declare-fun |expr_7_0| () Int)
(declare-fun |expr_8_0| () Int)
(declare-fun |expr_9_1| () Bool)
(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> (and true true) true) (and (= expr_8_0 0) (and (=> (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_3_0))
(check-sat)
(get-value (|EVALEXPR_0| ))
",
"0x4e70784a8a93c7429a716aa8b778f3de5d1f63b30158452534da5d44e5967d2b": "(set-logic HORN)
"0x0ebc730de380833af1e52ed063befb32994bc637929c942b7fd089b7cd3ba64e": "(set-logic HORN)
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(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.basefee| Int) (|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-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| 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-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-datatypes ((|abi_type| 0)) (((|abi_type|))))
@ -95,7 +68,7 @@
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (block_9_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 x_3_1 state_3 x_3_2) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true))))))) true) (summary_4_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_3 x_3_2))))
(=> (and (and (block_9_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 x_3_1 state_3 x_3_2) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| 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) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true))))))) true) (summary_4_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_3 x_3_2))))
(assert
@ -139,7 +112,7 @@
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (summary_constructor_2_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1))))
(=> (and (and (summary_constructor_2_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| 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))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1))))
(declare-fun |error_target_3_0| () Bool)
@ -151,7 +124,34 @@
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> error_target_3_0 false)))
(check-sat)"
(check-sat)",
"0xcb822e6220a39244d26887a0fa6f62b06718359056555679fb06dd7dff18bb86": "(set-option :produce-models true)
(set-logic ALL)
(declare-fun |x_3_3| () Int)
(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.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| 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-fun |x_3_4| () Int)
(declare-fun |x_3_0| () Int)
(declare-fun |expr_7_0| () Int)
(declare-fun |expr_8_0| () Int)
(declare-fun |expr_9_1| () Bool)
(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> (and true true) true) (and (= expr_8_0 0) (and (=> (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| 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) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_3_0))
(check-sat)
(get-value (|EVALEXPR_0| ))
"
}
},
"errors":

7
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol
View File

@ -3,12 +3,13 @@ contract C {
bytes memory b1 = abi.encodeWithSignature(sig, x, a);
bytes memory b2 = abi.encodeWithSelector(bytes4(keccak256(bytes(sig))), x, a);
// should hold but we do not evaluate keccak256 in an interpreted way
assert(b1.length == b2.length);
//assert(b1.length == b2.length);
assert(b1.length != b2.length); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (294-324): CHC: Assertion violation might happen here.
// Warning 7812: (294-324): BMC: Assertion violation might happen here.
// Warning 6328: (330-360): CHC: Assertion violation might happen here.
// Warning 7812: (330-360): BMC: Assertion violation might happen here.

2
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol
View File

@ -26,7 +26,7 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (335-365): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [69]\nb2 = [0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43]\nb3 = []\nb4 = []\nx = 0\ny = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSlice(sig, [69])
// Warning 6328: (335-365): CHC: Assertion violation happens here.
// Warning 6328: (589-619): CHC: Assertion violation happens here.
// Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
// Warning 4661: (1087-1117): BMC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/bmc_coverage/range_check.sol
View File

@ -17,6 +17,8 @@ contract C {
assert(block.chainid <= 2**256 - 1);
assert(block.difficulty >= 0);
assert(block.difficulty <= 2**256 - 1);
assert(block.prevrandao > 2**64);
assert(block.prevrandao <= 2**256 - 1);
assert(block.gaslimit >= 0);
assert(block.gaslimit <= 2**256 - 1);
assert(block.number >= 0);
@ -44,6 +46,8 @@ contract D {
assert(block.chainid <= 2**256 - 1);
assert(block.difficulty >= 0);
assert(block.difficulty <= 2**256 - 1);
assert(block.prevrandao > 2**64);
assert(block.prevrandao <= 2**256 - 1);
assert(block.gaslimit >= 0);
assert(block.gaslimit <= 2**256 - 1);
assert(block.number >= 0);
@ -54,3 +58,7 @@ contract D {
// ====
// SMTEngine: bmc
// ----
// Warning 8417: (565-581): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (598-614): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (1447-1463): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (1481-1497): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.

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

@ -16,5 +16,5 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Info 1180: Contract invariant(s) for :C:\n!(x >= 11)\nReentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!(x <= 10) || !(<errorCode> >= 3)) && (!(x <= 10) || !(x' >= 11)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Overflow at ++x\n<errorCode> = 3 -> Assertion failed at assert(x < 11)\n

3
test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol
View File

@ -30,7 +30,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTSolvers: z3
// SMTIgnoreOS: macos
// SMTSolvers: z3
// ----
// Info 1180: Contract invariant(s) for :C:\n!(x >= 7)\n

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

@ -24,6 +24,6 @@ contract LoopFor2 {
}
// ====
// SMTEngine: all
// SMTSolvers: z3
// SMTIgnoreOS: macos
// SMTSolvers: z3
// ----

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

@ -6,5 +6,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6368: (76-90): CHC: Out of bounds access might happen here.

2
test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol
View File

@ -22,6 +22,6 @@ contract C {
// ----
// Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 3944: (181-184): CHC: Underflow (resulting value less than 0) might happen here.
// Warning 6368: (259-263): CHC: Out of bounds access happens here.\nCounterexample:\na = [0], l = 1\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = [], l = 0\nC.p()\nState: a = [0], l = 1\nC.r()
// Warning 6368: (259-263): CHC: Out of bounds access happens here.
// Warning 2661: (112-115): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (181-184): BMC: Underflow (resulting value less than 0) happens here.

18
test/libsolidity/smtCheckerTests/special/block_vars_bmc_internal.sol
View File

@ -1,12 +1,14 @@
contract C {
address coin;
uint dif;
uint prevrandao;
uint gas;
uint number;
uint timestamp;
function f() public {
coin = block.coinbase;
dif = block.difficulty;
prevrandao = block.prevrandao;
gas = block.gaslimit;
number = block.number;
timestamp = block.timestamp;
@ -16,12 +18,14 @@ contract C {
function g() internal view {
assert(uint160(coin) >= 0); // should hold
assert(dif >= 0); // should hold
assert(prevrandao > 2**64); // should hold
assert(gas >= 0); // should hold
assert(number >= 0); // should hold
assert(timestamp >= 0); // should hold
assert(coin == block.coinbase); // should fail with BMC
assert(dif == block.difficulty); // should fail with BMC
assert(prevrandao == block.prevrandao); // should fail with BMC
assert(gas == block.gaslimit); // should fail with BMC
assert(number == block.number); // should fail with BMC
assert(timestamp == block.timestamp); // should fail with BMC
@ -30,8 +34,12 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (473-503): BMC: Assertion violation happens here.
// Warning 4661: (531-562): BMC: Assertion violation happens here.
// Warning 4661: (590-619): BMC: Assertion violation happens here.
// Warning 4661: (647-677): BMC: Assertion violation happens here.
// Warning 4661: (705-741): BMC: Assertion violation happens here.
// Warning 8417: (155-171): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (641-657): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 4661: (409-435): BMC: Assertion violation happens here.
// Warning 4661: (569-599): BMC: Assertion violation happens here.
// Warning 4661: (627-658): BMC: Assertion violation happens here.
// Warning 4661: (686-724): BMC: Assertion violation happens here.
// Warning 4661: (752-781): BMC: Assertion violation happens here.
// Warning 4661: (809-839): BMC: Assertion violation happens here.
// Warning 4661: (867-903): BMC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol
View File

@ -1,12 +1,14 @@
contract C {
address coin;
uint dif;
uint prevrandao;
uint gas;
uint number;
uint timestamp;
function f() public {
coin = block.coinbase;
dif = block.difficulty;
prevrandao = block.prevrandao;
gas = block.gaslimit;
number = block.number;
timestamp = block.timestamp;
@ -16,12 +18,14 @@ contract C {
function g() internal view {
assert(uint160(coin) >= 0); // should hold
assert(dif >= 0); // should hold
assert(prevrandao > 2**64); // should hold
assert(gas >= 0); // should hold
assert(number >= 0); // should hold
assert(timestamp >= 0); // should hold
assert(coin == block.coinbase); // should hold with CHC
assert(dif == block.difficulty); // should hold with CHC
assert(prevrandao == block.prevrandao); // should hold with CHC
assert(gas == block.gaslimit); // should hold with CHC
assert(number == block.number); // should hold with CHC
assert(timestamp == block.timestamp); // should hold with CHC
@ -33,4 +37,6 @@ contract C {
// SMTEngine: chc
// SMTIgnoreOS: macos
// ----
// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x0, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n C.g() -- internal call
// Warning 8417: (155-171): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (641-657): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 6328: (932-961): CHC: Assertion violation happens here.

11
test/libsolidity/smtCheckerTests/special/difficulty.sol
View File

@ -1,11 +0,0 @@
contract C
{
function f(uint difficulty) public view {
assert(block.difficulty == difficulty);
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (58-96): CHC: Assertion violation happens here.

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

@ -3,6 +3,7 @@ contract C
function f() public payable {
assert(msg.sender == block.coinbase);
assert(block.difficulty == block.gaslimit);
assert(block.prevrandao == block.gaslimit);
assert(block.number == block.timestamp);
assert(tx.gasprice == msg.value);
assert(tx.origin == msg.sender);
@ -17,11 +18,13 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 8417: (93-109): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 6328: (46-82): CHC: Assertion violation happens here.
// Warning 6328: (86-128): CHC: Assertion violation happens here.
// Warning 6328: (132-171): CHC: Assertion violation happens here.
// Warning 6328: (175-207): CHC: Assertion violation happens here.
// Warning 6328: (211-242): CHC: Assertion violation happens here.
// Warning 6328: (295-319): CHC: Assertion violation happens here.
// Warning 6328: (323-351): CHC: Assertion violation happens here.
// Warning 6328: (355-378): CHC: Assertion violation happens here.
// Warning 6328: (132-174): CHC: Assertion violation happens here.
// Warning 6328: (178-217): CHC: Assertion violation happens here.
// Warning 6328: (221-253): CHC: Assertion violation happens here.
// Warning 6328: (257-288): CHC: Assertion violation happens here.
// Warning 6328: (341-365): CHC: Assertion violation happens here.
// Warning 6328: (369-397): CHC: Assertion violation happens here.
// Warning 6328: (401-424): CHC: Assertion violation happens here.

15
test/libsolidity/smtCheckerTests/special/many_internal.sol
View File

@ -6,6 +6,7 @@ contract C
function g() internal {
assert(msg.sender == block.coinbase);
assert(block.difficulty == block.gaslimit);
assert(block.prevrandao == block.gaslimit);
assert(block.number == block.timestamp);
assert(tx.gasprice == msg.value);
assert(tx.origin == msg.sender);
@ -20,11 +21,13 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 8417: (128-144): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 6328: (81-117): CHC: Assertion violation happens here.
// Warning 6328: (121-163): CHC: Assertion violation happens here.
// Warning 6328: (167-206): CHC: Assertion violation happens here.
// Warning 6328: (210-242): CHC: Assertion violation happens here.
// Warning 6328: (246-277): CHC: Assertion violation happens here.
// Warning 6328: (330-354): CHC: Assertion violation happens here.
// Warning 6328: (358-386): CHC: Assertion violation happens here.
// Warning 6328: (390-413): CHC: Assertion violation happens here.
// Warning 6328: (167-209): CHC: Assertion violation happens here.
// Warning 6328: (213-252): CHC: Assertion violation happens here.
// Warning 6328: (256-288): CHC: Assertion violation happens here.
// Warning 6328: (292-323): CHC: Assertion violation happens here.
// Warning 6328: (376-400): CHC: Assertion violation happens here.
// Warning 6328: (404-432): CHC: Assertion violation happens here.
// Warning 6328: (436-459): CHC: Assertion violation happens here.

16
test/libsolidity/smtCheckerTests/special/prevrandao.sol Normal file
View File

@ -0,0 +1,16 @@
contract C
{
function f(uint prevrandao) public view {
assert(block.prevrandao == prevrandao); // should fail
assert(block.difficulty == prevrandao); // should fail
assert(block.difficulty == block.prevrandao); // should hold
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 8417: (122-138): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (179-195): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 6328: (58-96): CHC: Assertion violation happens here.
// Warning 6328: (115-153): CHC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/special/range_check.sol
View File

@ -17,6 +17,8 @@ contract C {
assert(block.chainid <= 2**256 - 1);
assert(block.difficulty >= 0);
assert(block.difficulty <= 2**256 - 1);
assert(block.prevrandao > 2**64);
assert(block.prevrandao <= 2**256 - 1);
assert(block.gaslimit >= 0);
assert(block.gaslimit <= 2**256 - 1);
assert(block.number >= 0);
@ -44,6 +46,8 @@ contract D {
assert(block.chainid <= 2**256 - 1);
assert(block.difficulty >= 0);
assert(block.difficulty <= 2**256 - 1);
assert(block.prevrandao > 2**64);
assert(block.prevrandao <= 2**256 - 1);
assert(block.gaslimit >= 0);
assert(block.gaslimit <= 2**256 - 1);
assert(block.number >= 0);
@ -55,3 +59,7 @@ contract D {
// ====
// SMTEngine: all
// ----
// Warning 8417: (565-581): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (598-614): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (1447-1463): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (1481-1497): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.

7
test/libsolidity/smtCheckerTests/special/tx_data_immutable.sol
View File

@ -2,6 +2,7 @@ contract C {
bytes32 bhash;
address coin;
uint dif;
uint prevrandao;
uint glimit;
uint number;
uint tstamp;
@ -16,6 +17,7 @@ contract C {
bhash = blockhash(12);
coin = block.coinbase;
dif = block.difficulty;
prevrandao = block.prevrandao;
glimit = block.gaslimit;
number = block.number;
tstamp = block.timestamp;
@ -31,6 +33,7 @@ contract C {
assert(bhash == blockhash(12));
assert(coin == block.coinbase);
assert(dif == block.difficulty);
assert(prevrandao == block.prevrandao);
assert(glimit == block.gaslimit);
assert(number == block.number);
assert(tstamp == block.timestamp);
@ -46,6 +49,7 @@ contract C {
assert(bhash == blockhash(12));
assert(coin == block.coinbase);
assert(dif == block.difficulty);
assert(prevrandao == block.prevrandao);
assert(glimit == block.gaslimit);
assert(number == block.number);
assert(tstamp == block.timestamp);
@ -60,3 +64,6 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 8417: (293-309): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (645-661): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (1127-1143): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.

57
test/libsolidity/smtCheckerTests/special/tx_data_immutable_fail.sol
View File

@ -2,6 +2,7 @@ contract C {
bytes32 bhash;
address coin;
uint dif;
uint prevrandao;
uint glimit;
uint number;
uint tstamp;
@ -16,6 +17,7 @@ contract C {
bhash = blockhash(12);
coin = block.coinbase;
dif = block.difficulty;
prevrandao = block.prevrandao;
glimit = block.gaslimit;
number = block.number;
tstamp = block.timestamp;
@ -31,6 +33,7 @@ contract C {
assert(bhash == blockhash(122));
assert(coin != block.coinbase);
assert(dif != block.difficulty);
assert(prevrandao != block.prevrandao);
assert(glimit != block.gaslimit);
assert(number != block.number);
assert(tstamp != block.timestamp);
@ -46,6 +49,7 @@ contract C {
assert(bhash == blockhash(122));
assert(coin != block.coinbase);
assert(dif != block.difficulty);
assert(prevrandao != block.prevrandao);
assert(glimit != block.gaslimit);
assert(number != block.number);
assert(tstamp != block.timestamp);
@ -61,27 +65,32 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (512-543): CHC: Assertion violation happens here.
// Warning 6328: (547-577): CHC: Assertion violation happens here.
// Warning 6328: (581-612): CHC: Assertion violation happens here.
// Warning 6328: (616-648): CHC: Assertion violation happens here.
// Warning 6328: (652-682): CHC: Assertion violation happens here.
// Warning 6328: (686-719): CHC: Assertion violation happens here.
// Warning 6328: (723-762): CHC: Assertion violation happens here.
// Warning 6328: (766-794): CHC: Assertion violation happens here.
// Warning 6328: (798-820): CHC: Assertion violation happens here.
// Warning 6328: (824-850): CHC: Assertion violation happens here.
// Warning 6328: (854-883): CHC: Assertion violation happens here.
// Warning 6328: (887-914): CHC: Assertion violation happens here.
// Warning 6328: (953-984): CHC: Assertion violation happens here.
// Warning 6328: (988-1018): CHC: Assertion violation happens here.
// Warning 6328: (1022-1053): CHC: Assertion violation happens here.
// Warning 6328: (1057-1089): CHC: Assertion violation happens here.
// Warning 6328: (1093-1123): CHC: Assertion violation happens here.
// Warning 6328: (1127-1160): CHC: Assertion violation happens here.
// Warning 6328: (1164-1203): CHC: Assertion violation happens here.
// Warning 6328: (1207-1235): CHC: Assertion violation happens here.
// Warning 6328: (1239-1261): CHC: Assertion violation happens here.
// Warning 6328: (1265-1291): CHC: Assertion violation happens here.
// Warning 6328: (1295-1324): CHC: Assertion violation happens here.
// Warning 6328: (1328-1355): CHC: Assertion violation happens here.
// Warning 8417: (293-309): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (646-662): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (1129-1145): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 6328: (563-594): CHC: Assertion violation happens here.
// Warning 6328: (598-628): CHC: Assertion violation happens here.
// Warning 6328: (632-663): CHC: Assertion violation happens here.
// Warning 6328: (667-705): CHC: Assertion violation happens here.
// Warning 6328: (709-741): CHC: Assertion violation happens here.
// Warning 6328: (745-775): CHC: Assertion violation happens here.
// Warning 6328: (779-812): CHC: Assertion violation happens here.
// Warning 6328: (816-855): CHC: Assertion violation happens here.
// Warning 6328: (859-887): CHC: Assertion violation happens here.
// Warning 6328: (891-913): CHC: Assertion violation happens here.
// Warning 6328: (917-943): CHC: Assertion violation happens here.
// Warning 6328: (947-976): CHC: Assertion violation happens here.
// Warning 6328: (980-1007): CHC: Assertion violation happens here.
// Warning 6328: (1046-1077): CHC: Assertion violation happens here.
// Warning 6328: (1081-1111): CHC: Assertion violation happens here.
// Warning 6328: (1115-1146): CHC: Assertion violation happens here.
// Warning 6328: (1150-1188): CHC: Assertion violation happens here.
// Warning 6328: (1192-1224): CHC: Assertion violation happens here.
// Warning 6328: (1228-1258): CHC: Assertion violation happens here.
// Warning 6328: (1262-1295): CHC: Assertion violation happens here.
// Warning 6328: (1299-1338): CHC: Assertion violation happens here.
// Warning 6328: (1342-1370): CHC: Assertion violation happens here.
// Warning 6328: (1374-1396): CHC: Assertion violation happens here.
// Warning 6328: (1400-1426): CHC: Assertion violation happens here.
// Warning 6328: (1430-1459): CHC: Assertion violation happens here.
// Warning 6328: (1463-1490): CHC: Assertion violation happens here.

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

@ -32,5 +32,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6368: (374-381): CHC: Out of bounds access might happen here.
// Warning 6368: (456-462): CHC: Out of bounds access happens here.
// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 4)\n!(a[2].length <= 2)\n

2
test/libsolidity/smtCheckerTests/userTypes/user_type_as_array_elem_1.sol
View File

@ -11,6 +11,8 @@ contract C {
assert(T.unwrap(arr[i]) == address(42)); // should hold
}
}
// ====
// SMTIgnoreOS: macos
// ----
// Warning 6328: (204-243): CHC: Assertion violation might happen here.
// Warning 4661: (204-243): BMC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/userTypes/user_type_as_struct_member_1.sol
View File

@ -23,3 +23,4 @@ contract C {
);
}
}
// ----