Merge pull request #10685 from ethereum/smt_virtual_functions

[SMTChecker] Fix calls to virtual/overriden functions

Changelog.md

@@ -9,7 +9,7 @@ Compiler Features:
 
 Bugfixes:
  * Code Generator: Fix length check when decoding malformed error data in catch clause.
- * SMTChecker: Fix false negatives in overriding modifiers.
+ * SMTChecker: Fix false negatives in overriding modifiers and functions.
  * SMTChecker: Fix false negatives when analyzing external function calls.
 
 ### 0.8.0 (2020-12-16)

libsolidity/formal/BMC.cpp

@@ -100,9 +100,9 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 	m_errorReporter.clear();
 }
 
-bool BMC::shouldInlineFunctionCall(FunctionCall const& _funCall)
+bool BMC::shouldInlineFunctionCall(FunctionCall const& _funCall, ContractDefinition const* _contract)
 {
-	FunctionDefinition const* funDef = functionCallToDefinition(_funCall);
+	auto [funDef, contextContract] = functionCallToDefinition(_funCall, _contract);
 	if (!funDef || !funDef->isImplemented())
 		return false;
 
@@ -473,8 +473,8 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall)
 
 void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 {
-	solAssert(shouldInlineFunctionCall(_funCall), "");
+	solAssert(shouldInlineFunctionCall(_funCall, m_currentContract), "");
-	FunctionDefinition const* funDef = functionCallToDefinition(_funCall);
+	auto [funDef, contextContract] = functionCallToDefinition(_funCall, m_currentContract);
 	solAssert(funDef, "");
 
 	if (visitedFunction(funDef))
@@ -488,7 +488,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 	}
 	else
 	{
-		initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall));
+		initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall, m_currentContract));
 
 		// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
 		// is that there we don't have `_funCall`.
@@ -498,13 +498,13 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 		popPathCondition();
 	}
 
-	createReturnedExpressions(_funCall);
+	createReturnedExpressions(_funCall, m_currentContract);
 }
 
 void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 {
 	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
-	if (shouldInlineFunctionCall(_funCall))
+	if (shouldInlineFunctionCall(_funCall, m_currentContract))
 		inlineFunctionCall(_funCall);
 	else if (isPublicGetter(_funCall.expression()))
 	{

libsolidity/formal/BMC.h

@@ -73,7 +73,7 @@ public:
 	std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
 
 	/// @returns true if _funCall should be inlined, otherwise false.
-	static bool shouldInlineFunctionCall(FunctionCall const& _funCall);
+	static bool shouldInlineFunctionCall(FunctionCall const& _funCall, ContractDefinition const* _contract);
 
 private:
 	/// AST visitors.

libsolidity/formal/CHC.cpp

@@ -476,7 +476,8 @@ void CHC::endVisit(FunctionCall const& _funCall)
 		break;
 	}
 
-	createReturnedExpressions(_funCall);
+
+	createReturnedExpressions(_funCall, m_currentContract);
 }
 
 void CHC::endVisit(Break const& _break)
@@ -580,18 +581,17 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 {
 	solAssert(m_currentContract, "");
 
-	auto const* function = functionCallToDefinition(_funCall);
+	auto [function, contract] = functionCallToDefinition(_funCall, m_currentContract);
 	if (function)
 	{
 		if (m_currentFunction && !m_currentFunction->isConstructor())
 			m_callGraph[m_currentFunction].insert(function);
 		else
 			m_callGraph[m_currentContract].insert(function);
-		auto const* contract = function->annotation().contract;
 
 		// Libraries can have constants as their "state" variables,
 		// so we need to ensure they were constructed correctly.
-		if (contract->isLibrary())
+		if (function->annotation().contract->isLibrary())
 			m_context.addAssertion(interface(*contract));
 	}
 
@@ -623,7 +623,8 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	auto kind = funType.kind();
 	solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
-	auto const* function = functionCallToDefinition(_funCall);
+	solAssert(m_currentContract, "");
+	auto [function, contextContract] = functionCallToDefinition(_funCall, m_currentContract);
 	if (!function)
 		return;
 
@@ -667,7 +668,8 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 	auto kind = funType.kind();
 	solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
-	auto const* function = functionCallToDefinition(_funCall);
+	solAssert(m_currentContract, "");
+	auto [function, contextContract] = functionCallToDefinition(_funCall, m_currentContract);
 	if (!function)
 		return;
 
@@ -1153,7 +1155,8 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 	auto kind = funType.kind();
 	solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
-	auto const* function = functionCallToDefinition(_funCall);
+	solAssert(m_currentContract, "");
+	auto [function, contextContract] = functionCallToDefinition(_funCall, m_currentContract);
 	if (!function)
 		return smtutil::Expression(true);
 
@@ -1170,19 +1173,19 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 
 	auto const* contract = function->annotation().contract;
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
-	solAssert(kind != FunctionType::Kind::Internal || contract->isLibrary() || contains(hierarchy, contract), "");
+	solAssert(kind != FunctionType::Kind::Internal || contract->isLibrary() || contains(hierarchy, contextContract), "");
 
 	/// If the call is to a library, we use that library as the called contract.
 	/// If the call is to a contract not in the inheritance hierarchy, we also use that as the called contract.
 	/// Otherwise, the call is to some contract in the inheritance hierarchy of the current contract.
 	/// In this case we use current contract as the called one since the interfaces/predicates are different.
-	auto const* calledContract = contains(hierarchy, contract) ?  m_currentContract : contract;
+	auto const* calledContract = contains(hierarchy, contract) ? contextContract : contract;
 	solAssert(calledContract, "");
 
 	bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View;
 
 	args += currentStateVariables(*calledContract);
-	args += symbolicArguments(_funCall);
+	args += symbolicArguments(_funCall, m_currentContract);
 	if (!calledContract->isLibrary() && !usesStaticCall)
 	{
 		state().newState();

libsolidity/formal/SMTEncoder.cpp

@@ -744,6 +744,7 @@ void SMTEncoder::initContract(ContractDefinition const& _contract)
 	m_context.pushSolver();
 	createStateVariables(_contract);
 	clearIndices(m_currentContract, nullptr);
+	m_variableUsage.setCurrentContract(_contract);
 }
 
 void SMTEncoder::initFunction(FunctionDefinition const& _function)
@@ -2598,26 +2599,43 @@ string SMTEncoder::extraComment()
 	return extra;
 }
 
-FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall const& _funCall)
+pair<FunctionDefinition const*, ContractDefinition const*> SMTEncoder::functionCallToDefinition(FunctionCall const& _funCall, ContractDefinition const* _contract)
 {
 	if (*_funCall.annotation().kind != FunctionCallKind::FunctionCall)
-		return nullptr;
+		return {};
 
-	FunctionDefinition const* funDef = nullptr;
 	Expression const* calledExpr = &_funCall.expression();
-
 	if (TupleExpression const* fun = dynamic_cast<TupleExpression const*>(calledExpr))
 	{
 		solAssert(fun->components().size() == 1, "");
 		calledExpr = innermostTuple(*calledExpr);
 	}
 
-	if (Identifier const* fun = dynamic_cast<Identifier const*>(calledExpr))
+	auto resolveVirtual = [&](auto const* _ref) -> pair<FunctionDefinition const*, ContractDefinition const*> {
-		funDef = dynamic_cast<FunctionDefinition const*>(fun->annotation().referencedDeclaration);
+		VirtualLookup lookup = *_ref->annotation().requiredLookup;
-	else if (MemberAccess const* fun = dynamic_cast<MemberAccess const*>(calledExpr))
+		solAssert(_contract || lookup == VirtualLookup::Static, "No contract context provided for function lookup resolution!");
-		funDef = dynamic_cast<FunctionDefinition const*>(fun->annotation().referencedDeclaration);
+		auto funDef = dynamic_cast<FunctionDefinition const*>(_ref->annotation().referencedDeclaration);
+		if (!funDef)
+			return {funDef, _contract};
+		auto contextContract = _contract;
+		if (lookup == VirtualLookup::Virtual)
+			funDef = &funDef->resolveVirtual(*_contract);
+		else if (lookup == VirtualLookup::Super)
+		{
+			auto super = _contract->superContract(*_contract);
+			solAssert(super, "Super contract not available.");
+			funDef = &funDef->resolveVirtual(*_contract, super);
+			contextContract = super;
+		}
+		return {funDef, contextContract};
+	};
 
-	return funDef;
+	if (Identifier const* fun = dynamic_cast<Identifier const*>(calledExpr))
+		return resolveVirtual(fun);
+	else if (MemberAccess const* fun = dynamic_cast<MemberAccess const*>(calledExpr))
+		return resolveVirtual(fun);
+
+	return {};
 }
 
 vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
@@ -2798,9 +2816,9 @@ set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
 	return ABIFunctions(_node).abiCalls;
 }
 
-void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
+void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contract)
 {
-	FunctionDefinition const* funDef = functionCallToDefinition(_funCall);
+	auto [funDef, contextContract] = functionCallToDefinition(_funCall, _contract);
 	if (!funDef)
 		return;
 
@@ -2826,18 +2844,18 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
 		defineExpr(_funCall, currentValue(*returnParams.front()));
 }
 
-vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall)
+vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contract)
 {
-	auto const* function = functionCallToDefinition(_funCall);
+	auto [funDef, contextContract] = functionCallToDefinition(_funCall, _contract);
-	solAssert(function, "");
+	solAssert(funDef, "");
 
 	vector<smtutil::Expression> args;
 	Expression const* calledExpr = &_funCall.expression();
-	auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
+	auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
 	solAssert(funType, "");
 
 	vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();
-	auto const& functionParams = function->parameters();
+	auto functionParams = funDef->parameters();
 	unsigned firstParam = 0;
 	if (funType->bound())
 	{

libsolidity/formal/SMTEncoder.h

@@ -69,7 +69,7 @@ public:
 
 	/// @returns the FunctionDefinition of a FunctionCall
 	/// if possible or nullptr.
-	static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall);
+	static std::pair<FunctionDefinition const*, ContractDefinition const*> functionCallToDefinition(FunctionCall const& _funCall, ContractDefinition const* _contract = nullptr);
 
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
@@ -331,12 +331,12 @@ protected:
 
 	/// Creates symbolic expressions for the returned values
 	/// and set them as the components of the symbolic tuple.
-	void createReturnedExpressions(FunctionCall const& _funCall);
+	void createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contract);
 
 	/// @returns the symbolic arguments for a function call,
 	/// taking into account bound functions and
 	/// type conversion.
-	std::vector<smtutil::Expression> symbolicArguments(FunctionCall const& _funCall);
+	std::vector<smtutil::Expression> symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contract);
 
 	/// @returns a note to be added to warnings.
 	std::string extraComment();

libsolidity/formal/VariableUsage.cpp

@@ -60,13 +60,13 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
 
 void VariableUsage::endVisit(FunctionCall const& _funCall)
 {
-	if (m_inlineFunctionCalls(_funCall))
+	if (m_inlineFunctionCalls(_funCall, m_currentContract))
-		if (auto funDef = SMTEncoder::functionCallToDefinition(_funCall))
+		if (
-		{
+			auto [funDef, contextContract] = SMTEncoder::functionCallToDefinition(_funCall, m_currentContract);
-			solAssert(funDef, "");
+			funDef
+		)
 			if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end())
 				funDef->accept(*this);
-		}
 }
 
 bool VariableUsage::visit(FunctionDefinition const& _function)

libsolidity/formal/VariableUsage.h

@@ -36,7 +36,9 @@ public:
 	std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node, std::vector<CallableDeclaration const*> const& _outerCallstack);
 
 	/// Sets whether to inline function calls.
-	void setFunctionInlining(std::function<bool(FunctionCall const&)> _inlineFunctionCalls) { m_inlineFunctionCalls = _inlineFunctionCalls; }
+	void setFunctionInlining(std::function<bool(FunctionCall const&, ContractDefinition const*)> _inlineFunctionCalls) { m_inlineFunctionCalls = _inlineFunctionCalls; }
+
+	void setCurrentContract(ContractDefinition const& _contract) { m_currentContract = &_contract; }
 
 private:
 	void endVisit(Identifier const& _node) override;
@@ -53,8 +55,9 @@ private:
 	std::set<VariableDeclaration const*> m_touchedVariables;
 	std::vector<CallableDeclaration const*> m_callStack;
 	CallableDeclaration const* m_lastCall = nullptr;
+	ContractDefinition const* m_currentContract = nullptr;
 
-	std::function<bool(FunctionCall const&)> m_inlineFunctionCalls = [](FunctionCall const&) { return false; };
+	std::function<bool(FunctionCall const&, ContractDefinition const*)> m_inlineFunctionCalls = [](FunctionCall const&, ContractDefinition const*) { return false; };
 };
 
 }

test/libsolidity/smtCheckerTests/functions/super_function_assert.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+contract A {
+	int x = 0;
+
+	function f() virtual internal {
+		x = 2;
+	}
+
+	function proxy() public {
+		f();
+	}
+}
+
+contract C is A {
+	function f() internal virtual override {
+		super.f();
+		assert(x == 2);
+		assert(x == 3); // should fail
+	}
+}
+
+contract D is C {
+
+	function f() internal override {
+		super.f();
+		assert(x == 2);
+		assert(x == 3); // should fail
+	}
+}
+// ----
+// Warning 6328: (237-251): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nproxy()
+// Warning 6328: (360-374): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nproxy()

test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+contract A {
+    int x = 0;
+
+    function f() virtual internal view {
+        assert(x == 0);
+    }
+
+    function proxy() public view {
+        f();
+    }
+}
+
+contract C is A {
+
+    function f() internal view override {
+        assert(x == 1);
+    }
+}
+// ----
+// Warning 6328: (259-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nproxy()