From 6f9b69ebc345202235e4986193d2c317fc9241da Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 25 Mar 2019 13:58:22 +0100
Subject: [PATCH] Refactor function that retrieves FunctionDefinition from
 FunctionCall

---
 libsolidity/formal/SMTChecker.cpp | 60 ++++++++++++++++++-------------
 libsolidity/formal/SMTChecker.h   |  4 +++
 2 files changed, 39 insertions(+), 25 deletions(-)

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 7cdaa49f3..4e25c44fe 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -616,20 +616,8 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 
 void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 {
-	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().at(0).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);
-	else
+	FunctionDefinition const* _funDef = inlinedFunctionCallToDefinition(_funCall);
+	if (!_funDef)
 	{
 		m_errorReporter.warning(
 			_funCall.location(),
@@ -637,7 +625,6 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 		);
 		return;
 	}
-	solAssert(_funDef, "");
 
 	if (visitedFunction(_funDef))
 		m_errorReporter.warning(
@@ -645,14 +632,15 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 			"Assertion checker does not support recursive function calls.",
 			SecondarySourceLocation().append("Starting from function:", _funDef->location())
 		);
-	else if (_funDef && _funDef->isImplemented())
+	else
 	{
 		vector<smt::Expression> funArgs;
-		auto const& funType = dynamic_cast<FunctionType const*>(_calledExpr->annotation().type.get());
+		Expression const* calledExpr = &_funCall.expression();
+		auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type.get());
 		solAssert(funType, "");
 		if (funType->bound())
 		{
-			auto const& boundFunction = dynamic_cast<MemberAccess const*>(_calledExpr);
+			auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
 			solAssert(boundFunction, "");
 			funArgs.push_back(expr(boundFunction->expression()));
 		}
@@ -672,13 +660,6 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 				defineExpr(_funCall, currentValue(*returnParams[0]));
 		}
 	}
-	else
-	{
-		m_errorReporter.warning(
-			_funCall.location(),
-			"Assertion checker does not support calls to functions without implementation."
-		);
-	}
 }
 
 void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
@@ -1673,3 +1654,32 @@ void SMTChecker::resetVariableIndices(VariableIndices const& _indices)
 	for (auto const& var: _indices)
 		m_variables.at(var.first)->index() = var.second;
 }
+
+FunctionDefinition const* SMTChecker::inlinedFunctionCallToDefinition(FunctionCall const& _funCall)
+{
+	if (_funCall.annotation().kind != FunctionCallKind::FunctionCall)
+		return nullptr;
+
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	if (funType.kind() != FunctionType::Kind::Internal)
+		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);
+
+	if (funDef && funDef->isImplemented())
+		return funDef;
+
+	return nullptr;
+}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 66f4397e8..4df80ec8f 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -55,6 +55,10 @@ public:
 	/// the constructor.
 	std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
 
+	/// @return the FunctionDefinition of a called function if possible and should inline,
+	/// otherwise nullptr.
+	static FunctionDefinition const* inlinedFunctionCallToDefinition(FunctionCall const& _funCall);
+
 private:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined