Move post input and post output filtering from CHC to Predicate

libsolidity/formal/CHC.cpp

@@ -29,7 +29,6 @@
 #include <libsmtutil/CHCSmtLib2Interface.h>
 #include <libsolutil/Algorithms.h>
 
-#include <boost/algorithm/string/join.hpp>
 #include <boost/range/adaptor/reversed.hpp>
 
 #include <queue>
@@ -1404,24 +1403,22 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		solAssert(edges.size() <= 2, "");
 
 		unsigned summaryId = edges.at(0);
-
 		optional<unsigned> interfaceId;
 		if (edges.size() == 2)
 		{
 			interfaceId = edges.at(1);
-			if (_graph.nodes.at(summaryId).first.rfind("summary", 0) != 0)
+			if (!Predicate::predicate(_graph.nodes.at(summaryId).first)->isSummary())
 				swap(summaryId, *interfaceId);
-			solAssert(_graph.nodes.at(*interfaceId).first.rfind("interface", 0) == 0, "");
+			auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first);
+			solAssert(interfacePredicate && interfacePredicate->isInterface(), "");
 		}
 		/// The children are unordered, so we need to check which is the summary and
 		/// which is the interface.
 
-		solAssert(_graph.nodes.at(summaryId).first.rfind("summary", 0) == 0, "");
+		Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).first);
+		solAssert(summaryPredicate && summaryPredicate->isSummary(), "");
 		/// At this point property 2 from the function description is verified for this node.
-
+		auto summaryArgs = _graph.nodes.at(summaryId).second;
-		auto const& summaryNode = _graph.nodes.at(summaryId);
-		Predicate const* summaryPredicate = Predicate::predicate(summaryNode.first);
-		solAssert(summaryPredicate, "");
 
 		FunctionDefinition const* calledFun = summaryPredicate->programFunction();
 		ContractDefinition const* calledContract = summaryPredicate->programContract();
@@ -1429,7 +1426,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		solAssert((calledFun && !calledContract) || (!calledFun && calledContract), "");
 		auto stateVars = summaryPredicate->stateVariables();
 		solAssert(stateVars.has_value(), "");
-		auto stateValues = summaryPredicate->summaryStateValues(summaryNode.second);
+		auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
 		solAssert(stateValues.size() == stateVars->size(), "");
 
 		/// This summary node is the end of a tx.
@@ -1440,36 +1437,23 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		{
 			lastTxSeen = true;
 			/// Generate counterexample message local to the failed target.
-			localState = formatStateCounterexample(*stateVars, stateValues) + "\n";
+			localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
 			if (calledFun)
 			{
-				/// The signature of a summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
+				auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
 				auto const& inParams = calledFun->parameters();
-				unsigned initLocals = stateVars->size() * 2 + 1 + inParams.size();
+				localState += formatVariableModel(inParams, inValues, "\n") + "\n";
-				/// In this loop we are interested in postInputVars.
+				auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs);
-				for (unsigned i = initLocals; i < initLocals + inParams.size(); ++i)
-				{
-					auto param = inParams.at(i - initLocals);
-					if (param->type()->isValueType())
-						localState += param->name() + " = " + summaryNode.second.at(i) + "\n";
-				}
 				auto const& outParams = calledFun->returnParameters();
-				initLocals += inParams.size();
+				localState += formatVariableModel(outParams, outValues, "\n") + "\n";
-				/// In this loop we are interested in outputVars.
-				for (unsigned i = initLocals; i < initLocals + outParams.size(); ++i)
-				{
-					auto param = outParams.at(i - initLocals);
-					if (param->type()->isValueType())
-						localState += param->name() + " = " + summaryNode.second.at(i) + "\n";
-				}
 			}
 		}
 		else
 			/// We report the state after every tx in the trace except for the last, which is reported
 			/// first in the code above.
-			path.emplace_back("State: " + formatStateCounterexample(*stateVars, stateValues));
+			path.emplace_back("State: " + formatVariableModel(*stateVars, stateValues, ", "));
 
-		string txCex = summaryPredicate->formatSummaryCall(summaryNode.second);
+		string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
 		path.emplace_back(txCex);
 
 		/// Recurse on the next interface node which represents the previous transaction
@@ -1483,21 +1467,6 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 	return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n");
 }
 
-string CHC::formatStateCounterexample(vector<VariableDeclaration const*> const& _stateVars, vector<string> const& _values)
-{
-	solAssert(_stateVars.size() == _values.size(), "");
-
-	vector<string> stateCex;
-	for (unsigned i = 0; i < _values.size(); ++i)
-	{
-		auto var = _stateVars.at(i);
-		if (var->type()->isValueType())
-			stateCex.emplace_back(var->name() + " = " + _values.at(i));
-	}
-
-	return boost::algorithm::join(stateCex, ", ");
-}
-
 string CHC::cex2dot(smtutil::CHCSolverInterface::CexGraph const& _cex)
 {
 	string dot = "digraph {\n";

libsolidity/formal/CHC.h

@@ -38,6 +38,8 @@
 
 #include <libsmtutil/CHCSolverInterface.h>
 
+#include <boost/algorithm/string/join.hpp>
+
 #include <map>
 #include <optional>
 #include <set>
@@ -221,11 +223,23 @@ private:
 	);
 
 	std::optional<std::string> generateCounterexample(smtutil::CHCSolverInterface::CexGraph const& _graph, std::string const& _root);
-	/// @returns values for the _stateVariables after a transaction calling
+
-	/// _function was executed.
+	/// @returns a set of pairs _var = _value separated by _separator.
-	/// _function = nullptr means the transaction was the deployment of a
+	template <typename T>
-	/// contract without an explicit constructor.
+	std::string formatVariableModel(std::vector<T> const& _variables, std::vector<std::string> const& _values, std::string const& _separator) const
-	std::string formatStateCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, std::vector<std::string> const& _values);
+	{
+		solAssert(_variables.size() == _values.size(), "");
+
+		std::vector<std::string> assignments;
+		for (unsigned i = 0; i < _values.size(); ++i)
+		{
+			auto var = _variables.at(i);
+			if (var && var->type()->isValueType())
+				assignments.emplace_back(var->name() + " = " + _values.at(i));
+		}
+
+		return boost::algorithm::join(assignments, _separator);
+	}
 
 	/// @returns a DAG in the dot format.
 	/// Used for debugging purposes.

libsolidity/formal/Predicate.cpp

@@ -214,3 +214,47 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
 	solAssert(stateArgs.size() == stateVars->size(), "");
 	return stateArgs;
 }
+
+vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) const
+{
+	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
+	/// Here we are interested in postInputVars.
+	auto const* function = programFunction();
+	solAssert(function, "");
+
+	auto stateVars = stateVariables();
+	solAssert(stateVars.has_value(), "");
+
+	auto const& inParams = function->parameters();
+
+	vector<string>::const_iterator first = _args.begin() + 1 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size());
+	vector<string>::const_iterator last = first + static_cast<int>(inParams.size());
+
+	solAssert(first >= _args.begin() && first <= _args.end(), "");
+	solAssert(last >= _args.begin() && last <= _args.end(), "");
+
+	vector<string> inValues(first, last);
+	solAssert(inValues.size() == inParams.size(), "");
+	return inValues;
+}
+
+vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) const
+{
+	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
+	/// Here we are interested in outputVars.
+	auto const* function = programFunction();
+	solAssert(function, "");
+
+	auto stateVars = stateVariables();
+	solAssert(stateVars.has_value(), "");
+
+	auto const& inParams = function->parameters();
+
+	vector<string>::const_iterator first = _args.begin() + 1 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2;
+
+	solAssert(first >= _args.begin() && first <= _args.end(), "");
+
+	vector<string> outValues(first, _args.end());
+	solAssert(outValues.size() == function->returnParameters().size(), "");
+	return outValues;
+}

libsolidity/formal/Predicate.h

@@ -96,6 +96,14 @@ public:
 	/// where this summary was reached.
 	std::vector<std::string> summaryStateValues(std::vector<std::string> const& _args) const;
 
+	/// @returns the values of the function input variables from _args at the point
+	/// where this summary was reached.
+	std::vector<std::string> summaryPostInputValues(std::vector<std::string> const& _args) const;
+
+	/// @returns the values of the function output variables from _args at the point
+	/// where this summary was reached.
+	std::vector<std::string> summaryPostOutputValues(std::vector<std::string> const& _args) const;
+
 private:
 	/// The actual SMT expression.
 	smt::SymbolicFunctionVariable m_predicate;