Supply scanner to model checker.

chriseth · chriseth · commit e3525b81d096 · 2021-07-14T15:12:10.000+02:00
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
@@ -22,6 +22,9 @@
 
 #include <libsmtutil/SMTPortfolio.h>
 
+#include <liblangutil/CharStream.h>
+#include <liblangutil/CharStreamProvider.h>
+
 #ifdef HAVE_Z3_DLOPEN
 #include <z3_version.h>
 #endif
@@ -38,9 +41,10 @@ BMC::BMC(
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
 	smtutil::SMTSolverChoice _enabledSolvers,
-	ModelCheckerSettings const& _settings
+	ModelCheckerSettings const& _settings,
+	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings),
+	SMTEncoder(_context, _settings, _charStreamProvider),
 	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout)),
 	m_outerErrorReporter(_errorReporter)
 {
@@ -650,7 +654,12 @@ pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
 		if (uf->annotation().type->isValueType())
 		{
 			expressionsToEvaluate.emplace_back(expr(*uf));
-			// TODO expressionNames.push_back(uf->location().text());
+			string expressionName;
+			if (uf->location().hasText())
+				expressionName = m_charStreamProvider.charStream(*uf->location().sourceName).text(
+					uf->location()
+				);
+			expressionNames.push_back(move(expressionName));
 		}
 
 	return {expressionsToEvaluate, expressionNames};
diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h
@@ -63,7 +63,8 @@ class BMC: public SMTEncoder
 		std::map<h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		smtutil::SMTSolverChoice _enabledSolvers,
-		ModelCheckerSettings const& _settings
+		ModelCheckerSettings const& _settings,
+		langutil::CharStreamProvider const& _charStreamProvider
 	);
 
 	void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTargetType>> _solvedTargets);
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
@@ -57,9 +57,10 @@ CHC::CHC(
 	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
 	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
 	SMTSolverChoice _enabledSolvers,
-	ModelCheckerSettings const& _settings
+	ModelCheckerSettings const& _settings,
+	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings),
+	SMTEncoder(_context, _settings, _charStreamProvider),
 	m_outerErrorReporter(_errorReporter),
 	m_enabledSolvers(_enabledSolvers)
 {
@@ -1741,7 +1742,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 				path.emplace_back("State: " + modelMsg);
 		}
 
-		string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
+		string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider);
 
 		list<string> calls;
 		auto dfs = [&](unsigned parent, unsigned node, unsigned depth, auto&& _dfs) -> void {
@@ -1753,7 +1754,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 			if (!pred->isConstructorSummary())
 				for (unsigned v: callGraph[node])
 					_dfs(node, v, depth + 1, _dfs);
-			calls.push_front(string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node)));
+			calls.push_front(string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node), m_charStreamProvider));
 			if (pred->isInternalCall())
 				calls.front() += " -- internal call";
 			else if (pred->isExternalCallTrusted())
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
@@ -57,7 +57,8 @@ class CHC: public SMTEncoder
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		smtutil::SMTSolverChoice _enabledSolvers,
-		ModelCheckerSettings const& _settings
+		ModelCheckerSettings const& _settings,
+		langutil::CharStreamProvider const& _charStreamProvider
 	);
 
 	void analyze(SourceUnit const& _sources);
diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp
@@ -32,6 +32,7 @@ using namespace solidity::frontend;
 
 ModelChecker::ModelChecker(
 	ErrorReporter& _errorReporter,
+	langutil::CharStreamProvider const& _charStreamProvider,
 	map<h256, string> const& _smtlib2Responses,
 	ModelCheckerSettings _settings,
 	ReadCallback::Callback const& _smtCallback,
@@ -40,8 +41,8 @@ ModelChecker::ModelChecker(
 	m_errorReporter(_errorReporter),
 	m_settings(_settings),
 	m_context(),
-	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings),
-	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings)
+	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings, _charStreamProvider),
+	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings, _charStreamProvider)
 {
 }
 
diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h
@@ -49,6 +49,7 @@ class ModelChecker
 	/// should be used, even if all are available. The default choice is to use all.
 	ModelChecker(
 		langutil::ErrorReporter& _errorReporter,
+		langutil::CharStreamProvider const& _charStreamProvider,
 		std::map<solidity::util::h256, std::string> const& _smtlib2Responses,
 		ModelCheckerSettings _settings = ModelCheckerSettings{},
 		ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(),
diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp
@@ -20,6 +20,8 @@
 
 #include <libsolidity/formal/SMTEncoder.h>
 
+#include <liblangutil/CharStreamProvider.h>
+#include <liblangutil/CharStream.h>
 #include <libsolidity/ast/AST.h>
 #include <libsolidity/ast/TypeProvider.h>
 
@@ -196,13 +198,20 @@ bool Predicate::isInterface() const
 	return m_type == PredicateType::Interface;
 }
 
-string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) const
+string Predicate::formatSummaryCall(
+	vector<smtutil::Expression> const& _args,
+	langutil::CharStreamProvider const& _charStreamProvider
+) const
 {
 	solAssert(isSummary(), "");
 
-	//if (auto funCall = programFunctionCall())
-//		return funCall->location().text();
-	// TODO
+	if (auto funCall = programFunctionCall())
+	{
+		if (funCall->location().hasText())
+			return string(_charStreamProvider.charStream(*funCall->location().sourceName).text(funCall->location()));
+		else
+			return {};
+	}
 
 	/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in preInputVars to format the function call,
diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h
@@ -27,6 +27,11 @@
 #include <optional>
 #include <vector>
 
+namespace solidity::langutil
+{
+class CharStreamProvider;
+}
+
 namespace solidity::frontend
 {
 
@@ -142,7 +147,10 @@ class Predicate
 
 	/// @returns a formatted string representing a call to this predicate
 	/// with _args.
-	std::string formatSummaryCall(std::vector<smtutil::Expression> const& _args) const;
+	std::string formatSummaryCall(
+		std::vector<smtutil::Expression> const& _args,
+		langutil::CharStreamProvider const& _charStreamProvider
+	) const;
 
 	/// @returns the values of the state variables from _args at the point
 	/// where this summary was reached.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
@@ -30,6 +30,8 @@
 #include <libsmtutil/SMTPortfolio.h>
 #include <libsmtutil/Helpers.h>
 
+#include <liblangutil/CharStreamProvider.h>
+
 #include <range/v3/view.hpp>
 
 #include <boost/range/adaptors.hpp>
@@ -45,11 +47,13 @@ using namespace solidity::frontend;
 
 SMTEncoder::SMTEncoder(
 	smt::EncodingContext& _context,
-	ModelCheckerSettings const& _settings
+	ModelCheckerSettings const& _settings,
+	langutil::CharStreamProvider const& _charStreamProvider
 ):
 	m_errorReporter(m_smtErrors),
 	m_context(_context),
-	m_settings(_settings)
+	m_settings(_settings),
+	m_charStreamProvider(_charStreamProvider)
 {
 }
 
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
@@ -43,6 +43,7 @@ namespace solidity::langutil
 {
 class ErrorReporter;
 struct SourceLocation;
+class CharStreamProvider;
 }
 
 namespace solidity::frontend
@@ -53,7 +54,8 @@ class SMTEncoder: public ASTConstVisitor
 public:
 	SMTEncoder(
 		smt::EncodingContext& _context,
-		ModelCheckerSettings const& _settings
+		ModelCheckerSettings const& _settings,
+		langutil::CharStreamProvider const& _charStreamProvider
 	);
 
 	/// @returns true if engine should proceed with analysis.
@@ -469,6 +471,10 @@ class SMTEncoder: public ASTConstVisitor
 
 	ModelCheckerSettings const& m_settings;
 
+	/// Character stream for each source,
+	/// used for retrieving source text of expressions for e.g. counter-examples.
+	langutil::CharStreamProvider const& m_charStreamProvider;
+
 	smt::SymbolicState& state();
 };
 
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
@@ -555,7 +555,7 @@ bool CompilerStack::analyze()
 
 		if (noErrors)
 		{
-			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers);
+			ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers);
 			auto allSources = applyMap(m_sourceOrder, [](Source const* _source) { return _source->ast; });
 			modelChecker.enableAllEnginesIfPragmaPresent(allSources);
 			modelChecker.checkRequestedSourcesAndContracts(allSources);
