Merge pull request #9388 from ethereum/develop

Merge develop into breaking.

libsolidity/analysis/StaticAnalyzer.cpp

@@ -155,29 +155,6 @@ bool StaticAnalyzer::visit(VariableDeclaration const& _variable)
 			// This is not a no-op, the entry might pre-exist.
 			m_localVarUseCount[make_pair(_variable.id(), &_variable)] += 0;
 	}
-	else if (_variable.isStateVariable())
-	{
-		set<StructDefinition const*> structsSeen;
-		TypeSet oversizedSubTypes;
-		if (structureSizeEstimate(*_variable.type(), structsSeen, oversizedSubTypes) >= bigint(1) << 64)
-			m_errorReporter.warning(
-				3408_error,
-				_variable.location(),
-				"Variable " + util::escapeAndQuoteString(_variable.name()) +
-				" covers a large part of storage and thus makes collisions likely. "
-				"Either use mappings or dynamic arrays and allow their size to be increased only "
-				"in small quantities per transaction."
-			);
-		for (Type const* type: oversizedSubTypes)
-			m_errorReporter.warning(
-				7325_error,
-				_variable.location(),
-				"Type " + util::escapeAndQuoteString(type->canonicalName()) +
-				" has large size and thus makes collisions likely. "
-				"Either use mappings or dynamic arrays and allow their size to be increased only "
-				"in small quantities per transaction."
-			);
-	}
 	return true;
 }
 
@@ -349,47 +326,3 @@ bool StaticAnalyzer::visit(FunctionCall const& _functionCall)
 	}
 	return true;
 }
-
-bigint StaticAnalyzer::structureSizeEstimate(
-	Type const& _type,
-	set<StructDefinition const*>& _structsSeen,
-	TypeSet& _oversizedSubTypes
-)
-{
-	switch (_type.category())
-	{
-	case Type::Category::Array:
-	{
-		auto const& t = dynamic_cast<ArrayType const&>(_type);
-		bigint baseTypeSize = structureSizeEstimate(*t.baseType(), _structsSeen, _oversizedSubTypes);
-		if (baseTypeSize >= bigint(1) << 64)
-			_oversizedSubTypes.insert(t.baseType());
-		if (!t.isDynamicallySized())
-			return structureSizeEstimate(*t.baseType(), _structsSeen, _oversizedSubTypes) * t.length();
-		break;
-	}
-	case Type::Category::Struct:
-	{
-		auto const& t = dynamic_cast<StructType const&>(_type);
-		bigint size = 1;
-		if (_structsSeen.count(&t.structDefinition()))
-			return size;
-		_structsSeen.insert(&t.structDefinition());
-		for (auto const& m: t.members(nullptr))
-			size += structureSizeEstimate(*m.type, _structsSeen, _oversizedSubTypes);
-		_structsSeen.erase(&t.structDefinition());
-		return size;
-	}
-	case Type::Category::Mapping:
-	{
-		auto const* valueType = dynamic_cast<MappingType const&>(_type).valueType();
-		bigint valueTypeSize = structureSizeEstimate(*valueType, _structsSeen, _oversizedSubTypes);
-		if (valueTypeSize >= bigint(1) << 64)
-			_oversizedSubTypes.insert(valueType);
-		break;
-	}
-	default:
-		break;
-	}
-	return bigint(1);
-}

libsolidity/analysis/StaticAnalyzer.h

@@ -73,23 +73,6 @@ private:
 	bool visit(BinaryOperation const& _operation) override;
 	bool visit(FunctionCall const& _functionCall) override;
 
-	struct TypeComp
-	{
-		bool operator()(Type const* lhs, Type const* rhs) const
-		{
-			solAssert(lhs && rhs, "");
-			return lhs->richIdentifier() < rhs->richIdentifier();
-		}
-	};
-	using TypeSet = std::set<Type const*, TypeComp>;
-
-	/// @returns the size of this type in storage, including all sub-types.
-	static bigint structureSizeEstimate(
-		Type const& _type,
-		std::set<StructDefinition const*>& _structsSeen,
-		TypeSet& _oversizedSubTypes
-	);
-
 	langutil::ErrorReporter& m_errorReporter;
 
 	/// Flag that indicates whether the current contract definition is a library.

libsolidity/analysis/TypeChecker.cpp

@@ -36,6 +36,7 @@
 
 #include <boost/algorithm/string/join.hpp>
 #include <boost/algorithm/string/predicate.hpp>
+#include <boost/range/adaptor/reversed.hpp>
 
 #include <memory>
 #include <vector>
@@ -91,6 +92,20 @@ bool TypeChecker::visit(ContractDefinition const& _contract)
 	for (auto const& n: _contract.subNodes())
 		n->accept(*this);
 
+	bigint size = 0;
+	vector<VariableDeclaration const*> variables;
+	for (ContractDefinition const* contract: boost::adaptors::reverse(m_currentContract->annotation().linearizedBaseContracts))
+		for (VariableDeclaration const* variable: contract->stateVariables())
+			if (!(variable->isConstant() || variable->immutable()))
+			{
+				size += storageSizeUpperBound(*(variable->annotation().type));
+				if (size >= bigint(1) << 256)
+				{
+					m_errorReporter.typeError(7676_error, m_currentContract->location(), "Contract too large for storage.");
+					break;
+				}
+			}
+
 	return false;
 }
 
@@ -555,6 +570,10 @@ bool TypeChecker::visit(VariableDeclaration const& _variable)
 			m_errorReporter.typeError(6744_error, _variable.location(), "Internal or recursive type is not allowed for public state variables.");
 	}
 
+	bool isStructMemberDeclaration = dynamic_cast<StructDefinition const*>(_variable.scope()) != nullptr;
+	if (isStructMemberDeclaration)
+		return false;
+
 	if (auto referenceType = dynamic_cast<ReferenceType const*>(varType))
 	{
 		auto result = referenceType->validForLocation(referenceType->location());
@@ -564,9 +583,33 @@ bool TypeChecker::visit(VariableDeclaration const& _variable)
 		{
 			solAssert(!result.message().empty(), "Expected detailed error message");
 			m_errorReporter.typeError(1534_error, _variable.location(), result.message());
+			return false;
 		}
 	}
 
+	if (varType->dataStoredIn(DataLocation::Storage))
+	{
+		auto collisionMessage = [&](string const& variableOrType, bool isVariable) -> string {
+			return
+				(isVariable ? "Variable " : "Type ") +
+				util::escapeAndQuoteString(variableOrType) +
+				" covers a large part of storage and thus makes collisions likely."
+				" Either use mappings or dynamic arrays and allow their size to be increased only"
+				" in small quantities per transaction.";
+		};
+
+		if (storageSizeUpperBound(*varType) >= bigint(1) << 64)
+		{
+			if (_variable.isStateVariable())
+				m_errorReporter.warning(3408_error, _variable.location(), collisionMessage(_variable.name(), true));
+			else
+				m_errorReporter.warning(2332_error, _variable.typeName()->location(), collisionMessage(varType->canonicalName(), false));
+		}
+		vector<Type const*> oversizedSubtypes = frontend::oversizedSubtypes(*varType);
+		for (Type const* subtype: oversizedSubtypes)
+			m_errorReporter.warning(7325_error, _variable.typeName()->location(), collisionMessage(subtype->canonicalName(), false));
+	}
+
 	return false;
 }
 

libsolidity/ast/Types.cpp

@@ -53,6 +53,88 @@ using namespace solidity::frontend;
 namespace
 {
 
+struct TypeComp
+{
+	bool operator()(Type const* lhs, Type const* rhs) const
+	{
+		solAssert(lhs && rhs, "");
+		return lhs->richIdentifier() < rhs->richIdentifier();
+	}
+};
+using TypeSet = std::set<Type const*, TypeComp>;
+
+bigint storageSizeUpperBoundInner(
+	Type const& _type,
+	set<StructDefinition const*>& _structsSeen
+)
+{
+	switch (_type.category())
+	{
+	case Type::Category::Array:
+	{
+		auto const& t = dynamic_cast<ArrayType const&>(_type);
+		if (!t.isDynamicallySized())
+			return storageSizeUpperBoundInner(*t.baseType(), _structsSeen) * t.length();
+		break;
+	}
+	case Type::Category::Struct:
+	{
+		auto const& t = dynamic_cast<StructType const&>(_type);
+		solAssert(!_structsSeen.count(&t.structDefinition()), "Recursive struct.");
+		bigint size = 1;
+		_structsSeen.insert(&t.structDefinition());
+		for (auto const& m: t.members(nullptr))
+			size += storageSizeUpperBoundInner(*m.type, _structsSeen);
+		_structsSeen.erase(&t.structDefinition());
+		return size;
+	}
+	default:
+		break;
+	}
+	return bigint(1);
+}
+
+void oversizedSubtypesInner(
+	Type const& _type,
+	bool _includeType,
+	set<StructDefinition const*>& _structsSeen,
+	TypeSet& _oversizedSubtypes
+)
+{
+	switch (_type.category())
+	{
+	case Type::Category::Array:
+	{
+		auto const& t = dynamic_cast<ArrayType const&>(_type);
+		if (_includeType && storageSizeUpperBound(t) >= bigint(1) << 64)
+			_oversizedSubtypes.insert(&t);
+		oversizedSubtypesInner(*t.baseType(), t.isDynamicallySized(), _structsSeen, _oversizedSubtypes);
+		break;
+	}
+	case Type::Category::Struct:
+	{
+		auto const& t = dynamic_cast<StructType const&>(_type);
+		if (_structsSeen.count(&t.structDefinition()))
+			return;
+		if (_includeType && storageSizeUpperBound(t) >= bigint(1) << 64)
+			_oversizedSubtypes.insert(&t);
+		_structsSeen.insert(&t.structDefinition());
+		for (auto const& m: t.members(nullptr))
+			oversizedSubtypesInner(*m.type, false, _structsSeen, _oversizedSubtypes);
+		_structsSeen.erase(&t.structDefinition());
+		break;
+	}
+	case Type::Category::Mapping:
+	{
+		auto const* valueType = dynamic_cast<MappingType const&>(_type).valueType();
+		oversizedSubtypesInner(*valueType, true, _structsSeen, _oversizedSubtypes);
+		break;
+	}
+	default:
+		break;
+	}
+}
+
 /// Check whether (_base ** _exp) fits into 4096 bits.
 bool fitsPrecisionExp(bigint const& _base, bigint const& _exp)
 {
@@ -149,6 +231,22 @@ util::Result<TypePointers> transformParametersToExternal(TypePointers const& _pa
 
 }
 
+bigint solidity::frontend::storageSizeUpperBound(frontend::Type const& _type)
+{
+	set<StructDefinition const*> structsSeen;
+	return storageSizeUpperBoundInner(_type, structsSeen);
+}
+
+vector<frontend::Type const*> solidity::frontend::oversizedSubtypes(frontend::Type const& _type)
+{
+	set<StructDefinition const*> structsSeen;
+	TypeSet oversized;
+	oversizedSubtypesInner(_type, false, structsSeen, oversized);
+	vector<frontend::Type const*> res;
+	copy(oversized.cbegin(), oversized.cend(), back_inserter(res));
+	return res;
+}
+
 void Type::clearCache() const
 {
 	m_members.clear();
@@ -1775,6 +1873,8 @@ BoolResult ArrayType::validForLocation(DataLocation _loc) const
 			break;
 		}
 		case DataLocation::Storage:
+			if (storageSizeUpperBound(*this) >= bigint(1) << 256)
+				return BoolResult::err("Type too large for storage.");
 			break;
 	}
 	return true;
@@ -2461,6 +2561,13 @@ BoolResult StructType::validForLocation(DataLocation _loc) const
 			if (!result)
 				return result;
 		}
+
+	if (
+		_loc == DataLocation::Storage &&
+		storageSizeUpperBound(*this) >= bigint(1) << 256
+	)
+		return BoolResult::err("Type too large for storage.");
+
 	return true;
 }
 

libsolidity/ast/Types.h

@@ -54,6 +54,14 @@ using rational = boost::rational<bigint>;
 using TypeResult = util::Result<TypePointer>;
 using BoolResult = util::Result<bool>;
 
+}
+
+namespace solidity::frontend
+{
+
+bigint storageSizeUpperBound(frontend::Type const& _type);
+std::vector<frontend::Type const*> oversizedSubtypes(frontend::Type const& _type);
+
 inline rational makeRational(bigint const& _numerator, bigint const& _denominator)
 {
 	solAssert(_denominator != 0, "division by zero");

libsolidity/codegen/ContractCompiler.cpp

@@ -646,7 +646,7 @@ bool ContractCompiler::visit(FunctionDefinition const& _function)
 		}
 		else
 		{
-			m_context << swapInstruction(stackLayout.size() - static_cast<size_t>(stackLayout.back()) - 1);
+			m_context << swapInstruction(stackLayout.size() - static_cast<unsigned>(stackLayout.back()) - 1u);
 			swap(stackLayout[static_cast<size_t>(stackLayout.back())], stackLayout.back());
 		}
 	for (size_t i = 0; i < stackLayout.size(); ++i)

libsolidity/formal/BMC.cpp

@@ -52,11 +52,11 @@ BMC::BMC(
 #endif
 }
 
-void BMC::analyze(SourceUnit const& _source, set<Expression const*> _safeAssertions)
+void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTarget::Type>> _solvedTargets)
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
-	m_safeAssertions += move(_safeAssertions);
+	m_solvedTargets = move(_solvedTargets);
 	m_context.setSolver(m_interface.get());
 	m_context.clear();
 	m_context.setAssertionAccumulation(true);
@@ -684,16 +684,22 @@ void BMC::checkBalance(BMCVerificationTarget& _target)
 void BMC::checkAssert(BMCVerificationTarget& _target)
 {
 	solAssert(_target.type == VerificationTarget::Type::Assert, "");
-	if (!m_safeAssertions.count(_target.expression))
-		checkCondition(
-			_target.constraints && !_target.value,
-			_target.callStack,
-			_target.modelExpressions,
-			_target.expression->location(),
-			4661_error,
-			7812_error,
-			"Assertion violation"
-		);
+
+	if (
+		m_solvedTargets.count(_target.expression) &&
+		m_solvedTargets.at(_target.expression).count(_target.type)
+	)
+		return;
+
+	checkCondition(
+		_target.constraints && !_target.value,
+		_target.callStack,
+		_target.modelExpressions,
+		_target.expression->location(),
+		4661_error,
+		7812_error,
+		"Assertion violation"
+	);
 }
 
 void BMC::addVerificationTarget(

libsolidity/formal/BMC.h

@@ -63,7 +63,7 @@ public:
 		smtutil::SMTSolverChoice _enabledSolvers
 	);
 
-	void analyze(SourceUnit const& _sources, std::set<Expression const*> _safeAssertions);
+	void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTarget::Type>> _solvedTargets);
 
 	/// This is used if the SMT solver is not directly linked into this binary.
 	/// @returns a list of inputs to the SMT solver that were not part of the argument to
@@ -180,8 +180,8 @@ private:
 
 	std::vector<BMCVerificationTarget> m_verificationTargets;
 
-	/// Assertions that are known to be safe.
-	std::set<Expression const*> m_safeAssertions;
+	/// Targets that were already proven.
+	std::map<ASTNode const*, std::set<VerificationTarget::Type>> m_solvedTargets;
 };
 
 }

libsolidity/formal/CHC.cpp

@@ -96,48 +96,7 @@ void CHC::analyze(SourceUnit const& _source)
 	for (auto const* source: sources)
 		source->accept(*this);
 
-	for (auto const& [scope, target]: m_verificationTargets)
-	{
-		if (target.type == VerificationTarget::Type::Assert)
-		{
-			auto assertions = transactionAssertions(scope);
-			for (auto const* assertion: assertions)
-			{
-				createErrorBlock();
-				connectBlocks(target.value, error(), target.constraints && (target.errorId == static_cast<size_t>(assertion->id())));
-				auto [result, model] = query(error(), assertion->location());
-				// This should be fine but it's a bug in the old compiler
-				(void)model;
-				if (result == smtutil::CheckResult::UNSATISFIABLE)
-					m_safeAssertions.insert(assertion);
-			}
-		}
-		else if (target.type == VerificationTarget::Type::PopEmptyArray)
-		{
-			solAssert(dynamic_cast<FunctionCall const*>(scope), "");
-			createErrorBlock();
-			connectBlocks(target.value, error(), target.constraints && (target.errorId == static_cast<size_t>(scope->id())));
-			auto [result, model] = query(error(), scope->location());
-			// This should be fine but it's a bug in the old compiler
-			(void)model;
-			if (result != smtutil::CheckResult::UNSATISFIABLE)
-			{
-				string msg = "Empty array \"pop\" ";
-				if (result == smtutil::CheckResult::SATISFIABLE)
-					msg += "detected here.";
-				else
-					msg += "might happen here.";
-				m_unsafeTargets.insert(scope);
-				m_outerErrorReporter.warning(
-					2529_error,
-					scope->location(),
-					msg
-				);
-			}
-		}
-		else
-			solAssert(false, "");
-	}
+	checkVerificationTargets();
 }
 
 vector<string> CHC::unhandledQueries() const
@@ -540,7 +499,7 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 		m_currentBlock,
 		m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction),
 		currentPathConditions() && !m_context.expression(*args.front())->currentValue() && (
-			m_error.currentValue() == static_cast<size_t>(_funCall.id())
+			m_error.currentValue() == newErrorId(_funCall)
 		)
 	);
 
@@ -638,7 +597,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
 	connectBlocks(
 		m_currentBlock,
 		m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction),
-		currentPathConditions() && symbArray->length() <= 0 && m_error.currentValue() == static_cast<size_t>(_arrayPop.id())
+		currentPathConditions() && symbArray->length() <= 0 && m_error.currentValue() == newErrorId(_arrayPop)
 	);
 
 	m_context.addAssertion(m_error.currentValue() == previousError);
@@ -647,9 +606,10 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
 void CHC::resetSourceAnalysis()
 {
 	m_verificationTargets.clear();
-	m_safeAssertions.clear();
+	m_safeTargets.clear();
 	m_unsafeTargets.clear();
 	m_functionAssertions.clear();
+	m_errorIds.clear();
 	m_callGraph.clear();
 	m_summaries.clear();
 }
@@ -990,13 +950,13 @@ vector<smtutil::Expression> CHC::initialStateVariables(ContractDefinition const&
 	return stateVariablesAtIndex(0, _contract);
 }
 
-vector<smtutil::Expression> CHC::stateVariablesAtIndex(int _index)
+vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index)
 {
 	solAssert(m_currentContract, "");
 	return stateVariablesAtIndex(_index, *m_currentContract);
 }
 
-vector<smtutil::Expression> CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract)
+vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract)
 {
 	return applyMap(
 		stateVariablesIncludingInheritedAndPrivate(_contract),
@@ -1167,7 +1127,98 @@ void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smtutil::Expressi
 	}
 }
 
+void CHC::checkVerificationTargets()
+{
+	for (auto const& [scope, target]: m_verificationTargets)
+	{
+		if (target.type == VerificationTarget::Type::Assert)
+			checkAssertTarget(scope, target);
+		else
+		{
+			string satMsg;
+			string unknownMsg;
+
+			if (target.type == VerificationTarget::Type::PopEmptyArray)
+			{
+				solAssert(dynamic_cast<FunctionCall const*>(scope), "");
+				satMsg = "Empty array \"pop\" detected here.";
+				unknownMsg = "Empty array \"pop\" might happen here.";
+			}
+			else
+				solAssert(false, "");
+
+			auto it = m_errorIds.find(scope->id());
+			solAssert(it != m_errorIds.end(), "");
+			checkAndReportTarget(scope, target, it->second, satMsg, unknownMsg);
+		}
+	}
+}
+
+void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const& _target)
+{
+	solAssert(_target.type == VerificationTarget::Type::Assert, "");
+	auto assertions = transactionAssertions(_scope);
+	for (auto const* assertion: assertions)
+	{
+		auto it = m_errorIds.find(assertion->id());
+		solAssert(it != m_errorIds.end(), "");
+		unsigned errorId = it->second;
+
+		createErrorBlock();
+		connectBlocks(_target.value, error(), _target.constraints && (_target.errorId == errorId));
+		auto [result, model] = query(error(), assertion->location());
+		// This should be fine but it's a bug in the old compiler
+		(void)model;
+		if (result == smtutil::CheckResult::UNSATISFIABLE)
+			m_safeTargets[assertion].insert(_target.type);
+	}
+}
+
+void CHC::checkAndReportTarget(
+	ASTNode const* _scope,
+	CHCVerificationTarget const& _target,
+	unsigned _errorId,
+	string _satMsg,
+	string _unknownMsg
+)
+{
+	createErrorBlock();
+	connectBlocks(_target.value, error(), _target.constraints && (_target.errorId == _errorId));
+	auto [result, model] = query(error(), _scope->location());
+	// This should be fine but it's a bug in the old compiler
+	(void)model;
+	if (result == smtutil::CheckResult::UNSATISFIABLE)
+		m_safeTargets[_scope].insert(_target.type);
+	else if (result == smtutil::CheckResult::SATISFIABLE)
+	{
+		solAssert(!_satMsg.empty(), "");
+		m_unsafeTargets[_scope].insert(_target.type);
+		m_outerErrorReporter.warning(
+			2529_error,
+			_scope->location(),
+			_satMsg
+		);
+	}
+	else if (!_unknownMsg.empty())
+		m_outerErrorReporter.warning(
+			1147_error,
+			_scope->location(),
+			_unknownMsg
+		);
+}
+
 string CHC::uniquePrefix()
 {
 	return to_string(m_blockCounter++);
 }
+
+unsigned CHC::newErrorId(frontend::Expression const& _expr)
+{
+	unsigned errorId = m_context.newUniqueId();
+	// We need to make sure the error id is not zero,
+	// because error id zero actually means no error in the CHC encoding.
+	if (errorId == 0)
+		errorId = m_context.newUniqueId();
+	m_errorIds.emplace(_expr.id(), errorId);
+	return errorId;
+}

libsolidity/formal/CHC.h

@@ -36,6 +36,7 @@
 
 #include <libsmtutil/CHCSolverInterface.h>
 
+#include <map>
 #include <set>
 
 namespace solidity::frontend
@@ -54,7 +55,8 @@ public:
 
 	void analyze(SourceUnit const& _sources);
 
-	std::set<Expression const*> const& safeAssertions() const { return m_safeAssertions; }
+	std::map<ASTNode const*, std::set<VerificationTarget::Type>> const& safeTargets() const { return m_safeTargets; }
+	std::map<ASTNode const*, std::set<VerificationTarget::Type>> const& unsafeTargets() const { return m_unsafeTargets; }
 
 	/// This is used if the Horn solver is not directly linked into this binary.
 	/// @returns a list of inputs to the Horn solver that were not part of the argument to
@@ -152,8 +154,8 @@ private:
 	/// of the current transaction.
 	std::vector<smtutil::Expression> initialStateVariables();
 	std::vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract);
-	std::vector<smtutil::Expression> stateVariablesAtIndex(int _index);
-	std::vector<smtutil::Expression> stateVariablesAtIndex(int _index, ContractDefinition const& _contract);
+	std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index);
+	std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract);
 	/// @returns the current symbolic values of the current state variables.
 	std::vector<smtutil::Expression> currentStateVariables();
 	std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract);
@@ -191,6 +193,18 @@ private:
 	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
 	void addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
 	void addArrayPopVerificationTarget(ASTNode const* _scope, smtutil::Expression _errorId);
+
+	void checkVerificationTargets();
+	// Forward declaration. Definition is below.
+	struct CHCVerificationTarget;
+	void checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const& _target);
+	void checkAndReportTarget(
+		ASTNode const* _scope,
+		CHCVerificationTarget const& _target,
+		unsigned _errorId,
+		std::string _satMsg,
+		std::string _unknownMsg
+	);
 	//@}
 
 	/// Misc.
@@ -198,6 +212,10 @@ private:
 	/// Returns a prefix to be used in a new unique block name
 	/// and increases the block counter.
 	std::string uniquePrefix();
+
+	/// @returns a new unique error id associated with _expr and stores
+	/// it into m_errorIds.
+	unsigned newErrorId(Expression const& _expr);
 	//@}
 
 	/// Predicates.
@@ -257,10 +275,10 @@ private:
 
 	std::map<ASTNode const*, CHCVerificationTarget, IdCompare> m_verificationTargets;
 
-	/// Assertions proven safe.
-	std::set<Expression const*> m_safeAssertions;
+	/// Targets proven safe.
+	std::map<ASTNode const*, std::set<VerificationTarget::Type>> m_safeTargets;
 	/// Targets proven unsafe.
-	std::set<ASTNode const*> m_unsafeTargets;
+	std::map<ASTNode const*, std::set<VerificationTarget::Type>> m_unsafeTargets;
 	//@}
 
 	/// Control-flow.
@@ -271,6 +289,11 @@ private:
 
 	std::map<ASTNode const*, std::set<Expression const*>, IdCompare> m_functionAssertions;
 
+	/// Maps ASTNode ids to error ids.
+	/// A multimap is used instead of map anticipating the UnderOverflow
+	/// target which has 2 error ids.
+	std::multimap<unsigned, unsigned> m_errorIds;
+
 	/// The current block.
 	smtutil::Expression m_currentBlock = smtutil::Expression(true);
 

libsolidity/formal/EncodingContext.cpp

@@ -32,21 +32,21 @@ EncodingContext::EncodingContext():
 void EncodingContext::reset()
 {
 	resetAllVariables();
-	resetSlackId();
+	resetUniqueId();
 	m_expressions.clear();
 	m_globalContext.clear();
 	m_state.reset();
 	m_assertions.clear();
 }
 
-void EncodingContext::resetSlackId()
+void EncodingContext::resetUniqueId()
 {
-	m_nextSlackId = 0;
+	m_nextUniqueId = 0;
 }
 
-unsigned EncodingContext::newSlackId()
+unsigned EncodingContext::newUniqueId()
 {
-	return m_nextSlackId++;
+	return m_nextUniqueId++;
 }
 
 void EncodingContext::clear()

libsolidity/formal/EncodingContext.h

@@ -41,9 +41,9 @@ public:
 	/// To be used in the beginning of a root function visit.
 	void reset();
 	/// Resets the fresh id for slack variables.
-	void resetSlackId();
+	void resetUniqueId();
 	/// Returns the current fresh slack id and increments it.
-	unsigned newSlackId();
+	unsigned newUniqueId();
 	/// Clears the entire context, erasing everything.
 	/// To be used before a model checking engine starts.
 	void clear();
@@ -173,8 +173,8 @@ private:
 	bool m_accumulateAssertions = true;
 	//@}
 
-	/// Fresh ids for slack variables to be created deterministically.
-	unsigned m_nextSlackId = 0;
+	/// Central source of unique ids.
+	unsigned m_nextUniqueId = 0;
 };
 
 }

libsolidity/formal/ModelChecker.cpp

@@ -41,7 +41,12 @@ void ModelChecker::analyze(SourceUnit const& _source)
 		return;
 
 	m_chc.analyze(_source);
-	m_bmc.analyze(_source, m_chc.safeAssertions());
+
+	auto solvedTargets = m_chc.safeTargets();
+	for (auto const& target: m_chc.unsafeTargets())
+		solvedTargets[target.first] += target.second;
+
+	m_bmc.analyze(_source, solvedTargets);
 }
 
 vector<string> ModelChecker::unhandledQueries()

libsolidity/formal/SMTEncoder.cpp

@@ -1253,7 +1253,7 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 		// - RHS is -1
 		// the result is then -(type.min), which wraps back to type.min
 		smtutil::Expression maxLeft = _left == smt::minValue(*intType);
-		smtutil::Expression minusOneRight = _right == -1;
+		smtutil::Expression minusOneRight = _right == numeric_limits<size_t >::max();
 		smtutil::Expression wrap = smtutil::Expression::ite(maxLeft && minusOneRight, smt::minValue(*intType), valueUnbounded);
 		return {wrap, valueUnbounded};
 	}
@@ -1262,7 +1262,7 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 	auto symbMax = smt::maxValue(*intType);
 
 	smtutil::Expression intValueRange = (0 - symbMin) + symbMax + 1;
-	string suffix = to_string(_operation.id()) + "_" + to_string(m_context.newSlackId());
+	string suffix = to_string(_operation.id()) + "_" + to_string(m_context.newUniqueId());
 	smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context);
 	smt::SymbolicIntVariable m(intType, intType, "m_" + suffix, m_context);