Merge pull request #7170 from ethereum/smt_fix_other_contract_state_var

[SMTChecker] Fix ICE when inlining functions from different source

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;
 };