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

Changelog.md

@@ -2,24 +2,39 @@
 
 
 
-### 0.7.1 (unreleased)
+### 0.7.2 (unreleased)
 
 Language Features:
- * Allow function definitions outside of contracts, behaving much like internal library functions.
 
 
+Compiler Features:
+ * SMTChecker: Support structs.
+ * Yul Optimizer: Prune unused parameters in functions.
+
+Bugfixes:
+
+
+### 0.7.1 (2020-09-02)
+
+Language Features:
+ * Allow function definitions outside of contracts, behaving much like internal library functions.
+ * Code generator: Implementing copying structs from calldata to storage.
+
 Compiler Features:
  * SMTChecker: Add underflow and overflow as verification conditions in the CHC engine.
- * Standard JSON Interface: Do not run EVM bytecode code generation, if only Yul IR or EWasm output is requested.
- * Yul: Report error when using non-string literals for ``datasize()``, ``dataoffset()``, ``linkersymbol()``, ``loadimmutable()``, ``setimmutable()``.
- * Yul Optimizer: LoopInvariantCodeMotion can move reading operations outside for-loops as long as the affected area is not modified inside the loop.
- * SMTChecker: Support conditional operator.
  * SMTChecker: Support bitwise or, xor and not operators.
+ * SMTChecker: Support conditional operator.
+ * Standard JSON Interface: Do not run EVM bytecode code generation, if only Yul IR or EWasm output is requested.
+ * Yul Optimizer: LoopInvariantCodeMotion can move reading operations outside for-loops as long as the affected area is not modified inside the loop.
+ * Yul: Report error when using non-string literals for ``datasize()``, ``dataoffset()``, ``linkersymbol()``, ``loadimmutable()``, ``setimmutable()``.
 
 Bugfixes:
  * AST: Remove ``null`` member values also when the compiler is used in standard-json-mode.
+ * General: Allow `type(Contract).name` for abstract contracts and interfaces.
+ * Immutables: Disallow assigning immutables more than once during their declaration.
  * Immutables: Properly treat complex assignment and increment/decrement as both reading and writing and thus disallow it everywhere for immutable variables.
  * Optimizer: Keep side-effects of ``x`` in ``byte(a, shr(b, x))`` even if the constants ``a`` and ``b`` would make the expression zero unconditionally. This optimizer rule is very hard if not impossible to trigger in a way that it can result in invalid code, though.
+ * References Resolver: Fix internal bug when using constructor for library.
  * Scanner: Fix bug where whitespace would be allowed within the ``->`` token (e.g. ``function f() -   > x {}`` becomes invalid in inline assembly and Yul).
  * SMTChecker: Fix internal error in BMC function inlining.
  * SMTChecker: Fix internal error on array implicit conversion.
@@ -28,14 +43,11 @@ Bugfixes:
  * SMTChecker: Fix internal error on tuple assignment.
  * SMTChecker: Fix internal error on tuples of one element that have tuple type.
  * SMTChecker: Fix soundness of array ``pop``.
- * References Resolver: Fix internal bug when using constructor for library.
- * Yul Optimizer: Make function inlining order more resilient to whether or not unrelated source files are present.
- * Yul Optimizer: Ensure that Yul keywords are not mistakenly used by the NameDispenser and VarNameCleaners. The bug would manifest as uncompilable code.
- * Type Checker: Disallow signed literals as exponent in exponentiation operator.
- * Allow `type(Contract).name` for abstract contracts and interfaces.
- * Type Checker: Disallow structs containing nested mapping in memory as parameters for library functions.
  * Type Checker: Disallow ``using for`` directive inside interfaces.
- * Immutables: Disallow assigning immutables more than once during their declaration.
+ * Type Checker: Disallow signed literals as exponent in exponentiation operator.
+ * Type Checker: Disallow structs containing nested mapping in memory as parameters for library functions.
+ * Yul Optimizer: Ensure that Yul keywords are not mistakenly used by the NameDispenser and VarNameCleaners. The bug would manifest as uncompilable code.
+ * Yul Optimizer: Make function inlining order more resilient to whether or not unrelated source files are present.
 
 
 ### 0.7.0 (2020-07-28)

cmake/EthToolchains.cmake

@@ -1,5 +1,7 @@
 # Require C++17.
+if (NOT DEFINED CMAKE_CXX_STANDARD)
   set(CMAKE_CXX_STANDARD 17) # This requires at least CMake 3.8 to accept this C++17 flag.
+endif ()
 set(CMAKE_CXX_STANDARD_REQUIRED TRUE)
 set(CMAKE_CXX_EXTENSIONS OFF)
 

docs/bugs_by_version.json

@@ -1185,5 +1185,9 @@
     "0.7.0": {
         "bugs": [],
         "released": "2020-07-28"
+    },
+    "0.7.1": {
+        "bugs": [],
+        "released": "2020-09-02"
     }
 }

docs/contracts/functions.rst

@@ -277,7 +277,7 @@ neither a receive Ether nor a payable fallback function is present, the
 contract cannot receive Ether through regular transactions and throws an
 exception.
 
-In the worst case, the fallback function can only rely on 2300 gas being
+In the worst case, the ``receive`` function can only rely on 2300 gas being
 available (for example when ``send`` or ``transfer`` is used), leaving little
 room to perform other operations except basic logging. The following operations
 will consume more gas than the 2300 gas stipend:

libsolidity/CMakeLists.txt

@@ -100,6 +100,8 @@ set(sources
 	formal/EncodingContext.h
 	formal/ModelChecker.cpp
 	formal/ModelChecker.h
+	formal/Predicate.cpp
+	formal/Predicate.h
 	formal/SMTEncoder.cpp
 	formal/SMTEncoder.h
 	formal/SSAVariable.cpp

libsolidity/codegen/LValue.cpp

@@ -357,7 +357,15 @@ void StorageItem::storeValue(Type const& _sourceType, SourceLocation const& _loc
 				"Struct assignment with conversion."
 			);
 			solAssert(!structType.containsNestedMapping(), "");
-			solAssert(sourceType.location() != DataLocation::CallData, "Structs in calldata not supported.");
+			if (sourceType.location() == DataLocation::CallData)
+			{
+				solAssert(sourceType.sizeOnStack() == 1, "");
+				solAssert(structType.sizeOnStack() == 1, "");
+				m_context << Instruction::DUP2 << Instruction::DUP2;
+				m_context.callYulFunction(m_context.utilFunctions().updateStorageValueFunction(sourceType, structType, 0), 2, 0);
+			}
+			else
+			{
 				for (auto const& member: structType.members(nullptr))
 				{
 					// assign each member that can live outside of storage
@@ -390,6 +398,7 @@ void StorageItem::storeValue(Type const& _sourceType, SourceLocation const& _loc
 					// stack: source_ref target_ref target_off source_value... target_member_ref target_member_byte_off
 					StorageItem(m_context, *memberType).storeValue(*sourceMemberType, _location, true);
 				}
+			}
 			// stack layout: source_ref target_ref
 			solAssert(sourceType.sizeOnStack() == 1, "Unexpected source size.");
 			if (_move)

libsolidity/codegen/YulUtilFunctions.cpp

@@ -964,7 +964,7 @@ string YulUtilFunctions::storageArrayPushFunction(ArrayType const& _type)
 			("dataAreaFunction", arrayDataAreaFunction(_type))
 			("isByteArray", _type.isByteArray())
 			("indexAccess", storageArrayIndexAccessFunction(_type))
-			("storeValue", updateStorageValueFunction(*_type.baseType()))
+			("storeValue", updateStorageValueFunction(*_type.baseType(), *_type.baseType()))
 			("maxArrayLength", (u256(1) << 64).str())
 			("shl", shiftLeftFunctionDynamic())
 			("shr", shiftRightFunction(248))
@@ -994,7 +994,7 @@ string YulUtilFunctions::storageArrayPushZeroFunction(ArrayType const& _type)
 			("functionName", functionName)
 			("fetchLength", arrayLengthFunction(_type))
 			("indexAccess", storageArrayIndexAccessFunction(_type))
-			("storeValue", updateStorageValueFunction(*_type.baseType()))
+			("storeValue", updateStorageValueFunction(*_type.baseType(), *_type.baseType()))
 			("maxArrayLength", (u256(1) << 64).str())
 			("zeroValueFunction", zeroValueFunction(*_type.baseType()))
 			.render();
@@ -1404,6 +1404,25 @@ string YulUtilFunctions::mappingIndexAccessFunction(MappingType const& _mappingT
 
 string YulUtilFunctions::readFromStorage(Type const& _type, size_t _offset, bool _splitFunctionTypes)
 {
+	if (_type.isValueType())
+		return readFromStorageValueType(_type, _offset, _splitFunctionTypes);
+	else
+	{
+		solAssert(_offset == 0, "");
+		return readFromStorageReferenceType(_type);
+	}
+}
+
+string YulUtilFunctions::readFromStorageDynamic(Type const& _type, bool _splitFunctionTypes)
+{
+	solAssert(_type.isValueType(), "");
+	return readFromStorageValueTypeDynamic(_type, _splitFunctionTypes);
+}
+
+string YulUtilFunctions::readFromStorageValueType(Type const& _type, size_t _offset, bool _splitFunctionTypes)
+{
+	solAssert(_type.isValueType(), "");
+
 	if (_type.category() == Type::Category::Function)
 		solUnimplementedAssert(!_splitFunctionTypes, "");
 	string functionName =
@@ -1413,6 +1432,7 @@ string YulUtilFunctions::readFromStorage(Type const& _type, size_t _offset, bool
 			to_string(_offset) +
 			"_" +
 			_type.identifier();
+
 	return m_functionCollector.createFunction(functionName, [&] {
 		solAssert(_type.sizeOnStack() == 1, "");
 		return Whiskers(R"(
@@ -1425,13 +1445,14 @@ string YulUtilFunctions::readFromStorage(Type const& _type, size_t _offset, bool
 				.render();
 	});
 }
-
+string YulUtilFunctions::readFromStorageValueTypeDynamic(Type const& _type, bool _splitFunctionTypes)
-string YulUtilFunctions::readFromStorageDynamic(Type const& _type, bool _splitFunctionTypes)
 {
+	solAssert(_type.isValueType(), "");
 	if (_type.category() == Type::Category::Function)
 		solUnimplementedAssert(!_splitFunctionTypes, "");
+
 	string functionName =
-		"read_from_storage_dynamic" +
+		"read_from_storage_value_type_dynamic" +
 		string(_splitFunctionTypes ? "split_" : "") +
 		"_" +
 		_type.identifier();
@@ -1447,6 +1468,55 @@ string YulUtilFunctions::readFromStorageDynamic(Type const& _type, bool _splitFu
 		.render();
 	});
 }
+string YulUtilFunctions::readFromStorageReferenceType(Type const& _type)
+{
+	solUnimplementedAssert(_type.category() == Type::Category::Struct, "");
+
+	string functionName = "read_from_storage_reference_type_" + _type.identifier();
+
+	auto const& structType = dynamic_cast<StructType const&>(_type);
+	solAssert(structType.location() == DataLocation::Memory, "");
+	MemberList::MemberMap structMembers = structType.nativeMembers(nullptr);
+	vector<map<string, string>> memberSetValues(structMembers.size());
+	for (size_t i = 0; i < structMembers.size(); ++i)
+	{
+		auto const& [memberSlotDiff, memberStorageOffset] = structType.storageOffsetsOfMember(structMembers[i].name);
+
+		memberSetValues[i]["setMember"] = Whiskers(R"(
+			{
+				let <memberValues> := <readFromStorage>(add(slot, <memberSlotDiff>)<?hasOffset>, <memberStorageOffset></hasOffset>)
+				<writeToMemory>(add(value, <memberMemoryOffset>), <memberValues>)
+			}
+		)")
+		("memberValues", suffixedVariableNameList("memberValue_", 0, structMembers[i].type->stackItems().size()))
+		("memberMemoryOffset", structType.memoryOffsetOfMember(structMembers[i].name).str())
+		("memberSlotDiff",  memberSlotDiff.str())
+		("memberStorageOffset", to_string(memberStorageOffset))
+		("readFromStorage",
+			structMembers[i].type->isValueType() ?
+				readFromStorageDynamic(*structMembers[i].type, true) :
+				readFromStorage(*structMembers[i].type, memberStorageOffset, true)
+		)
+		("writeToMemory", writeToMemoryFunction(*structMembers[i].type))
+		("hasOffset", structMembers[i].type->isValueType())
+		.render();
+	}
+
+	return m_functionCollector.createFunction(functionName, [&] {
+		return Whiskers(R"(
+			function <functionName>(slot) -> value {
+				value := <allocStruct>()
+				<#member>
+					<setMember>
+				</member>
+			}
+		)")
+		("functionName", functionName)
+		("allocStruct", allocateMemoryStructFunction(structType))
+		("member", memberSetValues)
+		.render();
+	});
+}
 
 string YulUtilFunctions::readFromMemory(Type const& _type)
 {
@@ -1458,18 +1528,25 @@ string YulUtilFunctions::readFromCalldata(Type const& _type)
 	return readFromMemoryOrCalldata(_type, true);
 }
 
-string YulUtilFunctions::updateStorageValueFunction(Type const& _type, std::optional<unsigned> const& _offset)
+string YulUtilFunctions::updateStorageValueFunction(
+	Type const& _fromType,
+	Type const& _toType,
+	std::optional<unsigned> const& _offset
+)
 {
 	string const functionName =
 		"update_storage_value_" +
 		(_offset.has_value() ? ("offset_" + to_string(*_offset)) : "") +
-		_type.identifier();
+		_fromType.identifier() +
+		"_to_" +
+		_toType.identifier();
 
 	return m_functionCollector.createFunction(functionName, [&] {
-		if (_type.isValueType())
+		if (_toType.isValueType())
 		{
-			solAssert(_type.storageBytes() <= 32, "Invalid storage bytes size.");
+			solAssert(_fromType.isImplicitlyConvertibleTo(_toType), "");
-			solAssert(_type.storageBytes() > 0, "Invalid storage bytes size.");
+			solAssert(_toType.storageBytes() <= 32, "Invalid storage bytes size.");
+			solAssert(_toType.storageBytes() > 0, "Invalid storage bytes size.");
 
 			return Whiskers(R"(
 				function <functionName>(slot, <offset>value) {
@@ -1480,19 +1557,83 @@ string YulUtilFunctions::updateStorageValueFunction(Type const& _type, std::opti
 			("functionName", functionName)
 			("update",
 				_offset.has_value() ?
-					updateByteSliceFunction(_type.storageBytes(), *_offset) :
+					updateByteSliceFunction(_toType.storageBytes(), *_offset) :
-					updateByteSliceFunctionDynamic(_type.storageBytes())
+					updateByteSliceFunctionDynamic(_toType.storageBytes())
 			)
 			("offset", _offset.has_value() ? "" : "offset, ")
-			("prepare", prepareStoreFunction(_type))
+			("prepare", prepareStoreFunction(_toType))
 			.render();
 		}
 		else
 		{
-			if (_type.category() == Type::Category::Array)
+			auto const* toReferenceType = dynamic_cast<ReferenceType const*>(&_toType);
-				solUnimplementedAssert(false, "");
+			auto const* fromReferenceType = dynamic_cast<ReferenceType const*>(&_toType);
-			else if (_type.category() == Type::Category::Struct)
+			solAssert(fromReferenceType && toReferenceType, "");
+			solAssert(*toReferenceType->copyForLocation(
+				fromReferenceType->location(),
+				fromReferenceType->isPointer()
+			).get() == *fromReferenceType, "");
+
+			if (_toType.category() == Type::Category::Array)
 				solUnimplementedAssert(false, "");
+			else if (_toType.category() == Type::Category::Struct)
+			{
+				solAssert(_fromType.category() == Type::Category::Struct, "");
+				auto const& fromStructType = dynamic_cast<StructType const&>(_fromType);
+				auto const& toStructType = dynamic_cast<StructType const&>(_toType);
+				solAssert(fromStructType.structDefinition() == toStructType.structDefinition(), "");
+				solAssert(fromStructType.location() != DataLocation::Storage, "");
+				solUnimplementedAssert(_offset.has_value() && _offset.value() == 0, "");
+
+				Whiskers templ(R"(
+					function <functionName>(slot, value) {
+						<#member>
+						{
+							<updateMemberCall>
+						}
+						</member>
+					}
+				)");
+				templ("functionName", functionName);
+
+				MemberList::MemberMap structMembers = fromStructType.nativeMembers(nullptr);
+
+				vector<map<string, string>> memberParams(structMembers.size());
+				for (size_t i = 0; i < structMembers.size(); ++i)
+				{
+					solAssert(structMembers[i].type->memoryHeadSize() == 32, "");
+					bool fromCalldata = fromStructType.location() == DataLocation::CallData;
+					auto const& [slotDiff, offset] = toStructType.storageOffsetsOfMember(structMembers[i].name);
+					memberParams[i]["updateMemberCall"] = Whiskers(R"(
+						let <memberValues> := <loadFromMemoryOrCalldata>(add(value, <memberOffset>))
+						<updateMember>(add(slot, <memberStorageSlotDiff>), <?hasOffset><memberStorageOffset>,</hasOffset> <memberValues>)
+					)")
+					("memberValues", suffixedVariableNameList(
+						"memberValue_",
+						0,
+						structMembers[i].type->stackItems().size()
+					))
+					("hasOffset", structMembers[i].type->isValueType())
+					(
+						"updateMember",
+						structMembers[i].type->isValueType() ?
+							updateStorageValueFunction(*structMembers[i].type, *structMembers[i].type) :
+							updateStorageValueFunction(*structMembers[i].type, *structMembers[i].type, offset)
+					)
+					("memberStorageSlotDiff", slotDiff.str())
+					("memberStorageOffset", to_string(offset))
+					("memberOffset",
+						fromCalldata ?
+							to_string(fromStructType.calldataOffsetOfMember(structMembers[i].name)) :
+							fromStructType.memoryOffsetOfMember(structMembers[i].name).str()
+					)
+					("loadFromMemoryOrCalldata", readFromMemoryOrCalldata(*structMembers[i].type, fromCalldata))
+					.render();
+				}
+				templ("member", memberParams);
+
+				return templ.render();
+			}
 			else
 				solAssert(false, "Invalid non-value type for assignment.");
 		}
@@ -2052,13 +2193,27 @@ string YulUtilFunctions::conversionFunction(Type const& _from, Type const& _to)
 
 			solUnimplementedAssert(!fromStructType.isDynamicallyEncoded(), "");
 			solUnimplementedAssert(toStructType.location() == DataLocation::Memory, "");
-			solUnimplementedAssert(fromStructType.location() == DataLocation::CallData, "");
+			solUnimplementedAssert(fromStructType.location() != DataLocation::Memory, "");
 
+			if (fromStructType.location() == DataLocation::CallData)
+			{
 				body = Whiskers(R"(
 					converted := <abiDecode>(value, calldatasize())
 				)")("abiDecode", ABIFunctions(m_evmVersion, m_revertStrings, m_functionCollector).tupleDecoder(
 					{&toStructType}
 				)).render();
+			}
+			else
+			{
+				solAssert(fromStructType.location() == DataLocation::Storage, "");
+
+				body = Whiskers(R"(
+					converted := <readFromStorage>(value)
+				)")
+				("readFromStorage", readFromStorage(toStructType, 0, true))
+				.render();
+			}
+
 			break;
 		}
 		case Type::Category::FixedBytes:
@@ -2490,7 +2645,7 @@ string YulUtilFunctions::storageSetToZeroFunction(Type const& _type)
 				}
 			)")
 			("functionName", functionName)
-			("store", updateStorageValueFunction(_type))
+			("store", updateStorageValueFunction(_type, _type))
 			("zeroValue", zeroValueFunction(_type))
 			.render();
 		else if (_type.category() == Type::Category::Array)

libsolidity/codegen/YulUtilFunctions.h

@@ -221,8 +221,7 @@ public:
 	/// @param _keyType the type of the value provided
 	std::string mappingIndexAccessFunction(MappingType const& _mappingType, Type const& _keyType);
 
-	/// @returns a function that reads a value type from storage.
+	/// @returns a function that reads a type from storage.
-	/// Performs bit mask/sign extend cleanup and appropriate left / right shift, but not validation.
 	/// @param _splitFunctionTypes if false, returns the address and function signature in a
 	/// single variable.
 	std::string readFromStorage(Type const& _type, size_t _offset, bool _splitFunctionTypes);
@@ -248,7 +247,11 @@ public:
 	/// the specified slot and offset. If offset is not given, it is expected as
 	/// runtime parameter.
 	/// signature: (slot, [offset,] value)
-	std::string updateStorageValueFunction(Type const& _type, std::optional<unsigned> const& _offset = std::optional<unsigned>());
+	std::string updateStorageValueFunction(
+		Type const& _fromType,
+		Type const& _toType,
+		std::optional<unsigned> const& _offset = std::optional<unsigned>()
+	);
 
 	/// Returns the name of a function that will write the given value to
 	/// the specified address.
@@ -401,6 +404,16 @@ private:
 
 	std::string readFromMemoryOrCalldata(Type const& _type, bool _fromCalldata);
 
+	/// @returns a function that reads a value type from storage.
+	/// Performs bit mask/sign extend cleanup and appropriate left / right shift, but not validation.
+	/// @param _splitFunctionTypes if false, returns the address and function signature in a
+	/// single variable.
+	std::string readFromStorageValueType(Type const& _type, size_t _offset, bool _splitFunctionTypes);
+	std::string readFromStorageValueTypeDynamic(Type const& _type, bool _splitFunctionTypes);
+
+	/// @returns a function that reads a reference type from storage to memory (performing a deep copy).
+	std::string readFromStorageReferenceType(Type const& _type);
+
 	langutil::EVMVersion m_evmVersion;
 	RevertStrings m_revertStrings;
 	MultiUseYulFunctionCollector& m_functionCollector;

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -314,9 +314,9 @@ bool IRGeneratorForStatements::visit(Assignment const& _assignment)
 
 	writeToLValue(*m_currentLValue, value);
 
-	m_currentLValue.reset();
+	if (m_currentLValue->type.category() != Type::Category::Struct && *_assignment.annotation().type != *TypeProvider::emptyTuple())
-	if (*_assignment.annotation().type != *TypeProvider::emptyTuple())
 		define(_assignment, value);
+	m_currentLValue.reset();
 
 	return false;
 }
@@ -749,8 +749,18 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall)
 
 			if (identifier)
 				functionDef = &functionDef->resolveVirtual(m_context.mostDerivedContract());
+			else
+			{
+				ContractType const* type = dynamic_cast<ContractType const*>(memberAccess->expression().annotation().type);
+				if (type && type->isSuper())
+				{
+					ContractDefinition const* super = type->contractDefinition().superContract(m_context.mostDerivedContract());
+					solAssert(super, "Super contract not available.");
+					functionDef = &functionDef->resolveVirtual(m_context.mostDerivedContract(), super);
+				}
+			}
 
-			solAssert(functionDef->isImplemented(), "");
+			solAssert(functionDef && functionDef->isImplemented(), "");
 		}
 
 		solAssert(!functionType->takesArbitraryParameters(), "");
@@ -1397,7 +1407,17 @@ void IRGeneratorForStatements::endVisit(MemberAccess const& _memberAccess)
 		ContractType const& type = dynamic_cast<ContractType const&>(*_memberAccess.expression().annotation().type);
 		if (type.isSuper())
 		{
-			solUnimplementedAssert(false, "");
+			solAssert(!!_memberAccess.annotation().referencedDeclaration, "Referenced declaration not resolved.");
+			ContractDefinition const* super = type.contractDefinition().superContract(m_context.mostDerivedContract());
+			solAssert(super, "Super contract not available.");
+			FunctionDefinition const& resolvedFunctionDef = dynamic_cast<FunctionDefinition const&>(
+				*_memberAccess.annotation().referencedDeclaration
+			).resolveVirtual(m_context.mostDerivedContract(), super);
+
+			define(_memberAccess) << to_string(resolvedFunctionDef.id()) << "\n";
+			solAssert(resolvedFunctionDef.functionType(true), "");
+			solAssert(resolvedFunctionDef.functionType(true)->kind() == FunctionType::Kind::Internal, "");
+			m_context.internalFunctionAccessed(_memberAccess, resolvedFunctionDef);
 		}
 		// ordinary contract type
 		else if (Declaration const* declaration = _memberAccess.annotation().referencedDeclaration)
@@ -2486,7 +2506,7 @@ void IRGeneratorForStatements::writeToLValue(IRLValue const& _lvalue, IRVariable
 					offset = std::get<unsigned>(_storage.offset);
 
 				m_code <<
-					m_utils.updateStorageValueFunction(_lvalue.type, offset) <<
+					m_utils.updateStorageValueFunction(_value.type(), _lvalue.type, offset) <<
 					"(" <<
 					_storage.slot <<
 					(

libsolidity/formal/BMC.cpp

@@ -580,7 +580,7 @@ pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
 		auto const& type = var.second->type();
 		if (
 			type->isValueType() &&
-			smt::smtKind(type->category()) != smtutil::Kind::Function
+			smt::smtKind(*type) != smtutil::Kind::Function
 		)
 		{
 			expressionsToEvaluate.emplace_back(var.second->currentValue());

libsolidity/formal/CHC.cpp

@@ -29,7 +29,6 @@
 #include <libsmtutil/CHCSmtLib2Interface.h>
 #include <libsolutil/Algorithms.h>
 
-#include <boost/algorithm/string/join.hpp>
 #include <boost/range/adaptor/reversed.hpp>
 
 #include <queue>
@@ -85,11 +84,7 @@ void CHC::analyze(SourceUnit const& _source)
 
 	resetSourceAnalysis();
 
-	auto genesisSort = make_shared<smtutil::FunctionSort>(
+	m_genesisPredicate = createSymbolicBlock(arity0FunctionSort(), "genesis");
-		vector<smtutil::SortPointer>(),
-		smtutil::SortProvider::boolSort
-	);
-	m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis");
 	addRule(genesis(), "genesis");
 
 	set<SourceUnit const*, IdCompare> sources;
@@ -118,16 +113,14 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 	initContract(_contract);
 
-	m_stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
+	m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
 	m_stateSorts = stateSorts(_contract);
 
 	clearIndices(&_contract);
 
 	string suffix = _contract.name() + "_" + to_string(_contract.id());
-	m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_" + suffix);
+	m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix, &_contract);
-	m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix);
+	m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix, &_contract);
-	m_symbolFunction[m_constructorSummaryPredicate->currentFunctionValue().name] = &_contract;
-	m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix);
 	auto stateExprs = currentStateVariables();
 	setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
 
@@ -233,7 +226,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		if (_function.isConstructor())
 		{
 			string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
-			auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix);
+			auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix, m_currentContract);
 			connectBlocks(m_currentBlock, predicate(*constructorExit, currentFunctionVariables(*m_currentContract)));
 
 			clearIndices(m_currentContract, m_currentFunction);
@@ -326,8 +319,8 @@ bool CHC::visit(WhileStatement const& _while)
 
 	auto outerBreakDest = m_breakDest;
 	auto outerContinueDest = m_continueDest;
-	m_breakDest = afterLoopBlock.get();
+	m_breakDest = afterLoopBlock;
-	m_continueDest = loopHeaderBlock.get();
+	m_continueDest = loopHeaderBlock;
 
 	if (_while.isDoWhile())
 		_while.body().accept(*this);
@@ -377,8 +370,8 @@ bool CHC::visit(ForStatement const& _for)
 
 	auto outerBreakDest = m_breakDest;
 	auto outerContinueDest = m_continueDest;
-	m_breakDest = afterLoopBlock.get();
+	m_breakDest = afterLoopBlock;
-	m_continueDest = postLoop ? postLoopBlock.get() : loopHeaderBlock.get();
+	m_continueDest = postLoop ? postLoopBlock : loopHeaderBlock;
 
 	if (auto init = _for.initializationExpression())
 		init->accept(*this);
@@ -571,7 +564,6 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 			m_context.variable(*var)->increaseIndex();
 
 	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables());
-	m_symbolFunction[nondet.name] = &_funCall;
 	m_context.addAssertion(nondet);
 
 	m_context.addAssertion(m_error.currentValue() == 0);
@@ -681,7 +673,9 @@ void CHC::resetSourceAnalysis()
 	m_errorIds.clear();
 	m_callGraph.clear();
 	m_summaries.clear();
-	m_symbolFunction.clear();
+	m_interfaces.clear();
+	m_nondetInterfaces.clear();
+	Predicate::reset();
 }
 
 void CHC::resetContractAnalysis()
@@ -717,7 +711,7 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
 }
 
 void CHC::setCurrentBlock(
-	smt::SymbolicFunctionVariable const& _block,
+	Predicate const& _block,
 	vector<smtutil::Expression> const* _arguments
 )
 {
@@ -743,24 +737,10 @@ set<frontend::Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTN
 	return assertions;
 }
 
-vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
-{
-	return fold(
-		_contract.annotation().linearizedBaseContracts,
-		vector<VariableDeclaration const*>{},
-		[](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); }
-	);
-}
-
-vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
-{
-	return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
-}
-
 vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
 {
 	return applyMap(
-		stateVariablesIncludingInheritedAndPrivate(_contract),
+		SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
 		[](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }
 	);
 }
@@ -806,7 +786,7 @@ smtutil::SortPointer CHC::nondetInterfaceSort(ContractDefinition const& _contrac
 	);
 }
 
-smtutil::SortPointer CHC::arity0FunctionSort()
+smtutil::SortPointer CHC::arity0FunctionSort() const
 {
 	return make_shared<smtutil::FunctionSort>(
 		vector<smtutil::SortPointer>(),
@@ -853,7 +833,7 @@ smtutil::SortPointer CHC::sort(ASTNode const* _node)
 
 smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract)
 {
-	auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
+	auto stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
 	auto sorts = stateSorts(_contract);
 
 	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
@@ -870,14 +850,10 @@ smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, Contr
 	);
 }
 
-unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smtutil::SortPointer _sort, string const& _name)
+Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, ASTNode const* _node)
 {
-	auto block = make_unique<smt::SymbolicFunctionVariable>(
+	auto const* block = Predicate::create(_sort, _name, m_context, _node);
-		_sort,
+	m_interface->registerRelation(block->functor());
-		_name,
-		m_context
-	);
-	m_interface->registerRelation(block->currentFunctionValue());
 	return block;
 }
 
@@ -887,20 +863,24 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 		if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
 			for (auto const* base: contract->annotation().linearizedBaseContracts)
 			{
-				string suffix = base->name() + "_" + to_string(base->id());
+				for (auto const* var: SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*base))
-				m_interfaces[base] = createSymbolicBlock(interfaceSort(*base), "interface_" + suffix);
-				m_nondetInterfaces[base] = createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix);
-
-				for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base))
 					if (!m_context.knownVariable(*var))
 						createVariable(*var);
 
+				if (!m_interfaces.count(base))
+				{
+					solAssert(!m_nondetInterfaces.count(base), "");
+					string suffix = base->name() + "_" + to_string(base->id());
+					m_interfaces.emplace(base, createSymbolicBlock(interfaceSort(*base), "interface_" + suffix, base));
+					m_nondetInterfaces.emplace(base, createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix, base));
+
 					/// Base nondeterministic interface that allows
 					/// 0 steps to be taken, used as base for the inductive
 					/// rule for each function.
-				auto const& iface = *m_nondetInterfaces.at(base);
+					auto const* iface = m_nondetInterfaces.at(base);
 					auto state0 = stateVariablesAtIndex(0, *base);
-				addRule(iface(state0 + state0), "base_nondet");
+					addRule((*iface)(state0 + state0), "base_nondet");
+				}
 
 				for (auto const* function: base->definedFunctions())
 				{
@@ -923,8 +903,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 						auto state1 = stateVariablesAtIndex(1, *base);
 						auto state2 = stateVariablesAtIndex(2, *base);
 
-						auto nondetPre = iface(state0 + state1);
+						auto const* iface = m_nondetInterfaces.at(base);
-						auto nondetPost = iface(state0 + state2);
+						auto state0 = stateVariablesAtIndex(0, *base);
+						auto nondetPre = (*iface)(state0 + state1);
+						auto nondetPost = (*iface)(state0 + state2);
 
 						vector<smtutil::Expression> args{m_error.currentValue()};
 						args += state1 +
@@ -960,7 +942,7 @@ smtutil::Expression CHC::error()
 
 smtutil::Expression CHC::error(unsigned _idx)
 {
-	return m_errorPredicate->functionValueAtIndex(_idx)({});
+	return m_errorPredicate->functor(_idx)({});
 }
 
 smtutil::Expression CHC::summary(ContractDefinition const& _contract)
@@ -994,37 +976,33 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function)
 	return summary(_function, *m_currentContract);
 }
 
-unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(ASTNode const* _node, string const& _prefix)
+Predicate const* CHC::createBlock(ASTNode const* _node, string const& _prefix)
 {
-	auto block = createSymbolicBlock(sort(_node),
+	auto block = createSymbolicBlock(
-		"block_" +
+		sort(_node),
-		uniquePrefix() +
+		"block_" + uniquePrefix() + "_" + _prefix + predicateName(_node),
-		"_" +
+		_node
-		_prefix +
+	);
-		predicateName(_node));
 
 	solAssert(m_currentFunction, "");
-	m_symbolFunction[block->currentFunctionValue().name] = m_currentFunction;
 	return block;
 }
 
-unique_ptr<smt::SymbolicFunctionVariable> CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract)
+Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract)
 {
-	auto block = createSymbolicBlock(summarySort(_function, _contract),
+	auto block = createSymbolicBlock(
-		"summary_" +
+		summarySort(_function, _contract),
-		uniquePrefix() +
+		"summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract),
-		"_" +
+		&_function
-		predicateName(&_function, &_contract));
+	);
 
-	m_symbolFunction[block->currentFunctionValue().name] = &_function;
 	return block;
 }
 
 void CHC::createErrorBlock()
 {
-	solAssert(m_errorPredicate, "");
+	m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId()));
-	m_errorPredicate->increaseIndex();
+	m_interface->registerRelation(m_errorPredicate->functor());
-	m_interface->registerRelation(m_errorPredicate->currentFunctionValue());
 }
 
 void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints)
@@ -1055,7 +1033,7 @@ vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index)
 vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract)
 {
 	return applyMap(
-		stateVariablesIncludingInheritedAndPrivate(_contract),
+		SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
 		[&](auto _var) { return valueAtIndex(*_var, _index); }
 	);
 }
@@ -1068,7 +1046,7 @@ vector<smtutil::Expression> CHC::currentStateVariables()
 
 vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const& _contract)
 {
-	return applyMap(stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
+	return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
 }
 
 vector<smtutil::Expression> CHC::currentFunctionVariables()
@@ -1128,13 +1106,13 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr
 	return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id());
 }
 
-smtutil::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block)
+smtutil::Expression CHC::predicate(Predicate const& _block)
 {
 	return _block(currentBlockVariables());
 }
 
 smtutil::Expression CHC::predicate(
-	smt::SymbolicFunctionVariable const& _block,
+	Predicate const& _block,
 	vector<smtutil::Expression> const& _arguments
 )
 {
@@ -1425,42 +1403,31 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		solAssert(edges.size() <= 2, "");
 
 		unsigned summaryId = edges.at(0);
-
 		optional<unsigned> interfaceId;
 		if (edges.size() == 2)
 		{
 			interfaceId = edges.at(1);
-			if (_graph.nodes.at(summaryId).first.rfind("summary", 0) != 0)
+			if (!Predicate::predicate(_graph.nodes.at(summaryId).first)->isSummary())
 				swap(summaryId, *interfaceId);
-			solAssert(_graph.nodes.at(*interfaceId).first.rfind("interface", 0) == 0, "");
+			auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first);
+			solAssert(interfacePredicate && interfacePredicate->isInterface(), "");
 		}
 		/// The children are unordered, so we need to check which is the summary and
 		/// which is the interface.
 
-		solAssert(_graph.nodes.at(summaryId).first.rfind("summary", 0) == 0, "");
+		Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).first);
+		solAssert(summaryPredicate && summaryPredicate->isSummary(), "");
 		/// At this point property 2 from the function description is verified for this node.
+		auto summaryArgs = _graph.nodes.at(summaryId).second;
 
-		auto const& summaryNode = _graph.nodes.at(summaryId);
+		FunctionDefinition const* calledFun = summaryPredicate->programFunction();
-		solAssert(m_symbolFunction.count(summaryNode.first), "");
+		ContractDefinition const* calledContract = summaryPredicate->programContract();
-
-		FunctionDefinition const* calledFun = nullptr;
-		ContractDefinition const* calledContract = nullptr;
-		if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_symbolFunction.at(summaryNode.first)))
-		{
-			if (auto const* constructor = contract->constructor())
-				calledFun = constructor;
-			else
-				calledContract = contract;
-		}
-		else if (auto const* fun = dynamic_cast<FunctionDefinition const*>(m_symbolFunction.at(summaryNode.first)))
-			calledFun = fun;
-		else
-			solAssert(false, "");
 
 		solAssert((calledFun && !calledContract) || (!calledFun && calledContract), "");
-		auto const& stateVars = calledFun ? stateVariablesIncludingInheritedAndPrivate(*calledFun) : stateVariablesIncludingInheritedAndPrivate(*calledContract);
+		auto stateVars = summaryPredicate->stateVariables();
-		/// calledContract != nullptr implies that the constructor of the analyzed contract is implicit and
+		solAssert(stateVars.has_value(), "");
-		/// therefore takes no parameters.
+		auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
+		solAssert(stateValues.size() == stateVars->size(), "");
 
 		/// This summary node is the end of a tx.
 		/// If it is the first summary node seen in this loop, it is the summary
@@ -1470,36 +1437,23 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		{
 			lastTxSeen = true;
 			/// Generate counterexample message local to the failed target.
-			localState = formatStateCounterexample(stateVars, calledFun, summaryNode.second) + "\n";
+			localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
 			if (calledFun)
 			{
-				/// The signature of a summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
+				auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
 				auto const& inParams = calledFun->parameters();
-				unsigned initLocals = stateVars.size() * 2 + 1 + inParams.size();
+				localState += formatVariableModel(inParams, inValues, "\n") + "\n";
-				/// In this loop we are interested in postInputVars.
+				auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs);
-				for (unsigned i = initLocals; i < initLocals + inParams.size(); ++i)
-				{
-					auto param = inParams.at(i - initLocals);
-					if (param->type()->isValueType())
-						localState += param->name() + " = " + summaryNode.second.at(i) + "\n";
-				}
 				auto const& outParams = calledFun->returnParameters();
-				initLocals += inParams.size();
+				localState += formatVariableModel(outParams, outValues, "\n") + "\n";
-				/// In this loop we are interested in outputVars.
-				for (unsigned i = initLocals; i < initLocals + outParams.size(); ++i)
-				{
-					auto param = outParams.at(i - initLocals);
-					if (param->type()->isValueType())
-						localState += param->name() + " = " + summaryNode.second.at(i) + "\n";
-				}
 			}
 		}
 		else
 			/// We report the state after every tx in the trace except for the last, which is reported
 			/// first in the code above.
-			path.emplace_back("State: " + formatStateCounterexample(stateVars, calledFun, summaryNode.second));
+			path.emplace_back("State: " + formatVariableModel(*stateVars, stateValues, ", "));
 
-		string txCex = calledContract ? "constructor()" : formatFunctionCallCounterexample(stateVars, *calledFun, summaryNode.second);
+		string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
 		path.emplace_back(txCex);
 
 		/// Recurse on the next interface node which represents the previous transaction
@@ -1513,66 +1467,6 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 	return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n");
 }
 
-string CHC::formatStateCounterexample(vector<VariableDeclaration const*> const& _stateVars, FunctionDefinition const* _function, vector<string> const& _summaryValues)
-{
-	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
-	/// The signature of an implicit constructor summary predicate is: summary(error, postStateVars).
-	/// Here we are interested in postStateVars.
-	vector<string>::const_iterator stateFirst;
-	vector<string>::const_iterator stateLast;
-	if (_function)
-	{
-		stateFirst = _summaryValues.begin() + 1 + static_cast<int>(_stateVars.size()) + static_cast<int>(_function->parameters().size());
-		stateLast = stateFirst + static_cast<int>(_stateVars.size());
-	}
-	else
-	{
-		stateFirst = _summaryValues.begin() + 1;
-		stateLast = stateFirst + static_cast<int>(_stateVars.size());
-	}
-
-	solAssert(stateFirst >= _summaryValues.begin() && stateFirst <= _summaryValues.end(), "");
-	solAssert(stateLast >= _summaryValues.begin() && stateLast <= _summaryValues.end(), "");
-	vector<string> stateArgs(stateFirst, stateLast);
-	solAssert(stateArgs.size() == _stateVars.size(), "");
-
-	vector<string> stateCex;
-	for (unsigned i = 0; i < stateArgs.size(); ++i)
-	{
-		auto var = _stateVars.at(i);
-		if (var->type()->isValueType())
-			stateCex.emplace_back(var->name() + " = " + stateArgs.at(i));
-	}
-
-	return boost::algorithm::join(stateCex, ", ");
-}
-
-string CHC::formatFunctionCallCounterexample(vector<VariableDeclaration const*> const& _stateVars, FunctionDefinition const& _function, vector<string> const& _summaryValues)
-{
-	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
-	/// Here we are interested in preInputVars.
-	vector<string>::const_iterator first = _summaryValues.begin() + static_cast<int>(_stateVars.size()) + 1;
-	vector<string>::const_iterator last = first + static_cast<int>(_function.parameters().size());
-	solAssert(first >= _summaryValues.begin() && first <= _summaryValues.end(), "");
-	solAssert(last >= _summaryValues.begin() && last <= _summaryValues.end(), "");
-	vector<string> functionArgsCex(first, last);
-	vector<string> functionArgs;
-
-	auto const& params = _function.parameters();
-	solAssert(params.size() == functionArgsCex.size(), "");
-	for (unsigned i = 0; i < params.size(); ++i)
-		if (params[i]->type()->isValueType())
-			functionArgs.emplace_back(functionArgsCex[i]);
-		else
-			functionArgs.emplace_back(params[i]->name());
-
-	string fName = _function.isConstructor() ? "constructor" :
-		_function.isFallback() ? "fallback" :
-		_function.isReceive() ? "receive" :
-		_function.name();
-	return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")";
-}
-
 string CHC::cex2dot(smtutil::CHCSolverInterface::CexGraph const& _cex)
 {
 	string dot = "digraph {\n";

libsolidity/formal/CHC.h

@@ -31,12 +31,15 @@
 
 #pragma once
 
+#include <libsolidity/formal/Predicate.h>
 #include <libsolidity/formal/SMTEncoder.h>
 
 #include <libsolidity/interface/ReadFile.h>
 
 #include <libsmtutil/CHCSolverInterface.h>
 
+#include <boost/algorithm/string/join.hpp>
+
 #include <map>
 #include <optional>
 #include <set>
@@ -108,10 +111,8 @@ private:
 	void resetContractAnalysis();
 	void eraseKnowledge();
 	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
-	void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
+	void setCurrentBlock(Predicate const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
 	std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
-	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
-	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
 	//@}
 
 	/// Sort helpers.
@@ -122,7 +123,7 @@ private:
 	smtutil::SortPointer nondetInterfaceSort();
 	static smtutil::SortPointer interfaceSort(ContractDefinition const& _const);
 	static smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _const);
-	smtutil::SortPointer arity0FunctionSort();
+	smtutil::SortPointer arity0FunctionSort() const;
 	smtutil::SortPointer sort(FunctionDefinition const& _function);
 	smtutil::SortPointer sort(ASTNode const* _block);
 	/// @returns the sort of a predicate that represents the summary of _function in the scope of _contract.
@@ -134,7 +135,7 @@ private:
 	/// Predicate helpers.
 	//@{
 	/// @returns a new block of given _sort and _name.
-	std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name);
+	Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, ASTNode const* _node = nullptr);
 
 	/// Creates summary predicates for all functions of all contracts
 	/// in a given _source.
@@ -150,10 +151,10 @@ private:
 	smtutil::Expression error(unsigned _idx);
 
 	/// Creates a block for the given _node.
-	std::unique_ptr<smt::SymbolicFunctionVariable> createBlock(ASTNode const* _node, std::string const& _prefix = "");
+	Predicate const* createBlock(ASTNode const* _node, std::string const& _prefix = "");
 	/// Creates a call block for the given function _function from contract _contract.
 	/// The contract is needed here because of inheritance.
-	std::unique_ptr<smt::SymbolicFunctionVariable> createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract);
+	Predicate const* createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract);
 
 	/// Creates a new error block to be used by an assertion.
 	/// Also registers the predicate.
@@ -184,9 +185,9 @@ private:
 	/// @returns the predicate name for a given node.
 	std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr);
 	/// @returns a predicate application over the current scoped variables.
-	smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block);
+	smtutil::Expression predicate(Predicate const& _block);
 	/// @returns a predicate application over @param _arguments.
-	smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector<smtutil::Expression> const& _arguments);
+	smtutil::Expression predicate(Predicate const& _block, std::vector<smtutil::Expression> const& _arguments);
 	/// @returns the summary predicate for the called function.
 	smtutil::Expression predicate(FunctionCall const& _funCall);
 	/// @returns a predicate that defines a constructor summary.
@@ -222,15 +223,23 @@ private:
 	);
 
 	std::optional<std::string> generateCounterexample(smtutil::CHCSolverInterface::CexGraph const& _graph, std::string const& _root);
-	/// @returns values for the _stateVariables after a transaction calling
+
-	/// _function was executed.
+	/// @returns a set of pairs _var = _value separated by _separator.
-	/// _function = nullptr means the transaction was the deployment of a
+	template <typename T>
-	/// contract without an explicit constructor.
+	std::string formatVariableModel(std::vector<T> const& _variables, std::vector<std::string> const& _values, std::string const& _separator) const
-	std::string formatStateCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, FunctionDefinition const* _function, std::vector<std::string> const& _summaryValues);
+	{
-	/// @returns a formatted text representing a call to _function
+		solAssert(_variables.size() == _values.size(), "");
-	/// with the concrete values for value type parameters and
+
-	/// the parameter name for reference types.
+		std::vector<std::string> assignments;
-	std::string formatFunctionCallCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, FunctionDefinition const& _function, std::vector<std::string> const& _summaryValues);
+		for (unsigned i = 0; i < _values.size(); ++i)
+		{
+			auto var = _variables.at(i);
+			if (var && var->type()->isValueType())
+				assignments.emplace_back(var->name() + " = " + _values.at(i));
+		}
+
+		return boost::algorithm::join(assignments, _separator);
+	}
 
 	/// @returns a DAG in the dot format.
 	/// Used for debugging purposes.
@@ -251,32 +260,32 @@ private:
 	/// Predicates.
 	//@{
 	/// Genesis predicate.
-	std::unique_ptr<smt::SymbolicFunctionVariable> m_genesisPredicate;
+	Predicate const* m_genesisPredicate = nullptr;
 
 	/// Implicit constructor predicate.
 	/// Explicit constructors are handled as functions.
-	std::unique_ptr<smt::SymbolicFunctionVariable> m_implicitConstructorPredicate;
+	Predicate const* m_implicitConstructorPredicate = nullptr;
 
 	/// Constructor summary predicate, exists after the constructor
 	/// (implicit or explicit) and before the interface.
-	std::unique_ptr<smt::SymbolicFunctionVariable> m_constructorSummaryPredicate;
+	Predicate const* m_constructorSummaryPredicate = nullptr;
 
 	/// Artificial Interface predicate.
 	/// Single entry block for all functions.
-	std::map<ContractDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>> m_interfaces;
+	std::map<ContractDefinition const*, Predicate const*> m_interfaces;
 
 	/// Nondeterministic interfaces.
 	/// These are used when the analyzed contract makes external calls to unknown code,
 	/// which means that the analyzed contract can potentially be called
 	/// nondeterministically.
-	std::map<ContractDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>> m_nondetInterfaces;
+	std::map<ContractDefinition const*, Predicate const*> m_nondetInterfaces;
 
 	/// Artificial Error predicate.
 	/// Single error block for all assertions.
-	std::unique_ptr<smt::SymbolicFunctionVariable> m_errorPredicate;
+	Predicate const* m_errorPredicate = nullptr;
 
 	/// Function predicates.
-	std::map<ContractDefinition const*, std::map<FunctionDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>>> m_summaries;
+	std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_summaries;
 
 	smt::SymbolicIntVariable m_error{
 		TypeProvider::uint256(),
@@ -337,9 +346,9 @@ private:
 	bool m_unknownFunctionCallSeen = false;
 
 	/// Block where a loop break should go to.
-	smt::SymbolicFunctionVariable const* m_breakDest = nullptr;
+	Predicate const* m_breakDest;
 	/// Block where a loop continue should go to.
-	smt::SymbolicFunctionVariable const* m_continueDest = nullptr;
+	Predicate const* m_continueDest;
 	//@}
 
 	/// CHC solver.

libsolidity/formal/Predicate.cpp

@@ -0,0 +1,260 @@
+/*
+	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/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolidity/formal/Predicate.h>
+
+#include <libsolidity/formal/SMTEncoder.h>
+
+#include <libsolidity/ast/AST.h>
+
+#include <boost/algorithm/string/join.hpp>
+#include <utility>
+
+using namespace std;
+using namespace solidity;
+using namespace solidity::smtutil;
+using namespace solidity::frontend;
+using namespace solidity::frontend::smt;
+
+map<string, Predicate> Predicate::m_predicates;
+
+Predicate const* Predicate::create(
+	SortPointer _sort,
+	string _name,
+	EncodingContext& _context,
+	ASTNode const* _node
+)
+{
+	smt::SymbolicFunctionVariable predicate{_sort, move(_name), _context};
+	string functorName = predicate.currentName();
+	solAssert(!m_predicates.count(functorName), "");
+	return &m_predicates.emplace(
+		std::piecewise_construct,
+		std::forward_as_tuple(functorName),
+		std::forward_as_tuple(move(predicate), _node)
+	).first->second;
+}
+
+Predicate::Predicate(
+	smt::SymbolicFunctionVariable&& _predicate,
+	ASTNode const* _node
+):
+	m_predicate(move(_predicate)),
+	m_node(_node)
+{
+}
+
+Predicate const* Predicate::predicate(string const& _name)
+{
+	return &m_predicates.at(_name);
+}
+
+void Predicate::reset()
+{
+	m_predicates.clear();
+}
+
+smtutil::Expression Predicate::operator()(vector<smtutil::Expression> const& _args) const
+{
+	return m_predicate(_args);
+}
+
+smtutil::Expression Predicate::functor() const
+{
+	return m_predicate.currentFunctionValue();
+}
+
+smtutil::Expression Predicate::functor(unsigned _idx) const
+{
+	return m_predicate.functionValueAtIndex(_idx);
+}
+
+void Predicate::newFunctor()
+{
+	m_predicate.increaseIndex();
+}
+
+ASTNode const* Predicate::programNode() const
+{
+	return m_node;
+}
+
+ContractDefinition const* Predicate::programContract() const
+{
+	if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_node))
+		if (!contract->constructor())
+			return contract;
+
+	return nullptr;
+}
+
+FunctionDefinition const* Predicate::programFunction() const
+{
+	if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_node))
+	{
+		if (contract->constructor())
+			return contract->constructor();
+		return nullptr;
+	}
+
+	if (auto const* fun = dynamic_cast<FunctionDefinition const*>(m_node))
+		return fun;
+
+	return nullptr;
+}
+
+optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const
+{
+	if (auto const* fun = programFunction())
+		return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun);
+	if (auto const* contract = programContract())
+		return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contract);
+
+	auto const* node = m_node;
+	while (auto const* scopable = dynamic_cast<Scopable const*>(node))
+	{
+		node = scopable->scope();
+		if (auto const* fun = dynamic_cast<FunctionDefinition const*>(node))
+			return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun);
+	}
+
+	return nullopt;
+}
+
+bool Predicate::isSummary() const
+{
+	return functor().name.rfind("summary", 0) == 0;
+}
+
+bool Predicate::isInterface() const
+{
+	return functor().name.rfind("interface", 0) == 0;
+}
+
+string Predicate::formatSummaryCall(vector<string> const& _args) const
+{
+	if (programContract())
+		return "constructor()";
+
+	solAssert(isSummary(), "");
+
+	auto stateVars = stateVariables();
+	solAssert(stateVars.has_value(), "");
+	auto const* fun = programFunction();
+	solAssert(fun, "");
+
+	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
+	/// Here we are interested in preInputVars.
+	vector<string>::const_iterator first = _args.begin() + static_cast<int>(stateVars->size()) + 1;
+	vector<string>::const_iterator last = first + static_cast<int>(fun->parameters().size());
+	solAssert(first >= _args.begin() && first <= _args.end(), "");
+	solAssert(last >= _args.begin() && last <= _args.end(), "");
+	vector<string> functionArgsCex(first, last);
+	vector<string> functionArgs;
+
+	auto const& params = fun->parameters();
+	solAssert(params.size() == functionArgsCex.size(), "");
+	for (unsigned i = 0; i < params.size(); ++i)
+		if (params[i]->type()->isValueType())
+			functionArgs.emplace_back(functionArgsCex[i]);
+		else
+			functionArgs.emplace_back(params[i]->name());
+
+	string fName = fun->isConstructor() ? "constructor" :
+		fun->isFallback() ? "fallback" :
+		fun->isReceive() ? "receive" :
+		fun->name();
+	return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")";
+
+}
+
+vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
+{
+	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
+	/// The signature of an implicit constructor summary predicate is: summary(error, postStateVars).
+	/// Here we are interested in postStateVars.
+
+	auto stateVars = stateVariables();
+	solAssert(stateVars.has_value(), "");
+
+	vector<string>::const_iterator stateFirst;
+	vector<string>::const_iterator stateLast;
+	if (auto const* function = programFunction())
+	{
+		stateFirst = _args.begin() + 1 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size());
+		stateLast = stateFirst + static_cast<int>(stateVars->size());
+	}
+	else if (programContract())
+	{
+		stateFirst = _args.begin() + 1;
+		stateLast = stateFirst + static_cast<int>(stateVars->size());
+	}
+	else
+		solAssert(false, "");
+
+	solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), "");
+	solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), "");
+
+	vector<string> stateArgs(stateFirst, stateLast);
+	solAssert(stateArgs.size() == stateVars->size(), "");
+	return stateArgs;
+}
+
+vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) const
+{
+	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
+	/// Here we are interested in postInputVars.
+	auto const* function = programFunction();
+	solAssert(function, "");
+
+	auto stateVars = stateVariables();
+	solAssert(stateVars.has_value(), "");
+
+	auto const& inParams = function->parameters();
+
+	vector<string>::const_iterator first = _args.begin() + 1 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size());
+	vector<string>::const_iterator last = first + static_cast<int>(inParams.size());
+
+	solAssert(first >= _args.begin() && first <= _args.end(), "");
+	solAssert(last >= _args.begin() && last <= _args.end(), "");
+
+	vector<string> inValues(first, last);
+	solAssert(inValues.size() == inParams.size(), "");
+	return inValues;
+}
+
+vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) const
+{
+	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
+	/// Here we are interested in outputVars.
+	auto const* function = programFunction();
+	solAssert(function, "");
+
+	auto stateVars = stateVariables();
+	solAssert(stateVars.has_value(), "");
+
+	auto const& inParams = function->parameters();
+
+	vector<string>::const_iterator first = _args.begin() + 1 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2;
+
+	solAssert(first >= _args.begin() && first <= _args.end(), "");
+
+	vector<string> outValues(first, _args.end());
+	solAssert(outValues.size() == function->returnParameters().size(), "");
+	return outValues;
+}

libsolidity/formal/Predicate.h

@@ -0,0 +1,120 @@
+/*
+	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/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <libsolidity/formal/SymbolicVariables.h>
+#include <libsolidity/formal/SymbolicVariables.h>
+
+#include <libsmtutil/Sorts.h>
+
+#include <map>
+#include <optional>
+#include <vector>
+
+namespace solidity::frontend
+{
+
+/**
+ * Represents a predicate used by the CHC engine.
+ */
+class Predicate
+{
+public:
+	static Predicate const* create(
+		smtutil::SortPointer _sort,
+		std::string _name,
+		smt::EncodingContext& _context,
+		ASTNode const* _node = nullptr
+	);
+
+	Predicate(
+		smt::SymbolicFunctionVariable&& _predicate,
+		ASTNode const* _node = nullptr
+	);
+
+	/// Predicate should not be copiable.
+	Predicate(Predicate const&) = delete;
+	Predicate& operator=(Predicate const&) = delete;
+
+	/// @returns the Predicate associated with _name.
+	static Predicate const* predicate(std::string const& _name);
+
+	/// Resets all the allocated predicates.
+	static void reset();
+
+	/// @returns a function application of the predicate over _args.
+	smtutil::Expression operator()(std::vector<smtutil::Expression> const& _args) const;
+
+	/// @returns the function declaration of the predicate.
+	smtutil::Expression functor() const;
+	/// @returns the function declaration of the predicate with index _idx.
+	smtutil::Expression functor(unsigned _idx) const;
+	/// Increases the index of the function declaration of the predicate.
+	void newFunctor();
+
+	/// @returns the program node this predicate represents.
+	ASTNode const* programNode() const;
+
+	/// @returns the ContractDefinition that this predicate represents
+	/// or nullptr otherwise.
+	ContractDefinition const* programContract() const;
+
+	/// @returns the FunctionDefinition that this predicate represents
+	/// or nullptr otherwise.
+	FunctionDefinition const* programFunction() const;
+
+	/// @returns the program state variables in the scope of this predicate.
+	std::optional<std::vector<VariableDeclaration const*>> stateVariables() const;
+
+	/// @returns true if this predicate represents a summary.
+	bool isSummary() const;
+
+	/// @returns true if this predicate represents an interface.
+	bool isInterface() const;
+
+	/// @returns a formatted string representing a call to this predicate
+	/// with _args.
+	std::string formatSummaryCall(std::vector<std::string> const& _args) const;
+
+	/// @returns the values of the state variables from _args at the point
+	/// where this summary was reached.
+	std::vector<std::string> summaryStateValues(std::vector<std::string> const& _args) const;
+
+	/// @returns the values of the function input variables from _args at the point
+	/// where this summary was reached.
+	std::vector<std::string> summaryPostInputValues(std::vector<std::string> const& _args) const;
+
+	/// @returns the values of the function output variables from _args at the point
+	/// where this summary was reached.
+	std::vector<std::string> summaryPostOutputValues(std::vector<std::string> const& _args) const;
+
+private:
+	/// The actual SMT expression.
+	smt::SymbolicFunctionVariable m_predicate;
+
+	/// The ASTNode that this predicate represents.
+	/// nullptr if this predicate is not associated with a specific program AST node.
+	ASTNode const* m_node = nullptr;
+
+	/// Maps the name of the predicate to the actual Predicate.
+	/// Used in counterexample generation.
+	static std::map<std::string, Predicate> m_predicates;
+};
+
+}

libsolidity/formal/SMTEncoder.cpp

@@ -378,7 +378,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 			"Assertion checker does not yet implement this assignment operator."
 		);
 	}
-	else if (!smt::isSupportedType(_assignment.annotation().type->category()))
+	else if (!smt::isSupportedType(*_assignment.annotation().type))
 	{
 		// Give it a new index anyway to keep the SSA scheme sound.
 
@@ -403,8 +403,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 			assignment(
 				_assignment.leftHandSide(),
 				expr(_assignment, type),
-				type,
+				type
-				_assignment.location()
 			);
 		}
 	}
@@ -452,28 +451,30 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 
 void SMTEncoder::endVisit(UnaryOperation const& _op)
 {
-	if (TokenTraits::isBitOp(_op.getOperator()))
+	/// We need to shortcut here due to potentially unknown
-		return bitwiseNotOperation(_op);
+	/// rational number sizes.
 	if (_op.annotation().type->category() == Type::Category::RationalNumber)
 		return;
 
+	if (TokenTraits::isBitOp(_op.getOperator()))
+		return bitwiseNotOperation(_op);
+
 	createExpr(_op);
 
 	auto const* subExpr = innermostTuple(_op.subExpression());
-
+	auto type = _op.annotation().type;
 	switch (_op.getOperator())
 	{
 	case Token::Not: // !
 	{
-		solAssert(smt::isBool(_op.annotation().type->category()), "");
+		solAssert(smt::isBool(*type), "");
 		defineExpr(_op, !expr(*subExpr));
 		break;
 	}
 	case Token::Inc: // ++ (pre- or postfix)
 	case Token::Dec: // -- (pre- or postfix)
 	{
-		auto cat = _op.annotation().type->category();
+		solAssert(smt::isInteger(*type) || smt::isFixedPoint(*type), "");
-		solAssert(smt::isInteger(cat) || smt::isFixedPoint(cat), "");
 		solAssert(subExpr->annotation().willBeWrittenTo, "");
 		if (auto identifier = dynamic_cast<Identifier const*>(subExpr))
 		{
@@ -484,12 +485,15 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 			defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
 			assignment(*decl, newValue);
 		}
-		else if (dynamic_cast<IndexAccess const*>(subExpr))
+		else if (
+			dynamic_cast<IndexAccess const*>(&_op.subExpression()) ||
+			dynamic_cast<MemberAccess const*>(&_op.subExpression())
+		)
 		{
 			auto innerValue = expr(*subExpr);
 			auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
 			defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
-			arrayIndexAssignment(*subExpr, newValue);
+			indexOrMemberAssignment(_op.subExpression(), newValue);
 		}
 		else
 			m_errorReporter.warning(
@@ -518,14 +522,13 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 			auto const& symbVar = m_context.expression(*subExpr);
 			symbVar->increaseIndex();
 			m_context.setZeroValue(*symbVar);
-			if (dynamic_cast<IndexAccess const*>(subExpr))
+			if (
-				arrayIndexAssignment(*subExpr, symbVar->currentValue());
+				dynamic_cast<IndexAccess const*>(&_op.subExpression()) ||
+				dynamic_cast<MemberAccess const*>(&_op.subExpression())
+			)
+				indexOrMemberAssignment(_op.subExpression(), symbVar->currentValue());
 			else
-				m_errorReporter.warning(
+				solAssert(false, "");
-					2683_error,
-					_op.location(),
-					"Assertion checker does not yet implement \"delete\" for this expression."
-				);
 		}
 		break;
 	}
@@ -823,11 +826,11 @@ void SMTEncoder::endVisit(Literal const& _literal)
 {
 	solAssert(_literal.annotation().type, "Expected type for AST node");
 	Type const& type = *_literal.annotation().type;
-	if (smt::isNumber(type.category()))
+	if (smt::isNumber(type))
 		defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal)));
-	else if (smt::isBool(type.category()))
+	else if (smt::isBool(type))
 		defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false));
-	else if (smt::isStringLiteral(type.category()))
+	else if (smt::isStringLiteral(type))
 		createExpr(_literal);
 	else
 	{
@@ -890,6 +893,13 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 		defineGlobalVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
 		return false;
 	}
+	else if (smt::isNonRecursiveStruct(*exprType))
+	{
+		_memberAccess.expression().accept(*this);
+		auto const& symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(_memberAccess.expression()));
+		defineExpr(_memberAccess, symbStruct->member(_memberAccess.memberName()));
+		return false;
+	}
 	else if (exprType->category() == Type::Category::TypeType)
 	{
 		if (identifier && dynamic_cast<EnumDefinition const*>(identifier->annotation().referencedDeclaration))
@@ -961,19 +971,10 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		solAssert(varDecl, "");
 		array = m_context.variable(*varDecl);
 	}
-	else if (auto const* innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
-	{
-		solAssert(m_context.knownExpression(*innerAccess), "");
-		array = m_context.expression(*innerAccess);
-	}
 	else
 	{
-		m_errorReporter.warning(
+		solAssert(m_context.knownExpression(_indexAccess.baseExpression()), "");
-			9118_error,
+		array = m_context.expression(_indexAccess.baseExpression());
-			_indexAccess.location(),
-			"Assertion checker does not yet implement this expression."
-		);
-		return;
 	}
 
 	auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
@@ -1005,14 +1006,58 @@ void SMTEncoder::arrayAssignment()
 	m_arrayAssignmentHappened = true;
 }
 
-void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
+void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
 {
 	auto toStore = _rightHandSide;
-	auto indexAccess = dynamic_cast<IndexAccess const*>(&_expr);
+	auto const* lastExpr = &_expr;
-	solAssert(indexAccess, "");
 	while (true)
 	{
-		if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess->baseExpression()))
+		if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(lastExpr))
+		{
+			auto const& base = indexAccess->baseExpression();
+			if (dynamic_cast<Identifier const*>(&base))
+				base.accept(*this);
+			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base));
+			solAssert(symbArray, "");
+			auto baseType = symbArray->type();
+			toStore = smtutil::Expression::tuple_constructor(
+				smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
+				{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
+			);
+			m_context.expression(*indexAccess)->increaseIndex();
+			defineExpr(*indexAccess, smtutil::Expression::select(
+				symbArray->elements(),
+				expr(*indexAccess->indexExpression())
+			));
+			lastExpr = &indexAccess->baseExpression();
+		}
+		else if (auto const* memberAccess = dynamic_cast<MemberAccess const*>(lastExpr))
+		{
+			auto const& base = memberAccess->expression();
+			if (dynamic_cast<Identifier const*>(&base))
+				base.accept(*this);
+
+			if (
+				auto const* structType = dynamic_cast<StructType const*>(base.annotation().type);
+				structType && structType->recursive()
+			)
+			{
+				m_errorReporter.warning(
+					4375_error,
+					memberAccess->location(),
+					"Assertion checker does not support recursive structs."
+				);
+				return;
+			}
+
+			auto symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(base));
+			solAssert(symbStruct, "");
+			symbStruct->assignMember(memberAccess->memberName(), toStore);
+			toStore = symbStruct->currentValue();
+			defineExpr(*memberAccess, symbStruct->member(memberAccess->memberName()));
+			lastExpr = &memberAccess->expression();
+		}
+		else if (auto const& id = dynamic_cast<Identifier const*>(lastExpr))
 		{
 			auto varDecl = identifierToVariable(*id);
 			solAssert(varDecl, "");
@@ -1020,43 +1065,22 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expressi
 			if (varDecl->hasReferenceOrMappingType())
 				resetReferences(*varDecl);
 
-			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.variable(*varDecl));
+			m_context.addAssertion(m_context.newValue(*varDecl) == toStore);
-			smtutil::Expression store = smtutil::Expression::store(
+			m_context.expression(*id)->increaseIndex();
-				symbArray->elements(),
+			defineExpr(*id,currentValue(*varDecl));
-				expr(*indexAccess->indexExpression()),
-				toStore
-			);
-			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, smtutil::Expression::select(
-				symbArray->elements(),
-				expr(*indexAccess->indexExpression())
-			));
-
 			break;
 		}
-		else if (auto base = dynamic_cast<IndexAccess const*>(&indexAccess->baseExpression()))
-		{
-			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*base));
-			solAssert(symbArray, "");
-			auto baseType = base->annotation().type;
-			toStore = smtutil::Expression::tuple_constructor(
-				smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
-				{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
-			);
-			indexAccess = base;
-		}
 		else
 		{
-			m_errorReporter.warning(
+			auto type = lastExpr->annotation().type;
-				9056_error,
+			if (
-				_expr.location(),
+				dynamic_cast<ReferenceType const*>(type) ||
-				"Assertion checker does not yet implement this expression."
+				dynamic_cast<MappingType const*>(type)
-			);
+			)
+				resetReferences(type);
+
+			m_context.expression(*lastExpr)->increaseIndex();
+			m_context.addAssertion(expr(*lastExpr) == toStore);
 			break;
 		}
 	}
@@ -1128,9 +1152,14 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
 		if (varDecl->hasReferenceOrMappingType())
 			resetReferences(*varDecl);
 		m_context.addAssertion(m_context.newValue(*varDecl) == _array);
+		m_context.expression(*id)->increaseIndex();
+		defineExpr(*id,currentValue(*varDecl));
 	}
-	else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(expr))
+	else if (
-		arrayIndexAssignment(*indexAccess, _array);
+		dynamic_cast<IndexAccess const*>(expr) ||
+		dynamic_cast<MemberAccess const*>(expr)
+	)
+		indexOrMemberAssignment(_expr, _array);
 	else if (auto const* funCall = dynamic_cast<FunctionCall const*>(expr))
 	{
 		FunctionType const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
@@ -1153,12 +1182,6 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
 			arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
 		}
 	}
-	else if (dynamic_cast<MemberAccess const*>(expr))
-		m_errorReporter.warning(
-			9599_error,
-			_expr.location(),
-			"Assertion checker does not yet implement this expression."
-		);
 	else
 		solAssert(false, "");
 }
@@ -1179,7 +1202,7 @@ void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _ex
 		m_context.globalSymbol(_name)->increaseIndex();
 	// The default behavior is not to increase the index since
 	// most of the global values stay the same throughout a tx.
-	if (smt::isSupportedType(_expr.annotation().type->category()))
+	if (smt::isSupportedType(*_expr.annotation().type))
 		defineExpr(_expr, m_context.globalSymbol(_name)->currentValue());
 }
 
@@ -1332,13 +1355,13 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
 {
 	auto const& commonType = _op.annotation().commonType;
 	solAssert(commonType, "");
-	if (smt::isSupportedType(commonType->category()))
+	if (smt::isSupportedType(*commonType))
 	{
 		smtutil::Expression left(expr(_op.leftExpression(), commonType));
 		smtutil::Expression right(expr(_op.rightExpression(), commonType));
 		Token op = _op.getOperator();
 		shared_ptr<smtutil::Expression> value;
-		if (smt::isNumber(commonType->category()))
+		if (smt::isNumber(*commonType))
 		{
 			value = make_shared<smtutil::Expression>(
 				op == Token::Equal ? (left == right) :
@@ -1351,7 +1374,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
 		}
 		else // Bool
 		{
-			solUnimplementedAssert(smt::isBool(commonType->category()), "Operation not yet supported");
+			solUnimplementedAssert(smt::isBool(*commonType), "Operation not yet supported");
 			value = make_shared<smtutil::Expression>(
 				op == Token::Equal ? (left == right) :
 				/*op == Token::NotEqual*/ (left != right)
@@ -1447,8 +1470,7 @@ smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Exp
 void SMTEncoder::assignment(
 	Expression const& _left,
 	smtutil::Expression const& _right,
-	TypePointer const& _type,
+	TypePointer const& _type
-	langutil::SourceLocation const& _location
 )
 {
 	solAssert(
@@ -1458,28 +1480,21 @@ void SMTEncoder::assignment(
 
 	Expression const* left = innermostTuple(_left);
 
-	if (!smt::isSupportedType(_type->category()))
+	if (!smt::isSupportedType(*_type))
 	{
 		// Give it a new index anyway to keep the SSA scheme sound.
 		if (auto varDecl = identifierToVariable(*left))
 			m_context.newValue(*varDecl);
-
-		m_errorReporter.warning(
-			6191_error,
-			_location,
-			"Assertion checker does not yet implement type " + _type->toString()
-		);
 	}
 	else if (auto varDecl = identifierToVariable(*left))
 		assignment(*varDecl, _right);
-	else if (dynamic_cast<IndexAccess const*>(left))
+	else if (
-		arrayIndexAssignment(*left, _right);
+		dynamic_cast<IndexAccess const*>(left) ||
+		dynamic_cast<MemberAccess const*>(left)
+	)
+		indexOrMemberAssignment(*left, _right);
 	else
-		m_errorReporter.warning(
+		solAssert(false, "");
-			8182_error,
-			_location,
-			"Assertion checker does not yet implement such assignments."
-		);
 }
 
 void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _right)
@@ -1508,7 +1523,7 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
 			else
 			{
 				auto type = lExpr.annotation().type;
-				assignment(lExpr, expr(rExpr, type), type, lExpr.location());
+				assignment(lExpr, expr(rExpr, type), type);
 			}
 		}
 	}
@@ -1525,7 +1540,7 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
 
 		for (unsigned i = 0; i < lComponents.size(); ++i)
 			if (auto component = lComponents.at(i); component && rComponents.at(i))
-				assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type, component->location());
+				assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type);
 	}
 }
 
@@ -1689,14 +1704,26 @@ void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)
 		if (_var.isStateVariable() && _varDecl.isStateVariable())
 			return false;
 
-		TypePointer prefix = _var.type();
+		return sameTypeOrSubtype(_var.type(), _varDecl.type());
-		TypePointer originalType = typeWithoutPointer(_varDecl.type());
+	});
+}
+
+void SMTEncoder::resetReferences(TypePointer _type)
+{
+	m_context.resetVariables([&](VariableDeclaration const& _var) {
+		return sameTypeOrSubtype(_var.type(), _type);
+	});
+}
+
+bool SMTEncoder::sameTypeOrSubtype(TypePointer _a, TypePointer _b)
+{
+	TypePointer prefix = _a;
 	while (
 		prefix->category() == Type::Category::Mapping ||
 		prefix->category() == Type::Category::Array
 	)
 	{
-			if (*originalType == *typeWithoutPointer(prefix))
+		if (*typeWithoutPointer(_b) == *typeWithoutPointer(prefix))
 			return true;
 		if (prefix->category() == Type::Category::Mapping)
 		{
@@ -1712,7 +1739,6 @@ void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)
 		}
 	}
 	return false;
-	});
 }
 
 TypePointer SMTEncoder::typeWithoutPointer(TypePointer const& _type)
@@ -1982,6 +2008,20 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall cons
 	return funDef;
 }
 
+vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
+{
+	return fold(
+		_contract.annotation().linearizedBaseContracts,
+		vector<VariableDeclaration const*>{},
+		[](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); }
+	);
+}
+
+vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
+{
+	return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
+}
+
 void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
 {
 	FunctionDefinition const* funDef = functionCallToDefinition(_funCall);

libsolidity/formal/SMTEncoder.h

@@ -62,6 +62,9 @@ public:
 	/// if possible or nullptr.
 	static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall);
 
+	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
+	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
+
 protected:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined
@@ -143,8 +146,8 @@ protected:
 	/// to variable of some SMT array type
 	/// while aliasing is not supported.
 	void arrayAssignment();
-	/// Handles assignment to SMT array index.
+	/// Handles assignments to index or member access.
-	void arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide);
+	void indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide);
 
 	void arrayPush(FunctionCall const& _funCall);
 	void arrayPop(FunctionCall const& _funCall);
@@ -165,8 +168,7 @@ protected:
 	void assignment(
 		Expression const& _left,
 		smtutil::Expression const& _right,
-		TypePointer const& _type,
+		TypePointer const& _type
-		langutil::SourceLocation const& _location
 	);
 	/// Handle assignments between tuples.
 	void tupleAssignment(Expression const& _left, Expression const& _right);
@@ -193,8 +195,12 @@ protected:
 	/// Resets all references/pointers that have the same type or have
 	/// a subexpression of the same type as _varDecl.
 	void resetReferences(VariableDeclaration const& _varDecl);
+	/// Resets all references/pointers that have type _type.
+	void resetReferences(TypePointer _type);
 	/// @returns the type without storage pointer information if it has it.
 	TypePointer typeWithoutPointer(TypePointer const& _type);
+	/// @returns whether _a or a subtype of _a is the same as _b.
+	bool sameTypeOrSubtype(TypePointer _a, TypePointer _b);
 
 	/// Given two different branches and the touched variables,
 	/// merge the touched variables into after-branch ite variables

libsolidity/formal/SymbolicTypes.cpp

@@ -25,6 +25,7 @@
 #include <vector>
 
 using namespace std;
+using namespace solidity::util;
 using namespace solidity::smtutil;
 
 namespace solidity::frontend::smt
@@ -32,7 +33,7 @@ namespace solidity::frontend::smt
 
 SortPointer smtSort(frontend::Type const& _type)
 {
-	switch (smtKind(_type.category()))
+	switch (smtKind(_type))
 	{
 	case Kind::Int:
 		if (auto const* intType = dynamic_cast<IntegerType const*>(&_type))
@@ -63,13 +64,13 @@ SortPointer smtSort(frontend::Type const& _type)
 	case Kind::Array:
 	{
 		shared_ptr<ArraySort> array;
-		if (isMapping(_type.category()))
+		if (isMapping(_type))
 		{
 			auto mapType = dynamic_cast<frontend::MappingType const*>(&_type);
 			solAssert(mapType, "");
 			array = make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
 		}
-		else if (isStringLiteral(_type.category()))
+		else if (isStringLiteral(_type))
 		{
 			auto stringLitType = dynamic_cast<frontend::StringLiteralType const*>(&_type);
 			solAssert(stringLitType, "");
@@ -130,18 +131,32 @@ SortPointer smtSort(frontend::Type const& _type)
 	}
 	case Kind::Tuple:
 	{
-		auto tupleType = dynamic_cast<frontend::TupleType const*>(&_type);
-		solAssert(tupleType, "");
 		vector<string> members;
-		auto const& tupleName = _type.identifier();
+		auto const& tupleName = _type.toString(true);
+		vector<SortPointer> sorts;
+
+		if (auto const* tupleType = dynamic_cast<frontend::TupleType const*>(&_type))
+		{
 			auto const& components = tupleType->components();
 			for (unsigned i = 0; i < components.size(); ++i)
 				members.emplace_back(tupleName + "_accessor_" + to_string(i));
-		return make_shared<TupleSort>(
+			sorts = smtSortAbstractFunction(tupleType->components());
-			tupleName,
+		}
-			members,
+		else if (auto const* structType = dynamic_cast<frontend::StructType const*>(&_type))
-			smtSortAbstractFunction(tupleType->components())
+		{
-		);
+			solAssert(!structType->recursive(), "");
+			auto const& structMembers = structType->structDefinition().members();
+			for (auto member: structMembers)
+				members.emplace_back(tupleName + "_accessor_" + member->name());
+			sorts = smtSortAbstractFunction(applyMap(
+				structMembers,
+				[](auto var) { return var->type(); }
+			));
+		}
+		else
+			solAssert(false, "");
+
+		return make_shared<TupleSort>(tupleName, members, sorts);
 	}
 	default:
 		// Abstract case.
@@ -159,7 +174,7 @@ vector<SortPointer> smtSort(vector<frontend::TypePointer> const& _types)
 
 SortPointer smtSortAbstractFunction(frontend::Type const& _type)
 {
-	if (isFunction(_type.category()))
+	if (isFunction(_type))
 		return SortProvider::uintSort;
 	return smtSort(_type);
 }
@@ -175,35 +190,36 @@ vector<SortPointer> smtSortAbstractFunction(vector<frontend::TypePointer> const&
 	return sorts;
 }
 
-Kind smtKind(frontend::Type::Category _category)
+Kind smtKind(frontend::Type const& _type)
 {
-	if (isNumber(_category))
+	if (isNumber(_type))
 		return Kind::Int;
-	else if (isBool(_category))
+	else if (isBool(_type))
 		return Kind::Bool;
-	else if (isFunction(_category))
+	else if (isFunction(_type))
 		return Kind::Function;
-	else if (isMapping(_category) || isArray(_category))
+	else if (isMapping(_type) || isArray(_type))
 		return Kind::Array;
-	else if (isTuple(_category))
+	else if (isTuple(_type) || isNonRecursiveStruct(_type))
 		return Kind::Tuple;
 	// Abstract case.
 	return Kind::Int;
 }
 
-bool isSupportedType(frontend::Type::Category _category)
+bool isSupportedType(frontend::Type const& _type)
 {
-	return isNumber(_category) ||
+	return isNumber(_type) ||
-		isBool(_category) ||
+		isBool(_type) ||
-		isMapping(_category) ||
+		isMapping(_type) ||
-		isArray(_category) ||
+		isArray(_type) ||
-		isTuple(_category);
+		isTuple(_type) ||
+		isNonRecursiveStruct(_type);
 }
 
-bool isSupportedTypeDeclaration(frontend::Type::Category _category)
+bool isSupportedTypeDeclaration(frontend::Type const& _type)
 {
-	return isSupportedType(_category) ||
+	return isSupportedType(_type) ||
-		isFunction(_category);
+		isFunction(_type);
 }
 
 pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
@@ -220,9 +236,9 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		abstract = true;
 		var = make_shared<SymbolicIntVariable>(frontend::TypeProvider::uint256(), type, _uniqueName, _context);
 	}
-	else if (isBool(_type.category()))
+	else if (isBool(_type))
 		var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _context);
-	else if (isFunction(_type.category()))
+	else if (isFunction(_type))
 	{
 		auto const& fType = dynamic_cast<FunctionType const*>(type);
 		auto const& paramsIn = fType->parameterTypes();
@@ -245,21 +261,21 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		else
 			var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context);
 	}
-	else if (isInteger(_type.category()))
+	else if (isInteger(_type))
 		var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
-	else if (isFixedPoint(_type.category()))
+	else if (isFixedPoint(_type))
 		var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
-	else if (isFixedBytes(_type.category()))
+	else if (isFixedBytes(_type))
 	{
 		auto fixedBytesType = dynamic_cast<frontend::FixedBytesType const*>(type);
 		solAssert(fixedBytesType, "");
 		var = make_shared<SymbolicFixedBytesVariable>(type, fixedBytesType->numBytes(), _uniqueName, _context);
 	}
-	else if (isAddress(_type.category()) || isContract(_type.category()))
+	else if (isAddress(_type) || isContract(_type))
 		var = make_shared<SymbolicAddressVariable>(_uniqueName, _context);
-	else if (isEnum(_type.category()))
+	else if (isEnum(_type))
 		var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _context);
-	else if (isRational(_type.category()))
+	else if (isRational(_type))
 	{
 		auto rational = dynamic_cast<frontend::RationalNumberType const*>(&_type);
 		solAssert(rational, "");
@@ -268,106 +284,104 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		else
 			var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
 	}
-	else if (isMapping(_type.category()) || isArray(_type.category()))
+	else if (isMapping(_type) || isArray(_type))
 		var = make_shared<SymbolicArrayVariable>(type, type, _uniqueName, _context);
-	else if (isTuple(_type.category()))
+	else if (isTuple(_type))
 		var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _context);
-	else if (isStringLiteral(_type.category()))
+	else if (isStringLiteral(_type))
 	{
 		auto stringType = TypeProvider::stringMemory();
 		var = make_shared<SymbolicArrayVariable>(stringType, type, _uniqueName, _context);
 	}
+	else if (isNonRecursiveStruct(_type))
+		var = make_shared<SymbolicStructVariable>(type, _uniqueName, _context);
 	else
 		solAssert(false, "");
 	return make_pair(abstract, var);
 }
 
-bool isSupportedType(frontend::Type const& _type)
+bool isInteger(frontend::Type const& _type)
 {
-	return isSupportedType(_type.category());
+	return _type.category() == frontend::Type::Category::Integer;
 }
 
-bool isSupportedTypeDeclaration(frontend::Type const& _type)
+bool isFixedPoint(frontend::Type const& _type)
 {
-	return isSupportedTypeDeclaration(_type.category());
+	return _type.category() == frontend::Type::Category::FixedPoint;
 }
 
-bool isInteger(frontend::Type::Category _category)
+bool isRational(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Integer;
+	return _type.category() == frontend::Type::Category::RationalNumber;
 }
 
-bool isFixedPoint(frontend::Type::Category _category)
+bool isFixedBytes(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::FixedPoint;
+	return _type.category() == frontend::Type::Category::FixedBytes;
 }
 
-bool isRational(frontend::Type::Category _category)
+bool isAddress(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::RationalNumber;
+	return _type.category() == frontend::Type::Category::Address;
 }
 
-bool isFixedBytes(frontend::Type::Category _category)
+bool isContract(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::FixedBytes;
+	return _type.category() == frontend::Type::Category::Contract;
 }
 
-bool isAddress(frontend::Type::Category _category)
+bool isEnum(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Address;
+	return _type.category() == frontend::Type::Category::Enum;
 }
 
-bool isContract(frontend::Type::Category _category)
+bool isNumber(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Contract;
+	return isInteger(_type) ||
+		isFixedPoint(_type) ||
+		isRational(_type) ||
+		isFixedBytes(_type) ||
+		isAddress(_type) ||
+		isContract(_type) ||
+		isEnum(_type);
 }
 
-bool isEnum(frontend::Type::Category _category)
+bool isBool(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Enum;
+	return _type.category() == frontend::Type::Category::Bool;
 }
 
-bool isNumber(frontend::Type::Category _category)
+bool isFunction(frontend::Type const& _type)
 {
-	return isInteger(_category) ||
+	return _type.category() == frontend::Type::Category::Function;
-		isFixedPoint(_category) ||
-		isRational(_category) ||
-		isFixedBytes(_category) ||
-		isAddress(_category) ||
-		isContract(_category) ||
-		isEnum(_category);
 }
 
-bool isBool(frontend::Type::Category _category)
+bool isMapping(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Bool;
+	return _type.category() == frontend::Type::Category::Mapping;
 }
 
-bool isFunction(frontend::Type::Category _category)
+bool isArray(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Function;
+	return _type.category() == frontend::Type::Category::Array ||
+		_type.category() == frontend::Type::Category::StringLiteral ||
+		_type.category() == frontend::Type::Category::ArraySlice;
 }
 
-bool isMapping(frontend::Type::Category _category)
+bool isTuple(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Mapping;
+	return _type.category() == frontend::Type::Category::Tuple;
 }
 
-bool isArray(frontend::Type::Category _category)
+bool isStringLiteral(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Array ||
+	return _type.category() == frontend::Type::Category::StringLiteral;
-		_category == frontend::Type::Category::StringLiteral ||
-		_category == frontend::Type::Category::ArraySlice;
 }
 
-bool isTuple(frontend::Type::Category _category)
+bool isNonRecursiveStruct(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Tuple;
+	auto structType = dynamic_cast<StructType const*>(&_type);
-}
+	return structType && !structType->recursive();
-
-bool isStringLiteral(frontend::Type::Category _category)
-{
-	return _category == frontend::Type::Category::StringLiteral;
 }
 
 smtutil::Expression minValue(frontend::IntegerType const& _type)
@@ -394,13 +408,13 @@ void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const
 smtutil::Expression zeroValue(frontend::TypePointer const& _type)
 {
 	solAssert(_type, "");
-	if (isSupportedType(_type->category()))
+	if (isSupportedType(*_type))
 	{
-		if (isNumber(_type->category()))
+		if (isNumber(*_type))
 			return 0;
-		if (isBool(_type->category()))
+		if (isBool(*_type))
 			return smtutil::Expression(false);
-		if (isArray(_type->category()) || isMapping(_type->category()))
+		if (isArray(*_type) || isMapping(*_type))
 		{
 			auto tupleSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
 			solAssert(tupleSort, "");
@@ -421,11 +435,23 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type)
 
 			solAssert(zeroArray, "");
 			return smtutil::Expression::tuple_constructor(
-				smtutil::Expression(std::make_shared<SortSort>(smtSort(*_type)), _type->toString(true)),
+				smtutil::Expression(std::make_shared<SortSort>(tupleSort), tupleSort->name),
 				vector<smtutil::Expression>{*zeroArray, length}
 			);
 
 		}
+		if (isNonRecursiveStruct(*_type))
+		{
+			auto const* structType = dynamic_cast<StructType const*>(_type);
+			auto structSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
+			return smtutil::Expression::tuple_constructor(
+				smtutil::Expression(make_shared<SortSort>(structSort), structSort->name),
+				applyMap(
+					structType->structDefinition().members(),
+					[](auto var) { return zeroValue(var->type()); }
+				)
+			);
+		}
 		solAssert(false, "");
 	}
 	// Unsupported types are abstracted as Int.
@@ -452,14 +478,14 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext&
 void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
 {
 	solAssert(_type, "");
-	if (isEnum(_type->category()))
+	if (isEnum(*_type))
 	{
 		auto enumType = dynamic_cast<frontend::EnumType const*>(_type);
 		solAssert(enumType, "");
 		_context.addAssertion(_expr >= 0);
 		_context.addAssertion(_expr < enumType->numberOfMembers());
 	}
-	else if (isInteger(_type->category()))
+	else if (isInteger(*_type))
 	{
 		auto intType = dynamic_cast<frontend::IntegerType const*>(_type);
 		solAssert(intType, "");

libsolidity/formal/SymbolicTypes.h

@@ -34,29 +34,30 @@ std::vector<smtutil::SortPointer> smtSort(std::vector<frontend::TypePointer> con
 smtutil::SortPointer smtSortAbstractFunction(frontend::Type const& _type);
 std::vector<smtutil::SortPointer> smtSortAbstractFunction(std::vector<frontend::TypePointer> const& _types);
 /// Returns the SMT kind that models the Solidity type type category _category.
-smtutil::Kind smtKind(frontend::Type::Category _category);
+smtutil::Kind smtKind(frontend::Type const& _type);
 
 /// Returns true if type is fully supported (declaration and operations).
-bool isSupportedType(frontend::Type::Category _category);
+bool isSupportedType(frontend::Type const& _type);
 bool isSupportedType(frontend::Type const& _type);
 /// Returns true if type is partially supported (declaration).
-bool isSupportedTypeDeclaration(frontend::Type::Category _category);
+bool isSupportedTypeDeclaration(frontend::Type const& _type);
 bool isSupportedTypeDeclaration(frontend::Type const& _type);
 
-bool isInteger(frontend::Type::Category _category);
+bool isInteger(frontend::Type const& _type);
-bool isFixedPoint(frontend::Type::Category _category);
+bool isFixedPoint(frontend::Type const& _type);
-bool isRational(frontend::Type::Category _category);
+bool isRational(frontend::Type const& _type);
-bool isFixedBytes(frontend::Type::Category _category);
+bool isFixedBytes(frontend::Type const& _type);
-bool isAddress(frontend::Type::Category _category);
+bool isAddress(frontend::Type const& _type);
-bool isContract(frontend::Type::Category _category);
+bool isContract(frontend::Type const& _type);
-bool isEnum(frontend::Type::Category _category);
+bool isEnum(frontend::Type const& _type);
-bool isNumber(frontend::Type::Category _category);
+bool isNumber(frontend::Type const& _type);
-bool isBool(frontend::Type::Category _category);
+bool isBool(frontend::Type const& _type);
-bool isFunction(frontend::Type::Category _category);
+bool isFunction(frontend::Type const& _type);
-bool isMapping(frontend::Type::Category _category);
+bool isMapping(frontend::Type const& _type);
-bool isArray(frontend::Type::Category _category);
+bool isArray(frontend::Type const& _type);
-bool isTuple(frontend::Type::Category _category);
+bool isTuple(frontend::Type const& _type);
-bool isStringLiteral(frontend::Type::Category _category);
+bool isStringLiteral(frontend::Type const& _type);
+bool isNonRecursiveStruct(frontend::Type const& _type);
 
 /// Returns a new symbolic variable, according to _type.
 /// Also returns whether the type is abstract or not,

libsolidity/formal/SymbolicVariables.cpp

@@ -21,8 +21,11 @@
 #include <libsolidity/formal/SymbolicTypes.h>
 #include <libsolidity/ast/AST.h>
 
+#include <libsolutil/Algorithms.h>
+
 using namespace std;
 using namespace solidity;
+using namespace solidity::util;
 using namespace solidity::smtutil;
 using namespace solidity::frontend;
 using namespace solidity::frontend::smt;
@@ -118,7 +121,7 @@ SymbolicIntVariable::SymbolicIntVariable(
 ):
 	SymbolicVariable(_type, _originalType, move(_uniqueName), _context)
 {
-	solAssert(isNumber(m_type->category()), "");
+	solAssert(isNumber(*m_type), "");
 }
 
 SymbolicAddressVariable::SymbolicAddressVariable(
@@ -218,7 +221,7 @@ SymbolicEnumVariable::SymbolicEnumVariable(
 ):
 	SymbolicVariable(_type, _type, move(_uniqueName), _context)
 {
-	solAssert(isEnum(m_type->category()), "");
+	solAssert(isEnum(*m_type), "");
 }
 
 SymbolicTupleVariable::SymbolicTupleVariable(
@@ -228,7 +231,7 @@ SymbolicTupleVariable::SymbolicTupleVariable(
 ):
 	SymbolicVariable(_type, _type, move(_uniqueName), _context)
 {
-	solAssert(isTuple(m_type->category()), "");
+	solAssert(isTuple(*m_type), "");
 }
 
 SymbolicTupleVariable::SymbolicTupleVariable(
@@ -274,7 +277,7 @@ SymbolicArrayVariable::SymbolicArrayVariable(
 		m_context
 	)
 {
-	solAssert(isArray(m_type->category()) || isMapping(m_type->category()), "");
+	solAssert(isArray(*m_type) || isMapping(*m_type), "");
 }
 
 SymbolicArrayVariable::SymbolicArrayVariable(
@@ -319,3 +322,47 @@ smtutil::Expression SymbolicArrayVariable::length()
 {
 	return m_pair.component(1);
 }
+
+SymbolicStructVariable::SymbolicStructVariable(
+	frontend::TypePointer _type,
+	string _uniqueName,
+	EncodingContext& _context
+):
+	SymbolicVariable(_type, _type, move(_uniqueName), _context)
+{
+	solAssert(isNonRecursiveStruct(*m_type), "");
+	auto const* structType = dynamic_cast<StructType const*>(_type);
+	solAssert(structType, "");
+	auto const& members = structType->structDefinition().members();
+	for (unsigned i = 0; i < members.size(); ++i)
+	{
+		solAssert(members.at(i), "");
+		m_memberIndices.emplace(members.at(i)->name(), i);
+	}
+}
+
+smtutil::Expression SymbolicStructVariable::member(string const& _member)
+{
+	return smtutil::Expression::tuple_get(currentValue(), m_memberIndices.at(_member));
+}
+
+smtutil::Expression SymbolicStructVariable::assignMember(string const& _member, smtutil::Expression const& _memberValue)
+{
+	auto const* structType = dynamic_cast<StructType const*>(m_type);
+	solAssert(structType, "");
+	auto const& structDef = structType->structDefinition();
+	auto const& structMembers = structDef.members();
+	auto oldMembers = applyMap(
+		structMembers,
+		[&](auto _member) { return member(_member->name()); }
+	);
+	increaseIndex();
+	for (unsigned i = 0; i < structMembers.size(); ++i)
+	{
+		auto const& memberName = structMembers.at(i)->name();
+		auto newMember = memberName == _member ? _memberValue : oldMembers.at(i);
+		m_context.addAssertion(member(memberName) == newMember);
+	}
+
+	return currentValue();
+}

libsolidity/formal/SymbolicVariables.h

@@ -23,6 +23,8 @@
 #include <libsolidity/ast/TypeProvider.h>
 
 #include <libsmtutil/SolverInterface.h>
+
+#include <map>
 #include <memory>
 
 namespace solidity::frontend::smt
@@ -265,4 +267,29 @@ private:
 	SymbolicTupleVariable m_pair;
 };
 
+/**
+ * Specialization of SymbolicVariable for Struct.
+ */
+class SymbolicStructVariable: public SymbolicVariable
+{
+public:
+	SymbolicStructVariable(
+		frontend::TypePointer _type,
+		std::string _uniqueName,
+		EncodingContext& _context
+	);
+
+	/// @returns the symbolic expression representing _member.
+	smtutil::Expression member(std::string const& _member);
+
+	/// @returns the symbolic expression representing this struct
+	/// with field _member updated.
+	smtutil::Expression assignMember(std::string const& _member, smtutil::Expression const& _memberValue);
+
+private:
+	std::map<std::string, unsigned> m_memberIndices;
+};
+
+
+
 }

libsolidity/interface/OptimiserSettings.h

@@ -41,7 +41,7 @@ struct OptimiserSettings
 
 			// should have good "compilability" property here.
 
-			"eul"                      // Run functional expression inliner
+			"Tpeul"                    // Run functional expression inliner
 			"xarulrul"                 // Prune a bit more in SSA
 			"xarrcL"                   // Turn into SSA again and simplify
 			"gvif"                     // Run full inliner

libsolutil/CommonData.h

@@ -209,6 +209,13 @@ std::map<V, K> invertMap(std::map<K, V> const& originalMap)
 	return inverseMap;
 }
 
+/// Returns a set of keys of a map.
+template <typename K, typename V>
+std::set<K> keys(std::map<K, V> const& _map)
+{
+	return applyMap(_map, [](auto const& _elem) { return _elem.first; }, std::set<K>{});
+}
+
 // String conversion functions, mainly to/from hex/nibble/byte representations.
 
 enum class WhenError

libyul/CMakeLists.txt

@@ -156,6 +156,9 @@ add_library(yul
 	optimiser/SyntacticalEquality.h
 	optimiser/TypeInfo.cpp
 	optimiser/TypeInfo.h
+	optimiser/UnusedFunctionParameterPruner.cpp
+	optimiser/UnusedFunctionParameterPruner.h
+	optimiser/UnusedFunctionsCommon.h
 	optimiser/UnusedPruner.cpp
 	optimiser/UnusedPruner.h
 	optimiser/VarDeclInitializer.cpp

libyul/optimiser/NameDisplacer.h

@@ -60,6 +60,8 @@ public:
 	void operator()(FunctionCall& _funCall) override;
 	void operator()(Block& _block) override;
 
+	std::map<YulString, YulString> const& translations() const { return m_translations; }
+
 protected:
 	/// Check if the newly introduced identifier @a _name has to be replaced.
 	void checkAndReplaceNew(YulString& _name);

libyul/optimiser/Suite.cpp

@@ -42,6 +42,7 @@
 #include <libyul/optimiser/ForLoopInitRewriter.h>
 #include <libyul/optimiser/ForLoopConditionIntoBody.h>
 #include <libyul/optimiser/Rematerialiser.h>
+#include <libyul/optimiser/UnusedFunctionParameterPruner.h>
 #include <libyul/optimiser/UnusedPruner.h>
 #include <libyul/optimiser/ExpressionSimplifier.h>
 #include <libyul/optimiser/CommonSubexpressionEliminator.h>
@@ -185,6 +186,7 @@ map<string, unique_ptr<OptimiserStep>> const& OptimiserSuite::allSteps()
 			SSAReverser,
 			SSATransform,
 			StructuralSimplifier,
+			UnusedFunctionParameterPruner,
 			UnusedPruner,
 			VarDeclInitializer
 		>();
@@ -221,6 +223,7 @@ map<string, char> const& OptimiserSuite::stepNameToAbbreviationMap()
 		{SSAReverser::name,                   'V'},
 		{SSATransform::name,                  'a'},
 		{StructuralSimplifier::name,          't'},
+		{UnusedFunctionParameterPruner::name, 'p'},
 		{UnusedPruner::name,                  'u'},
 		{VarDeclInitializer::name,            'd'},
 	};

libyul/optimiser/UnusedFunctionParameterPruner.cpp

@@ -0,0 +1,127 @@
+/*
+	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/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+/**
+ * UnusedFunctionParameterPruner: Optimiser step that removes unused parameters from function
+ * definition.
+ */
+
+#include <libyul/optimiser/UnusedFunctionParameterPruner.h>
+#include <libyul/optimiser/UnusedFunctionsCommon.h>
+#include <libyul/optimiser/OptimiserStep.h>
+#include <libyul/optimiser/NameCollector.h>
+#include <libyul/optimiser/NameDisplacer.h>
+#include <libyul/optimiser/NameDispenser.h>
+#include <libyul/YulString.h>
+#include <libyul/AsmData.h>
+
+#include <libsolutil/CommonData.h>
+
+#include <boost/algorithm/cxx11/all_of.hpp>
+
+#include <optional>
+#include <variant>
+
+using namespace std;
+using namespace solidity::util;
+using namespace solidity::yul;
+using namespace solidity::yul::unusedFunctionsCommon;
+
+void UnusedFunctionParameterPruner::run(OptimiserStepContext& _context, Block& _ast)
+{
+	map<YulString, size_t> references = ReferencesCounter::countReferences(_ast);
+	auto used = [&](auto v) -> bool { return references.count(v.name); };
+
+	// Function name and a pair of boolean masks, the first corresponds to parameters and the second
+	// corresponds to returnVariables.
+	//
+	// For the first vector in the pair, a value `false` at index `i` indicates that the function
+	// argument at index `i` in `FunctionDefinition::parameters` is unused inside the function body.
+	//
+	// Similarly for the second vector in the pair, a value `false` at index `i` indicates that the
+	// return parameter at index `i` in `FunctionDefinition::returnVariables` is unused inside
+	// function body.
+	map<YulString, pair<vector<bool>, vector<bool>>> usedParametersAndReturnVariables;
+
+	// Step 1 of UnusedFunctionParameterPruner: Find functions whose parameters (both arguments and
+	// return-parameters) are not used in its body.
+	for (auto const& statement: _ast.statements)
+		if (holds_alternative<FunctionDefinition>(statement))
+		{
+			FunctionDefinition const& f = std::get<FunctionDefinition>(statement);
+
+			if (tooSimpleToBePruned(f) || boost::algorithm::all_of(f.parameters + f.returnVariables, used))
+				continue;
+
+			usedParametersAndReturnVariables[f.name] = {
+				applyMap(f.parameters, used),
+				applyMap(f.returnVariables, used)
+			};
+		}
+
+	set<YulString> functionNamesToFree = util::keys(usedParametersAndReturnVariables);
+
+	// Step 2 of UnusedFunctionParameterPruner: Renames the function and replaces all references to
+	// the function, say `f`, by its new name, say `f_1`.
+	NameDisplacer replace{_context.dispenser, functionNamesToFree};
+	replace(_ast);
+
+	// Inverse-Map of the above translations. In the above example, this will store an element with
+	// key `f_1` and value `f`.
+	std::map<YulString, YulString> newToOriginalNames = invertMap(replace.translations());
+
+	// Step 3 of UnusedFunctionParameterPruner: introduce a new function in the block with body of
+	// the old one. Replace the body of the old one with a function call to the new one with reduced
+	// parameters.
+	//
+	// For example: introduce a new 'linking' function `f` with the same the body as `f_1`, but with
+	// reduced parameters, i.e., `function f() -> y { y := 1 }`. Now replace the body of `f_1` with
+	// a call to `f`, i.e., `f_1(x) -> y { y := f() }`.
+	iterateReplacing(_ast.statements, [&](Statement& _s) -> optional<vector<Statement>> {
+		if (holds_alternative<FunctionDefinition>(_s))
+		{
+			// The original function except that it has a new name (e.g., `f_1`)
+			FunctionDefinition& originalFunction = get<FunctionDefinition>(_s);
+			if (newToOriginalNames.count(originalFunction.name))
+			{
+
+				YulString linkingFunctionName = originalFunction.name;
+				YulString originalFunctionName = newToOriginalNames.at(linkingFunctionName);
+				pair<vector<bool>, vector<bool>> used =
+					usedParametersAndReturnVariables.at(originalFunctionName);
+
+				FunctionDefinition linkingFunction = createLinkingFunction(
+					originalFunction,
+					used,
+					originalFunctionName,
+					linkingFunctionName,
+					_context.dispenser
+				);
+
+				originalFunction.name = originalFunctionName;
+				originalFunction.parameters =
+					filter(originalFunction.parameters, used.first);
+				originalFunction.returnVariables =
+					filter(originalFunction.returnVariables, used.second);
+
+				return make_vector<Statement>(move(originalFunction), move(linkingFunction));
+			}
+		}
+
+		return nullopt;
+	});
+}

libyul/optimiser/UnusedFunctionParameterPruner.h

@@ -0,0 +1,52 @@
+/*
+	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/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <libyul/optimiser/OptimiserStep.h>
+
+namespace solidity::yul
+{
+
+/**
+ * UnusedFunctionParameterPruner: Optimiser step that removes unused parameters in a function.
+ *
+ * If a parameter is unused, like `c` and `y` in, `function f(a,b,c) -> x, y { x := div(a,b) }`
+ *
+ * We remove the parameter and create a new "linking" function as follows:
+ *
+ * `function f(a,b) -> x { x := div(a,b) }`
+ * `function f2(a,b,c) -> x, y { x := f(a,b) }`
+ *
+ * and replace all references to `f` by `f2`.
+ * The inliner should be run afterwards to make sure that all references to `f2` are replaced by
+ * `f`.
+ *
+ * Prerequisites: Disambiguator, FunctionHoister, LiteralRematerialiser
+ *
+ * The step LiteralRematerialiser is not required for correctness. It helps deal with cases such as:
+ * `function f(x) -> y { revert(y, y} }` where the literal `y` will be replaced by its value `0`,
+ * allowing us to rewrite the function.
+ */
+struct UnusedFunctionParameterPruner
+{
+	static constexpr char const* name{"UnusedFunctionParameterPruner"};
+	static void run(OptimiserStepContext& _context, Block& _ast);
+};
+
+}

libyul/optimiser/UnusedFunctionsCommon.h

@@ -0,0 +1,103 @@
+/*
+	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/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+#pragma once
+
+#include <libyul/optimiser/Metrics.h>
+#include <libyul/optimiser/NameDispenser.h>
+#include <libyul/AsmData.h>
+#include <libyul/Dialect.h>
+#include <libyul/Exceptions.h>
+
+#include <liblangutil/SourceLocation.h>
+
+#include <libsolutil/CommonData.h>
+
+#include <variant>
+
+namespace solidity::yul::unusedFunctionsCommon
+{
+
+template<typename T>
+std::vector<T> filter(std::vector<T> const& _vec, std::vector<bool> const& _mask)
+{
+	yulAssert(_vec.size() == _mask.size(), "");
+
+	std::vector<T> ret;
+
+	for (size_t i = 0; i < _mask.size(); ++i)
+		if (_mask[i])
+			ret.push_back(_vec[i]);
+
+	return ret;
+}
+
+/// Returns true if applying UnusedFunctionParameterPruner is not helpful or redundant because the
+/// inliner will be able to handle it anyway.
+bool tooSimpleToBePruned(FunctionDefinition const& _f)
+{
+	return _f.body.statements.size() <= 1 && CodeSize::codeSize(_f.body) <= 1;
+}
+
+FunctionDefinition createLinkingFunction(
+	FunctionDefinition const& _original,
+	std::pair<std::vector<bool>, std::vector<bool>> const& _usedParametersAndReturns,
+	YulString const& _originalFunctionName,
+	YulString const& _linkingFunctionName,
+	NameDispenser& _nameDispenser
+)
+{
+	auto generateTypedName = [&](TypedName t)
+	{
+		return TypedName{
+			t.location,
+			_nameDispenser.newName(t.name),
+			t.type
+		};
+	};
+
+	langutil::SourceLocation loc = _original.location;
+
+	FunctionDefinition linkingFunction{
+		loc,
+		_linkingFunctionName,
+		util::applyMap(_original.parameters, generateTypedName),
+		util::applyMap(_original.returnVariables, generateTypedName),
+		{loc, {}} // body
+	};
+
+	FunctionCall call{loc, Identifier{loc, _originalFunctionName}, {}};
+	for (auto const& p: filter(linkingFunction.parameters, _usedParametersAndReturns.first))
+		call.arguments.emplace_back(Identifier{loc, p.name});
+
+	Assignment assignment{loc, {}, nullptr};
+
+	for (auto const& r: filter(linkingFunction.returnVariables, _usedParametersAndReturns.second))
+		assignment.variableNames.emplace_back(Identifier{loc, r.name});
+
+	if (assignment.variableNames.empty())
+		linkingFunction.body.statements.emplace_back(ExpressionStatement{loc, std::move(call)});
+	else
+	{
+		assignment.value = std::make_unique<Expression>(std::move(call));
+		linkingFunction.body.statements.emplace_back(std::move(assignment));
+	}
+
+	return linkingFunction;
+}
+
+}

scripts/ASTImportTest.sh

@@ -1,10 +1,15 @@
 #!/usr/bin/env bash
 
+set -e
+
 # Bash script to test the ast-import option of the compiler by
 # first exporting a .sol file to JSON, then loading it into the compiler
 # and exporting it again. The second JSON should be identical to the first
-
+READLINK=readlink
-REPO_ROOT=$(readlink -f "$(dirname "$0")"/..)
+if [[ "$OSTYPE" == "darwin"* ]]; then
+    READLINK=greadlink
+fi
+REPO_ROOT=$(${READLINK} -f "$(dirname "$0")"/..)
 SOLIDITY_BUILD_DIR=${SOLIDITY_BUILD_DIR:-${REPO_ROOT}/build}
 SOLC=${SOLIDITY_BUILD_DIR}/solc/solc
 SPLITSOURCES=${REPO_ROOT}/scripts/splitSources.py
@@ -83,8 +88,11 @@ do
     FILETMP=$(mktemp -d)
     cd $FILETMP
 
+    set +e
     OUTPUT=$($SPLITSOURCES $solfile)
-    if [ $? != 1 ]
+    SPLITSOURCES_RC=$?
+    set -e
+    if [ ${SPLITSOURCES_RC} == 0 ]
     then
         # echo $OUTPUT
         NSOURCES=$((NSOURCES - 1))
@@ -93,9 +101,26 @@ do
             testImportExportEquivalence $i $OUTPUT
             NSOURCES=$((NSOURCES + 1))
         done
-
+    elif [ ${SPLITSOURCES_RC} == 1 ]
-    else
+    then
         testImportExportEquivalence $solfile
+    elif [ ${SPLITSOURCES_RC} == 2 ]
+    then
+        # The script will exit with return code 2, if an UnicodeDecodeError occurred.
+        # This is the case if e.g. some tests are using invalid utf-8 sequences. We will ignore
+        # these errors, but print the actual output of the script.
+        echo -e "\n${OUTPUT}\n"
+        testImportExportEquivalence $solfile
+    else
+        # All other return codes will be treated as critical errors. The script will exit.
+        echo -e "\nGot unexpected return code ${SPLITSOURCES_RC} from ${SPLITSOURCES}. Aborting."
+        echo -e "\n${OUTPUT}\n"
+
+        cd $WORKINGDIR
+        # Delete temporary files
+        rm -rf $FILETMP
+
+        exit 1
     fi
 
     cd $WORKINGDIR

scripts/release_ppa.sh

@@ -158,7 +158,7 @@ Vcs-Git: git://github.com/ethereum/solidity.git
 Vcs-Browser: https://github.com/ethereum/solidity
 
 Package: solc
-Architecture: any-i386 any-amd64
+Architecture: any-amd64
 Multi-Arch: same
 Depends: \${shlibs:Depends}, \${misc:Depends}
 Conflicts: libethereum (<= 1.2.9)

scripts/splitSources.py

@@ -11,10 +11,20 @@
 
 import sys
 import os
+import traceback
 
 hasMultipleSources = False
 createdSources = []
 
+
+def uncaught_exception_hook(exc_type, exc_value, exc_traceback):
+    # The script `scripts/ASTImportTest.sh` will interpret return code 3
+    # as a critical error (because of the uncaught exception) and will
+    # terminate further execution.
+    print("Unhandled exception: %s", "".join(traceback.format_exception(exc_type, exc_value, exc_traceback)))
+    sys.exit(3)
+
+
 def extractSourceName(line):
     if line.find("/") > -1:
         filePath = line[13: line.rindex("/")]
@@ -23,6 +33,7 @@ def extractSourceName(line):
         return filePath, srcName
     return False, line[line.find(":")+2 : line.find(" ====")]
 
+
 # expects the first line of lines to be "==== Source: sourceName ===="
 # writes the following source into a file named sourceName
 def writeSourceToFile(lines):
@@ -45,8 +56,12 @@ def writeSourceToFile(lines):
             writeSourceToFile(lines[1+idx:])
             break
 
+
 if __name__ == '__main__':
     filePath = sys.argv[1]
+    sys.excepthook = uncaught_exception_hook
+
+    try:
         # decide if file has multiple sources
         lines = open(filePath, mode='r', encoding='utf8').read().splitlines()
         if lines[0][:12] == "==== Source:":
@@ -58,5 +73,12 @@ if __name__ == '__main__':
             for src in createdSources:
                 srcString += src + ' '
             print(srcString)
+            sys.exit(0)
         else:
             sys.exit(1)
+
+    except UnicodeDecodeError as ude:
+        print("UnicodeDecodeError in '" + filePath + "': " + str(ude))
+        print("This is expected for some tests containing invalid utf8 sequences. "
+              "Exception will be ignored.")
+        sys.exit(2)

scripts/test_antlr_grammar.sh

@@ -2,7 +2,11 @@
 
 set -e
 
-ROOT_DIR=$(readlink -f "$(dirname "$0")"/..)
+READLINK=readlink
+if [[ "$OSTYPE" == "darwin"* ]]; then
+    READLINK=greadlink
+fi
+ROOT_DIR=$(${READLINK} -f "$(dirname "$0")"/..)
 WORKDIR="${ROOT_DIR}/build/antlr"
 ANTLR_JAR="${ROOT_DIR}/build/deps/antlr4.jar"
 ANTLR_JAR_URI="https://www.antlr.org/download/antlr-4.8-complete.jar"
@@ -54,7 +58,7 @@ failed_count=0
 test_file()
 {
   local SOL_FILE
-  SOL_FILE="$(readlink -m "${1}")"
+  SOL_FILE="$(${READLINK}  -m "${1}")"
   local cur=${2}
   local max=${3}
   local solOrYul=${4}

test/cmdlineTests/evm_to_wasm_break/output

@@ -31,9 +31,10 @@ object "object" {
             let x_6 := x_2
             let x_7 := x_3
             let _2 := 1
-            let _3:i32 := i32.eqz(i32.eqz(i64.eqz(i64.or(i64.or(_1, _1), i64.or(_1, _2)))))
+            let _3 := i64.or(_1, _1)
+            let _4:i32 := i32.eqz(i32.eqz(i64.eqz(i64.or(_3, i64.or(_1, _2)))))
             for { }
-            i32.eqz(_3)
+            i32.eqz(_4)
             {
                 let x_8, x_9, x_10, x_11 := add(x_4, x_5, x_6, x_7, _1, _1, _1, _2)
                 x_4 := x_8
@@ -42,13 +43,10 @@ object "object" {
                 x_7 := x_11
             }
             {
-                let _4, _5, _6, _7 := lt(x_4, x_5, x_6, x_7, _1, _1, _1, 10)
+                let _5, _6, _7, _8 := iszero_170_789(_1, _1, _1, lt_172(x_4, x_5, x_6, x_7, _1, _1, _1, 10))
-                let _8, _9, _10, _11 := iszero(_4, _5, _6, _7)
+                if i32.eqz(i64.eqz(i64.or(i64.or(_5, _6), i64.or(_7, _8)))) { break }
-                if i32.eqz(i64.eqz(i64.or(i64.or(_8, _9), i64.or(_10, _11)))) { break }
+                if i32.eqz(i64.eqz(i64.or(_3, i64.or(_1, eq(x_4, x_5, x_6, x_7, _1, _1, _1, 2))))) { break }
-                let _12, _13, _14, _15 := eq(x_4, x_5, x_6, x_7, _1, _1, _1, 2)
+                if i32.eqz(i64.eqz(i64.or(_3, i64.or(_1, eq(x_4, x_5, x_6, x_7, _1, _1, _1, 4))))) { continue }
-                if i32.eqz(i64.eqz(i64.or(i64.or(_12, _13), i64.or(_14, _15)))) { break }
-                let _16, _17, _18, _19 := eq(x_4, x_5, x_6, x_7, _1, _1, _1, 4)
-                if i32.eqz(i64.eqz(i64.or(i64.or(_16, _17), i64.or(_18, _19)))) { continue }
             }
             sstore(_1, _1, _1, _1, x_4, x_5, x_6, x_7)
         }
@@ -69,11 +67,11 @@ object "object" {
             let r1_1, carry_2 := add_carry(x1, y1, carry_1)
             r1 := r1_1
         }
-        function iszero(x1, x2, x3, x4) -> r1, r2, r3, r4
+        function iszero_170_789(x1, x2, x3, x4) -> r1, r2, r3, r4
         {
             r4 := i64.extend_i32_u(i64.eqz(i64.or(i64.or(x1, x2), i64.or(x3, x4))))
         }
-        function eq(x1, x2, x3, x4, y1, y2, y3, y4) -> r1, r2, r3, r4
+        function eq(x1, x2, x3, x4, y1, y2, y3, y4) -> r4
         {
             if i64.eq(x1, y1)
             {
@@ -89,7 +87,7 @@ object "object" {
             case 1:i32 { r := 0xffffffff:i32 }
             default { r := i64.ne(a, b) }
         }
-        function lt(x1, x2, x3, x4, y1, y2, y3, y4) -> z1, z2, z3, z4
+        function lt_172(x1, x2, x3, x4, y1, y2, y3, y4) -> z4
         {
             let z:i32 := false
             switch cmp(x1, y1)
@@ -154,7 +152,7 @@ object "object" {
 
 
 Binary representation:
-0061736d0100000001480a60000060017e017e60027e7e017f60037e7e7e017e60047e7e7e7e017e60087e7e7e7e7e7e7e7e0060087e7e7e7e7e7e7e7e017e60057f7e7e7e7e0060027f7f0060037f7f7f0002310208657468657265756d0c73746f7261676553746f7265000808657468657265756d0c63616c6c44617461436f70790009030e0d0003060406020604010101070505030100010610037e0142000b7e0142000b7e0142000b071102066d656d6f72790200046d61696e00020ac3080dde02030a7e017f147e02404200210002402000200020002000100921012300210223012103230221040b20012105200221062003210720042108420121092000200084200020098484504545210a02400340200a45450d01024002402005200620072008200020002000420a1008210b2300210c2301210d2302210e0b0240200b200c200d200e1005210f2300211023012111230221120b200f201084201120128484504504400c030b024020052006200720082000200020004202100621132300211423012115230221160b2013201484201520168484504504400c030b0240200520062007200820002000200042041006211723002118230121192302211a0b20172018842019201a8484504504400c010b0b0240200520062007200820002000200020091004211b2300211c2301211d2302211e0b201b2105201c2106201d2107201e21080c000b0b20002000200020002005200620072008100e0b0b2901037e0240200020017c2105200520027c21032005200054200320055472ad21040b2004240020030b6c010b7e0240200320077c210c200c42007c210b024020022006200c200354200b200c5472ad1003210d2300210e0b200d210a024020012005200e1003210f230021100b200f2109024020002004201010032111230021120b201121080b20092400200a2401200b240220080b2401047e0240200020018420022003848450ad21070b20052400200624012007240220040b3901047e0240200020045104402001200551044020022006510440200320075104404201210b0b0b0b0b0b20092400200a2401200b240220080b2701027f024002402000200154210320034101460440417f210205200020015221020b0b0b20020b960102047e047f02404100210c0240200020041007210d200d41004604400240200120051007210e200e41004604400240200220061007210f200f41004604402003200754210c05200f41014604404100210c054101210c0b0b0b05200e41014604404100210c054101210c0b0b0b05200d41014604404100210c054101210c0b0b0b200cad210b0b20092400200a2401200b240220080b7601087e024042002000200184200284520440000b42002003422088520440000b41002003a7412010014100290000100c2108410041086a290000100c2109410041106a290000100c210a410041186a290000100c210b2008210420092105200a2106200b21070b20052400200624012007240220040b1f01017e024020004208864280fe0383200042088842ff01838421010b20010b1e01027e02402000100a421086210220022000421088100a8421010b20010b1e01027e02402000100b422086210220022000422088100b8421010b20010b3200024020002001100c370000200041086a2002100c370000200041106a2003100c370000200041186a2004100c3700000b0b2300024041002000200120022003100d41202004200520062007100d4100412010000b0b
+0061736d0100000001480a60000060017e017e60027e7e017f60037e7e7e017e60047e7e7e7e017e60087e7e7e7e7e7e7e7e0060087e7e7e7e7e7e7e7e017e60057f7e7e7e7e0060027f7f0060037f7f7f0002310208657468657265756d0c73746f7261676553746f7265000808657468657265756d0c63616c6c44617461436f70790009030e0d0003060406020604010101070505030100010610037e0142000b7e0142000b7e0142000b071102066d656d6f72790200046d61696e00020af0070da302030b7e017f087e02404200210002402000200020002000100921012300210223012103230221040b20012105200221062003210720042108420121092000200084210a200a200020098484504545210b02400340200b45450d01024002402000200020002005200620072008200020002000420a10081005210c2300210d2301210e2302210f0b200c200d84200e200f8484504504400c030b200a20002005200620072008200020002000420210068484504504400c030b200a20002005200620072008200020002000420410068484504504400c010b0b024020052006200720082000200020002009100421102300211123012112230221130b201021052011210620122107201321080c000b0b20002000200020002005200620072008100e0b0b2901037e0240200020017c2105200520027c21032005200054200320055472ad21040b2004240020030b6c010b7e0240200320077c210c200c42007c210b024020022006200c200354200b200c5472ad1003210d2300210e0b200d210a024020012005200e1003210f230021100b200f2109024020002004201010032111230021120b201121080b20092400200a2401200b240220080b2401047e0240200020018420022003848450ad21070b20052400200624012007240220040b2d01017e024020002004510440200120055104402002200651044020032007510440420121080b0b0b0b0b20080b2701027f024002402000200154210320034101460440417f210205200020015221020b0b0b20020b8a0102017e047f0240410021090240200020041007210a200a41004604400240200120051007210b200b41004604400240200220061007210c200c41004604402003200754210905200c41014604404100210905410121090b0b0b05200b41014604404100210905410121090b0b0b05200a41014604404100210905410121090b0b0b2009ad21080b20080b7601087e024042002000200184200284520440000b42002003422088520440000b41002003a7412010014100290000100c2108410041086a290000100c2109410041106a290000100c210a410041186a290000100c210b2008210420092105200a2106200b21070b20052400200624012007240220040b1f01017e024020004208864280fe0383200042088842ff01838421010b20010b1e01027e02402000100a421086210220022000421088100a8421010b20010b1e01027e02402000100b422086210220022000422088100b8421010b20010b3200024020002001100c370000200041086a2002100c370000200041106a2003100c370000200041186a2004100c3700000b0b2300024041002000200120022003100d41202004200520062007100d4100412010000b0b
 
 Text representation:
 (module
@@ -177,23 +175,12 @@ Text representation:
     (local $x_6 i64)
     (local $x_7 i64)
     (local $_2 i64)
-    (local $_3 i32)
+    (local $_3 i64)
-    (local $_4 i64)
+    (local $_4 i32)
     (local $_5 i64)
     (local $_6 i64)
     (local $_7 i64)
     (local $_8 i64)
-    (local $_9 i64)
-    (local $_10 i64)
-    (local $_11 i64)
-    (local $_12 i64)
-    (local $_13 i64)
-    (local $_14 i64)
-    (local $_15 i64)
-    (local $_16 i64)
-    (local $_17 i64)
-    (local $_18 i64)
-    (local $_19 i64)
     (local $x_8 i64)
     (local $x_9 i64)
     (local $x_10 i64)
@@ -212,46 +199,26 @@ Text representation:
         (local.set $x_6 (local.get $x_2))
         (local.set $x_7 (local.get $x_3))
         (local.set $_2 (i64.const 1))
-        (local.set $_3 (i32.eqz (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_1) (local.get $_1)) (i64.or (local.get $_1) (local.get $_2)))))))
+        (local.set $_3 (i64.or (local.get $_1) (local.get $_1)))
+        (local.set $_4 (i32.eqz (i32.eqz (i64.eqz (i64.or (local.get $_3) (i64.or (local.get $_1) (local.get $_2)))))))
         (block $label__3
             (loop $label__5
-                (br_if $label__3 (i32.eqz (i32.eqz (local.get $_3))))
+                (br_if $label__3 (i32.eqz (i32.eqz (local.get $_4))))
                 (block $label__4
                     (block
-                        (local.set $_4 (call $lt (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 10)))
+                        (local.set $_5 (call $iszero_170_789 (local.get $_1) (local.get $_1) (local.get $_1) (call $lt_172 (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 10))))
-                        (local.set $_5 (global.get $global_))
+                        (local.set $_6 (global.get $global_))
-                        (local.set $_6 (global.get $global__1))
+                        (local.set $_7 (global.get $global__1))
-                        (local.set $_7 (global.get $global__2))
+                        (local.set $_8 (global.get $global__2))
 
                     )
-                    (block
+                    (if (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_5) (local.get $_6)) (i64.or (local.get $_7) (local.get $_8))))) (then
-                        (local.set $_8 (call $iszero (local.get $_4) (local.get $_5) (local.get $_6) (local.get $_7)))
-                        (local.set $_9 (global.get $global_))
-                        (local.set $_10 (global.get $global__1))
-                        (local.set $_11 (global.get $global__2))
-
-                    )
-                    (if (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_8) (local.get $_9)) (i64.or (local.get $_10) (local.get $_11))))) (then
                         (br $label__3)
                     ))
-                    (block
+                    (if (i32.eqz (i64.eqz (i64.or (local.get $_3) (i64.or (local.get $_1) (call $eq (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 2)))))) (then
-                        (local.set $_12 (call $eq (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 2)))
-                        (local.set $_13 (global.get $global_))
-                        (local.set $_14 (global.get $global__1))
-                        (local.set $_15 (global.get $global__2))
-
-                    )
-                    (if (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_12) (local.get $_13)) (i64.or (local.get $_14) (local.get $_15))))) (then
                         (br $label__3)
                     ))
-                    (block
+                    (if (i32.eqz (i64.eqz (i64.or (local.get $_3) (i64.or (local.get $_1) (call $eq (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 4)))))) (then
-                        (local.set $_16 (call $eq (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 4)))
-                        (local.set $_17 (global.get $global_))
-                        (local.set $_18 (global.get $global__1))
-                        (local.set $_19 (global.get $global__2))
-
-                    )
-                    (if (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_16) (local.get $_17)) (i64.or (local.get $_18) (local.get $_19))))) (then
                         (br $label__4)
                     ))
 
@@ -343,7 +310,7 @@ Text representation:
     (local.get $r1)
 )
 
-(func $iszero
+(func $iszero_170_789
     (param $x1 i64)
     (param $x2 i64)
     (param $x3 i64)
@@ -373,9 +340,6 @@ Text representation:
     (param $y3 i64)
     (param $y4 i64)
     (result i64)
-    (local $r1 i64)
-    (local $r2 i64)
-    (local $r3 i64)
     (local $r4 i64)
     (block $label__9
         (if (i64.eq (local.get $x1) (local.get $y1)) (then
@@ -389,10 +353,7 @@ Text representation:
         ))
 
     )
-    (global.set $global_ (local.get $r2))
+    (local.get $r4)
-    (global.set $global__1 (local.get $r3))
-    (global.set $global__2 (local.get $r4))
-    (local.get $r1)
 )
 
 (func $cmp
@@ -416,7 +377,7 @@ Text representation:
     (local.get $r)
 )
 
-(func $lt
+(func $lt_172
     (param $x1 i64)
     (param $x2 i64)
     (param $x3 i64)
@@ -426,9 +387,6 @@ Text representation:
     (param $y3 i64)
     (param $y4 i64)
     (result i64)
-    (local $z1 i64)
-    (local $z2 i64)
-    (local $z3 i64)
     (local $z4 i64)
     (local $z i32)
     (local $condition_12 i32)
@@ -476,10 +434,7 @@ Text representation:
         (local.set $z4 (i64.extend_i32_u (local.get $z)))
 
     )
-    (global.set $global_ (local.get $z2))
+    (local.get $z4)
-    (global.set $global__1 (local.get $z3))
-    (global.set $global__2 (local.get $z4))
-    (local.get $z1)
 )
 
 (func $calldataload

test/cmdlineTests/yul_stack_opt/input.sol

@@ -17,6 +17,21 @@
 		sstore(add(a, 10), b)
 		sstore(add(a, 11), b)
 		sstore(add(a, 12), b)
+		a3 := 1
+		b3 := 1
+		c3 := 1
+		d3 := 1
+		e3 := 1
+		f3 := 1
+		g3 := 1
+		h3 := 1
+		i3 := 1
+		j3 := 1
+		k3 := 1
+		l3 := 1
+		m3 := 1
+		o3 := 1
+		p3 := 1
 	}
 	let a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1 := fun()
 	let a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2 := fun()

test/cmdlineTests/yul_stack_opt/output

@@ -5,11 +5,11 @@ Pretty printed source:
 object "object" {
     code {
         {
-            let a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1 := fun()
+            let a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, o3, p3 := fun()
-            let a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2 := fun()
+            let a3_1, b3_1, c3_1, d3_1, e3_1, f3_1, g3_1, h3_1, i3_1, j3_1, k3_1, l3_1, m3_1, o3_1, p3_1 := fun()
-            sstore(a1, a2)
+            sstore(a3, a3_1)
         }
-        function fun() -> a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3
+        function fun() -> a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, o3, p3
         {
             let _1 := 1
             sstore(_1, _1)
@@ -25,21 +25,35 @@ object "object" {
             sstore(11, _1)
             sstore(12, _1)
             sstore(13, _1)
+            a3 := _1
+            b3 := _1
+            c3 := _1
+            d3 := _1
+            e3 := _1
+            f3 := _1
+            g3 := _1
+            h3 := _1
+            i3 := _1
+            j3 := _1
+            k3 := _1
+            l3 := _1
+            m3 := _1
+            o3 := _1
+            p3 := _1
         }
     }
 }
 
 
 Binary representation:
-60056032565b505050505050505050505050505050601a6032565b5050505050505050505050505050508082555050609b565b60006000600060006000600060006000600060006000600060006000600060006001808155806002558060035580600455806005558060065580600755806008558060095580600a5580600b5580600c5580600d55505b909192939495969798999a9b9c9d9e9f565b
+60056030565b505050505050505050505050505060196030565b5050505050505050505050505050808255505060c3565b6000600060006000600060006000600060006000600060006000600060006001808155806002558060035580600455806005558060065580600755806008558060095580600a5580600b5580600c5580600d55809f50809e50809d50809c50809b50809a50809950809850809750809650809550809450809350809250809150505b909192939495969798999a9b9c9d9e565b
 
 Text representation:
-    /* "yul_stack_opt/input.sol":495:500   */
+    /* "yul_stack_opt/input.sol":3:573   */
   tag_1
   tag_2
   jump	// in
 tag_1:
-    /* "yul_stack_opt/input.sol":425:500   */
   pop
   pop
   pop
@@ -54,13 +68,10 @@ tag_1:
   pop
   pop
   pop
-  pop
-    /* "yul_stack_opt/input.sol":572:577   */
   tag_3
   tag_2
   jump	// in
 tag_3:
-    /* "yul_stack_opt/input.sol":502:577   */
   pop
   pop
   pop
@@ -75,16 +86,15 @@ tag_3:
   pop
   pop
   pop
-  pop
+    /* "yul_stack_opt/input.sol":740:742   */
-    /* "yul_stack_opt/input.sol":590:592   */
   dup1
-    /* "yul_stack_opt/input.sol":586:588   */
+    /* "yul_stack_opt/input.sol":736:738   */
   dup3
-    /* "yul_stack_opt/input.sol":579:593   */
+    /* "yul_stack_opt/input.sol":729:743   */
   sstore
   pop
   pop
-    /* "yul_stack_opt/input.sol":3:423   */
+    /* "yul_stack_opt/input.sol":3:573   */
   jump(tag_4)
 tag_2:
   0x00
@@ -101,7 +111,6 @@ tag_2:
   0x00
   0x00
   0x00
-  0x00
   0x00
     /* "yul_stack_opt/input.sol":98:99   */
   0x01
@@ -181,8 +190,83 @@ tag_2:
   0x0d
     /* "yul_stack_opt/input.sol":399:420   */
   sstore
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":423:430   */
+  swap16
   pop
-    /* "yul_stack_opt/input.sol":85:423   */
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":433:440   */
+  swap15
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":443:450   */
+  swap14
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":453:460   */
+  swap13
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":463:470   */
+  swap12
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":473:480   */
+  swap11
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":483:490   */
+  swap10
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":493:500   */
+  swap9
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":503:510   */
+  swap8
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":513:520   */
+  swap7
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":523:530   */
+  swap6
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":533:540   */
+  swap5
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":543:550   */
+  swap4
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":553:560   */
+  swap3
+  pop
+    /* "yul_stack_opt/input.sol":98:99   */
+  dup1
+    /* "yul_stack_opt/input.sol":563:570   */
+  swap2
+  pop
+  pop
+    /* "yul_stack_opt/input.sol":85:573   */
 tag_5:
   swap1
   swap2
@@ -199,6 +283,5 @@ tag_5:
   swap13
   swap14
   swap15
-  swap16
   jump	// out
 tag_4:

test/libsolidity/StandardCompiler.cpp

@@ -29,6 +29,7 @@
 #include <libsolutil/CommonData.h>
 #include <test/Metadata.h>
 
+#include <algorithm>
 #include <set>
 
 using namespace std;
@@ -1235,9 +1236,16 @@ BOOST_AUTO_TEST_CASE(use_stack_optimization)
 	BOOST_REQUIRE(contract["evm"]["bytecode"]["object"].isString());
 	BOOST_CHECK(contract["evm"]["bytecode"]["object"].asString().length() > 20);
 
-	// Now disable stack optimizations
+	// Now disable stack optimizations and UnusedFunctionParameterPruner (p)
 	// results in "stack too deep"
+	string optimiserSteps = OptimiserSettings::DefaultYulOptimiserSteps;
+	optimiserSteps.erase(
+		remove_if(optimiserSteps.begin(), optimiserSteps.end(), [](char ch) { return ch == 'p'; }),
+		optimiserSteps.end()
+	);
 	parsedInput["settings"]["optimizer"]["details"]["yulDetails"]["stackAllocation"] = false;
+	parsedInput["settings"]["optimizer"]["details"]["yulDetails"]["optimizerSteps"] = optimiserSteps;
+
 	result = compiler.compile(parsedInput);
 	BOOST_REQUIRE(result["errors"].isArray());
 	BOOST_CHECK(result["errors"][0]["severity"] == "error");

test/libsolidity/gasTests/abiv2_optimised.sol

@@ -17,9 +17,9 @@ contract C {
 // optimize-yul: true
 // ----
 // creation:
-//   codeDepositCost: 616600
+//   codeDepositCost: 614600
 //   executionCost: 651
-//   totalCost: 617251
+//   totalCost: 615251
 // external:
 //   a(): 1029
 //   b(uint256): 2084

test/libsolidity/semanticTests/array/array_copy_memory_to_storage.sol

@@ -0,0 +1,11 @@
+contract C {
+    uint[] a;
+    function f() public returns (uint, uint) {
+        uint[] memory b = new uint[](3);
+        b[0] = 1;
+        a = b;
+        return (a[0], a.length);
+    }
+}
+// ----
+// f() -> 1, 3

test/libsolidity/semanticTests/array/array_copy_storage_to_memory.sol

@@ -0,0 +1,10 @@
+contract C {
+    uint[] a;
+    function f() public returns (uint, uint) {
+        a.push(1); a.push(0); a.push(0);
+        uint[] memory b = a;
+        return (b[0], b.length);
+    }
+}
+// ----
+// f() -> 1, 3

test/libsolidity/semanticTests/array/bytes_memory_to_storage.sol

@@ -0,0 +1,10 @@
+contract C {
+  bytes s;
+  function f() external returns (byte) {
+    bytes memory data = "abcd";
+    s = data;
+    return s[0];
+  }
+}
+// ----
+// f() -> "a"

test/libsolidity/semanticTests/array/bytes_storage_to_memory.sol

@@ -0,0 +1,9 @@
+contract C {
+  bytes s = "abcd";
+  function f() external returns (byte) {
+    bytes memory data = s;
+    return data[0];
+  }
+}
+// ----
+// f() -> "a"

test/libsolidity/semanticTests/calldata/calldata_bytes_to_storage.sol

@@ -0,0 +1,9 @@
+contract C {
+  bytes s;
+  function f(bytes calldata data) external returns (byte) {
+    s = data;
+    return s[0];
+  }
+}
+// ----
+// f(bytes): 0x20, 0x08, "abcdefgh" -> "a"

test/libsolidity/semanticTests/intheritance/super_in_constructor.sol

@@ -30,6 +30,7 @@ contract D is B, C {
         return data;
     }
 }
-
+// ====
+// compileViaYul: also
 // ----
 // f() -> 15

test/libsolidity/semanticTests/intheritance/super_in_constructor_assignment.sol

@@ -0,0 +1,39 @@
+contract A {
+    function f() public virtual returns (uint256 r) {
+        return 1;
+    }
+}
+
+
+contract B is A {
+    function f() public virtual override returns (uint256 r) {
+        function() internal returns (uint) x = super.f;
+        return x() | 2;
+    }
+}
+
+
+contract C is A {
+    function f() public virtual override returns (uint256 r) {
+        function() internal returns (uint) x = super.f;
+        return x() | 4;
+    }
+}
+
+
+contract D is B, C {
+    uint256 data;
+
+    constructor() {
+        function() internal returns (uint) x = super.f;
+        data = x() | 8;
+    }
+
+    function f() public override (B, C) returns (uint256 r) {
+        return data;
+    }
+}
+// ====
+// compileViaYul: also
+// ----
+// f() -> 15

test/libsolidity/semanticTests/intheritance/super_overload.sol

@@ -22,6 +22,8 @@ contract C is A, B {
     }
 }
 
+// ====
+// compileViaYul: also
 // ----
 // g() -> 10
 // h() -> 2

test/libsolidity/semanticTests/structs/calldata/calldata_struct_to_memory.sol

@@ -4,15 +4,16 @@ contract C {
     struct S {
         uint256 a;
         uint256 b;
+        bytes2 c;
     }
 
-    function f(S calldata s) external pure returns (uint256, uint256) {
+    function f(S calldata s) external pure returns (uint256, uint256, byte) {
         S memory m = s;
-        return (m.a, m.b);
+        return (m.a, m.b, m.c[1]);
     }
 }
 
 // ====
 // compileViaYul: also
 // ----
-// f((uint256,uint256)): 42, 23 -> 42, 23
+// f((uint256,uint256, bytes2)): 42, 23, "ab" -> 42, 23, "b"

test/libsolidity/semanticTests/structs/calldata/calldata_struct_to_storage.sol

@@ -0,0 +1,22 @@
+pragma experimental ABIEncoderV2;
+
+contract C {
+    struct S {
+        uint256 a;
+        uint64 b;
+        bytes2 c;
+    }
+
+    uint[153] r;
+    S s;
+
+    function f(uint32 a, S calldata c, uint256 b) external returns (uint256, uint256, byte) {
+        s = c;
+        return (s.a, s.b, s.c[1]);
+    }
+}
+
+// ====
+// compileViaYul: also
+// ----
+// f(uint32, (uint256, uint64, bytes2), uint256): 1, 42, 23, "ab", 1 -> 42, 23, "b"

test/libsolidity/semanticTests/structs/struct_copy_via_local.sol

@@ -3,6 +3,7 @@ contract c {
         uint256 a;
         uint256 b;
     }
+    uint[75] r;
     Struct data1;
     Struct data2;
 
@@ -15,5 +16,7 @@ contract c {
     }
 }
 
+// ====
+// compileViaYul: also
 // ----
 // test() -> true

test/libsolidity/semanticTests/structs/struct_memory_to_storage.sol

@@ -0,0 +1,28 @@
+pragma experimental ABIEncoderV2;
+
+contract C {
+    struct S {
+        uint32 a;
+        uint128 b;
+        uint256 c;
+    }
+
+    struct X {
+        uint256 a;
+        S s;
+    }
+
+    uint[79] r;
+    X x;
+
+    function f() external returns (uint32, uint128, uint256) {
+        X memory m = X(12, S(42, 23, 34));
+        x = m;
+        return (x.s.a, x.s.b, x.s.c);
+    }
+}
+
+// ====
+// compileViaYul: also
+// ----
+// f() -> 42, 23, 34

test/libsolidity/semanticTests/structs/struct_memory_to_storage_function_ptr.sol

@@ -0,0 +1,33 @@
+pragma experimental ABIEncoderV2;
+
+contract C {
+    struct S {
+        uint32 a;
+        uint128 b;
+        uint256 c;
+        function() internal returns (uint32) f;
+    }
+
+    struct X {
+        uint256 a;
+        S s;
+    }
+
+    uint[79] r;
+    X x;
+
+    function f() external returns (uint32, uint128, uint256, uint32, uint32) {
+        X memory m = X(12, S(42, 23, 34, g));
+        x = m;
+        return (x.s.a, x.s.b, x.s.c, x.s.f(), m.s.f());
+    }
+
+    function g() internal returns (uint32) {
+        return x.s.a;
+    }
+}
+
+// ====
+// compileViaYul: false
+// ----
+// f() -> 42, 23, 34, 42, 42

test/libsolidity/semanticTests/structs/struct_named_constructor.sol

@@ -10,5 +10,7 @@ contract C {
     }
 }
 
+// ====
+// compileViaYul: also
 // ----
 // s() -> 1, true

test/libsolidity/semanticTests/structs/struct_storage_to_memory.sol

@@ -0,0 +1,26 @@
+pragma experimental ABIEncoderV2;
+
+contract C {
+    struct S {
+        uint32 a;
+        uint128 b;
+        uint256 c;
+    }
+    struct X {
+        uint32 a;
+        S s;
+    }
+
+    uint[79] arr;
+    X x = X(12, S(42, 23, 34));
+
+    function f() external returns (uint32, uint128, uint256) {
+        X memory m = x;
+        return (m.s.a, m.s.b, m.s.c);
+    }
+}
+
+// ====
+// compileViaYul: also
+// ----
+// f() -> 42, 23, 34

test/libsolidity/semanticTests/structs/struct_storage_to_memory_function_ptr.sol

@@ -0,0 +1,32 @@
+pragma experimental ABIEncoderV2;
+
+contract C {
+    struct S {
+        uint32 a;
+        uint128 b;
+        uint256 c;
+        function() internal returns (uint32) f;
+    }
+
+    struct X {
+        uint256 a;
+        S s;
+    }
+
+    uint[79] arr;
+    X x = X(12, S(42, 23, 34, g));
+
+    function f() external returns (uint32, uint128, uint256, uint32, uint32) {
+        X memory m = x;
+        return (m.s.a, m.s.b, m.s.c, m.s.f(), x.s.f());
+    }
+
+    function g() internal returns (uint32) {
+        return x.s.a;
+    }
+}
+
+// ====
+// compileViaYul: false
+// ----
+// f() -> 42, 23, 34, 42, 42

test/libsolidity/semanticTests/various/super.sol

@@ -25,5 +25,7 @@ contract D is B, C {
     }
 }
 
+// ====
+// compileViaYul: also
 // ----
 // f() -> 15

test/libsolidity/semanticTests/various/super_parentheses.sol

@@ -0,0 +1,31 @@
+contract A {
+    function f() public virtual returns (uint256 r) {
+        return 1;
+    }
+}
+
+
+contract B is A {
+    function f() public virtual override returns (uint256 r) {
+        return ((super).f)() | 2;
+    }
+}
+
+
+contract C is A {
+    function f() public virtual override returns (uint256 r) {
+        return ((super).f)() | 4;
+    }
+}
+
+
+contract D is B, C {
+    function f() public override(B, C) returns (uint256 r) {
+        return ((super).f)() | 8;
+    }
+}
+
+// ====
+// compileViaYul: also
+// ----
+// f() -> 15

test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol

@@ -11,10 +11,3 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (119-157): Assertion violation happens here
-// Warning 8115: (76-80): Assertion checker does not yet support the type of this variable.
-// Warning 8115: (83-87): Assertion checker does not yet support the type of this variable.
-// Warning 7650: (126-132): Assertion checker does not yet support this expression.
-// Warning 8364: (126-128): Assertion checker does not yet implement type struct C.S storage ref
-// Warning 7650: (143-149): Assertion checker does not yet support this expression.
-// Warning 8364: (143-145): Assertion checker does not yet implement type struct C.S storage ref

test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol

@@ -11,12 +11,3 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (121-165): Assertion violation happens here
-// Warning 8115: (78-82): Assertion checker does not yet support the type of this variable.
-// Warning 8115: (85-89): Assertion checker does not yet support the type of this variable.
-// Warning 7650: (128-134): Assertion checker does not yet support this expression.
-// Warning 8364: (128-130): Assertion checker does not yet implement type struct C.S storage ref
-// Warning 9118: (128-137): Assertion checker does not yet implement this expression.
-// Warning 7650: (148-154): Assertion checker does not yet support this expression.
-// Warning 8364: (148-150): Assertion checker does not yet implement type struct C.S storage ref
-// Warning 9118: (148-157): Assertion checker does not yet implement this expression.

test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol

@@ -15,13 +15,3 @@ contract C {
 }
 
 // ----
-// Warning 8115: (72-75): Assertion checker does not yet support the type of this variable.
-// Warning 8115: (100-103): Assertion checker does not yet support the type of this variable.
-// Warning 7650: (130-133): Assertion checker does not yet support this expression.
-// Warning 8364: (130-131): Assertion checker does not yet implement type struct C.S storage ref
-// Warning 9599: (130-133): Assertion checker does not yet implement this expression.
-// Warning 7650: (144-149): Assertion checker does not yet support this expression.
-// Warning 8364: (144-147): Assertion checker does not yet implement type struct C.S storage ref
-// Warning 7650: (144-147): Assertion checker does not yet support this expression.
-// Warning 8364: (144-145): Assertion checker does not yet implement type struct C.T storage ref
-// Warning 9599: (144-149): Assertion checker does not yet implement this expression.

test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol

@@ -16,18 +16,3 @@ contract C {
 }
 
 // ----
-// Warning 8115: (72-75): Assertion checker does not yet support the type of this variable.
-// Warning 8115: (102-105): Assertion checker does not yet support the type of this variable.
-// Warning 7650: (132-135): Assertion checker does not yet support this expression.
-// Warning 8364: (132-133): Assertion checker does not yet implement type struct C.S storage ref
-// Warning 9599: (132-135): Assertion checker does not yet implement this expression.
-// Warning 7650: (146-149): Assertion checker does not yet support this expression.
-// Warning 8364: (146-147): Assertion checker does not yet implement type struct C.T storage ref
-// Warning 8364: (146-156): Assertion checker does not yet implement type struct C.S storage ref
-// Warning 9599: (146-149): Assertion checker does not yet implement this expression.
-// Warning 7650: (160-168): Assertion checker does not yet support this expression.
-// Warning 7650: (160-163): Assertion checker does not yet support this expression.
-// Warning 8364: (160-161): Assertion checker does not yet implement type struct C.T storage ref
-// Warning 8364: (160-166): Assertion checker does not yet implement type struct C.S storage ref
-// Warning 9118: (160-166): Assertion checker does not yet implement this expression.
-// Warning 9599: (160-168): Assertion checker does not yet implement this expression.

test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol

@@ -118,23 +118,3 @@ contract PropagateThroughReturnValue {
 }
 // ----
 // Warning 2018: (1879-1947): Function state mutability can be restricted to view
-// Warning 8115: (318-332): Assertion checker does not yet support the type of this variable.
-// Warning 8115: (338-347): Assertion checker does not yet support the type of this variable.
-// Warning 8115: (353-378): Assertion checker does not yet support the type of this variable.
-// Warning 8115: (384-409): Assertion checker does not yet support the type of this variable.
-// Warning 7650: (464-479): Assertion checker does not yet support this expression.
-// Warning 8364: (464-475): Assertion checker does not yet implement type struct Reference.St storage ref
-// Warning 8182: (464-494): Assertion checker does not yet implement such assignments.
-// Warning 7650: (539-554): Assertion checker does not yet support this expression.
-// Warning 8364: (539-550): Assertion checker does not yet implement type struct Reference.St storage ref
-// Warning 7650: (557-567): Assertion checker does not yet support this expression.
-// Warning 8364: (557-563): Assertion checker does not yet implement type struct Reference.St storage ref
-// Warning 8182: (539-567): Assertion checker does not yet implement such assignments.
-// Warning 8115: (629-643): Assertion checker does not yet support the type of this variable.
-// Warning 8364: (646-668): Assertion checker does not yet implement type struct Reference.St storage ref
-// Warning 8364: (700-703): Assertion checker does not yet implement type struct Reference.St storage pointer
-// Warning 8364: (706-728): Assertion checker does not yet implement type struct Reference.St storage ref
-// Warning 8364: (700-728): Assertion checker does not yet implement type struct Reference.St storage pointer
-// Warning 7650: (748-755): Assertion checker does not yet support this expression.
-// Warning 8364: (748-751): Assertion checker does not yet implement type struct Reference.St storage pointer
-// Warning 8182: (748-770): Assertion checker does not yet implement such assignments.

test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol

@@ -8,7 +8,5 @@ contract C {
 }
 // ----
 // Warning 2072: (133-143): Unused local variable.
-// Warning 8115: (133-143): Assertion checker does not yet support the type of this variable.
 // Warning 8364: (146-147): Assertion checker does not yet implement type type(struct C.A storage pointer)
-// Warning 8364: (146-163): Assertion checker does not yet implement type struct C.A memory
 // Warning 4639: (146-163): Assertion checker does not yet implement this expression.

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol

@@ -20,3 +20,4 @@ contract LoopFor2 {
 }
 // ----
 // Warning 6328: (363-382): Assertion violation happens here
+// Warning 4661: (316-336): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol

@@ -21,3 +21,4 @@ contract LoopFor2 {
 // ----
 // Warning 6328: (341-360): Assertion violation happens here
 // Warning 6328: (364-383): Assertion violation happens here
+// Warning 4661: (317-337): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol

@@ -21,5 +21,5 @@ contract C
 	}
 }
 // ----
-// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (136-149): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint x = uint(~1);
+		// This assertion fails because type conversion is still unsupported.
+		assert(x == 2**256 - 2);
+		assert(~1 == -2);
+	}
+}
+// ----
+// Warning 6328: (169-192): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		assert(~1 | (~0xff & 0) == -2);
+		int x = ~1 | (~0xff ^ 0);
+		/// Result is negative, assertion fails.
+		assert(x > 0);
+		int y = ~x | (0xff & 1);
+		assert(y > 0);
+		assert(y & (0xffffffffffffffffff & 1) == 1);
+	}
+}
+// ----
+// Warning 6328: (181-194): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol

@@ -10,7 +10,4 @@ contract C {
 	}
 }
 // ----
-// Warning 8115: (71-74): Assertion checker does not yet support the type of this variable.
-// Warning 7650: (117-120): Assertion checker does not yet support this expression.
-// Warning 8364: (117-118): Assertion checker does not yet implement type struct C.S storage ref
 // Warning 9149: (117-125): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol

@@ -10,8 +10,4 @@ contract C {
 	}
 }
 // ----
-// Warning 8115: (73-76): Assertion checker does not yet support the type of this variable.
-// Warning 7650: (119-122): Assertion checker does not yet support this expression.
-// Warning 8364: (119-120): Assertion checker does not yet implement type struct C.S storage ref
-// Warning 9118: (119-125): Assertion checker does not yet implement this expression.
 // Warning 9149: (119-130): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/delete_struct.sol

@@ -6,7 +6,7 @@ contract C
 	{
 		uint x;
 	}
-	function f(bool b) public {
+	function f(bool b) public pure {
 		S memory s;
 		s.x = 2;
 		if (b)
@@ -17,15 +17,3 @@ contract C
 	}
 }
 // ----
-// Warning 2018: (73-192): Function state mutability can be restricted to pure
-// Warning 6328: (172-188): Assertion violation happens here
-// Warning 8115: (103-113): Assertion checker does not yet support the type of this variable.
-// Warning 7650: (117-120): Assertion checker does not yet support this expression.
-// Warning 8364: (117-118): Assertion checker does not yet implement type struct C.S memory
-// Warning 8182: (117-124): Assertion checker does not yet implement such assignments.
-// Warning 8364: (145-146): Assertion checker does not yet implement type struct C.S memory
-// Warning 7650: (165-168): Assertion checker does not yet support this expression.
-// Warning 8364: (165-166): Assertion checker does not yet implement type struct C.S memory
-// Warning 2683: (158-168): Assertion checker does not yet implement "delete" for this expression.
-// Warning 7650: (179-182): Assertion checker does not yet support this expression.
-// Warning 8364: (179-180): Assertion checker does not yet implement type struct C.S memory

test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function h() internal returns (uint[] storage) {
+		if (a[2] == 0)
+			a[2] = 3;
+		return a;
+	}
+	function g() public {
+		h()[2] = 4;
+		assert(h()[2] == 3);
+	}
+}
+// ----
+// Warning 6328: (191-210): Assertion violation happens here

test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol

@@ -8,7 +8,6 @@ contract C {
   }
 }
 // ----
-// Warning 8115: (151-159): Assertion checker does not yet support the type of this variable.
 // Warning 8364: (206-209): Assertion checker does not yet implement type abi
 // Warning 8364: (225-226): Assertion checker does not yet implement type type(struct C.S storage pointer)
 // Warning 8364: (235-241): Assertion checker does not yet implement type type(uint256[] memory)

test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol

@@ -26,4 +26,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (400-457): Assertion violation happens here.
+// Warning 6328: (400-457): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol

@@ -14,19 +14,3 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (202-226): Assertion violation happens here
-// Warning 7650: (124-130): Assertion checker does not yet support this expression.
-// Warning 8364: (124-128): Assertion checker does not yet implement type struct C.S memory
-// Warning 9118: (124-133): Assertion checker does not yet implement this expression.
-// Warning 9056: (124-136): Assertion checker does not yet implement this expression.
-// Warning 7650: (154-160): Assertion checker does not yet support this expression.
-// Warning 8364: (154-158): Assertion checker does not yet implement type struct C.S memory
-// Warning 9118: (154-163): Assertion checker does not yet implement this expression.
-// Warning 9056: (154-166): Assertion checker does not yet implement this expression.
-// Warning 7650: (182-188): Assertion checker does not yet support this expression.
-// Warning 8364: (182-186): Assertion checker does not yet implement type struct C.S memory
-// Warning 9118: (182-191): Assertion checker does not yet implement this expression.
-// Warning 9056: (182-194): Assertion checker does not yet implement this expression.
-// Warning 7650: (209-215): Assertion checker does not yet support this expression.
-// Warning 8364: (209-213): Assertion checker does not yet implement type struct C.S memory
-// Warning 9118: (209-218): Assertion checker does not yet implement this expression.

test/libsolidity/smtCheckerTests/types/enum_in_struct.sol

@@ -11,10 +11,3 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (187-208): Assertion violation happens here
-// Warning 8115: (143-153): Assertion checker does not yet support the type of this variable.
-// Warning 7650: (171-174): Assertion checker does not yet support this expression.
-// Warning 8364: (171-172): Assertion checker does not yet implement type struct C.S memory
-// Warning 8182: (171-183): Assertion checker does not yet implement such assignments.
-// Warning 7650: (194-197): Assertion checker does not yet support this expression.
-// Warning 8364: (194-195): Assertion checker does not yet implement type struct C.S memory

test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol

@@ -13,6 +13,5 @@ contract C {
 	}
 }
 // ----
-// Warning 9118: (238-244): Assertion checker does not yet implement this expression.
 // Warning 7989: (238-247): Assertion checker does not yet support index accessing fixed bytes.
 // Warning 7989: (251-257): Assertion checker does not yet support index accessing fixed bytes.

test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol

@@ -12,8 +12,5 @@ contract C
 }
 // ----
 // Warning 6838: (140-144): Condition is always false.
-// Warning 8364: (149-156): Assertion checker does not yet implement type struct C.S storage ref
 // Warning 8364: (159-160): Assertion checker does not yet implement type type(struct C.S storage pointer)
-// Warning 8364: (159-163): Assertion checker does not yet implement type struct C.S memory
 // Warning 4639: (159-163): Assertion checker does not yet implement this expression.
-// Warning 8364: (149-163): Assertion checker does not yet implement type struct C.S storage ref

test/libsolidity/smtCheckerTests/types/no_effect_statements.sol

@@ -17,7 +17,6 @@ contract test {
 // Warning 6133: (156-163): Statement has no effect.
 // Warning 8364: (125-126): Assertion checker does not yet implement type type(struct test.s storage pointer)
 // Warning 8364: (130-131): Assertion checker does not yet implement type type(struct test.s storage pointer)
-// Warning 8364: (130-136): Assertion checker does not yet implement type struct test.s memory
 // Warning 4639: (130-136): Assertion checker does not yet implement this expression.
 // Warning 8364: (140-141): Assertion checker does not yet implement type type(struct test.s storage pointer)
 // Warning 8364: (140-144): Assertion checker does not yet implement type type(struct test.s memory[7] memory)

test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_safe.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	function f() public pure {
+		S[] memory s1 = new S[](3);
+		s1[0].x = 2;
+		assert(s1[0].x == 2);
+		s1[1].t.y = 3;
+		assert(s1[1].t.y == 3);
+		s1[2].a[2] = 4;
+		assert(s1[2].a[2] == 4);
+		s1[0].ts[3].y = 5;
+		assert(s1[0].ts[3].y == 5);
+		s1[1].ts[4].a[5] = 6;
+		assert(s1[1].ts[4].a[5] == 6);
+	}
+}
+// ----
+// Warning 4588: (217-227): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol

@@ -0,0 +1,35 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	function f(S memory s2) public pure {
+		S[] memory s1 = new S[](3);
+		s1[0].x = 2;
+		assert(s1[0].x == s2.x);
+		s1[1].t.y = 3;
+		assert(s1[1].t.y == s2.t.y);
+		s1[2].a[2] = 4;
+		assert(s1[2].a[2] == s2.a[2]);
+		s1[0].ts[3].y = 5;
+		assert(s1[0].ts[3].y == s2.ts[3].y);
+		s1[1].ts[4].a[5] = 6;
+		assert(s1[1].ts[4].a[5] == s2.ts[4].a[5]);
+	}
+}
+// ----
+// Warning 6328: (257-280): Assertion violation happens here
+// Warning 6328: (301-328): Assertion violation happens here
+// Warning 6328: (350-379): Assertion violation happens here
+// Warning 6328: (404-439): Assertion violation happens here
+// Warning 6328: (467-508): Assertion violation happens here
+// Warning 4588: (228-238): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol

@@ -0,0 +1,34 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	S[] s1;
+	function f() public {
+		s1.push();
+		s1.push();
+		s1.push();
+		s1[0].x = 2;
+		assert(s1[0].x == 2);
+		s1[1].t.y = 3;
+		assert(s1[1].t.y == 3);
+		s1[2].a[2] = 4;
+		assert(s1[2].a[2] == 4);
+		s1[0].ts[3].y = 5;
+		assert(s1[0].ts[3].y == 5);
+		s1[1].ts[4].a[5] = 6;
+		assert(s1[1].ts[4].a[5] == 6);
+		s1.pop();
+		s1.pop();
+		s1.pop();
+	}
+}

test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_memory.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	function f(S memory s1, S memory s2, bool b) public pure {
+		S memory s3 = b ? s1 : s2;
+		assert(s3.x == s1.x);
+		assert(s3.x == s2.x);
+		// This is safe.
+		assert(s3.x == s1.x || s3.x == s2.x);
+		// This fails as false positive because of lack of support to aliasing.
+		s3.x = 42;
+		assert(s3.x == s1.x || s3.x == s2.x);
+	}
+}
+// ----
+// Warning 6328: (208-228): Assertion violation happens here
+// Warning 6328: (232-252): Assertion violation happens here
+// Warning 6328: (402-438): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	S s1;
+	S s2;
+	function f(bool b) public {
+		S storage s3 = b ? s1 : s2;
+		assert(s3.x == s1.x);
+		assert(s3.x == s2.x);
+		// This is safe.
+		assert(s3.x == s1.x || s3.x == s2.x);
+		// This fails as false positive because of lack of support to aliasing.
+		s3.x = 42;
+		assert(s3.x == s1.x || s3.x == s2.x);
+	}
+	function g(bool b, uint _x) public {
+		if (b)
+			s1.x = _x;
+		else
+			s2.x = _x;
+	}
+}
+// ----
+// Warning 6328: (158-178): Assertion violation happens here
+// Warning 6328: (182-202): Assertion violation happens here
+// Warning 6328: (352-388): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_safe.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	function f() public pure {
+		S memory s1;
+		s1.x = 2;
+		assert(s1.x == 2);
+		s1.t.y = 3;
+		assert(s1.t.y == 3);
+		s1.a[2] = 4;
+		assert(s1.a[2] == 4);
+		s1.ts[3].y = 5;
+		assert(s1.ts[3].y == 5);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] == 6);
+	}
+}

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol

@@ -0,0 +1,34 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	function f() public pure {
+		S memory s1;
+		s1.x = 2;
+		assert(s1.x != 2);
+		s1.t.y = 3;
+		assert(s1.t.y != 3);
+		s1.a[2] = 4;
+		assert(s1.a[2] != 4);
+		s1.ts[3].y = 5;
+		assert(s1.ts[3].y != 5);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] != 6);
+	}
+}
+// ----
+// Warning 6328: (228-245): Assertion violation happens here
+// Warning 6328: (263-282): Assertion violation happens here
+// Warning 6328: (301-321): Assertion violation happens here
+// Warning 6328: (343-366): Assertion violation happens here
+// Warning 6328: (391-417): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol

@@ -0,0 +1,34 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	function f(S memory s2) public pure {
+		S memory s1;
+		s1.x = 2;
+		assert(s1.x == s2.x);
+		s1.t.y = 3;
+		assert(s1.t.y == s2.t.y);
+		s1.a[2] = 4;
+		assert(s1.a[2] == s2.a[2]);
+		s1.ts[3].y = 5;
+		assert(s1.ts[3].y == s2.ts[3].y);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] == s2.ts[4].a[5]);
+	}
+}
+// ----
+// Warning 6328: (239-259): Assertion violation happens here
+// Warning 6328: (277-301): Assertion violation happens here
+// Warning 6328: (320-346): Assertion violation happens here
+// Warning 6328: (368-400): Assertion violation happens here
+// Warning 6328: (425-463): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_safe.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	S s1;
+	function f() public {
+		s1.x = 2;
+		assert(s1.x == 2);
+		s1.t.y = 3;
+		assert(s1.t.y == 3);
+		s1.a[2] = 4;
+		assert(s1.a[2] == 4);
+		s1.ts[3].y = 5;
+		assert(s1.ts[3].y == 5);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] == 6);
+	}
+}

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol

@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	S s1;
+	function f() public {
+		s1.x = 2;
+		assert(s1.x != 2);
+		s1.t.y = 3;
+		assert(s1.t.y != 3);
+		s1.a[2] = 4;
+		assert(s1.a[2] != 4);
+		s1.ts[3].y = 5;
+		assert(s1.ts[3].y != 5);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] != 6);
+	}
+}
+// ----
+// Warning 6328: (181-198): Assertion violation happens here
+// Warning 6328: (216-235): Assertion violation happens here
+// Warning 6328: (254-274): Assertion violation happens here
+// Warning 6328: (296-319): Assertion violation happens here
+// Warning 6328: (344-370): Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/struct/struct_delete_memory.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	function f(S memory s1, S memory s2) public pure {
+		delete s1;
+		assert(s1.x == s2.x);
+		assert(s1.a.length == s2.a.length);
+		assert(s1.a.length == 0);
+	}
+}
+// ----
+// Warning 6328: (184-204): Assertion violation happens here
+// Warning 6328: (208-242): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_delete_storage.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	S s1;
+	function g(S memory s2) public {
+		s1.x = s2.x;
+		s1.a = s2.a;
+	}
+	function f(S memory s2) public {
+		delete s1;
+		assert(s1.x == s2.x);
+		assert(s1.a.length == s2.a.length);
+		assert(s1.a.length == 0);
+	}
+}
+// ----
+// Warning 6328: (240-260): Assertion violation happens here
+// Warning 6328: (264-298): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_mapping.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		mapping (uint => uint) m;
+	}
+	S s1;
+	S s2;
+	function f() public view {
+		assert(s1.m[0] == s2.m[0]);
+	}
+	function g(uint a, uint b) public {
+		s1.m[a] = b;
+	}
+}
+// ----
+// Warning 4661: (143-169): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_1.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f() public view {
+		assert(s1.x == s2.x);
+		assert(s1.a.length == s2.a.length);
+	}
+}
+// ----
+// Warning 6328: (124-144): Assertion violation happens here
+// Warning 6328: (148-182): Assertion violation happens here
+// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (131-135): Assertion checker does not yet support this expression.
+// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (139-143): Assertion checker does not yet support this expression.
+// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (155-159): Assertion checker does not yet support this expression.
+// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (170-174): Assertion checker does not yet support this expression.
+// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_2.sol

@@ -0,0 +1,69 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f() public view {
+		assert(s1.x == s2.x);
+		assert(s1.a.length == s2.a.length);
+		assert(s1.a[0].x == s2.a[0].x);
+	}
+	function g() public {
+		s1.x = 42;
+		s2.x = 42;
+		s1.a.push();
+		s2.a.push();
+		s1.a[0].x = 43;
+		s2.a[0].x = 43;
+	}
+}
+// ----
+// Warning 6328: (124-144): Assertion violation happens here
+// Warning 6328: (148-182): Assertion violation happens here
+// Warning 6328: (186-216): Assertion violation happens here
+// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (131-135): Assertion checker does not yet support this expression.
+// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (139-143): Assertion checker does not yet support this expression.
+// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (155-159): Assertion checker does not yet support this expression.
+// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (170-174): Assertion checker does not yet support this expression.
+// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (193-202): Assertion checker does not yet support this expression.
+// Warning 7650: (193-197): Assertion checker does not yet support this expression.
+// Warning 8364: (193-195): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (193-200): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (206-215): Assertion checker does not yet support this expression.
+// Warning 7650: (206-210): Assertion checker does not yet support this expression.
+// Warning 8364: (206-208): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (206-213): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (246-250): Assertion checker does not yet support this expression.
+// Warning 8364: (246-248): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (246-250): Assertion checker does not support recursive structs.
+// Warning 7650: (259-263): Assertion checker does not yet support this expression.
+// Warning 8364: (259-261): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (259-263): Assertion checker does not support recursive structs.
+// Warning 7650: (272-276): Assertion checker does not yet support this expression.
+// Warning 8364: (272-274): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (272-283): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (272-276): Assertion checker does not support recursive structs.
+// Warning 7650: (287-291): Assertion checker does not yet support this expression.
+// Warning 8364: (287-289): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (287-298): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (287-291): Assertion checker does not support recursive structs.
+// Warning 7650: (302-311): Assertion checker does not yet support this expression.
+// Warning 7650: (302-306): Assertion checker does not yet support this expression.
+// Warning 8364: (302-304): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (302-309): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (302-311): Assertion checker does not support recursive structs.
+// Warning 7650: (320-329): Assertion checker does not yet support this expression.
+// Warning 7650: (320-324): Assertion checker does not yet support this expression.
+// Warning 8364: (320-322): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (320-327): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (320-329): Assertion checker does not support recursive structs.

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol

@@ -0,0 +1,123 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f() public view {
+		assert(s1.x == s2.x);
+		assert(s1.a.length == s2.a.length);
+		assert(s1.a[0].x == s2.a[0].x);
+		assert(s1.a[0].a.length == s2.a[0].a.length);
+		assert(s1.a[0].a[0].x == s2.a[0].a[0].x);
+	}
+	function g() public {
+		s1.x = 42;
+		s2.x = 42;
+		s1.a.push();
+		s2.a.push();
+		s1.a[0].x = 43;
+		s2.a[0].x = 43;
+		s1.a[0].a.push();
+		s2.a[0].a.push();
+		s1.a[0].a[0].x = 44;
+		s2.a[0].a[0].x = 44;
+	}
+}
+// ----
+// Warning 6328: (124-144): Assertion violation happens here
+// Warning 6328: (148-182): Assertion violation happens here
+// Warning 6328: (186-216): Assertion violation happens here
+// Warning 6328: (220-264): Assertion violation happens here
+// Warning 6328: (268-308): Assertion violation happens here
+// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (131-135): Assertion checker does not yet support this expression.
+// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (139-143): Assertion checker does not yet support this expression.
+// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (155-159): Assertion checker does not yet support this expression.
+// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (170-174): Assertion checker does not yet support this expression.
+// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (193-202): Assertion checker does not yet support this expression.
+// Warning 7650: (193-197): Assertion checker does not yet support this expression.
+// Warning 8364: (193-195): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (193-200): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (206-215): Assertion checker does not yet support this expression.
+// Warning 7650: (206-210): Assertion checker does not yet support this expression.
+// Warning 8364: (206-208): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (206-213): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (227-236): Assertion checker does not yet support this expression.
+// Warning 7650: (227-231): Assertion checker does not yet support this expression.
+// Warning 8364: (227-229): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (227-234): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (247-256): Assertion checker does not yet support this expression.
+// Warning 7650: (247-251): Assertion checker does not yet support this expression.
+// Warning 8364: (247-249): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (247-254): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (275-289): Assertion checker does not yet support this expression.
+// Warning 7650: (275-284): Assertion checker does not yet support this expression.
+// Warning 7650: (275-279): Assertion checker does not yet support this expression.
+// Warning 8364: (275-277): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (275-282): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (275-287): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (293-307): Assertion checker does not yet support this expression.
+// Warning 7650: (293-302): Assertion checker does not yet support this expression.
+// Warning 7650: (293-297): Assertion checker does not yet support this expression.
+// Warning 8364: (293-295): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (293-300): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (293-305): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (338-342): Assertion checker does not yet support this expression.
+// Warning 8364: (338-340): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (338-342): Assertion checker does not support recursive structs.
+// Warning 7650: (351-355): Assertion checker does not yet support this expression.
+// Warning 8364: (351-353): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (351-355): Assertion checker does not support recursive structs.
+// Warning 7650: (364-368): Assertion checker does not yet support this expression.
+// Warning 8364: (364-366): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (364-375): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (364-368): Assertion checker does not support recursive structs.
+// Warning 7650: (379-383): Assertion checker does not yet support this expression.
+// Warning 8364: (379-381): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (379-390): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (379-383): Assertion checker does not support recursive structs.
+// Warning 7650: (394-403): Assertion checker does not yet support this expression.
+// Warning 7650: (394-398): Assertion checker does not yet support this expression.
+// Warning 8364: (394-396): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (394-401): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (394-403): Assertion checker does not support recursive structs.
+// Warning 7650: (412-421): Assertion checker does not yet support this expression.
+// Warning 7650: (412-416): Assertion checker does not yet support this expression.
+// Warning 8364: (412-414): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (412-419): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (412-421): Assertion checker does not support recursive structs.
+// Warning 7650: (430-439): Assertion checker does not yet support this expression.
+// Warning 7650: (430-434): Assertion checker does not yet support this expression.
+// Warning 8364: (430-432): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (430-437): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (430-446): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (430-439): Assertion checker does not support recursive structs.
+// Warning 7650: (450-459): Assertion checker does not yet support this expression.
+// Warning 7650: (450-454): Assertion checker does not yet support this expression.
+// Warning 8364: (450-452): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (450-457): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (450-466): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (450-459): Assertion checker does not support recursive structs.
+// Warning 7650: (470-484): Assertion checker does not yet support this expression.
+// Warning 7650: (470-479): Assertion checker does not yet support this expression.
+// Warning 7650: (470-474): Assertion checker does not yet support this expression.
+// Warning 8364: (470-472): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (470-477): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (470-482): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (470-484): Assertion checker does not support recursive structs.
+// Warning 7650: (493-507): Assertion checker does not yet support this expression.
+// Warning 7650: (493-502): Assertion checker does not yet support this expression.
+// Warning 7650: (493-497): Assertion checker does not yet support this expression.
+// Warning 8364: (493-495): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (493-500): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (493-505): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (493-507): Assertion checker does not support recursive structs.

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol

@@ -0,0 +1,56 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f(bool b1, bool b2) public {
+		S storage s3 = b1 ? s1 : s2;
+		S storage s4 = b2 ? s1 : s2;
+		assert(s3.x == s1.x || s3.x == s2.x);
+		assert(s4.x == s1.x || s4.x == s2.x);
+		s3.x = 44;
+		// Fails as false positive because of lack of support to aliasing.
+		assert(s1.x == 44 || s2.x == 44);
+	}
+}
+// ----
+// Warning 6328: (197-233): Assertion violation happens here
+// Warning 6328: (237-273): Assertion violation happens here
+// Warning 6328: (359-391): Assertion violation happens here
+// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (135-147): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (166-178): Assertion checker does not yet support the type of this variable.
+// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (160-162): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (150-162): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 8364: (186-188): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (191-193): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (181-193): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 7650: (204-208): Assertion checker does not yet support this expression.
+// Warning 8364: (204-206): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 7650: (212-216): Assertion checker does not yet support this expression.
+// Warning 8364: (212-214): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (220-224): Assertion checker does not yet support this expression.
+// Warning 8364: (220-222): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 7650: (228-232): Assertion checker does not yet support this expression.
+// Warning 8364: (228-230): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (244-248): Assertion checker does not yet support this expression.
+// Warning 8364: (244-246): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 7650: (252-256): Assertion checker does not yet support this expression.
+// Warning 8364: (252-254): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (260-264): Assertion checker does not yet support this expression.
+// Warning 8364: (260-262): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 7650: (268-272): Assertion checker does not yet support this expression.
+// Warning 8364: (268-270): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (277-281): Assertion checker does not yet support this expression.
+// Warning 8364: (277-279): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 4375: (277-281): Assertion checker does not support recursive structs.
+// Warning 7650: (366-370): Assertion checker does not yet support this expression.
+// Warning 8364: (366-368): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (380-384): Assertion checker does not yet support this expression.
+// Warning 8364: (380-382): Assertion checker does not yet implement type struct C.S storage ref

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_5.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		S[] a;
+	}
+	S[] sa;
+	S[][] sa2;
+	function f() public {
+		sa.push();
+		sa2.push();
+		sa2[0].push();
+		sa2[0][0].a.push();
+		assert(sa2[0][0].a.length == sa[0].a.length);
+	}
+}
+// ----
+// Warning 6328: (192-236): Assertion violation happens here
+// Warning 8364: (126-135): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (153-166): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (170-181): Assertion checker does not yet support this expression.
+// Warning 8364: (170-179): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (170-188): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (170-181): Assertion checker does not support recursive structs.
+// Warning 7650: (199-210): Assertion checker does not yet support this expression.
+// Warning 8364: (199-208): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (221-228): Assertion checker does not yet support this expression.
+// Warning 8364: (221-226): Assertion checker does not yet implement type struct C.S storage ref

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol

@@ -0,0 +1,66 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f() public {
+		s1.x = 10;
+		++s1.x;
+		s1.x++;
+		s2.x = 20;
+		--s2.x;
+		s2.x--;
+		assert(s1.x == s2.x + 6);
+		assert(s1.a.length == s2.a.length);
+		delete s1;
+		assert(s1.x == 0);
+	}
+}
+// ----
+// Warning 4984: (200-208): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 6328: (185-209): Assertion violation happens here
+// Warning 6328: (213-247): Assertion violation happens here
+// Warning 6328: (264-281): Assertion violation happens here
+// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (119-123): Assertion checker does not yet support this expression.
+// Warning 8364: (119-121): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (119-123): Assertion checker does not support recursive structs.
+// Warning 7650: (134-138): Assertion checker does not yet support this expression.
+// Warning 8364: (134-136): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (134-138): Assertion checker does not support recursive structs.
+// Warning 7650: (142-146): Assertion checker does not yet support this expression.
+// Warning 8364: (142-144): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (142-146): Assertion checker does not support recursive structs.
+// Warning 7650: (152-156): Assertion checker does not yet support this expression.
+// Warning 8364: (152-154): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (152-156): Assertion checker does not support recursive structs.
+// Warning 7650: (167-171): Assertion checker does not yet support this expression.
+// Warning 8364: (167-169): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (167-171): Assertion checker does not support recursive structs.
+// Warning 7650: (175-179): Assertion checker does not yet support this expression.
+// Warning 8364: (175-177): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (175-179): Assertion checker does not support recursive structs.
+// Warning 7650: (192-196): Assertion checker does not yet support this expression.
+// Warning 8364: (192-194): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (200-204): Assertion checker does not yet support this expression.
+// Warning 8364: (200-202): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (220-224): Assertion checker does not yet support this expression.
+// Warning 8364: (220-222): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (235-239): Assertion checker does not yet support this expression.
+// Warning 8364: (235-237): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (258-260): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (271-275): Assertion checker does not yet support this expression.
+// Warning 8364: (271-273): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4144: (132-138): Underflow (resulting value less than 0) happens here
+// Warning 2661: (132-138): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4144: (142-148): Underflow (resulting value less than 0) happens here
+// Warning 2661: (142-148): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4144: (165-171): Underflow (resulting value less than 0) happens here
+// Warning 2661: (165-171): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4144: (175-181): Underflow (resulting value less than 0) happens here
+// Warning 2661: (175-181): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_1.sol

@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		T[] a;
+	}
+	struct T {
+		uint y;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f() public view {
+		assert(s1.x == s2.x);
+		assert(s1.a.length == s2.a.length);
+	}
+}
+// ----
+// Warning 6328: (158-178): Assertion violation happens here
+// Warning 6328: (182-216): Assertion violation happens here
+// Warning 8115: (115-119): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (122-126): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (165-169): Assertion checker does not yet support this expression.
+// Warning 8364: (165-167): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (173-177): Assertion checker does not yet support this expression.
+// Warning 8364: (173-175): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (189-193): Assertion checker does not yet support this expression.
+// Warning 8364: (189-191): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (204-208): Assertion checker does not yet support this expression.
+// Warning 8364: (204-206): Assertion checker does not yet implement type struct C.S storage ref

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_2.sol

@@ -0,0 +1,57 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		T[] a;
+	}
+	struct T {
+		uint y;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f() public {
+		s1.a.push();
+		s2.a.push();
+		s1.a[0].a.push();
+		s2.a[0].a.push();
+		assert(s1.a[0].a[0].x == s2.a[0].a[0].x);
+	}
+}
+// ----
+// Warning 6328: (223-263): Assertion violation happens here
+// Warning 8115: (115-119): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (122-126): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (153-157): Assertion checker does not yet support this expression.
+// Warning 8364: (153-155): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (153-164): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 4375: (153-157): Assertion checker does not support recursive structs.
+// Warning 7650: (168-172): Assertion checker does not yet support this expression.
+// Warning 8364: (168-170): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (168-179): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 4375: (168-172): Assertion checker does not support recursive structs.
+// Warning 7650: (183-192): Assertion checker does not yet support this expression.
+// Warning 7650: (183-187): Assertion checker does not yet support this expression.
+// Warning 8364: (183-185): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (183-190): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 8364: (183-199): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (183-192): Assertion checker does not support recursive structs.
+// Warning 7650: (203-212): Assertion checker does not yet support this expression.
+// Warning 7650: (203-207): Assertion checker does not yet support this expression.
+// Warning 8364: (203-205): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (203-210): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 8364: (203-219): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (203-212): Assertion checker does not support recursive structs.
+// Warning 7650: (230-244): Assertion checker does not yet support this expression.
+// Warning 7650: (230-239): Assertion checker does not yet support this expression.
+// Warning 7650: (230-234): Assertion checker does not yet support this expression.
+// Warning 8364: (230-232): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (230-237): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 8364: (230-242): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (248-262): Assertion checker does not yet support this expression.
+// Warning 7650: (248-257): Assertion checker does not yet support this expression.
+// Warning 7650: (248-252): Assertion checker does not yet support this expression.
+// Warning 8364: (248-250): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (248-255): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 8364: (248-260): Assertion checker does not yet implement type struct C.S storage ref

test/libsolidity/smtCheckerTests/types/struct/struct_return.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	function s() internal pure returns (S memory s1) {
+		s1.x = 42;
+		s1.a[2] = 43;
+	}
+	function f() public pure {
+		S memory s2 = s();
+		assert(s2.x == 42);
+		assert(s2.a[2] == 43);
+		assert(s2.a[3] == 43);
+	}
+}
+// ----
+// Warning 6328: (265-286): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_state_var.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	S s;
+	function f(uint _x) public {
+		s.x = _x;
+		s.a[0] = _x;
+		assert(s.a[1] == s.a[0]);
+	}
+}
+// ----
+// Warning 6328: (148-172): Assertion violation happens here.