From de46bb2c429ac3a3fac2d86417cf4836e294c7bb Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 10 Dec 2018 11:34:29 +0100
Subject: [SMTChecker] Introduce SymbolicFunctionVariable

---
 libsolidity/formal/SymbolicVariables.cpp | 28 ++++++++++++++++++++++++++++
 libsolidity/formal/SymbolicVariables.h   | 29 ++++++++++++++++++++++++++++-
 2 files changed, 56 insertions(+), 1 deletion(-)

diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index f7d2a119..997635af 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -99,3 +99,31 @@ SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
 	SymbolicIntVariable(make_shared<IntegerType>(_numBytes * 8), _uniqueName, _interface)
 {
 }
+
+SymbolicFunctionVariable::SymbolicFunctionVariable(
+	TypePointer _type,
+	string const& _uniqueName,
+	smt::SolverInterface&_interface
+):
+	SymbolicVariable(move(_type), _uniqueName, _interface),
+	m_declaration(m_interface.newVariable(currentName(), smtSort(*m_type)))
+{
+	solAssert(m_type->category() == Type::Category::Function, "");
+}
+
+void SymbolicFunctionVariable::resetDeclaration()
+{
+	m_declaration = m_interface.newVariable(currentName(), smtSort(*m_type));
+}
+
+smt::Expression SymbolicFunctionVariable::increaseIndex()
+{
+	++(*m_ssa);
+	resetDeclaration();
+	return currentValue();
+}
+
+smt::Expression SymbolicFunctionVariable::operator()(vector<smt::Expression> _arguments) const
+{
+	return m_declaration(_arguments);
+}
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index ef40944c..6754ee07 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -49,7 +49,11 @@ public:
 	smt::Expression currentValue() const;
 	std::string currentName() const;
 	virtual smt::Expression valueAtIndex(int _index) const;
-	smt::Expression increaseIndex();
+	virtual smt::Expression increaseIndex();
+	virtual smt::Expression operator()(std::vector<smt::Expression> /*_arguments*/) const
+	{
+		solAssert(false, "Function application to non-function.");
+	}
 
 	unsigned index() const { return m_ssa->index(); }
 	unsigned& index() { return m_ssa->index(); }
@@ -116,5 +120,28 @@ public:
 	);
 };
 
+/**
+ * Specialization of SymbolicVariable for FunctionType
+ */
+class SymbolicFunctionVariable: public SymbolicVariable
+{
+public:
+	SymbolicFunctionVariable(
+		TypePointer _type,
+		std::string const& _uniqueName,
+		smt::SolverInterface& _interface
+	);
+
+	smt::Expression increaseIndex();
+	smt::Expression operator()(std::vector<smt::Expression> _arguments) const;
+
+private:
+	/// Creates a new function declaration.
+	void resetDeclaration();
+
+	/// Stores the current function declaration.
+	smt::Expression m_declaration;
+};
+
 }
 }
-- 
cgit