SMTChecker: Refactor processing invariants from the solver

Instead of extracting invariants as a single expression containing all
predicates and their definitions, we represent invariants as a map from
predicate names to the corresponding definitions.
Additionally, we need to remember formal arguments of the predicate so
we can apply substitutions to the definitions properly.

I believe the previous representation was an artifact of how Z3 returns
CHC model through its API. The new representation is more fitting for
models extracted from SMT-LIB.

Author: blishko

libsmtutil/CHCSmtLib2Interface.cpp

@@ -102,21 +102,18 @@ CHCSolverInterface::QueryResult CHCSmtLib2Interface::query(Expression const& _bl
 		// However, with CHC solvers, the meaning is flipped, UNSAT -> UNSAFE and SAT -> SAFE.
 		// So we have to flip the answer.
 		if (boost::starts_with(response, "sat"))
-		{
-			auto maybeInvariants = invariantsFromSolverResponse(response);
-			return {CheckResult::UNSATISFIABLE, maybeInvariants.value_or(Expression(true)), {}};
-		}
-		else if (boost::starts_with(response, "unsat"))
+			return {CheckResult::UNSATISFIABLE, invariantsFromSolverResponse(response), {}};
+		if (boost::starts_with(response, "unsat"))
 			result = CheckResult::SATISFIABLE;
 		else if (boost::starts_with(response, "unknown"))
 			result = CheckResult::UNKNOWN;
 		else
 			result = CheckResult::ERROR;
-		return {result, Expression(true), {}};
+		return {result, {}, {}};
 	}
 	catch(smtutil::SMTSolverInteractionError const&)
 	{
-		return {CheckResult::ERROR, Expression(true), {}};
+		return {CheckResult::ERROR, {}, {}};
 	}
 
 }
@@ -416,7 +413,7 @@ smtutil::Expression CHCSmtLib2Interface::ScopedParser::toSMTUtilExpression(SMTLi
 }
 
 
-std::optional<smtutil::Expression> CHCSmtLib2Interface::invariantsFromSolverResponse(std::string const& _response) const
+CHCSmtLib2Interface::Invariants CHCSmtLib2Interface::invariantsFromSolverResponse(std::string const& _response) const
 {
 	std::stringstream ss(_response);
 	std::string answer;
@@ -438,7 +435,7 @@ std::optional<smtutil::Expression> CHCSmtLib2Interface::invariantsFromSolverResp
 	smtSolverInteractionRequire(parser.isEOF(), "Error during parsing CHC model");
 	smtSolverInteractionRequire(!parsedOutput.empty(), "Error during parsing CHC model");
 	auto& commands = parsedOutput.size() == 1 ? asSubExpressions(parsedOutput[0]) : parsedOutput;
-	std::vector<Expression> definitions;
+	Invariants definitions;
 	for (auto& command: commands)
 	{
 		auto& args = asSubExpressions(command);
@@ -456,7 +453,7 @@ std::optional<smtutil::Expression> CHCSmtLib2Interface::invariantsFromSolverResp
 		inlineLetExpressions(interpretation);
 		ScopedParser scopedParser(m_context);
 		auto const& formalArguments = asSubExpressions(args[2]);
-		std::vector<Expression> predicateArgs;
+		std::vector<std::string> predicateArguments;
 		for (auto const& formalArgument: formalArguments)
 		{
 			smtSolverInteractionRequire(!isAtom(formalArgument), "Invalid format of CHC model");
@@ -465,7 +462,7 @@ std::optional<smtutil::Expression> CHCSmtLib2Interface::invariantsFromSolverResp
 			smtSolverInteractionRequire(isAtom(nameSortPair[0]), "Invalid format of CHC model");
 			SortPointer varSort = scopedParser.toSort(nameSortPair[1]);
 			scopedParser.addVariableDeclaration(asAtom(nameSortPair[0]), varSort);
-			predicateArgs.push_back(scopedParser.toSMTUtilExpression(nameSortPair[0]));
+			predicateArguments.push_back(asAtom(nameSortPair[0]));
 		}
 
 		auto parsedInterpretation = scopedParser.toSMTUtilExpression(interpretation);
@@ -476,11 +473,11 @@ std::optional<smtutil::Expression> CHCSmtLib2Interface::invariantsFromSolverResp
 				return first.name < second.name;
 			});
 
-		Expression predicate(asAtom(args[1]), predicateArgs, SortProvider::boolSort);
-		// FIXME: Why do we need to represent the predicate as Expression?
-		definitions.push_back(predicate == parsedInterpretation);
+		std::string const& predicateName = asAtom(args[1]);
+		smtSolverInteractionRequire(!definitions.contains(predicateName), "Predicates must be unique");
+		definitions.emplace(predicateName, InvariantInfo{parsedInterpretation, predicateArguments});
 	}
-	return Expression::mkAnd(std::move(definitions));
+	return definitions;
 }
 
 namespace

libsmtutil/CHCSmtLib2Interface.h

@@ -94,8 +94,8 @@ class CHCSmtLib2Interface: public CHCSolverInterface
 	/// Communicates with the solver via the callback. Throws SMTSolverError on error.
 	virtual std::string querySolver(std::string const& _input);
 
-	/// Translates CHC solver response with a model to our representation of invariants. Returns None on error.
-	std::optional<smtutil::Expression> invariantsFromSolverResponse(std::string const& _response) const;
+	/// Translates CHC solver response with a model to our representation of invariants.
+	Invariants invariantsFromSolverResponse(std::string const& _response) const;
 
 	std::set<std::string> collectVariableNames(Expression const& _expr) const;
 

libsmtutil/CHCSolverInterface.h

@@ -25,6 +25,7 @@
 #include <libsmtutil/SolverInterface.h>
 
 #include <map>
+#include <unordered_map>
 #include <vector>
 
 namespace solidity::smtutil
@@ -49,10 +50,19 @@ class CHCSolverInterface : public SolverInterface
 		std::map<unsigned, std::vector<unsigned>> edges;
 	};
 
+	struct InvariantInfo
+	{
+		/// Predicate definition as SMT expression
+		Expression expression;
+		/// Names of the formal arguments of the predicate definition
+		std::vector<std::string> variableNames;
+	};
+	/// Maps predicate to its definition as given by the solver and the formal arguments of the predicate
+	using Invariants = std::unordered_map<std::string, InvariantInfo>;
 	struct QueryResult
 	{
 		CheckResult answer;
-		Expression invariant;
+		Invariants invariants;
 		CexGraph cex;
 	};
 	/// Takes a function application _expr and checks for reachability.

libsolidity/formal/CHC.cpp

@@ -34,9 +34,8 @@
 #include <libsolutil/Algorithms.h>
 #include <libsolutil/StringUtils.h>
 
-#include <boost/algorithm/string.hpp>
-
 #include <range/v3/algorithm/for_each.hpp>
+#include <range/v3/algorithm/none_of.hpp>
 #include <range/v3/view.hpp>
 #include <range/v3/view/enumerate.hpp>
 #include <range/v3/view/reverse.hpp>
@@ -1895,7 +1894,7 @@ CHCSolverInterface::QueryResult CHC::query(smtutil::Expression const& _query, la
 			2339_error,
 			"CHC: Requested query:\n" + smtLibCode
 		);
-		return {.answer = CheckResult::UNKNOWN, .invariant = smtutil::Expression(true), .cex = {}};
+		return {.answer = CheckResult::UNKNOWN, .invariants = {}, .cex = {}};
 	}
 	auto result = m_interface->query(_query);
 	switch (result.answer)
@@ -2137,7 +2136,7 @@ void CHC::checkVerificationTargets()
 namespace
 {
 std::map<Predicate const*, std::set<std::string>> collectInvariants(
-	smtutil::Expression const& _proof,
+	CHCSmtLib2Interface::Invariants const& _invariants,
 	std::set<Predicate const*> const& _predicates,
 	ModelCheckerInvariants const& _invariantsSetting
 )
@@ -2148,38 +2147,23 @@ std::map<Predicate const*, std::set<std::string>> collectInvariants(
 	if (_invariantsSetting.has(InvariantType::Reentrancy))
 		targets.insert("nondet_interface_");
 
-	std::map<std::string, std::pair<smtutil::Expression, smtutil::Expression>> equalities;
-	// Collect equalities where one of the sides is a predicate we're interested in.
-	util::BreadthFirstSearch<smtutil::Expression const*>{{&_proof}}.run([&](auto&& _expr, auto&& _addChild) {
-		if (_expr->name == "=")
-			for (auto const& t: targets)
-			{
-				auto arg0 = _expr->arguments.at(0);
-				auto arg1 = _expr->arguments.at(1);
-				if (boost::algorithm::starts_with(arg0.name, t))
-					equalities.insert({arg0.name, {arg0, std::move(arg1)}});
-				else if (boost::algorithm::starts_with(arg1.name, t))
-					equalities.insert({arg1.name, {arg1, std::move(arg0)}});
-			}
-		for (auto const& arg: _expr->arguments)
-			_addChild(&arg);
-	});
-
 	std::map<Predicate const*, std::set<std::string>> invariants;
-	for (auto pred: _predicates)
+	for (auto const* pred: _predicates)
 	{
-		auto predName = pred->functor().name;
-		if (!equalities.count(predName))
+		smtAssert(pred);
+		auto const& predName = pred->functor().name;
+		if (!_invariants.contains(predName))
+			continue;
+		if (ranges::none_of(targets, [&](auto const& _target) { return predName.starts_with(_target); }))
 			continue;
 
-		solAssert(pred->contextContract(), "");
+		smtAssert(pred->contextContract());
 
-		auto const& [predExpr, invExpr] = equalities.at(predName);
+		auto const& [definition, formalArguments] = _invariants.at(predName);
 
-		static std::set<std::string> const ignore{"true", "false"};
-		auto r = substitute(invExpr, pred->expressionSubstitution(predExpr));
+		auto r = substitute(definition, pred->expressionSubstitution(formalArguments));
 		// No point in reporting true/false as invariants.
-		if (!ignore.count(r.name))
+		if (r.name != "true" && r.name != "false")
 			invariants[pred].insert(toSolidityStr(r));
 	}
 	return invariants;
@@ -2205,7 +2189,7 @@ void CHC::checkAndReportTarget(
 			placeholder.constraints && placeholder.errorExpression == _target.errorId
 		);
 	auto const& location = _target.errorNode->location();
-	auto [result, invariant, model] = query(error(), location);
+	auto [result, invariants, model] = query(error(), location);
 	if (result == CheckResult::UNSATISFIABLE)
 	{
 		m_safeTargets[_target.errorNode].insert(_target);
@@ -2214,9 +2198,9 @@ void CHC::checkAndReportTarget(
 			predicates.insert(pred);
 		for (auto const* pred: m_nondetInterfaces | ranges::views::values)
 			predicates.insert(pred);
-		std::map<Predicate const*, std::set<std::string>> invariants = collectInvariants(invariant, predicates, m_settings.invariants);
-		for (auto pred: invariants | ranges::views::keys)
-			m_invariants[pred] += std::move(invariants.at(pred));
+		std::map<Predicate const*, std::set<std::string>> invariantStrings = collectInvariants(invariants, predicates, m_settings.invariants);
+		for (auto pred: invariantStrings | ranges::views::keys)
+			m_invariants[pred] += std::move(invariantStrings.at(pred));
 	}
 	else if (result == CheckResult::SATISFIABLE)
 	{

libsolidity/formal/Predicate.cpp

@@ -27,12 +27,10 @@
 #include <libsolidity/ast/TypeProvider.h>
 
 #include <boost/algorithm/string/join.hpp>
-#include <boost/algorithm/string.hpp>
 
 #include <range/v3/view.hpp>
 #include <utility>
 
-using boost::algorithm::starts_with;
 using namespace solidity;
 using namespace solidity::smtutil;
 using namespace solidity::frontend;
@@ -434,28 +432,29 @@ std::pair<std::vector<std::optional<std::string>>, std::vector<VariableDeclarati
 	return {formatExpressions(outValuesInScope, outTypes), localVarsInScope};
 }
 
-std::map<std::string, std::string> Predicate::expressionSubstitution(smtutil::Expression const& _predExpr) const
+std::map<std::string, std::string> Predicate::expressionSubstitution(std::vector<std::string> const& _predArgs) const
 {
 	std::map<std::string, std::string> subst;
 	std::string predName = functor().name;
 
-	solAssert(contextContract(), "");
+	smtAssert(contextContract());
 	auto const& stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contextContract());
 
-	auto nArgs = _predExpr.arguments.size();
+	auto const nArgs = _predArgs.size();
 
 	// The signature of an interface predicate is
 	// interface(this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, blockchainState, stateVariables).
 	// An invariant for an interface predicate is a contract
 	// invariant over its state, for example `x <= 0`.
 	if (isInterface())
 	{
+		smtAssert(nArgs > 0);
 		size_t shift = txValuesIndex();
-		solAssert(starts_with(predName, "interface"), "");
-		subst[_predExpr.arguments.at(0).name] = "address(this)";
-		solAssert(nArgs == stateVars.size() + shift, "");
+		smtAssert(predName.starts_with("interface"));
+		subst[_predArgs.at(0)] = "address(this)";
+		smtAssert(nArgs == stateVars.size() + shift);
 		for (size_t i = nArgs - stateVars.size(); i < nArgs; ++i)
-			subst[_predExpr.arguments.at(i).name] = stateVars.at(i - shift)->name();
+			subst[_predArgs.at(i)] = stateVars.at(i - shift)->name();
 	}
 	// The signature of a nondet interface predicate is
 	// nondet_interface(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
@@ -466,14 +465,15 @@ std::map<std::string, std::string> Predicate::expressionSubstitution(smtutil::Ex
 	// `(x <= 0) => (x' <= 100)`.
 	else if (isNondetInterface())
 	{
-		solAssert(starts_with(predName, "nondet_interface"), "");
-		subst[_predExpr.arguments.at(0).name] = "<errorCode>";
-		subst[_predExpr.arguments.at(1).name] = "address(this)";
-		solAssert(nArgs == stateVars.size() * 2 + firstArgIndex(), "");
+		smtAssert(nArgs > 1);
+		smtAssert(predName.starts_with("nondet_interface"));
+		subst[_predArgs.at(0)] = "<errorCode>";
+		subst[_predArgs.at(1)] = "address(this)";
+		smtAssert(nArgs == stateVars.size() * 2 + firstArgIndex());
 		for (size_t i = nArgs - stateVars.size(), s = 0; i < nArgs; ++i, ++s)
-			subst[_predExpr.arguments.at(i).name] = stateVars.at(s)->name() + "'";
+			subst[_predArgs.at(i)] = stateVars.at(s)->name() + "'";
 		for (size_t i = nArgs - (stateVars.size() * 2 + 1), s = 0; i < nArgs - (stateVars.size() + 1); ++i, ++s)
-			subst[_predExpr.arguments.at(i).name] = stateVars.at(s)->name();
+			subst[_predArgs.at(i)] = stateVars.at(s)->name();
 	}
 
 	return subst;

libsolidity/formal/Predicate.h

@@ -179,9 +179,9 @@ class Predicate
 	/// @returns the values of the local variables used by this predicate.
 	std::pair<std::vector<std::optional<std::string>>, std::vector<VariableDeclaration const*>> localVariableValues(std::vector<smtutil::Expression> const& _args) const;
 
-	/// @returns a substitution map from the arguments of _predExpr
+	/// @returns a substitution map from the predicate arguments @p _predArgs
 	/// to a Solidity-like expression.
-	std::map<std::string, std::string> expressionSubstitution(smtutil::Expression const& _predExprs) const;
+	std::map<std::string, std::string> expressionSubstitution(std::vector<std::string> const& _predArgs) const;
 
 private:
 	/// Recursively fills _array from _expr.

libsolidity/formal/Z3CHCSmtLib2Interface.cpp

@@ -90,26 +90,23 @@ CHCSolverInterface::QueryResult Z3CHCSmtLib2Interface::query(smtutil::Expression
 #endif
 			setupSmtCallback(true);
 			if (!boost::starts_with(response, "unsat"))
-				return {CheckResult::SATISFIABLE, Expression(true), {}};
-			return {CheckResult::SATISFIABLE, Expression(true), graphFromZ3Answer(response)};
+				return {CheckResult::SATISFIABLE, {}, {}};
+			return {CheckResult::SATISFIABLE, {}, graphFromZ3Answer(response)};
 		}
 
 		CheckResult result;
 		if (boost::starts_with(response, "sat"))
-		{
-			auto maybeInvariants = invariantsFromSolverResponse(response);
-			return {CheckResult::UNSATISFIABLE, maybeInvariants.value_or(Expression(true)), {}};
-		}
-		else if (boost::starts_with(response, "unknown"))
+			return {CheckResult::UNSATISFIABLE, invariantsFromSolverResponse(response), {}};
+		if (boost::starts_with(response, "unknown"))
 			result = CheckResult::UNKNOWN;
 		else
 			result = CheckResult::ERROR;
 
-		return {result, Expression(true), {}};
+		return {result, {}, {}};
 	}
 	catch(smtutil::SMTSolverInteractionError const&)
 	{
-		return {CheckResult::ERROR, Expression(true), {}};
+		return {CheckResult::ERROR, {}, {}};
 	}
 }