Move formatFunctionCallCounterexample from CHC to Predicate

libsolidity/formal/CHC.cpp

@@ -1423,24 +1423,12 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		Predicate const* summaryPredicate = Predicate::predicate(summaryNode.first);
 		solAssert(summaryPredicate, "");
 
-		FunctionDefinition const* calledFun = nullptr;
+		FunctionDefinition const* calledFun = summaryPredicate->programFunction();
-		ContractDefinition const* calledContract = nullptr;
+		ContractDefinition const* calledContract = summaryPredicate->programContract();
-		if (auto const* contract = dynamic_cast<ContractDefinition const*>(summaryPredicate->programNode()))
-		{
-			if (auto const* constructor = contract->constructor())
-				calledFun = constructor;
-			else
-				calledContract = contract;
-		}
-		else if (auto const* fun = dynamic_cast<FunctionDefinition const*>(summaryPredicate->programNode()))
-			calledFun = fun;
-		else
-			solAssert(false, "");
 
 		solAssert((calledFun && !calledContract) || (!calledFun && calledContract), "");
-		auto const& stateVars = calledFun ? stateVariablesIncludingInheritedAndPrivate(*calledFun) : stateVariablesIncludingInheritedAndPrivate(*calledContract);
+		auto stateVars = summaryPredicate->stateVariables();
-		/// calledContract != nullptr implies that the constructor of the analyzed contract is implicit and
+		solAssert(stateVars.has_value(), "");
-		/// therefore takes no parameters.
 
 		/// This summary node is the end of a tx.
 		/// If it is the first summary node seen in this loop, it is the summary
@@ -1450,12 +1438,12 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		{
 			lastTxSeen = true;
 			/// Generate counterexample message local to the failed target.
-			localState = formatStateCounterexample(stateVars, calledFun, summaryNode.second) + "\n";
+			localState = formatStateCounterexample(*stateVars, calledFun, summaryNode.second) + "\n";
 			if (calledFun)
 			{
 				/// The signature of a summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
 				auto const& inParams = calledFun->parameters();
-				unsigned initLocals = stateVars.size() * 2 + 1 + inParams.size();
+				unsigned initLocals = stateVars->size() * 2 + 1 + inParams.size();
 				/// In this loop we are interested in postInputVars.
 				for (unsigned i = initLocals; i < initLocals + inParams.size(); ++i)
 				{
@@ -1477,9 +1465,9 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		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, calledFun, summaryNode.second));
+			path.emplace_back("State: " + formatStateCounterexample(*stateVars, calledFun, summaryNode.second));
 
-		string txCex = calledContract ? "constructor()" : formatFunctionCallCounterexample(stateVars, *calledFun, summaryNode.second);
+		string txCex = summaryPredicate->formatSummaryCall(summaryNode.second);
 		path.emplace_back(txCex);
 
 		/// Recurse on the next interface node which represents the previous transaction
@@ -1527,32 +1515,6 @@ string CHC::formatStateCounterexample(vector<VariableDeclaration const*> const&
 	return boost::algorithm::join(stateCex, ", ");
 }
 
-string CHC::formatFunctionCallCounterexample(vector<VariableDeclaration const*> const& _stateVars, FunctionDefinition const& _function, vector<string> const& _summaryValues)
-{
-	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
-	/// Here we are interested in preInputVars.
-	vector<string>::const_iterator first = _summaryValues.begin() + static_cast<int>(_stateVars.size()) + 1;
-	vector<string>::const_iterator last = first + static_cast<int>(_function.parameters().size());
-	solAssert(first >= _summaryValues.begin() && first <= _summaryValues.end(), "");
-	solAssert(last >= _summaryValues.begin() && last <= _summaryValues.end(), "");
-	vector<string> functionArgsCex(first, last);
-	vector<string> functionArgs;
-
-	auto const& params = _function.parameters();
-	solAssert(params.size() == functionArgsCex.size(), "");
-	for (unsigned i = 0; i < params.size(); ++i)
-		if (params[i]->type()->isValueType())
-			functionArgs.emplace_back(functionArgsCex[i]);
-		else
-			functionArgs.emplace_back(params[i]->name());
-
-	string fName = _function.isConstructor() ? "constructor" :
-		_function.isFallback() ? "fallback" :
-		_function.isReceive() ? "receive" :
-		_function.name();
-	return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")";
-}
-
 string CHC::cex2dot(smtutil::CHCSolverInterface::CexGraph const& _cex)
 {
 	string dot = "digraph {\n";

libsolidity/formal/CHC.h

@@ -226,10 +226,6 @@ private:
 	/// _function = nullptr means the transaction was the deployment of a
 	/// contract without an explicit constructor.
 	std::string formatStateCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, FunctionDefinition const* _function, std::vector<std::string> const& _summaryValues);
-	/// @returns a formatted text representing a call to _function
-	/// with the concrete values for value type parameters and
-	/// the parameter name for reference types.
-	std::string formatFunctionCallCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, FunctionDefinition const& _function, std::vector<std::string> const& _summaryValues);
 
 	/// @returns a DAG in the dot format.
 	/// Used for debugging purposes.

libsolidity/formal/Predicate.cpp

@@ -18,6 +18,8 @@
 
 #include <libsolidity/formal/Predicate.h>
 
+#include <libsolidity/formal/SMTEncoder.h>
+
 #include <libsolidity/ast/AST.h>
 
 #include <boost/algorithm/string/join.hpp>
@@ -87,6 +89,96 @@ void Predicate::newFunctor()
 	m_predicate.increaseIndex();
 }
 
-ASTNode const* Predicate::programNode() const {
+ASTNode const* Predicate::programNode() const
+{
 	return m_node;
 }
+
+ContractDefinition const* Predicate::programContract() const
+{
+	if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_node))
+		if (!contract->constructor())
+			return contract;
+
+	return nullptr;
+}
+
+FunctionDefinition const* Predicate::programFunction() const
+{
+	if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_node))
+	{
+		if (contract->constructor())
+			return contract->constructor();
+		return nullptr;
+	}
+
+	if (auto const* fun = dynamic_cast<FunctionDefinition const*>(m_node))
+		return fun;
+
+	return nullptr;
+}
+
+optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const
+{
+	if (auto const* fun = programFunction())
+		return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun);
+	if (auto const* contract = programContract())
+		return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contract);
+
+	auto const* node = m_node;
+	while (auto const* scopable = dynamic_cast<Scopable const*>(node))
+	{
+		node = scopable->scope();
+		if (auto const* fun = dynamic_cast<FunctionDefinition const*>(node))
+			return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun);
+	}
+
+	return nullopt;
+}
+
+bool Predicate::isSummary() const
+{
+	return functor().name.rfind("summary", 0) == 0;
+}
+
+bool Predicate::isInterface() const
+{
+	return functor().name.rfind("interface", 0) == 0;
+}
+
+string Predicate::formatSummaryCall(vector<string> const& _args) const
+{
+	if (programContract())
+		return "constructor()";
+
+	solAssert(isSummary(), "");
+
+	auto stateVars = stateVariables();
+	solAssert(stateVars.has_value(), "");
+	auto const* fun = programFunction();
+	solAssert(fun, "");
+
+	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
+	/// Here we are interested in preInputVars.
+	vector<string>::const_iterator first = _args.begin() + static_cast<int>(stateVars->size()) + 1;
+	vector<string>::const_iterator last = first + static_cast<int>(fun->parameters().size());
+	solAssert(first >= _args.begin() && first <= _args.end(), "");
+	solAssert(last >= _args.begin() && last <= _args.end(), "");
+	vector<string> functionArgsCex(first, last);
+	vector<string> functionArgs;
+
+	auto const& params = fun->parameters();
+	solAssert(params.size() == functionArgsCex.size(), "");
+	for (unsigned i = 0; i < params.size(); ++i)
+		if (params[i]->type()->isValueType())
+			functionArgs.emplace_back(functionArgsCex[i]);
+		else
+			functionArgs.emplace_back(params[i]->name());
+
+	string fName = fun->isConstructor() ? "constructor" :
+		fun->isFallback() ? "fallback" :
+		fun->isReceive() ? "receive" :
+		fun->name();
+	return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")";
+
+}

libsolidity/formal/Predicate.h

@@ -24,6 +24,7 @@
 #include <libsmtutil/Sorts.h>
 
 #include <map>
+#include <optional>
 #include <vector>
 
 namespace solidity::frontend
@@ -70,6 +71,27 @@ public:
 	/// @returns the program node this predicate represents.
 	ASTNode const* programNode() const;
 
+	/// @returns the ContractDefinition that this predicate represents
+	/// or nullptr otherwise.
+	ContractDefinition const* programContract() const;
+
+	/// @returns the FunctionDefinition that this predicate represents
+	/// or nullptr otherwise.
+	FunctionDefinition const* programFunction() const;
+
+	/// @returns the program state variables in the scope of this predicate.
+	std::optional<std::vector<VariableDeclaration const*>> stateVariables() const;
+
+	/// @returns true if this predicate represents a summary.
+	bool isSummary() const;
+
+	/// @returns true if this predicate represents an interface.
+	bool isInterface() const;
+
+	/// @returns a formatted string representing a call to this predicate
+	/// with _args.
+	std::string formatSummaryCall(std::vector<std::string> const& _args) const;
+
 private:
 	/// The actual SMT expression.
 	smt::SymbolicFunctionVariable m_predicate;