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

libsolidity/analysis/TypeChecker.cpp

@@ -2761,7 +2761,8 @@ bool TypeChecker::visit(MemberAccess const& _memberAccess)
 
 		if (!funType->bound())
 			if (auto contractType = dynamic_cast<ContractType const*>(exprType))
-				requiredLookup = contractType->isSuper() ? VirtualLookup::Super : VirtualLookup::Virtual;
+				if (contractType->isSuper())
+					requiredLookup = VirtualLookup::Super;
 	}
 
 	annotation.requiredLookup = requiredLookup;

libsolidity/codegen/ABIFunctions.cpp

@@ -802,7 +802,7 @@ string ABIFunctions::abiEncodingFunctionCompactStorageArray(
 					items[i]["inRange"] = "1";
 				else
 					items[i]["inRange"] = "0";
-				items[i]["extractFromSlot"] = m_utils.extractFromStorageValue(*_from.baseType(), i * storageBytes, false);
+				items[i]["extractFromSlot"] = m_utils.extractFromStorageValue(*_from.baseType(), i * storageBytes);
 			}
 			templ("items", items);
 			return templ.render();
@@ -888,7 +888,7 @@ string ABIFunctions::abiEncodingFunctionStruct(
 							members.back()["preprocess"] = "slotValue := sload(add(value, " + toCompactHexWithPrefix(storageSlotOffset) + "))";
 							previousSlotOffset = storageSlotOffset;
 						}
-						members.back()["retrieveValue"] = m_utils.extractFromStorageValue(*memberTypeFrom, intraSlotOffset, false) + "(slotValue)";
+						members.back()["retrieveValue"] = m_utils.extractFromStorageValue(*memberTypeFrom, intraSlotOffset) + "(slotValue)";
 					}
 					else
 					{

libsolidity/codegen/ContractCompiler.cpp

@@ -702,26 +702,7 @@ bool ContractCompiler::visit(InlineAssembly const& _inlineAssembly)
 		{
 			int const depositBefore = _assembly.stackHeight();
 			solAssert(!!decl->type(), "Type of declaration required but not yet determined.");
-			if (FunctionDefinition const* functionDef = dynamic_cast<FunctionDefinition const*>(decl))
-			{
-				solAssert(!ref->second.isOffset && !ref->second.isSlot, "");
-				functionDef = &functionDef->resolveVirtual(m_context.mostDerivedContract());
-				auto functionEntryLabel = m_context.functionEntryLabel(*functionDef).pushTag();
-				solAssert(functionEntryLabel.data() <= std::numeric_limits<size_t>::max(), "");
-				_assembly.appendLabelReference(static_cast<size_t>(functionEntryLabel.data()));
-				// If there is a runtime context, we have to merge both labels into the same
-				// stack slot in case we store it in storage.
-				if (CompilerContext* rtc = m_context.runtimeContext())
-				{
-					_assembly.appendConstant(u256(1) << 32);
-					_assembly.appendInstruction(Instruction::MUL);
-					auto runtimeEntryLabel = rtc->functionEntryLabel(*functionDef).toSubAssemblyTag(m_context.runtimeSub());
-					solAssert(runtimeEntryLabel.data() <= std::numeric_limits<size_t>::max(), "");
-					_assembly.appendLabelReference(static_cast<size_t>(runtimeEntryLabel.data()));
-					_assembly.appendInstruction(Instruction::OR);
-				}
-			}
-			else if (auto variable = dynamic_cast<VariableDeclaration const*>(decl))
+			if (auto variable = dynamic_cast<VariableDeclaration const*>(decl))
 			{
 				solAssert(!variable->immutable(), "");
 				if (variable->isConstant())

libsolidity/codegen/YulUtilFunctions.cpp

@@ -2153,58 +2153,47 @@ string YulUtilFunctions::readFromStorage(Type const& _type, size_t _offset, bool
 string YulUtilFunctions::readFromStorageDynamic(Type const& _type, bool _splitFunctionTypes)
 {
 	solAssert(_type.isValueType(), "");
-	return readFromStorageValueTypeDynamic(_type, _splitFunctionTypes);
+	return readFromStorageValueType(_type, {}, _splitFunctionTypes);
 }
 
-string YulUtilFunctions::readFromStorageValueType(Type const& _type, size_t _offset, bool _splitFunctionTypes)
+string YulUtilFunctions::readFromStorageValueType(Type const& _type, optional<size_t> _offset, bool _splitFunctionTypes)
 {
 	solAssert(_type.isValueType(), "");
 
-	if (_type.category() == Type::Category::Function)
-		solUnimplementedAssert(!_splitFunctionTypes, "");
 	string functionName =
 			"read_from_storage_" +
-			string(_splitFunctionTypes ? "split_" : "") +
-			"offset_" +
-			to_string(_offset) +
+			string(_splitFunctionTypes ? "split_" : "") + (
+				_offset.has_value() ?
+				"offset_" + to_string(*_offset) :
+				"dynamic"
+			) +
 			"_" +
 			_type.identifier();
 
 	return m_functionCollector.createFunction(functionName, [&] {
-		solAssert(_type.sizeOnStack() == 1, "");
-		return Whiskers(R"(
-			function <functionName>(slot) -> value {
-				value := <extract>(sload(slot))
+		Whiskers templ(R"(
+			function <functionName>(slot<?dynamic>, offset</dynamic>) -> <?split>addr, selector<!split>value</split> {
+				<?split>let</split> value := <extract>(sload(slot)<?dynamic>, offset</dynamic>)
+				<?split>
+					addr, selector := <splitFunction>(value)
+				</split>
 			}
-		)")
-				("functionName", functionName)
-				("extract", extractFromStorageValue(_type, _offset, false))
-				.render();
+		)");
+		templ("functionName", functionName);
+		templ("dynamic", !_offset.has_value());
+		if (_offset.has_value())
+			templ("extract", extractFromStorageValue(_type, *_offset));
+		else
+			templ("extract", extractFromStorageValueDynamic(_type));
+		auto const* funType = dynamic_cast<FunctionType const*>(&_type);
+		bool split = _splitFunctionTypes && funType && funType->kind() == FunctionType::Kind::External;
+		templ("split", split);
+		if (split)
+			templ("splitFunction", splitExternalFunctionIdFunction());
+		return templ.render();
 	});
 }
-string YulUtilFunctions::readFromStorageValueTypeDynamic(Type const& _type, bool _splitFunctionTypes)
-{
-	solAssert(_type.isValueType(), "");
-	if (_type.category() == Type::Category::Function)
-		solUnimplementedAssert(!_splitFunctionTypes, "");
 
-	string functionName =
-		"read_from_storage_value_type_dynamic" +
-		string(_splitFunctionTypes ? "split_" : "") +
-		"_" +
-		_type.identifier();
-	return m_functionCollector.createFunction(functionName, [&] {
-		solAssert(_type.sizeOnStack() == 1, "");
-		return Whiskers(R"(
-			function <functionName>(slot, offset) -> value {
-				value := <extract>(sload(slot), offset)
-			}
-		)")
-		("functionName", functionName)
-		("extract", extractFromStorageValueDynamic(_type, _splitFunctionTypes))
-		.render();
-	});
-}
 string YulUtilFunctions::readFromStorageReferenceType(Type const& _type)
 {
 	solUnimplementedAssert(_type.category() == Type::Category::Struct, "");
@@ -2437,9 +2426,7 @@ string YulUtilFunctions::updateStorageValueFunction(
 
 string YulUtilFunctions::writeToMemoryFunction(Type const& _type)
 {
-	string const functionName =
-		string("write_to_memory_") +
-		_type.identifier();
+	string const functionName = "write_to_memory_" + _type.identifier();
 
 	return m_functionCollector.createFunction(functionName, [&] {
 		solAssert(!dynamic_cast<StringLiteralType const*>(&_type), "");
@@ -2493,14 +2480,10 @@ string YulUtilFunctions::writeToMemoryFunction(Type const& _type)
 	});
 }
 
-string YulUtilFunctions::extractFromStorageValueDynamic(Type const& _type, bool _splitFunctionTypes)
+string YulUtilFunctions::extractFromStorageValueDynamic(Type const& _type)
 {
-	if (_type.category() == Type::Category::Function)
-		solUnimplementedAssert(!_splitFunctionTypes, "");
-
 	string functionName =
 		"extract_from_storage_value_dynamic" +
-		string(_splitFunctionTypes ? "split_" : "") +
 		_type.identifier();
 	return m_functionCollector.createFunction(functionName, [&] {
 		return Whiskers(R"(
@@ -2510,21 +2493,14 @@ string YulUtilFunctions::extractFromStorageValueDynamic(Type const& _type, bool
 		)")
 		("functionName", functionName)
 		("shr", shiftRightFunctionDynamic())
-		("cleanupStorage", cleanupFromStorageFunction(_type, _splitFunctionTypes))
+		("cleanupStorage", cleanupFromStorageFunction(_type))
 		.render();
 	});
 }
 
-string YulUtilFunctions::extractFromStorageValue(Type const& _type, size_t _offset, bool _splitFunctionTypes)
+string YulUtilFunctions::extractFromStorageValue(Type const& _type, size_t _offset)
 {
-	solUnimplementedAssert(!_splitFunctionTypes, "");
-
-	string functionName =
-		"extract_from_storage_value_" +
-		string(_splitFunctionTypes ? "split_" : "") +
-		"offset_" +
-		to_string(_offset) +
-		_type.identifier();
+	string functionName = "extract_from_storage_value_offset_" + to_string(_offset) + _type.identifier();
 	return m_functionCollector.createFunction(functionName, [&] {
 		return Whiskers(R"(
 			function <functionName>(slot_value) -> value {
@@ -2533,18 +2509,16 @@ string YulUtilFunctions::extractFromStorageValue(Type const& _type, size_t _offs
 		)")
 		("functionName", functionName)
 		("shr", shiftRightFunction(_offset * 8))
-		("cleanupStorage", cleanupFromStorageFunction(_type, _splitFunctionTypes))
+		("cleanupStorage", cleanupFromStorageFunction(_type))
 		.render();
 	});
 }
 
-string YulUtilFunctions::cleanupFromStorageFunction(Type const& _type, bool _splitFunctionTypes)
+string YulUtilFunctions::cleanupFromStorageFunction(Type const& _type)
 {
 	solAssert(_type.isValueType(), "");
-	if (_type.category() == Type::Category::Function)
-		solUnimplementedAssert(!_splitFunctionTypes, "");
 
-	string functionName = string("cleanup_from_storage_") + (_splitFunctionTypes ? "split_" : "") + _type.identifier();
+	string functionName = string("cleanup_from_storage_") + _type.identifier();
 	return m_functionCollector.createFunction(functionName, [&] {
 		Whiskers templ(R"(
 			function <functionName>(value) -> cleaned {
@@ -2581,22 +2555,37 @@ string YulUtilFunctions::cleanupFromStorageFunction(Type const& _type, bool _spl
 
 string YulUtilFunctions::prepareStoreFunction(Type const& _type)
 {
-	if (_type.category() == Type::Category::Function)
-		solUnimplementedAssert(dynamic_cast<FunctionType const&>(_type).kind() == FunctionType::Kind::Internal, "");
-
 	string functionName = "prepare_store_" + _type.identifier();
 	return m_functionCollector.createFunction(functionName, [&]() {
-		Whiskers templ(R"(
-			function <functionName>(value) -> ret {
-				ret := <actualPrepare>
-			}
-		)");
-		templ("functionName", functionName);
-		if (_type.category() == Type::Category::FixedBytes)
-			templ("actualPrepare", shiftRightFunction(256 - 8 * _type.storageBytes()) + "(value)");
+		solAssert(_type.isValueType(), "");
+		auto const* funType = dynamic_cast<FunctionType const*>(&_type);
+		if (funType && funType->kind() == FunctionType::Kind::External)
+		{
+			Whiskers templ(R"(
+				function <functionName>(addr, selector) -> ret {
+					ret := <prepareBytes>(<combine>(addr, selector))
+				}
+			)");
+			templ("functionName", functionName);
+			templ("prepareBytes", prepareStoreFunction(*TypeProvider::fixedBytes(24)));
+			templ("combine", combineExternalFunctionIdFunction());
+			return templ.render();
+		}
 		else
-			templ("actualPrepare", "value");
-		return templ.render();
+		{
+			solAssert(_type.sizeOnStack() == 1, "");
+			Whiskers templ(R"(
+				function <functionName>(value) -> ret {
+					ret := <actualPrepare>
+				}
+			)");
+			templ("functionName", functionName);
+			if (_type.category() == Type::Category::FixedBytes)
+				templ("actualPrepare", shiftRightFunction(256 - 8 * _type.storageBytes()) + "(value)");
+			else
+				templ("actualPrepare", "value");
+			return templ.render();
+		}
 	});
 }
 
@@ -3683,37 +3672,44 @@ string YulUtilFunctions::readFromMemoryOrCalldata(Type const& _type, bool _fromC
 		}
 
 		solAssert(_type.isValueType(), "");
-		if (auto const* funType = dynamic_cast<FunctionType const*>(&_type))
-			if (funType->kind() == FunctionType::Kind::External)
-				return Whiskers(R"(
-					function <functionName>(memPtr) -> addr, selector {
-						let combined := <load>(memPtr)
-						addr, selector := <splitFunction>(combined)
-					}
-				)")
-				("functionName", functionName)
-				("load", _fromCalldata ? "calldataload" : "mload")
-				("splitFunction", splitExternalFunctionIdFunction())
-				.render();
-
-
-		return Whiskers(R"(
-			function <functionName>(ptr) -> value {
+		Whiskers templ(R"(
+			function <functionName>(ptr) -> <returnVariables> {
 				<?fromCalldata>
-					value := calldataload(ptr)
+					let value := calldataload(ptr)
 					<validate>(value)
 				<!fromCalldata>
-					value := <cleanup>(mload(ptr))
+					let value := <cleanup>(mload(ptr))
 				</fromCalldata>
+
+				<returnVariables> :=
+				<?externalFunction>
+					<splitFunction>(value)
+				<!externalFunction>
+					value
+				</externalFunction>
 			}
-		)")
-		("functionName", functionName)
-		("fromCalldata", _fromCalldata)
-		("validate", validatorFunction(_type, true))
+		)");
+		templ("functionName", functionName);
+		templ("fromCalldata", _fromCalldata);
+		if (_fromCalldata)
+			templ("validate", validatorFunction(_type, true));
+		auto const* funType = dynamic_cast<FunctionType const*>(&_type);
+		if (funType && funType->kind() == FunctionType::Kind::External)
+		{
+			templ("externalFunction", true);
+			templ("splitFunction", splitExternalFunctionIdFunction());
+			templ("returnVariables", "addr, selector");
+		}
+		else
+		{
+			templ("externalFunction", false);
+			templ("returnVariables", "returnValue");
+		}
+
 		// Byte array elements generally need cleanup.
 		// Other types are cleaned as well to account for dirty memory e.g. due to inline assembly.
-		("cleanup", cleanupFunction(_type))
-		.render();
+		templ("cleanup", cleanupFunction(_type));
+		return templ.render();
 	});
 }
 

libsolidity/codegen/YulUtilFunctions.h

@@ -283,10 +283,10 @@ public:
 	/// @returns a function that extracts a value type from storage slot that has been
 	/// retrieved already.
 	/// 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 extractFromStorageValue(Type const& _type, size_t _offset, bool _splitFunctionTypes);
-	std::string extractFromStorageValueDynamic(Type const& _type, bool _splitFunctionTypes);
+	///
+	/// For external function types, input and output is in "compressed"/"unsplit" form.
+	std::string extractFromStorageValue(Type const& _type, size_t _offset);
+	std::string extractFromStorageValueDynamic(Type const& _type);
 
 	/// Returns the name of a function will write the given value to
 	/// the specified slot and offset. If offset is not given, it is expected as
@@ -309,9 +309,8 @@ public:
 	/// higher order bytes or left-aligns (in case of bytesNN).
 	/// The storage cleanup expects the value to be right-aligned with potentially
 	/// dirty higher order bytes.
-	/// @param _splitFunctionTypes if false, returns the address and function signature in a
-	/// single variable.
-	std::string cleanupFromStorageFunction(Type const& _type, bool _splitFunctionTypes);
+	/// For external functions, input and output is in "compressed"/"unsplit" form.
+	std::string cleanupFromStorageFunction(Type const& _type);
 
 	/// @returns the name of a function that prepares a value of the given type
 	/// for being stored in storage. This usually includes cleanup and right-alignment
@@ -459,8 +458,8 @@ private:
 	/// 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);
+	/// @param _offset if provided, read from static offset, otherwise offset is a parameter of the Yul function.
+	std::string readFromStorageValueType(Type const& _type, std::optional<size_t> _offset, bool _splitFunctionTypes);
 
 	/// @returns a function that reads a reference type from storage to memory (performing a deep copy).
 	std::string readFromStorageReferenceType(Type const& _type);

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -2720,7 +2720,7 @@ IRVariable IRGeneratorForStatements::readFromLValue(IRLValue const& _lvalue)
 				define(result) << _storage.slot << "\n";
 			else if (std::holds_alternative<string>(_storage.offset))
 				define(result) <<
-					m_utils.readFromStorageDynamic(_lvalue.type, false) <<
+					m_utils.readFromStorageDynamic(_lvalue.type, true) <<
 					"(" <<
 					_storage.slot <<
 					", " <<
@@ -2728,7 +2728,7 @@ IRVariable IRGeneratorForStatements::readFromLValue(IRLValue const& _lvalue)
 					")\n";
 			else
 				define(result) <<
-					m_utils.readFromStorage(_lvalue.type, std::get<unsigned>(_storage.offset), false) <<
+					m_utils.readFromStorage(_lvalue.type, std::get<unsigned>(_storage.offset), true) <<
 					"(" <<
 					_storage.slot <<
 					")\n";

libsolidity/formal/BMC.cpp

@@ -34,10 +34,11 @@ BMC::BMC(
 	ErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
-	smtutil::SMTSolverChoice _enabledSolvers
+	smtutil::SMTSolverChoice _enabledSolvers,
+	optional<unsigned> _timeout
 ):
 	SMTEncoder(_context),
-	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers)),
+	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers, _timeout)),
 	m_outerErrorReporter(_errorReporter)
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
@@ -491,7 +492,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 		m_errorReporter.warning(
 			5729_error,
 			_funCall.location(),
-			"Assertion checker does not yet implement this type of function call."
+			"BMC does not yet implement this type of function call."
 		);
 	else
 	{
@@ -909,9 +910,9 @@ void BMC::checkBooleanNotConstant(
 	m_interface->pop();
 
 	if (positiveResult == smtutil::CheckResult::ERROR || negatedResult == smtutil::CheckResult::ERROR)
-		m_errorReporter.warning(8592_error, _condition.location(), "Error trying to invoke SMT solver.");
+		m_errorReporter.warning(8592_error, _condition.location(), "BMC: Error trying to invoke SMT solver.");
 	else if (positiveResult == smtutil::CheckResult::CONFLICTING || negatedResult == smtutil::CheckResult::CONFLICTING)
-		m_errorReporter.warning(3356_error, _condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound.");
+		m_errorReporter.warning(3356_error, _condition.location(), "BMC: At least two SMT solvers provided conflicting answers. Results might not be sound.");
 	else if (positiveResult == smtutil::CheckResult::SATISFIABLE && negatedResult == smtutil::CheckResult::SATISFIABLE)
 	{
 		// everything fine.
@@ -921,7 +922,7 @@ void BMC::checkBooleanNotConstant(
 		// can't do anything.
 	}
 	else if (positiveResult == smtutil::CheckResult::UNSATISFIABLE && negatedResult == smtutil::CheckResult::UNSATISFIABLE)
-		m_errorReporter.warning(2512_error, _condition.location(), "Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
+		m_errorReporter.warning(2512_error, _condition.location(), "BMC: Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
 	else
 	{
 		string description;
@@ -956,7 +957,7 @@ BMC::checkSatisfiableAndGenerateModel(vector<smtutil::Expression> const& _expres
 	}
 	catch (smtutil::SolverError const& _e)
 	{
-		string description("Error querying SMT solver");
+		string description("BMC: Error querying SMT solver");
 		if (_e.comment())
 			description += ": " + *_e.comment();
 		m_errorReporter.warning(8140_error, description);

libsolidity/formal/BMC.h

@@ -61,7 +61,8 @@ public:
 		langutil::ErrorReporter& _errorReporter,
 		std::map<h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
-		smtutil::SMTSolverChoice _enabledSolvers
+		smtutil::SMTSolverChoice _enabledSolvers,
+		std::optional<unsigned> timeout
 	);
 
 	void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTarget::Type>> _solvedTargets);

libsolidity/formal/CHC.cpp

@@ -49,18 +49,20 @@ CHC::CHC(
 	ErrorReporter& _errorReporter,
 	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
 	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
-	SMTSolverChoice _enabledSolvers
+	SMTSolverChoice _enabledSolvers,
+	optional<unsigned> _timeout
 ):
 	SMTEncoder(_context),
 	m_outerErrorReporter(_errorReporter),
-	m_enabledSolvers(_enabledSolvers)
+	m_enabledSolvers(_enabledSolvers),
+	m_queryTimeout(_timeout)
 {
 	bool usesZ3 = _enabledSolvers.z3;
 #ifndef HAVE_Z3
 	usesZ3 = false;
 #endif
 	if (!usesZ3)
-		m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback);
+		m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback, m_queryTimeout);
 }
 
 void CHC::analyze(SourceUnit const& _source)
@@ -69,7 +71,7 @@ void CHC::analyze(SourceUnit const& _source)
 
 	resetSourceAnalysis();
 
-	set<SourceUnit const*, IdCompare> sources;
+	set<SourceUnit const*, EncodingContext::IdCompare> sources;
 	sources.insert(&_source);
 	for (auto const& source: _source.referencedSourceUnits(true))
 		sources.insert(source);
@@ -79,6 +81,24 @@ void CHC::analyze(SourceUnit const& _source)
 		source->accept(*this);
 
 	checkVerificationTargets();
+
+	bool ranSolver = true;
+#ifndef HAVE_Z3
+	ranSolver = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get())->unhandledQueries().empty();
+#endif
+	if (!ranSolver && !m_noSolverWarning)
+	{
+		m_noSolverWarning = true;
+		m_outerErrorReporter.warning(
+			3996_error,
+			SourceLocation(),
+			"CHC analysis was not possible since no integrated z3 SMT solver was found."
+		);
+	}
+	else
+		m_outerErrorReporter.append(m_errorReporter.errors());
+
+	m_errorReporter.clear();
 }
 
 vector<string> CHC::unhandledQueries() const
@@ -681,7 +701,7 @@ void CHC::resetSourceAnalysis()
 	if (usesZ3)
 	{
 		/// z3::fixedpoint does not have a reset mechanism, so we need to create another.
-		m_interface.reset(new Z3CHCInterface());
+		m_interface.reset(new Z3CHCInterface(m_queryTimeout));
 		auto z3Interface = dynamic_cast<Z3CHCInterface const*>(m_interface.get());
 		solAssert(z3Interface, "");
 		m_context.setSolver(z3Interface->z3Interface());
@@ -1076,10 +1096,10 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression c
 	case CheckResult::UNKNOWN:
 		break;
 	case CheckResult::CONFLICTING:
-		m_outerErrorReporter.warning(1988_error, _location, "CHC: At least two SMT solvers provided conflicting answers. Results might not be sound.");
+		m_errorReporter.warning(1988_error, _location, "CHC: At least two SMT solvers provided conflicting answers. Results might not be sound.");
 		break;
 	case CheckResult::ERROR:
-		m_outerErrorReporter.warning(1218_error, _location, "CHC: Error trying to invoke SMT solver.");
+		m_errorReporter.warning(1218_error, _location, "CHC: Error trying to invoke SMT solver.");
 		break;
 	}
 	return {result, cex};
@@ -1233,21 +1253,21 @@ void CHC::checkAndReportTarget(
 		m_unsafeTargets[_target.errorNode].insert(_target.type);
 		auto cex = generateCounterexample(model, error().name);
 		if (cex)
-			m_outerErrorReporter.warning(
+			m_errorReporter.warning(
 				_errorReporterId,
 				location,
 				"CHC: " + _satMsg,
 				SecondarySourceLocation().append("Counterexample:\n" + *cex, SourceLocation{})
 			);
 		else
-			m_outerErrorReporter.warning(
+			m_errorReporter.warning(
 				_errorReporterId,
 				location,
 				"CHC: " + _satMsg
 			);
 	}
 	else if (!_unknownMsg.empty())
-		m_outerErrorReporter.warning(
+		m_errorReporter.warning(
 			_errorReporterId,
 			location,
 			"CHC: " + _unknownMsg

libsolidity/formal/CHC.h

@@ -55,7 +55,8 @@ public:
 		langutil::ErrorReporter& _errorReporter,
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
-		smtutil::SMTSolverChoice _enabledSolvers
+		smtutil::SMTSolverChoice _enabledSolvers,
+		std::optional<unsigned> timeout
 	);
 
 	void analyze(SourceUnit const& _sources);
@@ -99,14 +100,6 @@ private:
 	) override;
 	//@}
 
-	struct IdCompare
-	{
-		bool operator()(ASTNode const* lhs, ASTNode const* rhs) const
-		{
-			return lhs->id() < rhs->id();
-		}
-	};
-
 	/// Helpers.
 	//@{
 	void resetSourceAnalysis();
@@ -286,12 +279,12 @@ private:
 	/// Query placeholders for constructors, if the key has type ContractDefinition*,
 	/// or external functions, if the key has type FunctionDefinition*.
 	/// A placeholder is created for each possible context of a function (e.g. multiple contracts in contract inheritance hierarchy).
-	std::map<ASTNode const*, std::vector<CHCQueryPlaceholder>, IdCompare> m_queryPlaceholders;
+	std::map<ASTNode const*, std::vector<CHCQueryPlaceholder>, smt::EncodingContext::IdCompare> m_queryPlaceholders;
 
 	/// Records verification conditions IDs per function encountered during an analysis of that function.
 	/// The key is the ASTNode of the function where the verification condition has been encountered,
 	/// or the ASTNode of the contract if the verification condition happens inside an implicit constructor.
-	std::map<ASTNode const*, std::vector<unsigned>, IdCompare> m_functionTargetIds;
+	std::map<ASTNode const*, std::vector<unsigned>, smt::EncodingContext::IdCompare> m_functionTargetIds;
 	/// Helper mapping unique IDs to actual verification targets.
 	std::map<unsigned, CHCVerificationTarget> m_verificationTargets;
 
@@ -305,7 +298,7 @@ private:
 	//@{
 	FunctionDefinition const* m_currentFunction = nullptr;
 
-	std::map<ASTNode const*, std::set<ASTNode const*, IdCompare>, IdCompare> m_callGraph;
+	std::map<ASTNode const*, std::set<ASTNode const*, smt::EncodingContext::IdCompare>, smt::EncodingContext::IdCompare> m_callGraph;
 
 	/// The current block.
 	smtutil::Expression m_currentBlock = smtutil::Expression(true);
@@ -330,6 +323,9 @@ private:
 
 	/// SMT solvers that are chosen at runtime.
 	smtutil::SMTSolverChoice m_enabledSolvers;
+
+	/// SMT query timeout in seconds.
+	std::optional<unsigned> m_queryTimeout;
 };
 
 }

libsolidity/formal/EncodingContext.h

@@ -23,8 +23,7 @@
 
 #include <libsmtutil/SolverInterface.h>
 
-#include <unordered_map>
-#include <set>
+#include <map>
 
 namespace solidity::frontend::smt
 {
@@ -67,12 +66,20 @@ public:
 		return m_solver->newVariable(move(_name), move(_sort));
 	}
 
+	struct IdCompare
+	{
+		bool operator()(ASTNode const* lhs, ASTNode const* rhs) const
+		{
+			return lhs->id() < rhs->id();
+		}
+	};
+
 	/// Variables.
 	//@{
 	/// @returns the symbolic representation of a program variable.
 	std::shared_ptr<SymbolicVariable> variable(frontend::VariableDeclaration const& _varDecl);
 	/// @returns all symbolic variables.
-	std::unordered_map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> const& variables() const { return m_variables; }
+	std::map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>, IdCompare> const& variables() const { return m_variables; }
 
 	/// Creates a symbolic variable and
 	/// @returns true if a variable's type is not supported and is therefore abstract.
@@ -105,7 +112,7 @@ public:
 	/// @returns the symbolic representation of an AST node expression.
 	std::shared_ptr<SymbolicVariable> expression(frontend::Expression const& _e);
 	/// @returns all symbolic expressions.
-	std::unordered_map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>> const& expressions() const { return m_expressions; }
+	std::map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>, IdCompare> const& expressions() const { return m_expressions; }
 
 	/// Creates the expression (value can be arbitrary).
 	/// @returns true if type is not supported.
@@ -119,7 +126,7 @@ public:
 	/// Global variables and functions.
 	std::shared_ptr<SymbolicVariable> globalSymbol(std::string const& _name);
 	/// @returns all symbolic globals.
-	std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> const& globalSymbols() const { return m_globalContext; }
+	std::map<std::string, std::shared_ptr<SymbolicVariable>> const& globalSymbols() const { return m_globalContext; }
 
 	/// Defines a new global variable or function
 	/// and @returns true if type was abstracted.
@@ -149,14 +156,14 @@ private:
 	/// Symbolic expressions.
 	//{@
 	/// Symbolic variables.
-	std::unordered_map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
+	std::map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>, IdCompare> m_variables;
 
 	/// Symbolic expressions.
-	std::unordered_map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
+	std::map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>, IdCompare> m_expressions;
 
 	/// Symbolic representation of global symbols including
 	/// variables and functions.
-	std::unordered_map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
+	std::map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
 
 	/// Symbolic representation of the blockchain state.
 	SymbolicState m_state;

libsolidity/formal/ModelChecker.cpp

@@ -27,14 +27,14 @@ using namespace solidity::frontend;
 ModelChecker::ModelChecker(
 	ErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
-	ModelCheckerEngine _engine,
+	ModelCheckerSettings _settings,
 	ReadCallback::Callback const& _smtCallback,
 	smtutil::SMTSolverChoice _enabledSolvers
 ):
-	m_engine(_engine),
+	m_settings(_settings),
 	m_context(),
-	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers),
-	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers)
+	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout),
+	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout)
 {
 }
 
@@ -43,14 +43,14 @@ void ModelChecker::analyze(SourceUnit const& _source)
 	if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		return;
 
-	if (m_engine.chc)
+	if (m_settings.engine.chc)
 		m_chc.analyze(_source);
 
 	auto solvedTargets = m_chc.safeTargets();
 	for (auto const& target: m_chc.unsafeTargets())
 		solvedTargets[target.first] += target.second;
 
-	if (m_engine.bmc)
+	if (m_settings.engine.bmc)
 		m_bmc.analyze(_source, solvedTargets);
 }
 

libsolidity/formal/ModelChecker.h

@@ -71,6 +71,12 @@ struct ModelCheckerEngine
 	}
 };
 
+struct ModelCheckerSettings
+{
+	ModelCheckerEngine engine = ModelCheckerEngine::All();
+	std::optional<unsigned> timeout;
+};
+
 class ModelChecker
 {
 public:
@@ -79,7 +85,7 @@ public:
 	ModelChecker(
 		langutil::ErrorReporter& _errorReporter,
 		std::map<solidity::util::h256, std::string> const& _smtlib2Responses,
-		ModelCheckerEngine _engine = ModelCheckerEngine::All(),
+		ModelCheckerSettings _settings = ModelCheckerSettings{},
 		ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(),
 		smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All()
 	);
@@ -95,7 +101,7 @@ public:
 	static smtutil::SMTSolverChoice availableSolvers();
 
 private:
-	ModelCheckerEngine m_engine;
+	ModelCheckerSettings m_settings;
 
 	/// Stores the context of the encoding.
 	smt::EncodingContext m_context;

libsolidity/formal/SMTEncoder.cpp

@@ -1799,23 +1799,25 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
 {
 	IntegerType const* intType = &_type;
 	string suffix = "div_mod_" + to_string(m_context.newUniqueId());
-	smt::SymbolicIntVariable d(intType, intType, "d_" + suffix, m_context);
-	smt::SymbolicIntVariable r(intType, intType, "r_" + suffix, m_context);
+	smt::SymbolicIntVariable dSymb(intType, intType, "d_" + suffix, m_context);
+	smt::SymbolicIntVariable rSymb(intType, intType, "r_" + suffix, m_context);
+	auto d = dSymb.currentValue();
+	auto r = rSymb.currentValue();
 
 	// x / y = d and x % y = r iff d * y + r = x and
 	// either x >= 0 and 0 <= r < abs(y) (or just 0 <= r < y for unsigned)
 	// or     x < 0 and -abs(y) < r <= 0
-	m_context.addAssertion(((d.currentValue() * _right) + r.currentValue()) == _left);
+	m_context.addAssertion(((d * _right) + r) == _left);
 	if (_type.isSigned())
 		m_context.addAssertion(
-			(_left >= 0 && 0 <= r.currentValue() && (_right == 0 || r.currentValue() < smtutil::abs(_right))) ||
-			(_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r.currentValue()) && r.currentValue() <= 0))
+			(_left >= 0 && 0 <= r && (_right == 0 || r < smtutil::abs(_right))) ||
+			(_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r) && r <= 0))
 		);
 	else // unsigned version
-		m_context.addAssertion(0 <= r.currentValue() && (_right == 0 || r.currentValue() < _right));
+		m_context.addAssertion(0 <= r && (_right == 0 || r < _right));
 
-	auto divResult = smtutil::Expression::ite(_right == 0, 0, d.currentValue());
-	auto modResult = smtutil::Expression::ite(_right == 0, 0, r.currentValue());
+	auto divResult = smtutil::Expression::ite(_right == 0, 0, d);
+	auto modResult = smtutil::Expression::ite(_right == 0, 0, r);
 	return {divResult, modResult};
 }
 

libsolidity/interface/CompilerStack.cpp

@@ -87,7 +87,6 @@ static int g_compilerStackCounts = 0;
 
 CompilerStack::CompilerStack(ReadCallback::Callback _readFile):
 	m_readFile{std::move(_readFile)},
-	m_modelCheckerEngine{ModelCheckerEngine::All()},
 	m_enabledSMTSolvers{smtutil::SMTSolverChoice::All()},
 	m_errorReporter{m_errorList}
 {
@@ -139,11 +138,11 @@ void CompilerStack::setEVMVersion(langutil::EVMVersion _version)
 	m_evmVersion = _version;
 }
 
-void CompilerStack::setModelCheckerEngine(ModelCheckerEngine _engine)
+void CompilerStack::setModelCheckerSettings(ModelCheckerSettings _settings)
 {
 	if (m_stackState >= ParsedAndImported)
-		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled model checking engines before parsing."));
-	m_modelCheckerEngine = _engine;
+		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set model checking settings before parsing."));
+	m_modelCheckerSettings = _settings;
 }
 
 void CompilerStack::setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSMTSolvers)
@@ -215,7 +214,7 @@ void CompilerStack::reset(bool _keepSettings)
 		m_remappings.clear();
 		m_libraries.clear();
 		m_evmVersion = langutil::EVMVersion();
-		m_modelCheckerEngine = ModelCheckerEngine::All();
+		m_modelCheckerSettings = ModelCheckerSettings{};
 		m_enabledSMTSolvers = smtutil::SMTSolverChoice::All();
 		m_generateIR = false;
 		m_generateEwasm = false;
@@ -452,7 +451,7 @@ bool CompilerStack::analyze()
 
 		if (noErrors)
 		{
-			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerEngine, m_readFile, m_enabledSMTSolvers);
+			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers);
 			for (Source const* source: m_sourceOrder)
 				if (source->ast)
 					modelChecker.analyze(*source->ast);

libsolidity/interface/CompilerStack.h

@@ -167,8 +167,8 @@ public:
 	/// Must be set before parsing.
 	void setEVMVersion(langutil::EVMVersion _version = langutil::EVMVersion{});
 
-	/// Set which model checking engines should be used.
-	void setModelCheckerEngine(ModelCheckerEngine _engine);
+	/// Set model checker settings.
+	void setModelCheckerSettings(ModelCheckerSettings _settings);
 	/// Set which SMT solvers should be enabled.
 	void setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSolvers);
 
@@ -456,7 +456,7 @@ private:
 	RevertStrings m_revertStrings = RevertStrings::Default;
 	State m_stopAfter = State::CompilationSuccessful;
 	langutil::EVMVersion m_evmVersion;
-	ModelCheckerEngine m_modelCheckerEngine;
+	ModelCheckerSettings m_modelCheckerSettings;
 	smtutil::SMTSolverChoice m_enabledSMTSolvers;
 	std::map<std::string, std::set<std::string>> m_requestedContractNames;
 	bool m_generateEvmBytecode = true;

libsolidity/interface/StandardCompiler.cpp

@@ -420,7 +420,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"engine"};
+	static set<string> keys{"engine", "timeout"};
 	return checkKeys(_input, keys, "modelCheckerSettings");
 }
 
@@ -885,7 +885,14 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		std::optional<ModelCheckerEngine> engine = ModelCheckerEngine::fromString(modelCheckerSettings["engine"].asString());
 		if (!engine)
 			return formatFatalError("JSONError", "Invalid model checker engine requested.");
-		ret.modelCheckerEngine = *engine;
+		ret.modelCheckerSettings.engine = *engine;
+	}
+
+	if (modelCheckerSettings.isMember("timeout"))
+	{
+		if (!modelCheckerSettings["timeout"].isUInt())
+			return formatFatalError("JSONError", "modelCheckerSettings.timeout must be an unsigned integer.");
+		ret.modelCheckerSettings.timeout = modelCheckerSettings["timeout"].asUInt();
 	}
 
 	return { std::move(ret) };
@@ -908,7 +915,7 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 	compilerStack.useMetadataLiteralSources(_inputsAndSettings.metadataLiteralSources);
 	compilerStack.setMetadataHash(_inputsAndSettings.metadataHash);
 	compilerStack.setRequestedContractNames(requestedContractNames(_inputsAndSettings.outputSelection));
-	compilerStack.setModelCheckerEngine(_inputsAndSettings.modelCheckerEngine);
+	compilerStack.setModelCheckerSettings(_inputsAndSettings.modelCheckerSettings);
 
 	compilerStack.enableEvmBytecodeGeneration(isEvmBytecodeRequested(_inputsAndSettings.outputSelection));
 	compilerStack.enableIRGeneration(isIRRequested(_inputsAndSettings.outputSelection));

libsolidity/interface/StandardCompiler.h

@@ -71,7 +71,7 @@ private:
 		bool metadataLiteralSources = false;
 		CompilerStack::MetadataHash metadataHash = CompilerStack::MetadataHash::IPFS;
 		Json::Value outputSelection;
-		ModelCheckerEngine modelCheckerEngine = ModelCheckerEngine::All();
+		ModelCheckerSettings modelCheckerSettings = ModelCheckerSettings{};
 	};
 
 	/// Parses the input json (and potentially invokes the read callback) and either returns