[SMTChecker] Inline calls to internal functions

1 files changed, 24 insertions, 4 deletions

diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 6cf4e48a..bef6ea0c 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -59,7 +59,6 @@ private:
 	virtual bool visit(WhileStatement const& _node) override;
 	virtual bool visit(ForStatement const& _node) override;
 	virtual void endVisit(VariableDeclarationStatement const& _node) override;
-	virtual void endVisit(ExpressionStatement const& _node) override;
 	virtual void endVisit(Assignment const& _node) override;
 	virtual void endVisit(TupleExpression const& _node) override;
 	virtual void endVisit(UnaryOperation const& _node) override;
@@ -67,11 +66,18 @@ private:
 	virtual void endVisit(FunctionCall const& _node) override;
 	virtual void endVisit(Identifier const& _node) override;
 	virtual void endVisit(Literal const& _node) override;
+	virtual void endVisit(Return const& _node) override;
 
 	void arithmeticOperation(BinaryOperation const& _op);
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 
+	void visitAssert(FunctionCall const&);
+	void visitRequire(FunctionCall const&);
+	/// Visits the FunctionDefinition of the called function
+	/// if available and inlines the return value.
+	void inlineFunctionCall(FunctionCall const&);
+
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
 	smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
@@ -113,6 +119,7 @@ private:
 	smt::CheckResult checkSatisfiable();
 
 	void initializeLocalVariables(FunctionDefinition const& _function);
+	void initializeFunctionCallParameters(FunctionDefinition const& _function, std::vector<smt::Expression> const& _callArgs);
 	void resetStateVariables();
 	void resetVariables(std::vector<VariableDeclaration const*> _variables);
 	/// Given two different branches and the touched variables,
@@ -147,6 +154,8 @@ private:
 	smt::Expression expr(Expression const& _e);
 	/// Creates the expression (value can be arbitrary)
 	void createExpr(Expression const& _e);
+	/// Checks if expression was created
+	bool hasExpr(Expression const& _e) const;
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smt::Expression _value);
 
@@ -161,18 +170,29 @@ private:
 	/// Add to the solver: the given expression implied by the current path conditions
 	void addPathImpliedExpression(smt::Expression const& _e);
 
-	/// Removes the local variables of a function.
+	/// Removes local variables from the context.
 	void removeLocalVariables();
 
+	/// Checks if VariableDeclaration was seen.
+	bool hasVariable(VariableDeclaration const& _e) const;
+
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::shared_ptr<VariableUsage> m_variableUsage;
 	bool m_loopExecutionHappened = false;
-	std::map<Expression const*, smt::Expression> m_expressions;
+	/// An Expression may have multiple smt::Expression due to
+	/// repeated calls to the same function.
+	std::multimap<Expression const*, smt::Expression> m_expressions;
 	std::map<VariableDeclaration const*, SSAVariable> m_variables;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;
 
-	FunctionDefinition const* m_currentFunction = nullptr;
+	/// Stores the current path of function calls.
+	std::vector<FunctionDefinition const*> m_functionPath;
+	/// Returns true if the current function was not visited by
+	/// a function call.
+	bool isRootFunction();
+	/// Returns true if _funDef was already visited.
+	bool visitedFunction(FunctionDefinition const* _funDef);
 };
 
 }