Merge pull request #15972 from ethereum/smt-refactor

SMTChecker: Refactor processing invariants from the solver

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/CMakeLists.txt

@@ -117,8 +117,6 @@ set(sources
 	formal/EncodingContext.h
 	formal/ExpressionFormatter.cpp
 	formal/ExpressionFormatter.h
-	formal/Invariants.cpp
-	formal/Invariants.h
 	formal/ModelChecker.cpp
 	formal/ModelChecker.h
 	formal/ModelCheckerSettings.cpp

libsolidity/formal/CHC.cpp

@@ -19,8 +19,8 @@
 #include <libsolidity/formal/CHC.h>
 
 #include <libsolidity/formal/ArraySlicePredicate.h>
+#include <libsolidity/formal/ExpressionFormatter.h>
 #include <libsolidity/formal/EldaricaCHCSmtLib2Interface.h>
-#include <libsolidity/formal/Invariants.h>
 #include <libsolidity/formal/ModelChecker.h>
 #include <libsolidity/formal/PredicateInstance.h>
 #include <libsolidity/formal/PredicateSort.h>
@@ -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)
@@ -2134,6 +2133,43 @@ void CHC::checkVerificationTargets()
 		m_safeTargets[m_verificationTargets.at(id).errorNode].insert(m_verificationTargets.at(id));
 }
 
+namespace
+{
+std::map<Predicate const*, std::set<std::string>> collectInvariants(
+	CHCSmtLib2Interface::Invariants const& _invariants,
+	std::set<Predicate const*> const& _predicates,
+	ModelCheckerInvariants const& _invariantsSetting
+)
+{
+	std::set<std::string> targets;
+	if (_invariantsSetting.has(InvariantType::Contract))
+		targets.insert("interface_");
+	if (_invariantsSetting.has(InvariantType::Reentrancy))
+		targets.insert("nondet_interface_");
+
+	std::map<Predicate const*, std::set<std::string>> invariants;
+	for (auto const* pred: _predicates)
+	{
+		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;
+
+		smtAssert(pred->contextContract());
+
+		auto const& [definition, formalArguments] = _invariants.at(predName);
+
+		auto r = substitute(definition, pred->expressionSubstitution(formalArguments));
+		// No point in reporting true/false as invariants.
+		if (r.name != "true" && r.name != "false")
+			invariants[pred].insert(toSolidityStr(r));
+	}
+	return invariants;
+}
+} // namespace
+
 void CHC::checkAndReportTarget(
 	CHCVerificationTarget const& _target,
 	std::vector<CHCQueryPlaceholder> const& _placeholders,
@@ -2153,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);
@@ -2162,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)
 	{