Merge remote-tracking branch 'origin/develop' into breaking

libsolidity/analysis/ContractLevelChecker.cpp

@@ -450,7 +450,7 @@ void ContractLevelChecker::checkLibraryRequirements(ContractDefinition const& _c
 
 void ContractLevelChecker::checkBaseABICompatibility(ContractDefinition const& _contract)
 {
-	if (_contract.sourceUnit().annotation().experimentalFeatures.count(ExperimentalFeature::ABIEncoderV2))
+	if (*_contract.sourceUnit().annotation().useABICoderV2)
 		return;
 
 	if (_contract.isLibrary())
@@ -469,7 +469,7 @@ void ContractLevelChecker::checkBaseABICompatibility(ContractDefinition const& _
 	{
 		solAssert(func.second->hasDeclaration(), "Function has no declaration?!");
 
-		if (!func.second->declaration().sourceUnit().annotation().experimentalFeatures.count(ExperimentalFeature::ABIEncoderV2))
+		if (!*func.second->declaration().sourceUnit().annotation().useABICoderV2)
 			continue;
 
 		auto const& currentLoc = func.second->declaration().location();
@@ -489,9 +489,9 @@ void ContractLevelChecker::checkBaseABICompatibility(ContractDefinition const& _
 			errors,
 			std::string("Contract \"") +
 			_contract.name() +
-			"\" does not use ABIEncoderV2 but wants to inherit from a contract " +
+			"\" does not use ABI coder v2 but wants to inherit from a contract " +
 			"which uses types that require it. " +
-			"Use \"pragma experimental ABIEncoderV2;\" for the inheriting contract as well to enable the feature."
+			"Use \"pragma abicoder v2;\" for the inheriting contract as well to enable the feature."
 		);
 
 }

libsolidity/analysis/SyntaxChecker.cpp

@@ -73,6 +73,8 @@ void SyntaxChecker::endVisit(SourceUnit const& _sourceUnit)
 		// when reporting the warning, print the source name only
 		m_errorReporter.warning(3420_error, {-1, -1, _sourceUnit.location().source}, errorString);
 	}
+	if (!m_sourceUnit->annotation().useABICoderV2.set())
+		m_sourceUnit->annotation().useABICoderV2 = false;
 	m_sourceUnit = nullptr;
 }
 
@@ -113,9 +115,45 @@ bool SyntaxChecker::visit(PragmaDirective const& _pragma)
 				m_sourceUnit->annotation().experimentalFeatures.insert(feature);
 				if (!ExperimentalFeatureWithoutWarning.count(feature))
 					m_errorReporter.warning(2264_error, _pragma.location(), "Experimental features are turned on. Do not use experimental features on live deployments.");
+
+				if (feature == ExperimentalFeature::ABIEncoderV2)
+				{
+					if (m_sourceUnit->annotation().useABICoderV2.set())
+					{
+						if (!*m_sourceUnit->annotation().useABICoderV2)
+							m_errorReporter.syntaxError(
+								8273_error,
+								_pragma.location(),
+								"ABI coder v1 has already been selected through \"pragma abicoder v1\"."
+							);
+					}
+					else
+						m_sourceUnit->annotation().useABICoderV2 = true;
+				}
 			}
 		}
 	}
+	else if (_pragma.literals()[0] == "abicoder")
+	{
+		solAssert(m_sourceUnit, "");
+		if (
+			_pragma.literals().size() != 2 ||
+			!set<string>{"v1", "v2"}.count(_pragma.literals()[1])
+		)
+			m_errorReporter.syntaxError(
+				2745_error,
+				_pragma.location(),
+				"Expected either \"pragma abicoder v1\" or \"pragma abicoder v2\"."
+			);
+		else if (m_sourceUnit->annotation().useABICoderV2.set())
+			m_errorReporter.syntaxError(
+				3845_error,
+				_pragma.location(),
+				"ABI coder has already been selected for this source unit."
+			);
+		else
+			m_sourceUnit->annotation().useABICoderV2 = (_pragma.literals()[1] == "v2");
+	}
 	else if (_pragma.literals()[0] == "solidity")
 	{
 		vector<Token> tokens(_pragma.tokens().begin() + 1, _pragma.tokens().end());
@@ -135,6 +173,7 @@ bool SyntaxChecker::visit(PragmaDirective const& _pragma)
 	}
 	else
 		m_errorReporter.syntaxError(4936_error, _pragma.location(), "Unknown pragma \"" + _pragma.literals()[0] + "\"");
+
 	return true;
 }
 

libsolidity/analysis/SyntaxChecker.h

@@ -39,6 +39,7 @@ namespace solidity::frontend
  *  - issues deprecation warnings for unary '+'
  *  - issues deprecation warning for throw
  *  - whether the msize instruction is used and the Yul optimizer is enabled at the same time.
+ *  - selection of the ABI coder through pragmas.
  */
 class SyntaxChecker: private ASTConstVisitor
 {

libsolidity/analysis/TypeChecker.cpp

@@ -398,13 +398,13 @@ bool TypeChecker::visit(FunctionDefinition const& _function)
 				m_errorReporter.typeError(4103_error, _var.location(), message);
 			}
 			else if (
-				!experimentalFeatureActive(ExperimentalFeature::ABIEncoderV2) &&
+				!useABICoderV2() &&
 				!typeSupportedByOldABIEncoder(*type(_var), _function.libraryFunction())
 			)
 			{
 				string message =
-					"This type is only supported in ABIEncoderV2. "
-					"Use \"pragma experimental ABIEncoderV2;\" to enable the feature.";
+					"This type is only supported in ABI coder v2. "
+					"Use \"pragma abicoder v2;\" to enable the feature.";
 				if (_function.isConstructor())
 					message +=
 						" Alternatively, make the contract abstract and supply the "
@@ -570,7 +570,7 @@ bool TypeChecker::visit(VariableDeclaration const& _variable)
 	else if (_variable.visibility() >= Visibility::Public)
 	{
 		FunctionType getter(_variable);
-		if (!experimentalFeatureActive(ExperimentalFeature::ABIEncoderV2))
+		if (!useABICoderV2())
 		{
 			vector<string> unsupportedTypes;
 			for (auto const& param: getter.parameterTypes() + getter.returnParameterTypes())
@@ -580,9 +580,9 @@ bool TypeChecker::visit(VariableDeclaration const& _variable)
 				m_errorReporter.typeError(
 					2763_error,
 					_variable.location(),
-					"The following types are only supported for getters in ABIEncoderV2: " +
+					"The following types are only supported for getters in ABI coder v2: " +
 					joinHumanReadable(unsupportedTypes) +
-					". Either remove \"public\" or use \"pragma experimental ABIEncoderV2;\" to enable the feature."
+					". Either remove \"public\" or use \"pragma abicoder v2;\" to enable the feature."
 				);
 		}
 		if (!getter.interfaceFunctionType())
@@ -695,14 +695,14 @@ bool TypeChecker::visit(EventDefinition const& _eventDef)
 		if (!type(*var)->interfaceType(false))
 			m_errorReporter.typeError(3417_error, var->location(), "Internal or recursive type is not allowed as event parameter type.");
 		if (
-			!experimentalFeatureActive(ExperimentalFeature::ABIEncoderV2) &&
+			!useABICoderV2() &&
 			!typeSupportedByOldABIEncoder(*type(*var), false /* isLibrary */)
 		)
 			m_errorReporter.typeError(
 				3061_error,
 				var->location(),
-				"This type is only supported in ABIEncoderV2. "
-				"Use \"pragma experimental ABIEncoderV2;\" to enable the feature."
+				"This type is only supported in ABI coder v2. "
+				"Use \"pragma abicoder v2;\" to enable the feature."
 			);
 	}
 	if (_eventDef.isAnonymous() && numIndexed > 4)
@@ -1900,7 +1900,7 @@ void TypeChecker::typeCheckABIEncodeFunctions(
 	bool const isPacked = _functionType->kind() == FunctionType::Kind::ABIEncodePacked;
 	solAssert(_functionType->padArguments() != isPacked, "ABI function with unexpected padding");
 
-	bool const abiEncoderV2 = experimentalFeatureActive(ExperimentalFeature::ABIEncoderV2);
+	bool const abiEncoderV2 = useABICoderV2();
 
 	// Check for named arguments
 	if (!_functionCall.names().empty())
@@ -2192,7 +2192,7 @@ void TypeChecker::typeCheckFunctionGeneralChecks(
 		_functionType->kind() == FunctionType::Kind::Creation ||
 		_functionType->kind() == FunctionType::Kind::Event;
 
-	if (callRequiresABIEncoding && !experimentalFeatureActive(ExperimentalFeature::ABIEncoderV2))
+	if (callRequiresABIEncoding && !useABICoderV2())
 	{
 		solAssert(!isVariadic, "");
 		solAssert(parameterTypes.size() == arguments.size(), "");
@@ -2208,8 +2208,8 @@ void TypeChecker::typeCheckFunctionGeneralChecks(
 					2443_error,
 					paramArgMap[i]->location(),
 					"The type of this parameter, " + parameterTypes[i]->toString(true) + ", "
-					"is only supported in ABIEncoderV2. "
-					"Use \"pragma experimental ABIEncoderV2;\" to enable the feature."
+					"is only supported in ABI coder v2. "
+					"Use \"pragma abicoder v2;\" to enable the feature."
 				);
 		}
 
@@ -2222,8 +2222,8 @@ void TypeChecker::typeCheckFunctionGeneralChecks(
 					2428_error,
 					_functionCall.location(),
 					"The type of return parameter " + toString(i + 1) + ", " + returnParameterTypes[i]->toString(true) + ", "
-					"is only supported in ABIEncoderV2. "
-					"Use \"pragma experimental ABIEncoderV2;\" to enable the feature."
+					"is only supported in ABI coder v2. "
+					"Use \"pragma abicoder v2;\" to enable the feature."
 				);
 		}
 	}
@@ -2340,7 +2340,7 @@ bool TypeChecker::visit(FunctionCall const& _functionCall)
 		{
 			returnTypes = typeCheckABIDecodeAndRetrieveReturnType(
 				_functionCall,
-				experimentalFeatureActive(ExperimentalFeature::ABIEncoderV2)
+				useABICoderV2()
 			);
 			break;
 		}
@@ -3414,10 +3414,11 @@ void TypeChecker::requireLValue(Expression const& _expression, bool _ordinaryAss
 	m_errorReporter.typeError(errorId, _expression.location(), description);
 }
 
-bool TypeChecker::experimentalFeatureActive(ExperimentalFeature _feature) const
+bool TypeChecker::useABICoderV2() const
 {
 	solAssert(m_currentSourceUnit, "");
 	if (m_currentContract)
 		solAssert(m_currentSourceUnit == &m_currentContract->sourceUnit(), "");
-	return m_currentSourceUnit->annotation().experimentalFeatures.count(_feature);
+	return *m_currentSourceUnit->annotation().useABICoderV2;
+
 }

libsolidity/analysis/TypeChecker.h

@@ -168,7 +168,7 @@ private:
 	/// Runs type checks on @a _expression to infer its type and then checks that it is an LValue.
 	void requireLValue(Expression const& _expression, bool _ordinaryAssignment);
 
-	bool experimentalFeatureActive(ExperimentalFeature _feature) const;
+	bool useABICoderV2() const;
 
 	/// @returns the current scope that can have function or type definitions.
 	/// This is either a contract or a source unit.

libsolidity/ast/AST.cpp

@@ -84,16 +84,6 @@ TypePointer ImportDirective::type() const
 	return TypeProvider::module(*annotation().sourceUnit);
 }
 
-vector<VariableDeclaration const*> ContractDefinition::stateVariablesIncludingInherited() const
-{
-	vector<VariableDeclaration const*> stateVars;
-	for (auto const& contract: annotation().linearizedBaseContracts)
-		for (auto var: contract->stateVariables())
-			if (*contract == *this || var->isVisibleInDerivedContracts())
-				stateVars.push_back(var);
-	return stateVars;
-}
-
 bool ContractDefinition::derivesFrom(ContractDefinition const& _base) const
 {
 	return util::contains(annotation().linearizedBaseContracts, &_base);

libsolidity/ast/AST.h

@@ -500,7 +500,6 @@ public:
 	std::vector<StructDefinition const*> definedStructs() const { return filteredNodes<StructDefinition>(m_subNodes); }
 	std::vector<EnumDefinition const*> definedEnums() const { return filteredNodes<EnumDefinition>(m_subNodes); }
 	std::vector<VariableDeclaration const*> stateVariables() const { return filteredNodes<VariableDeclaration>(m_subNodes); }
-	std::vector<VariableDeclaration const*> stateVariablesIncludingInherited() const;
 	std::vector<ModifierDefinition const*> functionModifiers() const { return filteredNodes<ModifierDefinition>(m_subNodes); }
 	std::vector<FunctionDefinition const*> definedFunctions() const { return filteredNodes<FunctionDefinition>(m_subNodes); }
 	std::vector<EventDefinition const*> events() const { return filteredNodes<EventDefinition>(m_subNodes); }

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;
+	SetOnce<bool> useABICoderV2;
 };
 
 struct ScopableAnnotation

libsolidity/codegen/ArrayUtils.cpp

@@ -1172,7 +1172,7 @@ void ArrayUtils::accessCallDataArrayElement(ArrayType const& _arrayType, bool _d
 			if (
 				!_arrayType.isByteArray() &&
 				_arrayType.baseType()->storageBytes() < 32 &&
-				m_context.experimentalFeatureActive(ExperimentalFeature::ABIEncoderV2)
+				m_context.useABICoderV2()
 			)
 			{
 				m_context << u256(32);

libsolidity/codegen/CompilerContext.h

@@ -77,11 +77,8 @@ public:
 
 	langutil::EVMVersion const& evmVersion() const { return m_evmVersion; }
 
-	/// Update currently enabled set of experimental features.
-	void setExperimentalFeatures(std::set<ExperimentalFeature> const& _features) { m_experimentalFeatures = _features; }
-	std::set<ExperimentalFeature> const& experimentalFeaturesActive() const { return m_experimentalFeatures; }
-	/// @returns true if the given feature is enabled.
-	bool experimentalFeatureActive(ExperimentalFeature _feature) const { return m_experimentalFeatures.count(_feature); }
+	void setUseABICoderV2(bool _value) { m_useABICoderV2 = _value; }
+	bool useABICoderV2() const { return m_useABICoderV2; }
 
 	void addStateVariable(VariableDeclaration const& _declaration, u256 const& _storageOffset, unsigned _byteOffset);
 	void addImmutable(VariableDeclaration const& _declaration);
@@ -365,8 +362,7 @@ private:
 	/// Version of the EVM to compile against.
 	langutil::EVMVersion m_evmVersion;
 	RevertStrings const m_revertStrings;
-	/// Activated experimental features.
-	std::set<ExperimentalFeature> m_experimentalFeatures;
+	bool m_useABICoderV2 = false;
 	/// Other already compiled contracts to be used in contract creation calls.
 	std::map<ContractDefinition const*, std::shared_ptr<Compiler const>> m_otherCompilers;
 	/// Storage offsets of state variables

libsolidity/codegen/CompilerUtils.cpp

@@ -230,7 +230,7 @@ void CompilerUtils::storeInMemoryDynamic(Type const& _type, bool _padToWordBound
 void CompilerUtils::abiDecode(TypePointers const& _typeParameters, bool _fromMemory)
 {
 	/// Stack: <source_offset> <length>
-	if (m_context.experimentalFeatureActive(ExperimentalFeature::ABIEncoderV2))
+	if (m_context.useABICoderV2())
 	{
 		// Use the new Yul-based decoding function
 		auto stackHeightBefore = m_context.stackHeight();
@@ -412,7 +412,7 @@ void CompilerUtils::encodeToMemory(
 )
 {
 	// stack: <v1> <v2> ... <vn> <mem>
-	bool const encoderV2 = m_context.experimentalFeatureActive(ExperimentalFeature::ABIEncoderV2);
+	bool const encoderV2 = m_context.useABICoderV2();
 	TypePointers targetTypes = _targetTypes.empty() ? _givenTypes : _targetTypes;
 	solAssert(targetTypes.size() == _givenTypes.size(), "");
 	for (TypePointer& t: targetTypes)

libsolidity/codegen/ContractCompiler.cpp

@@ -127,7 +127,7 @@ void ContractCompiler::initializeContext(
 	map<ContractDefinition const*, shared_ptr<Compiler const>> const& _otherCompilers
 )
 {
-	m_context.setExperimentalFeatures(_contract.sourceUnit().annotation().experimentalFeatures);
+	m_context.setUseABICoderV2(*_contract.sourceUnit().annotation().useABICoderV2);
 	m_context.setOtherCompilers(_otherCompilers);
 	m_context.setMostDerivedContract(_contract);
 	if (m_runtimeCompiler)
@@ -1349,13 +1349,13 @@ void ContractCompiler::appendModifierOrFunctionCode()
 	{
 		m_context.setArithmetic(Arithmetic::Checked);
 
-		std::set<ExperimentalFeature> experimentalFeaturesOutside = m_context.experimentalFeaturesActive();
-		m_context.setExperimentalFeatures(codeBlock->sourceUnit().annotation().experimentalFeatures);
+		bool coderV2Outside = m_context.useABICoderV2();
+		m_context.setUseABICoderV2(*codeBlock->sourceUnit().annotation().useABICoderV2);
 
 		m_returnTags.emplace_back(m_context.newTag(), m_context.stackHeight());
 		codeBlock->accept(*this);
 
-		m_context.setExperimentalFeatures(experimentalFeaturesOutside);
+		m_context.setUseABICoderV2(coderV2Outside);
 
 		solAssert(!m_returnTags.empty(), "");
 		m_context << m_returnTags.back().first;

libsolidity/codegen/ExpressionCompiler.cpp

@@ -1676,7 +1676,7 @@ bool ExpressionCompiler::visit(MemberAccess const& _memberAccess)
 				{
 					solAssert(memberType->calldataEncodedSize() > 0, "");
 					solAssert(memberType->storageBytes() <= 32, "");
-					if (memberType->storageBytes() < 32 && m_context.experimentalFeatureActive(ExperimentalFeature::ABIEncoderV2))
+					if (memberType->storageBytes() < 32 && m_context.useABICoderV2())
 					{
 						m_context << u256(32);
 						CompilerUtils(m_context).abiDecodeV2({memberType}, false);
@@ -2522,7 +2522,7 @@ void ExpressionCompiler::appendExternalFunctionCall(
 		// memory pointer), but kept references to the return data for
 		// (statically-sized) arrays
 		bool needToUpdateFreeMemoryPtr = false;
-		if (dynamicReturnSize || m_context.experimentalFeatureActive(ExperimentalFeature::ABIEncoderV2))
+		if (dynamicReturnSize || m_context.useABICoderV2())
 			needToUpdateFreeMemoryPtr = true;
 		else
 			for (auto const& retType: returnTypes)

libsolidity/codegen/YulUtilFunctions.cpp

@@ -1556,13 +1556,14 @@ string YulUtilFunctions::clearStorageStructFunction(StructType const& _type)
 	});
 }
 
-string YulUtilFunctions::copyArrayToStorage(ArrayType const& _fromType, ArrayType const& _toType)
+string YulUtilFunctions::copyArrayToStorageFunction(ArrayType const& _fromType, ArrayType const& _toType)
 {
 	solAssert(
 		*_fromType.copyForLocation(_toType.location(), _toType.isPointer()) == dynamic_cast<ReferenceType const&>(_toType),
 		""
 	);
-	solUnimplementedAssert(!_fromType.isByteArray(), "");
+	if (_fromType.isByteArray())
+		return copyByteArrayToStorageFunction(_fromType, _toType);
 	solUnimplementedAssert(!_fromType.dataStoredIn(DataLocation::Storage), "");
 
 	string functionName = "copy_array_to_storage_from_" + _fromType.identifier() + "_to_" + _toType.identifier();
@@ -1655,6 +1656,84 @@ string YulUtilFunctions::copyArrayToStorage(ArrayType const& _fromType, ArrayTyp
 	});
 }
 
+
+string YulUtilFunctions::copyByteArrayToStorageFunction(ArrayType const& _fromType, ArrayType const& _toType)
+{
+	solAssert(
+		*_fromType.copyForLocation(_toType.location(), _toType.isPointer()) == dynamic_cast<ReferenceType const&>(_toType),
+		""
+	);
+	solAssert(_fromType.isByteArray(), "");
+	solAssert(_toType.isByteArray(), "");
+	solUnimplementedAssert(!_fromType.dataStoredIn(DataLocation::Storage), "");
+
+	string functionName = "copy_byte_array_to_storage_from_" + _fromType.identifier() + "_to_" + _toType.identifier();
+	return m_functionCollector.createFunction(functionName, [&](){
+		Whiskers templ(R"(
+			function <functionName>(slot, src<?fromCalldata>, len</fromCalldata>) {
+				let newLen := <arrayLength>(src<?fromCalldata>, len</fromCalldata>)
+				// Make sure array length is sane
+				if gt(newLen, 0xffffffffffffffff) { <panic>() }
+
+				let oldLen := <byteArrayLength>(sload(slot))
+
+				<?fromMemory>
+					src := add(src, 0x20)
+				</fromMemory>
+
+				// This is not needed in all branches.
+				let dstDataArea
+				if or(gt(oldLen, 31), gt(newLen, 31)) {
+					dstDataArea := <dstDataLocation>(slot)
+				}
+
+				if gt(oldLen, 31) {
+					// potentially truncate data
+					let deleteStart := add(dstDataArea, div(add(newLen, 31), 32))
+					if lt(newLen, 32) { deleteStart := dstDataArea }
+					<clearStorageRange>(deleteStart, add(dstDataArea, div(add(oldLen, 31), 32)))
+				}
+				switch gt(newLen, 31)
+				case 1 {
+					let loopEnd := and(newLen, not(0x1f))
+					let dstPtr := dstDataArea
+					let i := 0
+					for { } lt(i, loopEnd) { i := add(i, 32) } {
+						sstore(dstPtr, <readFromCalldataOrMemory>(add(src, i)))
+						dstPtr := add(dstPtr, 1)
+					}
+					if lt(loopEnd, newLen) {
+						let lastValue := <readFromCalldataOrMemory>(add(src, i))
+						sstore(dstPtr, <maskBytes>(lastValue, and(newLen, 0x1f)))
+					}
+					sstore(slot, add(mul(newLen, 2), 1))
+				}
+				default {
+					let value := 0
+					if newLen {
+						value := <readFromCalldataOrMemory>(src)
+					}
+					sstore(slot, <byteArrayCombineShort>(value, newLen))
+				}
+			}
+		)");
+		templ("functionName", functionName);
+		bool fromCalldata = _fromType.dataStoredIn(DataLocation::CallData);
+		templ("fromMemory", _fromType.dataStoredIn(DataLocation::Memory));
+		templ("fromCalldata", fromCalldata);
+		templ("arrayLength", arrayLengthFunction(_fromType));
+		templ("panic", panicFunction(PanicCode::ResourceError));
+		templ("byteArrayLength", extractByteArrayLengthFunction());
+		templ("dstDataLocation", arrayDataAreaFunction(_toType));
+		templ("clearStorageRange", clearStorageRangeFunction(*_toType.baseType()));
+		templ("readFromCalldataOrMemory", readFromMemoryOrCalldata(*TypeProvider::uint256(), fromCalldata));
+		templ("maskBytes", maskBytesFunctionDynamic());
+		templ("byteArrayCombineShort", shortByteArrayEncodeUsedAreaSetLengthFunction());
+
+		return templ.render();
+	});
+}
+
 string YulUtilFunctions::arrayConvertLengthToSize(ArrayType const& _type)
 {
 	string functionName = "array_convert_length_to_size_" + _type.identifier();
@@ -2207,8 +2286,9 @@ string YulUtilFunctions::updateStorageValueFunction(
 			solAssert(_toType.storageBytes() > 0, "Invalid storage bytes size.");
 
 			return Whiskers(R"(
-				function <functionName>(slot, <offset>value) {
-					sstore(slot, <update>(sload(slot), <offset><prepare>(value)))
+				function <functionName>(slot, <offset><fromValues>) {
+					let <toValues> := <convert>(<fromValues>)
+					sstore(slot, <update>(sload(slot), <offset><prepare>(<toValues>)))
 				}
 
 			)")
@@ -2219,6 +2299,9 @@ string YulUtilFunctions::updateStorageValueFunction(
 					updateByteSliceFunctionDynamic(_toType.storageBytes())
 			)
 			("offset", _offset.has_value() ? "" : "offset, ")
+			("convert", conversionFunction(_fromType, _toType))
+			("fromValues", suffixedVariableNameList("value_", 0, _fromType.sizeOnStack()))
+			("toValues", suffixedVariableNameList("convertedValue_", 0, _toType.sizeOnStack()))
 			("prepare", prepareStoreFunction(_toType))
 			.render();
 		}
@@ -2248,7 +2331,7 @@ string YulUtilFunctions::updateStorageValueFunction(
 				)");
 				templ("functionName", functionName);
 				templ("value", suffixedVariableNameList("value_", 0, _fromType.sizeOnStack()));
-				templ("copyArrayToStorage", copyArrayToStorage(
+				templ("copyArrayToStorage", copyArrayToStorageFunction(
 					dynamic_cast<ArrayType const&>(_fromType),
 					dynamic_cast<ArrayType const&>(_toType)
 				));
@@ -2478,9 +2561,16 @@ string YulUtilFunctions::cleanupFromStorageFunction(Type const& _type, bool _spl
 				return templ.render();
 			}
 
+		bool leftAligned = false;
+		if (
+			_type.category() != Type::Category::Function ||
+			dynamic_cast<FunctionType const&>(_type).kind() == FunctionType::Kind::External
+		)
+			leftAligned = _type.leftAligned();
+
 		if (storageBytes == 32)
 			templ("cleaned", "value");
-		else if (_type.leftAligned())
+		else if (leftAligned)
 			templ("cleaned", shiftLeftFunction(256 - 8 * storageBytes) + "(value)");
 		else
 			templ("cleaned", "and(value, " + toCompactHexWithPrefix((u256(1) << (8 * storageBytes)) - 1) + ")");
@@ -2491,7 +2581,8 @@ string YulUtilFunctions::cleanupFromStorageFunction(Type const& _type, bool _spl
 
 string YulUtilFunctions::prepareStoreFunction(Type const& _type)
 {
-	solUnimplementedAssert(_type.category() != Type::Category::Function, "");
+	if (_type.category() == Type::Category::Function)
+		solUnimplementedAssert(dynamic_cast<FunctionType const&>(_type).kind() == FunctionType::Kind::Internal, "");
 
 	string functionName = "prepare_store_" + _type.identifier();
 	return m_functionCollector.createFunction(functionName, [&]() {
@@ -2718,12 +2809,13 @@ string YulUtilFunctions::conversionFunction(Type const& _from, Type const& _to)
 			_to.identifier();
 		return m_functionCollector.createFunction(functionName, [&]() {
 			return Whiskers(R"(
-				function <functionName>(addr, functionId) -> outAddr, outFunctionId {
-					outAddr := addr
+				function <functionName>(<?external>addr, </external>functionId) -> <?external>outAddr, </external>outFunctionId {
+					<?external>outAddr := addr</external>
 					outFunctionId := functionId
 				}
 			)")
 			("functionName", functionName)
+			("external", fromType.kind() == FunctionType::Kind::External)
 			.render();
 		});
 	}

libsolidity/codegen/YulUtilFunctions.h

@@ -205,7 +205,11 @@ public:
 
 	/// @returns the name of a function that will copy array from calldata or memory to storage
 	/// signature (to_slot, from_ptr) ->
-	std::string copyArrayToStorage(ArrayType const& _fromType, ArrayType const& _toType);
+	std::string copyArrayToStorageFunction(ArrayType const& _fromType, ArrayType const& _toType);
+
+	/// @returns the name of a function that will copy a byte array from calldata or memory to storage
+	/// signature (to_slot, from_ptr) ->
+	std::string copyByteArrayToStorageFunction(ArrayType const& _fromType, ArrayType const& _toType);
 
 	/// Returns the name of a function that will convert a given length to the
 	/// size in memory (number of storage slots or calldata/memory bytes) it

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -425,7 +425,7 @@ bool IRGeneratorForStatements::visit(TupleExpression const& _tuple)
 				"(" <<
 				("add(" + mpos + ", " + to_string(i * arrayType.memoryStride()) + ")") <<
 				", " <<
-				converted.name() <<
+				converted.commaSeparatedList() <<
 				")\n";
 		}
 	}
@@ -2543,47 +2543,50 @@ string IRGeneratorForStatements::binaryOperation(
 		!TokenTraits::isShiftOp(_operator),
 		"Have to use specific shift operation function for shifts."
 	);
-	if (IntegerType const* type = dynamic_cast<IntegerType const*>(&_type))
+	string fun;
+	if (TokenTraits::isBitOp(_operator))
 	{
-		string fun;
+		solAssert(
+			_type.category() == Type::Category::Integer ||
+			_type.category() == Type::Category::FixedBytes,
+		"");
+		switch (_operator)
+		{
+		case Token::BitOr: fun = "or"; break;
+		case Token::BitXor: fun = "xor"; break;
+		case Token::BitAnd: fun = "and"; break;
+		default: break;
+		}
+	}
+	else if (TokenTraits::isArithmeticOp(_operator))
+	{
+		IntegerType const* type = dynamic_cast<IntegerType const*>(&_type);
+		solAssert(type, "");
 		bool checked = m_context.arithmetic() == Arithmetic::Checked;
 		switch (_operator)
 		{
-			case Token::Add:
-				fun = checked ? m_utils.overflowCheckedIntAddFunction(*type) : m_utils.wrappingIntAddFunction(*type);
-				break;
-			case Token::Sub:
-				fun = checked ? m_utils.overflowCheckedIntSubFunction(*type) : m_utils.wrappingIntSubFunction(*type);
-				break;
-			case Token::Mul:
-				fun = checked ? m_utils.overflowCheckedIntMulFunction(*type) : m_utils.wrappingIntMulFunction(*type);
-				break;
-			case Token::Div:
-				fun = checked ?  m_utils.overflowCheckedIntDivFunction(*type) : m_utils.wrappingIntDivFunction(*type);
-				break;
-			case Token::Mod:
-				fun = m_utils.intModFunction(*type);
-				break;
-			case Token::BitOr:
-				fun = "or";
-				break;
-			case Token::BitXor:
-				fun = "xor";
-				break;
-			case Token::BitAnd:
-				fun = "and";
-				break;
-			default:
-				break;
+		case Token::Add:
+			fun = checked ? m_utils.overflowCheckedIntAddFunction(*type) : m_utils.wrappingIntAddFunction(*type);
+			break;
+		case Token::Sub:
+			fun = checked ? m_utils.overflowCheckedIntSubFunction(*type) : m_utils.wrappingIntSubFunction(*type);
+			break;
+		case Token::Mul:
+			fun = checked ? m_utils.overflowCheckedIntMulFunction(*type) : m_utils.wrappingIntMulFunction(*type);
+			break;
+		case Token::Div:
+			fun = checked ? m_utils.overflowCheckedIntDivFunction(*type) : m_utils.wrappingIntDivFunction(*type);
+			break;
+		case Token::Mod:
+			fun = m_utils.intModFunction(*type);
+			break;
+		default:
+			break;
 		}
-
-		solUnimplementedAssert(!fun.empty(), "");
-		return fun + "(" + _left + ", " + _right + ")\n";
 	}
-	else
-		solUnimplementedAssert(false, "");
 
-	return {};
+	solUnimplementedAssert(!fun.empty(), "Type: " + _type.toString());
+	return fun + "(" + _left + ", " + _right + ")\n";
 }
 
 std::string IRGeneratorForStatements::shiftOperation(

libsolidity/formal/CHC.cpp

@@ -134,7 +134,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
 
 	setCurrentBlock(*m_constructorSummaryPredicate);
 
-	addAssertVerificationTarget(m_currentContract, m_currentBlock, smtutil::Expression(true), errorFlag().currentValue());
+	m_queryPlaceholders[&_contract].push_back({smtutil::Expression(true), errorFlag().currentValue(), m_currentBlock});
 	connectBlocks(m_currentBlock, interface(), errorFlag().currentValue() == 0);
 
 	SMTEncoder::endVisit(_contract);
@@ -231,16 +231,14 @@ void CHC::endVisit(FunctionDefinition const& _function)
 			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);
-				addAssertVerificationTarget(&_function, ifacePre, txConstraints && sum, assertionError);
+				m_queryPlaceholders[&_function].push_back({txConstraints && sum, assertionError, ifacePre});
 				connectBlocks(ifacePre, iface, txConstraints && sum && (assertionError == 0));
 			}
 		}
@@ -512,30 +510,15 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 
 	solAssert(m_currentContract, "");
 	solAssert(m_currentFunction, "");
-	if (m_currentFunction->isConstructor())
-		m_functionAssertions[m_currentContract].insert(&_funCall);
-	else
-		m_functionAssertions[m_currentFunction].insert(&_funCall);
-
-	auto previousError = errorFlag().currentValue();
-	errorFlag().increaseIndex();
-
-	connectBlocks(
-		m_currentBlock,
-		m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction),
-		currentPathConditions() && !m_context.expression(*args.front())->currentValue() && (
-			errorFlag().currentValue() == newErrorId(_funCall)
-		)
-	);
-
-	m_context.addAssertion(errorFlag().currentValue() == previousError);
+	auto errorCondition = !m_context.expression(*args.front())->currentValue();
+	verificationTargetEncountered(&_funCall, VerificationTarget::Type::Assert, errorCondition);
 }
 
 void CHC::visitAddMulMod(FunctionCall const& _funCall)
 {
 	solAssert(_funCall.arguments().at(2), "");
 
-	addVerificationTarget(_funCall, VerificationTarget::Type::DivByZero, expr(*_funCall.arguments().at(2)) == 0);
+	verificationTargetEncountered(&_funCall, VerificationTarget::Type::DivByZero, expr(*_funCall.arguments().at(2)) == 0);
 
 	SMTEncoder::visitAddMulMod(_funCall);
 }
@@ -634,7 +617,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
 	auto symbArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
 	solAssert(symbArray, "");
 
-	addVerificationTarget(_arrayPop, VerificationTarget::Type::PopEmptyArray, symbArray->length() <= 0);
+	verificationTargetEncountered(&_arrayPop, VerificationTarget::Type::PopEmptyArray, symbArray->length() <= 0);
 }
 
 pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
@@ -646,7 +629,7 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 )
 {
 	if (_op == Token::Mod || _op == Token::Div)
-		addVerificationTarget(_expression, VerificationTarget::Type::DivByZero, _right == 0);
+		verificationTargetEncountered(&_expression, VerificationTarget::Type::DivByZero, _right == 0);
 
 	auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
 
@@ -662,16 +645,16 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 		return values;
 
 	if (_op == Token::Div)
-		addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
+		verificationTargetEncountered(&_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
 	else if (intType->isSigned())
 	{
-		addVerificationTarget(_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
-		addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
+		verificationTargetEncountered(&_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
+		verificationTargetEncountered(&_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
 	}
 	else if (_op == Token::Sub)
-		addVerificationTarget(_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
+		verificationTargetEncountered(&_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
 	else if (_op == Token::Add || _op == Token::Mul)
-		addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
+		verificationTargetEncountered(&_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
 	else
 		solAssert(false, "");
 	return values;
@@ -679,11 +662,11 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 
 void CHC::resetSourceAnalysis()
 {
-	m_verificationTargets.clear();
 	m_safeTargets.clear();
 	m_unsafeTargets.clear();
-	m_functionAssertions.clear();
-	m_errorIds.clear();
+	m_functionTargetIds.clear();
+	m_verificationTargets.clear();
+	m_queryPlaceholders.clear();
 	m_callGraph.clear();
 	m_summaries.clear();
 	m_interfaces.clear();
@@ -713,6 +696,7 @@ void CHC::resetSourceAnalysis()
 	}
 
 	m_context.clear();
+	m_context.resetUniqueId();
 	m_context.setAssertionAccumulation(false);
 }
 
@@ -759,15 +743,15 @@ void CHC::setCurrentBlock(Predicate const& _block)
 	m_currentBlock = predicate(_block);
 }
 
-set<frontend::Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTNode const* _txRoot)
+set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot)
 {
-	set<Expression const*, IdCompare> assertions;
+	set<unsigned> verificationTargetsIds;
 	solidity::util::BreadthFirstSearch<ASTNode const*>{{_txRoot}}.run([&](auto const* function, auto&& _addChild) {
-		assertions.insert(m_functionAssertions[function].begin(), m_functionAssertions[function].end());
+		verificationTargetsIds.insert(m_functionTargetIds[function].begin(), m_functionTargetIds[function].end());
 		for (auto const* called: m_callGraph[function])
 		_addChild(called);
 	});
-	return assertions;
+	return verificationTargetsIds;
 }
 
 SortPointer CHC::sort(FunctionDefinition const& _function)
@@ -1101,186 +1085,171 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression c
 	return {result, cex};
 }
 
-void CHC::addVerificationTarget(
-	ASTNode const* _scope,
+void CHC::verificationTargetEncountered(
+	ASTNode const* const _errorNode,
 	VerificationTarget::Type _type,
-	smtutil::Expression _from,
-	smtutil::Expression _constraints,
-	smtutil::Expression _errorId
+	smtutil::Expression const& _errorCondition
 )
 {
 	solAssert(m_currentContract || m_currentFunction, "");
-	SourceUnit const* source = nullptr;
-	if (m_currentContract)
-		source = sourceUnitContaining(*m_currentContract);
-	else
-		source = sourceUnitContaining(*m_currentFunction);
+	SourceUnit const* source = m_currentContract ? sourceUnitContaining(*m_currentContract) : sourceUnitContaining(*m_currentFunction);
 	solAssert(source, "");
 	if (!source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		return;
 
-	m_verificationTargets[_scope].push_back(CHCVerificationTarget{{_type, _from, _constraints}, _errorId});
-}
-
-void CHC::addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _errorId)
-{
-	solAssert(m_currentContract, "");
-
-	if (!m_currentFunction || m_currentFunction->isConstructor())
-		addVerificationTarget(_scope, _type, summary(*m_currentContract), smtutil::Expression(true), _errorId);
+	bool scopeIsFunction = m_currentFunction && !m_currentFunction->isConstructor();
+	auto errorId = newErrorId();
+	solAssert(m_verificationTargets.count(errorId) == 0, "Error ID is not unique!");
+	m_verificationTargets.emplace(errorId, CHCVerificationTarget{{_type, _errorCondition, smtutil::Expression(true)}, errorId, _errorNode});
+	if (scopeIsFunction)
+		m_functionTargetIds[m_currentFunction].push_back(errorId);
 	else
-	{
-		auto iface = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
-		auto sum = summary(*m_currentFunction);
-		addVerificationTarget(_scope, _type, iface, sum, _errorId);
-	}
-}
-
-void CHC::addVerificationTarget(frontend::Expression const& _scope, VerificationTarget::Type _type, smtutil::Expression const& _target)
-{
+		m_functionTargetIds[m_currentContract].push_back(errorId);
 	auto previousError = errorFlag().currentValue();
 	errorFlag().increaseIndex();
-	addVerificationTarget(&_scope, _type, errorFlag().currentValue());
 
-	m_context.addAssertion(
-		errorFlag().currentValue() == previousError ||
-		(_target && errorFlag().currentValue() == newErrorId(_scope))
+	// create an error edge to the summary
+	connectBlocks(
+		m_currentBlock,
+		scopeIsFunction ? summary(*m_currentFunction) : summary(*m_currentContract),
+		currentPathConditions() && _errorCondition && errorFlag().currentValue() == errorId
 	);
-}
 
-void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId)
-{
-	addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId);
+	m_context.addAssertion(errorFlag().currentValue() == previousError);
 }
 
 void CHC::checkVerificationTargets()
 {
-	for (auto const& [scope, targets]: m_verificationTargets)
+	// The verification conditions have been collected per function where they have been encountered (m_verificationTargets).
+	// Also, all possible contexts in which an external function can be called has been recorded (m_queryPlaceholders).
+	// Here we combine every context in which an external function can be called with all possible verification conditions
+	// in its call graph. Each such combination forms a unique verification target.
+	vector<CHCVerificationTarget> verificationTargets;
+	for (auto const& [function, placeholders]: m_queryPlaceholders)
 	{
-		for (size_t i = 0; i < targets.size(); ++i)
-		{
-			auto const& target = targets[i];
-
-			if (target.type == VerificationTarget::Type::Assert)
-				checkAssertTarget(scope, target);
-			else
+		auto functionTargets = transactionVerificationTargetsIds(function);
+		for (auto const& placeholder: placeholders)
+			for (unsigned id: functionTargets)
 			{
-				string satMsg;
-				string satMsgUnderflow;
-				string satMsgOverflow;
-				string unknownMsg;
-				ErrorId errorReporterId;
-				ErrorId underflowErrorId = 3944_error;
-				ErrorId overflowErrorId = 4984_error;
+				auto const& target = m_verificationTargets.at(id);
+				verificationTargets.push_back(CHCVerificationTarget{
+					{target.type, placeholder.fromPredicate, placeholder.constraints && placeholder.errorExpression == target.errorId},
+					target.errorId,
+					target.errorNode
+				});
+			}
+	}
 
-				if (target.type == VerificationTarget::Type::PopEmptyArray)
-				{
-					solAssert(dynamic_cast<FunctionCall const*>(scope), "");
-					satMsg = "Empty array \"pop\" detected here.";
-					unknownMsg = "Empty array \"pop\" might happen here.";
-					errorReporterId = 2529_error;
-				}
-				else if (
-					target.type == VerificationTarget::Type::Underflow ||
-					target.type == VerificationTarget::Type::Overflow
-				)
-				{
-					auto const* expr = dynamic_cast<Expression const*>(scope);
-					solAssert(expr, "");
-					auto const* intType = dynamic_cast<IntegerType const*>(expr->annotation().type);
-					if (!intType)
-						intType = TypeProvider::uint256();
+	set<unsigned> checkedErrorIds;
+	for (auto const& target: verificationTargets)
+	{
+		string errorType;
+		ErrorId errorReporterId;
 
-					satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")";
-					satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")";
-					if (target.type == VerificationTarget::Type::Underflow)
-					{
-						satMsg = satMsgUnderflow + " happens here.";
-						unknownMsg = satMsgUnderflow + " might happen here.";
-						errorReporterId = underflowErrorId;
-					}
-					else if (target.type == VerificationTarget::Type::Overflow)
-					{
-						satMsg = satMsgOverflow + " happens here.";
-						unknownMsg = satMsgOverflow + " might happen here.";
-						errorReporterId = overflowErrorId;
-					}
-				}
-				else if (target.type == VerificationTarget::Type::DivByZero)
-				{
-					satMsg = "Division by zero happens here.";
-					unknownMsg = "Division by zero might happen here.";
-					errorReporterId = 4281_error;
-				}
-				else
-					solAssert(false, "");
+		if (target.type == VerificationTarget::Type::PopEmptyArray)
+		{
+			solAssert(dynamic_cast<FunctionCall const*>(target.errorNode), "");
+			errorType = "Empty array \"pop\"";
+			errorReporterId = 2529_error;
+		}
+		else if (
+			target.type == VerificationTarget::Type::Underflow ||
+			target.type == VerificationTarget::Type::Overflow
+		)
+		{
+			auto const* expr = dynamic_cast<Expression const*>(target.errorNode);
+			solAssert(expr, "");
+			auto const* intType = dynamic_cast<IntegerType const*>(expr->annotation().type);
+			if (!intType)
+				intType = TypeProvider::uint256();
 
-				auto it = m_errorIds.find(scope->id());
-				solAssert(it != m_errorIds.end(), "");
-				solAssert(i < it->second.size(), "");
-				unsigned errorId = it->second[i];
-
-				checkAndReportTarget(scope, target, errorId, errorReporterId, satMsg, unknownMsg);
+			if (target.type == VerificationTarget::Type::Underflow)
+			{
+				errorType = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")";
+				errorReporterId = 3944_error;
+			}
+			else if (target.type == VerificationTarget::Type::Overflow)
+			{
+				errorType = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")";
+				errorReporterId = 4984_error;
 			}
 		}
-	}
-}
+		else if (target.type == VerificationTarget::Type::DivByZero)
+		{
+			errorType = "Division by zero";
+			errorReporterId = 4281_error;
+		}
+		else if (target.type == VerificationTarget::Type::Assert)
+		{
+			errorType = "Assertion violation";
+			errorReporterId = 6328_error;
+		}
+		else
+			solAssert(false, "");
 
-void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const& _target)
-{
-	solAssert(_target.type == VerificationTarget::Type::Assert, "");
-	auto assertions = transactionAssertions(_scope);
-	for (auto const* assertion: assertions)
-	{
-		auto it = m_errorIds.find(assertion->id());
-		solAssert(it != m_errorIds.end(), "");
-		solAssert(!it->second.empty(), "");
-		unsigned errorId = it->second[0];
-
-		checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here.", "Assertion violation might happen here.");
+		checkAndReportTarget(target, errorReporterId, errorType + " happens here.", errorType + " might happen here.");
+		checkedErrorIds.insert(target.errorId);
 	}
+
+	// There can be targets in internal functions that are not reachable from the external interface.
+	// These are safe by definition and are not even checked by the CHC engine, but this information
+	// must still be reported safe by the BMC engine.
+	set<unsigned> allErrorIds;
+	for (auto const& entry: m_functionTargetIds)
+		for (unsigned id: entry.second)
+			allErrorIds.insert(id);
+
+	set<unsigned> unreachableErrorIds;
+	set_difference(
+		allErrorIds.begin(),
+		allErrorIds.end(),
+		checkedErrorIds.begin(),
+		checkedErrorIds.end(),
+		inserter(unreachableErrorIds, unreachableErrorIds.begin())
+	);
+	for (auto id: unreachableErrorIds)
+		m_safeTargets[m_verificationTargets.at(id).errorNode].insert(m_verificationTargets.at(id).type);
 }
 
 void CHC::checkAndReportTarget(
-	ASTNode const* _scope,
 	CHCVerificationTarget const& _target,
-	unsigned _errorId,
 	ErrorId _errorReporterId,
 	string _satMsg,
 	string _unknownMsg
 )
 {
-	if (m_unsafeTargets.count(_scope) && m_unsafeTargets.at(_scope).count(_target.type))
+	if (m_unsafeTargets.count(_target.errorNode) && m_unsafeTargets.at(_target.errorNode).count(_target.type))
 		return;
 
 	createErrorBlock();
-	connectBlocks(_target.value, error(), _target.constraints && (_target.errorId == _errorId));
-	auto const& [result, model] = query(error(), _scope->location());
+	connectBlocks(_target.value, error(), _target.constraints);
+	auto const& location = _target.errorNode->location();
+	auto const& [result, model] = query(error(), location);
 	if (result == CheckResult::UNSATISFIABLE)
-		m_safeTargets[_scope].insert(_target.type);
+		m_safeTargets[_target.errorNode].insert(_target.type);
 	else if (result == CheckResult::SATISFIABLE)
 	{
 		solAssert(!_satMsg.empty(), "");
-		m_unsafeTargets[_scope].insert(_target.type);
+		m_unsafeTargets[_target.errorNode].insert(_target.type);
 		auto cex = generateCounterexample(model, error().name);
 		if (cex)
 			m_outerErrorReporter.warning(
 				_errorReporterId,
-				_scope->location(),
+				location,
 				"CHC: " + _satMsg,
 				SecondarySourceLocation().append("Counterexample:\n" + *cex, SourceLocation{})
 			);
 		else
 			m_outerErrorReporter.warning(
 				_errorReporterId,
-				_scope->location(),
+				location,
 				"CHC: " + _satMsg
 			);
 	}
 	else if (!_unknownMsg.empty())
 		m_outerErrorReporter.warning(
 			_errorReporterId,
-			_scope->location(),
+			location,
 			"CHC: " + _unknownMsg
 		);
 }
@@ -1431,14 +1400,13 @@ string CHC::contractSuffix(ContractDefinition const& _contract)
 	return _contract.name() + "_" + to_string(_contract.id());
 }
 
-unsigned CHC::newErrorId(frontend::Expression const& _expr)
+unsigned CHC::newErrorId()
 {
 	unsigned errorId = m_context.newUniqueId();
 	// We need to make sure the error id is not zero,
 	// because error id zero actually means no error in the CHC encoding.
 	if (errorId == 0)
 		errorId = m_context.newUniqueId();
-	m_errorIds[_expr.id()].push_back(errorId);
 	return errorId;
 }
 

libsolidity/formal/CHC.h

@@ -114,7 +114,7 @@ private:
 	void eraseKnowledge();
 	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
 	void setCurrentBlock(Predicate const& _block);
-	std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
+	std::set<unsigned> transactionVerificationTargetsIds(ASTNode const* _txRoot);
 	//@}
 
 	/// Sort helpers.
@@ -181,19 +181,14 @@ private:
 	/// @returns <false, model> otherwise.
 	std::pair<smtutil::CheckResult, smtutil::CHCSolverInterface::CexGraph> query(smtutil::Expression const& _query, langutil::SourceLocation const& _location);
 
-	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
-	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _errorId);
-	void addVerificationTarget(frontend::Expression const& _scope, VerificationTarget::Type _type, smtutil::Expression const& _target);
-	void addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
+	void verificationTargetEncountered(ASTNode const* const _errorNode, VerificationTarget::Type _type, smtutil::Expression const& _errorCondition);
 
 	void checkVerificationTargets();
 	// Forward declaration. Definition is below.
 	struct CHCVerificationTarget;
 	void checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const& _target);
 	void checkAndReportTarget(
-		ASTNode const* _scope,
 		CHCVerificationTarget const& _target,
-		unsigned _errorId,
 		langutil::ErrorId _errorReporterId,
 		std::string _satMsg,
 		std::string _unknownMsg = ""
@@ -234,7 +229,7 @@ private:
 
 	/// @returns a new unique error id associated with _expr and stores
 	/// it into m_errorIds.
-	unsigned newErrorId(Expression const& _expr);
+	unsigned newErrorId();
 
 	smt::SymbolicState& state();
 	smt::SymbolicIntVariable& errorFlag();
@@ -275,12 +270,30 @@ private:
 	//@{
 	struct CHCVerificationTarget: VerificationTarget
 	{
-		smtutil::Expression errorId;
+		unsigned const errorId;
+		ASTNode const* const errorNode;
 	};
 
-	/// Verification targets corresponding to ASTNodes. There can be multiple targets for a single ASTNode,
-	/// e.g., divByZero and Overflow for signed division.
-	std::map<ASTNode const*, std::vector<CHCVerificationTarget>, IdCompare> m_verificationTargets;
+	/// Query placeholder stores information necessary to create the final query edge in the CHC system.
+	/// It is combined with the unique error id (and error type) to create a complete Verification Target.
+	struct CHCQueryPlaceholder
+	{
+		smtutil::Expression const constraints;
+		smtutil::Expression const errorExpression;
+		smtutil::Expression const fromPredicate;
+	};
+
+	/// Query placeholders for constructors, if the key has type ContractDefinition*,
+	/// or external functions, if the key has type FunctionDefinition*.
+	/// A placeholder is created for each possible context of a function (e.g. multiple contracts in contract inheritance hierarchy).
+	std::map<ASTNode const*, std::vector<CHCQueryPlaceholder>, IdCompare> m_queryPlaceholders;
+
+	/// Records verification conditions IDs per function encountered during an analysis of that function.
+	/// The key is the ASTNode of the function where the verification condition has been encountered,
+	/// or the ASTNode of the contract if the verification condition happens inside an implicit constructor.
+	std::map<ASTNode const*, std::vector<unsigned>, IdCompare> m_functionTargetIds;
+	/// Helper mapping unique IDs to actual verification targets.
+	std::map<unsigned, CHCVerificationTarget> m_verificationTargets;
 
 	/// Targets proven safe.
 	std::map<ASTNode const*, std::set<VerificationTarget::Type>> m_safeTargets;
@@ -294,12 +307,6 @@ private:
 
 	std::map<ASTNode const*, std::set<ASTNode const*, IdCompare>, IdCompare> m_callGraph;
 
-	std::map<ASTNode const*, std::set<Expression const*>, IdCompare> m_functionAssertions;
-
-	/// Maps ASTNode ids to error ids.
-	/// There can be multiple errorIds associated with a single ASTNode.
-	std::map<unsigned, std::vector<unsigned>> m_errorIds;
-
 	/// The current block.
 	smtutil::Expression m_currentBlock = smtutil::Expression(true);
 

libsolidity/formal/EncodingContext.cpp

@@ -33,7 +33,6 @@ EncodingContext::EncodingContext():
 void EncodingContext::reset()
 {
 	resetAllVariables();
-	resetUniqueId();
 	m_expressions.clear();
 	m_globalContext.clear();
 	m_state.reset();

libsolidity/formal/SMTEncoder.cpp

@@ -348,6 +348,36 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
 
 }
 
+bool SMTEncoder::visit(Assignment const& _assignment)
+{
+	auto const& left = _assignment.leftHandSide();
+	auto const& right = _assignment.rightHandSide();
+
+	if (auto const* memberAccess = isEmptyPush(left))
+	{
+		right.accept(*this);
+		left.accept(*this);
+
+		auto const& memberExpr = memberAccess->expression();
+		auto& symbArray = dynamic_cast<smt::SymbolicArrayVariable&>(*m_context.expression(memberExpr));
+		smtutil::Expression oldElements = symbArray.elements();
+		smtutil::Expression length = symbArray.length();
+		symbArray.increaseIndex();
+		m_context.addAssertion(symbArray.elements() == smtutil::Expression::store(
+			oldElements,
+			length - 1,
+			expr(right)
+		));
+		m_context.addAssertion(symbArray.length() == length);
+
+		arrayPushPopAssign(memberExpr, symbArray.currentValue());
+		defineExpr(_assignment, expr(left));
+		return false;
+	}
+
+	return true;
+}
+
 void SMTEncoder::endVisit(Assignment const& _assignment)
 {
 	createExpr(_assignment);
@@ -355,6 +385,9 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 	Token op = _assignment.assignmentOperator();
 	solAssert(TokenTraits::isAssignmentOp(op), "");
 
+	if (isEmptyPush(_assignment.leftHandSide()))
+		return;
+
 	if (!smt::isSupportedType(*_assignment.annotation().type))
 	{
 		// Give it a new index anyway to keep the SSA scheme sound.
@@ -465,14 +498,14 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 			assignment(*decl, newValue);
 		}
 		else if (
-			dynamic_cast<IndexAccess const*>(&_op.subExpression()) ||
-			dynamic_cast<MemberAccess const*>(&_op.subExpression())
+			dynamic_cast<IndexAccess const*>(subExpr) ||
+			dynamic_cast<MemberAccess const*>(subExpr)
 		)
 		{
 			auto innerValue = expr(*subExpr);
 			auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
 			defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
-			indexOrMemberAssignment(_op.subExpression(), newValue);
+			indexOrMemberAssignment(*subExpr, newValue);
 		}
 		else
 			m_errorReporter.warning(
@@ -502,11 +535,12 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 			symbVar->increaseIndex();
 			m_context.setZeroValue(*symbVar);
 			if (
-				dynamic_cast<IndexAccess const*>(&_op.subExpression()) ||
-				dynamic_cast<MemberAccess const*>(&_op.subExpression())
+				dynamic_cast<IndexAccess const*>(subExpr) ||
+				dynamic_cast<MemberAccess const*>(subExpr)
 			)
-				indexOrMemberAssignment(_op.subExpression(), symbVar->currentValue());
-			else
+				indexOrMemberAssignment(*subExpr, symbVar->currentValue());
+			// Empty push added a zero value anyway, so no need to delete extra.
+			else if (!isEmptyPush(*subExpr))
 				solAssert(false, "");
 		}
 		break;
@@ -1968,7 +2002,7 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
 
 void SMTEncoder::createStateVariables(ContractDefinition const& _contract)
 {
-	for (auto var: _contract.stateVariablesIncludingInherited())
+	for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
 		createVariable(*var);
 }
 
@@ -2252,7 +2286,7 @@ void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
 void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
 {
 	solAssert(_contract, "");
-	for (auto var: _contract->stateVariablesIncludingInherited())
+	for (auto var: stateVariablesIncludingInheritedAndPrivate(*_contract))
 		m_context.variable(*var)->resetIndex();
 	if (_function)
 	{
@@ -2309,7 +2343,7 @@ set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _nod
 	return m_variableUsage.touchedVariables(_node, callStack);
 }
 
-Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr)
+Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr) const
 {
 	if (auto const* identifier = dynamic_cast<Identifier const*>(&_expr))
 		return identifier->annotation().referencedDeclaration;
@@ -2318,7 +2352,7 @@ Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr)
 	return nullptr;
 }
 
-VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _expr)
+VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _expr) const
 {
 	// We do not use `expressionToDeclaration` here because we are not interested in
 	// struct.field, for example.
@@ -2331,6 +2365,20 @@ VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _e
 	return nullptr;
 }
 
+MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const
+{
+	if (
+		auto const* funCall = dynamic_cast<FunctionCall const*>(&_expr);
+		funCall && funCall->arguments().empty()
+	)
+	{
+		auto const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
+		if (funType.kind() == FunctionType::Kind::ArrayPush)
+			return &dynamic_cast<MemberAccess const&>(funCall->expression());
+	}
+	return nullptr;
+}
+
 string SMTEncoder::extraComment()
 {
 	string extra;

libsolidity/formal/SMTEncoder.h

@@ -90,6 +90,7 @@ protected:
 	bool visit(WhileStatement const&) override { return false; }
 	bool visit(ForStatement const&) override { return false; }
 	void endVisit(VariableDeclarationStatement const& _node) override;
+	bool visit(Assignment const& _node) override;
 	void endVisit(Assignment const& _node) override;
 	void endVisit(TupleExpression const& _node) override;
 	bool visit(UnaryOperation const& _node) override;
@@ -282,10 +283,14 @@ protected:
 
 	/// @returns the declaration referenced by _expr, if any,
 	/// and nullptr otherwise.
-	Declaration const* expressionToDeclaration(Expression const& _expr);
+	Declaration const* expressionToDeclaration(Expression const& _expr) const;
 
 	/// @returns the VariableDeclaration referenced by an Expression or nullptr.
-	VariableDeclaration const* identifierToVariable(Expression const& _expr);
+	VariableDeclaration const* identifierToVariable(Expression const& _expr) const;
+
+	/// @returns the MemberAccess <expression>.push if _expr is an empty array push call,
+	/// otherwise nullptr.
+	MemberAccess const* isEmptyPush(Expression const& _expr) const;
 
 	/// Creates symbolic expressions for the returned values
 	/// and set them as the components of the symbolic tuple.

libsolidity/formal/SymbolicVariables.cpp

@@ -332,12 +332,12 @@ smtutil::Expression SymbolicArrayVariable::valueAtIndex(unsigned _index) const
 	return m_pair.valueAtIndex(_index);
 }
 
-smtutil::Expression SymbolicArrayVariable::elements()
+smtutil::Expression SymbolicArrayVariable::elements() const
 {
 	return m_pair.component(0);
 }
 
-smtutil::Expression SymbolicArrayVariable::length()
+smtutil::Expression SymbolicArrayVariable::length() const
 {
 	return m_pair.component(1);
 }

libsolidity/formal/SymbolicVariables.h

@@ -260,8 +260,8 @@ public:
 	smtutil::Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); }
 	smtutil::Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); }
 	smtutil::Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); }
-	smtutil::Expression elements();
-	smtutil::Expression length();
+	smtutil::Expression elements() const;
+	smtutil::Expression length() const;
 
 	smtutil::SortPointer tupleSort() { return m_pair.sort(); }