[SMTChecker] More precise creation of verification targets.

Changelog.md

@@ -10,6 +10,8 @@ Bugfixes:
  * SMTChecker: Fix internal error on conversion from string literal to byte.
  * SMTChecker: Fix internal error when using tuples of rational literals inside the conditional operator.
  * SMTChecker: Fix internal error when assigning state variable via contract's name.
+ * SMTChecker: Fix incorrect counterexamples reported by the CHC engine.
+ * SMTChecker: Fix false negative in modifier applied multiple times.
  * Code generator: Fix missing creation dependency tracking for abstract contracts.
 
 

docs/security-considerations.rst

@@ -620,26 +620,32 @@ types.
 
     // SPDX-License-Identifier: GPL-3.0
     pragma solidity >=0.5.0;
+    pragma experimental ABIEncoderV2;
     pragma experimental SMTChecker;
     // This will report a warning
 
     contract Aliasing
     {
-        uint[] array;
+        uint[] array1;
+        uint[][] array2;
         function f(
             uint[] memory a,
             uint[] memory b,
             uint[][] memory c,
             uint[] storage d
-        ) internal view {
+        ) internal {
-            require(array[0] == 42);
+            array1[0] = 42;
-            require(a[0] == 2);
+            a[0] = 2;
-            require(c[0][0] == 2);
+            c[0][0] = 2;
-            require(d[0] == 2);
             b[0] = 1;
             // Erasing knowledge about memory references should not
             // erase knowledge about state variables.
-            assert(array[0] == 42);
+            assert(array1[0] == 42);
+            // However, an assignment to a storage reference will erase
+            // storage knowledge accordingly.
+            d[0] = 2;
+            // Fails as false positive because of the assignment above.
+            assert(array1[0] == 42);
             // Fails because `a == b` is possible.
             assert(a[0] == 2);
             // Fails because `c[i] == b` is possible.
@@ -647,6 +653,14 @@ types.
             assert(d[0] == 2);
             assert(b[0] == 1);
         }
+        function g(
+            uint[] memory a,
+            uint[] memory b,
+            uint[][] memory c,
+            uint x
+        ) public {
+            f(a, b, c, array2[x]);
+        }
     }
 
 After the assignment to ``b[0]``, we need to clear knowledge about ``a`` since

libsolidity/formal/CHC.cpp

@@ -134,7 +134,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
 
 	setCurrentBlock(*m_constructorSummaryPredicate);
 
-	addAssertVerificationTarget(m_currentContract, m_currentBlock, smtutil::Expression(true), errorFlag().currentValue());
+	m_queryPlaceholders[&_contract].push_back({smtutil::Expression(true), errorFlag().currentValue(), m_currentBlock});
 	connectBlocks(m_currentBlock, interface(), errorFlag().currentValue() == 0);
 
 	SMTEncoder::endVisit(_contract);
@@ -231,16 +231,14 @@ void CHC::endVisit(FunctionDefinition const& _function)
 			auto assertionError = errorFlag().currentValue();
 			auto sum = summary(_function);
 			connectBlocks(m_currentBlock, sum);
-
 			auto iface = interface();
-
 			setCurrentBlock(*m_interfaces.at(m_currentContract));
 
 			auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
 			if (_function.isPublic())
 			{
 				auto txConstraints = m_context.state().txConstraints(_function);
-				addAssertVerificationTarget(&_function, ifacePre, txConstraints && sum, assertionError);
+				m_queryPlaceholders[&_function].push_back({txConstraints && sum, assertionError, ifacePre});
 				connectBlocks(ifacePre, iface, txConstraints && sum && (assertionError == 0));
 			}
 		}
@@ -512,30 +510,15 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 
 	solAssert(m_currentContract, "");
 	solAssert(m_currentFunction, "");
-	if (m_currentFunction->isConstructor())
+	auto errorCondition = !m_context.expression(*args.front())->currentValue();
-		m_functionAssertions[m_currentContract].insert(&_funCall);
+	verificationTargetEncountered(&_funCall, VerificationTarget::Type::Assert, errorCondition);
-	else
-		m_functionAssertions[m_currentFunction].insert(&_funCall);
-
-	auto previousError = errorFlag().currentValue();
-	errorFlag().increaseIndex();
-
-	connectBlocks(
-		m_currentBlock,
-		m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction),
-		currentPathConditions() && !m_context.expression(*args.front())->currentValue() && (
-			errorFlag().currentValue() == newErrorId(_funCall)
-		)
-	);
-
-	m_context.addAssertion(errorFlag().currentValue() == previousError);
 }
 
 void CHC::visitAddMulMod(FunctionCall const& _funCall)
 {
 	solAssert(_funCall.arguments().at(2), "");
 
-	addVerificationTarget(_funCall, VerificationTarget::Type::DivByZero, expr(*_funCall.arguments().at(2)) == 0);
+	verificationTargetEncountered(&_funCall, VerificationTarget::Type::DivByZero, expr(*_funCall.arguments().at(2)) == 0);
 
 	SMTEncoder::visitAddMulMod(_funCall);
 }
@@ -634,7 +617,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
 	auto symbArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
 	solAssert(symbArray, "");
 
-	addVerificationTarget(_arrayPop, VerificationTarget::Type::PopEmptyArray, symbArray->length() <= 0);
+	verificationTargetEncountered(&_arrayPop, VerificationTarget::Type::PopEmptyArray, symbArray->length() <= 0);
 }
 
 pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
@@ -646,7 +629,7 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 )
 {
 	if (_op == Token::Mod || _op == Token::Div)
-		addVerificationTarget(_expression, VerificationTarget::Type::DivByZero, _right == 0);
+		verificationTargetEncountered(&_expression, VerificationTarget::Type::DivByZero, _right == 0);
 
 	auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
 
@@ -662,16 +645,16 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 		return values;
 
 	if (_op == Token::Div)
-		addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
+		verificationTargetEncountered(&_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
 	else if (intType->isSigned())
 	{
-		addVerificationTarget(_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
+		verificationTargetEncountered(&_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
-		addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
+		verificationTargetEncountered(&_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
 	}
 	else if (_op == Token::Sub)
-		addVerificationTarget(_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
+		verificationTargetEncountered(&_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
 	else if (_op == Token::Add || _op == Token::Mul)
-		addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
+		verificationTargetEncountered(&_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
 	else
 		solAssert(false, "");
 	return values;
@@ -679,11 +662,11 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 
 void CHC::resetSourceAnalysis()
 {
-	m_verificationTargets.clear();
 	m_safeTargets.clear();
 	m_unsafeTargets.clear();
-	m_functionAssertions.clear();
+	m_functionTargetIds.clear();
-	m_errorIds.clear();
+	m_verificationTargets.clear();
+	m_queryPlaceholders.clear();
 	m_callGraph.clear();
 	m_summaries.clear();
 	m_interfaces.clear();
@@ -713,6 +696,7 @@ void CHC::resetSourceAnalysis()
 	}
 
 	m_context.clear();
+	m_context.resetUniqueId();
 	m_context.setAssertionAccumulation(false);
 }
 
@@ -759,15 +743,15 @@ void CHC::setCurrentBlock(Predicate const& _block)
 	m_currentBlock = predicate(_block);
 }
 
-set<frontend::Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTNode const* _txRoot)
+set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot)
 {
-	set<Expression const*, IdCompare> assertions;
+	set<unsigned> verificationTargetsIds;
 	solidity::util::BreadthFirstSearch<ASTNode const*>{{_txRoot}}.run([&](auto const* function, auto&& _addChild) {
-		assertions.insert(m_functionAssertions[function].begin(), m_functionAssertions[function].end());
+		verificationTargetsIds.insert(m_functionTargetIds[function].begin(), m_functionTargetIds[function].end());
 		for (auto const* called: m_callGraph[function])
 		_addChild(called);
 	});
-	return assertions;
+	return verificationTargetsIds;
 }
 
 SortPointer CHC::sort(FunctionDefinition const& _function)
@@ -1101,186 +1085,171 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression c
 	return {result, cex};
 }
 
-void CHC::addVerificationTarget(
+void CHC::verificationTargetEncountered(
-	ASTNode const* _scope,
+	ASTNode const* const _errorNode,
 	VerificationTarget::Type _type,
-	smtutil::Expression _from,
+	smtutil::Expression const& _errorCondition
-	smtutil::Expression _constraints,
-	smtutil::Expression _errorId
 )
 {
 	solAssert(m_currentContract || m_currentFunction, "");
-	SourceUnit const* source = nullptr;
+	SourceUnit const* source = m_currentContract ? sourceUnitContaining(*m_currentContract) : sourceUnitContaining(*m_currentFunction);
-	if (m_currentContract)
-		source = sourceUnitContaining(*m_currentContract);
-	else
-		source = sourceUnitContaining(*m_currentFunction);
 	solAssert(source, "");
 	if (!source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		return;
 
-	m_verificationTargets[_scope].push_back(CHCVerificationTarget{{_type, _from, _constraints}, _errorId});
+	bool scopeIsFunction = m_currentFunction && !m_currentFunction->isConstructor();
-}
+	auto errorId = newErrorId();
-
+	solAssert(m_verificationTargets.count(errorId) == 0, "Error ID is not unique!");
-void CHC::addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _errorId)
+	m_verificationTargets.emplace(errorId, CHCVerificationTarget{{_type, _errorCondition, smtutil::Expression(true)}, errorId, _errorNode});
-{
+	if (scopeIsFunction)
-	solAssert(m_currentContract, "");
+		m_functionTargetIds[m_currentFunction].push_back(errorId);
-
-	if (!m_currentFunction || m_currentFunction->isConstructor())
-		addVerificationTarget(_scope, _type, summary(*m_currentContract), smtutil::Expression(true), _errorId);
 	else
-	{
+		m_functionTargetIds[m_currentContract].push_back(errorId);
-		auto iface = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
-		auto sum = summary(*m_currentFunction);
-		addVerificationTarget(_scope, _type, iface, sum, _errorId);
-	}
-}
-
-void CHC::addVerificationTarget(frontend::Expression const& _scope, VerificationTarget::Type _type, smtutil::Expression const& _target)
-{
 	auto previousError = errorFlag().currentValue();
 	errorFlag().increaseIndex();
-	addVerificationTarget(&_scope, _type, errorFlag().currentValue());
 
-	m_context.addAssertion(
+	// create an error edge to the summary
-		errorFlag().currentValue() == previousError ||
+	connectBlocks(
-		(_target && errorFlag().currentValue() == newErrorId(_scope))
+		m_currentBlock,
+		scopeIsFunction ? summary(*m_currentFunction) : summary(*m_currentContract),
+		currentPathConditions() && _errorCondition && errorFlag().currentValue() == errorId
 	);
-}
 
-void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId)
+	m_context.addAssertion(errorFlag().currentValue() == previousError);
-{
-	addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId);
 }
 
 void CHC::checkVerificationTargets()
 {
-	for (auto const& [scope, targets]: m_verificationTargets)
+	// The verification conditions have been collected per function where they have been encountered (m_verificationTargets).
+	// Also, all possible contexts in which an external function can be called has been recorded (m_queryPlaceholders).
+	// Here we combine every context in which an external function can be called with all possible verification conditions
+	// in its call graph. Each such combination forms a unique verification target.
+	vector<CHCVerificationTarget> verificationTargets;
+	for (auto const& [function, placeholders]: m_queryPlaceholders)
 	{
-		for (size_t i = 0; i < targets.size(); ++i)
+		auto functionTargets = transactionVerificationTargetsIds(function);
-		{
+		for (auto const& placeholder: placeholders)
-			auto const& target = targets[i];
+			for (unsigned id: functionTargets)
-
-			if (target.type == VerificationTarget::Type::Assert)
-				checkAssertTarget(scope, target);
-			else
 			{
-				string satMsg;
+				auto const& target = m_verificationTargets.at(id);
-				string satMsgUnderflow;
+				verificationTargets.push_back(CHCVerificationTarget{
-				string satMsgOverflow;
+					{target.type, placeholder.fromPredicate, placeholder.constraints && placeholder.errorExpression == target.errorId},
-				string unknownMsg;
+					target.errorId,
-				ErrorId errorReporterId;
+					target.errorNode
-				ErrorId underflowErrorId = 3944_error;
+				});
-				ErrorId overflowErrorId = 4984_error;
+			}
+	}
 
-				if (target.type == VerificationTarget::Type::PopEmptyArray)
+	set<unsigned> checkedErrorIds;
-				{
+	for (auto const& target: verificationTargets)
-					solAssert(dynamic_cast<FunctionCall const*>(scope), "");
+	{
-					satMsg = "Empty array \"pop\" detected here.";
+		string errorType;
-					unknownMsg = "Empty array \"pop\" might happen here.";
+		ErrorId errorReporterId;
-					errorReporterId = 2529_error;
-				}
-				else if (
-					target.type == VerificationTarget::Type::Underflow ||
-					target.type == VerificationTarget::Type::Overflow
-				)
-				{
-					auto const* expr = dynamic_cast<Expression const*>(scope);
-					solAssert(expr, "");
-					auto const* intType = dynamic_cast<IntegerType const*>(expr->annotation().type);
-					if (!intType)
-						intType = TypeProvider::uint256();
 
-					satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")";
+		if (target.type == VerificationTarget::Type::PopEmptyArray)
-					satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")";
+		{
-					if (target.type == VerificationTarget::Type::Underflow)
+			solAssert(dynamic_cast<FunctionCall const*>(target.errorNode), "");
-					{
+			errorType = "Empty array \"pop\"";
-						satMsg = satMsgUnderflow + " happens here.";
+			errorReporterId = 2529_error;
-						unknownMsg = satMsgUnderflow + " might happen here.";
+		}
-						errorReporterId = underflowErrorId;
+		else if (
-					}
+			target.type == VerificationTarget::Type::Underflow ||
-					else if (target.type == VerificationTarget::Type::Overflow)
+			target.type == VerificationTarget::Type::Overflow
-					{
+		)
-						satMsg = satMsgOverflow + " happens here.";
+		{
-						unknownMsg = satMsgOverflow + " might happen here.";
+			auto const* expr = dynamic_cast<Expression const*>(target.errorNode);
-						errorReporterId = overflowErrorId;
+			solAssert(expr, "");
-					}
+			auto const* intType = dynamic_cast<IntegerType const*>(expr->annotation().type);
-				}
+			if (!intType)
-				else if (target.type == VerificationTarget::Type::DivByZero)
+				intType = TypeProvider::uint256();
-				{
-					satMsg = "Division by zero happens here.";
-					unknownMsg = "Division by zero might happen here.";
-					errorReporterId = 4281_error;
-				}
-				else
-					solAssert(false, "");
 
-				auto it = m_errorIds.find(scope->id());
+			if (target.type == VerificationTarget::Type::Underflow)
-				solAssert(it != m_errorIds.end(), "");
+			{
-				solAssert(i < it->second.size(), "");
+				errorType = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")";
-				unsigned errorId = it->second[i];
+				errorReporterId = 3944_error;
-
+			}
-				checkAndReportTarget(scope, target, errorId, errorReporterId, satMsg, unknownMsg);
+			else if (target.type == VerificationTarget::Type::Overflow)
+			{
+				errorType = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")";
+				errorReporterId = 4984_error;
 			}
 		}
-	}
+		else if (target.type == VerificationTarget::Type::DivByZero)
-}
+		{
+			errorType = "Division by zero";
+			errorReporterId = 4281_error;
+		}
+		else if (target.type == VerificationTarget::Type::Assert)
+		{
+			errorType = "Assertion violation";
+			errorReporterId = 6328_error;
+		}
+		else
+			solAssert(false, "");
 
-void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const& _target)
+		checkAndReportTarget(target, errorReporterId, errorType + " happens here.", errorType + " might happen here.");
-{
+		checkedErrorIds.insert(target.errorId);
-	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(), "");
-		solAssert(!it->second.empty(), "");
-		unsigned errorId = it->second[0];
-
-		checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here.", "Assertion violation might happen here.");
 	}
+
+	// There can be targets in internal functions that are not reachable from the external interface.
+	// These are safe by definition and are not even checked by the CHC engine, but this information
+	// must still be reported safe by the BMC engine.
+	set<unsigned> allErrorIds;
+	for (auto const& entry: m_functionTargetIds)
+		for (unsigned id: entry.second)
+			allErrorIds.insert(id);
+
+	set<unsigned> unreachableErrorIds;
+	set_difference(
+		allErrorIds.begin(),
+		allErrorIds.end(),
+		checkedErrorIds.begin(),
+		checkedErrorIds.end(),
+		inserter(unreachableErrorIds, unreachableErrorIds.begin())
+	);
+	for (auto id: unreachableErrorIds)
+		m_safeTargets[m_verificationTargets.at(id).errorNode].insert(m_verificationTargets.at(id).type);
 }
 
 void CHC::checkAndReportTarget(
-	ASTNode const* _scope,
 	CHCVerificationTarget const& _target,
-	unsigned _errorId,
 	ErrorId _errorReporterId,
 	string _satMsg,
 	string _unknownMsg
 )
 {
-	if (m_unsafeTargets.count(_scope) && m_unsafeTargets.at(_scope).count(_target.type))
+	if (m_unsafeTargets.count(_target.errorNode) && m_unsafeTargets.at(_target.errorNode).count(_target.type))
 		return;
 
 	createErrorBlock();
-	connectBlocks(_target.value, error(), _target.constraints && (_target.errorId == _errorId));
+	connectBlocks(_target.value, error(), _target.constraints);
-	auto const& [result, model] = query(error(), _scope->location());
+	auto const& location = _target.errorNode->location();
+	auto const& [result, model] = query(error(), location);
 	if (result == CheckResult::UNSATISFIABLE)
-		m_safeTargets[_scope].insert(_target.type);
+		m_safeTargets[_target.errorNode].insert(_target.type);
 	else if (result == CheckResult::SATISFIABLE)
 	{
 		solAssert(!_satMsg.empty(), "");
-		m_unsafeTargets[_scope].insert(_target.type);
+		m_unsafeTargets[_target.errorNode].insert(_target.type);
 		auto cex = generateCounterexample(model, error().name);
 		if (cex)
 			m_outerErrorReporter.warning(
 				_errorReporterId,
-				_scope->location(),
+				location,
 				"CHC: " + _satMsg,
 				SecondarySourceLocation().append("Counterexample:\n" + *cex, SourceLocation{})
 			);
 		else
 			m_outerErrorReporter.warning(
 				_errorReporterId,
-				_scope->location(),
+				location,
 				"CHC: " + _satMsg
 			);
 	}
 	else if (!_unknownMsg.empty())
 		m_outerErrorReporter.warning(
 			_errorReporterId,
-			_scope->location(),
+			location,
 			"CHC: " + _unknownMsg
 		);
 }
@@ -1431,14 +1400,13 @@ string CHC::contractSuffix(ContractDefinition const& _contract)
 	return _contract.name() + "_" + to_string(_contract.id());
 }
 
-unsigned CHC::newErrorId(frontend::Expression const& _expr)
+unsigned CHC::newErrorId()
 {
 	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[_expr.id()].push_back(errorId);
 	return errorId;
 }
 

libsolidity/formal/CHC.h

@@ -114,7 +114,7 @@ private:
 	void eraseKnowledge();
 	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
 	void setCurrentBlock(Predicate const& _block);
-	std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
+	std::set<unsigned> transactionVerificationTargetsIds(ASTNode const* _txRoot);
 	//@}
 
 	/// Sort helpers.
@@ -181,19 +181,14 @@ private:
 	/// @returns <false, model> otherwise.
 	std::pair<smtutil::CheckResult, smtutil::CHCSolverInterface::CexGraph> query(smtutil::Expression const& _query, langutil::SourceLocation const& _location);
 
-	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
+	void verificationTargetEncountered(ASTNode const* const _errorNode, VerificationTarget::Type _type, smtutil::Expression const& _errorCondition);
-	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _errorId);
-	void addVerificationTarget(frontend::Expression const& _scope, VerificationTarget::Type _type, smtutil::Expression const& _target);
-	void addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, 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,
 		langutil::ErrorId _errorReporterId,
 		std::string _satMsg,
 		std::string _unknownMsg = ""
@@ -234,7 +229,7 @@ private:
 
 	/// @returns a new unique error id associated with _expr and stores
 	/// it into m_errorIds.
-	unsigned newErrorId(Expression const& _expr);
+	unsigned newErrorId();
 
 	smt::SymbolicState& state();
 	smt::SymbolicIntVariable& errorFlag();
@@ -275,12 +270,30 @@ private:
 	//@{
 	struct CHCVerificationTarget: VerificationTarget
 	{
-		smtutil::Expression errorId;
+		unsigned const errorId;
+		ASTNode const* const errorNode;
 	};
 
-	/// Verification targets corresponding to ASTNodes. There can be multiple targets for a single ASTNode,
+	/// Query placeholder stores information necessary to create the final query edge in the CHC system.
-	/// e.g., divByZero and Overflow for signed division.
+	/// It is combined with the unique error id (and error type) to create a complete Verification Target.
-	std::map<ASTNode const*, std::vector<CHCVerificationTarget>, IdCompare> m_verificationTargets;
+	struct CHCQueryPlaceholder
+	{
+		smtutil::Expression const constraints;
+		smtutil::Expression const errorExpression;
+		smtutil::Expression const fromPredicate;
+	};
+
+	/// 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;
+
+	/// 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;
+	/// Helper mapping unique IDs to actual verification targets.
+	std::map<unsigned, CHCVerificationTarget> m_verificationTargets;
 
 	/// Targets proven safe.
 	std::map<ASTNode const*, std::set<VerificationTarget::Type>> m_safeTargets;
@@ -294,12 +307,6 @@ private:
 
 	std::map<ASTNode const*, std::set<ASTNode const*, IdCompare>, IdCompare> m_callGraph;
 
-	std::map<ASTNode const*, std::set<Expression const*>, IdCompare> m_functionAssertions;
-
-	/// Maps ASTNode ids to error ids.
-	/// There can be multiple errorIds associated with a single ASTNode.
-	std::map<unsigned, std::vector<unsigned>> m_errorIds;
-
 	/// The current block.
 	smtutil::Expression m_currentBlock = smtutil::Expression(true);
 

libsolidity/formal/EncodingContext.cpp

@@ -33,7 +33,6 @@ EncodingContext::EncodingContext():
 void EncodingContext::reset()
 {
 	resetAllVariables();
-	resetUniqueId();
 	m_expressions.clear();
 	m_globalContext.clear();
 	m_state.reset();

test/libsolidity/smtCheckerTests/array_members/array_pop_length_1.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): CHC: Empty array "pop" detected here.
+// Warning 2529: (82-89): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/array_members/array_pop_length_2.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): CHC: Empty array "pop" detected here.
+// Warning 2529: (82-89): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/array_members/array_pop_length_3.sol

@@ -8,5 +8,5 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): CHC: Empty array "pop" detected here.
+// Warning 2529: (82-89): CHC: Empty array "pop" happens here.
-// Warning 2529: (93-100): CHC: Empty array "pop" detected here.
+// Warning 2529: (93-100): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/array_members/array_pop_length_4.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (94-101): CHC: Empty array "pop" detected here.
+// Warning 2529: (94-101): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/array_members/array_pop_length_5.sol

@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (122-129): CHC: Empty array "pop" detected here.
+// Warning 2529: (122-129): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/array_members/array_pop_length_6.sol

@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (127-134): CHC: Empty array "pop" detected here.
+// Warning 2529: (127-134): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/array_members/array_pop_length_8.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): CHC: Empty array "pop" detected here.
+// Warning 2529: (82-89): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol

@@ -7,4 +7,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): CHC: Empty array "pop" detected here.
+// Warning 2529: (82-89): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol

@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (111-121): CHC: Empty array "pop" detected here.
+// Warning 2529: (111-121): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol

@@ -7,4 +7,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (76-83): CHC: Empty array "pop" detected here.
+// Warning 2529: (76-83): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol

@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (150-157): CHC: Empty array "pop" detected here.
+// Warning 2529: (150-157): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol

@@ -18,6 +18,6 @@ contract A is B {
 	}
 }
 // ----
-// Warning 4984: (198-203): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (207-212): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (198-203): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (230-235): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol

@@ -13,5 +13,5 @@ contract C {
 	}
 }
 // ----
-// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (162-176): CHC: Assertion violation happens here.
+// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/imports/imported_fail_1.sol

@@ -21,4 +21,5 @@ contract B is A {
 	}
 }
 // ----
+// Warning 6328: (B.sol:71-85): CHC: Assertion violation happens here.
 // Warning 6328: (C.sol:103-117): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol

@@ -15,4 +15,6 @@ contract C
 }
 // ----
 // Warning 4984: (176-181): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 6328: (296-309): CHC: Assertion violation might happen here.
 // Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4661: (296-309): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol

@@ -16,5 +16,7 @@ contract LoopFor2 {
 	}
 }
 // ----
+// Warning 4984: (252-257): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4984: (232-238): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (373-392): CHC: Assertion violation happens here.
 // Warning 6328: (396-415): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol

@@ -20,3 +20,5 @@ contract LoopFor2 {
 // ====
 // SMTSolvers: z3
 // ----
+// Warning 4984: (245-250): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4984: (225-231): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol

@@ -19,4 +19,6 @@ contract LoopFor2 {
 	}
 }
 // ----
+// Warning 4984: (236-241): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4984: (216-222): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (363-382): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol

@@ -19,5 +19,7 @@ contract LoopFor2 {
 	}
 }
 // ----
+// Warning 4984: (237-242): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4984: (217-223): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (341-360): CHC: Assertion violation happens here.
 // Warning 6328: (364-383): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol

@@ -14,12 +14,12 @@ contract LoopFor2 {
 			c[i] = b[i];
 			++i;
 		}
-		assert(b[0] == c[0]);
+		//assert(b[0] == c[0]); // Removed because of Spacer's nondeterminism
 		assert(a[0] == 900);
 		assert(b[0] == 900);
 	}
 }
 // ----
 // Warning 4984: (229-234): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 6328: (290-309): CHC: Assertion violation happens here.
+// Warning 6328: (338-357): CHC: Assertion violation happens here.
-// Warning 6328: (313-332): CHC: Assertion violation happens here.
+// Warning 6328: (361-380): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations_2.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint x;
+
+	modifier m {
+		require(x == 0);
+		_;
+		x = x + 1;
+		assert(x <= 2);
+	}
+
+	function f() m m public {
+		x = x + 1;
+	}
+}
+// ----
+// Warning 6328: (109-123): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/slice_default_end.sol

@@ -7,14 +7,10 @@ contract C {
 		require(b[b.length - 1] == 0xaa);
 		assert(bytes(b[10:]).length == 20);
 		assert(bytes(b[10:])[0] == 0xff);
-		assert(bytes(b[10:])[5] == 0xff);
+		//assert(bytes(b[10:])[5] == 0xff); // Removed because of Spacer's nondeterminism
 		assert(bytes(b[10:])[19] == 0xaa);
 	}
 }
 // ----
 // Warning 6328: (221-253): CHC: Assertion violation might happen here.
-// Warning 6328: (257-289): CHC: Assertion violation might happen here.
-// Warning 6328: (293-326): CHC: Assertion violation might happen here.
 // Warning 4661: (221-253): BMC: Assertion violation happens here.
-// Warning 4661: (257-289): BMC: Assertion violation happens here.
-// Warning 4661: (293-326): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/overflow/overflow_sum.sol

@@ -14,5 +14,6 @@ contract C
 	}
 }
 // ----
+// Warning 4984: (109-116): CHC: Overflow (resulting value larger than 255) happens here.
 // Warning 4984: (154-159): CHC: Overflow (resulting value larger than 255) happens here.
 // Warning 4984: (185-192): CHC: Overflow (resulting value larger than 255) happens here.

test/libsolidity/smtCheckerTests/overflow/safe_add_1.sol

@@ -7,3 +7,5 @@ contract C
 		return x + y;
 	}
 }
+// ----
+// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/overflow/safe_add_2.sol

@@ -8,3 +8,5 @@ contract C
 		return z;
 	}
 }
+// ----
+// Warning 4984: (116-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/overflow/signed_guard_sum_overflow.sol

@@ -8,4 +8,5 @@ contract C  {
 }
 // ----
 // Warning 3944: (111-116): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here.
+// Warning 4984: (111-116): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
 // Warning 3944: (133-138): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here.

test/libsolidity/smtCheckerTests/overflow/unsigned_guard_sum_overflow.sol

@@ -6,3 +6,5 @@ contract C  {
 		return x + y;
 	}
 }
+// ----
+// Warning 4984: (114-119): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/special/many.sol

@@ -15,12 +15,12 @@ contract C
 	}
 }
 // ----
-// Warning 4984: (311-316): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (79-115): CHC: Assertion violation happens here.
 // Warning 6328: (119-161): CHC: Assertion violation happens here.
 // Warning 6328: (165-204): CHC: Assertion violation happens here.
 // Warning 6328: (208-240): CHC: Assertion violation happens here.
 // Warning 6328: (244-275): CHC: Assertion violation happens here.
+// Warning 4984: (311-316): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (304-332): CHC: Assertion violation happens here.
 // Warning 6328: (336-364): CHC: Assertion violation happens here.
 // Warning 6328: (368-391): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/function_type_external_address.sol

@@ -7,4 +7,3 @@ contract C {
 }
 // ----
 // Warning 7650: (128-137): Assertion checker does not yet support this expression.
-// Warning 4661: (141-155): BMC: Assertion violation happens here.

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

@@ -21,5 +21,5 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (121-130): CHC: Empty array "pop" detected here.
+// Warning 2529: (121-130): CHC: Empty array "pop" happens here.
 // Warning 6328: (230-254): CHC: Assertion violation happens here.

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

@@ -18,5 +18,5 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (133-142): CHC: Empty array "pop" detected here.
+// Warning 2529: (133-142): CHC: Empty array "pop" happens here.
 // Warning 6328: (189-213): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/tuple_array_pop_1.sol

@@ -4,4 +4,4 @@ contract C {
 	function f() public { (a).pop();}
 }
 // ----
-// Warning 2529: (78-87): CHC: Empty array "pop" detected here.
+// Warning 2529: (78-87): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/types/tuple_array_pop_2.sol

@@ -4,4 +4,4 @@ contract C {
 	function f() public { (((((a))))).pop();}
 }
 // ----
-// Warning 2529: (78-95): CHC: Empty array "pop" detected here.
+// Warning 2529: (78-95): CHC: Empty array "pop" happens here.

test/libsolidity/smtCheckerTests/types/tuple_declarations_function_2.sol

@@ -15,4 +15,3 @@ contract C
 	}
 }
 // ----
-// Warning 4984: (152-157): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.