From 94e250613265afdc499477ed05634d080cc47437 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 28 Oct 2020 18:13:40 +0000
Subject: [PATCH] Fix inherited state vars for BMC

---
 Changelog.md                                     |  1 +
 libsolidity/ast/AST.cpp                          | 10 ----------
 libsolidity/ast/AST.h                            |  1 -
 libsolidity/formal/SMTEncoder.cpp                |  4 ++--
 .../smtCheckerTests/imports/private_vars.sol     | 16 ++++++++++++++++
 5 files changed, 19 insertions(+), 13 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/imports/private_vars.sol

diff --git a/Changelog.md b/Changelog.md
index 06ffd5f7c..6cf856712 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -12,6 +12,7 @@ Bugfixes:
  * SMTChecker: Fix internal error when assigning state variable via contract's name.
  * SMTChecker: Fix incorrect counterexamples reported by the CHC engine.
  * SMTChecker: Fix false negative in modifier applied multiple times.
+ * SMTChecker: Fix internal error in the BMC engine when inherited contract from a different source unit has private state variables.
  * Code generator: Fix missing creation dependency tracking for abstract contracts.
 
 
diff --git a/libsolidity/ast/AST.cpp b/libsolidity/ast/AST.cpp
index e69f97887..188562576 100644
--- a/libsolidity/ast/AST.cpp
+++ b/libsolidity/ast/AST.cpp
@@ -84,16 +84,6 @@ 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;
-}
-
 bool ContractDefinition::derivesFrom(ContractDefinition const& _base) const
 {
 	return util::contains(annotation().linearizedBaseContracts, &_base);
diff --git a/libsolidity/ast/AST.h b/libsolidity/ast/AST.h
index f3a79fcb0..87a4e826a 100644
--- a/libsolidity/ast/AST.h
+++ b/libsolidity/ast/AST.h
@@ -500,7 +500,6 @@ 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); }
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 210fe6af2..bb94def0c 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1973,7 +1973,7 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
 
 void SMTEncoder::createStateVariables(ContractDefinition const& _contract)
 {
-	for (auto var: _contract.stateVariablesIncludingInherited())
+	for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
 		createVariable(*var);
 }
 
@@ -2257,7 +2257,7 @@ void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
 void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
 {
 	solAssert(_contract, "");
-	for (auto var: _contract->stateVariablesIncludingInherited())
+	for (auto var: stateVariablesIncludingInheritedAndPrivate(*_contract))
 		m_context.variable(*var)->resetIndex();
 	if (_function)
 	{
diff --git a/test/libsolidity/smtCheckerTests/imports/private_vars.sol b/test/libsolidity/smtCheckerTests/imports/private_vars.sol
new file mode 100644
index 000000000..c17cdb46f
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/imports/private_vars.sol
@@ -0,0 +1,16 @@
+==== Source: ERC20.sol ====
+pragma experimental SMTChecker;
+contract ERC20 {
+    uint256 private a;
+    function f() internal virtual {
+        a = 2;
+    }
+}
+==== Source: Token.sol ====
+pragma experimental SMTChecker;
+import "ERC20.sol";
+contract Token is ERC20 {
+    constructor() {
+      f();
+    }
+}