Merge remote-tracking branch 'upstream/develop' into 0.7

.circleci/config.yml

@@ -114,6 +114,7 @@ defaults:
       root: build
       paths:
         - test/tools/ossfuzz/abiv2_proto_ossfuzz
+        - test/tools/ossfuzz/abiv2_isabelle_ossfuzz
         - test/tools/ossfuzz/const_opt_ossfuzz
         - test/tools/ossfuzz/solc_noopt_mutator_ossfuzz
         - test/tools/ossfuzz/solc_noopt_ossfuzz
@@ -863,9 +864,6 @@ jobs:
           name: External GnosisSafe tests
           command: |
             test/externalTests/gnosis.sh /tmp/workspace/soljson.js
-      # TODO: Re-enable notifications once this is running nightly rather than as a PR check
-      #- run: *gitter_notify_failure
-      #- run: *gitter_notify_success
 
   t_ems_compile_ext_gnosis_v2:
     docker:
@@ -896,9 +894,6 @@ jobs:
           name: External GnosisSafe v2 tests
           command: |
             test/externalTests/gnosis-v2.sh /tmp/workspace/soljson.js
-      # TODO: Re-enable notifications once this is running nightly rather than as a PR check
-      #- run: *gitter_notify_failure
-      #- run: *gitter_notify_success
 
   t_ems_compile_ext_zeppelin:
     docker:
@@ -928,9 +923,6 @@ jobs:
           name: External Zeppelin tests
           command: |
             test/externalTests/zeppelin.sh /tmp/workspace/soljson.js
-      # TODO: Re-enable notifications once this is running nightly rather than as a PR check
-      #- run: *gitter_notify_failure
-      #- run: *gitter_notify_success
 
   t_ems_compile_ext_colony:
     docker:
@@ -968,9 +960,8 @@ jobs:
           name: External ColonyNetworks tests
           command: |
             test/externalTests/colony.sh /tmp/workspace/soljson.js
-      # TODO: Re-enable notifications once this is running nightly rather than as a PR check
-      #- run: *gitter_notify_failure
-      #- run: *gitter_notify_success
+      - run: *gitter_notify_failure
+      - run: *gitter_notify_success
 
   t_ems_compile_ext_ens:
     docker:
@@ -1010,9 +1001,6 @@ jobs:
           name: External Ens compilation
           command: |
             test/externalTests/ens.sh /tmp/workspace/soljson.js
-      # TODO: Re-enable notifications once this is running nightly rather than as a PR check
-      #- run: *gitter_notify_failure
-      #- run: *gitter_notify_success
 
   b_win: &b_win
     executor:
@@ -1312,15 +1300,14 @@ workflows:
       - t_ubu_release_cli: *workflow_ubuntu2004_release
       - t_ubu_release_soltest: *workflow_ubuntu2004_release
 
-      # Emscripten build and selected tests
+      # Emscripten build and tests that take 15 minutes or less
       - b_ems: *workflow_trigger_on_tags
       - t_ems_solcjs: *workflow_emscripten
       - t_ems_compile_ext_colony: *workflow_emscripten
       - t_ems_compile_ext_gnosis: *workflow_emscripten
       - t_ems_compile_ext_gnosis_v2: *workflow_emscripten
       - t_ems_compile_ext_zeppelin: *workflow_emscripten
       - t_ems_compile_ext_ens: *workflow_emscripten
-      - t_ems_test_ext_colony: *workflow_emscripten
       # FIXME: Gnosis tests are pretty flaky right now. They often fail on CircleCI due to random ProviderError
       # and there are also other less frequent problems. See https://github.com/gnosis/safe-contracts/issues/216.
       #- t_ems_test_ext_gnosis: *workflow_emscripten
@@ -1370,6 +1357,10 @@ workflows:
       - t_ubu_asan_constantinople_clang: *workflow_ubuntu2004_asan_clang
       - t_ubu_asan_cli: *workflow_ubuntu2004_asan
 
+      # Emscripten build and tests that take more than 15 minutes to execute
+      - b_ems: *workflow_trigger_on_tags
+      - t_ems_test_ext_colony: *workflow_emscripten
+
       # solc-verify build and tests
       - b_ubu_sverif: *workflow_trigger_on_tags
       - t_ubu_sverif_bg: *workflow_sverif

Changelog.md

@@ -8,19 +8,19 @@ Language Features:
 
 Compiler Features:
  * Code Generator: Avoid memory allocation for default value if it is not used.
+ * SMTChecker: Report struct values in counterexamples from CHC engine.
+ * SMTChecker: Support early returns in the CHC engine.
+ * SMTChecker: Support getters.
  * SMTChecker: Support named arguments in function calls.
  * SMTChecker: Support struct constructor.
- * SMTChecker: Support getters.
- * SMTChecker: Support early returns in the CHC engine.
- * SMTChecker: Report struct values in counterexamples from CHC engine.
  * Standard-Json: Properly filter the requested output artifacts.
 
 Bugfixes:
  * Code generator: Do not pad empty string literals with a single 32-byte zero field in the ABI coder v1.
+ * SMTChecker: Fix cast string literals to byte arrays.
  * 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.
- * SMTChecker: Fix cast string literals to byte arrays.
  * Type Checker: ``super`` is not available in libraries.
  * 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.

libsolidity/ast/ASTAnnotations.h

@@ -94,6 +94,7 @@ struct SourceUnitAnnotation: ASTAnnotation
 	SetOnce<std::map<ASTString, std::vector<Declaration const*>>> exportedSymbols;
 	/// Experimental features.
 	std::set<ExperimentalFeature> experimentalFeatures;
+	/// Using the new ABI coder. Set to `false` if using ABI coder v1.
 	SetOnce<bool> useABICoderV2;
 };
 

libsolidity/formal/BMC.cpp

@@ -58,13 +58,18 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
-	m_solvedTargets = move(_solvedTargets);
-	m_context.setSolver(m_interface.get());
-	m_context.clear();
-	m_context.setAssertionAccumulation(true);
-	m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
+	/// This is currently used to abort analysis of SourceUnits
+	/// containing file level functions or constants.
+	if (SMTEncoder::analyze(_source))
+	{
+		m_solvedTargets = move(_solvedTargets);
+		m_context.setSolver(m_interface.get());
+		m_context.clear();
+		m_context.setAssertionAccumulation(true);
+		m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
 
-	_source.accept(*this);
+		_source.accept(*this);
+	}
 
 	solAssert(m_interface->solvers() > 0, "");
 	// If this check is true, Z3 and CVC4 are not available

libsolidity/formal/CHC.cpp

@@ -69,18 +69,23 @@ void CHC::analyze(SourceUnit const& _source)
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
-	resetSourceAnalysis();
-
-	set<SourceUnit const*, EncodingContext::IdCompare> sources;
-	sources.insert(&_source);
-	for (auto const& source: _source.referencedSourceUnits(true))
-		sources.insert(source);
-	for (auto const* source: sources)
-		defineInterfacesAndSummaries(*source);
-	for (auto const* source: sources)
-		source->accept(*this);
-
-	checkVerificationTargets();
+	/// This is currently used to abort analysis of SourceUnits
+	/// containing file level functions or constants.
+	if (SMTEncoder::analyze(_source))
+	{
+		resetSourceAnalysis();
+
+		set<SourceUnit const*, EncodingContext::IdCompare> sources;
+		sources.insert(&_source);
+		for (auto const& source: _source.referencedSourceUnits(true))
+			sources.insert(source);
+		for (auto const* source: sources)
+			defineInterfacesAndSummaries(*source);
+		for (auto const* source: sources)
+			source->accept(*this);
+
+		checkVerificationTargets();
+	}
 
 	bool ranSolver = true;
 #ifndef HAVE_Z3

libsolidity/formal/SMTEncoder.cpp

@@ -40,6 +40,38 @@ SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
 {
 }
 
+bool SMTEncoder::analyze(SourceUnit const& _source)
+{
+	set<SourceUnit const*, smt::EncodingContext::IdCompare> sources;
+	sources.insert(&_source);
+	for (auto const& source: _source.referencedSourceUnits(true))
+		sources.insert(source);
+
+	bool analysis = true;
+	for (auto source: sources)
+		for (auto node: source->nodes())
+			if (auto function = dynamic_pointer_cast<FunctionDefinition>(node))
+			{
+				m_errorReporter.warning(
+					6660_error,
+					function->location(),
+					"Model checker analysis was not possible because file level functions are not supported."
+				);
+				analysis = false;
+			}
+			else if (auto var = dynamic_pointer_cast<VariableDeclaration>(node))
+			{
+				m_errorReporter.warning(
+					8195_error,
+					var->location(),
+					"Model checker analysis was not possible because file level constants are not supported."
+				);
+				analysis = false;
+			}
+
+	return analysis;
+}
+
 bool SMTEncoder::visit(ContractDefinition const& _contract)
 {
 	solAssert(m_currentContract, "");

libsolidity/formal/SMTEncoder.h

@@ -52,6 +52,9 @@ class SMTEncoder: public ASTConstVisitor
 public:
 	SMTEncoder(smt::EncodingContext& _context);
 
+	/// @returns true if engine should proceed with analysis.
+	bool analyze(SourceUnit const& _sources);
+
 	/// @returns the leftmost identifier in a multi-d IndexAccess.
 	static Expression const* leftmostBase(IndexAccess const& _indexAccess);
 

libsolidity/interface/CompilerStack.cpp

@@ -1250,6 +1250,14 @@ void CompilerStack::generateIR(ContractDefinition const& _contract)
 	if (!compiledContract.yulIR.empty())
 		return;
 
+	if (!*_contract.sourceUnit().annotation().useABICoderV2)
+		m_errorReporter.warning(
+			2066_error,
+			_contract.location(),
+			"Contract requests the ABI coder v1, which is incompatible with the IR. "
+			"Using ABI coder v2 instead."
+		);
+
 	string dependenciesSource;
 	for (auto const* dependency: _contract.annotation().contractDependencies)
 		generateIR(*dependency);

libyul/CMakeLists.txt

@@ -1,4 +1,22 @@
+# This will re-generate the polyfill headers, if any file within libyul/backends/wasm/polyfill/ was modified.
+set_directory_properties(PROPERTY CMAKE_CONFIGURE_DEPENDS ${CMAKE_SOURCE_DIR}/libyul/backends/wasm/polyfill/)
+
+set(POLYFILLS Arithmetic Bitwise Comparison Conversion Interface Keccak Logical Memory)
+set(GENERATED_POLYFILL_HEADERS)
+foreach(polyfill IN LISTS POLYFILLS)
+	set(POLYFILL_FILE ${CMAKE_SOURCE_DIR}/libyul/backends/wasm/polyfill/${polyfill}.yul)
+	file(READ ${POLYFILL_FILE} EWASM_POLYFILL_CONTENT HEX)
+	string(REGEX MATCHALL ".." EWASM_POLYFILL_CONTENT "${EWASM_POLYFILL_CONTENT}")
+	string(REGEX REPLACE ";" ",\n\t0x" EWASM_POLYFILL_CONTENT "${EWASM_POLYFILL_CONTENT}")
+	set(EWASM_POLYFILL_CONTENT "0x${EWASM_POLYFILL_CONTENT}")
+	set(EWASM_POLYFILL_NAME ${polyfill})
+	configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/ewasm_polyfill.in" ${CMAKE_BINARY_DIR}/include/ewasmPolyfills/${polyfill}.h @ONLY)
+	list(APPEND GENERATED_POLYFILL_HEADERS ${CMAKE_BINARY_DIR}/include/ewasmPolyfills/${polyfill}.h)
+endforeach()
+
 add_library(yul
+	${GENERATED_POLYFILL_HEADERS}
+
 	AsmAnalysis.cpp
 	AsmAnalysis.h
 	AsmAnalysisInfo.h
@@ -61,14 +79,6 @@ add_library(yul
 	backends/wasm/WasmObjectCompiler.h
 	backends/wasm/WordSizeTransform.cpp
 	backends/wasm/WordSizeTransform.h
-	backends/wasm/polyfill/Arithmetic.yul
-	backends/wasm/polyfill/Bitwise.yul
-	backends/wasm/polyfill/Comparison.yul
-	backends/wasm/polyfill/Conversion.yul
-	backends/wasm/polyfill/Interface.yul
-	backends/wasm/polyfill/Keccak.yul
-	backends/wasm/polyfill/Logical.yul
-	backends/wasm/polyfill/Memory.yul
 	optimiser/ASTCopier.cpp
 	optimiser/ASTCopier.h
 	optimiser/ASTWalker.cpp
@@ -187,15 +197,4 @@ add_library(yul
 	optimiser/VarNameCleaner.h
 )
 
-set(POLYFILLS Arithmetic Bitwise Comparison Conversion Interface Keccak Logical Memory)
-foreach(polyfill IN LISTS POLYFILLS)
-	set(POLYFILL_FILE ${CMAKE_SOURCE_DIR}/libyul/backends/wasm/polyfill/${polyfill}.yul)
-	file(READ ${POLYFILL_FILE} EWASM_POLYFILL_CONTENT HEX)
-	string(REGEX MATCHALL ".." EWASM_POLYFILL_CONTENT "${EWASM_POLYFILL_CONTENT}")
-	string(REGEX REPLACE ";" ",\n\t0x" EWASM_POLYFILL_CONTENT "${EWASM_POLYFILL_CONTENT}")
-	set(EWASM_POLYFILL_CONTENT "0x${EWASM_POLYFILL_CONTENT}")
-	set(EWASM_POLYFILL_NAME ${polyfill})
-	configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/ewasm_polyfill.in" ${CMAKE_BINARY_DIR}/include/ewasmPolyfills/${polyfill}.h @ONLY)
-endforeach()
-
 target_link_libraries(yul PUBLIC evmasm solutil langutil smtutil)

scripts/error_codes.py

@@ -222,7 +222,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
 
     old_source_only_ids = {
         "1123", "1220", "1584", "1823",
-        "1988", "2657", "2800", "3356",
+        "1988", "2066", "2657", "2800", "3356",
         "3893", "3996", "4010", "4802",
         "5073", "5272", "5622", "7128",
         "7589", "7593", "7653", "8065", "8084", "8140",

test/cmdlineTests/exp_base_literal/input.sol

@@ -1,5 +1,6 @@
 // SPDX-License-Identifier: GPL-3.0
 pragma solidity > 0.7.1;
+pragma abicoder v2;
 
 contract C {
 	function f(uint a, uint b, uint c, uint d) public pure returns (uint, int, uint, uint) {