From b3174db322ffec340f6590fec72b411159b3a809 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Mon, 11 Nov 2019 14:14:17 +0100 Subject: [PATCH 1/6] Update PPA build script for Z3 to version 4.8.6. And add eoan to Z3 and release PPA script. --- scripts/deps-ppa/static_z3.sh | 6 +++--- scripts/release_ppa.sh | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/scripts/deps-ppa/static_z3.sh b/scripts/deps-ppa/static_z3.sh index b971fdd24..9f39a79c9 100755 --- a/scripts/deps-ppa/static_z3.sh +++ b/scripts/deps-ppa/static_z3.sh @@ -25,9 +25,9 @@ set -ev keyid=70D110489D66E2F6 email=builds@ethereum.org packagename=libz3-static-dev -version=4.8.5 +version=4.8.6 -DISTRIBUTIONS="bionic disco" +DISTRIBUTIONS="bionic disco eoan" for distribution in $DISTRIBUTIONS do @@ -40,7 +40,7 @@ pparepo=cpp-build-deps ppafilesurl=https://launchpad.net/~ethereum/+archive/ubuntu/${pparepo}/+files # Fetch source -git clone --depth 1 --branch Z3-${version} https://github.com/Z3Prover/z3.git +git clone --depth 1 --branch z3-${version} https://github.com/Z3Prover/z3.git cd z3 debversion="$version" diff --git a/scripts/release_ppa.sh b/scripts/release_ppa.sh index 78ea3118b..fcf3a8102 100755 --- a/scripts/release_ppa.sh +++ b/scripts/release_ppa.sh @@ -57,7 +57,7 @@ packagename=solc static_build_distribution=disco -DISTRIBUTIONS="bionic disco" +DISTRIBUTIONS="bionic disco eoan" if is_release then From 3b75466b769aa99752d693b3426516177b07c689 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Mon, 11 Nov 2019 15:54:04 +0100 Subject: [PATCH 2/6] Update to Z3 4.8.6 in ubuntu clang Dockerfile. --- .circleci/docker/Dockerfile.clang.ubuntu1904 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.circleci/docker/Dockerfile.clang.ubuntu1904 b/.circleci/docker/Dockerfile.clang.ubuntu1904 index 9c975984d..4fb9b1132 100644 --- a/.circleci/docker/Dockerfile.clang.ubuntu1904 +++ b/.circleci/docker/Dockerfile.clang.ubuntu1904 @@ -62,7 +62,7 @@ RUN git clone --recursive -b boost-1.69.0 https://github.com/boostorg/boost.git rm -rf /usr/src/boost # Z3 -RUN git clone --depth 1 -b Z3-4.8.5 https://github.com/Z3Prover/z3.git \ +RUN git clone --depth 1 -b z3-4.8.6 https://github.com/Z3Prover/z3.git \ /usr/src/z3; \ cd /usr/src/z3; \ python scripts/mk_make.py --prefix=/usr ; \ From e643c4ca288617192975069f7e2d22fa92bd73e7 Mon Sep 17 00:00:00 2001 From: Mathias Baumann Date: Mon, 11 Nov 2019 17:09:59 +0100 Subject: [PATCH 3/6] Add ``while (..)` to style checker --- libsolidity/analysis/StaticAnalyzer.cpp | 2 +- scripts/check_style.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/libsolidity/analysis/StaticAnalyzer.cpp b/libsolidity/analysis/StaticAnalyzer.cpp index 2a0aaddcb..0d2a978db 100644 --- a/libsolidity/analysis/StaticAnalyzer.cpp +++ b/libsolidity/analysis/StaticAnalyzer.cpp @@ -227,7 +227,7 @@ bool StaticAnalyzer::visit(MemberAccess const& _memberAccess) if (m_constructor) { auto const* expr = &_memberAccess.expression(); - while(expr) + while (expr) { if (auto id = dynamic_cast(expr)) { diff --git a/scripts/check_style.sh b/scripts/check_style.sh index 0f9a8096e..e4f31a1f6 100755 --- a/scripts/check_style.sh +++ b/scripts/check_style.sh @@ -17,7 +17,7 @@ fi FORMATERROR=$( ( - git grep -nIE "\<(if|for)\(" -- '*.h' '*.cpp' # no space after "if" or "for" + git grep -nIE "\<(if|for|while)\(" -- '*.h' '*.cpp' # no space after "if", "for" or "while" git grep -nIE "\\s*\([^=]*\>\s:\s.*\)" -- '*.h' '*.cpp' # no space before range based for-loop git grep -nIE "\\s*\(.*\)\s*\{\s*$" -- '*.h' '*.cpp' # "{\n" on same line as "if" / "for" git grep -nIE "[,\(<]\s*const " -- '*.h' '*.cpp' # const on left side of type From e35a23bbcca1b2542b2bdff8c563ab56ae08c623 Mon Sep 17 00:00:00 2001 From: Mathias Baumann Date: Mon, 11 Nov 2019 17:09:59 +0100 Subject: [PATCH 4/6] Add ``switch (..)` to style checker --- liblangutil/Exceptions.cpp | 2 +- libsolidity/analysis/ControlFlowBuilder.cpp | 2 +- libsolidity/analysis/ReferencesResolver.cpp | 2 +- libsolidity/ast/AST.h | 2 +- libsolidity/ast/ASTEnums.h | 2 +- libsolidity/ast/Types.cpp | 4 ++-- libsolidity/parsing/Parser.cpp | 4 ++-- libyul/Utilities.cpp | 2 +- scripts/check_style.sh | 2 +- 9 files changed, 11 insertions(+), 11 deletions(-) diff --git a/liblangutil/Exceptions.cpp b/liblangutil/Exceptions.cpp index 4e68dfa5b..4fd411b6e 100644 --- a/liblangutil/Exceptions.cpp +++ b/liblangutil/Exceptions.cpp @@ -29,7 +29,7 @@ using namespace langutil; Error::Error(Type _type, SourceLocation const& _location, string const& _description): m_type(_type) { - switch(m_type) + switch (m_type) { case Type::DeclarationError: m_typeName = "DeclarationError"; diff --git a/libsolidity/analysis/ControlFlowBuilder.cpp b/libsolidity/analysis/ControlFlowBuilder.cpp index fb766eea9..6bafc4caa 100644 --- a/libsolidity/analysis/ControlFlowBuilder.cpp +++ b/libsolidity/analysis/ControlFlowBuilder.cpp @@ -49,7 +49,7 @@ bool ControlFlowBuilder::visit(BinaryOperation const& _operation) { solAssert(!!m_currentNode, ""); - switch(_operation.getOperator()) + switch (_operation.getOperator()) { case Token::Or: case Token::And: diff --git a/libsolidity/analysis/ReferencesResolver.cpp b/libsolidity/analysis/ReferencesResolver.cpp index e9a10bb35..cb6471020 100644 --- a/libsolidity/analysis/ReferencesResolver.cpp +++ b/libsolidity/analysis/ReferencesResolver.cpp @@ -126,7 +126,7 @@ bool ReferencesResolver::visit(ElementaryTypeName const& _typeName) { // for non-address types this was already caught by the parser solAssert(_typeName.annotation().type->category() == Type::Category::Address, ""); - switch(*_typeName.stateMutability()) + switch (*_typeName.stateMutability()) { case StateMutability::Payable: _typeName.annotation().type = TypeProvider::payableAddress(); diff --git a/libsolidity/ast/AST.h b/libsolidity/ast/AST.h index 3ae78e44e..b86b28bc6 100644 --- a/libsolidity/ast/AST.h +++ b/libsolidity/ast/AST.h @@ -187,7 +187,7 @@ public: static std::string visibilityToString(Declaration::Visibility _visibility) { - switch(_visibility) + switch (_visibility) { case Declaration::Visibility::Public: return "public"; diff --git a/libsolidity/ast/ASTEnums.h b/libsolidity/ast/ASTEnums.h index a1a36efbd..11e539a8c 100644 --- a/libsolidity/ast/ASTEnums.h +++ b/libsolidity/ast/ASTEnums.h @@ -36,7 +36,7 @@ enum class StateMutability { Pure, View, NonPayable, Payable }; inline std::string stateMutabilityToString(StateMutability const& _stateMutability) { - switch(_stateMutability) + switch (_stateMutability) { case StateMutability::Pure: return "pure"; diff --git a/libsolidity/ast/Types.cpp b/libsolidity/ast/Types.cpp index 65c10d9ce..6739f4914 100644 --- a/libsolidity/ast/Types.cpp +++ b/libsolidity/ast/Types.cpp @@ -658,7 +658,7 @@ BoolResult FixedPointType::isExplicitlyConvertibleTo(Type const& _convertTo) con TypeResult FixedPointType::unaryOperatorResult(Token _operator) const { - switch(_operator) + switch (_operator) { case Token::Delete: // "delete" is ok for all fixed types @@ -2846,7 +2846,7 @@ unsigned FunctionType::sizeOnStack() const unsigned size = 0; - switch(kind) + switch (kind) { case Kind::External: case Kind::DelegateCall: diff --git a/libsolidity/parsing/Parser.cpp b/libsolidity/parsing/Parser.cpp index ad63ba505..f1145ee83 100644 --- a/libsolidity/parsing/Parser.cpp +++ b/libsolidity/parsing/Parser.cpp @@ -241,7 +241,7 @@ ASTPointer Parser::parseImportDirective() ContractDefinition::ContractKind Parser::parseContractKind() { ContractDefinition::ContractKind kind; - switch(m_scanner->currentToken()) + switch (m_scanner->currentToken()) { case Token::Interface: kind = ContractDefinition::ContractKind::Interface; @@ -388,7 +388,7 @@ StateMutability Parser::parseStateMutability() { StateMutability stateMutability(StateMutability::NonPayable); Token token = m_scanner->currentToken(); - switch(token) + switch (token) { case Token::Payable: stateMutability = StateMutability::Payable; diff --git a/libyul/Utilities.cpp b/libyul/Utilities.cpp index a5a2859c8..a9958716f 100644 --- a/libyul/Utilities.cpp +++ b/libyul/Utilities.cpp @@ -113,7 +113,7 @@ u256 yul::valueOfBoolLiteral(Literal const& _literal) u256 yul::valueOfLiteral(Literal const& _literal) { - switch(_literal.kind) + switch (_literal.kind) { case LiteralKind::Number: return valueOfNumberLiteral(_literal); diff --git a/scripts/check_style.sh b/scripts/check_style.sh index e4f31a1f6..340aba47e 100755 --- a/scripts/check_style.sh +++ b/scripts/check_style.sh @@ -17,7 +17,7 @@ fi FORMATERROR=$( ( - git grep -nIE "\<(if|for|while)\(" -- '*.h' '*.cpp' # no space after "if", "for" or "while" + git grep -nIE "\<(if|for|while|switch)\(" -- '*.h' '*.cpp' # no space after "if", "for", "while" or "switch" git grep -nIE "\\s*\([^=]*\>\s:\s.*\)" -- '*.h' '*.cpp' # no space before range based for-loop git grep -nIE "\\s*\(.*\)\s*\{\s*$" -- '*.h' '*.cpp' # "{\n" on same line as "if" / "for" git grep -nIE "[,\(<]\s*const " -- '*.h' '*.cpp' # const on left side of type From b323134ef08324a015199e1c9661ed801de095a2 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 11 Nov 2019 16:59:28 +0100 Subject: [PATCH 5/6] [SMTChecker] Update test expectations for z3 4.8.6 --- .../invariants/loop_array_for.sol | 5 ++-- ...e_loop_array_assignment_storage_memory.sol | 23 ------------------- ..._loop_array_assignment_storage_storage.sol | 6 +++-- 3 files changed, 7 insertions(+), 27 deletions(-) delete mode 100644 test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol b/test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol index 1bd8c7517..7169b444e 100644 --- a/test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol +++ b/test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol @@ -7,10 +7,11 @@ contract Simple { for (i = 0; i < n; ++i) a[i] = i; require(n > 1); - // Assertion is safe but current solver version cannot solve it. + // Assertion is safe but current solver version times out. // Keep test for next solver release. assert(a[n-1] > a[n-2]); } } // ---- -// Warning: (267-290): Assertion violation happens here +// Warning: (261-284): Error trying to invoke SMT solver. +// Warning: (261-284): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol deleted file mode 100644 index 6cb6cd6d9..000000000 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol +++ /dev/null @@ -1,23 +0,0 @@ -pragma experimental SMTChecker; - -contract LoopFor2 { - uint[] b; - uint[] c; - - function testUnboundedForLoop(uint n) public { - b[0] = 900; - uint[] memory a = b; - require(n > 0 && n < 100); - uint i; - while (i < n) { - b[i] = i + 1; - c[i] = b[i]; - ++i; - } - assert(b[0] == c[0]); - assert(a[0] == 900); - assert(b[0] == 900); - } -} -// ---- -// Warning: (312-331): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol index 7670ddb6d..92d1ded3e 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol @@ -14,11 +14,13 @@ contract LoopFor2 { c[i] = b[i]; ++i; } + // Fails as false positive. assert(b[0] == c[0]); assert(a[0] == 900); assert(b[0] == 900); } } // ---- -// Warning: (290-309): Assertion violation happens here -// Warning: (313-332): Assertion violation happens here +// Warning: (296-316): Assertion violation happens here +// Warning: (320-339): Assertion violation happens here +// Warning: (343-362): Assertion violation happens here From 999d8c6bb8d546ceb6cf0c98a8dc80d9e949ba2c Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 11 Nov 2019 18:48:20 +0100 Subject: [PATCH 6/6] Extend CircleCI MaxOS cache keys --- .circleci/config.yml | 8 ++++---- .circleci/osx_install_dependencies.sh | 14 +++++++------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index a35ef3b7c..939610467 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -431,12 +431,12 @@ jobs: - checkout - restore_cache: keys: - - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }} + - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }} - run: name: Install build dependencies command: ./.circleci/osx_install_dependencies.sh - save_cache: - key: dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }} + key: dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }} paths: - /usr/local/bin - /usr/local/sbin @@ -459,7 +459,7 @@ jobs: - checkout - restore_cache: keys: - - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }} + - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }} - attach_workspace: at: build - run: *run_soltest @@ -475,7 +475,7 @@ jobs: - checkout - restore_cache: keys: - - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }} + - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }} - attach_workspace: at: build - run: *run_cmdline_tests diff --git a/.circleci/osx_install_dependencies.sh b/.circleci/osx_install_dependencies.sh index 99c447e0f..22e14af7e 100755 --- a/.circleci/osx_install_dependencies.sh +++ b/.circleci/osx_install_dependencies.sh @@ -43,13 +43,13 @@ then ./scripts/install_obsolete_jsoncpp_1_7_4.sh # z3 - wget https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-osx-10.14.2.zip - unzip z3-4.8.5-x64-osx-10.14.2.zip - rm -f z3-4.8.5-x64-osx-10.14.2.zip - cp z3-4.8.5-x64-osx-10.14.2/bin/libz3.a /usr/local/lib - cp z3-4.8.5-x64-osx-10.14.2/bin/z3 /usr/local/bin - cp z3-4.8.5-x64-osx-10.14.2/include/* /usr/local/include - rm -rf z3-4.8.5-x64-osx-10.14.2 + wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.6/z3-4.8.6-x64-osx-10.14.6.zip + unzip z3-4.8.6-x64-osx-10.14.6.zip + rm -f z3-4.8.6-x64-osx-10.14.6.zip + cp z3-4.8.6-x64-osx-10.14.6/bin/libz3.a /usr/local/lib + cp z3-4.8.6-x64-osx-10.14.6/bin/z3 /usr/local/bin + cp z3-4.8.6-x64-osx-10.14.6/include/* /usr/local/include + rm -rf z3-4.8.6-x64-osx-10.14.6 # evmone wget https://github.com/ethereum/evmone/releases/download/v0.1.0/evmone-0.1.0-darwin-x86_64.tar.gz