Print a warning about function parameter names being used instead of values in SMTChecker (#14832)

Author: pgebal

Diff for: Changelog.md

@@ -23,6 +23,7 @@ Language Features:
 Compiler Features:
  * EVM: Support for the EVM Version "Cancun".
  * SMTChecker: Support `bytes.concat` except when string literals are passed as arguments.
+ * SMTChecker: Print a message that function parameter name was used instead of a concrete value in a counterexample when the concrete value found by the solver is too long to print.
  * Standard JSON Interface: Add experimental support to import EVM assembly in the format used by ``--asm-json``.
  * TypeChecker: Comparison of internal function pointers now yields a warning, as it can produce unexpected results with the legacy pipeline enabled.
 

Diff for: libsolidity/formal/Predicate.cpp

@@ -316,11 +316,14 @@ std::string Predicate::formatSummaryCall(
 
 	auto const& params = fun->parameters();
 	solAssert(params.size() == functionArgsCex.size(), "");
+	bool paramNameInsteadOfValue = false;
 	for (unsigned i = 0; i < params.size(); ++i)
 		if (params.at(i) && functionArgsCex.at(i))
 			functionArgs.emplace_back(*functionArgsCex.at(i));
-		else
+		else {
+			paramNameInsteadOfValue = true;
 			functionArgs.emplace_back(params[i]->name());
+		}
 
 	std::string fName = fun->isConstructor() ? "constructor" :
 		fun->isFallback() ? "fallback" :
@@ -335,7 +338,11 @@ std::string Predicate::formatSummaryCall(
 		solAssert(fun->annotation().contract, "");
 		prefix = fun->annotation().contract->name() + ".";
 	}
-	return prefix + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + txModel;
+
+	std::string summary = prefix + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + txModel;
+	if (paramNameInsteadOfValue)
+		summary += " -- counterexample incomplete; parameter name used instead of value";
+	return summary;
 }
 
 std::vector<std::optional<std::string>> Predicate::summaryStateValues(std::vector<smtutil::Expression> const& _args) const

Diff for: test/libsolidity/smtCheckerTests/types/string_1.sol

@@ -6,5 +6,6 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (77-121): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(s1, s2)
+// Warning 6328: (77-121): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(s1, s2) -- counterexample incomplete; parameter name used instead of value