[SMTChecker] Fix super and virtual

libsolidity/formal/BMC.cpp

@@ -101,9 +101,13 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 	m_errorReporter.clear();
 }
 
-bool BMC::shouldInlineFunctionCall(FunctionCall const& _funCall, ContractDefinition const* _contract)
+bool BMC::shouldInlineFunctionCall(
+	FunctionCall const& _funCall,
+	ContractDefinition const* _scopeContract,
+	ContractDefinition const* _contextContract
+)
 {
-	auto [funDef, contextContract] = functionCallToDefinition(_funCall, _contract);
+	auto funDef = functionCallToDefinition(_funCall, _scopeContract, _contextContract);
 	if (!funDef || !funDef->isImplemented())
 		return false;
 
@@ -508,8 +512,8 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall)
 
 void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 {
-	solAssert(shouldInlineFunctionCall(_funCall, m_currentContract), "");
-	auto [funDef, contextContract] = functionCallToDefinition(_funCall, m_currentContract);
+	solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), "");
+	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
 	solAssert(funDef, "");
 
 	if (visitedFunction(funDef))
@@ -541,7 +545,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 {
 	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
-	if (shouldInlineFunctionCall(_funCall, m_currentContract))
+	if (shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract))
 		inlineFunctionCall(_funCall);
 	else if (isPublicGetter(_funCall.expression()))
 	{

libsolidity/formal/BMC.h

@@ -74,7 +74,13 @@ 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, ContractDefinition const* _contract);
+	/// @param _scopeContract The contract that contains the current function being analyzed.
+	/// @param _contextContract The most derived contract, currently being analyzed.
+	static bool shouldInlineFunctionCall(
+		FunctionCall const& _funCall,
+		ContractDefinition const* _scopeContract,
+		ContractDefinition const* _contextContract
+	);
 
 private:
 	/// AST visitors.

libsolidity/formal/CHC.cpp

@@ -254,16 +254,17 @@ void CHC::endVisit(FunctionDefinition const& _function)
 	// Query placeholders for constructors are not created here because
 	// of contracts without constructors.
 	// Instead, those are created in endVisit(ContractDefinition).
-	if (!_function.isConstructor())
+	if (
+		!_function.isConstructor() &&
+		_function.isPublic() &&
+		contractFunctions(*m_currentContract).count(&_function)
+	)
 	{
 		auto sum = summary(_function);
 		auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
-		if (_function.isPublic())
-		{
-			auto txConstraints = m_context.state().txConstraints(_function);
-			m_queryPlaceholders[&_function].push_back({txConstraints && sum, errorFlag().currentValue(), ifacePre});
-			connectBlocks(ifacePre, interface(), txConstraints && sum && errorFlag().currentValue() == 0);
-		}
+		auto txConstraints = m_context.state().txConstraints(_function);
+		m_queryPlaceholders[&_function].push_back({txConstraints && sum, errorFlag().currentValue(), ifacePre});
+		connectBlocks(ifacePre, interface(), txConstraints && sum && errorFlag().currentValue() == 0);
 	}
 
 	m_currentFunction = nullptr;
@@ -622,7 +623,8 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 {
 	solAssert(m_currentContract, "");
 
-	auto [function, contract] = functionCallToDefinition(_funCall, m_currentContract);
+	auto scopeContract = currentScopeContract();
+	auto function = functionCallToDefinition(_funCall, scopeContract, m_currentContract);
 	if (function)
 	{
 		if (m_currentFunction && !m_currentFunction->isConstructor())
@@ -633,7 +635,7 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 		// Libraries can have constants as their "state" variables,
 		// so we need to ensure they were constructed correctly.
 		if (function->annotation().contract->isLibrary())
-			m_context.addAssertion(interface(*contract));
+			m_context.addAssertion(interface(*scopeContract));
 	}
 
 	m_context.addAssertion(predicate(_funCall));
@@ -665,7 +667,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
 	solAssert(m_currentContract, "");
-	auto [function, contextContract] = functionCallToDefinition(_funCall, m_currentContract);
+	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
 	if (!function)
 		return;
 
@@ -721,7 +723,7 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 	solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
 	solAssert(m_currentContract, "");
-	auto [function, contextContract] = functionCallToDefinition(_funCall, m_currentContract);
+	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
 	if (!function)
 		return;
 
@@ -959,7 +961,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 			auto const& iface = *m_nondetInterfaces.at(contract);
 			addRule(smtutil::Expression::implies(errorFlag().currentValue() == 0, smt::nondetInterface(iface, *contract, m_context, 0, 0)), "base_nondet");
 
-			for (auto const* function: contractFunctions(*contract))
+			auto const& resolved = contractFunctions(*contract);
+			for (auto const* function: contractFunctionsWithoutVirtual(*contract))
 			{
 				for (auto var: function->parameters())
 					createVariable(*var);
@@ -970,7 +973,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 
 				m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));
 
-				if (!function->isConstructor() && function->isPublic())
+				if (!function->isConstructor() && function->isPublic() && resolved.count(function))
 				{
 					auto state1 = stateVariablesAtIndex(1, *contract);
 					auto state2 = stateVariablesAtIndex(2, *contract);
@@ -1215,7 +1218,8 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 	solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
 	solAssert(m_currentContract, "");
-	auto [function, contextContract] = functionCallToDefinition(_funCall, m_currentContract);
+	auto scopeContract = currentScopeContract();
+	auto function = functionCallToDefinition(_funCall, scopeContract, m_currentContract);
 	if (!function)
 		return smtutil::Expression(true);
 
@@ -1232,13 +1236,13 @@ 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, contextContract), "");
+	solAssert(kind != FunctionType::Kind::Internal || contract->isLibrary() || contains(hierarchy, contract), "");
 
 	/// 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) ? contextContract : contract;
+	auto const* calledContract = contains(hierarchy, contract) ? m_currentContract : contract;
 	solAssert(calledContract, "");
 
 	bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View;

libsolidity/formal/SMTEncoder.cpp

@@ -30,6 +30,8 @@
 #include <libsmtutil/SMTPortfolio.h>
 #include <libsmtutil/Helpers.h>
 
+#include <range/v3/view.hpp>
+
 #include <boost/range/adaptors.hpp>
 #include <boost/range/adaptor/reversed.hpp>
 
@@ -112,7 +114,7 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
 	// the constructor.
 	// Constructors are visited as part of the constructor
 	// hierarchy inlining.
-	for (auto const* function: contractFunctions(_contract))
+	for (auto const* function: contractFunctionsWithoutVirtual(_contract))
 		if (!function->isConstructor())
 			function->accept(*this);
 
@@ -776,6 +778,7 @@ void SMTEncoder::initFunction(FunctionDefinition const& _function)
 	createLocalVariables(_function);
 	m_arrayAssignmentHappened = false;
 	clearIndices(m_currentContract, &_function);
+	m_variableUsage.setCurrentFunction(_function);
 	m_checked = true;
 }
 
@@ -2534,6 +2537,14 @@ bool SMTEncoder::visitedFunction(FunctionDefinition const* _funDef)
 	return false;
 }
 
+ContractDefinition const* SMTEncoder::currentScopeContract()
+{
+	for (auto&& f: m_callStack | ranges::views::reverse | ranges::views::keys)
+		if (auto fun = dynamic_cast<FunctionDefinition const*>(f))
+			return fun->annotation().contract;
+	return nullptr;
+}
+
 SMTEncoder::VariableIndices SMTEncoder::copyVariableIndices()
 {
 	VariableIndices indices;
@@ -2678,7 +2689,11 @@ string SMTEncoder::extraComment()
 	return extra;
 }
 
-pair<FunctionDefinition const*, ContractDefinition const*> SMTEncoder::functionCallToDefinition(FunctionCall const& _funCall, ContractDefinition const* _contract)
+FunctionDefinition const* SMTEncoder::functionCallToDefinition(
+	FunctionCall const& _funCall,
+	ContractDefinition const* _scopeContract,
+	ContractDefinition const* _contextContract
+)
 {
 	if (*_funCall.annotation().kind != FunctionCallKind::FunctionCall)
 		return {};
@@ -2690,32 +2705,27 @@ pair<FunctionDefinition const*, ContractDefinition const*> SMTEncoder::functionC
 		calledExpr = innermostTuple(*calledExpr);
 	}
 
-	auto resolveVirtual = [&](auto const* _ref) -> pair<FunctionDefinition const*, ContractDefinition const*> {
+	auto resolveVirtual = [&](auto const* _ref) -> FunctionDefinition const* {
 		VirtualLookup lookup = *_ref->annotation().requiredLookup;
-		solAssert(_contract || lookup == VirtualLookup::Static, "No contract context provided for function lookup resolution!");
+		solAssert(_contextContract || lookup == VirtualLookup::Static, "No contract context provided for function lookup resolution!");
 		auto funDef = dynamic_cast<FunctionDefinition const*>(_ref->annotation().referencedDeclaration);
 		if (!funDef)
-			return {funDef, _contract};
-		ContractDefinition const* contextContract = nullptr;
+			return funDef;
 		switch (lookup)
 		{
 		case VirtualLookup::Virtual:
-			funDef = &funDef->resolveVirtual(*_contract);
-			contextContract = _contract;
-			break;
+			return &(funDef->resolveVirtual(*_contextContract));
 		case VirtualLookup::Super:
 		{
-			auto super = _contract->superContract(*_contract);
+			solAssert(_scopeContract, "");
+			auto super = _scopeContract->superContract(*_contextContract);
 			solAssert(super, "Super contract not available.");
-			funDef = &funDef->resolveVirtual(*_contract, super);
-			contextContract = super;
-			break;
+			return &funDef->resolveVirtual(*_contextContract, super);
 		}
 		case VirtualLookup::Static:
-			contextContract = funDef->annotation().contract;
-			break;
+			return funDef;
 		}
-		return {funDef, contextContract};
+		solAssert(false, "");
 	};
 
 	if (Identifier const* fun = dynamic_cast<Identifier const*>(calledExpr))
@@ -2810,11 +2820,12 @@ ModifierDefinition const* SMTEncoder::resolveModifierInvocation(ModifierInvocati
 	return modifier;
 }
 
-vector<FunctionDefinition const*> const& SMTEncoder::contractFunctions(ContractDefinition const& _contract)
+set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contractFunctions(ContractDefinition const& _contract)
 {
 	if (!m_contractFunctions.count(&_contract))
 	{
-		vector<FunctionDefinition const *> resolvedFunctions = _contract.definedFunctions();
+		auto const& functions = _contract.definedFunctions();
+		set<FunctionDefinition const*, ASTNode::CompareByID> resolvedFunctions(begin(functions), end(functions));
 		for (auto const* base: _contract.annotation().linearizedBaseContracts)
 		{
 			if (base == &_contract)
@@ -2836,7 +2847,7 @@ vector<FunctionDefinition const*> const& SMTEncoder::contractFunctions(ContractD
 						break;
 					}
 				if (!overridden)
-					resolvedFunctions.push_back(baseFunction);
+					resolvedFunctions.insert(baseFunction);
 			}
 		}
 		m_contractFunctions.emplace(&_contract, move(resolvedFunctions));
@@ -2844,6 +2855,22 @@ vector<FunctionDefinition const*> const& SMTEncoder::contractFunctions(ContractD
 	return m_contractFunctions.at(&_contract);
 }
 
+set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contractFunctionsWithoutVirtual(ContractDefinition const& _contract)
+{
+	if (!m_contractFunctionsWithoutVirtual.count(&_contract))
+	{
+		auto allFunctions = contractFunctions(_contract);
+		for (auto const* base: _contract.annotation().linearizedBaseContracts)
+			for (auto const* baseFun: base->definedFunctions())
+				if (!baseFun->isConstructor())
+					allFunctions.insert(baseFun);
+
+		m_contractFunctionsWithoutVirtual.emplace(&_contract, move(allFunctions));
+
+	}
+	return m_contractFunctionsWithoutVirtual.at(&_contract);
+}
+
 SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
 {
 	for (auto const* s = &_scopable; s; s = dynamic_cast<Scopable const*>(s->scope()))
@@ -2926,9 +2953,9 @@ set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
 	return ABIFunctions(_node).abiCalls;
 }
 
-void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contract)
+void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
 {
-	auto [funDef, contextContract] = functionCallToDefinition(_funCall, _contract);
+	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
 	if (!funDef)
 		return;
 
@@ -2954,9 +2981,9 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, Contrac
 		defineExpr(_funCall, currentValue(*returnParams.front()));
 }
 
-vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contract)
+vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
 {
-	auto [funDef, contextContract] = functionCallToDefinition(_funCall, _contract);
+	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
 	solAssert(funDef, "");
 
 	vector<smtutil::Expression> args;

libsolidity/formal/SMTEncoder.h

@@ -70,7 +70,19 @@ public:
 
 	/// @returns the FunctionDefinition of a FunctionCall
 	/// if possible or nullptr.
-	static std::pair<FunctionDefinition const*, ContractDefinition const*> functionCallToDefinition(FunctionCall const& _funCall, ContractDefinition const* _contract = nullptr);
+	/// @param _scopeContract is the contract that contains the function currently being
+	///        analyzed, if applicable.
+	/// @param _contextContract is the most derived contract currently being analyzed.
+	/// The difference between the two parameters appears in the case of inheritance.
+	/// Let A and B be two contracts so that B derives from A, and A defines a function `f`
+	/// that `B` does not override. Function `f` is visited twice:
+	/// - Once when A is the most derived contract, where both _scopeContract and _contextContract are A.
+	/// - Once when B is the most derived contract, where _scopeContract is A and _contextContract is B.
+	static FunctionDefinition const* functionCallToDefinition(
+		FunctionCall const& _funCall,
+		ContractDefinition const* _scopeContract,
+		ContractDefinition const* _contextContract
+	);
 
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
@@ -339,12 +351,12 @@ protected:
 
 	/// Creates symbolic expressions for the returned values
 	/// and set them as the components of the symbolic tuple.
-	void createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contract);
+	void createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract);
 
 	/// @returns the symbolic arguments for a function call,
 	/// taking into account bound functions and
 	/// type conversion.
-	std::vector<smtutil::Expression> symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contract);
+	std::vector<smtutil::Expression> symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract);
 
 	/// @returns a note to be added to warnings.
 	std::string extraComment();
@@ -384,12 +396,21 @@ protected:
 	bool isRootFunction();
 	/// Returns true if _funDef was already visited.
 	bool visitedFunction(FunctionDefinition const* _funDef);
+	/// @returns the contract that contains the current FunctionDefinition that is being visited,
+	/// or nullptr if the analysis is not inside a FunctionDefinition.
+	ContractDefinition const* currentScopeContract();
 
 	/// @returns FunctionDefinitions of the given contract (including its constructor and inherited methods),
 	/// taking into account overriding of the virtual functions.
-	std::vector<FunctionDefinition const*> const& contractFunctions(ContractDefinition const& _contract);
+	std::set<FunctionDefinition const*, ASTNode::CompareByID> const& contractFunctions(ContractDefinition const& _contract);
 	/// Cache for the method contractFunctions.
-	std::map<ContractDefinition const*, std::vector<FunctionDefinition const*>> m_contractFunctions;
+	std::map<ContractDefinition const*, std::set<FunctionDefinition const*, ASTNode::CompareByID>> m_contractFunctions;
+
+	/// @returns FunctionDefinitions of the given contract (including its constructor and methods of bases),
+	/// without taking into account overriding of the virtual functions.
+	std::set<FunctionDefinition const*, ASTNode::CompareByID> const& contractFunctionsWithoutVirtual(ContractDefinition const& _contract);
+	/// Cache for the method contractFunctionsWithoutVirtual.
+	std::map<ContractDefinition const*, std::set<FunctionDefinition const*, ASTNode::CompareByID>> m_contractFunctionsWithoutVirtual;
 
 	/// Depth of visit to modifiers.
 	/// When m_modifierDepth == #modifiers the function can be visited

libsolidity/formal/VariableUsage.cpp

@@ -60,11 +60,9 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
 
 void VariableUsage::endVisit(FunctionCall const& _funCall)
 {
-	if (m_inlineFunctionCalls(_funCall, m_currentContract))
-		if (
-			auto [funDef, contextContract] = SMTEncoder::functionCallToDefinition(_funCall, m_currentContract);
-			funDef
-		)
+	auto scopeContract = m_currentFunction->annotation().contract;
+	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())
 				funDef->accept(*this);
 }

libsolidity/formal/VariableUsage.h

@@ -36,9 +36,10 @@ 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&, ContractDefinition const*)> _inlineFunctionCalls) { m_inlineFunctionCalls = _inlineFunctionCalls; }
+	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;
@@ -56,8 +57,9 @@ private:
 	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*)> m_inlineFunctionCalls = [](FunctionCall const&, ContractDefinition const*) { return false; };
+	std::function<bool(FunctionCall const&, ContractDefinition const*, ContractDefinition const*)> m_inlineFunctionCalls = [](FunctionCall const&, ContractDefinition const*, ContractDefinition const*) { return false; };
 };
 
 }