Merge pull request #9376 from ethereum/smt_refactor_targets

[SMTChecker] Refactor verification targets

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,7 +684,13 @@ void BMC::checkBalance(BMCVerificationTarget& _target)
 void BMC::checkAssert(BMCVerificationTarget& _target)
 {
 	solAssert(_target.type == VerificationTarget::Type::Assert, "");
-	if (!m_safeAssertions.count(_target.expression))
+
+	if (
+		m_solvedTargets.count(_target.expression) &&
+		m_solvedTargets.at(_target.expression).count(_target.type)
+	)
+		return;
+
 	checkCondition(
 		_target.constraints && !_target.value,
 		_target.callStack,

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();
 }
@@ -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
@@ -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

@@ -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);