From 21c6b80fc98f6d584f240a47d4a01827768f18f3 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leonardoaltt@gmail.com>
Date: Sat, 17 Feb 2018 09:35:37 +0100
Subject: Supported types listed in SSAVariable

---
 libsolidity/formal/SMTChecker.cpp     | 4 ++--
 libsolidity/formal/SSAVariable.cpp    | 7 ++++++-
 libsolidity/formal/SSAVariable.h      | 9 +++++++++
 libsolidity/formal/SymbolicVariable.h | 3 +++
 4 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index ad42c105..1da5b291 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -370,7 +370,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 	{
 		// Will be translated as part of the node that requested the lvalue.
 	}
-	else if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
+	else if (SSAVariable::supportedType(_identifier.annotation().type.get()))
 		defineExpr(_identifier, currentValue(*decl));
 	else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
 	{
@@ -728,7 +728,7 @@ void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, sm
 
 bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 {
-	if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
+	if (SSAVariable::supportedType(_varDecl.type().get()))
 	{
 		solAssert(m_variables.count(&_varDecl) == 0, "");
 		m_variables.emplace(&_varDecl, SSAVariable(&_varDecl, *m_interface));
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
index d6e97a8d..7f214687 100644
--- a/libsolidity/formal/SSAVariable.cpp
+++ b/libsolidity/formal/SSAVariable.cpp
@@ -34,10 +34,15 @@ SSAVariable::SSAVariable(Declaration const* _decl,
 		m_symbVar = make_shared<SymbolicIntVariable>(_decl, _interface);
 	else
 	{
-		//solAssert(false, "");
+		solAssert(false, "");
 	}
 }
 
+bool SSAVariable::supportedType(Type const* _decl)
+{
+	return dynamic_cast<IntegerType const*>(_decl);
+}
+
 void SSAVariable::resetIndex()
 {
 	m_currentSequenceCounter = 0;
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
index 3d7eb80c..b87693c2 100644
--- a/libsolidity/formal/SSAVariable.h
+++ b/libsolidity/formal/SSAVariable.h
@@ -34,6 +34,8 @@ class Declaration;
 class SSAVariable
 {
 public:
+	/// @param _decl Used to determine the type and forwarded to the symbolic var.
+	/// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver.
 	explicit SSAVariable(Declaration const* _decl,
 		smt::SolverInterface& _interface);
 	SSAVariable(SSAVariable const&) = default;
@@ -61,9 +63,14 @@ public:
 		return valueAtSequence(_seq);
 	}
 
+	/// These two functions forward the call to the symbolic var
+	/// which generates the constraints according to the type.
 	void setZeroValue();
 	void setUnknownValue();
 
+	/// So far Int is supported.
+	static bool supportedType(Type const* _decl);
+
 private:
 	smt::Expression valueAtSequence(int _seq) const
 	{
@@ -72,6 +79,8 @@ private:
 
 	std::shared_ptr<SymbolicVariable> m_symbVar = nullptr;
 	int m_currentSequenceCounter;
+	/// The next free sequence counter is a shared pointer because we want
+	/// the copy and the copied to share it.
 	std::shared_ptr<int> m_nextFreeSequenceCounter;
 };
 
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
index 4de59504..66633b73 100644
--- a/libsolidity/formal/SymbolicVariable.h
+++ b/libsolidity/formal/SymbolicVariable.h
@@ -50,7 +50,10 @@ public:
 
 	std::string uniqueSymbol() const;
 
+	/// Sets the var to the default value of its type.
 	virtual void setZeroValue(int _seq) = 0;
+	/// The unknown value depends on the type. For example, an interval is set for Integers.
+	/// This is decided by the subclasses.
 	virtual void setUnknownValue(int _seq) = 0;
 
 protected:
-- 
cgit