From 61fd76cb27fd7b900106cc17efb24d3e895d3f13 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 3 Dec 2020 18:02:51 +0100 Subject: [PATCH 01/17] Fix documentation about revert data. --- docs/yul.rst | 5 ++--- .../reverts/revert_return_area.sol | 20 +++++++++++++++++++ 2 files changed, 22 insertions(+), 3 deletions(-) create mode 100644 test/libsolidity/semanticTests/reverts/revert_return_area.sol diff --git a/docs/yul.rst b/docs/yul.rst index 326f9cf58..5d2913a2d 100644 --- a/docs/yul.rst +++ b/docs/yul.rst @@ -896,12 +896,11 @@ the ``dup`` and ``swap`` instructions as well as ``jump`` instructions, labels a .. note:: The ``call*`` instructions use the ``out`` and ``outsize`` parameters to define an area in memory where - the return data is placed. This area is written to depending on how many bytes the called contract returns. + the return or failure data is placed. This area is written to depending on how many bytes the called contract returns. If it returns more data, only the first ``outsize`` bytes are written. You can access the rest of the data using the ``returndatacopy`` opcode. If it returns less data, then the remaining bytes are not touched at all. You need to use the ``returndatasize`` opcode to check which part of this memory area contains the return data. - The remaining bytes will retain their values as of before the call. If the call fails (it returns ``0``), - nothing is written to that area, but you can still retrieve the failure data using ``returndatacopy``. + The remaining bytes will retain their values as of before the call. In some internal dialects, there are additional functions: diff --git a/test/libsolidity/semanticTests/reverts/revert_return_area.sol b/test/libsolidity/semanticTests/reverts/revert_return_area.sol new file mode 100644 index 000000000..360e5fe9f --- /dev/null +++ b/test/libsolidity/semanticTests/reverts/revert_return_area.sol @@ -0,0 +1,20 @@ +contract C { + fallback() external { + revert("abc"); + } + + function f() public returns (uint s, uint r) { + address x = address(this); + assembly { + mstore(0, 7) + s := call(sub(0, 1), x, 0, 0, 0, 0, 32) + r := mload(0) + } + } +} + +// ==== +// compileViaYul: also +// EVMVersion: >=byzantium +// ---- +// f() -> 0x00, 0x08c379a000000000000000000000000000000000000000000000000000000000 From 96a50b52e2dcddd425bfbbc8a410edc946dccf70 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Thu, 3 Dec 2020 18:48:17 +0100 Subject: [PATCH 02/17] Add storage load/store functions to Yul dialect. --- libyul/Dialect.h | 2 + libyul/backends/evm/EVMDialect.h | 2 + libyul/optimiser/DataFlowAnalyzer.cpp | 76 ++++++++++++--------------- libyul/optimiser/DataFlowAnalyzer.h | 22 ++++---- libyul/optimiser/LoadResolver.cpp | 23 ++++---- libyul/optimiser/LoadResolver.h | 6 +-- 6 files changed, 61 insertions(+), 70 deletions(-) diff --git a/libyul/Dialect.h b/libyul/Dialect.h index 78b950d58..9b615141a 100644 --- a/libyul/Dialect.h +++ b/libyul/Dialect.h @@ -74,6 +74,8 @@ struct Dialect: boost::noncopyable virtual BuiltinFunction const* memoryStoreFunction(YulString /* _type */) const { return nullptr; } virtual BuiltinFunction const* memoryLoadFunction(YulString /* _type */) const { return nullptr; } + virtual BuiltinFunction const* storageStoreFunction(YulString /* _type */) const { return nullptr; } + virtual BuiltinFunction const* storageLoadFunction(YulString /* _type */) const { return nullptr; } /// Check whether the given type is legal for the given literal value. /// Should only be called if the type exists in the dialect at all. diff --git a/libyul/backends/evm/EVMDialect.h b/libyul/backends/evm/EVMDialect.h index a890a0ce2..7ffc09418 100644 --- a/libyul/backends/evm/EVMDialect.h +++ b/libyul/backends/evm/EVMDialect.h @@ -75,6 +75,8 @@ struct EVMDialect: public Dialect BuiltinFunctionForEVM const* booleanNegationFunction() const override { return builtin("iszero"_yulstring); } BuiltinFunctionForEVM const* memoryStoreFunction(YulString /*_type*/) const override { return builtin("mstore"_yulstring); } BuiltinFunctionForEVM const* memoryLoadFunction(YulString /*_type*/) const override { return builtin("mload"_yulstring); } + BuiltinFunctionForEVM const* storageStoreFunction(YulString /*_type*/) const override { return builtin("sstore"_yulstring); } + BuiltinFunctionForEVM const* storageLoadFunction(YulString /*_type*/) const override { return builtin("sload"_yulstring); } static EVMDialect const& strictAssemblyForEVM(langutil::EVMVersion _version); static EVMDialect const& strictAssemblyForEVMObjects(langutil::EVMVersion _version); diff --git a/libyul/optimiser/DataFlowAnalyzer.cpp b/libyul/optimiser/DataFlowAnalyzer.cpp index cd1bb7da3..b845d2722 100644 --- a/libyul/optimiser/DataFlowAnalyzer.cpp +++ b/libyul/optimiser/DataFlowAnalyzer.cpp @@ -25,8 +25,8 @@ #include #include #include +#include #include -#include #include @@ -39,9 +39,27 @@ using namespace solidity; using namespace solidity::util; using namespace solidity::yul; +DataFlowAnalyzer::DataFlowAnalyzer( + Dialect const& _dialect, + map _functionSideEffects +): +m_dialect(_dialect), +m_functionSideEffects(std::move(_functionSideEffects)), +m_knowledgeBase(_dialect, m_value) +{ + if (auto const* builtin = _dialect.memoryStoreFunction(YulString{})) + m_storeFunctionName[static_cast(StoreLoadLocation::Memory)] = builtin->name; + if (auto const* builtin = _dialect.memoryLoadFunction(YulString{})) + m_loadFunctionName[static_cast(StoreLoadLocation::Memory)] = builtin->name; + if (auto const* builtin = _dialect.storageStoreFunction(YulString{})) + m_storeFunctionName[static_cast(StoreLoadLocation::Storage)] = builtin->name; + if (auto const* builtin = _dialect.storageLoadFunction(YulString{})) + m_loadFunctionName[static_cast(StoreLoadLocation::Storage)] = builtin->name; +} + void DataFlowAnalyzer::operator()(ExpressionStatement& _statement) { - if (auto vars = isSimpleStore(evmasm::Instruction::SSTORE, _statement)) + if (auto vars = isSimpleStore(StoreLoadLocation::Storage, _statement)) { ASTModifier::operator()(_statement); set keysToErase; @@ -55,7 +73,7 @@ void DataFlowAnalyzer::operator()(ExpressionStatement& _statement) m_storage.eraseKey(key); m_storage.set(vars->first, vars->second); } - else if (auto vars = isSimpleStore(evmasm::Instruction::MSTORE, _statement)) + else if (auto vars = isSimpleStore(StoreLoadLocation::Memory, _statement)) { ASTModifier::operator()(_statement); set keysToErase; @@ -265,9 +283,9 @@ void DataFlowAnalyzer::handleAssignment(set const& _variables, Expres // This might erase additional knowledge about the slot. // On the other hand, if we knew the value in the slot // already, then the sload() / mload() would have been replaced by a variable anyway. - if (auto key = isSimpleLoad(evmasm::Instruction::MLOAD, *_value)) + if (auto key = isSimpleLoad(StoreLoadLocation::Memory, *_value)) m_memory.set(*key, variable); - else if (auto key = isSimpleLoad(evmasm::Instruction::SLOAD, *_value)) + else if (auto key = isSimpleLoad(StoreLoadLocation::Storage, *_value)) m_storage.set(*key, variable); } } @@ -391,53 +409,27 @@ bool DataFlowAnalyzer::inScope(YulString _variableName) const } std::optional> DataFlowAnalyzer::isSimpleStore( - evmasm::Instruction _store, + StoreLoadLocation _location, ExpressionStatement const& _statement ) const { - yulAssert( - _store == evmasm::Instruction::MSTORE || - _store == evmasm::Instruction::SSTORE, - "" - ); - if (holds_alternative(_statement.expression)) - { - FunctionCall const& funCall = std::get(_statement.expression); - if (EVMDialect const* dialect = dynamic_cast(&m_dialect)) - if (auto const* builtin = dialect->builtin(funCall.functionName.name)) - if (builtin->instruction == _store) - if ( - holds_alternative(funCall.arguments.at(0)) && - holds_alternative(funCall.arguments.at(1)) - ) - { - YulString key = std::get(funCall.arguments.at(0)).name; - YulString value = std::get(funCall.arguments.at(1)).name; - return make_pair(key, value); - } - } + if (FunctionCall const* funCall = get_if(&_statement.expression)) + if (funCall->functionName.name == m_storeFunctionName[static_cast(_location)]) + if (Identifier const* key = std::get_if(&funCall->arguments.front())) + if (Identifier const* value = std::get_if(&funCall->arguments.back())) + return make_pair(key->name, value->name); return {}; } std::optional DataFlowAnalyzer::isSimpleLoad( - evmasm::Instruction _load, + StoreLoadLocation _location, Expression const& _expression ) const { - yulAssert( - _load == evmasm::Instruction::MLOAD || - _load == evmasm::Instruction::SLOAD, - "" - ); - if (holds_alternative(_expression)) - { - FunctionCall const& funCall = std::get(_expression); - if (EVMDialect const* dialect = dynamic_cast(&m_dialect)) - if (auto const* builtin = dialect->builtin(funCall.functionName.name)) - if (builtin->instruction == _load) - if (holds_alternative(funCall.arguments.at(0))) - return std::get(funCall.arguments.at(0)).name; - } + if (FunctionCall const* funCall = get_if(&_expression)) + if (funCall->functionName.name == m_loadFunctionName[static_cast(_location)]) + if (Identifier const* key = std::get_if(&funCall->arguments.front())) + return key->name; return {}; } diff --git a/libyul/optimiser/DataFlowAnalyzer.h b/libyul/optimiser/DataFlowAnalyzer.h index 4da6ee1a7..7a9b36a24 100644 --- a/libyul/optimiser/DataFlowAnalyzer.h +++ b/libyul/optimiser/DataFlowAnalyzer.h @@ -29,9 +29,6 @@ #include // Needed for m_zero below. #include -// TODO avoid -#include - #include #include @@ -89,11 +86,7 @@ public: explicit DataFlowAnalyzer( Dialect const& _dialect, std::map _functionSideEffects = {} - ): - m_dialect(_dialect), - m_functionSideEffects(std::move(_functionSideEffects)), - m_knowledgeBase(_dialect, m_value) - {} + ); using ASTModifier::operator(); void operator()(ExpressionStatement& _statement) override; @@ -143,17 +136,23 @@ protected: /// Returns true iff the variable is in scope. bool inScope(YulString _variableName) const; + enum class StoreLoadLocation { + Memory = 0, + Storage = 1, + Last = Storage + }; + /// Checks if the statement is sstore(a, b) / mstore(a, b) /// where a and b are variables and returns these variables in that case. std::optional> isSimpleStore( - evmasm::Instruction _store, + StoreLoadLocation _location, ExpressionStatement const& _statement ) const; /// Checks if the expression is sload(a) / mload(a) /// where a is a variable and returns the variable in that case. std::optional isSimpleLoad( - evmasm::Instruction _load, + StoreLoadLocation _location, Expression const& _expression ) const; @@ -173,6 +172,9 @@ protected: KnowledgeBase m_knowledgeBase; + YulString m_storeFunctionName[static_cast(StoreLoadLocation::Last) + 1]; + YulString m_loadFunctionName[static_cast(StoreLoadLocation::Last) + 1]; + /// Current nesting depth of loops. size_t m_loopDepth{0}; diff --git a/libyul/optimiser/LoadResolver.cpp b/libyul/optimiser/LoadResolver.cpp index cc69b630a..21992e547 100644 --- a/libyul/optimiser/LoadResolver.cpp +++ b/libyul/optimiser/LoadResolver.cpp @@ -46,21 +46,18 @@ void LoadResolver::visit(Expression& _e) { DataFlowAnalyzer::visit(_e); - if (!dynamic_cast(&m_dialect)) - return; - - if (holds_alternative(_e)) - { - FunctionCall const& funCall = std::get(_e); - if (auto const* builtin = dynamic_cast(m_dialect).builtin(funCall.functionName.name)) - if (builtin->instruction) - tryResolve(_e, *builtin->instruction, funCall.arguments); - } + if (FunctionCall const* funCall = std::get_if(&_e)) + for (auto location: { StoreLoadLocation::Memory, StoreLoadLocation::Storage }) + if (funCall->functionName.name == m_loadFunctionName[static_cast(location)]) + { + tryResolve(_e, location, funCall->arguments); + break; + } } void LoadResolver::tryResolve( Expression& _e, - evmasm::Instruction _instruction, + StoreLoadLocation _location, vector const& _arguments ) { @@ -69,13 +66,13 @@ void LoadResolver::tryResolve( YulString key = std::get(_arguments.at(0)).name; if ( - _instruction == evmasm::Instruction::SLOAD && + _location == StoreLoadLocation::Storage && m_storage.values.count(key) ) _e = Identifier{locationOf(_e), m_storage.values[key]}; else if ( m_optimizeMLoad && - _instruction == evmasm::Instruction::MLOAD && + _location == StoreLoadLocation::Memory && m_memory.values.count(key) ) _e = Identifier{locationOf(_e), m_memory.values[key]}; diff --git a/libyul/optimiser/LoadResolver.h b/libyul/optimiser/LoadResolver.h index 00579e95f..a376ab059 100644 --- a/libyul/optimiser/LoadResolver.h +++ b/libyul/optimiser/LoadResolver.h @@ -24,14 +24,10 @@ #include #include -#include namespace solidity::yul { -struct EVMDialect; -struct BuiltinFunctionForEVM; - /** * Optimisation stage that replaces expressions of type ``sload(x)`` and ``mload(x)`` by the value * currently stored in storage resp. memory, if known. @@ -63,7 +59,7 @@ protected: void tryResolve( Expression& _e, - evmasm::Instruction _instruction, + StoreLoadLocation _location, std::vector const& _arguments ); From 4210e09d9a433d767ee039a8f99c207043d43211 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 3 Dec 2020 19:16:04 +0100 Subject: [PATCH 03/17] Do not request proof for old z3 --- Changelog.md | 1 + libsmtutil/Z3CHCInterface.cpp | 22 ++++++++++++++++------ libsmtutil/Z3CHCInterface.h | 3 +++ 3 files changed, 20 insertions(+), 6 deletions(-) diff --git a/Changelog.md b/Changelog.md index 32d3db1d4..b4a833463 100644 --- a/Changelog.md +++ b/Changelog.md @@ -15,6 +15,7 @@ Compiler Features: Bugfixes: * Code generator: Do not pad empty string literals with a single 32-byte zero field in the ABI coder v1. * SMTChecker: Fix internal compiler error when doing bitwise compound assignment with string literals. + * SMTChecker: Fix internal error when trying to generate counterexamples with old z3. * Yul Optimizer: Fix a bug in NameSimplifier where a new name created by NameSimplifier could also be created by NameDispenser. * Yul Optimizer: Removed NameSimplifier from optimization steps available to users. diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp index 66ba55801..1196b27ff 100644 --- a/libsmtutil/Z3CHCInterface.cpp +++ b/libsmtutil/Z3CHCInterface.cpp @@ -33,6 +33,13 @@ Z3CHCInterface::Z3CHCInterface(optional _queryTimeout): m_context(m_z3Interface->context()), m_solver(*m_context) { + Z3_get_version( + &get<0>(m_version), + &get<1>(m_version), + &get<2>(m_version), + &get<3>(m_version) + ); + // These need to be set globally. z3::set_param("rewriter.pull_cheap_ite", true); @@ -73,7 +80,6 @@ void Z3CHCInterface::addRule(Expression const& _expr, string const& _name) pair Z3CHCInterface::query(Expression const& _expr) { CheckResult result; - CHCSolverInterface::CexGraph cex; try { z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr); @@ -82,9 +88,14 @@ pair Z3CHCInterface::query(Expression case z3::check_result::sat: { result = CheckResult::SATISFIABLE; - auto proof = m_solver.get_answer(); - auto cex = cexGraph(proof); - return {result, cex}; + // z3 version 4.8.8 modified Spacer to also return + // proofs containing nonlinear clauses. + if (m_version >= tuple(4, 8, 8, 0)) + { + auto proof = m_solver.get_answer(); + return {result, cexGraph(proof)}; + } + break; } case z3::check_result::unsat: { @@ -112,10 +123,9 @@ pair Z3CHCInterface::query(Expression result = CheckResult::UNKNOWN; else result = CheckResult::ERROR; - cex = {}; } - return {result, cex}; + return {result, {}}; } void Z3CHCInterface::setSpacerOptions(bool _preProcessing) diff --git a/libsmtutil/Z3CHCInterface.h b/libsmtutil/Z3CHCInterface.h index a0d678536..a0e4bfa67 100644 --- a/libsmtutil/Z3CHCInterface.h +++ b/libsmtutil/Z3CHCInterface.h @@ -25,6 +25,7 @@ #include #include +#include #include namespace solidity::smtutil @@ -64,6 +65,8 @@ private: z3::context* m_context; // Horn solver. z3::fixedpoint m_solver; + + std::tuple m_version = std::tuple(0, 0, 0, 0); }; } From 0a292188482c6530adf60be06adcfb6e26a58656 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= Date: Tue, 1 Dec 2020 20:31:30 +0100 Subject: [PATCH 04/17] external test scripts: Quote variables properly --- scripts/common.sh | 10 +++++----- test/externalTests.sh | 8 ++++---- test/externalTests/solc-js/solc-js.sh | 6 +++--- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/scripts/common.sh b/scripts/common.sh index fbb730241..797510d33 100644 --- a/scripts/common.sh +++ b/scripts/common.sh @@ -37,21 +37,21 @@ safe_kill() local n=1 # only proceed if $PID does exist - kill -0 $PID 2>/dev/null || return + kill -0 "$PID" 2>/dev/null || return echo "Sending SIGTERM to ${NAME} (${PID}) ..." - kill $PID + kill "$PID" # wait until process terminated gracefully - while kill -0 $PID 2>/dev/null && [[ $n -le 4 ]]; do + while kill -0 "$PID" 2>/dev/null && [[ $n -le 4 ]]; do echo "Waiting ($n) ..." sleep 1 n=$[n + 1] done # process still alive? then hard-kill - if kill -0 $PID 2>/dev/null; then + if kill -0 "$PID" 2>/dev/null; then echo "Sending SIGKILL to ${NAME} (${PID}) ..." - kill -9 $PID + kill -9 "$PID" fi } diff --git a/test/externalTests.sh b/test/externalTests.sh index 7bf3eb76b..e53f9925a 100755 --- a/test/externalTests.sh +++ b/test/externalTests.sh @@ -42,10 +42,10 @@ source test/externalTests/common.sh printTask "Running external tests..." -$REPO_ROOT/externalTests/zeppelin.sh "$SOLJSON" -$REPO_ROOT/externalTests/gnosis.sh "$SOLJSON" -$REPO_ROOT/externalTests/colony.sh "$SOLJSON" -$REPO_ROOT/externalTests/ens.sh "$SOLJSON" +"$REPO_ROOT/externalTests/zeppelin.sh" "$SOLJSON" +"$REPO_ROOT/externalTests/gnosis.sh" "$SOLJSON" +"$REPO_ROOT/externalTests/colony.sh" "$SOLJSON" +"$REPO_ROOT/externalTests/ens.sh" "$SOLJSON" # Disabled temporarily as it needs to be updated to latest Truffle first. #test_truffle Gnosis https://github.com/axic/pm-contracts.git solidity-050 diff --git a/test/externalTests/solc-js/solc-js.sh b/test/externalTests/solc-js/solc-js.sh index db01a2ae7..fd59c4398 100755 --- a/test/externalTests/solc-js/solc-js.sh +++ b/test/externalTests/solc-js/solc-js.sh @@ -41,10 +41,10 @@ function solcjs_test echo "require('./determinism.js');" >> test/index.js printLog "Copying determinism.js..." - cp -f $SOLCJS_INPUT_DIR/determinism.js test/ + cp -f "$SOLCJS_INPUT_DIR/determinism.js" test/ printLog "Copying contracts..." - cp -Rf $SOLCJS_INPUT_DIR/DAO test/ + cp -Rf "$SOLCJS_INPUT_DIR/DAO" test/ printLog "Copying SMTChecker tests..." cp -Rf "$TEST_DIR"/test/libsolidity/smtCheckerTests test/ @@ -52,7 +52,7 @@ function solcjs_test # Update version (needed for some tests) echo "Updating package.json to version $VERSION" - npm version --allow-same-version --no-git-tag-version $VERSION + npm version --allow-same-version --no-git-tag-version "$VERSION" run_test compile_fn test_fn } From 3590311e6fda867a2a7049c39bb9060610ee56ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= Date: Tue, 1 Dec 2020 20:32:12 +0100 Subject: [PATCH 05/17] external test scripts: Replace the old dollar expressions with newer variants --- scripts/common.sh | 2 +- test/externalTests/common.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/common.sh b/scripts/common.sh index 797510d33..f39768166 100644 --- a/scripts/common.sh +++ b/scripts/common.sh @@ -46,7 +46,7 @@ safe_kill() while kill -0 "$PID" 2>/dev/null && [[ $n -le 4 ]]; do echo "Waiting ($n) ..." sleep 1 - n=$[n + 1] + n=$((n + 1)) done # process still alive? then hard-kill diff --git a/test/externalTests/common.sh b/test/externalTests/common.sh index d56912a85..14eeb9810 100644 --- a/test/externalTests/common.sh +++ b/test/externalTests/common.sh @@ -80,7 +80,7 @@ function download_project printLog "Cloning $branch of $repo..." git clone --depth 1 "$repo" -b "$branch" "$dir/ext" cd ext - echo "Current commit hash: `git rev-parse HEAD`" + echo "Current commit hash: $(git rev-parse HEAD)" } function force_truffle_version From a6921bc39b3e0759c01fc1b8faf3d29b1ea9e04d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= Date: Tue, 1 Dec 2020 20:32:25 +0100 Subject: [PATCH 06/17] external test scripts: Add missing bash shebangs --- scripts/common.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/common.sh b/scripts/common.sh index f39768166..3518a21aa 100644 --- a/scripts/common.sh +++ b/scripts/common.sh @@ -1,3 +1,4 @@ +#!/usr/bin/env bash # ------------------------------------------------------------------------------ # vim:ts=4:et # This file is part of solidity. From fcf053822427263381e95dea7386b6146b4b64f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= Date: Tue, 1 Dec 2020 20:38:15 +0100 Subject: [PATCH 07/17] external test scripts: Replace global $FORCE_ABIv2 variable with a parameter --- test/externalTests/colony.sh | 3 +-- test/externalTests/common.sh | 5 ++++- test/externalTests/ens.sh | 2 +- test/externalTests/gnosis.sh | 2 +- test/externalTests/zeppelin.sh | 2 +- 5 files changed, 8 insertions(+), 6 deletions(-) diff --git a/test/externalTests/colony.sh b/test/externalTests/colony.sh index 6a246b2b9..91a82d8bb 100755 --- a/test/externalTests/colony.sh +++ b/test/externalTests/colony.sh @@ -31,7 +31,6 @@ function test_fn { yarn run test:contracts; } function colony_test { OPTIMIZER_LEVEL=3 - FORCE_ABIv2=false CONFIG="truffle.js" truffle_setup https://github.com/solidity-external-tests/colonyNetwork.git develop_070 @@ -42,7 +41,7 @@ function colony_test git clone https://github.com/solidity-external-tests/dappsys-monolithic.git -b master_060 dappsys cd .. - truffle_run_test compile_fn test_fn + truffle_run_test compile_fn test_fn "NO-FORCE-ABI-V2" } external_test ColonyNetworks colony_test diff --git a/test/externalTests/common.sh b/test/externalTests/common.sh index 14eeb9810..6e4924762 100644 --- a/test/externalTests/common.sh +++ b/test/externalTests/common.sh @@ -234,6 +234,9 @@ function truffle_run_test { local compile_fn="$1" local test_fn="$2" + local force_abi_v2_flag="$3" + + test "$force_abi_v2_flag" = "FORCE-ABI-V2" || test "$force_abi_v2_flag" = "NO-FORCE-ABI-V2" replace_version_pragmas force_solc "$CONFIG" "$DIR" "$SOLJSON" @@ -258,7 +261,7 @@ function truffle_run_test clean force_solc_settings "$CONFIG" "$optimize" "istanbul" # Force abi coder v2 in the last step. Has to be the last because code is modified. - if [ "$FORCE_ABIv2" = true ]; then + if [ "$force_abi_v2_flag" = "FORCE-ABI-V2" ]; then [[ "$optimize" =~ yul ]] && force_abi_v2 fi diff --git a/test/externalTests/ens.sh b/test/externalTests/ens.sh index 52cccdb56..d67f1fe77 100755 --- a/test/externalTests/ens.sh +++ b/test/externalTests/ens.sh @@ -42,7 +42,7 @@ function ens_test run_install install_fn - truffle_run_test compile_fn test_fn + truffle_run_test compile_fn test_fn "NO-FORCE-ABI-V2" } external_test Ens ens_test diff --git a/test/externalTests/gnosis.sh b/test/externalTests/gnosis.sh index 8a5ccd0c7..83a8cd499 100755 --- a/test/externalTests/gnosis.sh +++ b/test/externalTests/gnosis.sh @@ -43,7 +43,7 @@ function gnosis_safe_test run_install install_fn replace_libsolc_call - truffle_run_test compile_fn test_fn + truffle_run_test compile_fn test_fn "NO-FORCE-ABI-V2" } external_test Gnosis-Safe gnosis_safe_test diff --git a/test/externalTests/zeppelin.sh b/test/externalTests/zeppelin.sh index 51051f334..35e47faba 100755 --- a/test/externalTests/zeppelin.sh +++ b/test/externalTests/zeppelin.sh @@ -36,7 +36,7 @@ function zeppelin_test truffle_setup https://github.com/solidity-external-tests/openzeppelin-contracts.git upgrade-0.7.0 run_install install_fn - truffle_run_test compile_fn test_fn + truffle_run_test compile_fn test_fn "NO-FORCE-ABI-V2" } external_test Zeppelin zeppelin_test From 8080be94450b55a01357401d83c950ac959d5372 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= Date: Tue, 1 Dec 2020 20:44:21 +0100 Subject: [PATCH 08/17] external test scripts: Replace global $SOLJSON variable with a parameter --- test/externalTests/colony.sh | 6 +++--- test/externalTests/common.sh | 26 +++++++++++++++----------- test/externalTests/ens.sh | 6 +++--- test/externalTests/gnosis.sh | 6 +++--- test/externalTests/solc-js/solc-js.sh | 2 +- test/externalTests/zeppelin.sh | 6 +++--- 6 files changed, 28 insertions(+), 24 deletions(-) diff --git a/test/externalTests/colony.sh b/test/externalTests/colony.sh index 91a82d8bb..349cabf2a 100755 --- a/test/externalTests/colony.sh +++ b/test/externalTests/colony.sh @@ -33,15 +33,15 @@ function colony_test OPTIMIZER_LEVEL=3 CONFIG="truffle.js" - truffle_setup https://github.com/solidity-external-tests/colonyNetwork.git develop_070 - run_install install_fn + truffle_setup "$SOLJSON" https://github.com/solidity-external-tests/colonyNetwork.git develop_070 + run_install "$SOLJSON" install_fn cd lib rm -Rf dappsys git clone https://github.com/solidity-external-tests/dappsys-monolithic.git -b master_060 dappsys cd .. - truffle_run_test compile_fn test_fn "NO-FORCE-ABI-V2" + truffle_run_test "$SOLJSON" compile_fn test_fn "NO-FORCE-ABI-V2" } external_test ColonyNetworks colony_test diff --git a/test/externalTests/common.sh b/test/externalTests/common.sh index 6e4924762..ad36a5ff4 100644 --- a/test/externalTests/common.sh +++ b/test/externalTests/common.sh @@ -40,9 +40,10 @@ function verify_version_input function setup { - local branch="$1" + local soljson="$1" + local branch="$2" - setup_solcjs "$DIR" "$SOLJSON" "$branch" "solc" + setup_solcjs "$DIR" "$soljson" "$branch" "solc" cd solc } @@ -92,10 +93,11 @@ function force_truffle_version function truffle_setup { - local repo="$1" - local branch="$2" + local soljson="$1" + local repo="$2" + local branch="$3" - setup_solcjs "$DIR" "$SOLJSON" "master" "solc" + setup_solcjs "$DIR" "$soljson" "master" "solc" download_project "$repo" "$branch" "$DIR" } @@ -207,11 +209,12 @@ function clean function run_install { - local init_fn="$1" + local soljson="$1" + local init_fn="$2" printLog "Running install function..." replace_version_pragmas - force_solc "$CONFIG" "$DIR" "$SOLJSON" + force_solc "$CONFIG" "$DIR" "$soljson" $init_fn } @@ -232,14 +235,15 @@ function run_test function truffle_run_test { - local compile_fn="$1" - local test_fn="$2" - local force_abi_v2_flag="$3" + local soljson="$1" + local compile_fn="$2" + local test_fn="$3" + local force_abi_v2_flag="$4" test "$force_abi_v2_flag" = "FORCE-ABI-V2" || test "$force_abi_v2_flag" = "NO-FORCE-ABI-V2" replace_version_pragmas - force_solc "$CONFIG" "$DIR" "$SOLJSON" + force_solc "$CONFIG" "$DIR" "$soljson" printLog "Checking optimizer level..." if [ -z "$OPTIMIZER_LEVEL" ]; then diff --git a/test/externalTests/ens.sh b/test/externalTests/ens.sh index d67f1fe77..40432198f 100755 --- a/test/externalTests/ens.sh +++ b/test/externalTests/ens.sh @@ -35,14 +35,14 @@ function ens_test export OPTIMIZER_LEVEL=1 export CONFIG="truffle-config.js" - truffle_setup https://github.com/solidity-external-tests/ens.git upgrade-0.8.0 + truffle_setup "$SOLJSON" https://github.com/solidity-external-tests/ens.git upgrade-0.8.0 # Use latest Truffle. Older versions crash on the output from 0.8.0. force_truffle_version ^5.1.55 - run_install install_fn + run_install "$SOLJSON" install_fn - truffle_run_test compile_fn test_fn "NO-FORCE-ABI-V2" + truffle_run_test "$SOLJSON" compile_fn test_fn "NO-FORCE-ABI-V2" } external_test Ens ens_test diff --git a/test/externalTests/gnosis.sh b/test/externalTests/gnosis.sh index 83a8cd499..73870f8db 100755 --- a/test/externalTests/gnosis.sh +++ b/test/externalTests/gnosis.sh @@ -33,17 +33,17 @@ function gnosis_safe_test OPTIMIZER_LEVEL=1 CONFIG="truffle.js" - truffle_setup https://github.com/solidity-external-tests/safe-contracts.git development_070 + truffle_setup "$SOLJSON" https://github.com/solidity-external-tests/safe-contracts.git development_070 force_truffle_version ^5.0.42 sed -i 's|github:gnosis/mock-contract#sol_0_5_0|github:solidity-external-tests/mock-contract#master_070|g' package.json rm -f package-lock.json rm -rf node_modules/ - run_install install_fn + run_install "$SOLJSON" install_fn replace_libsolc_call - truffle_run_test compile_fn test_fn "NO-FORCE-ABI-V2" + truffle_run_test "$SOLJSON" compile_fn test_fn "NO-FORCE-ABI-V2" } external_test Gnosis-Safe gnosis_safe_test diff --git a/test/externalTests/solc-js/solc-js.sh b/test/externalTests/solc-js/solc-js.sh index fd59c4398..9cc753959 100755 --- a/test/externalTests/solc-js/solc-js.sh +++ b/test/externalTests/solc-js/solc-js.sh @@ -35,7 +35,7 @@ function solcjs_test SOLCJS_INPUT_DIR="$TEST_DIR"/test/externalTests/solc-js # set up solc-js on the branch specified - setup master + setup "$SOLJSON" master printLog "Updating index.js file..." echo "require('./determinism.js');" >> test/index.js diff --git a/test/externalTests/zeppelin.sh b/test/externalTests/zeppelin.sh index 35e47faba..e71e974d6 100755 --- a/test/externalTests/zeppelin.sh +++ b/test/externalTests/zeppelin.sh @@ -33,10 +33,10 @@ function zeppelin_test OPTIMIZER_LEVEL=1 CONFIG="truffle-config.js" - truffle_setup https://github.com/solidity-external-tests/openzeppelin-contracts.git upgrade-0.7.0 - run_install install_fn + truffle_setup "$SOLJSON" https://github.com/solidity-external-tests/openzeppelin-contracts.git upgrade-0.7.0 + run_install "$SOLJSON" install_fn - truffle_run_test compile_fn test_fn "NO-FORCE-ABI-V2" + truffle_run_test "$SOLJSON" compile_fn test_fn "NO-FORCE-ABI-V2" } external_test Zeppelin zeppelin_test From 55ccfc32f547cf33838dcc86358c680116c0411a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= Date: Tue, 1 Dec 2020 20:33:01 +0100 Subject: [PATCH 09/17] Remove external test scripts from shellcheck ignores --- scripts/chk_shellscripts/ignore.txt | 7 ------- test/externalTests/ens.sh | 2 -- 2 files changed, 9 deletions(-) diff --git a/scripts/chk_shellscripts/ignore.txt b/scripts/chk_shellscripts/ignore.txt index 220ed9f57..188efb0ab 100644 --- a/scripts/chk_shellscripts/ignore.txt +++ b/scripts/chk_shellscripts/ignore.txt @@ -1,12 +1,5 @@ ./test/docsCodeStyle.sh ./test/cmdlineTests.sh -./test/externalTests.sh -./test/externalTests/common.sh -./test/externalTests/gnosis.sh -./test/externalTests/zeppelin.sh -./test/externalTests/colony.sh -./test/externalTests/solc-js/solc-js.sh -./scripts/common.sh ./scripts/isoltest.sh ./scripts/get_version.sh ./scripts/soltest.sh diff --git a/test/externalTests/ens.sh b/test/externalTests/ens.sh index 40432198f..99f4b8971 100755 --- a/test/externalTests/ens.sh +++ b/test/externalTests/ens.sh @@ -18,9 +18,7 @@ # # (c) 2019 solidity contributors. #------------------------------------------------------------------------------ -# shellcheck disable=SC1091 source scripts/common.sh -# shellcheck disable=SC1091 source test/externalTests/common.sh verify_input "$1" From 7490ffbe13985f0cb55b0d8d052944b3cfa92b1a Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 9 Nov 2020 15:37:08 +0000 Subject: [PATCH 10/17] Use nonlinear clauses instead of inlining for base constructors --- libsolidity/formal/BMC.cpp | 3 + libsolidity/formal/CHC.cpp | 274 ++++++++++-------- libsolidity/formal/CHC.h | 31 +- libsolidity/formal/Predicate.cpp | 8 +- libsolidity/formal/Predicate.h | 1 - libsolidity/formal/PredicateInstance.cpp | 79 ++++- libsolidity/formal/PredicateInstance.h | 22 +- libsolidity/formal/PredicateSort.cpp | 12 +- libsolidity/formal/PredicateSort.h | 19 +- libsolidity/formal/SMTEncoder.cpp | 34 ++- libsolidity/formal/SMTEncoder.h | 3 + .../functions/constructor_hierarchy_3.sol | 2 +- .../functions/constructor_hierarchy_4.sol | 2 +- .../constructor_hierarchy_diamond_3.sol | 2 +- .../getters/nested_arrays_mappings_3.sol | 4 +- .../getters/nested_arrays_mappings_6.sol | 4 +- ...chy_base_calls_inheritance_specifier_1.sol | 36 +++ ...chy_base_calls_inheritance_specifier_2.sol | 38 +++ ...erarchy_base_calls_with_side_effects_1.sol | 34 +++ ...erarchy_base_calls_with_side_effects_2.sol | 33 +++ ...erarchy_base_calls_with_side_effects_3.sol | 35 +++ ...erarchy_base_calls_with_side_effects_4.sol | 35 +++ ...erarchy_base_calls_with_side_effects_5.sol | 39 +++ ...erarchy_base_calls_with_side_effects_6.sol | 38 +++ ...erarchy_base_calls_with_side_effects_7.sol | 35 +++ ...erarchy_base_calls_with_side_effects_8.sol | 22 ++ ...erarchy_base_calls_with_side_effects_9.sol | 24 ++ ...onstructor_state_variable_init_asserts.sol | 39 +++ ...ctor_state_variable_init_chain_run_all.sol | 2 +- ...or_state_variable_init_chain_run_all_2.sol | 2 +- ...tructor_state_variable_init_chain_tree.sol | 43 +++ ...tor_state_variable_init_diamond_middle.sol | 13 +- .../constructor_uses_function_base.sol | 19 ++ .../types/array_aliasing_memory_3.sol | 4 +- ...uct_array_struct_array_memory_unsafe_2.sol | 6 +- 35 files changed, 811 insertions(+), 186 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_2.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_1.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_2.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_3.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_4.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_5.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_6.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_7.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_8.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_9.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_asserts.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_tree.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 544db45da..502db5836 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -149,6 +149,9 @@ bool BMC::visit(FunctionDefinition const& _function) resetStateVariables(); } + if (_function.isConstructor()) + inlineConstructorHierarchy(dynamic_cast(*_function.scope())); + /// Already visits the children. SMTEncoder::visit(_function); diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index be3413770..42d424bc3 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -112,20 +112,11 @@ vector CHC::unhandledQueries() const bool CHC::visit(ContractDefinition const& _contract) { resetContractAnalysis(); - initContract(_contract); - - m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract); - clearIndices(&_contract); + m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract); solAssert(m_currentContract, ""); - m_constructorSummaryPredicate = createSymbolicBlock( - constructorSort(*m_currentContract, state()), - "summary_constructor_" + contractSuffix(_contract), - PredicateType::ConstructorSummary, - &_contract - ); SMTEncoder::visit(_contract); return false; @@ -133,27 +124,64 @@ bool CHC::visit(ContractDefinition const& _contract) void CHC::endVisit(ContractDefinition const& _contract) { - auto implicitConstructorPredicate = createSymbolicBlock( - implicitConstructorSort(state()), - "implicit_constructor_" + contractSuffix(_contract), - PredicateType::ImplicitConstructor, - &_contract - ); - addRule( - (*implicitConstructorPredicate)({0, state().thisAddress(), state().crypto(), state().tx(), state().state()}), - implicitConstructorPredicate->functor().name - ); - setCurrentBlock(*implicitConstructorPredicate); - if (auto constructor = _contract.constructor()) constructor->accept(*this); - else - inlineConstructorHierarchy(_contract); + + defineContractInitializer(_contract); + + auto const& entry = *createConstructorBlock(_contract, "implicit_constructor_entry"); + + // In case constructors use uninitialized state variables, + // they need to be zeroed. + // This is not part of `initialConstraints` because it's only true here, + // at the beginning of the deployment routine. + smtutil::Expression zeroes(true); + for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract)) + zeroes = zeroes && currentValue(*var) == smt::zeroValue(var->type()); + addRule(smtutil::Expression::implies(initialConstraints(_contract) && zeroes, predicate(entry)), entry.functor().name); + setCurrentBlock(entry); + + solAssert(!m_errorDest, ""); + m_errorDest = m_constructorSummaries.at(&_contract); + // We need to evaluate the base constructor calls (arguments) from derived -> base + auto baseArgs = baseArguments(_contract); + for (auto base: _contract.annotation().linearizedBaseContracts) + { + if (base != &_contract) + { + m_callGraph[&_contract].insert(base); + vector> const& args = baseArgs.count(base) ? baseArgs.at(base) : decltype(args){}; + + auto baseConstructor = base->constructor(); + if (baseConstructor && !args.empty()) + { + auto const& params = baseConstructor->parameters(); + solAssert(params.size() == args.size(), ""); + for (unsigned i = 0; i < params.size(); ++i) + { + args.at(i)->accept(*this); + if (params.at(i)) + { + solAssert(m_context.knownVariable(*params.at(i)), ""); + m_context.addAssertion(currentValue(*params.at(i)) == expr(*args.at(i), params.at(i)->type())); + } + } + } + } + } + m_errorDest = nullptr; + // Then call initializer_Base from base -> derived + for (auto base: _contract.annotation().linearizedBaseContracts | boost::adaptors::reversed) + { + errorFlag().increaseIndex(); + m_context.addAssertion(smt::constructorCall(*m_contractInitializers.at(base), m_context)); + connectBlocks(m_currentBlock, summary(_contract), errorFlag().currentValue() > 0); + m_context.addAssertion(errorFlag().currentValue() == 0); + } connectBlocks(m_currentBlock, summary(_contract)); - setCurrentBlock(*m_constructorSummaryPredicate); - + setCurrentBlock(*m_constructorSummaries.at(&_contract)); m_queryPlaceholders[&_contract].push_back({smtutil::Expression(true), errorFlag().currentValue(), m_currentBlock}); connectBlocks(m_currentBlock, interface(), errorFlag().currentValue() == 0); @@ -168,16 +196,7 @@ bool CHC::visit(FunctionDefinition const& _function) return false; } - // This is the case for base constructor inlining. - if (m_currentFunction) - { - solAssert(m_currentFunction->isConstructor(), ""); - solAssert(_function.isConstructor(), ""); - solAssert(_function.scope() != m_currentContract, ""); - SMTEncoder::visit(_function); - return false; - } - + // No inlining. solAssert(!m_currentFunction, "Function inlining should not happen in CHC."); m_currentFunction = &_function; @@ -189,23 +208,19 @@ bool CHC::visit(FunctionDefinition const& _function) auto functionPred = predicate(*functionEntryBlock); auto bodyPred = predicate(*bodyBlock); - if (_function.isConstructor()) - connectBlocks(m_currentBlock, functionPred); - else - addRule(functionPred, functionPred.name); + addRule(functionPred, functionPred.name); - m_context.addAssertion(errorFlag().currentValue() == 0); - for (auto const* var: m_stateVariables) - m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var)); - for (auto const& var: _function.parameters()) - m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var)); - m_context.addAssertion(state().state(0) == state().state()); + solAssert(m_currentContract, ""); + m_context.addAssertion(initialConstraints(*m_currentContract, &_function)); connectBlocks(functionPred, bodyPred); setCurrentBlock(*bodyBlock); + solAssert(!m_errorDest, ""); + m_errorDest = m_summaries.at(m_currentContract).at(&_function); SMTEncoder::visit(*m_currentFunction); + m_errorDest = nullptr; return false; } @@ -216,55 +231,29 @@ void CHC::endVisit(FunctionDefinition const& _function) return; solAssert(m_currentFunction && m_currentContract, ""); + // No inlining. + solAssert(m_currentFunction == &_function, ""); - // This is the case for base constructor inlining. - if (m_currentFunction != &_function) + connectBlocks(m_currentBlock, summary(_function)); + setCurrentBlock(*m_summaries.at(m_currentContract).at(&_function)); + + // Query placeholders for constructors are not created here because + // of contracts without constructors. + // Instead, those are created in endVisit(ContractDefinition). + if (!_function.isConstructor()) { - solAssert(m_currentFunction && m_currentFunction->isConstructor(), ""); - solAssert(_function.isConstructor(), ""); - solAssert(_function.scope() != m_currentContract, ""); - } - else - { - // We create an extra exit block for constructors that simply - // connects to the interface in case an explicit constructor - // exists in the hierarchy. - // It is not connected directly here, as normal functions are, - // because of the case where there are only implicit constructors. - // This is done in endVisit(ContractDefinition). - if (_function.isConstructor()) + auto sum = summary(_function); + auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context); + if (_function.isPublic()) { - string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id()); - solAssert(m_currentContract, ""); - auto constructorExit = createSymbolicBlock( - constructorSort(*m_currentContract, state()), - "constructor_exit_" + suffix, - PredicateType::ConstructorSummary, - m_currentContract - ); - connectBlocks(m_currentBlock, predicate(*constructorExit)); - - setCurrentBlock(*constructorExit); + auto txConstraints = m_context.state().txConstraints(_function); + m_queryPlaceholders[&_function].push_back({txConstraints && sum, errorFlag().currentValue(), ifacePre}); + connectBlocks(ifacePre, interface(), txConstraints && sum && errorFlag().currentValue() == 0); } - else - { - auto assertionError = errorFlag().currentValue(); - auto sum = summary(_function); - connectBlocks(m_currentBlock, sum); - auto iface = interface(); - setCurrentBlock(*m_interfaces.at(m_currentContract)); - - auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context); - if (_function.isPublic()) - { - auto txConstraints = m_context.state().txConstraints(_function); - m_queryPlaceholders[&_function].push_back({txConstraints && sum, assertionError, ifacePre}); - connectBlocks(ifacePre, iface, txConstraints && sum && (assertionError == 0)); - } - } - m_currentFunction = nullptr; } + m_currentFunction = nullptr; + SMTEncoder::endVisit(_function); } @@ -564,10 +553,11 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall) m_context.addAssertion(predicate(_funCall)); + solAssert(m_errorDest, ""); connectBlocks( m_currentBlock, - (m_currentFunction && !m_currentFunction->isConstructor()) ? summary(*m_currentFunction) : summary(*m_currentContract), - (errorFlag().currentValue() > 0) + predicate(*m_errorDest), + errorFlag().currentValue() > 0 ); m_context.addAssertion(errorFlag().currentValue() == 0); } @@ -644,9 +634,10 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall) state().newTx(); m_context.addAssertion(originalTx == state().tx()); + solAssert(m_errorDest, ""); connectBlocks( m_currentBlock, - (m_currentFunction && !m_currentFunction->isConstructor()) ? summary(*m_currentFunction) : summary(*m_currentContract), + predicate(*m_errorDest), (errorFlag().currentValue() > 0) ); m_context.addAssertion(errorFlag().currentValue() == 0); @@ -728,6 +719,8 @@ void CHC::resetSourceAnalysis() m_summaries.clear(); m_interfaces.clear(); m_nondetInterfaces.clear(); + m_constructorSummaries.clear(); + m_contractInitializers.clear(); Predicate::reset(); ArraySlicePredicate::reset(); m_blockCounter = 0; @@ -840,6 +833,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) string suffix = contract->name() + "_" + to_string(contract->id()); m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + suffix, PredicateType::Interface, contract); m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract); + m_constructorSummaries[contract] = createConstructorBlock(*contract, "summary_constructor"); + m_contractInitializers[contract] = createConstructorBlock(*contract, "contract_initializer"); for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract)) if (!m_context.knownVariable(*var)) @@ -890,6 +885,39 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) } } +void CHC::defineContractInitializer(ContractDefinition const& _contract) +{ + auto const& implicitConstructorPredicate = *createConstructorBlock(_contract, "contract_initializer_entry"); + + auto implicitFact = smt::constructor(implicitConstructorPredicate, m_context); + addRule(smtutil::Expression::implies(initialConstraints(_contract), implicitFact), implicitFact.name); + setCurrentBlock(implicitConstructorPredicate); + + solAssert(!m_errorDest, ""); + m_errorDest = m_contractInitializers.at(&_contract); + for (auto var: _contract.stateVariables()) + if (var->value()) + { + var->value()->accept(*this); + assignment(*var, *var->value()); + } + m_errorDest = nullptr; + + auto const& afterInit = *createConstructorBlock(_contract, "contract_initializer_after_init"); + connectBlocks(m_currentBlock, predicate(afterInit)); + setCurrentBlock(afterInit); + + if (auto constructor = _contract.constructor()) + { + errorFlag().increaseIndex(); + m_context.addAssertion(smt::functionCall(*m_summaries.at(&_contract).at(constructor), &_contract, m_context)); + connectBlocks(m_currentBlock, initializer(_contract), errorFlag().currentValue() > 0); + m_context.addAssertion(errorFlag().currentValue() == 0); + } + + connectBlocks(m_currentBlock, initializer(_contract)); +} + smtutil::Expression CHC::interface() { solAssert(m_currentContract, ""); @@ -911,14 +939,19 @@ smtutil::Expression CHC::error(unsigned _idx) return m_errorPredicate->functor(_idx)({}); } +smtutil::Expression CHC::initializer(ContractDefinition const& _contract) +{ + return predicate(*m_contractInitializers.at(&_contract)); +} + smtutil::Expression CHC::summary(ContractDefinition const& _contract) { - return constructor(*m_constructorSummaryPredicate, _contract, m_context); + return predicate(*m_constructorSummaries.at(&_contract)); } smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDefinition const& _contract) { - return smt::function(*m_summaries.at(&_contract).at(&_function), _function, &_contract, m_context); + return smt::function(*m_summaries.at(&_contract).at(&_function), &_contract, m_context); } smtutil::Expression CHC::summary(FunctionDefinition const& _function) @@ -942,14 +975,22 @@ Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract) { - auto block = createSymbolicBlock( + return createSymbolicBlock( functionSort(_function, &_contract, state()), "summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract), PredicateType::FunctionSummary, &_function ); +} - return block; +Predicate const* CHC::createConstructorBlock(ContractDefinition const& _contract, string const& _prefix) +{ + return createSymbolicBlock( + constructorSort(_contract, state()), + _prefix + "_" + contractSuffix(_contract) + "_" + uniquePrefix(), + PredicateType::ConstructorSummary, + &_contract + ); } void CHC::createErrorBlock() @@ -967,6 +1008,21 @@ void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression co addRule(edge, _from.name + "_to_" + _to.name); } +smtutil::Expression CHC::initialConstraints(ContractDefinition const& _contract, FunctionDefinition const* _function) +{ + smtutil::Expression conj = state().state() == state().state(0); + conj = conj && errorFlag().currentValue() == 0; + for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract)) + conj = conj && m_context.variable(*var)->valueAtIndex(0) == currentValue(*var); + + FunctionDefinition const* function = _function ? _function : _contract.constructor(); + if (function) + for (auto var: function->parameters()) + conj = conj && m_context.variable(*var)->valueAtIndex(0) == currentValue(*var); + + return conj; +} + vector CHC::initialStateVariables() { return stateVariablesAtIndex(0); @@ -1021,16 +1077,11 @@ smtutil::Expression CHC::predicate(Predicate const& _block) case PredicateType::Interface: solAssert(m_currentContract, ""); return ::interface(_block, *m_currentContract, m_context); - case PredicateType::ImplicitConstructor: - solAssert(m_currentContract, ""); - return implicitConstructor(_block, *m_currentContract, m_context); case PredicateType::ConstructorSummary: - solAssert(m_currentContract, ""); - return constructor(_block, *m_currentContract, m_context); + return constructor(_block, m_context); case PredicateType::FunctionEntry: case PredicateType::FunctionSummary: - solAssert(m_currentFunction, ""); - return smt::function(_block, *m_currentFunction, m_currentContract, m_context); + return smt::function(_block, m_currentContract, m_context); case PredicateType::FunctionBlock: solAssert(m_currentFunction, ""); return functionBlock(_block, *m_currentFunction, m_currentContract, m_context); @@ -1173,9 +1224,10 @@ void CHC::verificationTargetEncountered( errorFlag().increaseIndex(); // create an error edge to the summary + solAssert(m_errorDest, ""); connectBlocks( m_currentBlock, - scopeIsFunction ? summary(*m_currentFunction) : summary(*m_currentContract), + predicate(*m_errorDest), currentPathConditions() && _errorCondition && errorFlag().currentValue() == errorId ); @@ -1416,16 +1468,12 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& string txCex = summaryPredicate->formatSummaryCall(summaryArgs); path.emplace_back(txCex); - /// Recurse on the next interface node which represents the previous transaction - /// or stop. - if (interfaceId) - { - Predicate const* interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).name); - solAssert(interfacePredicate && interfacePredicate->isInterface(), ""); - node = *interfaceId; - } - else + /// Stop when we reach the summary of the analyzed constructor. + if (summaryPredicate->type() == PredicateType::ConstructorSummary) break; + + /// Recurse on the next interface node which represents the previous transaction. + node = *interfaceId; } return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n"); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 9f712ba39..5eb91b64c 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -126,6 +126,11 @@ private: /// in a given _source. void defineInterfacesAndSummaries(SourceUnit const& _source); + /// Creates a CHC system that, for a given contract, + /// - initializes its state variables (as 0 or given value, if any). + /// - "calls" the explicit constructor function of the contract, if any. + void defineContractInitializer(ContractDefinition const& _contract); + /// Interface predicate over current variables. smtutil::Expression interface(); smtutil::Expression interface(ContractDefinition const& _contract); @@ -139,12 +144,18 @@ private: /// The contract is needed here because of inheritance. Predicate const* createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract); + /// @returns a block related to @a _contract's constructor. + Predicate const* createConstructorBlock(ContractDefinition const& _contract, std::string const& _prefix); + /// Creates a new error block to be used by an assertion. /// Also registers the predicate. void createErrorBlock(); void connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints = smtutil::Expression(true)); + /// @returns The initial constraints that set up the beginning of a function. + smtutil::Expression initialConstraints(ContractDefinition const& _contract, FunctionDefinition const* _function = nullptr); + /// @returns the symbolic values of the state variables at the beginning /// of the current transaction. std::vector initialStateVariables(); @@ -160,6 +171,8 @@ private: smtutil::Expression predicate(Predicate const& _block); /// @returns the summary predicate for the called function. smtutil::Expression predicate(FunctionCall const& _funCall); + /// @returns a predicate that defines a contract initializer. + smtutil::Expression initializer(ContractDefinition const& _contract); /// @returns a predicate that defines a constructor summary. smtutil::Expression summary(ContractDefinition const& _contract); /// @returns a predicate that defines a function summary. @@ -231,10 +244,6 @@ private: /// Predicates. //@{ - /// Constructor summary predicate, exists after the constructor - /// (implicit or explicit) and before the interface. - Predicate const* m_constructorSummaryPredicate = nullptr; - /// Artificial Interface predicate. /// Single entry block for all functions. std::map m_interfaces; @@ -245,6 +254,9 @@ private: /// nondeterministically. std::map m_nondetInterfaces; + std::map m_constructorSummaries; + std::map m_contractInitializers; + /// Artificial Error predicate. /// Single error block for all assertions. Predicate const* m_errorPredicate = nullptr; @@ -311,9 +323,16 @@ private: bool m_unknownFunctionCallSeen = false; /// Block where a loop break should go to. - Predicate const* m_breakDest; + Predicate const* m_breakDest = nullptr; /// Block where a loop continue should go to. - Predicate const* m_continueDest; + Predicate const* m_continueDest = nullptr; + + /// Block where an error condition should go to. + /// This can be: + /// 1) Constructor initializer summary, if error happens while evaluating initial values of state variables. + /// 2) Constructor summary, if error happens while evaluating base constructor arguments. + /// 3) Function summary, if error happens inside a function. + Predicate const* m_errorDest = nullptr; //@} /// CHC solver. diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index fb2ef9e8e..335cabb98 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -141,12 +141,12 @@ optional> Predicate::stateVariables() const bool Predicate::isSummary() const { - return functor().name.rfind("summary", 0) == 0; + return m_type == PredicateType::ConstructorSummary || m_type == PredicateType::FunctionSummary; } bool Predicate::isInterface() const { - return functor().name.rfind("interface", 0) == 0; + return m_type == PredicateType::Interface; } string Predicate::formatSummaryCall(vector const& _args) const @@ -190,7 +190,7 @@ string Predicate::formatSummaryCall(vector const& _args) co vector> Predicate::summaryStateValues(vector const& _args) const { /// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). - /// The signature of an implicit constructor summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, postStateVars). + /// The signature of the summary predicate of a contract without constructor is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars). /// Here we are interested in postStateVars. auto stateVars = stateVariables(); solAssert(stateVars.has_value(), ""); @@ -204,7 +204,7 @@ vector> Predicate::summaryStateValues(vector(stateVars->size()); stateLast = stateFirst + static_cast(stateVars->size()); } else diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index 3be3d4927..62f941b38 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -34,7 +34,6 @@ enum class PredicateType { Interface, NondetInterface, - ImplicitConstructor, ConstructorSummary, FunctionEntry, FunctionSummary, diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp index 3c38d4d60..53cc03c79 100644 --- a/libsolidity/formal/PredicateInstance.cpp +++ b/libsolidity/formal/PredicateInstance.cpp @@ -51,31 +51,50 @@ smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition c ); } -smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext& _context) +smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _context) { - auto& state = _context.state(); - vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)}; - return _pred(stateExprs); -} - -smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) -{ - if (auto const* constructor = _contract.constructor()) - return _pred(currentFunctionVariables(*constructor, &_contract, _context)); + auto const& contract = dynamic_cast(*_pred.programNode()); + if (auto const* constructor = contract.constructor()) + return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context)); auto& state = _context.state(); vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0), state.state()}; - return _pred(stateExprs + currentStateVariables(_contract, _context)); + return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context)); +} + +smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context) +{ + auto const& contract = dynamic_cast(*_pred.programNode()); + if (auto const* constructor = contract.constructor()) + return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context)); + + auto& state = _context.state(); + vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state()}; + state.newState(); + stateExprs += vector{state.state()}; + stateExprs += currentStateVariables(contract, _context); + stateExprs += newStateVariables(contract, _context); + return _pred(stateExprs); } smtutil::Expression function( Predicate const& _pred, - FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context ) { - return _pred(currentFunctionVariables(_function, _contract, _context)); + auto const& function = dynamic_cast(*_pred.programNode()); + return _pred(currentFunctionVariablesForDefinition(function, _contract, _context)); +} + +smtutil::Expression functionCall( + Predicate const& _pred, + ContractDefinition const* _contract, + EncodingContext& _context +) +{ + auto const& function = dynamic_cast(*_pred.programNode()); + return _pred(currentFunctionVariablesForCall(function, _contract, _context)); } smtutil::Expression functionBlock( @@ -111,14 +130,22 @@ vector currentStateVariables(ContractDefinition const& _con ); } -vector currentFunctionVariables( +vector newStateVariables(ContractDefinition const& _contract, EncodingContext& _context) +{ + return applyMap( + SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), + [&](auto _var) { return _context.variable(*_var)->increaseIndex(); } + ); +} + +vector currentFunctionVariablesForDefinition( FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context ) { auto& state = _context.state(); - vector exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)}; + vector exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)}; exprs += _contract ? initialStateVariables(*_contract, _context) : vector{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); }); exprs += vector{state.state()}; @@ -128,9 +155,29 @@ vector currentFunctionVariables( return exprs; } +vector currentFunctionVariablesForCall( + FunctionDefinition const& _function, + ContractDefinition const* _contract, + EncodingContext& _context +) +{ + auto& state = _context.state(); + vector exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state()}; + exprs += _contract ? currentStateVariables(*_contract, _context) : vector{}; + exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); + + state.newState(); + + exprs += vector{state.state()}; + exprs += _contract ? newStateVariables(*_contract, _context) : vector{}; + exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->increaseIndex(); }); + exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); + return exprs; +} + vector currentBlockVariables(FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context) { - return currentFunctionVariables(_function, _contract, _context) + + return currentFunctionVariablesForDefinition(_function, _contract, _context) + applyMap( SMTEncoder::localVariablesIncludingModifiers(_function), [&](auto _var) { return _context.variable(*_var)->currentValue(); } diff --git a/libsolidity/formal/PredicateInstance.h b/libsolidity/formal/PredicateInstance.h index 6e287eac8..2f6c77381 100644 --- a/libsolidity/formal/PredicateInstance.h +++ b/libsolidity/formal/PredicateInstance.h @@ -36,13 +36,17 @@ smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx); -smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context); - -smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context); +smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _context); +smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context); smtutil::Expression function( Predicate const& _pred, - FunctionDefinition const& _function, + ContractDefinition const* _contract, + EncodingContext& _context +); + +smtutil::Expression functionCall( + Predicate const& _pred, ContractDefinition const* _contract, EncodingContext& _context ); @@ -62,7 +66,15 @@ std::vector stateVariablesAtIndex(unsigned _index, Contract std::vector currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context); -std::vector currentFunctionVariables( +std::vector newStateVariables(ContractDefinition const& _contract, EncodingContext& _context); + +std::vector currentFunctionVariablesForDefinition( + FunctionDefinition const& _function, + ContractDefinition const* _contract, + EncodingContext& _context +); + +std::vector currentFunctionVariablesForCall( FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context diff --git a/libsolidity/formal/PredicateSort.cpp b/libsolidity/formal/PredicateSort.cpp index 18fcbdfc3..2c3443bc6 100644 --- a/libsolidity/formal/PredicateSort.cpp +++ b/libsolidity/formal/PredicateSort.cpp @@ -46,21 +46,15 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta ); } -SortPointer implicitConstructorSort(SymbolicState& _state) -{ - return make_shared( - vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()}, - SortProvider::boolSort - ); -} - SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state) { if (auto const* constructor = _contract.constructor()) return functionSort(*constructor, &_contract, _state); + auto varSorts = stateSorts(_contract); + vector stateSort{_state.stateSort()}; return make_shared( - vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract), + vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts, SortProvider::boolSort ); } diff --git a/libsolidity/formal/PredicateSort.h b/libsolidity/formal/PredicateSort.h index e87b773fa..b30d09a71 100644 --- a/libsolidity/formal/PredicateSort.h +++ b/libsolidity/formal/PredicateSort.h @@ -39,19 +39,17 @@ namespace solidity::frontend::smt * The nondeterminism behavior of a contract. Signature: * nondet_interface(blockchainState, stateVariables, blockchainState', stateVariables'). * - * 3. Implicit constructor - * The implicit constructor of a contract, that is, without input parameters. Signature: - * implicit_constructor(error, this, cryptoFunctions, txData, blockchainState). + * 3. Constructor entry/summary + * The summary of a contract's deployment procedure. + * Signature: + * If the contract has a constructor function, this is the same as the summary of that function. Otherwise: + * constructor_summary(error, this, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables'). * - * 4. Constructor entry/summary - * The summary of an implicit constructor. Signature: - * constructor_summary(error, this, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables'). - * - * 5. Function entry/summary + * 4. Function entry/summary * The entry point of a function definition. Signature: * function_entry(error, this, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables'). * - * 6. Function body + * 5. Function body * Use for any predicate within a function. Signature: * function_body(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables). */ @@ -62,9 +60,6 @@ smtutil::SortPointer interfaceSort(ContractDefinition const& _contract, Symbolic /// @returns the nondeterminisc interface predicate sort for _contract. smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state); -/// @returns the implicit constructor predicate sort. -smtutil::SortPointer implicitConstructorSort(SymbolicState& _state); - /// @returns the constructor entry/summary predicate sort for _contract. smtutil::SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state); diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index a4044bdea..ecd0800f3 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -131,9 +131,6 @@ bool SMTEncoder::visit(FunctionDefinition const& _function) { m_modifierDepthStack.push_back(-1); - if (_function.isConstructor()) - inlineConstructorHierarchy(dynamic_cast(*_function.scope())); - initializeLocalVariables(_function); _function.parameterList().accept(*this); @@ -2563,6 +2560,37 @@ SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable) solAssert(false, ""); } +map>> SMTEncoder::baseArguments(ContractDefinition const& _contract) +{ + map>> baseArgs; + + for (auto contract: _contract.annotation().linearizedBaseContracts) + { + /// Collect base contracts and potential constructor arguments. + for (auto specifier: contract->baseContracts()) + { + solAssert(specifier, ""); + auto const& base = dynamic_cast(*specifier->name().annotation().referencedDeclaration); + if (auto args = specifier->arguments()) + baseArgs[&base] = *args; + } + /// Collect base constructor arguments given as constructor modifiers. + if (auto constructor = contract->constructor()) + for (auto mod: constructor->modifiers()) + { + auto decl = mod->name()->annotation().referencedDeclaration; + if (auto base = dynamic_cast(decl)) + { + solAssert(!baseArgs.count(base), ""); + if (auto args = mod->arguments()) + baseArgs[base] = *args; + } + } + } + + return baseArgs; +} + void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) { FunctionDefinition const* funDef = functionCallToDefinition(_funCall); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 56cc53938..3ce605ad6 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -77,6 +77,9 @@ public: /// @returns the SourceUnit that contains _scopable. static SourceUnit const* sourceUnitContaining(Scopable const& _scopable); + /// @returns the arguments for each base constructor call in the hierarchy of @a _contract. + std::map>> baseArguments(ContractDefinition const& _contract); + protected: // TODO: Check that we do not have concurrent reads and writes to a variable, // because the order of expression evaluation is undefined diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol index 7a90d2cfb..d48e56b54 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol @@ -19,6 +19,6 @@ contract A is B { } } // ---- -// Warning 4984: (203-208): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (244-249): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 6328: (232-250): CHC: Assertion violation happens here. +// Warning 4984: (203-208): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol index bf8ff11d5..824f79cec 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol @@ -18,6 +18,6 @@ contract A is B { } } // ---- +// Warning 4984: (230-235): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (207-212): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (198-203): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4984: (230-235): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol index 1a9cdbdce..8d8c1f837 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol @@ -28,6 +28,6 @@ contract A is B2, B1 { } // ---- // Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (241-246): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 6328: (334-350): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol index 422d060f6..404c1ee9b 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol @@ -19,8 +19,8 @@ contract C { function f() public view { uint y = this.m(0,1,2,3); assert(y == m[0][1][2][3]); // should hold - assert(y == 1); // should fail + // Disabled because of Spacer seg fault + //assert(y == 1); // should fail } } // ---- -// Warning 6328: (401-415): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol index df70036df..336fad8d5 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol @@ -14,8 +14,8 @@ contract C { function f() public view { uint y = this.m(0,1,2,3); assert(y == m[0][1][2][3]); // should hold - assert(y == 1); // should fail + // Disabled because Spacer seg faults + //assert(y == 1); // should fail } } // ---- -// Warning 6328: (349-363): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol new file mode 100644 index 000000000..81dd66284 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol @@ -0,0 +1,36 @@ +pragma experimental SMTChecker; + +contract A { + uint public x; + constructor(uint a) { x = a; } +} + +contract B is A { + constructor(uint b) A(b) { + } + + function f() internal returns (uint) { + x = x + 1; + return x; + } + + function g() internal returns (uint) { + x = 42; + return x; + } +} + +contract Z is B { + constructor(uint z) B(z + f()) { + } +} + +contract C is Z(5) { + constructor() { + assert(x == 6); + assert(x > 9); // should fail + } +} +// ---- +// Warning 4984: (325-332): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 6328: (400-413): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_2.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_2.sol new file mode 100644 index 000000000..2165b6191 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_2.sol @@ -0,0 +1,38 @@ +pragma experimental SMTChecker; + +contract A { + uint public x; + constructor(uint a) { x = a; } +} + +contract B is A(9) { + constructor(uint b) { + x += b; + } + + function f() internal returns (uint) { + x = x + 1; + return x; + } + + function g() internal returns (uint) { + x = 42; + return x; + } +} + +contract Z is B { + constructor(uint z) B(z + f()) { + } +} + +contract C is Z(5) { + constructor() { + assert(x == 15); + assert(x > 90); // should fail + } +} +// ---- +// Warning 4984: (143-149): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4984: (333-340): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 6328: (409-423): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_1.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_1.sol new file mode 100644 index 000000000..217eaca65 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_1.sol @@ -0,0 +1,34 @@ +pragma experimental SMTChecker; + +contract A { + uint public x; + constructor(uint a) { x = a; } +} + +contract B is A { + constructor(uint b) A(b + f()) { + } + + function f() internal returns (uint) { + x = x + 1; + return x; + } +} + +abstract contract Z is A { + uint k; + constructor(uint z) { + k = z; + } +} + +contract C is Z, B { + constructor() B(x) Z(x) { + assert(x == 1); + assert(k == 0); + assert(x == k); // should fail + } +} +// ---- +// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 6328: (384-398): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_2.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_2.sol new file mode 100644 index 000000000..6c209b1fb --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_2.sol @@ -0,0 +1,33 @@ +pragma experimental SMTChecker; + +contract A { + uint public x; + constructor(uint a) { x = a; } +} + +contract B is A { + constructor(uint b) A(b) { + } + + function f() internal returns (uint) { + x = x + 1; + return x; + } +} + +abstract contract Z is A { + uint k; + constructor(uint z) { + k = z; + } +} + +contract C is Z, B { + constructor() B(f()) Z(f()) { + assert(x == 1); + assert(k == 2); + assert(x == k); // should fail + } +} +// ---- +// Warning 6328: (382-396): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_3.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_3.sol new file mode 100644 index 000000000..e10d6ff75 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_3.sol @@ -0,0 +1,35 @@ +pragma experimental SMTChecker; + +contract A { + uint public x; + constructor(uint a) { x = a; } +} + +contract B is A { + constructor(uint b) A(b + f()) { + } + + function f() internal returns (uint) { + x = x + 1; + return x; + } +} + +abstract contract Z is A { + uint k; + constructor(uint z) { + k = z; + } +} + +contract C is Z, B { + constructor(uint c) B(c) Z(x) { + assert(x == c + 1); + assert(k == 0); + assert(x == k); // should fail + } +} +// ---- +// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4984: (366-371): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 6328: (394-408): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_4.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_4.sol new file mode 100644 index 000000000..6e4054d22 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_4.sol @@ -0,0 +1,35 @@ +pragma experimental SMTChecker; + +contract A { + uint public x; + constructor(uint a) { x = a; } +} + +contract B is A { + constructor(uint b) A(b + f()) { + } + + function f() internal returns (uint) { + x = x + 1; + return x; + } +} + +abstract contract Z is A { + uint k; + constructor(uint z) { + k = z; + } +} + +contract C is Z, B { + constructor(uint c) Z(x) B(c) { + assert(x == c + 1); + assert(k == 0); + assert(x == k); // should fail + } +} +// ---- +// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4984: (366-371): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 6328: (394-408): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_5.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_5.sol new file mode 100644 index 000000000..580cbb46a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_5.sol @@ -0,0 +1,39 @@ +pragma experimental SMTChecker; + +contract A { + uint public x; + constructor(uint a) { x = a; } +} + +contract B is A { + constructor(uint b) A(b + f()) { + } + + function f() internal returns (uint) { + x = x + 1; + return x; + } + + function g() internal returns (uint) { + x = 42; + return x; + } +} + +abstract contract Z is A { + uint k; + constructor(uint z) { + k = z; + } +} + +contract C is Z, B { + constructor() Z(g()) B(f()) { + assert(x == 44); + assert(k == 42); + assert(x == k); // should fail + } +} +// ---- +// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 6328: (456-470): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_6.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_6.sol new file mode 100644 index 000000000..e0d0eab4e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_6.sol @@ -0,0 +1,38 @@ +pragma experimental SMTChecker; + +contract A { + uint public x; + constructor(uint a) { x = a; } +} + +contract B is A { + constructor(uint b) A(b) { + } + + function f() internal returns (uint) { + x = x + 1; + return x; + } + + function g() internal returns (uint) { + x = 42; + return x; + } +} + +abstract contract Z is A { + uint k; + constructor(uint z) { + k = z; + } +} + +contract C is Z, B { + constructor() Z(g()) B(f()) { + assert(x == 1); + assert(k == 42); + assert(x == k); // should fail + } +} +// ---- +// Warning 6328: (449-463): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_7.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_7.sol new file mode 100644 index 000000000..555e77446 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_7.sol @@ -0,0 +1,35 @@ +pragma experimental SMTChecker; + +contract A { + uint public x; + constructor(uint a) { x = a; } +} + +contract B is A { + constructor(uint b) A(b) { + } + + function f() internal returns (uint) { + x = x + 1; + return x; + } + + function g() internal returns (uint) { + x = 42; + return x; + } +} + +contract Z is B { + constructor() B(f()) { + } +} + +contract C is Z { + constructor() { + assert(x == 1); + assert(x > 2); // should fail + } +} +// ---- +// Warning 6328: (387-400): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_8.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_8.sol new file mode 100644 index 000000000..1959ea161 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_8.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract A { + uint public x; + constructor(uint) {} + + function f() internal returns (uint) { + x = x + 1; + return x; + } +} + +contract C is A { + constructor() A(f()) { + assert(x == 1); + assert(x == 0); // should fail + assert(x > 2000); // should fail + } +} +// ---- +// Warning 6328: (218-232): CHC: Assertion violation happens here. +// Warning 6328: (251-267): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_9.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_9.sol new file mode 100644 index 000000000..bb792691c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_9.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; + +contract A { + uint public x = 42; + constructor(uint) {} + + function f() internal returns (uint) { + x = x + 1; + return x; + } +} + +contract C is A { + constructor() A(f()) { + assert(x == 42); + assert(x == 0); // should fail + assert(x == 1); // should fail + assert(x > 2000); // should fail + } +} +// ---- +// Warning 6328: (224-238): CHC: Assertion violation happens here. +// Warning 6328: (257-271): CHC: Assertion violation happens here. +// Warning 6328: (290-306): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_asserts.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_asserts.sol new file mode 100644 index 000000000..ca5662622 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_asserts.sol @@ -0,0 +1,39 @@ +pragma experimental SMTChecker; + +contract A { + int x; + constructor (int a) { x = a;} +} + +contract B is A { + int y; + constructor(int a) A(-a) { + if (a > 0) { + y = 2; + } + else { + y = 4; + } + } +} + +contract C is B { + constructor(int a) B(a) { + assert(y != 3); // should hold + assert(y == 4); // should fail + if (a > 0) { + assert(x < 0 && y == 2); // should hold + assert(x < 0 && y == 4); // should fail + } + else { + assert(x >= 0 && y == 4); // should hold + assert(x >= 0 && y == 2); // should fail + assert(x > 0); // should fail + } + } +} +// ---- +// Warning 6328: (280-294): CHC: Assertion violation happens here. +// Warning 6328: (372-395): CHC: Assertion violation happens here. +// Warning 6328: (472-496): CHC: Assertion violation happens here. +// Warning 6328: (516-529): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol index 4a4e49517..957677bf8 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol @@ -23,9 +23,9 @@ contract A is B { // ---- // Warning 4984: (157-162): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4984: (216-221): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (239-244): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (261-266): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (261-270): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (287-292): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 6328: (275-293): CHC: Assertion violation happens here. +// Warning 4984: (216-221): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol index f1768f693..566d907bd 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol @@ -23,8 +23,8 @@ contract A is B { // ---- // Warning 4984: (157-163): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4984: (217-222): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (240-245): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (262-268): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (285-290): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 6328: (273-291): CHC: Assertion violation happens here. +// Warning 4984: (217-222): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_tree.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_tree.sol new file mode 100644 index 000000000..a7ae53fc4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_tree.sol @@ -0,0 +1,43 @@ +pragma experimental SMTChecker; + +contract A { + int x; + constructor (int a) { x = a; } +} + +contract Z { + int z; + constructor(int _z) { + z = _z; + } +} + +contract B is A, Z { + constructor(int b) A(b) Z(x) { + assert(x == b); + assert(z == 0); + } +} + +contract F is Z, A { + constructor(int b) Z(x) A(b) { + assert(x == b); + assert(z == 0); + } +} + +contract C is B { + constructor(int c) B(-c) { + if (x > 0) { + assert(c < 0); // should hold + assert(c >= 0); // should fail + } + else { + assert(c < 0); // should fail + assert(c >= 0); // should hold + } + } +} +// ---- +// Warning 6328: (436-450): CHC: Assertion violation happens here. +// Warning 6328: (483-496): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol index 08690b634..f049ce10b 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol @@ -5,11 +5,17 @@ contract A { } contract B is A { - constructor() { x = 2; } + constructor() { + assert(x == 1); + x = 2; + } } contract C is A { - constructor() { x = 3; } + constructor() { + assert(x == 1); + x = 3; + } } contract D is B, C { @@ -19,4 +25,5 @@ contract D is B, C { } } // ---- -// Warning 6328: (214-228): CHC: Assertion violation happens here. +// Warning 6328: (167-181): CHC: Assertion violation happens here. +// Warning 6328: (256-270): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol new file mode 100644 index 000000000..af505cc52 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract A { + uint x; + constructor() { + x = 42; + } + function f() public view returns(uint256) { + return x; + } +} +contract B is A { + uint y = f(); +} +contract C is B { + function g() public view { + assert(y == 42); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol index 94116f30a..b13c8d300 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol @@ -15,10 +15,10 @@ contract C // Erasing knowledge about memory references should not // erase knowledge about storage references. assert(c[0] == 42); - assert(a[0] == 2); + // Removed because current Spacer seg faults in cex generation. + //assert(a[0] == 2); // Removed because current Spacer seg faults in cex generation. //assert(b[0] == 1); } } // ---- -// Warning 6328: (476-493): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol index 59fb6c067..abf3441df 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol @@ -21,7 +21,8 @@ contract C { // Removed because current Spacer seg faults in cex generation. //assert(s1.t.y == s2.t.y); s1.a[2] = 4; - assert(s1.a[2] == s2.a[2]); + // Removed because current Spacer seg faults in cex generation. + //assert(s1.a[2] == s2.a[2]); s1.ts[3].y = 5; // Removed because current Spacer seg faults in cex generation. //assert(s1.ts[3].y == s2.ts[3].y); @@ -30,5 +31,4 @@ contract C { } } // ---- -// Warning 6328: (456-482): CHC: Assertion violation happens here. -// Warning 6328: (629-667): CHC: Assertion violation happens here. +// Warning 6328: (697-735): CHC: Assertion violation happens here. From cb72d76aaf22d0c93e5922567c6fdaac7d69f0b1 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Thu, 3 Dec 2020 22:40:30 +0100 Subject: [PATCH 11/17] Add const ref to prevent segfaults. --- Changelog.md | 1 + libsmtutil/CHCSmtLib2Interface.cpp | 2 +- libsmtutil/CHCSmtLib2Interface.h | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Changelog.md b/Changelog.md index b4a833463..de89f7aca 100644 --- a/Changelog.md +++ b/Changelog.md @@ -16,6 +16,7 @@ Bugfixes: * Code generator: Do not pad empty string literals with a single 32-byte zero field in the ABI coder v1. * SMTChecker: Fix internal compiler error when doing bitwise compound assignment with string literals. * SMTChecker: Fix internal error when trying to generate counterexamples with old z3. + * SMTChecker: Fix segmentation fault that could occur on certain SMT-enabled sources when no SMT solver was available. * Yul Optimizer: Fix a bug in NameSimplifier where a new name created by NameSimplifier could also be created by NameDispenser. * Yul Optimizer: Removed NameSimplifier from optimization steps available to users. diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index d64f39379..bbbc63bfe 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -36,7 +36,7 @@ using namespace solidity::frontend; using namespace solidity::smtutil; CHCSmtLib2Interface::CHCSmtLib2Interface( - map _queryResponses, + map const& _queryResponses, ReadCallback::Callback _smtCallback, optional _queryTimeout ): diff --git a/libsmtutil/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h index f797d3d77..17227867e 100644 --- a/libsmtutil/CHCSmtLib2Interface.h +++ b/libsmtutil/CHCSmtLib2Interface.h @@ -33,7 +33,7 @@ class CHCSmtLib2Interface: public CHCSolverInterface { public: explicit CHCSmtLib2Interface( - std::map _queryResponses = {}, + std::map const& _queryResponses = {}, frontend::ReadCallback::Callback _smtCallback = {}, std::optional _queryTimeout = {} ); From 0d6cae304bc759127047af8c3e4c0e6bd83a899e Mon Sep 17 00:00:00 2001 From: Bhargava Shastry Date: Fri, 4 Dec 2020 15:31:32 +0100 Subject: [PATCH 12/17] abiv2 proto fuzzer: Move anon namespace utility functions to common source --- test/tools/ossfuzz/abiV2FuzzerCommon.cpp | 43 ++++++++++++++ test/tools/ossfuzz/abiV2FuzzerCommon.h | 37 +++++++++++- test/tools/ossfuzz/abiV2ProtoFuzzer.cpp | 73 ++---------------------- 3 files changed, 84 insertions(+), 69 deletions(-) diff --git a/test/tools/ossfuzz/abiV2FuzzerCommon.cpp b/test/tools/ossfuzz/abiV2FuzzerCommon.cpp index c9109ecdb..9e506b7d7 100644 --- a/test/tools/ossfuzz/abiV2FuzzerCommon.cpp +++ b/test/tools/ossfuzz/abiV2FuzzerCommon.cpp @@ -37,3 +37,46 @@ solidity::bytes SolidityCompilationFramework::compileContract( ); return obj.bytecode; } + +bool AbiV2Utility::isOutputExpected( + uint8_t const* _result, + size_t _length, + std::vector const& _expectedOutput +) +{ + if (_length != _expectedOutput.size()) + return false; + + return (memcmp(_result, _expectedOutput.data(), _length) == 0); +} + +evmc_message AbiV2Utility::initializeMessage(bytes const& _input) +{ + // Zero initialize all message fields + evmc_message msg = {}; + // Gas available (value of type int64_t) is set to its maximum + // value. + msg.gas = std::numeric_limits::max(); + msg.input_data = _input.data(); + msg.input_size = _input.size(); + return msg; +} + +evmc::result AbiV2Utility::executeContract( + EVMHost& _hostContext, + bytes const& _functionHash, + evmc_address _deployedAddress +) +{ + evmc_message message = initializeMessage(_functionHash); + message.destination = _deployedAddress; + message.kind = EVMC_CALL; + return _hostContext.call(message); +} + +evmc::result AbiV2Utility::deployContract(EVMHost& _hostContext, bytes const& _code) +{ + evmc_message message = initializeMessage(_code); + message.kind = EVMC_CREATE; + return _hostContext.call(message); +} \ No newline at end of file diff --git a/test/tools/ossfuzz/abiV2FuzzerCommon.h b/test/tools/ossfuzz/abiV2FuzzerCommon.h index e18458b77..d7e274dc4 100644 --- a/test/tools/ossfuzz/abiV2FuzzerCommon.h +++ b/test/tools/ossfuzz/abiV2FuzzerCommon.h @@ -1,5 +1,7 @@ #pragma once +#include + #include #include @@ -9,9 +11,10 @@ #include +#include + namespace solidity::test::abiv2fuzzer { - class SolidityCompilationFramework { public: @@ -32,4 +35,36 @@ protected: langutil::EVMVersion m_evmVersion; }; +struct AbiV2Utility +{ + /// Compares the contents of the memory address pointed to + /// by `_result` of `_length` bytes to the expected output. + /// Returns true if `_result` matches expected output, false + /// otherwise. + static bool isOutputExpected( + uint8_t const* _result, + size_t _length, + std::vector const& _expectedOutput + ); + /// Accepts a reference to a user-specified input and returns an + /// evmc_message with all of its fields zero initialized except + /// gas and input fields. + /// The gas field is set to the maximum permissible value so that we + /// don't run into out of gas errors. The input field is copied from + /// user input. + static evmc_message initializeMessage(bytes const& _input); + /// Accepts host context implementation, and keccak256 hash of the function + /// to be called at a specified address in the simulated blockchain as + /// input and returns the result of the execution of the called function. + static evmc::result executeContract( + EVMHost& _hostContext, + bytes const& _functionHash, + evmc_address _deployedAddress + ); + /// Accepts a reference to host context implementation and byte code + /// as input and deploys it on the simulated blockchain. Returns the + /// result of deployment. + static evmc::result deployContract(EVMHost& _hostContext, bytes const& _code); +}; + } diff --git a/test/tools/ossfuzz/abiV2ProtoFuzzer.cpp b/test/tools/ossfuzz/abiV2ProtoFuzzer.cpp index 8c529630f..c31ec8ee0 100644 --- a/test/tools/ossfuzz/abiV2ProtoFuzzer.cpp +++ b/test/tools/ossfuzz/abiV2ProtoFuzzer.cpp @@ -16,89 +16,26 @@ */ // SPDX-License-Identifier: GPL-3.0 -#include #include #include -#include #include #include -static evmc::VM evmone = evmc::VM{evmc_create_evmone()}; - using namespace solidity::test::abiv2fuzzer; using namespace solidity::test; using namespace solidity::util; using namespace solidity; using namespace std; -namespace -{ -/// Test function returns a uint256 value -static size_t const expectedOutputLength = 32; +static evmc::VM evmone = evmc::VM{evmc_create_evmone()}; /// Expected output value is decimal 0 -static uint8_t const expectedOutput[expectedOutputLength] = { +static vector const expectedOutput = { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 }; -/// Compares the contents of the memory address pointed to -/// by `_result` of `_length` bytes to the expected output. -/// Returns true if `_result` matches expected output, false -/// otherwise. -bool isOutputExpected(uint8_t const* _result, size_t _length) -{ - if (_length != expectedOutputLength) - return false; - - return (memcmp(_result, expectedOutput, expectedOutputLength) == 0); -} - -/// Accepts a reference to a user-specified input and returns an -/// evmc_message with all of its fields zero initialized except -/// gas and input fields. -/// The gas field is set to the maximum permissible value so that we -/// don't run into out of gas errors. The input field is copied from -/// user input. -evmc_message initializeMessage(bytes const& _input) -{ - // Zero initialize all message fields - evmc_message msg = {}; - // Gas available (value of type int64_t) is set to its maximum - // value. - msg.gas = std::numeric_limits::max(); - msg.input_data = _input.data(); - msg.input_size = _input.size(); - return msg; -} - -/// Accepts host context implementation, and keccak256 hash of the function -/// to be called at a specified address in the simulated blockchain as -/// input and returns the result of the execution of the called function. -evmc::result executeContract( - EVMHost& _hostContext, - bytes const& _functionHash, - evmc_address _deployedAddress -) -{ - evmc_message message = initializeMessage(_functionHash); - message.destination = _deployedAddress; - message.kind = EVMC_CALL; - return _hostContext.call(message); -} - -/// Accepts a reference to host context implementation and byte code -/// as input and deploys it on the simulated blockchain. Returns the -/// result of deployment. -evmc::result deployContract(EVMHost& _hostContext, bytes const& _code) -{ - evmc_message message = initializeMessage(_code); - message.kind = EVMC_CREATE; - return _hostContext.call(message); -} -} - DEFINE_PROTO_FUZZER(Contract const& _input) { string contract_source = ProtoConverter{}.contractToString(_input); @@ -147,7 +84,7 @@ DEFINE_PROTO_FUZZER(Contract const& _input) EVMHost hostContext(version, evmone); // Deploy contract and signal failure if deploy failed - evmc::result createResult = deployContract(hostContext, byteCode); + evmc::result createResult = AbiV2Utility::deployContract(hostContext, byteCode); solAssert( createResult.status_code == EVMC_SUCCESS, "Proto ABIv2 Fuzzer: Contract creation failed" @@ -155,7 +92,7 @@ DEFINE_PROTO_FUZZER(Contract const& _input) // Execute test function and signal failure if EVM reverted or // did not return expected output on successful execution. - evmc::result callResult = executeContract( + evmc::result callResult = AbiV2Utility::executeContract( hostContext, fromHex(hexEncodedInput), createResult.create_address @@ -165,7 +102,7 @@ DEFINE_PROTO_FUZZER(Contract const& _input) solAssert(callResult.status_code != EVMC_REVERT, "Proto ABIv2 fuzzer: EVM One reverted"); if (callResult.status_code == EVMC_SUCCESS) solAssert( - isOutputExpected(callResult.output_data, callResult.output_size), + AbiV2Utility::isOutputExpected(callResult.output_data, callResult.output_size, expectedOutput), "Proto ABIv2 fuzzer: ABIv2 coding failure found" ); } From 2839a1b0bfc635ce56361033eea95f02b3346422 Mon Sep 17 00:00:00 2001 From: Djordje Mijovic Date: Fri, 4 Dec 2020 14:17:52 +0100 Subject: [PATCH 13/17] [Sol->Yul] Documenting difference in initialization order in case of inheritance. Co-authored-by: Leonardo Co-authored-by: Daniel Kirchner --- docs/ir/ir-breaking-changes.rst | 36 +++++++++++++++++++ .../constructor_inheritance_init_order_3.sol | 12 +++++++ 2 files changed, 48 insertions(+) create mode 100644 test/libsolidity/constructor_inheritance_init_order_3.sol diff --git a/docs/ir/ir-breaking-changes.rst b/docs/ir/ir-breaking-changes.rst index 7ffa49508..ec6126beb 100644 --- a/docs/ir/ir-breaking-changes.rst +++ b/docs/ir/ir-breaking-changes.rst @@ -33,3 +33,39 @@ Consequently, if the padding space within a struct is used to store data (e.g. i } We have the same behavior for implicit delete, for example when array of structs is shortened. + + * The order of contract initialization has changed in case of inheritance. + +The order used to be: + - All state variables are zero-initialized at the beginning. + - Evaluate base constructor arguments from most derived to most base contract. + - Initialize all state variables in the whole inheritance hierarchy from most base to most derived. + - Run the constructor, if present, for all contracts in the linearized hierarchy from most base to most derived. + +New order: + - All state variables are zero-initialized at the beginning. + - Evaluate base constructor arguments from most derived to most base contract. + - For every contract in order from most base to most derived in the linearized hierarchy execute: + 1. State variables are assigned value their initial values, if present at declaration. + 2. Constructor, if present. + +This causes differences in some contracts, for example: +:: + // SPDX-License-Identifier: GPL-3.0 + pragma solidity >0.7.0; + + contract A { + uint x; + constructor() { + x = 42; + } + function f() public view returns(uint256) { + return x; + } + } + contract B is A { + uint public y = f(); + } + +Previously, ``y`` would be set to 0. This is due to the fact that we would first initialize state variables: First, ``x`` is set to 0, and when initializing ``y``, ``f()`` would return 0 causing ``y`` to be 0 as well. +With the new rules, ``y`` will be set to 42. We first initialize ``x`` to 0, then call A's constructor which sets ``x`` to 42. Finally, when initializing ``y``, ``f()`` returns 42 causing ``y`` to be 42. diff --git a/test/libsolidity/constructor_inheritance_init_order_3.sol b/test/libsolidity/constructor_inheritance_init_order_3.sol new file mode 100644 index 000000000..c9719a108 --- /dev/null +++ b/test/libsolidity/constructor_inheritance_init_order_3.sol @@ -0,0 +1,12 @@ +contract A { + uint public x; + constructor(uint) {} + function f() public { x = 4; } +} +contract B is A { + constructor() A(f()) {} +} +// ==== +// compileViaYul: also +// ---- +// x() -> 4 From 32fd692c51da8f23afa603d4f745fe723417eb1c Mon Sep 17 00:00:00 2001 From: Bhargava Shastry Date: Thu, 23 Jul 2020 11:58:10 +0200 Subject: [PATCH 14/17] Yul interpreter: Introduce expression evaluation maximum nesting depth --- test/libyul/EwasmTranslationTest.cpp | 1 + test/libyul/YulInterpreterTest.cpp | 1 + .../expr_nesting_depth_exceeded.yul | 14 ++++++++++++++ .../expr_nesting_depth_not_exceeded.yul | 14 ++++++++++++++ test/tools/ossfuzz/yulFuzzerCommon.cpp | 8 +++++++- test/tools/ossfuzz/yulFuzzerCommon.h | 5 ++++- test/tools/ossfuzz/yulProto_diff_ossfuzz.cpp | 7 ++++--- test/tools/yulInterpreter/Interpreter.cpp | 13 +++++++++++++ test/tools/yulInterpreter/Interpreter.h | 12 ++++++++++++ 9 files changed, 70 insertions(+), 5 deletions(-) create mode 100644 test/libyul/yulInterpreterTests/expr_nesting_depth_exceeded.yul create mode 100644 test/libyul/yulInterpreterTests/expr_nesting_depth_not_exceeded.yul diff --git a/test/libyul/EwasmTranslationTest.cpp b/test/libyul/EwasmTranslationTest.cpp index fe3d42969..a8fc1a586 100644 --- a/test/libyul/EwasmTranslationTest.cpp +++ b/test/libyul/EwasmTranslationTest.cpp @@ -102,6 +102,7 @@ string EwasmTranslationTest::interpret() InterpreterState state; state.maxTraceSize = 10000; state.maxSteps = 1000000; + state.maxExprNesting = 64; try { Interpreter::run(state, WasmDialect{}, *m_object->code); diff --git a/test/libyul/YulInterpreterTest.cpp b/test/libyul/YulInterpreterTest.cpp index ec1fa53f1..259e879b3 100644 --- a/test/libyul/YulInterpreterTest.cpp +++ b/test/libyul/YulInterpreterTest.cpp @@ -89,6 +89,7 @@ string YulInterpreterTest::interpret() InterpreterState state; state.maxTraceSize = 32; state.maxSteps = 512; + state.maxExprNesting = 64; try { Interpreter::run(state, EVMDialect::strictAssemblyForEVMObjects(langutil::EVMVersion{}), *m_ast); diff --git a/test/libyul/yulInterpreterTests/expr_nesting_depth_exceeded.yul b/test/libyul/yulInterpreterTests/expr_nesting_depth_exceeded.yul new file mode 100644 index 000000000..c1456b00f --- /dev/null +++ b/test/libyul/yulInterpreterTests/expr_nesting_depth_exceeded.yul @@ -0,0 +1,14 @@ +{ + function f(x) -> y + { + // 32 nested additions are computed in + // exactly 66 expression evaluation steps + y := add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,x)))))))))))))))))))))))))))))))) + } + mstore(0,f(0)) +} +// ---- +// Trace: +// Maximum expression nesting level reached. +// Memory dump: +// Storage dump: diff --git a/test/libyul/yulInterpreterTests/expr_nesting_depth_not_exceeded.yul b/test/libyul/yulInterpreterTests/expr_nesting_depth_not_exceeded.yul new file mode 100644 index 000000000..0a3470571 --- /dev/null +++ b/test/libyul/yulInterpreterTests/expr_nesting_depth_not_exceeded.yul @@ -0,0 +1,14 @@ +{ + function f(x) -> y + { + // 31 nested additions are computed in + // exactly 64 expression evaluation steps + y := add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,x))))))))))))))))))))))))))))))) + } + mstore(0,f(0)) +} +// ---- +// Trace: +// Memory dump: +// 0: 000000000000000000000000000000000000000000000000000000000000001f +// Storage dump: diff --git a/test/tools/ossfuzz/yulFuzzerCommon.cpp b/test/tools/ossfuzz/yulFuzzerCommon.cpp index 86cea8327..d977c7761 100644 --- a/test/tools/ossfuzz/yulFuzzerCommon.cpp +++ b/test/tools/ossfuzz/yulFuzzerCommon.cpp @@ -27,12 +27,14 @@ yulFuzzerUtil::TerminationReason yulFuzzerUtil::interpret( shared_ptr _ast, Dialect const& _dialect, size_t _maxSteps, - size_t _maxTraceSize + size_t _maxTraceSize, + size_t _maxExprNesting ) { InterpreterState state; state.maxTraceSize = _maxTraceSize; state.maxSteps = _maxSteps; + state.maxExprNesting = _maxExprNesting; // Add 64 bytes of pseudo-randomly generated calldata so that // calldata opcodes perform non trivial work. state.calldata = { @@ -59,6 +61,10 @@ yulFuzzerUtil::TerminationReason yulFuzzerUtil::interpret( { reason = TerminationReason::TraceLimitReached; } + catch (ExpressionNestingLimitReached const&) + { + reason = TerminationReason::ExpresionNestingLimitReached; + } catch (ExplicitlyTerminated const&) { reason = TerminationReason::ExplicitlyTerminated; diff --git a/test/tools/ossfuzz/yulFuzzerCommon.h b/test/tools/ossfuzz/yulFuzzerCommon.h index cc20d6163..489cc4532 100644 --- a/test/tools/ossfuzz/yulFuzzerCommon.h +++ b/test/tools/ossfuzz/yulFuzzerCommon.h @@ -28,6 +28,7 @@ struct yulFuzzerUtil ExplicitlyTerminated, StepLimitReached, TraceLimitReached, + ExpresionNestingLimitReached, None }; @@ -36,10 +37,12 @@ struct yulFuzzerUtil std::shared_ptr _ast, Dialect const& _dialect, size_t _maxSteps = maxSteps, - size_t _maxTraceSize = maxTraceSize + size_t _maxTraceSize = maxTraceSize, + size_t _maxExprNesting = maxExprNesting ); static size_t constexpr maxSteps = 100; static size_t constexpr maxTraceSize = 75; + static size_t constexpr maxExprNesting = 64; }; } diff --git a/test/tools/ossfuzz/yulProto_diff_ossfuzz.cpp b/test/tools/ossfuzz/yulProto_diff_ossfuzz.cpp index de9bfe9c7..2ee2b702e 100644 --- a/test/tools/ossfuzz/yulProto_diff_ossfuzz.cpp +++ b/test/tools/ossfuzz/yulProto_diff_ossfuzz.cpp @@ -99,7 +99,8 @@ DEFINE_PROTO_FUZZER(Program const& _input) if ( termReason == yulFuzzerUtil::TerminationReason::StepLimitReached || - termReason == yulFuzzerUtil::TerminationReason::TraceLimitReached + termReason == yulFuzzerUtil::TerminationReason::TraceLimitReached || + termReason == yulFuzzerUtil::TerminationReason::ExpresionNestingLimitReached ) return; @@ -109,10 +110,10 @@ DEFINE_PROTO_FUZZER(Program const& _input) stack.parserResult()->code, EVMDialect::strictAssemblyForEVMObjects(version) ); - if ( termReason == yulFuzzerUtil::TerminationReason::StepLimitReached || - termReason == yulFuzzerUtil::TerminationReason::TraceLimitReached + termReason == yulFuzzerUtil::TerminationReason::TraceLimitReached || + termReason == yulFuzzerUtil::TerminationReason::ExpresionNestingLimitReached ) return; diff --git a/test/tools/yulInterpreter/Interpreter.cpp b/test/tools/yulInterpreter/Interpreter.cpp index 70cd9dc29..df1aaaef3 100644 --- a/test/tools/yulInterpreter/Interpreter.cpp +++ b/test/tools/yulInterpreter/Interpreter.cpp @@ -247,6 +247,7 @@ void Interpreter::incrementStep() void ExpressionEvaluator::operator()(Literal const& _literal) { + incrementStep(); static YulString const trueString("true"); static YulString const falseString("false"); @@ -256,6 +257,7 @@ void ExpressionEvaluator::operator()(Literal const& _literal) void ExpressionEvaluator::operator()(Identifier const& _identifier) { solAssert(m_variables.count(_identifier.name), ""); + incrementStep(); setValue(m_variables.at(_identifier.name)); } @@ -326,6 +328,7 @@ void ExpressionEvaluator::evaluateArgs( vector> const* _literalArguments ) { + incrementStep(); vector values; size_t i = 0; /// Function arguments are evaluated in reverse. @@ -341,3 +344,13 @@ void ExpressionEvaluator::evaluateArgs( m_values = std::move(values); std::reverse(m_values.begin(), m_values.end()); } + +void ExpressionEvaluator::incrementStep() +{ + m_nestingLevel++; + if (m_state.maxExprNesting > 0 && m_nestingLevel > m_state.maxExprNesting) + { + m_state.trace.emplace_back("Maximum expression nesting level reached."); + throw ExpressionNestingLimitReached(); + } +} diff --git a/test/tools/yulInterpreter/Interpreter.h b/test/tools/yulInterpreter/Interpreter.h index 42c8c9138..7af799bbd 100644 --- a/test/tools/yulInterpreter/Interpreter.h +++ b/test/tools/yulInterpreter/Interpreter.h @@ -55,6 +55,10 @@ class TraceLimitReached: public InterpreterTerminatedGeneric { }; +class ExpressionNestingLimitReached: public InterpreterTerminatedGeneric +{ +}; + enum class ControlFlowState { Default, @@ -92,6 +96,7 @@ struct InterpreterState size_t maxTraceSize = 0; size_t maxSteps = 0; size_t numSteps = 0; + size_t maxExprNesting = 0; ControlFlowState controlFlowState = ControlFlowState::Default; void dumpTraceAndState(std::ostream& _out) const; @@ -202,6 +207,11 @@ private: std::vector> const* _literalArguments ); + /// Increment evaluation count, throwing exception if the + /// nesting level is beyond the upper bound configured in + /// the interpreter state. + void incrementStep(); + InterpreterState& m_state; Dialect const& m_dialect; /// Values of variables. @@ -209,6 +219,8 @@ private: Scope& m_scope; /// Current value of the expression std::vector m_values; + /// Current expression nesting level + unsigned m_nestingLevel = 0; }; } From 6383d64ef49395cd79070028fc596dc029cd9864 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= Date: Fri, 4 Dec 2020 23:40:19 +0100 Subject: [PATCH 15/17] Upgrade the CircleCI job running bytecode comparison from node.js 10 to 14 --- .circleci/config.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index 6a7a03a61..da0941987 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -1046,7 +1046,7 @@ jobs: b_bytecode_ems: docker: - - image: circleci/node:10 + - image: circleci/node:14 environment: SOLC_EMSCRIPTEN: "On" steps: From c39a5e2b7a3fabbf687f53a2823fc087be6c1a7e Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Mon, 7 Dec 2020 11:24:13 +0100 Subject: [PATCH 16/17] Fix accidental repetition in ir breaking changes docs. --- docs/ir/ir-breaking-changes.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/ir/ir-breaking-changes.rst b/docs/ir/ir-breaking-changes.rst index ec6126beb..0d8521c52 100644 --- a/docs/ir/ir-breaking-changes.rst +++ b/docs/ir/ir-breaking-changes.rst @@ -46,7 +46,7 @@ New order: - All state variables are zero-initialized at the beginning. - Evaluate base constructor arguments from most derived to most base contract. - For every contract in order from most base to most derived in the linearized hierarchy execute: - 1. State variables are assigned value their initial values, if present at declaration. + 1. State variables are assigned their initial values, if present at declaration. 2. Constructor, if present. This causes differences in some contracts, for example: From 804e98a13610bcf65523abdbd4db71dc34827028 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Mon, 7 Dec 2020 11:28:20 +0100 Subject: [PATCH 17/17] Rephrase. --- docs/ir/ir-breaking-changes.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/ir/ir-breaking-changes.rst b/docs/ir/ir-breaking-changes.rst index 0d8521c52..13a3e0759 100644 --- a/docs/ir/ir-breaking-changes.rst +++ b/docs/ir/ir-breaking-changes.rst @@ -46,7 +46,7 @@ New order: - All state variables are zero-initialized at the beginning. - Evaluate base constructor arguments from most derived to most base contract. - For every contract in order from most base to most derived in the linearized hierarchy execute: - 1. State variables are assigned their initial values, if present at declaration. + 1. If present at declaration, initial values are assigned to state variables. 2. Constructor, if present. This causes differences in some contracts, for example: