Merge pull request #6310 from ethereum/smt_callstack_model

[SMTChecker] Add callstack to model report

Changelog.md

@@ -5,6 +5,7 @@ Language Features:
 
 Compiler Features:
  * Inline Assembly: Issue error when using ``callvalue()`` inside nonpayable function (in the same way that ``msg.value`` already does).
+ * SMTChecker: Show callstack together with model if applicable.
  * Yul Optimizer: Enable stack allocation optimization by default if yul optimizer is active (disable in yulDetails).
 
 

liblangutil/Exceptions.h

@@ -28,6 +28,7 @@
 #include <memory>
 #include <libdevcore/Exceptions.h>
 #include <libdevcore/Assertions.h>
+#include <libdevcore/CommonData.h>
 #include <liblangutil/SourceLocation.h>
 
 namespace langutil
@@ -108,6 +109,11 @@ public:
 		infos.emplace_back(_errMsg, _sourceLocation);
 		return *this;
 	}
+	SecondarySourceLocation& append(SecondarySourceLocation&& _other)
+	{
+		infos += std::move(_other.infos);
+		return *this;
+	}
 
 	/// Limits the number of secondary source locations to 32 and appends a notice to the
 	/// error message.

libsolidity/formal/SMTChecker.cpp

@@ -24,6 +24,7 @@
 #include <libdevcore/StringUtils.h>
 
 #include <boost/range/adaptor/map.hpp>
+#include <boost/range/adaptors.hpp>
 #include <boost/algorithm/string/replace.hpp>
 
 using namespace std;
@@ -105,6 +106,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 	{
 		m_interface->reset();
 		m_pathConditions.clear();
+		m_callStack.clear();
 		m_expressions.clear();
 		m_globalContext.clear();
 		m_uninterpretedTerms.clear();
@@ -495,7 +497,9 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 		visitGasLeft(_funCall);
 		break;
 	case FunctionType::Kind::Internal:
+		m_callStack.push_back(&_funCall);
 		inlineFunctionCall(_funCall);
+		m_callStack.pop_back();
 		break;
 	case FunctionType::Kind::External:
 		resetStateVariables();
@@ -1165,18 +1169,21 @@ void SMTChecker::checkCondition(
 	vector<string> values;
 	tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate);
 
-	string loopComment;
+	string extraComment;
 	if (m_loopExecutionHappened)
-		loopComment =
+		extraComment =
 			"\nNote that some information is erased after the execution of loops.\n"
 			"You can re-introduce information using require().";
 	if (m_arrayAssignmentHappened)
-		loopComment +=
+		extraComment +=
 			"\nNote that array aliasing is not supported,"
 			" therefore all mapping information is erased after"
 			" a mapping local variable/parameter is assigned.\n"
 			"You can re-introduce information using require().";
 
+	SecondarySourceLocation secondaryLocation{};
+	secondaryLocation.append(extraComment, SourceLocation{});
+
 	switch (result)
 	{
 	case smt::CheckResult::SATISFIABLE:
@@ -1195,19 +1202,25 @@ void SMTChecker::checkCondition(
 
 			for (auto const& eval: sortedModel)
 				modelMessage << "  " << eval.first << " = " << eval.second << "\n";
-			m_errorReporter.warning(_location, message.str(), SecondarySourceLocation().append(modelMessage.str(), SourceLocation()).append(loopComment, SourceLocation()));
+			m_errorReporter.warning(
+				_location,
+				message.str(),
+				SecondarySourceLocation().append(modelMessage.str(), SourceLocation{})
+				.append(currentCallStack())
+				.append(move(secondaryLocation))
+			);
 		}
 		else
 		{
 			message << ".";
-			m_errorReporter.warning(_location, message.str(), SecondarySourceLocation().append(loopComment, SourceLocation()));
+			m_errorReporter.warning(_location, message.str(), secondaryLocation);
 		}
 		break;
 	}
 	case smt::CheckResult::UNSATISFIABLE:
 		break;
 	case smt::CheckResult::UNKNOWN:
-		m_errorReporter.warning(_location, _description + " might happen here.", SecondarySourceLocation().append(loopComment, SourceLocation()));
+		m_errorReporter.warning(_location, _description + " might happen here.", secondaryLocation);
 		break;
 	case smt::CheckResult::CONFLICTING:
 		m_errorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
@@ -1540,6 +1553,17 @@ smt::Expression SMTChecker::currentPathConditions()
 	return m_pathConditions.back();
 }
 
+SecondarySourceLocation SMTChecker::currentCallStack()
+{
+	SecondarySourceLocation callStackLocation;
+	if (m_callStack.empty())
+		return callStackLocation;
+	callStackLocation.append("Callstack: ", SourceLocation());
+	for (auto const& call: m_callStack | boost::adaptors::reversed)
+		callStackLocation.append("", call->location());
+	return callStackLocation;
+}
+
 void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e)
 {
 	m_interface->addAssertion(currentPathConditions() && _e);

libsolidity/formal/SMTChecker.h

@@ -229,6 +229,8 @@ private:
 	void popPathCondition();
 	/// Returns the conjunction of all path conditions or True if empty
 	smt::Expression currentPathConditions();
+	/// Returns the current callstack. Used for models.
+	langutil::SecondarySourceLocation currentCallStack();
 	/// Conjoin the current path conditions with the given parameter and add to the solver
 	void addPathConjoinedExpression(smt::Expression const& _e);
 	/// Add to the solver: the given expression implied by the current path conditions
@@ -269,6 +271,8 @@ private:
 
 	/// Stores the current path of function calls.
 	std::vector<FunctionDefinition const*> m_functionPath;
+	/// Stores the current call/invocation path.
+	std::vector<ASTNode const*> m_callStack;
 	/// Returns true if the current function was not visited by
 	/// a function call.
 	bool isRootFunction();