[SMTChecker] Refactor function inlining

libsolidity/formal/BMC.cpp

@@ -76,47 +76,32 @@ void BMC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner
 	m_errorReporter.clear();
 }
 
-FunctionDefinition const* BMC::inlinedFunctionCallToDefinition(FunctionCall const& _funCall)
+bool BMC::shouldInlineFunctionCall(FunctionCall const& _funCall)
 {
-	if (_funCall.annotation().kind != FunctionCallKind::FunctionCall)
+	FunctionDefinition const* funDef = functionCallToDefinition(_funCall);
-		return nullptr;
+	if (!funDef || !funDef->isImplemented())
+		return false;
 
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	if (funType.kind() == FunctionType::Kind::External)
 	{
 		auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
-		auto identifier = memberAccess ?
+		if (!memberAccess)
-			dynamic_cast<Identifier const*>(&memberAccess->expression()) :
+			return false;
-			nullptr;
+
+		auto identifier = dynamic_cast<Identifier const*>(&memberAccess->expression());
 		if (!(
 			identifier &&
 			identifier->name() == "this" &&
 			identifier->annotation().referencedDeclaration &&
 			dynamic_cast<MagicVariableDeclaration const*>(identifier->annotation().referencedDeclaration)
 		))
-			return nullptr;
+			return false;
 	}
 	else if (funType.kind() != FunctionType::Kind::Internal)
-		return nullptr;
+		return false;
 
-	FunctionDefinition const* funDef = nullptr;
+	return true;
-	Expression const* calledExpr = &_funCall.expression();
-
-	if (TupleExpression const* fun = dynamic_cast<TupleExpression const*>(&_funCall.expression()))
-	{
-		solAssert(fun->components().size() == 1, "");
-		calledExpr = fun->components().front().get();
-	}
-
-	if (Identifier const* fun = dynamic_cast<Identifier const*>(calledExpr))
-		funDef = dynamic_cast<FunctionDefinition const*>(fun->annotation().referencedDeclaration);
-	else if (MemberAccess const* fun = dynamic_cast<MemberAccess const*>(calledExpr))
-		funDef = dynamic_cast<FunctionDefinition const*>(fun->annotation().referencedDeclaration);
-
-	if (funDef && funDef->isImplemented())
-		return funDef;
-
-	return nullptr;
 }
 
 /// AST visitors.
@@ -403,7 +388,8 @@ void BMC::visitRequire(FunctionCall const& _funCall)
 
 void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 {
-	FunctionDefinition const* funDef = inlinedFunctionCallToDefinition(_funCall);
+	solAssert(shouldInlineFunctionCall(_funCall), "");
+	FunctionDefinition const* funDef = functionCallToDefinition(_funCall);
 	solAssert(funDef, "");
 	if (visitedFunction(funDef))
 		m_errorReporter.warning(
@@ -468,9 +454,8 @@ void BMC::abstractFunctionCall(FunctionCall const& _funCall)
 
 void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 {
-	auto funDef = inlinedFunctionCallToDefinition(_funCall);
 	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
-	if (funDef)
+	if (shouldInlineFunctionCall(_funCall))
 		inlineFunctionCall(_funCall);
 	else if (funType.kind() == FunctionType::Kind::Internal)
 		m_errorReporter.warning(

libsolidity/formal/BMC.h

@@ -62,9 +62,8 @@ public:
 	/// the constructor.
 	std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
 
-	/// @returns the FunctionDefinition of a called function if possible and should inline,
+	/// @returns true if _funCall should be inlined, otherwise false.
-	/// otherwise nullptr.
+	static bool shouldInlineFunctionCall(FunctionCall const& _funCall);
-	static FunctionDefinition const* inlinedFunctionCallToDefinition(FunctionCall const& _funCall);
 
 	std::shared_ptr<smt::SolverInterface> solver() { return m_interface; }
 

libsolidity/formal/SMTEncoder.cpp

@@ -1354,3 +1354,25 @@ string SMTEncoder::extraComment()
 			"You can re-introduce information using require().";
 	return extra;
 }
+
+FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall const& _funCall)
+{
+	if (_funCall.annotation().kind != FunctionCallKind::FunctionCall)
+		return nullptr;
+
+	FunctionDefinition const* funDef = nullptr;
+	Expression const* calledExpr = &_funCall.expression();
+
+	if (TupleExpression const* fun = dynamic_cast<TupleExpression const*>(&_funCall.expression()))
+	{
+		solAssert(fun->components().size() == 1, "");
+		calledExpr = fun->components().front().get();
+	}
+
+	if (Identifier const* fun = dynamic_cast<Identifier const*>(calledExpr))
+		funDef = dynamic_cast<FunctionDefinition const*>(fun->annotation().referencedDeclaration);
+	else if (MemberAccess const* fun = dynamic_cast<MemberAccess const*>(calledExpr))
+		funDef = dynamic_cast<FunctionDefinition const*>(fun->annotation().referencedDeclaration);
+
+	return funDef;
+}

libsolidity/formal/SMTEncoder.h

@@ -55,6 +55,10 @@ public:
 	/// @returns the leftmost identifier in a multi-d IndexAccess.
 	static Expression const* leftmostBase(IndexAccess const& _indexAccess);
 
+	/// @returns the FunctionDefinition of a FunctionCall
+	/// if possible or nullptr.
+	static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall);
+
 protected:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined

libsolidity/formal/VariableUsage.cpp

@@ -58,9 +58,12 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
 void VariableUsage::endVisit(FunctionCall const& _funCall)
 {
 	if (m_inlineFunctionCalls)
-		if (auto const& funDef = BMC::inlinedFunctionCallToDefinition(_funCall))
+		if (auto const& funDef = SMTEncoder::functionCallToDefinition(_funCall))
+		{
+			solAssert(funDef, "");
 			if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end())
 				funDef->accept(*this);
+		}
 }
 
 bool VariableUsage::visit(FunctionDefinition const& _function)