[SMTChecker] Fix ICE when reporting cex concerning state vars from different source files

Changelog.md

@@ -28,6 +28,7 @@ Bugfixes:
  * SMTChecker: Fix internal error when using compound bitwise assignment operators inside branches.
  * SMTChecker: Fix internal error when inlining a function that returns a tuple containing an unsupported type inside a branch.
  * SMTChecker: Fix internal error when inlining functions that use state variables and belong to a different source.
+ * SMTChecker: Fix internal error when reporting counterexamples concerning state variables from different source files.
  * View/Pure Checker: Properly detect state variable access through base class.
  * Yul analyzer: Check availability of data objects already in analysis phase.
  * Yul Optimizer: Fix an issue where memory-accessing code was removed even though ``msize`` was used in the program.

liblangutil/SourceLocation.h

@@ -22,7 +22,9 @@
 
 #pragma once
 
+#include <libdevcore/Assertions.h>
 #include <libdevcore/Common.h> // defines noexcept macro for MSVC
+#include <libdevcore/Exceptions.h>
 #include <liblangutil/CharStream.h>
 #include <memory>
 #include <string>
@@ -31,6 +33,7 @@
 
 namespace langutil
 {
+struct SourceLocationError: virtual dev::Exception {};
 
 /**
  * Representation of an interval of source positions.
@@ -49,6 +52,15 @@ struct SourceLocation
 
 	bool isEmpty() const { return start == -1 && end == -1; }
 
+	std::string text() const
+	{
+		assertThrow(source, SourceLocationError, "Requested text from null source.");
+		assertThrow(!isEmpty(), SourceLocationError, "Requested text from empty source location.");
+		assertThrow(start <= end, SourceLocationError, "Invalid source location.");
+		assertThrow(end <= int(source->source().length()), SourceLocationError, "Invalid source location.");
+		return source->source().substr(start, end - start);
+	}
+
 	/// @returns the smallest SourceLocation that contains both @param _a and @param _b.
 	/// Assumes that @param _a and @param _b refer to the same source (exception: if the source of either one
 	/// is unset, the source of the other will be used for the result, even if that is unset as well).

libsolidity/formal/BMC.cpp

@@ -43,12 +43,10 @@ BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map<h256
 #endif
 }
 
-void BMC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner, set<Expression const*> _safeAssertions)
+void BMC::analyze(SourceUnit const& _source, set<Expression const*> _safeAssertions)
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
-	m_scanner = _scanner;
-
 	m_safeAssertions += move(_safeAssertions);
 	m_context.setSolver(m_interface);
 	m_context.clear();
@@ -542,7 +540,7 @@ pair<vector<smt::Expression>, vector<string>> BMC::modelExpressions()
 		if (uf->annotation().type->isValueType())
 		{
 			expressionsToEvaluate.emplace_back(expr(*uf));
-			expressionNames.push_back(m_scanner->sourceAt(uf->location()));
+			expressionNames.push_back(uf->location().text());
 		}
 
 	return {expressionsToEvaluate, expressionNames};
@@ -717,14 +715,11 @@ void BMC::checkCondition(
 	vector<string> expressionNames;
 	tie(expressionsToEvaluate, expressionNames) = _modelExpressions;
 	if (callStack.size())
-	{
-		solAssert(m_scanner, "");
 		if (_additionalValue)
 		{
 			expressionsToEvaluate.emplace_back(*_additionalValue);
 			expressionNames.push_back(_additionalValueName);
 		}
-	}
 	smt::CheckResult result;
 	vector<string> values;
 	tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate);

libsolidity/formal/BMC.h

@@ -34,7 +34,6 @@
 
 #include <libsolidity/interface/ReadFile.h>
 #include <liblangutil/ErrorReporter.h>
-#include <liblangutil/Scanner.h>
 
 #include <set>
 #include <string>
@@ -56,7 +55,7 @@ class BMC: public SMTEncoder
 public:
 	BMC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
 
-	void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner, std::set<Expression const*> _safeAssertions);
+	void analyze(SourceUnit const& _sources, std::set<Expression const*> _safeAssertions);
 
 	/// This is used if the SMT solver is not directly linked into this binary.
 	/// @returns a list of inputs to the SMT solver that were not part of the argument to

libsolidity/formal/CHC.cpp

@@ -39,12 +39,10 @@ CHC::CHC(smt::EncodingContext& _context, ErrorReporter& _errorReporter):
 {
 }
 
-void CHC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
+void CHC::analyze(SourceUnit const& _source)
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
-	m_scanner = _scanner;
-
 #ifdef HAVE_Z3
 	auto z3Interface = dynamic_pointer_cast<smt::Z3CHCInterface>(m_interface);
 	solAssert(z3Interface, "");

libsolidity/formal/CHC.h

@@ -46,7 +46,7 @@ class CHC: public SMTEncoder
 public:
 	CHC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter);
 
-	void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
+	void analyze(SourceUnit const& _sources);
 
 	std::set<Expression const*> const& safeAssertions() const { return m_safeAssertions; }
 

libsolidity/formal/ModelChecker.cpp

@@ -29,13 +29,13 @@ ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map<h256, string> cons
 {
 }
 
-void ModelChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
+void ModelChecker::analyze(SourceUnit const& _source)
 {
 	if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		return;
 
-	m_chc.analyze(_source, _scanner);
+	m_chc.analyze(_source);
-	m_bmc.analyze(_source, _scanner, m_chc.safeAssertions());
+	m_bmc.analyze(_source, m_chc.safeAssertions());
 }
 
 vector<string> ModelChecker::unhandledQueries()

libsolidity/formal/ModelChecker.h

@@ -28,7 +28,6 @@
 
 #include <libsolidity/interface/ReadFile.h>
 #include <liblangutil/ErrorReporter.h>
-#include <liblangutil/Scanner.h>
 
 namespace langutil
 {
@@ -46,7 +45,7 @@ class ModelChecker
 public:
 	ModelChecker(langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
 
-	void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
+	void analyze(SourceUnit const& _sources);
 
 	/// This is used if the SMT solver is not directly linked into this binary.
 	/// @returns a list of inputs to the SMT solver that were not part of the argument to

libsolidity/formal/SMTEncoder.h

@@ -30,7 +30,6 @@
 #include <libsolidity/ast/ASTVisitor.h>
 #include <libsolidity/interface/ReadFile.h>
 #include <liblangutil/ErrorReporter.h>
-#include <liblangutil/Scanner.h>
 
 #include <string>
 #include <unordered_map>
@@ -231,7 +230,6 @@ protected:
 	/// warning before the others in case it's needed.
 	langutil::ErrorReporter m_errorReporter;
 	langutil::ErrorList m_smtErrors;
-	std::shared_ptr<langutil::Scanner> m_scanner;
 
 	/// Stores the current function/modifier call/invocation path.
 	std::vector<CallStackEntry> m_callStack;

libsolidity/interface/CompilerStack.cpp

@@ -373,7 +373,7 @@ bool CompilerStack::analyze()
 		{
 			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses);
 			for (Source const* source: m_sourceOrder)
-				modelChecker.analyze(*source->ast, source->scanner);
+				modelChecker.analyze(*source->ast);
 			m_unhandledSMTLib2Queries += modelChecker.unhandledQueries();
 		}
 	}

test/libsolidity/SMTChecker.cpp

@@ -257,8 +257,11 @@ BOOST_AUTO_TEST_CASE(import_base)
 		pragma solidity >=0.0;
 		contract Base {
 			uint x;
-			function f() internal {
+			address a;
+			function f() internal returns (uint) {
+				a = address(this);
 				++x;
+				return 2;
 			}
 		}
 	)"},
@@ -268,7 +271,7 @@ BOOST_AUTO_TEST_CASE(import_base)
 		import "base";
 		contract Der is Base {
 			function g(uint y) public {
-				f();
+				x += f();
 				assert(y > x);
 			}
 		}
@@ -328,6 +331,7 @@ BOOST_AUTO_TEST_CASE(import_library)
 
 }
 
+
 BOOST_AUTO_TEST_SUITE_END()
 
 }