Merge pull request #8983 from ethereum/develop

Merge develop into breaking.

libsolidity/CMakeLists.txt

@@ -79,6 +79,8 @@ set(sources
 	codegen/ReturnInfo.cpp
 	codegen/YulUtilFunctions.h
 	codegen/YulUtilFunctions.cpp
+	codegen/ir/Common.cpp
+	codegen/ir/Common.h
 	codegen/ir/IRGenerator.cpp
 	codegen/ir/IRGenerator.h
 	codegen/ir/IRGeneratorForStatements.cpp

libsolidity/analysis/TypeChecker.cpp

@@ -455,7 +455,15 @@ bool TypeChecker::visit(VariableDeclaration const& _variable)
 		if (contractType->contractDefinition().isLibrary())
 			m_errorReporter.typeError(1273_error, _variable.location(), "The type of a variable cannot be a library.");
 	if (_variable.value())
-		expectType(*_variable.value(), *varType);
+	{
+		if (_variable.isStateVariable() && dynamic_cast<MappingType const*>(varType))
+		{
+			m_errorReporter.typeError(6280_error, _variable.location(), "Mappings cannot be assigned to.");
+			_variable.value()->accept(*this);
+		}
+		else
+			expectType(*_variable.value(), *varType);
+	}
 	if (_variable.isConstant())
 	{
 		if (!_variable.type()->isValueType())

libsolidity/ast/AST.cpp

@@ -153,10 +153,10 @@ FunctionDefinition const* ContractDefinition::receiveFunction() const
 
 vector<EventDefinition const*> const& ContractDefinition::interfaceEvents() const
 {
-	if (!m_interfaceEvents)
-	{
+	return m_interfaceEvents.init([&]{
 		set<string> eventsSeen;
-		m_interfaceEvents = make_unique<vector<EventDefinition const*>>();
+		vector<EventDefinition const*> interfaceEvents;
+
 		for (ContractDefinition const* contract: annotation().linearizedBaseContracts)
 			for (EventDefinition const* e: contract->events())
 			{
@@ -169,19 +169,20 @@ vector<EventDefinition const*> const& ContractDefinition::interfaceEvents() cons
 				if (eventsSeen.count(eventSignature) == 0)
 				{
 					eventsSeen.insert(eventSignature);
-					m_interfaceEvents->push_back(e);
+					interfaceEvents.push_back(e);
 				}
 			}
-	}
-	return *m_interfaceEvents;
+
+		return interfaceEvents;
+	});
 }
 
 vector<pair<util::FixedHash<4>, FunctionTypePointer>> const& ContractDefinition::interfaceFunctionList(bool _includeInheritedFunctions) const
 {
-	if (!m_interfaceFunctionList[_includeInheritedFunctions])
-	{
+	return m_interfaceFunctionList[_includeInheritedFunctions].init([&]{
 		set<string> signaturesSeen;
-		m_interfaceFunctionList[_includeInheritedFunctions] = make_unique<vector<pair<util::FixedHash<4>, FunctionTypePointer>>>();
+		vector<pair<util::FixedHash<4>, FunctionTypePointer>> interfaceFunctionList;
+
 		for (ContractDefinition const* contract: annotation().linearizedBaseContracts)
 		{
 			if (_includeInheritedFunctions == false && contract != this)
@@ -203,12 +204,13 @@ vector<pair<util::FixedHash<4>, FunctionTypePointer>> const& ContractDefinition:
 				{
 					signaturesSeen.insert(functionSignature);
 					util::FixedHash<4> hash(util::keccak256(functionSignature));
-					m_interfaceFunctionList[_includeInheritedFunctions]->emplace_back(hash, fun);
+					interfaceFunctionList.emplace_back(hash, fun);
 				}
 			}
 		}
-	}
-	return *m_interfaceFunctionList[_includeInheritedFunctions];
+
+		return interfaceFunctionList;
+	});
 }
 
 TypePointer ContractDefinition::type() const

libsolidity/ast/AST.h

@@ -31,6 +31,7 @@
 #include <liblangutil/SourceLocation.h>
 #include <libevmasm/Instruction.h>
 #include <libsolutil/FixedHash.h>
+#include <libsolutil/LazyInit.h>
 
 #include <boost/noncopyable.hpp>
 #include <json/json.h>
@@ -536,8 +537,8 @@ private:
 	ContractKind m_contractKind;
 	bool m_abstract{false};
 
-	mutable std::unique_ptr<std::vector<std::pair<util::FixedHash<4>, FunctionTypePointer>>> m_interfaceFunctionList[2];
-	mutable std::unique_ptr<std::vector<EventDefinition const*>> m_interfaceEvents;
+	util::LazyInit<std::vector<std::pair<util::FixedHash<4>, FunctionTypePointer>>> m_interfaceFunctionList[2];
+	util::LazyInit<std::vector<EventDefinition const*>> m_interfaceEvents;
 };
 
 class InheritanceSpecifier: public ASTNode

libsolidity/ast/Types.cpp

@@ -207,26 +207,31 @@ void MemberList::combine(MemberList const & _other)
 
 pair<u256, unsigned> const* MemberList::memberStorageOffset(string const& _name) const
 {
-	if (!m_storageOffsets)
-	{
-		TypePointers memberTypes;
-		memberTypes.reserve(m_memberTypes.size());
-		for (auto const& member: m_memberTypes)
-			memberTypes.push_back(member.type);
-		m_storageOffsets = std::make_unique<StorageOffsets>();
-		m_storageOffsets->computeOffsets(memberTypes);
-	}
+	StorageOffsets const& offsets = storageOffsets();
+
 	for (size_t index = 0; index < m_memberTypes.size(); ++index)
 		if (m_memberTypes[index].name == _name)
-			return m_storageOffsets->offset(index);
+			return offsets.offset(index);
 	return nullptr;
 }
 
 u256 const& MemberList::storageSize() const
 {
-	// trigger lazy computation
-	memberStorageOffset("");
-	return m_storageOffsets->storageSize();
+	return storageOffsets().storageSize();
+}
+
+StorageOffsets const& MemberList::storageOffsets() const {
+	return m_storageOffsets.init([&]{
+		TypePointers memberTypes;
+		memberTypes.reserve(m_memberTypes.size());
+		for (auto const& member: m_memberTypes)
+			memberTypes.push_back(member.type);
+
+		StorageOffsets storageOffsets;
+		storageOffsets.computeOffsets(memberTypes);
+
+		return storageOffsets;
+	});
 }
 
 /// Helper functions for type identifier

libsolidity/ast/Types.h

@@ -29,6 +29,7 @@
 
 #include <libsolutil/Common.h>
 #include <libsolutil/CommonIO.h>
+#include <libsolutil/LazyInit.h>
 #include <libsolutil/Result.h>
 
 #include <boost/rational.hpp>
@@ -139,8 +140,10 @@ public:
 	MemberMap::const_iterator end() const { return m_memberTypes.end(); }
 
 private:
+	StorageOffsets const& storageOffsets() const;
+
 	MemberMap m_memberTypes;
-	mutable std::unique_ptr<StorageOffsets> m_storageOffsets;
+	util::LazyInit<StorageOffsets> m_storageOffsets;
 };
 
 static_assert(std::is_nothrow_move_constructible<MemberList>::value, "MemberList should be noexcept move constructible");

libsolidity/codegen/YulUtilFunctions.cpp

@@ -602,6 +602,25 @@ string YulUtilFunctions::overflowCheckedIntSubFunction(IntegerType const& _type)
 	});
 }
 
+string YulUtilFunctions::extractByteArrayLengthFunction()
+{
+	string functionName = "extract_byte_array_length";
+	return m_functionCollector.createFunction(functionName, [&]() {
+		Whiskers w(R"(
+			function <functionName>(data) -> length {
+				// Retrieve length both for in-place strings and off-place strings:
+				// Computes (x & (0x100 * (ISZERO (x & 1)) - 1)) / 2
+				// i.e. for short strings (x & 1 == 0) it does (x & 0xff) / 2 and for long strings it
+				// computes (x & (-1)) / 2, which is equivalent to just x / 2.
+				let mask := sub(mul(0x100, iszero(and(data, 1))), 1)
+				length := div(and(data, mask), 2)
+			}
+		)");
+		w("functionName", functionName);
+		return w.render();
+	});
+}
+
 string YulUtilFunctions::arrayLengthFunction(ArrayType const& _type)
 {
 	string functionName = "array_length_" + _type.identifier();
@@ -615,12 +634,7 @@ string YulUtilFunctions::arrayLengthFunction(ArrayType const& _type)
 					<?storage>
 						length := sload(value)
 						<?byteArray>
-							// Retrieve length both for in-place strings and off-place strings:
-							// Computes (x & (0x100 * (ISZERO (x & 1)) - 1)) / 2
-							// i.e. for short strings (x & 1 == 0) it does (x & 0xff) / 2 and for long strings it
-							// computes (x & (-1)) / 2, which is equivalent to just x / 2.
-							let mask := sub(mul(0x100, iszero(and(length, 1))), 1)
-							length := div(and(length, mask), 2)
+							length := <extractByteArrayLength>(length)
 						</byteArray>
 					</storage>
 				<!dynamic>
@@ -634,7 +648,12 @@ string YulUtilFunctions::arrayLengthFunction(ArrayType const& _type)
 			w("length", toCompactHexWithPrefix(_type.length()));
 		w("memory", _type.location() == DataLocation::Memory);
 		w("storage", _type.location() == DataLocation::Storage);
-		w("byteArray", _type.isByteArray());
+		if (_type.location() == DataLocation::Storage)
+		{
+			w("byteArray", _type.isByteArray());
+			if (_type.isByteArray())
+				w("extractByteArrayLength", extractByteArrayLengthFunction());
+		}
 		if (_type.isDynamicallySized())
 			solAssert(
 				_type.location() != DataLocation::CallData,
@@ -689,8 +708,9 @@ string YulUtilFunctions::storageArrayPopFunction(ArrayType const& _type)
 {
 	solAssert(_type.location() == DataLocation::Storage, "");
 	solAssert(_type.isDynamicallySized(), "");
-	solUnimplementedAssert(!_type.isByteArray(), "Byte Arrays not yet implemented!");
 	solUnimplementedAssert(_type.baseType()->storageBytes() <= 32, "Base type is not yet implemented.");
+	if (_type.isByteArray())
+		return storageByteArrayPopFunction(_type);
 
 	string functionName = "array_pop_" + _type.identifier();
 	return m_functionCollector.createFunction(functionName, [&]() {
@@ -699,10 +719,8 @@ string YulUtilFunctions::storageArrayPopFunction(ArrayType const& _type)
 				let oldLen := <fetchLength>(array)
 				if iszero(oldLen) { invalid() }
 				let newLen := sub(oldLen, 1)
-
 				let slot, offset := <indexAccess>(array, newLen)
 				<setToZero>(slot, offset)
-
 				sstore(array, newLen)
 			})")
 			("functionName", functionName)
@@ -713,29 +731,115 @@ string YulUtilFunctions::storageArrayPopFunction(ArrayType const& _type)
 	});
 }
 
+string YulUtilFunctions::storageByteArrayPopFunction(ArrayType const& _type)
+{
+	solAssert(_type.location() == DataLocation::Storage, "");
+	solAssert(_type.isDynamicallySized(), "");
+	solAssert(_type.isByteArray(), "");
+
+	string functionName = "byte_array_pop_" + _type.identifier();
+	return m_functionCollector.createFunction(functionName, [&]() {
+		return Whiskers(R"(
+			function <functionName>(array) {
+				let data := sload(array)
+				let oldLen := <extractByteArrayLength>(data)
+				if iszero(oldLen) { invalid() }
+
+				switch eq(oldLen, 32)
+				case 1 {
+					// Here we have a special case where array transitions to shorter than 32
+					// So we need to copy data
+					let copyFromSlot := <dataAreaFunction>(array)
+					data := sload(copyFromSlot)
+					sstore(copyFromSlot, 0)
+					// New length is 31, encoded to 31 * 2 = 62
+					data := or(and(data, not(0xff)), 62)
+				}
+				default {
+					data := sub(data, 2)
+					let newLen := sub(oldLen, 1)
+					switch lt(oldLen, 32)
+					case 1 {
+						// set last element to zero
+						let mask := not(<shl>(mul(8, sub(31, newLen)), 0xff))
+						data := and(data, mask)
+					}
+					default {
+						let slot, offset := <indexAccess>(array, newLen)
+						<setToZero>(slot, offset)
+					}
+				}
+				sstore(array, data)
+			})")
+			("functionName", functionName)
+			("extractByteArrayLength", extractByteArrayLengthFunction())
+			("dataAreaFunction", arrayDataAreaFunction(_type))
+			("indexAccess", storageArrayIndexAccessFunction(_type))
+			("setToZero", storageSetToZeroFunction(*_type.baseType()))
+			("shl", shiftLeftFunctionDynamic())
+			.render();
+	});
+}
+
 string YulUtilFunctions::storageArrayPushFunction(ArrayType const& _type)
 {
 	solAssert(_type.location() == DataLocation::Storage, "");
 	solAssert(_type.isDynamicallySized(), "");
-	solUnimplementedAssert(!_type.isByteArray(), "Byte Arrays not yet implemented!");
 	solUnimplementedAssert(_type.baseType()->storageBytes() <= 32, "Base type is not yet implemented.");
 
 	string functionName = "array_push_" + _type.identifier();
 	return m_functionCollector.createFunction(functionName, [&]() {
 		return Whiskers(R"(
 			function <functionName>(array, value) {
-				let oldLen := <fetchLength>(array)
-				if iszero(lt(oldLen, <maxArrayLength>)) { invalid() }
-				sstore(array, add(oldLen, 1))
+				<?isByteArray>
+					let data := sload(array)
+					let oldLen := <extractByteArrayLength>(data)
+					if iszero(lt(oldLen, <maxArrayLength>)) { invalid() }
 
-				let slot, offset := <indexAccess>(array, oldLen)
-				<storeValue>(slot, offset, value)
+					switch gt(oldLen, 31)
+					case 0 {
+						value := byte(0, value)
+						switch oldLen
+						case 31 {
+							// Here we have special case when array switches from short array to long array
+							// We need to copy data
+							let dataArea := <dataAreaFunction>(array)
+							data := and(data, not(0xff))
+							sstore(dataArea, or(and(0xff, value), data))
+							// New length is 32, encoded as (32 * 2 + 1)
+							sstore(array, 65)
+						}
+						default {
+							data := add(data, 2)
+							let shiftBits := mul(8, sub(31, oldLen))
+							let valueShifted := <shl>(shiftBits, and(0xff, value))
+							let mask := <shl>(shiftBits, 0xff)
+							data := or(and(data, not(mask)), valueShifted)
+							sstore(array, data)
+						}
+					}
+					default {
+						sstore(array, add(data, 2))
+						let slot, offset := <indexAccess>(array, oldLen)
+						<storeValue>(slot, offset, value)
+					}
+				<!isByteArray>
+					let oldLen := sload(array)
+					if iszero(lt(oldLen, <maxArrayLength>)) { invalid() }
+					sstore(array, add(oldLen, 1))
+					let slot, offset := <indexAccess>(array, oldLen)
+					<storeValue>(slot, offset, value)
+				</isByteArray>
 			})")
 			("functionName", functionName)
-			("fetchLength", arrayLengthFunction(_type))
+			("extractByteArrayLength", _type.isByteArray() ? extractByteArrayLengthFunction() : "")
+			("dataAreaFunction", arrayDataAreaFunction(_type))
+			("isByteArray", _type.isByteArray())
 			("indexAccess", storageArrayIndexAccessFunction(_type))
 			("storeValue", updateStorageValueFunction(*_type.baseType()))
 			("maxArrayLength", (u256(1) << 64).str())
+			("shl", shiftLeftFunctionDynamic())
+			("shr", shiftRightFunction(248))
 			.render();
 	});
 }
@@ -947,21 +1051,33 @@ string YulUtilFunctions::arrayDataAreaFunction(ArrayType const& _type)
 
 string YulUtilFunctions::storageArrayIndexAccessFunction(ArrayType const& _type)
 {
-	solUnimplementedAssert(_type.baseType()->storageBytes() > 16, "");
-
 	string functionName = "storage_array_index_access_" + _type.identifier();
 	return m_functionCollector.createFunction(functionName, [&]() {
 		return Whiskers(R"(
 			function <functionName>(array, index) -> slot, offset {
-				if iszero(lt(index, <arrayLen>(array))) {
-					invalid()
-				}
+				let arrayLength := <arrayLen>(array)
+				if iszero(lt(index, arrayLength)) { invalid() }
 
-				let data := <dataAreaFunc>(array)
 				<?multipleItemsPerSlot>
-
+					<?isBytesArray>
+						offset := sub(31, mod(index, 0x20))
+						switch lt(arrayLength, 0x20)
+						case 0 {
+							let dataArea := <dataAreaFunc>(array)
+							slot := add(dataArea, div(index, 0x20))
+						}
+						default {
+							slot := array
+						}
+					<!isBytesArray>
+						let itemsPerSlot := div(0x20, <storageBytes>)
+						let dataArea := <dataAreaFunc>(array)
+						slot := add(dataArea, div(index, itemsPerSlot))
+						offset := mod(index, itemsPerSlot)
+					</isBytesArray>
 				<!multipleItemsPerSlot>
-					slot := add(data, mul(index, <storageSize>))
+					let dataArea := <dataAreaFunc>(array)
+					slot := add(dataArea, mul(index, <storageSize>))
 					offset := 0
 				</multipleItemsPerSlot>
 			}
@@ -970,7 +1086,9 @@ string YulUtilFunctions::storageArrayIndexAccessFunction(ArrayType const& _type)
 		("arrayLen", arrayLengthFunction(_type))
 		("dataAreaFunc", arrayDataAreaFunction(_type))
 		("multipleItemsPerSlot", _type.baseType()->storageBytes() <= 16)
+		("isBytesArray", _type.isByteArray())
 		("storageSize", _type.baseType()->storageSize().str())
+		("storageBytes", toString(_type.baseType()->storageBytes()))
 		.render();
 	});
 }

libsolidity/codegen/YulUtilFunctions.h

@@ -364,6 +364,14 @@ private:
 	/// use exactly one variable to hold the value.
 	std::string conversionFunctionSpecial(Type const& _from, Type const& _to);
 
+	/// @returns function name that extracts and returns byte array length
+	/// signature: (data) -> length
+	std::string extractByteArrayLengthFunction();
+
+	/// @returns the name of a function that reduces the size of a storage byte array by one element
+	/// signature: (byteArray)
+	std::string storageByteArrayPopFunction(ArrayType const& _type);
+
 	std::string readFromMemoryOrCalldata(Type const& _type, bool _fromCalldata);
 
 	langutil::EVMVersion m_evmVersion;

libsolidity/codegen/ir/Common.cpp

@@ -0,0 +1,86 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/codegen/ir/Common.h>
+
+#include <libsolutil/CommonIO.h>
+
+using namespace std;
+using namespace solidity::util;
+using namespace solidity::frontend;
+
+string IRNames::function(FunctionDefinition const& _function)
+{
+	// @TODO previously, we had to distinguish creation context and runtime context,
+	// but since we do not work with jump positions anymore, this should not be a problem, right?
+	return "fun_" + _function.name() + "_" + to_string(_function.id());
+}
+
+string IRNames::function(VariableDeclaration const& _varDecl)
+{
+	return "getter_fun_" + _varDecl.name() + "_" + to_string(_varDecl.id());
+}
+
+string IRNames::creationObject(ContractDefinition const& _contract)
+{
+	return _contract.name() + "_" + toString(_contract.id());
+}
+
+string IRNames::runtimeObject(ContractDefinition const& _contract)
+{
+	return _contract.name() + "_" + toString(_contract.id()) + "_deployed";
+}
+
+string IRNames::implicitConstructor(ContractDefinition const& _contract)
+{
+	return "constructor_" + _contract.name() + "_" + to_string(_contract.id());
+}
+
+string IRNames::constantValueFunction(VariableDeclaration const& _constant)
+{
+	solAssert(_constant.isConstant(), "");
+	return "constant_" + _constant.name() + "_" + to_string(_constant.id());
+}
+
+string IRNames::localVariable(VariableDeclaration const& _declaration)
+{
+	return "vloc_" + _declaration.name() + '_' + std::to_string(_declaration.id());
+}
+
+string IRNames::localVariable(Expression const& _expression)
+{
+	return "expr_" + to_string(_expression.id());
+}
+
+string IRNames::trySuccessConditionVariable(Expression const& _expression)
+{
+	auto annotation = dynamic_cast<FunctionCallAnnotation const*>(&_expression.annotation());
+	solAssert(annotation, "");
+	solAssert(annotation->tryCall, "Parameter must be a FunctionCall with tryCall-annotation set.");
+
+	return "trySuccessCondition_" + to_string(_expression.id());
+}
+
+string IRNames::tupleComponent(size_t _i)
+{
+	return "component_" + to_string(_i + 1);
+}
+
+string IRNames::zeroValue(Type const& _type, string const& _variableName)
+{
+	return "zero_value_for_type_" + _type.identifier() + _variableName;
+}

libsolidity/codegen/ir/Common.h

@@ -0,0 +1,47 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+/**
+ * Miscellaneous utilities for use in IR generator.
+ */
+
+#pragma once
+
+#include <libsolidity/ast/AST.h>
+
+#include <string>
+
+namespace solidity::frontend
+{
+
+struct IRNames
+{
+	static std::string function(FunctionDefinition const& _function);
+	static std::string function(VariableDeclaration const& _varDecl);
+	static std::string creationObject(ContractDefinition const& _contract);
+	static std::string runtimeObject(ContractDefinition const& _contract);
+	static std::string implicitConstructor(ContractDefinition const& _contract);
+	static std::string constantValueFunction(VariableDeclaration const& _constant);
+	static std::string localVariable(VariableDeclaration const& _declaration);
+	static std::string localVariable(Expression const& _expression);
+	/// @returns the variable name that can be used to inspect the success or failure of an external
+	/// function call that was invoked as part of the try statement.
+	static std::string trySuccessConditionVariable(Expression const& _expression);
+	static std::string tupleComponent(size_t _i);
+	static std::string zeroValue(Type const& _type, std::string const& _variableName);
+};
+
+}

libsolidity/codegen/ir/IRGenerationContext.cpp

@@ -36,7 +36,7 @@ using namespace solidity::frontend;
 
 string IRGenerationContext::enqueueFunctionForCodeGeneration(FunctionDefinition const& _function)
 {
-	string name = functionName(_function);
+	string name = IRNames::function(_function);
 
 	if (!m_functions.contains(name))
 		m_functionGenerationQueue.insert(&_function);
@@ -116,43 +116,11 @@ void IRGenerationContext::addStateVariable(
 	m_stateVariables[&_declaration] = make_pair(move(_storageOffset), _byteOffset);
 }
 
-string IRGenerationContext::functionName(FunctionDefinition const& _function)
-{
-	// @TODO previously, we had to distinguish creation context and runtime context,
-	// but since we do not work with jump positions anymore, this should not be a problem, right?
-	return "fun_" + _function.name() + "_" + to_string(_function.id());
-}
-
-string IRGenerationContext::functionName(VariableDeclaration const& _varDecl)
-{
-	return "getter_fun_" + _varDecl.name() + "_" + to_string(_varDecl.id());
-}
-
-string IRGenerationContext::creationObjectName(ContractDefinition const& _contract) const
-{
-	return _contract.name() + "_" + toString(_contract.id());
-}
-string IRGenerationContext::runtimeObjectName(ContractDefinition const& _contract) const
-{
-	return _contract.name() + "_" + toString(_contract.id()) + "_deployed";
-}
-
 string IRGenerationContext::newYulVariable()
 {
 	return "_" + to_string(++m_varCounter);
 }
 
-string IRGenerationContext::trySuccessConditionVariable(Expression const& _expression) const
-{
-	// NB: The TypeChecker already ensured that the Expression is of type FunctionCall.
-	solAssert(
-		static_cast<FunctionCallAnnotation const&>(_expression.annotation()).tryCall,
-		"Parameter must be a FunctionCall with tryCall-annotation set."
-	);
-
-	return "trySuccessCondition_" + to_string(_expression.id());
-}
-
 string IRGenerationContext::internalDispatch(size_t _in, size_t _out)
 {
 	string funName = "dispatch_internal_in_" + to_string(_in) + "_out_" + to_string(_out);
@@ -196,7 +164,7 @@ string IRGenerationContext::internalDispatch(size_t _in, size_t _out)
 
 					functions.emplace_back(map<string, string> {
 						{ "funID", to_string(function->id()) },
-						{ "name", functionName(*function)}
+						{ "name", IRNames::function(*function)}
 					});
 
 					enqueueFunctionForCodeGeneration(*function);

libsolidity/codegen/ir/IRGenerationContext.h

@@ -26,6 +26,7 @@
 #include <libsolidity/interface/DebugSettings.h>
 
 #include <libsolidity/codegen/MultiUseYulFunctionCollector.h>
+#include <libsolidity/codegen/ir/Common.h>
 
 #include <liblangutil/EVMVersion.h>
 
@@ -99,12 +100,6 @@ public:
 		return m_stateVariables.at(&_varDecl);
 	}
 
-	std::string functionName(FunctionDefinition const& _function);
-	std::string functionName(VariableDeclaration const& _varDecl);
-
-	std::string creationObjectName(ContractDefinition const& _contract) const;
-	std::string runtimeObjectName(ContractDefinition const& _contract) const;
-
 	std::string newYulVariable();
 
 	std::string internalDispatch(size_t _in, size_t _out);
@@ -122,10 +117,6 @@ public:
 
 	RevertStrings revertStrings() const { return m_revertStrings; }
 
-	/// @returns the variable name that can be used to inspect the success or failure of an external
-	/// function call that was invoked as part of the try statement.
-	std::string trySuccessConditionVariable(Expression const& _expression) const;
-
 	std::set<ContractDefinition const*, ASTNode::CompareByID>& subObjectsCreated() { return m_subObjects; }
 
 private:

libsolidity/codegen/ir/IRGenerator.cpp

@@ -114,7 +114,7 @@ string IRGenerator::generate(
 	for (VariableDeclaration const* var: ContractType(_contract).immutableVariables())
 		m_context.registerImmutableVariable(*var);
 
-	t("CreationObject", m_context.creationObjectName(_contract));
+	t("CreationObject", IRNames::creationObject(_contract));
 	t("memoryInit", memoryInit());
 	t("notLibrary", !_contract.isLibrary());
 
@@ -127,12 +127,12 @@ string IRGenerator::generate(
 			constructorParams.emplace_back(m_context.newYulVariable());
 		t(
 			"copyConstructorArguments",
-			m_utils.copyConstructorArgumentsToMemoryFunction(_contract, m_context.creationObjectName(_contract))
+			m_utils.copyConstructorArgumentsToMemoryFunction(_contract, IRNames::creationObject(_contract))
 		);
 	}
 	t("constructorParams", joinHumanReadable(constructorParams));
 	t("constructorHasParams", !constructorParams.empty());
-	t("implicitConstructor", implicitConstructorName(_contract));
+	t("implicitConstructor", IRNames::implicitConstructor(_contract));
 
 	t("deploy", deployCode(_contract));
 	generateImplicitConstructors(_contract);
@@ -142,7 +142,7 @@ string IRGenerator::generate(
 
 	resetContext(_contract);
 	// Do not register immutables to avoid assignment.
-	t("RuntimeObject", m_context.runtimeObjectName(_contract));
+	t("RuntimeObject", IRNames::runtimeObject(_contract));
 	t("dispatch", dispatchRoutine(_contract));
 	generateQueuedFunctions();
 	t("runtimeFunctions", m_context.functionCollector().requestedFunctions());
@@ -166,7 +166,7 @@ void IRGenerator::generateQueuedFunctions()
 
 string IRGenerator::generateFunction(FunctionDefinition const& _function)
 {
-	string functionName = m_context.functionName(_function);
+	string functionName = IRNames::function(_function);
 	return m_context.functionCollector().createFunction(functionName, [&]() {
 		Whiskers t(R"(
 			function <functionName>(<params>)<?+retParams> -> <retParams></+retParams> {
@@ -195,7 +195,7 @@ string IRGenerator::generateFunction(FunctionDefinition const& _function)
 
 string IRGenerator::generateGetter(VariableDeclaration const& _varDecl)
 {
-	string functionName = m_context.functionName(_varDecl);
+	string functionName = IRNames::function(_varDecl);
 
 	Type const* type = _varDecl.annotation().type;
 
@@ -378,7 +378,7 @@ void IRGenerator::generateImplicitConstructors(ContractDefinition const& _contra
 		ContractDefinition const* contract = _contract.annotation().linearizedBaseContracts[i];
 		baseConstructorParams.erase(contract);
 
-		m_context.functionCollector().createFunction(implicitConstructorName(*contract), [&]() {
+		m_context.functionCollector().createFunction(IRNames::implicitConstructor(*contract), [&]() {
 			Whiskers t(R"(
 				function <functionName>(<params><comma><baseParams>) {
 					<evalBaseArguments>
@@ -395,7 +395,7 @@ void IRGenerator::generateImplicitConstructors(ContractDefinition const& _contra
 			vector<string> baseParams = listAllParams(baseConstructorParams);
 			t("baseParams", joinHumanReadable(baseParams));
 			t("comma", !params.empty() && !baseParams.empty() ? ", " : "");
-			t("functionName", implicitConstructorName(*contract));
+			t("functionName", IRNames::implicitConstructor(*contract));
 			pair<string, map<ContractDefinition const*, vector<string>>> evaluatedArgs = evaluateConstructorArguments(*contract);
 			baseConstructorParams.insert(evaluatedArgs.second.begin(), evaluatedArgs.second.end());
 			t("evalBaseArguments", evaluatedArgs.first);
@@ -403,7 +403,7 @@ void IRGenerator::generateImplicitConstructors(ContractDefinition const& _contra
 			{
 				t("hasNextConstructor", true);
 				ContractDefinition const* nextContract = _contract.annotation().linearizedBaseContracts[i + 1];
-				t("nextConstructor", implicitConstructorName(*nextContract));
+				t("nextConstructor", IRNames::implicitConstructor(*nextContract));
 				t("nextParams", joinHumanReadable(listAllParams(baseConstructorParams)));
 			}
 			else
@@ -431,7 +431,7 @@ string IRGenerator::deployCode(ContractDefinition const& _contract)
 
 		return(0, datasize("<object>"))
 	)X");
-	t("object", m_context.runtimeObjectName(_contract));
+	t("object", IRNames::runtimeObject(_contract));
 
 	vector<map<string, string>> loadImmutables;
 	vector<map<string, string>> storeImmutables;
@@ -462,11 +462,6 @@ string IRGenerator::callValueCheck()
 	return "if callvalue() { revert(0, 0) }";
 }
 
-string IRGenerator::implicitConstructorName(ContractDefinition const& _contract)
-{
-	return "constructor_" + _contract.name() + "_" + to_string(_contract.id());
-}
-
 string IRGenerator::dispatchRoutine(ContractDefinition const& _contract)
 {
 	Whiskers t(R"X(

libsolidity/codegen/ir/IRGenerator.h

@@ -92,8 +92,6 @@ private:
 	std::string deployCode(ContractDefinition const& _contract);
 	std::string callValueCheck();
 
-	std::string implicitConstructorName(ContractDefinition const& _contract);
-
 	std::string dispatchRoutine(ContractDefinition const& _contract);
 
 	std::string memoryInit();

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -181,7 +181,7 @@ IRVariable IRGeneratorForStatements::evaluateExpression(Expression const& _expre
 
 string IRGeneratorForStatements::constantValueFunction(VariableDeclaration const& _constant)
 {
-	string functionName = "constant_" + _constant.name() + "_" + to_string(_constant.id());
+	string functionName = IRNames::constantValueFunction(_constant);
 	return m_context.functionCollector().createFunction(functionName, [&] {
 		Whiskers templ(R"(
 			function <functionName>() -> <ret> {
@@ -952,14 +952,6 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall)
 			"))\n";
 		break;
 	}
-	case FunctionType::Kind::ECRecover:
-	case FunctionType::Kind::SHA256:
-	case FunctionType::Kind::RIPEMD160:
-	{
-		solAssert(!_functionCall.annotation().tryCall, "");
-		appendExternalFunctionCall(_functionCall, arguments);
-		break;
-	}
 	case FunctionType::Kind::ArrayPop:
 	{
 		auto const& memberAccessExpression = dynamic_cast<MemberAccess const&>(_functionCall.expression()).expression();
@@ -971,10 +963,12 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall)
 			")\n";
 		break;
 	}
+	case FunctionType::Kind::ByteArrayPush:
 	case FunctionType::Kind::ArrayPush:
 	{
 		auto const& memberAccessExpression = dynamic_cast<MemberAccess const&>(_functionCall.expression()).expression();
 		ArrayType const& arrayType = dynamic_cast<ArrayType const&>(*memberAccessExpression.annotation().type);
+
 		if (arguments.empty())
 		{
 			auto slotName = m_context.newYulVariable();
@@ -1111,7 +1105,7 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall)
 		t("memEnd", m_context.newYulVariable());
 		t("allocateTemporaryMemory", m_utils.allocationTemporaryMemoryFunction());
 		t("releaseTemporaryMemory", m_utils.releaseTemporaryMemoryFunction());
-		t("object", m_context.creationObjectName(*contract));
+		t("object", IRNames::creationObject(*contract));
 		t("abiEncode",
 			m_context.abiFunctions().tupleEncoder(argumentTypes, functionType->parameterTypes(), false)
 		);
@@ -1153,6 +1147,69 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall)
 
 		break;
 	}
+	case FunctionType::Kind::ECRecover:
+	case FunctionType::Kind::RIPEMD160:
+	case FunctionType::Kind::SHA256:
+	{
+		solAssert(!_functionCall.annotation().tryCall, "");
+		solAssert(!functionType->valueSet(), "");
+		solAssert(!functionType->gasSet(), "");
+		solAssert(!functionType->bound(), "");
+
+		static map<FunctionType::Kind, std::tuple<u160, size_t>> precompiles = {
+			{FunctionType::Kind::ECRecover, std::make_tuple(1, 0)},
+			{FunctionType::Kind::SHA256, std::make_tuple(2, 0)},
+			{FunctionType::Kind::RIPEMD160, std::make_tuple(3, 12)},
+		};
+		auto [ address, offset ] = precompiles[functionType->kind()];
+		TypePointers argumentTypes;
+		vector<string> argumentStrings;
+		for (auto const& arg: arguments)
+		{
+			argumentTypes.emplace_back(&type(*arg));
+			argumentStrings += IRVariable(*arg).stackSlots();
+		}
+		Whiskers templ(R"(
+			let <pos> := <allocateTemporary>()
+			let <end> := <encodeArgs>(<pos> <argumentString>)
+			<?isECRecover>
+				mstore(0, 0)
+			</isECRecover>
+			let <success> := <call>(<gas>, <address> <?isCall>, 0</isCall>, <pos>, sub(<end>, <pos>), 0, 32)
+			if iszero(<success>) { <forwardingRevert>() }
+			let <retVars> := <shl>(mload(0))
+		)");
+		templ("call", m_context.evmVersion().hasStaticCall() ? "staticcall" : "call");
+		templ("isCall", !m_context.evmVersion().hasStaticCall());
+		templ("shl", m_utils.shiftLeftFunction(offset * 8));
+		templ("allocateTemporary", m_utils.allocationTemporaryMemoryFunction());
+		templ("pos", m_context.newYulVariable());
+		templ("end", m_context.newYulVariable());
+		templ("isECRecover", FunctionType::Kind::ECRecover == functionType->kind());
+		if (FunctionType::Kind::ECRecover == functionType->kind())
+			templ("encodeArgs", m_context.abiFunctions().tupleEncoder(argumentTypes, parameterTypes));
+		else
+			templ("encodeArgs", m_context.abiFunctions().tupleEncoderPacked(argumentTypes, parameterTypes));
+		templ("argumentString", joinHumanReadablePrefixed(argumentStrings));
+		templ("address", toString(address));
+		templ("success", m_context.newYulVariable());
+		templ("retVars", IRVariable(_functionCall).commaSeparatedList());
+		templ("forwardingRevert", m_utils.forwardingRevertFunction());
+		if (m_context.evmVersion().canOverchargeGasForCall())
+			// Send all gas (requires tangerine whistle EVM)
+			templ("gas", "gas()");
+		else
+		{
+			// @todo The value 10 is not exact and this could be fine-tuned,
+			// but this has worked for years in the old code generator.
+			u256 gasNeededByCaller = evmasm::GasCosts::callGas(m_context.evmVersion()) + 10 + evmasm::GasCosts::callNewAccountGas;
+			templ("gas", "sub(gas(), " + formatNumber(gasNeededByCaller) + ")");
+		}
+
+		m_code << templ.render();
+
+		break;
+	}
 	default:
 		solUnimplemented("FunctionKind " + toString(static_cast<int>(functionType->kind())) + " not yet implemented");
 	}
@@ -1316,7 +1373,7 @@ void IRGeneratorForStatements::endVisit(MemberAccess const& _memberAccess)
 			)")
 			("allocationFunction", m_utils.allocationFunction())
 			("size", m_context.newYulVariable())
-			("objectName", m_context.creationObjectName(contract))
+			("objectName", IRNames::creationObject(contract))
 			("result", IRVariable(_memberAccess).commaSeparatedList()).render();
 		}
 		else if (member == "name")
@@ -1835,7 +1892,7 @@ void IRGeneratorForStatements::appendExternalFunctionCall(
 	templ("pos", m_context.newYulVariable());
 	templ("end", m_context.newYulVariable());
 	if (_functionCall.annotation().tryCall)
-		templ("success", m_context.trySuccessConditionVariable(_functionCall));
+		templ("success", IRNames::trySuccessConditionVariable(_functionCall));
 	else
 		templ("success", m_context.newYulVariable());
 	templ("freeMemory", freeMemory());
@@ -2070,10 +2127,7 @@ void IRGeneratorForStatements::declareAssign(IRVariable const& _lhs, IRVariable
 
 IRVariable IRGeneratorForStatements::zeroValue(Type const& _type, bool _splitFunctionTypes)
 {
-	IRVariable irVar{
-		"zero_value_for_type_" + _type.identifier() + m_context.newYulVariable(),
-		_type
-	};
+	IRVariable irVar{IRNames::zeroValue(_type, m_context.newYulVariable()), _type};
 	define(irVar) << m_utils.zeroValueFunction(_type, _splitFunctionTypes) << "()\n";
 	return irVar;
 }
@@ -2392,7 +2446,7 @@ bool IRGeneratorForStatements::visit(TryStatement const& _tryStatement)
 	Expression const& externalCall = _tryStatement.externalCall();
 	externalCall.accept(*this);
 
-	m_code << "switch iszero(" << m_context.trySuccessConditionVariable(externalCall) << ")\n";
+	m_code << "switch iszero(" << IRNames::trySuccessConditionVariable(externalCall) << ")\n";
 
 	m_code << "case 0 { // success case\n";
 	TryCatchClause const& successClause = *_tryStatement.clauses().front();

libsolidity/codegen/ir/IRVariable.cpp

@@ -14,6 +14,7 @@
 	You should have received a copy of the GNU General Public License
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
+#include <libsolidity/codegen/ir/Common.h>
 #include <libsolidity/codegen/ir/IRVariable.h>
 #include <libsolidity/ast/AST.h>
 #include <boost/range/adaptor/transformed.hpp>
@@ -30,19 +31,13 @@ IRVariable::IRVariable(std::string _baseName, Type const& _type):
 }
 
 IRVariable::IRVariable(VariableDeclaration const& _declaration):
-	IRVariable(
-		"vloc_" + _declaration.name() + '_' + std::to_string(_declaration.id()),
-		*_declaration.annotation().type
-	)
+	IRVariable(IRNames::localVariable(_declaration), *_declaration.annotation().type)
 {
 	solAssert(!_declaration.isStateVariable(), "");
 }
 
 IRVariable::IRVariable(Expression const& _expression):
-	IRVariable(
-		"expr_" + to_string(_expression.id()),
-		*_expression.annotation().type
-	)
+	IRVariable(IRNames::localVariable(_expression), *_expression.annotation().type)
 {
 }
 
@@ -99,7 +94,7 @@ IRVariable IRVariable::tupleComponent(size_t _i) const
 		m_type.category() == Type::Category::Tuple,
 		"Requested tuple component of non-tuple IR variable."
 	);
-	return part("component_" + std::to_string(_i + 1));
+	return part(IRNames::tupleComponent(_i));
 }
 
 string IRVariable::suffixedName(string const& _suffix) const

libsolidity/formal/CHC.cpp

@@ -98,17 +98,45 @@ void CHC::analyze(SourceUnit const& _source)
 
 	for (auto const& [scope, target]: m_verificationTargets)
 	{
-		auto assertions = transactionAssertions(scope);
-		for (auto const* assertion: assertions)
+		if (target.type == VerificationTarget::Type::Assert)
 		{
+			auto assertions = transactionAssertions(scope);
+			for (auto const* assertion: assertions)
+			{
+				createErrorBlock();
+				connectBlocks(target.value, error(), target.constraints && (target.errorId == assertion->id()));
+				auto [result, model] = query(error(), assertion->location());
+				// This should be fine but it's a bug in the old compiler
+				(void)model;
+				if (result == smt::CheckResult::UNSATISFIABLE)
+					m_safeAssertions.insert(assertion);
+			}
+		}
+		else if (target.type == VerificationTarget::Type::PopEmptyArray)
+		{
+			solAssert(dynamic_cast<FunctionCall const*>(scope), "");
 			createErrorBlock();
-			connectBlocks(target.value, error(), target.constraints && (target.errorId == assertion->id()));
-			auto [result, model] = query(error(), assertion->location());
+			connectBlocks(target.value, error(), target.constraints && (target.errorId == scope->id()));
+			auto [result, model] = query(error(), scope->location());
 			// This should be fine but it's a bug in the old compiler
 			(void)model;
-			if (result == smt::CheckResult::UNSATISFIABLE)
-				m_safeAssertions.insert(assertion);
+			if (result != smt::CheckResult::UNSATISFIABLE)
+			{
+				string msg = "Empty array \"pop\" ";
+				if (result == smt::CheckResult::SATISFIABLE)
+					msg += "detected here.";
+				else
+					msg += "might happen here.";
+				m_unsafeTargets.insert(scope);
+				m_outerErrorReporter.warning(
+					2529_error,
+					scope->location(),
+					msg
+				);
+			}
 		}
+		else
+			solAssert(false, "");
 	}
 }
 
@@ -161,7 +189,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	auto stateExprs = vector<smt::Expression>{m_error.currentValue()} + currentStateVariables();
 	setCurrentBlock(*m_constructorSummaryPredicate, &stateExprs);
 
-	addVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue());
+	addAssertVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue());
 	connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0);
 
 	SMTEncoder::endVisit(_contract);
@@ -256,7 +284,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
 
 			if (_function.isPublic())
 			{
-				addVerificationTarget(&_function, m_currentBlock, sum, assertionError);
+				addAssertVerificationTarget(&_function, m_currentBlock, sum, assertionError);
 				connectBlocks(m_currentBlock, iface, sum && (assertionError == 0));
 			}
 		}
@@ -556,10 +584,34 @@ void CHC::unknownFunctionCall(FunctionCall const&)
 	m_unknownFunctionCallSeen = true;
 }
 
+void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
+{
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_arrayPop.expression().annotation().type);
+	solAssert(funType.kind() == FunctionType::Kind::ArrayPop, "");
+
+	auto memberAccess = dynamic_cast<MemberAccess const*>(&_arrayPop.expression());
+	solAssert(memberAccess, "");
+	auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
+	solAssert(symbArray, "");
+
+	auto previousError = m_error.currentValue();
+	m_error.increaseIndex();
+
+	addArrayPopVerificationTarget(&_arrayPop, m_error.currentValue());
+	connectBlocks(
+		m_currentBlock,
+		m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction),
+		currentPathConditions() && symbArray->length() <= 0 && m_error.currentValue() == _arrayPop.id()
+	);
+
+	m_context.addAssertion(m_error.currentValue() == previousError);
+}
+
 void CHC::resetSourceAnalysis()
 {
 	m_verificationTargets.clear();
 	m_safeAssertions.clear();
+	m_unsafeTargets.clear();
 	m_functionAssertions.clear();
 	m_callGraph.clear();
 	m_summaries.clear();
@@ -974,9 +1026,35 @@ pair<smt::CheckResult, vector<string>> CHC::query(smt::Expression const& _query,
 	return {result, values};
 }
 
-void CHC::addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId)
+void CHC::addVerificationTarget(
+	ASTNode const* _scope,
+	VerificationTarget::Type _type,
+	smt::Expression _from,
+	smt::Expression _constraints,
+	smt::Expression _errorId
+)
 {
-	m_verificationTargets.emplace(_scope, CHCVerificationTarget{{VerificationTarget::Type::Assert, _from, _constraints}, _errorId});
+	m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId});
+}
+
+void CHC::addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId)
+{
+	addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId);
+}
+
+void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId)
+{
+	solAssert(m_currentContract, "");
+	solAssert(m_currentFunction, "");
+
+	if (m_currentFunction->isConstructor())
+		addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, summary(*m_currentContract), smt::Expression(true), _errorId);
+	else
+	{
+		auto iface = (*m_interfaces.at(m_currentContract))(initialStateVariables());
+		auto sum = summary(*m_currentFunction);
+		addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, iface, sum, _errorId);
+	}
 }
 
 string CHC::uniquePrefix()

libsolidity/formal/CHC.h

@@ -78,6 +78,7 @@ private:
 	void visitAssert(FunctionCall const& _funCall);
 	void internalFunctionCall(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);
+	void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override;
 	//@}
 
 	struct IdCompare
@@ -182,7 +183,9 @@ private:
 	/// @returns <false, model> otherwise.
 	std::pair<smt::CheckResult, std::vector<std::string>> query(smt::Expression const& _query, langutil::SourceLocation const& _location);
 
-	void addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
+	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
+	void addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
+	void addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId);
 	//@}
 
 	/// Misc.
@@ -245,6 +248,8 @@ private:
 
 	/// Assertions proven safe.
 	std::set<Expression const*> m_safeAssertions;
+	/// Targets proven unsafe.
+	std::set<ASTNode const*> m_unsafeTargets;
 	//@}
 
 	/// Control-flow.

libsolidity/formal/CVC4Interface.cpp

@@ -206,6 +206,15 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 			CVC4::Expr s = dt[0][index].getSelector();
 			return m_context.mkExpr(CVC4::kind::APPLY_SELECTOR, s, arguments[0]);
 		}
+		else if (n == "tuple_constructor")
+		{
+			shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.sort);
+			solAssert(tupleSort, "");
+			CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
+			CVC4::Datatype const& dt = tt.getDatatype();
+			CVC4::Expr c = dt[0].getConstructor();
+			return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments);
+		}
 
 		solAssert(false, "");
 	}

libsolidity/formal/SMTEncoder.cpp

@@ -646,6 +646,12 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 		m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value));
 		break;
 	}
+	case FunctionType::Kind::ArrayPush:
+		arrayPush(_funCall);
+		break;
+	case FunctionType::Kind::ArrayPop:
+		arrayPop(_funCall);
+		break;
 	default:
 		m_errorReporter.warning(
 			4588_error,
@@ -890,6 +896,23 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 			return false;
 		}
 	}
+	else if (exprType->category() == Type::Category::Array)
+	{
+		_memberAccess.expression().accept(*this);
+		if (_memberAccess.memberName() == "length")
+		{
+			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_memberAccess.expression()));
+			solAssert(symbArray, "");
+			defineExpr(_memberAccess, symbArray->length());
+			m_uninterpretedTerms.insert(&_memberAccess);
+			setSymbolicUnknownValue(
+				expr(_memberAccess),
+				_memberAccess.annotation().type,
+				m_context
+			);
+		}
+		return false;
+	}
 	else
 		m_errorReporter.warning(
 			7650_error,
@@ -939,9 +962,10 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		return;
 	}
 
-	solAssert(array, "");
+	auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
+	solAssert(arrayVar, "");
 	defineExpr(_indexAccess, smt::Expression::select(
-		array->currentValue(),
+		arrayVar->elements(),
 		expr(*_indexAccess.indexExpression())
 	));
 	setSymbolicUnknownValue(
@@ -1013,16 +1037,20 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 					return false;
 				});
 
+			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.variable(*varDecl));
 			smt::Expression store = smt::Expression::store(
-				m_context.variable(*varDecl)->currentValue(),
+				symbArray->elements(),
 				expr(*indexAccess->indexExpression()),
 				toStore
 			);
-			m_context.addAssertion(m_context.newValue(*varDecl) == store);
+			auto oldLength = symbArray->length();
+			symbArray->increaseIndex();
+			m_context.addAssertion(symbArray->elements() == store);
+			m_context.addAssertion(symbArray->length() == oldLength);
 			// Update the SMT select value after the assignment,
 			// necessary for sound models.
 			defineExpr(*indexAccess, smt::Expression::select(
-				m_context.variable(*varDecl)->currentValue(),
+				symbArray->elements(),
 				expr(*indexAccess->indexExpression())
 			));
 
@@ -1030,7 +1058,12 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 		}
 		else if (auto base = dynamic_cast<IndexAccess const*>(&indexAccess->baseExpression()))
 		{
-			toStore = smt::Expression::store(expr(*base), expr(*indexAccess->indexExpression()), toStore);
+			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*base));
+			solAssert(symbArray, "");
+			toStore = smt::Expression::tuple_constructor(
+				smt::Expression(base->annotation().type),
+				{smt::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
+			);
 			indexAccess = base;
 		}
 		else
@@ -1045,6 +1078,76 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 	}
 }
 
+void SMTEncoder::arrayPush(FunctionCall const& _funCall)
+{
+	auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
+	solAssert(memberAccess, "");
+	auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
+	solAssert(symbArray, "");
+	auto oldLength = symbArray->length();
+	m_context.addAssertion(oldLength >= 0);
+	// Real world assumption: the array length is assumed to not overflow.
+	// This assertion guarantees that both the current and updated lengths have the above property.
+	m_context.addAssertion(oldLength + 1 < (smt::maxValue(*TypeProvider::uint256()) - 1));
+
+	auto const& arguments = _funCall.arguments();
+	smt::Expression element = arguments.empty() ?
+		smt::zeroValue(_funCall.annotation().type) :
+		expr(*arguments.front());
+	smt::Expression store = smt::Expression::store(
+		symbArray->elements(),
+		oldLength,
+		element
+	);
+	symbArray->increaseIndex();
+	m_context.addAssertion(symbArray->elements() == store);
+	m_context.addAssertion(symbArray->length() == oldLength + 1);
+
+	if (arguments.empty())
+		defineExpr(_funCall, element);
+
+	arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
+}
+
+void SMTEncoder::arrayPop(FunctionCall const& _funCall)
+{
+	auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
+	solAssert(memberAccess, "");
+	auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
+	solAssert(symbArray, "");
+
+	makeArrayPopVerificationTarget(_funCall);
+
+	auto oldElements = symbArray->elements();
+	auto oldLength = symbArray->length();
+	m_context.addAssertion(oldLength > 0);
+
+	symbArray->increaseIndex();
+	m_context.addAssertion(symbArray->elements() == oldElements);
+	auto newLength = smt::Expression::ite(
+		oldLength == 0,
+		smt::maxValue(*TypeProvider::uint256()),
+		oldLength - 1
+	);
+	m_context.addAssertion(symbArray->length() == oldLength - 1);
+
+	arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
+}
+
+void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array)
+{
+	if (auto const* id = dynamic_cast<Identifier const*>(&_expr))
+	{
+		auto varDecl = identifierToVariable(*id);
+		solAssert(varDecl, "");
+		m_context.addAssertion(m_context.newValue(*varDecl) == _array);
+	}
+	else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(&_expr))
+		arrayIndexAssignment(*indexAccess, _array);
+	else
+		solAssert(false, "");
+}
+
 void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
 {
 	if (!m_context.knownGlobalSymbol(_name))
@@ -1326,7 +1429,14 @@ smt::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
 
 void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value)
 {
-	assignment(_variable, expr(_value, _variable.type()));
+	// In general, at this point, the SMT sorts of _variable and _value are the same,
+	// even if there is implicit conversion.
+	// This is a special case where the SMT sorts are different.
+	// For now we are unaware of other cases where this happens, but if they do appear
+	// we should extract this into an `implicitConversion` function.
+	if (_variable.type()->category() != Type::Category::Array || _value.annotation().type->category() != Type::Category::StringLiteral)
+		assignment(_variable, expr(_value, _variable.type()));
+	// TODO else { store each string literal byte into the array }
 }
 
 void SMTEncoder::assignment(VariableDeclaration const& _variable, smt::Expression const& _value)
@@ -1616,7 +1726,7 @@ SMTEncoder::VariableIndices SMTEncoder::copyVariableIndices()
 void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
 {
 	for (auto const& var: _indices)
-		m_context.variable(*var.first)->index() = var.second;
+		m_context.variable(*var.first)->setIndex(var.second);
 }
 
 void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)

libsolidity/formal/SMTEncoder.h

@@ -137,6 +137,13 @@ protected:
 	/// Handles assignment to SMT array index.
 	void arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide);
 
+	void arrayPush(FunctionCall const& _funCall);
+	void arrayPop(FunctionCall const& _funCall);
+	void arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array);
+	/// Allows BMC and CHC to create verification targets for popping
+	/// an empty array.
+	virtual void makeArrayPopVerificationTarget(FunctionCall const&) {}
+
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
 	smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
@@ -240,7 +247,7 @@ protected:
 
 	struct VerificationTarget
 	{
-		enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert } type;
+		enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray } type;
 		smt::Expression value;
 		smt::Expression constraints;
 	};

libsolidity/formal/SMTLib2Interface.cpp

@@ -153,7 +153,15 @@ string SMTLib2Interface::toSExpr(smt::Expression const& _expr)
 		auto tupleSort = dynamic_pointer_cast<TupleSort>(_expr.arguments.at(0).sort);
 		unsigned index = std::stoi(_expr.arguments.at(1).name);
 		solAssert(index < tupleSort->members.size(), "");
-		sexpr += tupleSort->members.at(index) + " " + toSExpr(_expr.arguments.at(0));
+		sexpr += "|" + tupleSort->members.at(index) + "| " + toSExpr(_expr.arguments.at(0));
+	}
+	else if (_expr.name == "tuple_constructor")
+	{
+		auto tupleSort = dynamic_pointer_cast<TupleSort>(_expr.sort);
+		solAssert(tupleSort, "");
+		sexpr += "|" + tupleSort->name + "|";
+		for (auto const& arg: _expr.arguments)
+			sexpr += " " + toSExpr(arg);
 	}
 	else
 	{
@@ -182,18 +190,19 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 	case Kind::Tuple:
 	{
 		auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
-		if (!m_userSorts.count(tupleSort.name))
+		string tupleName = "|" + tupleSort.name + "|";
+		if (!m_userSorts.count(tupleName))
 		{
-			m_userSorts.insert(tupleSort.name);
-			string decl("(declare-datatypes ((" + tupleSort.name + " 0)) (((" + tupleSort.name);
+			m_userSorts.insert(tupleName);
+			string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName);
 			solAssert(tupleSort.members.size() == tupleSort.components.size(), "");
 			for (unsigned i = 0; i < tupleSort.members.size(); ++i)
-				decl += " (" + tupleSort.members.at(i) + " " + toSmtLibSort(*tupleSort.components.at(i)) + ")";
+				decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(*tupleSort.components.at(i)) + ")";
 			decl += "))))";
 			write(decl);
 		}
 
-		return tupleSort.name;
+		return tupleName;
 	}
 	default:
 		solAssert(false, "Invalid SMT sort");

libsolidity/formal/SSAVariable.cpp

@@ -29,5 +29,12 @@ SSAVariable::SSAVariable()
 void SSAVariable::resetIndex()
 {
 	m_currentIndex = 0;
-	m_nextFreeIndex = make_unique<unsigned>(1);
+	m_nextFreeIndex = 1;
+}
+
+void SSAVariable::setIndex(unsigned _index)
+{
+	m_currentIndex = _index;
+	if (m_nextFreeIndex <= _index)
+		m_nextFreeIndex = _index + 1;
 }

libsolidity/formal/SSAVariable.h

@@ -29,7 +29,10 @@ class SSAVariable
 {
 public:
 	SSAVariable();
+	/// Resets index to 0 and next index to 1.
 	void resetIndex();
+	/// Sets index to _index and only adjusts next if next <= _index.
+	void setIndex(unsigned _index);
 
 	/// This function returns the current index of this SSA variable.
 	unsigned index() const { return m_currentIndex; }
@@ -37,12 +40,12 @@ public:
 
 	unsigned operator++()
 	{
-		return m_currentIndex = (*m_nextFreeIndex)++;
+		return m_currentIndex = m_nextFreeIndex++;
 	}
 
 private:
 	unsigned m_currentIndex;
-	std::unique_ptr<unsigned> m_nextFreeIndex;
+	unsigned m_nextFreeIndex;
 };
 
 }

libsolidity/formal/SolverInterface.h

@@ -28,6 +28,7 @@
 #include <boost/noncopyable.hpp>
 #include <cstdio>
 #include <map>
+#include <memory>
 #include <string>
 #include <vector>
 
@@ -63,7 +64,8 @@ class Expression
 	friend class SolverInterface;
 public:
 	explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
-	explicit Expression(frontend::TypePointer _type): Expression(_type->toString(), {}, std::make_shared<SortSort>(smtSort(*_type))) {}
+	explicit Expression(frontend::TypePointer _type): Expression(_type->toString(true), {}, std::make_shared<SortSort>(smtSort(*_type))) {}
+	explicit Expression(std::shared_ptr<SortSort> _sort): Expression("", {}, _sort) {}
 	Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
 	Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
 	Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {}
@@ -76,6 +78,13 @@ public:
 
 	bool hasCorrectArity() const
 	{
+		if (name == "tuple_constructor")
+		{
+			auto tupleSort = std::dynamic_pointer_cast<TupleSort>(sort);
+			solAssert(tupleSort, "");
+			return arguments.size() == tupleSort->components.size();
+		}
+
 		static std::map<std::string, unsigned> const operatorsArity{
 			{"ite", 3},
 			{"not", 1},
@@ -138,8 +147,7 @@ public:
 	/// The function is pure and returns the modified array.
 	static Expression store(Expression _array, Expression _index, Expression _element)
 	{
-		solAssert(_array.sort->kind == Kind::Array, "");
-		std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
+		auto arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
 		solAssert(arraySort, "");
 		solAssert(_index.sort, "");
 		solAssert(_element.sort, "");
@@ -180,6 +188,20 @@ public:
 		);
 	}
 
+	static Expression tuple_constructor(Expression _tuple, std::vector<Expression> _arguments)
+	{
+		solAssert(_tuple.sort->kind == Kind::Sort, "");
+		auto sortSort = std::dynamic_pointer_cast<SortSort>(_tuple.sort);
+		auto tupleSort = std::dynamic_pointer_cast<TupleSort>(sortSort->inner);
+		solAssert(tupleSort, "");
+		solAssert(_arguments.size() == tupleSort->components.size(), "");
+		return Expression(
+			"tuple_constructor",
+			std::move(_arguments),
+			tupleSort
+		);
+	}
+
 	friend Expression operator!(Expression _a)
 	{
 		return Expression("not", std::move(_a), Kind::Bool);

libsolidity/formal/SymbolicState.cpp

@@ -47,7 +47,7 @@ Expression SymbolicState::balance()
 
 Expression SymbolicState::balance(Expression _address)
 {
-	return Expression::select(m_balances.currentValue(), move(_address));
+	return Expression::select(m_balances.elements(), move(_address));
 }
 
 void SymbolicState::transfer(Expression _from, Expression _to, Expression _value)
@@ -72,11 +72,13 @@ void SymbolicState::transfer(Expression _from, Expression _to, Expression _value
 void SymbolicState::addBalance(Expression _address, Expression _value)
 {
 	auto newBalances = Expression::store(
-		m_balances.currentValue(),
+		m_balances.elements(),
 		_address,
 		balance(_address) + move(_value)
 	);
+	auto oldLength = m_balances.length();
 	m_balances.increaseIndex();
-	m_context.addAssertion(newBalances == m_balances.currentValue());
+	m_context.addAssertion(m_balances.elements() == newBalances);
+	m_context.addAssertion(m_balances.length() == oldLength);
 }
 

libsolidity/formal/SymbolicTypes.cpp

@@ -21,6 +21,7 @@
 #include <libsolidity/ast/Types.h>
 #include <libsolutil/CommonData.h>
 #include <memory>
+#include <vector>
 
 using namespace std;
 
@@ -55,17 +56,18 @@ SortPointer smtSort(frontend::Type const& _type)
 	}
 	case Kind::Array:
 	{
+		shared_ptr<ArraySort> array;
 		if (isMapping(_type.category()))
 		{
 			auto mapType = dynamic_cast<frontend::MappingType const*>(&_type);
 			solAssert(mapType, "");
-			return make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
+			array = make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
 		}
 		else if (isStringLiteral(_type.category()))
 		{
 			auto stringLitType = dynamic_cast<frontend::StringLiteralType const*>(&_type);
 			solAssert(stringLitType, "");
-			return make_shared<ArraySort>(SortProvider::intSort, SortProvider::intSort);
+			array = make_shared<ArraySort>(SortProvider::intSort, SortProvider::intSort);
 		}
 		else
 		{
@@ -78,8 +80,25 @@ SortPointer smtSort(frontend::Type const& _type)
 				solAssert(false, "");
 
 			solAssert(arrayType, "");
-			return make_shared<ArraySort>(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType()));
+			array = make_shared<ArraySort>(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType()));
 		}
+
+		string tupleName;
+		if (
+			auto arrayType = dynamic_cast<ArrayType const*>(&_type);
+			(arrayType && arrayType->isString()) ||
+			_type.category() == frontend::Type::Category::ArraySlice ||
+			_type.category() == frontend::Type::Category::StringLiteral
+		)
+			tupleName = "bytes_tuple";
+		else
+			tupleName = _type.toString(true) + "_tuple";
+
+		return make_shared<TupleSort>(
+			tupleName,
+			vector<string>{tupleName + "_accessor_array", tupleName + "_accessor_length"},
+			vector<SortPointer>{array, SortProvider::intSort}
+		);
 	}
 	case Kind::Tuple:
 	{
@@ -219,9 +238,7 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		else
 			var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
 	}
-	else if (isMapping(_type.category()))
-		var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _context);
-	else if (isArray(_type.category()))
+	else if (isMapping(_type.category()) || isArray(_type.category()))
 		var = make_shared<SymbolicArrayVariable>(type, type, _uniqueName, _context);
 	else if (isTuple(_type.category()))
 		var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _context);
@@ -349,11 +366,26 @@ Expression zeroValue(frontend::TypePointer const& _type)
 			return Expression(false);
 		if (isArray(_type->category()) || isMapping(_type->category()))
 		{
+			auto tupleSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
+			solAssert(tupleSort, "");
+			auto sortSort = make_shared<SortSort>(tupleSort->components.front());
+
+			std::optional<Expression> zeroArray;
+			auto length = bigint(0);
 			if (auto arrayType = dynamic_cast<ArrayType const*>(_type))
-				return Expression::const_array(Expression(arrayType), zeroValue(arrayType->baseType()));
-			auto mappingType = dynamic_cast<MappingType const*>(_type);
-			solAssert(mappingType, "");
-			return Expression::const_array(Expression(mappingType), zeroValue(mappingType->valueType()));
+			{
+				zeroArray = Expression::const_array(Expression(sortSort), zeroValue(arrayType->baseType()));
+				if (!arrayType->isDynamicallySized())
+					length = bigint(arrayType->length());
+			}
+			else if (auto mappingType = dynamic_cast<MappingType const*>(_type))
+				zeroArray = Expression::const_array(Expression(sortSort), zeroValue(mappingType->valueType()));
+			else
+				solAssert(false, "");
+
+			solAssert(zeroArray, "");
+			return Expression::tuple_constructor(Expression(_type), vector<Expression>{*zeroArray, length});
+
 		}
 		solAssert(false, "");
 	}

libsolidity/formal/SymbolicVariables.cpp

@@ -86,6 +86,12 @@ smt::Expression SymbolicVariable::resetIndex()
 	return currentValue();
 }
 
+smt::Expression SymbolicVariable::setIndex(unsigned _index)
+{
+	m_ssa->setIndex(_index);
+	return currentValue();
+}
+
 smt::Expression SymbolicVariable::increaseIndex()
 {
 	++(*m_ssa);
@@ -179,6 +185,12 @@ smt::Expression SymbolicFunctionVariable::resetIndex()
 	return m_abstract.resetIndex();
 }
 
+smt::Expression SymbolicFunctionVariable::setIndex(unsigned _index)
+{
+	SymbolicVariable::setIndex(_index);
+	return m_abstract.setIndex(_index);
+}
+
 smt::Expression SymbolicFunctionVariable::increaseIndex()
 {
 	++(*m_ssa);
@@ -197,46 +209,6 @@ void SymbolicFunctionVariable::resetDeclaration()
 	m_declaration = m_context.newVariable(currentName(), m_sort);
 }
 
-SymbolicMappingVariable::SymbolicMappingVariable(
-	frontend::TypePointer _type,
-	string _uniqueName,
-	EncodingContext& _context
-):
-	SymbolicVariable(_type, _type, move(_uniqueName), _context)
-{
-	solAssert(isMapping(m_type->category()), "");
-}
-
-SymbolicArrayVariable::SymbolicArrayVariable(
-	frontend::TypePointer _type,
-	frontend::TypePointer _originalType,
-	string _uniqueName,
-	EncodingContext& _context
-):
-	SymbolicVariable(_type, _originalType, move(_uniqueName), _context)
-{
-	solAssert(isArray(m_type->category()), "");
-}
-
-SymbolicArrayVariable::SymbolicArrayVariable(
-	SortPointer _sort,
-	string _uniqueName,
-	EncodingContext& _context
-):
-	SymbolicVariable(move(_sort), move(_uniqueName), _context)
-{
-	solAssert(m_sort->kind == Kind::Array, "");
-}
-
-smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
-{
-	optional<smt::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
-	if (conversion)
-		return *conversion;
-
-	return SymbolicVariable::currentValue(_targetType);
-}
-
 SymbolicEnumVariable::SymbolicEnumVariable(
 	frontend::TypePointer _type,
 	string _uniqueName,
@@ -286,3 +258,62 @@ smt::Expression SymbolicTupleVariable::component(
 
 	return smt::Expression::tuple_get(currentValue(), _index);
 }
+
+SymbolicArrayVariable::SymbolicArrayVariable(
+	frontend::TypePointer _type,
+	frontend::TypePointer _originalType,
+	string _uniqueName,
+	EncodingContext& _context
+):
+	SymbolicVariable(_type, _originalType, move(_uniqueName), _context),
+	m_pair(
+		smtSort(*_type),
+		m_uniqueName + "_length_pair",
+		m_context
+	)
+{
+	solAssert(isArray(m_type->category()) || isMapping(m_type->category()), "");
+}
+
+SymbolicArrayVariable::SymbolicArrayVariable(
+	SortPointer _sort,
+	string _uniqueName,
+	EncodingContext& _context
+):
+	SymbolicVariable(move(_sort), move(_uniqueName), _context),
+	m_pair(
+		std::make_shared<TupleSort>(
+			"array_length_pair",
+			std::vector<std::string>{"array", "length"},
+			std::vector<SortPointer>{m_sort, SortProvider::intSort}
+		),
+		m_uniqueName + "_array_length_pair",
+		m_context
+	)
+{
+	solAssert(m_sort->kind == Kind::Array, "");
+}
+
+smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
+{
+	optional<smt::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
+	if (conversion)
+		return *conversion;
+
+	return m_pair.currentValue();
+}
+
+smt::Expression SymbolicArrayVariable::valueAtIndex(int _index) const
+{
+	return m_pair.valueAtIndex(_index);
+}
+
+smt::Expression SymbolicArrayVariable::elements()
+{
+	return m_pair.component(0);
+}
+
+smt::Expression SymbolicArrayVariable::length()
+{
+	return m_pair.component(1);
+}

libsolidity/formal/SymbolicVariables.h

@@ -56,6 +56,7 @@ public:
 	virtual Expression valueAtIndex(int _index) const;
 	virtual std::string nameAtIndex(int _index) const;
 	virtual Expression resetIndex();
+	virtual Expression setIndex(unsigned _index);
 	virtual Expression increaseIndex();
 	virtual Expression operator()(std::vector<Expression> /*_arguments*/) const
 	{
@@ -169,6 +170,7 @@ public:
 	Expression functionValueAtIndex(int _index) const;
 
 	Expression resetIndex() override;
+	Expression setIndex(unsigned _index) override;
 	Expression increaseIndex() override;
 
 	Expression operator()(std::vector<Expression> _arguments) const override;
@@ -189,42 +191,6 @@ private:
 	};
 };
 
-/**
- * Specialization of SymbolicVariable for Mapping
- */
-class SymbolicMappingVariable: public SymbolicVariable
-{
-public:
-	SymbolicMappingVariable(
-		frontend::TypePointer _type,
-		std::string _uniqueName,
-		EncodingContext& _context
-	);
-};
-
-/**
- * Specialization of SymbolicVariable for Array
- */
-class SymbolicArrayVariable: public SymbolicVariable
-{
-public:
-	SymbolicArrayVariable(
-		frontend::TypePointer _type,
-		frontend::TypePointer _originalTtype,
-		std::string _uniqueName,
-		EncodingContext& _context
-	);
-	SymbolicArrayVariable(
-		SortPointer _sort,
-		std::string _uniqueName,
-		EncodingContext& _context
-	);
-
-	SymbolicArrayVariable(SymbolicArrayVariable&&) = default;
-
-	Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
-};
-
 /**
  * Specialization of SymbolicVariable for Enum
  */
@@ -263,4 +229,38 @@ public:
 	);
 };
 
+/**
+ * Specialization of SymbolicVariable for Array
+ */
+class SymbolicArrayVariable: public SymbolicVariable
+{
+public:
+	SymbolicArrayVariable(
+		frontend::TypePointer _type,
+		frontend::TypePointer _originalTtype,
+		std::string _uniqueName,
+		EncodingContext& _context
+	);
+	SymbolicArrayVariable(
+		SortPointer _sort,
+		std::string _uniqueName,
+		EncodingContext& _context
+	);
+
+	SymbolicArrayVariable(SymbolicArrayVariable&&) = default;
+
+	Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
+	Expression valueAtIndex(int _index) const override;
+	Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); }
+	Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); }
+	Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); }
+	Expression elements();
+	Expression length();
+
+	SortPointer tupleSort() { return m_pair.sort(); }
+
+private:
+	SymbolicTupleVariable m_pair;
+};
+
 }

libsolidity/formal/Z3Interface.cpp

@@ -198,6 +198,15 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 			size_t index = std::stoi(_expr.arguments[1].name);
 			return z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, z3Sort(*_expr.arguments[0].sort), index))(arguments[0]);
 		}
+		else if (n == "tuple_constructor")
+		{
+			auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, z3Sort(*_expr.sort)));
+			solAssert(constructor.arity() == arguments.size(), "");
+			z3::expr_vector args(m_context);
+			for (auto const& arg: arguments)
+				args.push_back(arg);
+			return constructor(args);
+		}
 
 		solAssert(false, "");
 	}

libsolidity/interface/CompilerStack.cpp

@@ -733,11 +733,7 @@ Json::Value const& CompilerStack::contractABI(Contract const& _contract) const
 
 	solAssert(_contract.contract, "");
 
-	// caches the result
-	if (!_contract.abi)
-		_contract.abi = make_unique<Json::Value>(ABI::generate(*_contract.contract));
-
-	return *_contract.abi;
+	return _contract.abi.init([&]{ return ABI::generate(*_contract.contract); });
 }
 
 Json::Value const& CompilerStack::storageLayout(string const& _contractName) const
@@ -755,11 +751,7 @@ Json::Value const& CompilerStack::storageLayout(Contract const& _contract) const
 
 	solAssert(_contract.contract, "");
 
-	// caches the result
-	if (!_contract.storageLayout)
-		_contract.storageLayout = make_unique<Json::Value>(StorageLayout().generate(*_contract.contract));
-
-	return *_contract.storageLayout;
+	return _contract.storageLayout.init([&]{ return StorageLayout().generate(*_contract.contract); });
 }
 
 Json::Value const& CompilerStack::natspecUser(string const& _contractName) const
@@ -777,11 +769,7 @@ Json::Value const& CompilerStack::natspecUser(Contract const& _contract) const
 
 	solAssert(_contract.contract, "");
 
-	// caches the result
-	if (!_contract.userDocumentation)
-		_contract.userDocumentation = make_unique<Json::Value>(Natspec::userDocumentation(*_contract.contract));
-
-	return *_contract.userDocumentation;
+	return _contract.userDocumentation.init([&]{ return Natspec::userDocumentation(*_contract.contract); });
 }
 
 Json::Value const& CompilerStack::natspecDev(string const& _contractName) const
@@ -799,11 +787,7 @@ Json::Value const& CompilerStack::natspecDev(Contract const& _contract) const
 
 	solAssert(_contract.contract, "");
 
-	// caches the result
-	if (!_contract.devDocumentation)
-		_contract.devDocumentation = make_unique<Json::Value>(Natspec::devDocumentation(*_contract.contract));
-
-	return *_contract.devDocumentation;
+	return _contract.devDocumentation.init([&]{ return Natspec::devDocumentation(*_contract.contract); });
 }
 
 Json::Value CompilerStack::methodIdentifiers(string const& _contractName) const
@@ -832,11 +816,7 @@ string const& CompilerStack::metadata(Contract const& _contract) const
 
 	solAssert(_contract.contract, "");
 
-	// cache the result
-	if (!_contract.metadata)
-		_contract.metadata = make_unique<string>(createMetadata(_contract));
-
-	return *_contract.metadata;
+	return _contract.metadata.init([&]{ return createMetadata(_contract); });
 }
 
 Scanner const& CompilerStack::scanner(string const& _sourceName) const

libsolidity/interface/CompilerStack.h

@@ -37,6 +37,7 @@
 
 #include <libsolutil/Common.h>
 #include <libsolutil/FixedHash.h>
+#include <libsolutil/LazyInit.h>
 
 #include <boost/noncopyable.hpp>
 #include <json/json.h>
@@ -342,11 +343,11 @@ private:
 		std::string yulIROptimized; ///< Optimized experimental Yul IR code.
 		std::string ewasm; ///< Experimental Ewasm text representation
 		evmasm::LinkerObject ewasmObject; ///< Experimental Ewasm code
-		mutable std::unique_ptr<std::string const> metadata; ///< The metadata json that will be hashed into the chain.
-		mutable std::unique_ptr<Json::Value const> abi;
-		mutable std::unique_ptr<Json::Value const> storageLayout;
-		mutable std::unique_ptr<Json::Value const> userDocumentation;
-		mutable std::unique_ptr<Json::Value const> devDocumentation;
+		util::LazyInit<std::string const> metadata; ///< The metadata json that will be hashed into the chain.
+		util::LazyInit<Json::Value const> abi;
+		util::LazyInit<Json::Value const> storageLayout;
+		util::LazyInit<Json::Value const> userDocumentation;
+		util::LazyInit<Json::Value const> devDocumentation;
 		mutable std::unique_ptr<std::string const> sourceMapping;
 		mutable std::unique_ptr<std::string const> runtimeSourceMapping;
 	};

libsolidity/interface/StandardCompiler.cpp

@@ -30,6 +30,7 @@
 #include <libevmasm/Instruction.h>
 #include <libsolutil/JSON.h>
 #include <libsolutil/Keccak256.h>
+#include <libsolutil/CommonData.h>
 
 #include <boost/algorithm/string/predicate.hpp>
 
@@ -1127,16 +1128,29 @@ Json::Value StandardCompiler::compileYul(InputsAndSettings _inputsAndSettings)
 
 	stack.optimize();
 
-	MachineAssemblyObject object = stack.assemble(AssemblyStack::Machine::EVM);
+	MachineAssemblyObject object;
+	MachineAssemblyObject runtimeObject;
+	tie(object, runtimeObject) = stack.assembleAndGuessRuntime();
 
-	if (isArtifactRequested(
-		_inputsAndSettings.outputSelection,
-		sourceName,
-		contractName,
-		{ "evm.bytecode", "evm.bytecode.object", "evm.bytecode.opcodes", "evm.bytecode.sourceMap", "evm.bytecode.linkReferences" },
-		wildcardMatchesExperimental
-	))
-		output["contracts"][sourceName][contractName]["evm"]["bytecode"] = collectEVMObject(*object.bytecode, object.sourceMappings.get(), false);
+	for (string const& objectKind: vector<string>{"bytecode", "deployedBytecode"})
+	{
+		auto artifacts = util::applyMap(
+			vector<string>{"", ".object", ".opcodes", ".sourceMap", ".linkReferences"},
+			[&](auto const& _s) { return "evm." + objectKind + _s; }
+		);
+		if (isArtifactRequested(
+			_inputsAndSettings.outputSelection,
+			sourceName,
+			contractName,
+			artifacts,
+			wildcardMatchesExperimental
+		))
+		{
+			MachineAssemblyObject const& o = objectKind == "bytecode" ? object : runtimeObject;
+			if (o.bytecode)
+				output["contracts"][sourceName][contractName]["evm"][objectKind] = collectEVMObject(*o.bytecode, o.sourceMappings.get(), false);
+		}
+	}
 
 	if (isArtifactRequested(_inputsAndSettings.outputSelection, sourceName, contractName, "irOptimized", wildcardMatchesExperimental))
 		output["contracts"][sourceName][contractName]["irOptimized"] = stack.print();