Merge pull request #9967 from ethereum/develop

Merge develop into breaking.

libsolidity/CMakeLists.txt

@@ -94,6 +94,8 @@ set(sources
 	codegen/ir/IRLValue.h
 	codegen/ir/IRVariable.cpp
 	codegen/ir/IRVariable.h
+	formal/ArraySlicePredicate.cpp
+	formal/ArraySlicePredicate.h
 	formal/BMC.cpp
 	formal/BMC.h
 	formal/CHC.cpp

libsolidity/analysis/TypeChecker.cpp

@@ -2684,10 +2684,20 @@ bool TypeChecker::visit(MemberAccess const& _memberAccess)
 				"Using \"." + memberName + "(...)\" is deprecated. Use \"{" + memberName + ": ...}\" instead."
 			);
 
+		if (
+			funType->kind() == FunctionType::Kind::ArrayPush &&
+			arguments.value().numArguments() != 0 &&
+			exprType->containsNestedMapping()
+		)
+			m_errorReporter.typeError(
+				8871_error,
+				_memberAccess.location(),
+				"Storage arrays with nested mappings do not support .push(<arg>)."
+			);
+
 		if (!funType->bound())
 			if (auto contractType = dynamic_cast<ContractType const*>(exprType))
 				requiredLookup = contractType->isSuper() ? VirtualLookup::Super : VirtualLookup::Virtual;
-
 	}
 
 	annotation.requiredLookup = requiredLookup;

libsolidity/ast/ASTJsonConverter.cpp

@@ -23,6 +23,7 @@
 #include <libsolidity/ast/ASTJsonConverter.h>
 
 #include <libsolidity/ast/AST.h>
+#include <libsolidity/ast/TypeProvider.h>
 
 #include <libyul/AsmJsonConverter.h>
 #include <libyul/AsmData.h>
@@ -69,8 +70,9 @@ void addIfSet(std::vector<pair<string, Json::Value>>& _attributes, string const&
 namespace solidity::frontend
 {
 
-ASTJsonConverter::ASTJsonConverter(bool _legacy, map<string, unsigned> _sourceIndices):
+ASTJsonConverter::ASTJsonConverter(bool _legacy, CompilerStack::State _stackState, map<string, unsigned> _sourceIndices):
 	m_legacy(_legacy),
+	m_stackState(_stackState),
 	m_sourceIndices(std::move(_sourceIndices))
 {
 }
@@ -204,7 +206,6 @@ void ASTJsonConverter::appendExpressionAttributes(
 {
 	std::vector<pair<string, Json::Value>> exprAttributes = {
 		make_pair("typeDescriptions", typePointerToJson(_annotation.type)),
-		make_pair("lValueRequested", _annotation.willBeWrittenTo),
 		make_pair("argumentTypes", typePointerToJson(_annotation.arguments))
 	};
 
@@ -212,6 +213,9 @@ void ASTJsonConverter::appendExpressionAttributes(
 	addIfSet(exprAttributes, "isPure", _annotation.isPure);
 	addIfSet(exprAttributes, "isConstant", _annotation.isConstant);
 
+	if (m_stackState > CompilerStack::State::ParsedAndImported)
+		exprAttributes.emplace_back("lValueRequested", _annotation.willBeWrittenTo);
+
 	_attributes += exprAttributes;
 }
 
@@ -260,6 +264,7 @@ bool ASTJsonConverter::visit(SourceUnit const& _node)
 	addIfSet(attributes, "absolutePath", _node.annotation().path);
 
 	setJsonNode(_node, "SourceUnit", std::move(attributes));
+
 	return false;
 }
 
@@ -268,7 +273,7 @@ bool ASTJsonConverter::visit(PragmaDirective const& _node)
 	Json::Value literals(Json::arrayValue);
 	for (auto const& literal: _node.literals())
 		literals.append(literal);
-	setJsonNode( _node, "PragmaDirective", {
+	setJsonNode(_node, "PragmaDirective", {
 		make_pair("literals", std::move(literals))
 	});
 	return false;
@@ -278,7 +283,7 @@ bool ASTJsonConverter::visit(ImportDirective const& _node)
 {
 	std::vector<pair<string, Json::Value>> attributes = {
 		make_pair("file", _node.path()),
-		make_pair(m_legacy ? "SourceUnit" : "sourceUnit", nodeId(*_node.annotation().sourceUnit)),
+		make_pair(m_legacy ? "SourceUnit" : "sourceUnit", idOrNull(_node.annotation().sourceUnit)),
 		make_pair("scope", idOrNull(_node.scope()))
 	};
 
@@ -395,18 +400,11 @@ bool ASTJsonConverter::visit(OverrideSpecifier const& _node)
 
 bool ASTJsonConverter::visit(FunctionDefinition const& _node)
 {
-	Visibility visibility;
-	if (_node.isConstructor())
-		visibility = _node.annotation().contract->abstract() ? Visibility::Internal : Visibility::Public;
-	else
-		visibility = _node.visibility();
-
 	std::vector<pair<string, Json::Value>> attributes = {
 		make_pair("name", _node.name()),
 		make_pair("documentation", _node.documentation() ? toJson(*_node.documentation()) : Json::nullValue),
 		make_pair("kind", _node.isFree() ? "freeFunction" : TokenTraits::toString(_node.kind())),
 		make_pair("stateMutability", stateMutabilityToString(_node.stateMutability())),
-		make_pair("visibility", Declaration::visibilityToString(visibility)),
 		make_pair("virtual", _node.markedVirtual()),
 		make_pair("overrides", _node.overrides() ? toJson(*_node.overrides()) : Json::nullValue),
 		make_pair("parameters", toJson(_node.parameterList())),
@@ -417,7 +415,19 @@ bool ASTJsonConverter::visit(FunctionDefinition const& _node)
 		make_pair("scope", idOrNull(_node.scope()))
 	};
 
-	if (_node.isPartOfExternalInterface())
+	optional<Visibility> visibility;
+	if (_node.isConstructor())
+	{
+		if (_node.annotation().contract)
+			visibility = _node.annotation().contract->abstract() ? Visibility::Internal : Visibility::Public;
+	}
+	else
+		visibility = _node.visibility();
+
+	if (visibility)
+		attributes.emplace_back("visibility", Declaration::visibilityToString(*visibility));
+
+	if (_node.isPartOfExternalInterface() && m_stackState > CompilerStack::State::ParsedAndImported)
 		attributes.emplace_back("functionSelector", _node.externalIdentifierHex());
 	if (!_node.annotation().baseFunctions.empty())
 		attributes.emplace_back(make_pair("baseFunctions", getContainerIds(_node.annotation().baseFunctions, true)));
@@ -718,7 +728,7 @@ bool ASTJsonConverter::visit(Assignment const& _node)
 		make_pair("rightHandSide", toJson(_node.rightHandSide()))
 	};
 	appendExpressionAttributes(attributes, _node.annotation());
-	setJsonNode( _node, "Assignment", std::move(attributes));
+	setJsonNode(_node, "Assignment", std::move(attributes));
 	return false;
 }
 
@@ -770,15 +780,19 @@ bool ASTJsonConverter::visit(FunctionCall const& _node)
 		make_pair("tryCall", _node.annotation().tryCall)
 	};
 
-	FunctionCallKind nodeKind = *_node.annotation().kind;
-
-	if (m_legacy)
+	if (_node.annotation().kind.set())
 	{
-		attributes.emplace_back("isStructConstructorCall", nodeKind == FunctionCallKind::StructConstructorCall);
-		attributes.emplace_back("type_conversion", nodeKind == FunctionCallKind::TypeConversion);
+		FunctionCallKind nodeKind = *_node.annotation().kind;
+
+		if (m_legacy)
+		{
+			attributes.emplace_back("isStructConstructorCall", nodeKind == FunctionCallKind::StructConstructorCall);
+			attributes.emplace_back("type_conversion", nodeKind == FunctionCallKind::TypeConversion);
+		}
+		else
+			attributes.emplace_back("kind", functionCallKind(nodeKind));
 	}
-	else
-		attributes.emplace_back("kind", functionCallKind(nodeKind));
+
 	appendExpressionAttributes(attributes, _node.annotation());
 	setJsonNode(_node, "FunctionCall", std::move(attributes));
 	return false;

libsolidity/ast/ASTJsonConverter.h

@@ -25,6 +25,7 @@
 
 #include <libsolidity/ast/ASTAnnotations.h>
 #include <libsolidity/ast/ASTVisitor.h>
+#include <libsolidity/interface/CompilerStack.h>
 #include <liblangutil/Exceptions.h>
 
 #include <json/json.h>
@@ -51,9 +52,11 @@ class ASTJsonConverter: public ASTConstVisitor
 public:
 	/// Create a converter to JSON for the given abstract syntax tree.
 	/// @a _legacy if true, use legacy format
+	/// @a _stackState state of the compiler stack to avoid outputting incomplete data
 	/// @a _sourceIndices is used to abbreviate source names in source locations.
 	explicit ASTJsonConverter(
 		bool _legacy,
+		CompilerStack::State _stackState,
 		std::map<std::string, unsigned> _sourceIndices = std::map<std::string, unsigned>()
 	);
 	/// Output the json representation of the AST to _stream.
@@ -189,6 +192,7 @@ private:
 	}
 
 	bool m_legacy = false; ///< if true, use legacy format
+	CompilerStack::State m_stackState = CompilerStack::State::Empty; ///< Used to only access information that already exists
 	bool m_inEvent = false; ///< whether we are currently inside an event or not
 	Json::Value m_currentValue;
 	std::map<std::string, unsigned> m_sourceIndices;

libsolidity/ast/Types.cpp

@@ -140,7 +140,9 @@ util::Result<TypePointers> transformParametersToExternal(TypePointers const& _pa
 
 	for (auto const& type: _parameters)
 	{
-		if (TypePointer ext = type->interfaceType(_inLibrary).get())
+		if (!type)
+			return util::Result<TypePointers>::err("Type information not present.");
+		else if (TypePointer ext = type->interfaceType(_inLibrary).get())
 			transformed.push_back(ext);
 		else
 			return util::Result<TypePointers>::err("Parameter should have external type.");

libsolidity/codegen/ExpressionCompiler.cpp

@@ -867,11 +867,26 @@ bool ExpressionCompiler::visit(FunctionCall const& _functionCall)
 					else
 					{
 						solAssert(paramTypes[arg - 1]->isValueType(), "");
-						utils().convertType(
-							*arguments[arg - 1]->annotation().type,
-							*paramTypes[arg - 1],
-							true
-						);
+						if (auto functionType =	dynamic_cast<FunctionType const*>(paramTypes[arg - 1]))
+						{
+							auto argumentType =
+								dynamic_cast<FunctionType const*>(arguments[arg-1]->annotation().type);
+							solAssert(
+								argumentType &&
+								functionType->kind() == FunctionType::Kind::External &&
+								argumentType->kind() == FunctionType::Kind::External &&
+								!argumentType->bound(),
+								""
+							);
+
+							utils().combineExternalFunctionType(true);
+						}
+						else
+							utils().convertType(
+								*arguments[arg - 1]->annotation().type,
+								*paramTypes[arg - 1],
+								true
+							);
 					}
 				}
 			if (!event.isAnonymous())

libsolidity/codegen/LValue.cpp

@@ -291,7 +291,7 @@ void StorageItem::storeValue(Type const& _sourceType, SourceLocation const& _loc
 			// stack: value storage_ref multiplier
 			// fetch old value
 			m_context << Instruction::DUP2 << Instruction::SLOAD;
-			// stack: value storege_ref multiplier old_full_value
+			// stack: value storage_ref multiplier old_full_value
 			// clear bytes in old value
 			m_context
 				<< Instruction::DUP2 << ((u256(1) << (8 * m_dataType->storageBytes())) - 1)
@@ -461,7 +461,7 @@ void StorageItem::setToZero(SourceLocation const&, bool _removeReference) const
 			// stack: storage_ref multiplier
 			// fetch old value
 			m_context << Instruction::DUP2 << Instruction::SLOAD;
-			// stack: storege_ref multiplier old_full_value
+			// stack: storage_ref multiplier old_full_value
 			// clear bytes in old value
 			m_context
 				<< Instruction::SWAP1 << ((u256(1) << (8 * m_dataType->storageBytes())) - 1)

libsolidity/codegen/YulUtilFunctions.cpp

@@ -873,6 +873,12 @@ std::string YulUtilFunctions::resizeDynamicArrayFunction(ArrayType const& _type)
 					let arrayDataStart := <dataPosition>(array)
 					let deleteStart := add(arrayDataStart, newSlotCount)
 					let deleteEnd := add(arrayDataStart, oldSlotCount)
+					<?packed>
+						// if we are dealing with packed array and offset is greater than zero
+						// we have  to partially clear last slot that is still used, so decreasing start by one
+						let offset := mul(mod(newLen, <itemsPerSlot>), <storageBytes>)
+						if gt(offset, 0) { <partialClearStorageSlot>(sub(deleteStart, 1), offset) }
+					</packed>
 					<clearStorageRange>(deleteStart, deleteEnd)
 				}
 			})")
@@ -883,6 +889,10 @@ std::string YulUtilFunctions::resizeDynamicArrayFunction(ArrayType const& _type)
 			("dataPosition", arrayDataAreaFunction(_type))
 			("clearStorageRange", clearStorageRangeFunction(*_type.baseType()))
 			("maxArrayLength", (u256(1) << 64).str())
+			("packed", _type.baseType()->storageBytes() <= 16)
+			("itemsPerSlot", to_string(32 / _type.baseType()->storageBytes()))
+			("storageBytes", to_string(_type.baseType()->storageBytes()))
+			("partialClearStorageSlot", partialClearStorageSlotFunction())
 			.render();
 	});
 }
@@ -1037,8 +1047,6 @@ string YulUtilFunctions::storageArrayPushZeroFunction(ArrayType const& _type)
 	solUnimplementedAssert(!_type.isByteArray(), "Byte Arrays not yet implemented!");
 	solUnimplementedAssert(_type.baseType()->storageBytes() <= 32, "Base type is not yet implemented.");
 
-	solAssert(_type.baseType()->isValueType(), "");
-
 	string functionName = "array_push_zero_" + _type.identifier();
 	return m_functionCollector.createFunction(functionName, [&]() {
 		return Whiskers(R"(
@@ -1047,24 +1055,39 @@ string YulUtilFunctions::storageArrayPushZeroFunction(ArrayType const& _type)
 				if iszero(lt(oldLen, <maxArrayLength>)) { <panic>() }
 				sstore(array, add(oldLen, 1))
 				slot, offset := <indexAccess>(array, oldLen)
-				<storeValue>(slot, offset, <zeroValueFunction>())
 			})")
 			("functionName", functionName)
 			("panic", panicFunction())
 			("fetchLength", arrayLengthFunction(_type))
 			("indexAccess", storageArrayIndexAccessFunction(_type))
-			("storeValue", updateStorageValueFunction(*_type.baseType(), *_type.baseType()))
 			("maxArrayLength", (u256(1) << 64).str())
-			("zeroValueFunction", zeroValueFunction(*_type.baseType()))
 			.render();
 	});
 }
 
+string YulUtilFunctions::partialClearStorageSlotFunction()
+{
+	string functionName = "partial_clear_storage_slot";
+	return m_functionCollector.createFunction(functionName, [&]() {
+		return Whiskers(R"(
+		function <functionName>(slot, offset) {
+			let mask := <shr>(mul(8, sub(32, offset)), <ones>)
+			sstore(slot, and(mask, sload(slot)))
+		}
+		)")
+		("functionName", functionName)
+		("ones", formatNumber((bigint(1) << 256) - 1))
+		("shr", shiftRightFunctionDynamic())
+		.render();
+	});
+}
+
 string YulUtilFunctions::clearStorageRangeFunction(Type const& _type)
 {
-	string functionName = "clear_storage_range_" + _type.identifier();
+	if (_type.storageBytes() < 32)
+		solAssert(_type.isValueType(), "");
 
-	solAssert(_type.storageBytes() >= 32, "Expected smaller value for storage bytes");
+	string functionName = "clear_storage_range_" + _type.identifier();
 
 	return m_functionCollector.createFunction(functionName, [&]() {
 		return Whiskers(R"(
@@ -1076,7 +1099,7 @@ string YulUtilFunctions::clearStorageRangeFunction(Type const& _type)
 			}
 		)")
 		("functionName", functionName)
-		("setToZero", storageSetToZeroFunction(_type))
+		("setToZero", storageSetToZeroFunction(_type.storageBytes() < 32 ? *TypeProvider::uint256() : _type))
 		("increment", _type.storageSize().str())
 		.render();
 	});

libsolidity/codegen/YulUtilFunctions.h

@@ -422,6 +422,11 @@ private:
 	/// @returns a function that reads a reference type from storage to memory (performing a deep copy).
 	std::string readFromStorageReferenceType(Type const& _type);
 
+	/// @returns the name of a function that will clear given storage slot
+	/// starting with given offset until the end of the slot
+	/// signature: (slot, offset)
+	std::string partialClearStorageSlotFunction();
+
 	langutil::EVMVersion m_evmVersion;
 	RevertStrings m_revertStrings;
 	MultiUseYulFunctionCollector& m_functionCollector;

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -929,6 +929,20 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall)
 						"(" <<
 						IRVariable(arg).commaSeparatedList() <<
 						")";
+				else if (auto functionType = dynamic_cast<FunctionType const*>(paramTypes[i]))
+				{
+					solAssert(
+						IRVariable(arg).type() == *functionType &&
+						functionType->kind() == FunctionType::Kind::External &&
+						!functionType->bound(),
+						""
+					);
+					define(indexedArgs.emplace_back(m_context.newYulVariable(), *TypeProvider::fixedBytes(32))) <<
+						m_utils.combineExternalFunctionIdFunction() <<
+						"(" <<
+						IRVariable(arg).commaSeparatedList() <<
+						")\n";
+				}
 				else
 					indexedArgs.emplace_back(convert(arg, *paramTypes[i]));
 			}

libsolidity/formal/ArraySlicePredicate.cpp

@@ -0,0 +1,91 @@
+/*
+	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/ArraySlicePredicate.h>
+
+#include <liblangutil/Exceptions.h>
+
+using namespace std;
+using namespace solidity;
+using namespace solidity::smtutil;
+using namespace solidity::frontend;
+using namespace solidity::frontend::smt;
+
+map<string, ArraySlicePredicate::SliceData> ArraySlicePredicate::m_slicePredicates;
+
+pair<bool, ArraySlicePredicate::SliceData const&> ArraySlicePredicate::create(SortPointer _sort, EncodingContext& _context)
+{
+	solAssert(_sort->kind == Kind::Tuple, "");
+	auto tupleSort = dynamic_pointer_cast<TupleSort>(_sort);
+	solAssert(tupleSort, "");
+
+	auto tupleName = tupleSort->name;
+	if (m_slicePredicates.count(tupleName))
+		return {true, m_slicePredicates.at(tupleName)};
+
+	auto sort = tupleSort->components.at(0);
+	solAssert(sort->kind == Kind::Array, "");
+
+	smt::SymbolicArrayVariable aVar{sort, "a_" + tupleName, _context };
+	smt::SymbolicArrayVariable bVar{sort, "b_" + tupleName, _context};
+	smt::SymbolicIntVariable startVar{TypeProvider::uint256(), TypeProvider::uint256(), "start_" + tupleName, _context};
+	smt::SymbolicIntVariable endVar{TypeProvider::uint256(), TypeProvider::uint256(), "end_" + tupleName, _context };
+	smt::SymbolicIntVariable iVar{TypeProvider::uint256(), TypeProvider::uint256(), "i_" + tupleName, _context};
+
+	vector<SortPointer> domain{sort, sort, startVar.sort(), endVar.sort()};
+	auto sliceSort = make_shared<FunctionSort>(domain, SortProvider::boolSort);
+	Predicate const& slice = *Predicate::create(sliceSort, "array_slice_" + tupleName, PredicateType::Custom, _context);
+
+	domain.emplace_back(iVar.sort());
+	auto predSort = make_shared<FunctionSort>(domain, SortProvider::boolSort);
+	Predicate const& header = *Predicate::create(predSort, "array_slice_header_" + tupleName, PredicateType::Custom, _context);
+	Predicate const& loop = *Predicate::create(predSort, "array_slice_loop_" + tupleName, PredicateType::Custom, _context);
+
+	auto a = aVar.elements();
+	auto b = bVar.elements();
+	auto start = startVar.currentValue();
+	auto end = endVar.currentValue();
+	auto i = iVar.currentValue();
+
+	auto rule1 = smtutil::Expression::implies(
+		end > start,
+		header({a, b, start, end, 0})
+	);
+
+	auto rule2 = smtutil::Expression::implies(
+		header({a, b, start, end, i}) && i >= (end - start),
+		slice({a, b, start, end})
+	);
+
+	auto rule3 = smtutil::Expression::implies(
+		header({a, b, start, end, i}) && i >= 0 && i < (end - start),
+		loop({a, b, start, end, i})
+	);
+
+	auto b_i = smtutil::Expression::select(b, i);
+	auto a_start_i = smtutil::Expression::select(a, start + i);
+	auto rule4 = smtutil::Expression::implies(
+		loop({a, b, start, end, i}) && b_i == a_start_i,
+		header({a, b, start, end, i + 1})
+	);
+
+	return {false, m_slicePredicates[tupleName] = {
+		{&slice, &header, &loop},
+		{move(rule1), move(rule2), move(rule3), move(rule4)}
+	}};
+}

libsolidity/formal/ArraySlicePredicate.h

@@ -0,0 +1,62 @@
+/*
+	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/EncodingContext.h>
+#include <libsolidity/formal/Predicate.h>
+#include <libsolidity/formal/SymbolicVariables.h>
+
+#include <libsmtutil/Sorts.h>
+
+#include <vector>
+
+namespace solidity::frontend
+{
+
+/**
+ * Contains the set of rules to compute an array slice.
+ * Rules:
+ * 1. end > start => ArraySliceHeader(a, b, start, end, 0)
+ * 2. ArraySliceHeader(a, b, start, end, i) && i >= (end - start) => ArraySlice(a, b, start, end)
+ * 3. ArraySliceHeader(a, b, start, end, i) && i >= 0 && i < (end - start) => ArraySliceLoop(a, b, start, end, i)
+ * 4. ArraySliceLoop(a, b, start, end, i) && b[i] = a[start + i] => ArraySliceHeader(a, b, start, end, i + 1)
+ *
+ * The rule to be used by CHC is ArraySlice(a, b, start, end).
+ */
+
+struct ArraySlicePredicate
+{
+	/// Contains the predicates and rules created to compute
+	/// array slices for a given sort.
+	struct SliceData
+	{
+		std::vector<Predicate const*> predicates;
+		std::vector<smtutil::Expression> rules;
+	};
+
+	/// @returns a flag representing whether the array slice predicates had already been created before for this sort,
+	/// and the corresponding slice data.
+	static std::pair<bool, SliceData const&> create(smtutil::SortPointer _sort, smt::EncodingContext& _context);
+
+	static void reset() { m_slicePredicates.clear(); }
+
+private:
+	/// Maps a unique sort name to its slice data.
+	static std::map<std::string, SliceData> m_slicePredicates;
+};
+
+}

libsolidity/formal/CHC.cpp

@@ -22,6 +22,7 @@
 #include <libsmtutil/Z3CHCInterface.h>
 #endif
 
+#include <libsolidity/formal/ArraySlicePredicate.h>
 #include <libsolidity/formal/PredicateInstance.h>
 #include <libsolidity/formal/PredicateSort.h>
 #include <libsolidity/formal/SymbolicTypes.h>
@@ -470,6 +471,36 @@ void CHC::endVisit(Continue const& _continue)
 	m_currentBlock = predicate(*continueGhost);
 }
 
+void CHC::endVisit(IndexRangeAccess const& _range)
+{
+	createExpr(_range);
+
+	auto baseArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(_range.baseExpression()));
+	auto sliceArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(_range));
+	solAssert(baseArray && sliceArray, "");
+
+	auto const& sliceData = ArraySlicePredicate::create(sliceArray->sort(), m_context);
+	if (!sliceData.first)
+	{
+		for (auto pred: sliceData.second.predicates)
+			m_interface->registerRelation(pred->functor());
+		for (auto const& rule: sliceData.second.rules)
+			addRule(rule, "");
+	}
+
+	auto start = _range.startExpression() ? expr(*_range.startExpression()) : 0;
+	auto end = _range.endExpression() ? expr(*_range.endExpression()) : baseArray->length();
+	auto slicePred = (*sliceData.second.predicates.at(0))({
+		baseArray->elements(),
+		sliceArray->elements(),
+		start,
+		end
+	});
+
+	m_context.addAssertion(slicePred);
+	m_context.addAssertion(sliceArray->length() == end - start);
+}
+
 void CHC::visitAssert(FunctionCall const& _funCall)
 {
 	auto const& args = _funCall.arguments();
@@ -688,6 +719,7 @@ void CHC::resetSourceAnalysis()
 	m_interfaces.clear();
 	m_nondetInterfaces.clear();
 	Predicate::reset();
+	ArraySlicePredicate::reset();
 	m_blockCounter = 0;
 
 	bool usesZ3 = false;
@@ -994,6 +1026,9 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
 	case PredicateType::NondetInterface:
 		// Nondeterministic interface predicates are handled differently.
 		solAssert(false, "");
+	case PredicateType::Custom:
+		// Custom rules are handled separately.
+		solAssert(false, "");
 	}
 	solAssert(false, "");
 }

libsolidity/formal/CHC.h

@@ -81,6 +81,7 @@ private:
 	void endVisit(FunctionCall const& _node) override;
 	void endVisit(Break const& _node) override;
 	void endVisit(Continue const& _node) override;
+	void endVisit(IndexRangeAccess const& _node) override;
 
 	void visitAssert(FunctionCall const& _funCall);
 	void visitAddMulMod(FunctionCall const& _funCall) override;

libsolidity/formal/Predicate.h

@@ -39,7 +39,8 @@ enum class PredicateType
 	FunctionEntry,
 	FunctionSummary,
 	FunctionBlock,
-	Error
+	Error,
+	Custom
 };
 
 /**

libsolidity/formal/SMTEncoder.cpp

@@ -817,43 +817,125 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
 {
 	solAssert(*_funCall.annotation().kind == FunctionCallKind::TypeConversion, "");
 	solAssert(_funCall.arguments().size() == 1, "");
+
 	auto argument = _funCall.arguments().front();
+	auto const& argType = argument->annotation().type;
+
 	unsigned argSize = argument->annotation().type->storageBytes();
 	unsigned castSize = _funCall.annotation().type->storageBytes();
-	auto const& funCallCategory = _funCall.annotation().type->category();
-	// Allow casting number literals to address.
-	// TODO: remove the isNegative() check once the type checker disallows this
-	if (
-		auto const* numberType = dynamic_cast<RationalNumberType const*>(argument->annotation().type);
-		numberType && !numberType->isNegative() && (funCallCategory == Type::Category::Address)
-	)
-		defineExpr(_funCall, numberType->literalValue(nullptr));
-	else if (argSize == castSize)
-		defineExpr(_funCall, expr(*argument));
-	else
-	{
-		m_context.setUnknownValue(*m_context.expression(_funCall));
-		// TODO: truncating and bytesX needs a different approach because of right padding.
-		if (funCallCategory == Type::Category::Integer || funCallCategory == Type::Category::Address)
-		{
-			if (argSize < castSize)
-				defineExpr(_funCall, expr(*argument));
-			else
-			{
-				auto const& intType = dynamic_cast<IntegerType const&>(*m_context.expression(_funCall)->type());
-				defineExpr(_funCall, smtutil::Expression::ite(
-					expr(*argument) >= smt::minValue(intType) && expr(*argument) <= smt::maxValue(intType),
-					expr(*argument),
-					expr(_funCall)
-				));
-			}
-		}
 
-		m_errorReporter.warning(
-			5084_error,
-			_funCall.location(),
-			"Type conversion is not yet fully supported and might yield false positives."
-		);
+	auto const& funCallType = _funCall.annotation().type;
+
+	// TODO Simplify this whole thing for 0.8.0 where weird casts are disallowed.
+
+	auto symbArg = expr(*argument, funCallType);
+	bool castIsSigned = smt::isNumber(*funCallType) && smt::isSigned(funCallType);
+	bool argIsSigned = smt::isNumber(*argType) && smt::isSigned(argType);
+	optional<smtutil::Expression> symbMin;
+	optional<smtutil::Expression> symbMax;
+	if (smt::isNumber(*funCallType))
+	{
+		symbMin = smt::minValue(funCallType);
+		symbMax = smt::maxValue(funCallType);
+	}
+	if (argSize == castSize)
+	{
+		// If sizes are the same, it's possible that the signs are different.
+		if (smt::isNumber(*funCallType))
+		{
+			solAssert(smt::isNumber(*argType), "");
+
+			// castIsSigned && !argIsSigned => might overflow if arg > castType.max
+			// !castIsSigned && argIsSigned => might underflow if arg < castType.min
+			// !castIsSigned && !argIsSigned => ok
+			// castIsSigned && argIsSigned => ok
+
+			if (castIsSigned && !argIsSigned)
+			{
+				auto wrap = smtutil::Expression::ite(
+					symbArg > *symbMax,
+					symbArg - (*symbMax - *symbMin + 1),
+					symbArg
+				);
+				defineExpr(_funCall, wrap);
+			}
+			else if (!castIsSigned && argIsSigned)
+			{
+				auto wrap = smtutil::Expression::ite(
+					symbArg < *symbMin,
+					symbArg + (*symbMax + 1),
+					symbArg
+				);
+				defineExpr(_funCall, wrap);
+			}
+			else
+				defineExpr(_funCall, symbArg);
+		}
+		else
+			defineExpr(_funCall, symbArg);
+	}
+	else if (castSize > argSize)
+	{
+		solAssert(smt::isNumber(*funCallType), "");
+		// RationalNumbers have size 32.
+		solAssert(argType->category() != Type::Category::RationalNumber, "");
+
+		// castIsSigned && !argIsSigned => ok
+		// castIsSigned && argIsSigned => ok
+		// !castIsSigned && !argIsSigned => ok except for FixedBytesType, need to adjust padding
+		// !castIsSigned && argIsSigned => might underflow if arg < castType.min
+
+		if (!castIsSigned && argIsSigned)
+		{
+			auto wrap = smtutil::Expression::ite(
+				symbArg < *symbMin,
+				symbArg + (*symbMax + 1),
+				symbArg
+			);
+			defineExpr(_funCall, wrap);
+		}
+		else if (!castIsSigned && !argIsSigned)
+		{
+			if (auto const* fixedCast = dynamic_cast<FixedBytesType const*>(funCallType))
+			{
+				auto const* fixedArg = dynamic_cast<FixedBytesType const*>(argType);
+				solAssert(fixedArg, "");
+				auto diff = fixedCast->numBytes() - fixedArg->numBytes();
+				solAssert(diff > 0, "");
+				auto bvSize = fixedCast->numBytes() * 8;
+				defineExpr(
+					_funCall,
+					smtutil::Expression::bv2int(smtutil::Expression::int2bv(symbArg, bvSize) << smtutil::Expression::int2bv(diff * 8, bvSize))
+				);
+			}
+			else
+				defineExpr(_funCall, symbArg);
+		}
+		else
+			defineExpr(_funCall, symbArg);
+	}
+	else // castSize < argSize
+	{
+		solAssert(smt::isNumber(*funCallType), "");
+
+		auto const* fixedCast = dynamic_cast<FixedBytesType const*>(funCallType);
+		auto const* fixedArg = dynamic_cast<FixedBytesType const*>(argType);
+		if (fixedCast && fixedArg)
+		{
+			createExpr(_funCall);
+			auto diff = argSize - castSize;
+			solAssert(fixedArg->numBytes() - fixedCast->numBytes() == diff, "");
+
+			auto argValueBV = smtutil::Expression::int2bv(symbArg, argSize * 8);
+			auto shr = smtutil::Expression::int2bv(diff * 8, argSize * 8);
+			solAssert(!castIsSigned, "");
+			defineExpr(_funCall, smtutil::Expression::bv2int(argValueBV >> shr));
+		}
+		else
+		{
+			auto argValueBV = smtutil::Expression::int2bv(symbArg, castSize * 8);
+			defineExpr(_funCall, smtutil::Expression::bv2int(argValueBV, castIsSigned));
+		}
 	}
 }
 
@@ -1095,11 +1177,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 void SMTEncoder::endVisit(IndexRangeAccess const& _indexRangeAccess)
 {
 	createExpr(_indexRangeAccess);
-	m_errorReporter.warning(
-		2923_error,
-		_indexRangeAccess.location(),
-		"Assertion checker does not yet implement this expression."
-	);
+	/// The actual slice is created by CHC which also assigns the length.
 }
 
 void SMTEncoder::arrayAssignment()

libsolidity/formal/SymbolicTypes.cpp

@@ -389,11 +389,47 @@ smtutil::Expression minValue(frontend::IntegerType const& _type)
 	return smtutil::Expression(_type.minValue());
 }
 
+smtutil::Expression minValue(frontend::TypePointer _type)
+{
+	solAssert(isNumber(*_type), "");
+	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
+		return intType->minValue();
+	if (auto const* fixedType = dynamic_cast<FixedPointType const*>(_type))
+		return fixedType->minIntegerValue();
+	if (
+		dynamic_cast<AddressType const*>(_type) ||
+		dynamic_cast<ContractType const*>(_type) ||
+		dynamic_cast<EnumType const*>(_type) ||
+		dynamic_cast<FixedBytesType const*>(_type)
+	)
+		return 0;
+	solAssert(false, "");
+}
+
 smtutil::Expression maxValue(frontend::IntegerType const& _type)
 {
 	return smtutil::Expression(_type.maxValue());
 }
 
+smtutil::Expression maxValue(frontend::TypePointer _type)
+{
+	solAssert(isNumber(*_type), "");
+	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
+		return intType->maxValue();
+	if (auto const* fixedType = dynamic_cast<FixedPointType const*>(_type))
+		return fixedType->maxIntegerValue();
+	if (
+		dynamic_cast<AddressType const*>(_type) ||
+		dynamic_cast<ContractType const*>(_type)
+	)
+		return TypeProvider::uint(160)->maxValue();
+	if (auto const* enumType = dynamic_cast<EnumType const*>(_type))
+		return enumType->numberOfMembers();
+	if (auto const* bytesType = dynamic_cast<FixedBytesType const*>(_type))
+		return TypeProvider::uint(bytesType->numBytes() * 8)->maxValue();
+	solAssert(false, "");
+}
+
 void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context)
 {
 	setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _context);
@@ -458,6 +494,29 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type)
 	return 0;
 }
 
+bool isSigned(TypePointer const& _type)
+{
+	solAssert(smt::isNumber(*_type), "");
+	bool isSigned = false;
+	if (auto const* numberType = dynamic_cast<RationalNumberType const*>(_type))
+		isSigned |= numberType->isNegative();
+	else if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
+		isSigned |= intType->isSigned();
+	else if (auto const* fixedType = dynamic_cast<FixedPointType const*>(_type))
+		isSigned |= fixedType->isSigned();
+	else if (
+		dynamic_cast<AddressType const*>(_type) ||
+		dynamic_cast<ContractType const*>(_type) ||
+		dynamic_cast<EnumType const*>(_type) ||
+		dynamic_cast<FixedBytesType const*>(_type)
+	)
+		return false;
+	else
+		solAssert(false, "");
+
+	return isSigned;
+}
+
 pair<unsigned, bool> typeBvSizeAndSignedness(frontend::TypePointer const& _type)
 {
 	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))

libsolidity/formal/SymbolicTypes.h

@@ -65,8 +65,11 @@ bool isNonRecursiveStruct(frontend::Type const& _type);
 std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(frontend::Type const& _type, std::string const& _uniqueName, EncodingContext& _context);
 
 smtutil::Expression minValue(frontend::IntegerType const& _type);
+smtutil::Expression minValue(frontend::TypePointer _type);
 smtutil::Expression maxValue(frontend::IntegerType const& _type);
+smtutil::Expression maxValue(frontend::TypePointer _type);
 smtutil::Expression zeroValue(frontend::TypePointer const& _type);
+bool isSigned(frontend::TypePointer const& _type);
 
 std::pair<unsigned, bool> typeBvSizeAndSignedness(frontend::TypePointer const& type);
 

libsolidity/interface/CompilerStack.cpp

@@ -124,7 +124,7 @@ std::optional<CompilerStack::Remapping> CompilerStack::parseRemapping(string con
 
 void CompilerStack::setRemappings(vector<Remapping> const& _remappings)
 {
-	if (m_stackState >= ParsingPerformed)
+	if (m_stackState >= ParsedAndImported)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set remappings before parsing."));
 	for (auto const& remapping: _remappings)
 		solAssert(!remapping.prefix.empty(), "");
@@ -133,21 +133,21 @@ void CompilerStack::setRemappings(vector<Remapping> const& _remappings)
 
 void CompilerStack::setEVMVersion(langutil::EVMVersion _version)
 {
-	if (m_stackState >= ParsingPerformed)
+	if (m_stackState >= ParsedAndImported)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set EVM version before parsing."));
 	m_evmVersion = _version;
 }
 
 void CompilerStack::setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSMTSolvers)
 {
-	if (m_stackState >= ParsingPerformed)
+	if (m_stackState >= ParsedAndImported)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled SMT solvers before parsing."));
 	m_enabledSMTSolvers = _enabledSMTSolvers;
 }
 
 void CompilerStack::setLibraries(std::map<std::string, util::h160> const& _libraries)
 {
-	if (m_stackState >= ParsingPerformed)
+	if (m_stackState >= ParsedAndImported)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set libraries before parsing."));
 	m_libraries = _libraries;
 }
@@ -161,14 +161,14 @@ void CompilerStack::setOptimiserSettings(bool _optimize, unsigned _runs)
 
 void CompilerStack::setOptimiserSettings(OptimiserSettings _settings)
 {
-	if (m_stackState >= ParsingPerformed)
+	if (m_stackState >= ParsedAndImported)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set optimiser settings before parsing."));
 	m_optimiserSettings = std::move(_settings);
 }
 
 void CompilerStack::setRevertStringBehaviour(RevertStrings _revertStrings)
 {
-	if (m_stackState >= ParsingPerformed)
+	if (m_stackState >= ParsedAndImported)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set revert string settings before parsing."));
 	solUnimplementedAssert(_revertStrings != RevertStrings::VerboseDebug, "");
 	m_revertStrings = _revertStrings;
@@ -176,21 +176,21 @@ void CompilerStack::setRevertStringBehaviour(RevertStrings _revertStrings)
 
 void CompilerStack::useMetadataLiteralSources(bool _metadataLiteralSources)
 {
-	if (m_stackState >= ParsingPerformed)
+	if (m_stackState >= ParsedAndImported)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set use literal sources before parsing."));
 	m_metadataLiteralSources = _metadataLiteralSources;
 }
 
 void CompilerStack::setMetadataHash(MetadataHash _metadataHash)
 {
-	if (m_stackState >= ParsingPerformed)
+	if (m_stackState >= ParsedAndImported)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set metadata hash before parsing."));
 	m_metadataHash = _metadataHash;
 }
 
 void CompilerStack::addSMTLib2Response(h256 const& _hash, string const& _response)
 {
-	if (m_stackState >= ParsingPerformed)
+	if (m_stackState >= ParsedAndImported)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must add SMTLib2 responses before parsing."));
 	m_smtlib2Responses[_hash] = _response;
 }
@@ -214,6 +214,7 @@ void CompilerStack::reset(bool _keepSettings)
 		m_optimiserSettings = OptimiserSettings::minimal();
 		m_metadataLiteralSources = false;
 		m_metadataHash = MetadataHash::IPFS;
+		m_stopAfter = State::CompilationSuccessful;
 	}
 	m_globalContext.reset();
 	m_sourceOrder.clear();
@@ -247,6 +248,7 @@ bool CompilerStack::parse()
 	vector<string> sourcesToParse;
 	for (auto const& s: m_sources)
 		sourcesToParse.push_back(s.first);
+
 	for (size_t i = 0; i < sourcesToParse.size(); ++i)
 	{
 		string const& path = sourcesToParse[i];
@@ -258,19 +260,26 @@ bool CompilerStack::parse()
 		else
 		{
 			source.ast->annotation().path = path;
-			for (auto const& newSource: loadMissingSources(*source.ast, path))
-			{
-				string const& newPath = newSource.first;
-				string const& newContents = newSource.second;
-				m_sources[newPath].scanner = make_shared<Scanner>(CharStream(newContents, newPath));
-				sourcesToParse.push_back(newPath);
-			}
+			if (m_stopAfter >= ParsedAndImported)
+				for (auto const& newSource: loadMissingSources(*source.ast, path))
+				{
+					string const& newPath = newSource.first;
+					string const& newContents = newSource.second;
+					m_sources[newPath].scanner = make_shared<Scanner>(CharStream(newContents, newPath));
+					sourcesToParse.push_back(newPath);
+				}
 		}
 	}
 
-	m_stackState = ParsingPerformed;
+	if (m_stopAfter <= Parsed)
+		m_stackState = Parsed;
+	else
+		m_stackState = ParsedAndImported;
 	if (!Error::containsOnlyWarnings(m_errorReporter.errors()))
 		m_hasError = true;
+
+	storeContractDefinitions();
+
 	return !m_hasError;
 }
 
@@ -290,13 +299,15 @@ void CompilerStack::importASTs(map<string, Json::Value> const& _sources)
 		source.scanner = scanner;
 		m_sources[path] = source;
 	}
-	m_stackState = ParsingPerformed;
+	m_stackState = ParsedAndImported;
 	m_importedSources = true;
+
+	storeContractDefinitions();
 }
 
 bool CompilerStack::analyze()
 {
-	if (m_stackState != ParsingPerformed || m_stackState >= AnalysisPerformed)
+	if (m_stackState != ParsedAndImported || m_stackState >= AnalysisPerformed)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must call analyze only after parsing was performed."));
 	resolveImports();
 
@@ -336,26 +347,6 @@ bool CompilerStack::analyze()
 			if (source->ast && !resolver.resolveNamesAndTypes(*source->ast))
 				return false;
 
-		// Store contract definitions.
-		for (Source const* source: m_sourceOrder)
-			if (source->ast)
-				for (
-					ContractDefinition const* contract:
-					ASTNode::filteredNodes<ContractDefinition>(source->ast->nodes())
-				)
-				{
-					// Note that we now reference contracts by their fully qualified names, and
-					// thus contracts can only conflict if declared in the same source file. This
-					// should already cause a double-declaration error elsewhere.
-					if (!m_contracts.count(contract->fullyQualifiedName()))
-						m_contracts[contract->fullyQualifiedName()].contract = contract;
-					else
-						solAssert(
-							m_errorReporter.hasErrors(),
-							"Contract already present (name clash?), but no error was reported."
-						);
-				}
-
 		DeclarationTypeChecker declarationTypeChecker(m_errorReporter, m_evmVersion);
 		for (Source const* source: m_sourceOrder)
 			if (source->ast && !declarationTypeChecker.check(*source->ast))
@@ -469,9 +460,13 @@ bool CompilerStack::analyze()
 	return !m_hasError;
 }
 
-bool CompilerStack::parseAndAnalyze()
+bool CompilerStack::parseAndAnalyze(State _stopAfter)
 {
+	m_stopAfter = _stopAfter;
+
 	bool success = parse();
+	if (m_stackState >= m_stopAfter)
+		return success;
 	if (success || m_parserErrorRecovery)
 		success = analyze();
 	return success;
@@ -502,12 +497,16 @@ bool CompilerStack::isRequestedContract(ContractDefinition const& _contract) con
 	return false;
 }
 
-bool CompilerStack::compile()
+bool CompilerStack::compile(State _stopAfter)
 {
+	m_stopAfter = _stopAfter;
 	if (m_stackState < AnalysisPerformed)
-		if (!parseAndAnalyze())
+		if (!parseAndAnalyze(_stopAfter))
 			return false;
 
+	if (m_stackState >= m_stopAfter)
+		return true;
+
 	if (m_hasError)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Called compile with errors."));
 
@@ -574,7 +573,7 @@ void CompilerStack::link()
 
 vector<string> CompilerStack::contractNames() const
 {
-	if (m_stackState < AnalysisPerformed)
+	if (m_stackState < Parsed)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Parsing was not successful."));
 	vector<string> contractNames;
 	for (auto const& contract: m_contracts)
@@ -921,7 +920,7 @@ Scanner const& CompilerStack::scanner(string const& _sourceName) const
 
 SourceUnit const& CompilerStack::ast(string const& _sourceName) const
 {
-	if (m_stackState < ParsingPerformed)
+	if (m_stackState < Parsed)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Parsing not yet performed."));
 	if (!source(_sourceName).ast && !m_parserErrorRecovery)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Parsing was not successful."));
@@ -994,7 +993,7 @@ string const& CompilerStack::Source::ipfsUrl() const
 
 StringMap CompilerStack::loadMissingSources(SourceUnit const& _ast, std::string const& _sourcePath)
 {
-	solAssert(m_stackState < ParsingPerformed, "");
+	solAssert(m_stackState < ParsedAndImported, "");
 	StringMap newSources;
 	try
 	{
@@ -1038,7 +1037,7 @@ StringMap CompilerStack::loadMissingSources(SourceUnit const& _ast, std::string
 
 string CompilerStack::applyRemapping(string const& _path, string const& _context)
 {
-	solAssert(m_stackState < ParsingPerformed, "");
+	solAssert(m_stackState < ParsedAndImported, "");
 	// Try to find the longest prefix match in all remappings that are active in the current context.
 	auto isPrefixOf = [](string const& _a, string const& _b)
 	{
@@ -1080,7 +1079,7 @@ string CompilerStack::applyRemapping(string const& _path, string const& _context
 
 void CompilerStack::resolveImports()
 {
-	solAssert(m_stackState == ParsingPerformed, "");
+	solAssert(m_stackState == ParsedAndImported, "");
 
 	// topological sorting (depth first search) of the import graph, cutting potential cycles
 	vector<Source const*> sourceOrder;
@@ -1110,6 +1109,24 @@ void CompilerStack::resolveImports()
 	swap(m_sourceOrder, sourceOrder);
 }
 
+void CompilerStack::storeContractDefinitions()
+{
+	for (auto const& pair: m_sources)
+		if (pair.second.ast)
+			for (
+				ContractDefinition const* contract:
+				ASTNode::filteredNodes<ContractDefinition>(pair.second.ast->nodes())
+			)
+			{
+				string fullyQualifiedName = *pair.second.ast->annotation().path + ":" + contract->name();
+				// Note that we now reference contracts by their fully qualified names, and
+				// thus contracts can only conflict if declared in the same source file. This
+				// should already cause a double-declaration error elsewhere.
+				if (!m_contracts.count(fullyQualifiedName))
+					m_contracts[fullyQualifiedName].contract = contract;
+			}
+}
+
 namespace
 {
 bool onlySafeExperimentalFeaturesActivated(set<ExperimentalFeature> const& features)

libsolidity/interface/CompilerStack.h

@@ -90,7 +90,8 @@ public:
 	enum State {
 		Empty,
 		SourcesSet,
-		ParsingPerformed,
+		Parsed,
+		ParsedAndImported,
 		AnalysisPerformed,
 		CompilationSuccessful
 	};
@@ -216,11 +217,11 @@ public:
 
 	/// Parses and analyzes all source units that were added
 	/// @returns false on error.
-	bool parseAndAnalyze();
+	bool parseAndAnalyze(State _stopAfter = State::CompilationSuccessful);
 
 	/// Compiles the source units that were previously added and parsed.
 	/// @returns false on error.
-	bool compile();
+	bool compile(State _stopAfter = State::CompilationSuccessful);
 
 	/// @returns the list of sources (paths) used
 	std::vector<std::string> sourceNames() const;
@@ -373,6 +374,9 @@ private:
 	std::string applyRemapping(std::string const& _path, std::string const& _context);
 	void resolveImports();
 
+	/// Store the contract definitions in m_contracts.
+	void storeContractDefinitions();
+
 	/// @returns true if the source is requested to be compiled.
 	bool isRequestedSource(std::string const& _sourceName) const;
 
@@ -446,6 +450,7 @@ private:
 	ReadCallback::Callback m_readFile;
 	OptimiserSettings m_optimiserSettings;
 	RevertStrings m_revertStrings = RevertStrings::Default;
+	State m_stopAfter = State::CompilationSuccessful;
 	langutil::EVMVersion m_evmVersion;
 	smtutil::SMTSolverChoice m_enabledSMTSolvers;
 	std::map<std::string, std::set<std::string>> m_requestedContractNames;

libsolidity/interface/StandardCompiler.cpp

@@ -414,7 +414,7 @@ std::optional<Json::Value> checkAuxiliaryInputKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"parserErrorRecovery", "debug", "evmVersion", "libraries", "metadata", "optimizer", "outputSelection", "remappings"};
+	static set<string> keys{"parserErrorRecovery", "debug", "evmVersion", "libraries", "metadata", "optimizer", "outputSelection", "remappings", "stopAfter"};
 	return checkKeys(_input, keys, "settings");
 }
 
@@ -724,6 +724,17 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 	if (auto result = checkSettingsKeys(settings))
 		return *result;
 
+	if (settings.isMember("stopAfter"))
+	{
+		if (!settings["stopAfter"].isString())
+			return formatFatalError("JSONError", "\"settings.stopAfter\" must be a string.");
+
+		if (settings["stopAfter"].asString() != "parsing")
+			return formatFatalError("JSONError", "Invalid value for \"settings.stopAfter\". Only valid value is \"parsing\".");
+
+		ret.stopAfter = CompilerStack::State::Parsed;
+	}
+
 	if (settings.isMember("parserErrorRecovery"))
 	{
 		if (!settings["parserErrorRecovery"].isBool())
@@ -849,6 +860,12 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 
 	ret.outputSelection = std::move(outputSelection);
 
+	if (ret.stopAfter != CompilerStack::State::CompilationSuccessful && isBinaryRequested(ret.outputSelection))
+		return formatFatalError(
+			"JSONError",
+			"Requested output selection conflicts with \"settings.stopAfter\"."
+		);
+
 	return { std::move(ret) };
 }
 
@@ -883,7 +900,7 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 		if (binariesRequested)
 			compilerStack.compile();
 		else
-			compilerStack.parseAndAnalyze();
+			compilerStack.parseAndAnalyze(_inputsAndSettings.stopAfter);
 
 		for (auto const& error: compilerStack.errors())
 		{
@@ -1005,7 +1022,10 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 		analysisPerformed = false;
 
 	/// Inconsistent state - stop here to receive error reports from users
-	if (((binariesRequested && !compilationSuccess) || !analysisPerformed) && errors.empty())
+	if (
+		((binariesRequested && !compilationSuccess) || !analysisPerformed) &&
+		(errors.empty() && _inputsAndSettings.stopAfter >= CompilerStack::State::AnalysisPerformed)
+	)
 		return formatFatalError("InternalCompilerError", "No error reported, but compilation failed.");
 
 	Json::Value output = Json::objectValue;
@@ -1021,16 +1041,17 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 
 	output["sources"] = Json::objectValue;
 	unsigned sourceIndex = 0;
-	for (string const& sourceName: analysisPerformed ? compilerStack.sourceNames() : vector<string>())
-	{
-		Json::Value sourceResult = Json::objectValue;
-		sourceResult["id"] = sourceIndex++;
-		if (isArtifactRequested(_inputsAndSettings.outputSelection, sourceName, "", "ast", wildcardMatchesExperimental))
-			sourceResult["ast"] = ASTJsonConverter(false, compilerStack.sourceIndices()).toJson(compilerStack.ast(sourceName));
-		if (isArtifactRequested(_inputsAndSettings.outputSelection, sourceName, "", "legacyAST", wildcardMatchesExperimental))
-			sourceResult["legacyAST"] = ASTJsonConverter(true, compilerStack.sourceIndices()).toJson(compilerStack.ast(sourceName));
-		output["sources"][sourceName] = sourceResult;
-	}
+	if (compilerStack.state() >= CompilerStack::State::Parsed && (!compilerStack.hasError() || _inputsAndSettings.parserErrorRecovery))
+		for (string const& sourceName: compilerStack.sourceNames())
+		{
+			Json::Value sourceResult = Json::objectValue;
+			sourceResult["id"] = sourceIndex++;
+			if (isArtifactRequested(_inputsAndSettings.outputSelection, sourceName, "", "ast", wildcardMatchesExperimental))
+				sourceResult["ast"] = ASTJsonConverter(false, compilerStack.state(), compilerStack.sourceIndices()).toJson(compilerStack.ast(sourceName));
+			if (isArtifactRequested(_inputsAndSettings.outputSelection, sourceName, "", "legacyAST", wildcardMatchesExperimental))
+				sourceResult["legacyAST"] = ASTJsonConverter(true, compilerStack.state(), compilerStack.sourceIndices()).toJson(compilerStack.ast(sourceName));
+			output["sources"][sourceName] = sourceResult;
+		}
 
 	Json::Value contractsOutput = Json::objectValue;
 	for (string const& contractName: analysisPerformed ? compilerStack.contractNames() : vector<string>())

libsolidity/interface/StandardCompiler.h

@@ -60,6 +60,7 @@ private:
 		std::string language;
 		Json::Value errors;
 		bool parserErrorRecovery = false;
+		CompilerStack::State stopAfter = CompilerStack::State::CompilationSuccessful;
 		std::map<std::string, std::string> sources;
 		std::map<util::h256, std::string> smtLib2Responses;
 		langutil::EVMVersion evmVersion;