Merge pull request #5398 from ethereum/smt_model_scanner

Add Scanner function that prints source based on SourceLocation

4 files changed, 15 insertions, 3 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 51b310ae..cc580021 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -37,9 +37,10 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback con
 {
 }
 
-void SMTChecker::analyze(SourceUnit const& _source)
+void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
 {
 	m_variableUsage = make_shared<VariableUsage>(_source);
+	m_scanner = _scanner;
 	if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		_source.accept(*this);
 }
@@ -753,6 +754,7 @@ void SMTChecker::checkCondition(
 	vector<string> expressionNames;
 	if (m_functionPath.size())
 	{
+		solAssert(m_scanner, "");
 		if (_additionalValue)
 		{
 			expressionsToEvaluate.emplace_back(*_additionalValue);
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 376b73fd..a7f955dd 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -25,6 +25,8 @@
 
 #include <libsolidity/interface/ReadFile.h>
 
+#include <libsolidity/parsing/Scanner.h>
+
 #include <unordered_map>
 #include <string>
 #include <vector>
@@ -42,7 +44,7 @@ class SMTChecker: private ASTConstVisitor
 public:
 	SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback);
 
-	void analyze(SourceUnit const& _sources);
+	void analyze(SourceUnit const& _sources, std::shared_ptr<Scanner> const& _scanner);
 
 private:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
@@ -193,6 +195,7 @@ private:
 	std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;
+	std::shared_ptr<Scanner> m_scanner;
 
 	/// Stores the current path of function calls.
 	std::vector<FunctionDefinition const*> m_functionPath;
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index 7aa0faa7..441c7897 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -284,7 +284,7 @@ bool CompilerStack::analyze()
 		{
 			SMTChecker smtChecker(m_errorReporter, m_smtQuery);
 			for (Source const* source: m_sourceOrder)
-				smtChecker.analyze(*source->ast);
+				smtChecker.analyze(*source->ast, source->scanner);
 		}
 	}
 	catch(FatalError const&)
diff --git a/libsolidity/parsing/Scanner.h b/libsolidity/parsing/Scanner.h
index 02e0553f..14eeb66e 100644
--- a/libsolidity/parsing/Scanner.h
+++ b/libsolidity/parsing/Scanner.h
@@ -162,6 +162,13 @@ public:
 	/// Do only use in error cases, they are quite expensive.
 	std::string lineAtPosition(int _position) const { return m_source.lineAtPosition(_position); }
 	std::tuple<int, int> translatePositionToLineColumn(int _position) const { return m_source.translatePositionToLineColumn(_position); }
+	std::string sourceAt(SourceLocation const& _location) const
+	{
+		solAssert(!_location.isEmpty(), "");
+		solAssert(m_sourceName && _location.sourceName, "");
+		solAssert(*m_sourceName == *_location.sourceName, "");
+		return m_source.source().substr(_location.start, _location.end - _location.start);
+	}
 	///@}
 
 private: