[SMTChecker] Correctly resolve current scope contract in VariableUsage.

Changelog.md

@@ -11,6 +11,7 @@ Compiler Features:
 Bugfixes:
  * AST Import: For constructors, a public visibility is ignored during importing.
  * Error Reporter: Fix handling of carriage return.
+ * SMTChecker: Fix internal error in BMC on resolving virtual functions inside branches.
  * SMTChecker: Fix internal error on ``array.pop`` nested inside 1-tuple.
  * SMTChecker: Fix internal error on ``FixedBytes`` constant initialized with string literal.
  * SMTChecker: Fix internal error on array slices.

libsolidity/formal/SMTEncoder.cpp

@@ -782,7 +782,6 @@ void SMTEncoder::initFunction(FunctionDefinition const& _function)
 	createLocalVariables(_function);
 	m_arrayAssignmentHappened = false;
 	clearIndices(m_currentContract, &_function);
-	m_variableUsage.setCurrentFunction(_function);
 	m_checked = true;
 }
 

libsolidity/formal/VariableUsage.cpp

@@ -21,6 +21,8 @@
 #include <libsolidity/formal/BMC.h>
 #include <libsolidity/formal/SMTEncoder.h>
 
+#include <range/v3/view.hpp>
+
 #include <algorithm>
 
 using namespace std;
@@ -60,7 +62,7 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
 
 void VariableUsage::endVisit(FunctionCall const& _funCall)
 {
-	auto scopeContract = m_currentFunction->annotation().contract;
+	auto scopeContract = currentScopeContract();
 	if (m_inlineFunctionCalls(_funCall, scopeContract, m_currentContract))
 		if (auto funDef = SMTEncoder::functionCallToDefinition(_funCall, scopeContract, m_currentContract))
 			if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end())
@@ -107,3 +109,11 @@ void VariableUsage::checkIdentifier(Identifier const& _identifier)
 			m_touchedVariables.insert(varDecl);
 	}
 }
+
+ContractDefinition const* VariableUsage::currentScopeContract()
+{
+	for (auto&& f: m_callStack | ranges::views::reverse)
+		if (auto fun = dynamic_cast<FunctionDefinition const*>(f))
+			return fun->annotation().contract;
+	return nullptr;
+}

libsolidity/formal/VariableUsage.h

@@ -39,7 +39,6 @@ public:
 	void setFunctionInlining(std::function<bool(FunctionCall const&, ContractDefinition const*, ContractDefinition const*)> _inlineFunctionCalls) { m_inlineFunctionCalls = _inlineFunctionCalls; }
 
 	void setCurrentContract(ContractDefinition const& _contract) { m_currentContract = &_contract; }
-	void setCurrentFunction(FunctionDefinition const& _function) { m_currentFunction = &_function; }
 
 private:
 	void endVisit(Identifier const& _node) override;
@@ -53,11 +52,12 @@ private:
 	/// Checks whether an identifier should be added to touchedVariables.
 	void checkIdentifier(Identifier const& _identifier);
 
+	ContractDefinition const* currentScopeContract();
+
 	std::set<VariableDeclaration const*> m_touchedVariables;
 	std::vector<CallableDeclaration const*> m_callStack;
 	CallableDeclaration const* m_lastCall = nullptr;
 	ContractDefinition const* m_currentContract = nullptr;
-	FunctionDefinition const* m_currentFunction = nullptr;
 
 	std::function<bool(FunctionCall const&, ContractDefinition const*, ContractDefinition const*)> m_inlineFunctionCalls = [](FunctionCall const&, ContractDefinition const*, ContractDefinition const*) { return false; };
 };

test/libsolidity/smtCheckerTests/control_flow/virtual_function_call_inside_branch_1.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract Context {}
+
+contract ERC20 is Context {
+    function approve() public virtual { _approve(); }
+    function _approve() internal virtual {}
+}
+
+contract __unstable__ERC20Owned is ERC20 {
+    function _approve() internal override {
+        if (true) {
+            super._approve();
+        }
+    }
+}

test/libsolidity/smtCheckerTests/control_flow/virtual_function_call_inside_branch_2.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+contract A {
+    function f() internal virtual {
+        v();
+    }
+    function v() internal virtual {
+    }
+}
+
+contract B is A {
+    function f() internal virtual override {
+        super.f();
+    }
+}
+
+contract C is B {
+    function v() internal override {
+        if (0==1)
+            f();
+    }
+}
+// ----
+// Warning 6838: (303-307): BMC: Condition is always false.