Merge pull request #13026 from ethereum/develop

Merge develop into breaking.
This commit is contained in:
chriseth 2022-05-16 15:29:39 +02:00 committed by GitHub
commit 3c2cee5836
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
43 changed files with 292 additions and 133 deletions

View File

@ -9,20 +9,20 @@ version: 2.1
parameters: parameters:
ubuntu-2004-docker-image: ubuntu-2004-docker-image:
type: string type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-12 # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-13
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:5087cc068b48787e89887804e632120b3e65bc5c25086bdf7b152be4fe5fc9ba" default: "solbuildpackpusher/solidity-buildpack-deps@sha256:aa64242ecba4f040a839eadfaf20e8489cf93d1cb96ab90df2b240cdbbfe7f7c"
ubuntu-2004-clang-docker-image: ubuntu-2004-clang-docker-image:
type: string type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-12 # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-13
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:7f53f1bc3d89bdfb0725f604efbbec570d80ffa9b731b47a4842f4e286de0355" default: "solbuildpackpusher/solidity-buildpack-deps@sha256:caaf8d42aaf07397d1540e570f096a4fb1ef11fda7da3f1141d8852ec8322a9e"
ubuntu-1604-clang-ossfuzz-docker-image: ubuntu-1604-clang-ossfuzz-docker-image:
type: string type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-17 # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-18
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:85b298c763adf5c516238246beb283640eb555e79e7ad6a8e7a6c9ed47ef6324" default: "solbuildpackpusher/solidity-buildpack-deps@sha256:048002d71a1f86f83dedb79dd057760b752256c75646ba5ad5c1bbe92e1695aa"
emscripten-docker-image: emscripten-docker-image:
type: string type: string
# solbuildpackpusher/solidity-buildpack-deps:emscripten-10 # solbuildpackpusher/solidity-buildpack-deps:emscripten-11
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:bd23831e0025e35a106005b4ac06cb3618f690bfa2833a5881b573c02d35d9fc" default: "solbuildpackpusher/solidity-buildpack-deps@sha256:0ad7c65e8c54d926ba9cb80d56246e4fc49f9284ad5188aaaa4834f46ab0c315"
evm-version: evm-version:
type: string type: string
default: london default: london
@ -990,7 +990,7 @@ jobs:
- gitter_notify_failure_unless_pr - gitter_notify_failure_unless_pr
t_ubu_soltest_all: &t_ubu_soltest_all t_ubu_soltest_all: &t_ubu_soltest_all
<<: *base_ubuntu2004 <<: *base_ubuntu2004_large
parallelism: 50 parallelism: 50
<<: *steps_soltest_all <<: *steps_soltest_all

View File

@ -61,11 +61,11 @@ then
./scripts/install_obsolete_jsoncpp_1_7_4.sh ./scripts/install_obsolete_jsoncpp_1_7_4.sh
# z3 # z3
z3_version="4.8.16" z3_version="4.8.17"
z3_dir="z3-${z3_version}-x64-osx-10.16" z3_dir="z3-${z3_version}-x64-osx-10.16"
z3_package="${z3_dir}.zip" z3_package="${z3_dir}.zip"
wget "https://github.com/Z3Prover/z3/releases/download/z3-${z3_version}/${z3_package}" wget "https://github.com/Z3Prover/z3/releases/download/z3-${z3_version}/${z3_package}"
validate_checksum "$z3_package" 71ed7b6d10c01198187df72cccb8eb6de6d9aa2bf9557b3dd052032524b598a5 validate_checksum "$z3_package" 189667930517aee07f1ce36485d5924a9a2cb4f8c3c9586b03e714a2c657541a
unzip "$z3_package" unzip "$z3_package"
rm "$z3_package" rm "$z3_package"
cp "${z3_dir}/bin/libz3.a" /usr/local/lib cp "${z3_dir}/bin/libz3.a" /usr/local/lib

View File

@ -65,7 +65,7 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
include(EthOptions) include(EthOptions)
configure_project(TESTS) configure_project(TESTS)
set(LATEST_Z3_VERSION "4.8.16") set(LATEST_Z3_VERSION "4.8.17")
set(MINIMUM_Z3_VERSION "4.8.0") set(MINIMUM_Z3_VERSION "4.8.0")
find_package(Z3) find_package(Z3)
if (${Z3_FOUND}) if (${Z3_FOUND})

View File

@ -12,6 +12,10 @@ Breaking changes:
### 0.8.14 (unreleased) ### 0.8.14 (unreleased)
Important Bugfixes:
* ABI Encoding: When ABI-encoding values from calldata that contain nested arrays, correctly validate the nested array length against ``calldatasize()`` in all cases.
Language Features: Language Features:
@ -25,10 +29,10 @@ Compiler Features:
Bugfixes: Bugfixes:
* Type Checker: Properly check restrictions of ``using ... global`` in conjunction with libraries. * Type Checker: Properly check restrictions of ``using ... global`` in conjunction with libraries.
* Assembly-Json: Fix assembly json export to store jump types of operations in `jumpType` field instead of `value`. * Assembly-Json: Fix assembly json export to store jump types of operations in `jumpType` field instead of `value`.
* TypeChecker: Convert parameters of function type to how they would be called for ``abi.encodeCall``. * SMTChecker: Fix bug when z3 is selected but not available at runtime.
* View Pure Checker: Mark ``returndatasize`` and ``returndatacopy`` as view to disallow them in inline assembly blocks in pure functions. * SMTChecker: Fix ABI compatibility with z3 >=4.8.16.
* TypeChecker: Convert parameters of function type to how they would be called for ``abi.encodeCall``.
### 0.8.13 (2022-03-16) ### 0.8.13 (2022-03-16)

View File

@ -1,4 +1,14 @@
[ [
{
"uid": "SOL-2022-2",
"name": "NestedCallataArrayAbiReencodingSizeValidation",
"summary": "ABI-reencoding of nested dynamic calldata arrays did not always perform proper size checks against the size of calldata and could read beyond ``calldatasize()``.",
"description": "Calldata validation for nested dynamic types is deferred until the first access to the nested values. Such an access may for example be a copy to memory or an index or member access to the outer type. While in most such accesses calldata validation correctly checks that the data area of the nested array is completely contained in the passed calldata (i.e. in the range [0, calldatasize()]), this check may not be performed, when ABI encoding such nested types again directly from calldata. For instance, this can happen, if a value in calldata with a nested dynamic array is passed to an external call, used in ``abi.encode`` or emitted as event. In such cases, if the data area of the nested array extends beyond ``calldatasize()``, ABI encoding it did not revert, but continued reading values from beyond ``calldatasize()`` (i.e. zero values).",
"link": "https://blog.soliditylang.org/2022/05/17/calldata-reencode-size-check-bug/",
"introduced": "0.5.8",
"fixed": "0.8.14",
"severity": "very low"
},
{ {
"uid": "SOL-2022-1", "uid": "SOL-2022-1",
"name": "AbiEncodeCallLiteralAsFixedBytesBug", "name": "AbiEncodeCallLiteralAsFixedBytesBug",

View File

@ -1036,6 +1036,7 @@
}, },
"0.5.10": { "0.5.10": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1051,6 +1052,7 @@
}, },
"0.5.11": { "0.5.11": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1065,6 +1067,7 @@
}, },
"0.5.12": { "0.5.12": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1079,6 +1082,7 @@
}, },
"0.5.13": { "0.5.13": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1093,6 +1097,7 @@
}, },
"0.5.14": { "0.5.14": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1109,6 +1114,7 @@
}, },
"0.5.15": { "0.5.15": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1124,6 +1130,7 @@
}, },
"0.5.16": { "0.5.16": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1138,6 +1145,7 @@
}, },
"0.5.17": { "0.5.17": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1269,6 +1277,7 @@
}, },
"0.5.8": { "0.5.8": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1287,6 +1296,7 @@
}, },
"0.5.9": { "0.5.9": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1304,6 +1314,7 @@
}, },
"0.6.0": { "0.6.0": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1319,6 +1330,7 @@
}, },
"0.6.1": { "0.6.1": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1333,6 +1345,7 @@
}, },
"0.6.10": { "0.6.10": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
@ -1343,6 +1356,7 @@
}, },
"0.6.11": { "0.6.11": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
@ -1353,6 +1367,7 @@
}, },
"0.6.12": { "0.6.12": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
@ -1363,6 +1378,7 @@
}, },
"0.6.2": { "0.6.2": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1377,6 +1393,7 @@
}, },
"0.6.3": { "0.6.3": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1391,6 +1408,7 @@
}, },
"0.6.4": { "0.6.4": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
"EmptyByteArrayCopy", "EmptyByteArrayCopy",
@ -1405,6 +1423,7 @@
}, },
"0.6.5": { "0.6.5": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
@ -1419,6 +1438,7 @@
}, },
"0.6.6": { "0.6.6": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
@ -1432,6 +1452,7 @@
}, },
"0.6.7": { "0.6.7": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
@ -1445,6 +1466,7 @@
}, },
"0.6.8": { "0.6.8": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
@ -1455,6 +1477,7 @@
}, },
"0.6.9": { "0.6.9": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
@ -1466,6 +1489,7 @@
}, },
"0.7.0": { "0.7.0": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
@ -1476,6 +1500,7 @@
}, },
"0.7.1": { "0.7.1": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
@ -1487,6 +1512,7 @@
}, },
"0.7.2": { "0.7.2": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
@ -1497,6 +1523,7 @@
}, },
"0.7.3": { "0.7.3": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching", "KeccakCaching",
@ -1506,6 +1533,7 @@
}, },
"0.7.4": { "0.7.4": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching" "KeccakCaching"
@ -1514,6 +1542,7 @@
}, },
"0.7.5": { "0.7.5": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching" "KeccakCaching"
@ -1522,6 +1551,7 @@
}, },
"0.7.6": { "0.7.6": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching" "KeccakCaching"
@ -1530,6 +1560,7 @@
}, },
"0.8.0": { "0.8.0": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching" "KeccakCaching"
@ -1538,6 +1569,7 @@
}, },
"0.8.1": { "0.8.1": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching" "KeccakCaching"
@ -1545,27 +1577,34 @@
"released": "2021-01-27" "released": "2021-01-27"
}, },
"0.8.10": { "0.8.10": {
"bugs": [], "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation"
],
"released": "2021-11-09" "released": "2021-11-09"
}, },
"0.8.11": { "0.8.11": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"AbiEncodeCallLiteralAsFixedBytesBug" "AbiEncodeCallLiteralAsFixedBytesBug"
], ],
"released": "2021-12-20" "released": "2021-12-20"
}, },
"0.8.12": { "0.8.12": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"AbiEncodeCallLiteralAsFixedBytesBug" "AbiEncodeCallLiteralAsFixedBytesBug"
], ],
"released": "2022-02-16" "released": "2022-02-16"
}, },
"0.8.13": { "0.8.13": {
"bugs": [], "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation"
],
"released": "2022-03-16" "released": "2022-03-16"
}, },
"0.8.2": { "0.8.2": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory", "ABIDecodeTwoDimensionalArrayMemory",
"KeccakCaching" "KeccakCaching"
@ -1574,6 +1613,7 @@
}, },
"0.8.3": { "0.8.3": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables", "SignedImmutables",
"ABIDecodeTwoDimensionalArrayMemory" "ABIDecodeTwoDimensionalArrayMemory"
], ],
@ -1581,37 +1621,44 @@
}, },
"0.8.4": { "0.8.4": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables" "SignedImmutables"
], ],
"released": "2021-04-21" "released": "2021-04-21"
}, },
"0.8.5": { "0.8.5": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables" "SignedImmutables"
], ],
"released": "2021-06-10" "released": "2021-06-10"
}, },
"0.8.6": { "0.8.6": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables" "SignedImmutables"
], ],
"released": "2021-06-22" "released": "2021-06-22"
}, },
"0.8.7": { "0.8.7": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"SignedImmutables" "SignedImmutables"
], ],
"released": "2021-08-11" "released": "2021-08-11"
}, },
"0.8.8": { "0.8.8": {
"bugs": [ "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation",
"UserDefinedValueTypesBug", "UserDefinedValueTypesBug",
"SignedImmutables" "SignedImmutables"
], ],
"released": "2021-09-27" "released": "2021-09-27"
}, },
"0.8.9": { "0.8.9": {
"bugs": [], "bugs": [
"NestedCallataArrayAbiReencodingSizeValidation"
],
"released": "2021-09-29" "released": "2021-09-29"
} }
} }

View File

@ -629,6 +629,11 @@ option ``--model-checker-solvers {all,cvc4,smtlib2,z3}`` or the JSON option
- if a dynamic ``z3`` library of version 4.8.x is installed in a Linux system (from Solidity 0.7.6); - if a dynamic ``z3`` library of version 4.8.x is installed in a Linux system (from Solidity 0.7.6);
- statically in ``soljson.js`` (from Solidity 0.6.9), that is, the Javascript binary of the compiler. - statically in ``soljson.js`` (from Solidity 0.6.9), that is, the Javascript binary of the compiler.
.. note::
z3 version 4.8.16 broke ABI compatibility with previous versions and cannot
be used with solc <=0.8.13. If you are using z3 >=4.8.16 please use solc
>=0.8.14.
Since both BMC and CHC use ``z3``, and ``z3`` is available in a greater variety Since both BMC and CHC use ``z3``, and ``z3`` is available in a greater variety
of environments, including in the browser, most users will almost never need to be of environments, including in the browser, most users will almost never need to be
concerned about this option. More advanced users might apply this option to try concerned about this option. More advanced users might apply this option to try

View File

@ -349,7 +349,7 @@ Array Members
**pop()**: **pop()**:
Dynamic storage arrays and ``bytes`` (not ``string``) have a member Dynamic storage arrays and ``bytes`` (not ``string``) have a member
function called ``pop()`` that you can use to remove an element from the function called ``pop()`` that you can use to remove an element from the
end of the array. This also implicitly calls :ref:`delete<delete>` on the removed element. end of the array. This also implicitly calls :ref:`delete<delete>` on the removed element. The function returns nothing.
.. note:: .. note::
Increasing the length of a storage array by calling ``push()`` Increasing the length of a storage array by calling ``push()``

View File

@ -481,8 +481,6 @@ bool SemanticInformation::invalidInPureFunctions(Instruction _instruction)
case Instruction::EXTCODESIZE: case Instruction::EXTCODESIZE:
case Instruction::EXTCODECOPY: case Instruction::EXTCODECOPY:
case Instruction::EXTCODEHASH: case Instruction::EXTCODEHASH:
case Instruction::RETURNDATASIZE:
case Instruction::RETURNDATACOPY:
case Instruction::BLOCKHASH: case Instruction::BLOCKHASH:
case Instruction::COINBASE: case Instruction::COINBASE:
case Instruction::TIMESTAMP: case Instruction::TIMESTAMP:

View File

@ -96,8 +96,8 @@ public:
void clear() { m_errorReporter.clear(); } void clear() { m_errorReporter.clear(); }
private: private:
ErrorReporter m_errorReporter;
ErrorList m_uniqueErrors; ErrorList m_uniqueErrors;
ErrorReporter m_errorReporter;
std::map<std::pair<ErrorId, SourceLocation>, std::string> m_seenErrors; std::map<std::pair<ErrorId, SourceLocation>, std::string> m_seenErrors;
}; };

View File

@ -298,6 +298,7 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
arguments.push_back(fromZ3Expr(_expr.arg(i))); arguments.push_back(fromZ3Expr(_expr.arg(i)));
auto kind = _expr.decl().decl_kind(); auto kind = _expr.decl().decl_kind();
if (_expr.is_ite()) if (_expr.is_ite())
return Expression::ite(arguments[0], arguments[1], arguments[2]); return Expression::ite(arguments[0], arguments[1], arguments[2]);
else if (_expr.is_not()) else if (_expr.is_not())
@ -371,7 +372,10 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
return Expression("dt_accessor_" + _expr.decl().name().str(), arguments, sort); return Expression("dt_accessor_" + _expr.decl().name().str(), arguments, sort);
else if (kind == Z3_OP_DT_IS) else if (kind == Z3_OP_DT_IS)
return Expression("dt_is", {arguments.at(0)}, sort); return Expression("dt_is", {arguments.at(0)}, sort);
else if (kind == Z3_OP_UNINTERPRETED) else if (
kind == Z3_OP_UNINTERPRETED ||
kind == Z3_OP_RECURSIVE
)
return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort())); return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort()));
smtAssert(false, ""); smtAssert(false, "");

View File

@ -1454,7 +1454,7 @@ string ABIFunctions::calldataAccessFunction(Type const& _type)
length := calldataload(value) length := calldataload(value)
value := add(value, 0x20) value := add(value, 0x20)
if gt(length, 0xffffffffffffffff) { <revertStringLength>() } if gt(length, 0xffffffffffffffff) { <revertStringLength>() }
if sgt(base_ref, sub(calldatasize(), mul(length, <calldataStride>))) { <revertStringStride>() } if sgt(value, sub(calldatasize(), mul(length, <calldataStride>))) { <revertStringStride>() }
)") )")
("calldataStride", toCompactHexWithPrefix(arrayType->calldataStride())) ("calldataStride", toCompactHexWithPrefix(arrayType->calldataStride()))
// TODO add test // TODO add test

View File

@ -63,15 +63,14 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
{ {
if (m_interface->solvers() == 0) if (m_interface->solvers() == 0)
{ {
if (!m_noSolverWarning)
{
m_noSolverWarning = true;
m_errorReporter.warning( m_errorReporter.warning(
7710_error, 7710_error,
SourceLocation(), SourceLocation(),
"BMC analysis was not possible since no SMT solver was found and enabled." "BMC analysis was not possible since no SMT solver was found and enabled."
#ifdef HAVE_Z3_DLOPEN
" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
#endif
); );
}
return; return;
} }
@ -108,10 +107,6 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
m_interface->solvers() == 1 && m_interface->solvers() == 1 &&
m_settings.solvers.smtlib2 m_settings.solvers.smtlib2
) )
{
if (!m_noSolverWarning)
{
m_noSolverWarning = true;
m_errorReporter.warning( m_errorReporter.warning(
8084_error, 8084_error,
SourceLocation(), SourceLocation(),
@ -121,8 +116,6 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3." " Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
#endif #endif
); );
}
}
} }
bool BMC::shouldInlineFunctionCall( bool BMC::shouldInlineFunctionCall(

View File

@ -60,21 +60,15 @@ using namespace solidity::frontend::smt;
CHC::CHC( CHC::CHC(
EncodingContext& _context, EncodingContext& _context,
UniqueErrorReporter& _errorReporter, UniqueErrorReporter& _errorReporter,
[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses, map<util::h256, string> const& _smtlib2Responses,
[[maybe_unused]] ReadCallback::Callback const& _smtCallback, ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings, ModelCheckerSettings const& _settings,
CharStreamProvider const& _charStreamProvider CharStreamProvider const& _charStreamProvider
): ):
SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider) SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
m_smtlib2Responses(_smtlib2Responses),
m_smtCallback(_smtCallback)
{ {
bool usesZ3 = m_settings.solvers.z3;
#ifdef HAVE_Z3
usesZ3 = usesZ3 && Z3Interface::available();
#else
usesZ3 = false;
#endif
if (!usesZ3 && m_settings.solvers.smtlib2)
m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback, m_settings.timeout);
} }
void CHC::analyze(SourceUnit const& _source) void CHC::analyze(SourceUnit const& _source)
@ -82,17 +76,26 @@ void CHC::analyze(SourceUnit const& _source)
if (!shouldAnalyze(_source)) if (!shouldAnalyze(_source))
return; return;
if (!m_settings.solvers.z3 && !m_settings.solvers.smtlib2) bool usesZ3 = m_settings.solvers.z3;
#ifdef HAVE_Z3_DLOPEN
if (m_settings.solvers.z3 && !Z3Interface::available())
{ {
if (!m_noSolverWarning) usesZ3 = false;
m_errorReporter.warning(
8158_error,
SourceLocation(),
"z3 was selected as a Horn solver for CHC analysis but libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
);
}
#endif
if (!usesZ3 && !m_settings.solvers.smtlib2)
{ {
m_noSolverWarning = true;
m_errorReporter.warning( m_errorReporter.warning(
7649_error, 7649_error,
SourceLocation(), SourceLocation(),
"CHC analysis was not possible since no Horn solver was enabled." "CHC analysis was not possible since no Horn solver was found and enabled."
); );
}
return; return;
} }
@ -115,20 +118,13 @@ void CHC::analyze(SourceUnit const& _source)
// actually given and the queries were solved. // actually given and the queries were solved.
if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get())) if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
ranSolver = smtLibInterface->unhandledQueries().empty(); ranSolver = smtLibInterface->unhandledQueries().empty();
if (!ranSolver && !m_noSolverWarning) if (!ranSolver)
{
m_noSolverWarning = true;
m_errorReporter.warning( m_errorReporter.warning(
3996_error, 3996_error,
SourceLocation(), SourceLocation(),
#ifdef HAVE_Z3_DLOPEN
"CHC analysis was not possible since libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
#else
"CHC analysis was not possible. No Horn solver was available." "CHC analysis was not possible. No Horn solver was available."
" None of the installed solvers was enabled." " None of the installed solvers was enabled."
#endif
); );
}
} }
vector<string> CHC::unhandledQueries() const vector<string> CHC::unhandledQueries() const
@ -1012,6 +1008,11 @@ void CHC::resetSourceAnalysis()
#endif #endif
if (!usesZ3) if (!usesZ3)
{ {
solAssert(m_settings.solvers.smtlib2);
if (!m_interface)
m_interface = make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.timeout);
auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get()); auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
solAssert(smtlib2Interface, ""); solAssert(smtlib2Interface, "");
smtlib2Interface->reset(); smtlib2Interface->reset();

View File

@ -421,6 +421,9 @@ private:
/// CHC solver. /// CHC solver.
std::unique_ptr<smtutil::CHCSolverInterface> m_interface; std::unique_ptr<smtutil::CHCSolverInterface> m_interface;
std::map<util::h256, std::string> const& m_smtlib2Responses;
ReadCallback::Callback const& m_smtCallback;
}; };
} }

View File

@ -426,8 +426,6 @@ protected:
smt::VariableUsage m_variableUsage; smt::VariableUsage m_variableUsage;
bool m_arrayAssignmentHappened = false; bool m_arrayAssignmentHappened = false;
// True if the "No SMT solver available" warning was already created.
bool m_noSolverWarning = false;
/// Stores the instances of an Uninterpreted Function applied to arguments. /// Stores the instances of an Uninterpreted Function applied to arguments.
/// These may be direct application of UFs or Array index access. /// These may be direct application of UFs or Array index access.

View File

@ -29,7 +29,15 @@
#error "Unsupported Boost version. At least 1.65 required." #error "Unsupported Boost version. At least 1.65 required."
#endif #endif
// TODO: do this only conditionally as soon as a boost version with gcc 12 support is released.
#if defined(__GNUC__) && !defined(__clang__) && (__GNUC__ >= 12)
#pragma GCC diagnostic push
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
#endif
#include <boost/multiprecision/cpp_int.hpp> #include <boost/multiprecision/cpp_int.hpp>
#if defined(__GNUC__) && !defined(__clang__) && (__GNUC__ >= 12)
#pragma GCC diagnostic pop
#endif
#include <limits> #include <limits>

View File

@ -34,7 +34,7 @@ else
BUILD_DIR="$1" BUILD_DIR="$1"
fi fi
# solbuildpackpusher/solidity-buildpack-deps:emscripten-10 # solbuildpackpusher/solidity-buildpack-deps:emscripten-11
docker run -v "$(pwd):/root/project" -w /root/project \ docker run -v "$(pwd):/root/project" -w /root/project \
solbuildpackpusher/solidity-buildpack-deps@sha256:bd23831e0025e35a106005b4ac06cb3618f690bfa2833a5881b573c02d35d9fc\ solbuildpackpusher/solidity-buildpack-deps@sha256:0ad7c65e8c54d926ba9cb80d56246e4fc49f9284ad5188aaaa4834f46ab0c315 \
./scripts/ci/build_emscripten.sh "$BUILD_DIR" ./scripts/ci/build_emscripten.sh "$BUILD_DIR"

View File

@ -51,7 +51,17 @@ docker build "scripts/docker/${IMAGE_NAME}" --file "scripts/docker/${IMAGE_NAME}
echo "-- test_docker @ '${PWD}'" echo "-- test_docker @ '${PWD}'"
docker run --rm --volume "${PWD}:/root/project" "${IMAGE_NAME}" "/root/project/scripts/ci/${IMAGE_NAME}_test_${IMAGE_VARIANT}.sh" # NOTE: Since /root/project/ is a dir from outside the container and the owner of the files is different,
# git show in the script refuses to work. It must be marked as safe to use first.
# See https://github.blog/2022-04-12-git-security-vulnerability-announced/
docker run \
--rm \
--volume "${PWD}:/root/project" \
"${IMAGE_NAME}" \
bash -c "
git config --global --add safe.directory /root/project &&
/root/project/scripts/ci/${IMAGE_NAME}_test_${IMAGE_VARIANT}.sh
"
echo "-- push_docker" echo "-- push_docker"

View File

@ -25,7 +25,7 @@ set -ev
keyid=70D110489D66E2F6 keyid=70D110489D66E2F6
email=builds@ethereum.org email=builds@ethereum.org
packagename=z3-static packagename=z3-static
version=4.8.16 version=4.8.17
DISTRIBUTIONS="focal impish jammy" DISTRIBUTIONS="focal impish jammy"

View File

@ -33,12 +33,12 @@
# Using $(em-config CACHE)/sysroot/usr seems to work, though, and still has cmake find the # Using $(em-config CACHE)/sysroot/usr seems to work, though, and still has cmake find the
# dependencies automatically. # dependencies automatically.
FROM emscripten/emsdk:2.0.33 AS base FROM emscripten/emsdk:2.0.33 AS base
LABEL version="9" LABEL version="11"
ADD emscripten.jam /usr/src ADD emscripten.jam /usr/src
RUN set -ex; \ RUN set -ex; \
cd /usr/src; \ cd /usr/src; \
git clone https://github.com/Z3Prover/z3.git -b z3-4.8.14 --depth 1 ; \ git clone https://github.com/Z3Prover/z3.git -b z3-4.8.17 --depth 1 ; \
cd z3; \ cd z3; \
mkdir build; \ mkdir build; \
cd build; \ cd build; \

View File

@ -22,7 +22,7 @@
# (c) 2016-2021 solidity contributors. # (c) 2016-2021 solidity contributors.
#------------------------------------------------------------------------------ #------------------------------------------------------------------------------
FROM gcr.io/oss-fuzz-base/base-clang:latest as base FROM gcr.io/oss-fuzz-base/base-clang:latest as base
LABEL version="16" LABEL version="18"
ARG DEBIAN_FRONTEND=noninteractive ARG DEBIAN_FRONTEND=noninteractive
@ -61,7 +61,7 @@ RUN set -ex; \
# Z3 # Z3
RUN set -ex; \ RUN set -ex; \
git clone --depth 1 -b z3-4.8.14 https://github.com/Z3Prover/z3.git \ git clone --depth 1 -b z3-4.8.17 https://github.com/Z3Prover/z3.git \
/usr/src/z3; \ /usr/src/z3; \
cd /usr/src/z3; \ cd /usr/src/z3; \
mkdir build; \ mkdir build; \

View File

@ -22,7 +22,7 @@
# (c) 2016-2019 solidity contributors. # (c) 2016-2019 solidity contributors.
#------------------------------------------------------------------------------ #------------------------------------------------------------------------------
FROM buildpack-deps:focal AS base FROM buildpack-deps:focal AS base
LABEL version="11" LABEL version="13"
ARG DEBIAN_FRONTEND=noninteractive ARG DEBIAN_FRONTEND=noninteractive

View File

@ -22,7 +22,7 @@
# (c) 2016-2019 solidity contributors. # (c) 2016-2019 solidity contributors.
#------------------------------------------------------------------------------ #------------------------------------------------------------------------------
FROM buildpack-deps:focal AS base FROM buildpack-deps:focal AS base
LABEL version="11" LABEL version="13"
ARG DEBIAN_FRONTEND=noninteractive ARG DEBIAN_FRONTEND=noninteractive

View File

@ -231,7 +231,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
"3893", "3996", "4010", "4802", "3893", "3996", "4010", "4802",
"5272", "5622", "7128", "7400", "5272", "5622", "7128", "7400",
"7589", "7593", "7649", "7710", "7589", "7593", "7649", "7710",
"8065", "8084", "8140", "8065", "8084", "8140", "8158",
"8312", "8592", "9134", "9609", "8312", "8592", "9134", "9609",
} }

View File

@ -94,7 +94,10 @@ public:
else if (value == 21) else if (value == 21)
return "true"; return "true";
else else
{
assertThrow(false, CBORException, "Unsupported simple value (not a boolean)."); assertThrow(false, CBORException, "Unsupported simple value (not a boolean).");
return ""; // unreachable, but prevents compiler warning.
}
} }
default: default:
assertThrow(false, CBORException, "Unsupported value type."); assertThrow(false, CBORException, "Unsupported value type.");

View File

@ -1,5 +1,5 @@
{"errors":[{"component":"general","errorCode":"7649","formattedMessage":"Warning: CHC analysis was not possible since no Horn solver was enabled. {"errors":[{"component":"general","errorCode":"7649","formattedMessage":"Warning: CHC analysis was not possible since no Horn solver was found and enabled.
","message":"CHC analysis was not possible since no Horn solver was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"7710","formattedMessage":"Warning: BMC analysis was not possible since no SMT solver was found and enabled. ","message":"CHC analysis was not possible since no Horn solver was found and enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"7710","formattedMessage":"Warning: BMC analysis was not possible since no SMT solver was found and enabled.
","message":"BMC analysis was not possible since no SMT solver was found and enabled.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}} ","message":"BMC analysis was not possible since no SMT solver was found and enabled.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}

View File

@ -85,6 +85,10 @@ function gnosis_safe_test
# TODO: Remove when https://github.com/ethers-io/ethers.js/discussions/2849 is resolved. # TODO: Remove when https://github.com/ethers-io/ethers.js/discussions/2849 is resolved.
npm install ethers@5.6.1 npm install ethers@5.6.1
# Hardhat 2.9.5 introduced a bug with handling padded arguments to getStorageAt().
# TODO: Remove when https://github.com/NomicFoundation/hardhat/issues/2709 is fixed.
npm install hardhat@2.9.4
replace_version_pragmas replace_version_pragmas
[[ $BINARY_TYPE == solcjs ]] && force_solc_modules "${DIR}/solc/dist" [[ $BINARY_TYPE == solcjs ]] && force_solc_modules "${DIR}/solc/dist"

View File

@ -0,0 +1,12 @@
pragma abicoder v2;
contract C {
function f(uint[] calldata) public {}
}
// ====
// revertStrings: debug
// compileViaYul: also
// ----
// f(uint256[]): 0x20, 0 ->
// f(uint256[]): 0x20, 1 -> FAILURE, hex"08c379a0", 0x20, 0x2b, "ABI decoding: invalid calldata a", "rray stride"
// f(uint256[]): 0x20, 2 -> FAILURE, hex"08c379a0", 0x20, 0x2b, "ABI decoding: invalid calldata a", "rray stride"

View File

@ -0,0 +1,10 @@
contract C {
function f(uint[] calldata) public {}
}
// ====
// compileViaYul: also
// ----
// f(uint256[]): 0x20, 0 ->
// f(uint256[]): 0x20, 1 -> FAILURE
// f(uint256[]): 0x20, 2 -> FAILURE

View File

@ -0,0 +1,23 @@
pragma abicoder v2;
contract C {
function h(uint[][] calldata a) public {
abi.encode(a);
}
struct S { uint[] x; }
function f(S calldata a) public {
abi.encode(a);
}
}
// ====
// compileViaYul: also
// revertStrings: debug
// ----
// h(uint256[][]): 0x20, 1, 0x20, 0 ->
// h(uint256[][]): 0x20, 1, 0x20, 1 -> FAILURE, hex"08c379a0", 0x20, 0x1e, "Invalid calldata access stride"
// h(uint256[][]): 0x20, 1, 0x20, 2 -> FAILURE, hex"08c379a0", 0x20, 0x1e, "Invalid calldata access stride"
// h(uint256[][]): 0x20, 1, 0x20, 3 -> FAILURE, hex"08c379a0", 0x20, 0x1e, "Invalid calldata access stride"
// f((uint256[])): 0x20, 0x20, 0 ->
// f((uint256[])): 0x20, 0x20, 1 -> FAILURE, hex"08c379a0", 0x20, 0x1e, "Invalid calldata access stride"
// f((uint256[])): 0x20, 0x20, 2 -> FAILURE, hex"08c379a0", 0x20, 0x1e, "Invalid calldata access stride"
// f((uint256[])): 0x20, 0x20, 3 -> FAILURE, hex"08c379a0", 0x20, 0x1e, "Invalid calldata access stride"

View File

@ -0,0 +1,27 @@
pragma abicoder v2;
contract C {
function f(uint[3][] calldata a) public {
abi.encode(a);
}
function f(uint[][3] calldata a) public {
abi.encode(a);
}
function f(uint[2][2] calldata a) public {
abi.encode(a);
}
}
// ====
// compileViaYul: also
// ----
// f(uint256[3][]): 0x20, 1, 0x01 -> FAILURE
// f(uint256[3][]): 0x20, 1, 0x01, 0x02 -> FAILURE
// f(uint256[3][]): 0x20, 1, 0x01, 0x02, 0x03 ->
// f(uint256[][3]): 0x20, 0x60, 0x60, 0x60, 3, 0x01 -> FAILURE
// f(uint256[][3]): 0x20, 0x60, 0x60, 0x60, 3, 0x01, 0x02 -> FAILURE
// f(uint256[][3]): 0x20, 0x60, 0x60, 0x60, 3, 0x01, 0x02, 0x03 ->
// f(uint256[2][2]): 0x01 -> FAILURE
// f(uint256[2][2]): 0x01, 0x02 -> FAILURE
// f(uint256[2][2]): 0x01, 0x02, 0x03 -> FAILURE
// f(uint256[2][2]): 0x01, 0x02, 0x03, 0x04 ->
// f(uint256[2][2]): 0x01, 0x02, 0x03, 0x04, 0x05 ->

View File

@ -11,5 +11,5 @@ contract C {
// ---- // ----
// Warning 9302: (96-116): Return value of low-level calls not used. // Warning 9302: (96-116): Return value of low-level calls not used.
// Warning 6328: (120-156): CHC: Assertion violation might happen here. // Warning 6328: (120-156): CHC: Assertion violation might happen here.
// Warning 6328: (175-210): CHC: Assertion violation happens here. // Warning 6328: (175-210): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n i.call{value: 0}("") -- untrusted external call
// Warning 4661: (120-156): BMC: Assertion violation happens here. // Warning 4661: (120-156): BMC: Assertion violation happens here.

View File

@ -14,6 +14,8 @@ contract C {
// SMTEngine: all // SMTEngine: all
// SMTIgnoreOS: macos // SMTIgnoreOS: macos
// ---- // ----
// Warning 1218: (202-236): CHC: Error trying to invoke SMT solver.
// Warning 6328: (150-183): CHC: Assertion violation might happen here. // Warning 6328: (150-183): CHC: Assertion violation might happen here.
// Warning 6328: (202-236): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n i.f{value: 20}() -- untrusted external call // Warning 6328: (202-236): CHC: Assertion violation might happen here.
// Warning 4661: (150-183): BMC: Assertion violation happens here. // Warning 4661: (150-183): BMC: Assertion violation happens here.
// Warning 4661: (202-236): BMC: Assertion violation happens here.

View File

@ -21,4 +21,6 @@ contract C is B {
// Warning 7812: (b.sol:62-75): BMC: Assertion violation might happen here. // Warning 7812: (b.sol:62-75): BMC: Assertion violation might happen here.
// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. // Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.
// Warning 6328: (c.sol:68-81): CHC: Assertion violation might happen here. // Warning 6328: (c.sol:68-81): CHC: Assertion violation might happen here.
// Warning 3996: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
// Warning 7812: (c.sol:68-81): BMC: Assertion violation might happen here. // Warning 7812: (c.sol:68-81): BMC: Assertion violation might happen here.
// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.

View File

@ -21,5 +21,4 @@ contract C {
// SMTEngine: all // SMTEngine: all
// SMTIgnoreOS: macos // SMTIgnoreOS: macos
// ---- // ----
// Warning 6328: (280-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() // Warning 6328: (280-300): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n(!(m[0][1] >= 43) && !(m[0][1] <= 41))\n

View File

@ -1,5 +1,5 @@
contract C { contract C {
function f() view external { function f() pure external {
assembly { assembly {
let s := returndatasize() let s := returndatasize()
returndatacopy(0, 0, s) returndatacopy(0, 0, s)

View File

@ -1,5 +1,5 @@
contract C { contract C {
function f() view external { function f() pure external {
assembly { assembly {
let s := returndatasize() let s := returndatasize()
returndatacopy(0, 0, s) returndatacopy(0, 0, s)

View File

@ -1,5 +1,5 @@
contract C { contract C {
function f() public view { function f() public pure {
uint returndatasize; uint returndatasize;
returndatasize; returndatasize;
assembly { assembly {

View File

@ -1,5 +1,5 @@
contract C { contract C {
function f() public view { function f() public pure {
uint returndatasize; uint returndatasize;
returndatasize; returndatasize;
assembly { assembly {

View File

@ -1,4 +1,4 @@
contract C { function f() public view { uint returndatasize; returndatasize; assembly { pop(returndatasize()) }}} contract C { function f() public pure { uint returndatasize; returndatasize; assembly { pop(returndatasize()) }}}
// ==== // ====
// EVMVersion: =homestead // EVMVersion: =homestead
// ---- // ----

View File

@ -47,8 +47,8 @@ contract C {
codecopy(0, 1, 2) codecopy(0, 1, 2)
//pop(extcodesize(0)) //pop(extcodesize(0))
//extcodecopy(0, 1, 2, 3) //extcodecopy(0, 1, 2, 3)
//pop(returndatasize()) pop(returndatasize())
//returndatacopy(0, 1, 2) returndatacopy(0, 1, 2)
//pop(extcodehash(0)) //pop(extcodehash(0))
//pop(create(0, 1, 2)) //pop(create(0, 1, 2))
//pop(create2(0, 1, 2, 3)) //pop(create2(0, 1, 2, 3))
@ -85,6 +85,6 @@ contract C {
// ==== // ====
// EVMVersion: >=london // EVMVersion: >=london
// ---- // ----
// Warning 5740: (94-1759): Unreachable code. // Warning 5740: (94-1755): Unreachable code.
// Warning 5740: (1772-1784): Unreachable code. // Warning 5740: (1768-1780): Unreachable code.
// Warning 5740: (1827-1836): Unreachable code. // Warning 5740: (1823-1832): Unreachable code.

View File

@ -11,8 +11,6 @@ contract C {
pop(callvalue()) pop(callvalue())
pop(extcodesize(0)) pop(extcodesize(0))
extcodecopy(0, 1, 2, 3) extcodecopy(0, 1, 2, 3)
pop(returndatasize())
returndatacopy(0, 1, 2)
pop(extcodehash(0)) pop(extcodehash(0))
pop(create(0, 1, 2)) pop(create(0, 1, 2))
pop(create2(0, 1, 2, 3)) pop(create2(0, 1, 2, 3))
@ -46,7 +44,7 @@ contract C {
// ==== // ====
// EVMVersion: >=london // EVMVersion: >=london
// ---- // ----
// Warning 5740: (742-1153): Unreachable code. // Warning 5740: (672-1083): Unreachable code.
// TypeError 2527: (79-87): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (79-87): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 8961: (101-113): Function cannot be declared as pure because this expression (potentially) modifies the state. // TypeError 8961: (101-113): Function cannot be declared as pure because this expression (potentially) modifies the state.
// TypeError 2527: (130-135): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (130-135): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
@ -57,28 +55,26 @@ contract C {
// TypeError 2527: (265-276): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (265-276): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (294-308): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (294-308): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (322-345): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (322-345): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (362-378): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (362-376): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (392-415): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 8961: (394-409): Function cannot be declared as pure because this expression (potentially) modifies the state.
// TypeError 2527: (432-446): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 8961: (427-446): Function cannot be declared as pure because this expression (potentially) modifies the state.
// TypeError 8961: (464-479): Function cannot be declared as pure because this expression (potentially) modifies the state. // TypeError 8961: (464-489): Function cannot be declared as pure because this expression (potentially) modifies the state.
// TypeError 8961: (497-516): Function cannot be declared as pure because this expression (potentially) modifies the state. // TypeError 8961: (507-536): Function cannot be declared as pure because this expression (potentially) modifies the state.
// TypeError 8961: (534-559): Function cannot be declared as pure because this expression (potentially) modifies the state. // TypeError 8961: (554-584): Function cannot be declared as pure because this expression (potentially) modifies the state.
// TypeError 8961: (577-606): Function cannot be declared as pure because this expression (potentially) modifies the state. // TypeError 2527: (602-630): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 8961: (624-654): Function cannot be declared as pure because this expression (potentially) modifies the state. // TypeError 8961: (644-659): Function cannot be declared as pure because this expression (potentially) modifies the state.
// TypeError 2527: (672-700): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 8961: (672-682): Function cannot be declared as pure because this expression (potentially) modifies the state.
// TypeError 8961: (714-729): Function cannot be declared as pure because this expression (potentially) modifies the state. // TypeError 8961: (695-708): Function cannot be declared as pure because this expression (potentially) modifies the state.
// TypeError 8961: (742-752): Function cannot be declared as pure because this expression (potentially) modifies the state. // TypeError 8961: (721-737): Function cannot be declared as pure because this expression (potentially) modifies the state.
// TypeError 8961: (765-778): Function cannot be declared as pure because this expression (potentially) modifies the state. // TypeError 8961: (750-769): Function cannot be declared as pure because this expression (potentially) modifies the state.
// TypeError 8961: (791-807): Function cannot be declared as pure because this expression (potentially) modifies the state. // TypeError 8961: (782-804): Function cannot be declared as pure because this expression (potentially) modifies the state.
// TypeError 8961: (820-839): Function cannot be declared as pure because this expression (potentially) modifies the state. // TypeError 2527: (821-830): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 8961: (852-874): Function cannot be declared as pure because this expression (potentially) modifies the state. // TypeError 2527: (848-857): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (891-900): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (875-883): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (918-927): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (901-911): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (945-953): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (929-941): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (971-981): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (959-969): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (999-1011): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (987-998): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (1029-1039): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (1016-1024): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (1057-1068): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (1042-1054): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (1086-1094): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view". // TypeError 2527: (1072-1082): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (1112-1124): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".
// TypeError 2527: (1142-1152): Function declared as pure, but this expression (potentially) reads from the environment or state and thus requires "view".