[SMTChecker] Fix ICE when inlining functions that use state vars and are in a different source

Changelog.md

@@ -27,6 +27,7 @@ Bugfixes:
  * SMTChecker: Fix pointer knowledge erasing in loops.
  * 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.
  * 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.

libsolidity/ast/AST.cpp

@@ -109,6 +109,16 @@ TypePointer ImportDirective::type() const
 	return TypeProvider::module(*annotation().sourceUnit);
 }
 
+vector<VariableDeclaration const*> ContractDefinition::stateVariablesIncludingInherited() const
+{
+	vector<VariableDeclaration const*> stateVars;
+	for (auto const& contract: annotation().linearizedBaseContracts)
+		for (auto var: contract->stateVariables())
+			if (*contract == *this || var->isVisibleInDerivedContracts())
+				stateVars.push_back(var);
+	return stateVars;
+}
+
 map<FixedHash<4>, FunctionTypePointer> ContractDefinition::interfaceFunctions() const
 {
 	auto exportedFunctionList = interfaceFunctionList();

libsolidity/ast/AST.h

@@ -396,6 +396,7 @@ public:
 	std::vector<StructDefinition const*> definedStructs() const { return filteredNodes<StructDefinition>(m_subNodes); }
 	std::vector<EnumDefinition const*> definedEnums() const { return filteredNodes<EnumDefinition>(m_subNodes); }
 	std::vector<VariableDeclaration const*> stateVariables() const { return filteredNodes<VariableDeclaration>(m_subNodes); }
+	std::vector<VariableDeclaration const*> stateVariablesIncludingInherited() const;
 	std::vector<ModifierDefinition const*> functionModifiers() const { return filteredNodes<ModifierDefinition>(m_subNodes); }
 	std::vector<FunctionDefinition const*> definedFunctions() const { return filteredNodes<FunctionDefinition>(m_subNodes); }
 	std::vector<EventDefinition const*> events() const { return filteredNodes<EventDefinition>(m_subNodes); }

libsolidity/formal/BMC.cpp

@@ -120,8 +120,20 @@ bool BMC::visit(ContractDefinition const& _contract)
 	return true;
 }
 
+void BMC::endVisit(ContractDefinition const& _contract)
+{
+	SMTEncoder::endVisit(_contract);
+}
+
 bool BMC::visit(FunctionDefinition const& _function)
 {
+	auto contract = dynamic_cast<ContractDefinition const*>(_function.scope());
+	solAssert(contract, "");
+	solAssert(m_currentContract, "");
+	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
+	if (find(hierarchy.begin(), hierarchy.end(), contract) == hierarchy.end())
+		initializeStateVariables(*contract);
+
 	if (m_callStack.empty())
 		reset();
 

libsolidity/formal/BMC.h

@@ -74,6 +74,7 @@ private:
 	/// or checked are visited.
 	//@{
 	bool visit(ContractDefinition const& _node) override;
+	void endVisit(ContractDefinition const& _node) override;
 	bool visit(FunctionDefinition const& _node) override;
 	void endVisit(FunctionDefinition const& _node) override;
 	bool visit(IfStatement const& _node) override;

libsolidity/formal/SMTEncoder.cpp

@@ -36,16 +36,19 @@ SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
 
 bool SMTEncoder::visit(ContractDefinition const& _contract)
 {
-	for (auto const& contract: _contract.annotation().linearizedBaseContracts)
-		for (auto var: contract->stateVariables())
-			if (*contract == _contract || var->isVisibleInDerivedContracts())
-				createVariable(*var);
+	solAssert(m_currentContract == nullptr, "");
+	m_currentContract = &_contract;
+
+	initializeStateVariables(_contract);
 	return true;
 }
 
-void SMTEncoder::endVisit(ContractDefinition const&)
+void SMTEncoder::endVisit(ContractDefinition const& _contract)
 {
 	m_context.resetAllVariables();
+
+	solAssert(m_currentContract == &_contract, "");
+	m_currentContract = nullptr;
 }
 
 void SMTEncoder::endVisit(VariableDeclaration const& _varDecl)
@@ -1158,6 +1161,12 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
 			}
 }
 
+void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract)
+{
+	for (auto var: _contract.stateVariablesIncludingInherited())
+		createVariable(*var);
+}
+
 void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
 {
 	for (auto const& variable: _function.localVariables())

libsolidity/formal/SMTEncoder.h

@@ -156,6 +156,7 @@ protected:
 
 	using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
 
+	void initializeStateVariables(ContractDefinition const& _contract);
 	void initializeLocalVariables(FunctionDefinition const& _function);
 	void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smt::Expression> const& _callArgs);
 	void resetStateVariables();
@@ -246,6 +247,8 @@ protected:
 	/// Needs to be a stack because of function calls.
 	std::vector<int> m_modifierDepthStack;
 
+	ContractDefinition const* m_currentContract = nullptr;
+
 	/// Stores the context of the encoding.
 	smt::EncodingContext& m_context;
 };

test/libsolidity/SMTChecker.cpp

@@ -19,6 +19,7 @@
  */
 
 #include <test/libsolidity/AnalysisFramework.h>
+#include <test/Options.h>
 
 #include <boost/test/unit_test.hpp>
 
@@ -248,6 +249,85 @@ BOOST_AUTO_TEST_CASE(mod)
 	CHECK_SUCCESS_NO_WARNINGS(text);
 }
 
+BOOST_AUTO_TEST_CASE(import_base)
+{
+	CompilerStack c;
+	c.setSources({
+	{"base", R"(
+		pragma solidity >=0.0;
+		contract Base {
+			uint x;
+			function f() internal {
+				++x;
+			}
+		}
+	)"},
+	{"der", R"(
+		pragma solidity >=0.0;
+		pragma experimental SMTChecker;
+		import "base";
+		contract Der is Base {
+			function g(uint y) public {
+				f();
+				assert(y > x);
+			}
+		}
+	)"}
+	});
+	c.setEVMVersion(dev::test::Options::get().evmVersion());
+	BOOST_CHECK(c.compile());
+
+	unsigned asserts = 0;
+	for (auto const& e: c.errors())
+	{
+		string const* msg = e->comment();
+		BOOST_REQUIRE(msg);
+		if (msg->find("Assertion violation") != string::npos)
+			++asserts;
+	}
+	BOOST_CHECK_EQUAL(asserts, 1);
+}
+
+BOOST_AUTO_TEST_CASE(import_library)
+{
+	CompilerStack c;
+	c.setSources({
+	{"lib", R"(
+		pragma solidity >=0.0;
+		library L {
+			uint constant one = 1;
+			function f() internal pure returns (uint) {
+				return one;
+			}
+		}
+	)"},
+	{"c", R"(
+		pragma solidity >=0.0;
+		pragma experimental SMTChecker;
+		import "lib";
+		contract C {
+			function g(uint x) public pure {
+				uint y = L.f();
+				assert(x > y);
+			}
+		}
+	)"}
+	});
+	c.setEVMVersion(dev::test::Options::get().evmVersion());
+	BOOST_CHECK(c.compile());
+
+	unsigned asserts = 0;
+	for (auto const& e: c.errors())
+	{
+		string const* msg = e->comment();
+		BOOST_REQUIRE(msg);
+		if (msg->find("Assertion violation") != string::npos)
+			++asserts;
+	}
+	BOOST_CHECK_EQUAL(asserts, 1);
+
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 }