[SMTChecker] A little refactoring on SSA vars

8 files changed, 395 insertions, 54 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index a64024b3..37dce96c 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -23,6 +23,7 @@
 #include <libsolidity/formal/SMTLib2Interface.h>
 #endif
 
+#include <libsolidity/formal/SSAVariable.h>
 #include <libsolidity/formal/VariableUsage.h>
 
 #include <libsolidity/interface/ErrorReporter.h>
@@ -69,8 +70,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 	// We only handle local variables, so we clear at the beginning of the function.
 	// If we add storage variables, those should be cleared differently.
 	m_interface->reset();
-	m_currentSequenceCounter.clear();
-	m_nextFreeSequenceCounter.clear();
+	m_variables.clear();
 	m_pathConditions.clear();
 	m_conditionalExecutionHappened = false;
 	initializeLocalVariables(_function);
@@ -91,14 +91,18 @@ bool SMTChecker::visit(IfStatement const& _node)
 
 	checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
 
-	auto countersEndFalse = m_currentSequenceCounter;
 	auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
 	vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
+	decltype(countersEndTrue) countersEndFalse;
 	if (_node.falseStatement())
 	{
 		countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition()));
 		touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
 	}
+	else
+	{
+		countersEndFalse = m_variables;
+	}
 
 	mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse);
 
@@ -152,7 +156,7 @@ bool SMTChecker::visit(ForStatement const& _node)
 		checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
 	}
 
-	VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
+	VariableSequenceCounters sequenceCountersStart = m_variables;
 	m_interface->push();
 	if (_node.condition())
 		m_interface->addAssertion(expr(*_node.condition()));
@@ -163,7 +167,7 @@ bool SMTChecker::visit(ForStatement const& _node)
 	m_interface->pop();
 
 	m_conditionalExecutionHappened = true;
-	m_currentSequenceCounter = sequenceCountersStart;
+	std::swap(sequenceCountersStart, m_variables);
 
 	resetVariables(touchedVariables);
 
@@ -514,7 +518,7 @@ SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _s
 
 SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
 {
-	VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
+	VariableSequenceCounters beforeVars = m_variables;
 
 	if (_condition)
 		pushPathCondition(*_condition);
@@ -523,8 +527,9 @@ SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _s
 		popPathCondition();
 
 	m_conditionalExecutionHappened = true;
-	std::swap(sequenceCountersStart, m_currentSequenceCounter);
-	return sequenceCountersStart;
+	std::swap(m_variables, beforeVars);
+
+	return beforeVars;
 }
 
 void SMTChecker::checkCondition(
@@ -709,8 +714,8 @@ void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, sm
 	set<Declaration const*> uniqueVars(_variables.begin(), _variables.end());
 	for (auto const* decl: uniqueVars)
 	{
-		int trueCounter = _countersEndTrue.at(decl);
-		int falseCounter = _countersEndFalse.at(decl);
+		int trueCounter = _countersEndTrue.at(decl).index();
+		int falseCounter = _countersEndFalse.at(decl).index();
 		solAssert(trueCounter != falseCounter, "");
 		m_interface->addAssertion(newValue(*decl) == smt::Expression::ite(
 			_condition,
@@ -724,12 +729,8 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 {
 	if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
 	{
-		solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
-		solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, "");
 		solAssert(m_variables.count(&_varDecl) == 0, "");
-		m_currentSequenceCounter[&_varDecl] = 0;
-		m_nextFreeSequenceCounter[&_varDecl] = 1;
-		m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
+		m_variables.emplace(&_varDecl, SSAVariable(&_varDecl, *m_interface));
 		return true;
 	}
 	else
@@ -742,11 +743,6 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 	}
 }
 
-string SMTChecker::uniqueSymbol(Declaration const& _decl)
-{
-	return _decl.name() + "_" + to_string(_decl.id());
-}
-
 string SMTChecker::uniqueSymbol(Expression const& _expr)
 {
 	return "expr_" + to_string(_expr.id());
@@ -754,48 +750,38 @@ string SMTChecker::uniqueSymbol(Expression const& _expr)
 
 bool SMTChecker::knownVariable(Declaration const& _decl)
 {
-	return m_currentSequenceCounter.count(&_decl);
+	return m_variables.count(&_decl);
 }
 
 smt::Expression SMTChecker::currentValue(Declaration const& _decl)
 {
-	solAssert(m_currentSequenceCounter.count(&_decl), "");
-	return valueAtSequence(_decl, m_currentSequenceCounter.at(&_decl));
+	solAssert(knownVariable(_decl), "");
+	return m_variables.at(&_decl)();
 }
 
-smt::Expression SMTChecker::valueAtSequence(const Declaration& _decl, int _sequence)
+smt::Expression SMTChecker::valueAtSequence(Declaration const& _decl, int _sequence)
 {
-	return var(_decl)(_sequence);
+	solAssert(knownVariable(_decl), "");
+	return m_variables.at(&_decl)(_sequence);
 }
 
 smt::Expression SMTChecker::newValue(Declaration const& _decl)
 {
-	solAssert(m_nextFreeSequenceCounter.count(&_decl), "");
-	m_currentSequenceCounter[&_decl] = m_nextFreeSequenceCounter[&_decl]++;
-	return currentValue(_decl);
+	solAssert(knownVariable(_decl), "");
+	++m_variables.at(&_decl);
+	return m_variables.at(&_decl)();
 }
 
 void SMTChecker::setZeroValue(Declaration const& _decl)
 {
-	solAssert(_decl.type()->category() == Type::Category::Integer, "");
-	m_interface->addAssertion(currentValue(_decl) == 0);
+	solAssert(knownVariable(_decl), "");
+	m_variables.at(&_decl).setZeroValue();
 }
 
 void SMTChecker::setUnknownValue(Declaration const& _decl)
 {
-	auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());
-	m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
-	m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
-}
-
-smt::Expression SMTChecker::minValue(IntegerType const& _t)
-{
-	return smt::Expression(_t.minValue());
-}
-
-smt::Expression SMTChecker::maxValue(IntegerType const& _t)
-{
-	return smt::Expression(_t.maxValue());
+	solAssert(knownVariable(_decl), "");
+	m_variables.at(&_decl).setUnknownValue();
 }
 
 smt::Expression SMTChecker::expr(Expression const& _e)
@@ -842,12 +828,15 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
 	m_interface->addAssertion(expr(_e) == _value);
 }
 
-smt::Expression SMTChecker::var(Declaration const& _decl)
+smt::Expression SMTChecker::minValue(IntegerType const& _t)
 {
-	solAssert(m_variables.count(&_decl), "");
-	return m_variables.at(&_decl);
+	return smt::Expression(_t.minValue());
 }
 
+smt::Expression SMTChecker::maxValue(IntegerType const& _t)
+{
+	return smt::Expression(_t.maxValue());
+}
 void SMTChecker::popPathCondition()
 {
 	solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty.");
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index b57f0f96..7481e1c8 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -20,6 +20,8 @@
 
 #include <libsolidity/formal/SolverInterface.h>
 
+#include <libsolidity/formal/SSAVariable.h>
+
 #include <libsolidity/ast/ASTVisitor.h>
 
 #include <libsolidity/interface/ReadFile.h>
@@ -76,7 +78,7 @@ private:
 	void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
 
 	/// Maps a variable to an SSA index.
-	using VariableSequenceCounters = std::map<Declaration const*, int>;
+	using VariableSequenceCounters = std::map<Declaration const*, SSAVariable>;
 
 	/// Visits the branch given by the statement, pushes and pops the current path conditions.
 	/// @param _condition if present, asserts that this condition is true within the branch.
@@ -118,7 +120,6 @@ private:
 	/// This fails if the type is not supported.
 	bool createVariable(VariableDeclaration const& _varDecl);
 
-	static std::string uniqueSymbol(Declaration const& _decl);
 	static std::string uniqueSymbol(Expression const& _expr);
 
 	/// @returns true if _delc is a variable that is known at the current point, i.e.
@@ -148,9 +149,6 @@ private:
 	void createExpr(Expression const& _e);
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smt::Expression _value);
-	/// Returns the function declaration corresponding to the given variable.
-	/// The function takes one argument which is the "sequence number".
-	smt::Expression var(Declaration const& _decl);
 
 	/// Adds a new path condition
 	void pushPathCondition(smt::Expression const& _e);
@@ -166,10 +164,8 @@ private:
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::shared_ptr<VariableUsage> m_variableUsage;
 	bool m_conditionalExecutionHappened = false;
-	std::map<Declaration const*, int> m_currentSequenceCounter;
-	std::map<Declaration const*, int> m_nextFreeSequenceCounter;
 	std::map<Expression const*, smt::Expression> m_expressions;
-	std::map<Declaration const*, smt::Expression> m_variables;
+	std::map<Declaration const*, SSAVariable> m_variables;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;
 
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
new file mode 100644
index 00000000..d6e97a8d
--- /dev/null
+++ b/libsolidity/formal/SSAVariable.cpp
@@ -0,0 +1,66 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/SSAVariable.h>
+
+#include <libsolidity/formal/SymbolicIntVariable.h>
+
+#include <libsolidity/ast/AST.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+SSAVariable::SSAVariable(Declaration const* _decl,
+	smt::SolverInterface& _interface)
+{
+	resetIndex();
+
+	if (dynamic_cast<IntegerType const*>(_decl->type().get()))
+		m_symbVar = make_shared<SymbolicIntVariable>(_decl, _interface);
+	else
+	{
+		//solAssert(false, "");
+	}
+}
+
+void SSAVariable::resetIndex()
+{
+	m_currentSequenceCounter = 0;
+	m_nextFreeSequenceCounter.reset (new int);
+	*m_nextFreeSequenceCounter = 1;
+}
+
+int SSAVariable::index() const
+{
+	return m_currentSequenceCounter;
+}
+
+int SSAVariable::next() const
+{
+	return *m_nextFreeSequenceCounter;
+}
+
+void SSAVariable::setZeroValue()
+{
+	m_symbVar->setZeroValue(index());
+}
+
+void SSAVariable::setUnknownValue()
+{
+	m_symbVar->setUnknownValue(index());
+}
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
new file mode 100644
index 00000000..3d7eb80c
--- /dev/null
+++ b/libsolidity/formal/SSAVariable.h
@@ -0,0 +1,79 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <libsolidity/formal/SymbolicVariable.h>
+
+#include <memory>
+
+namespace dev
+{
+namespace solidity
+{
+
+class Declaration;
+
+/**
+ * This class represents the SSA representation of a program variable.
+ */
+class SSAVariable
+{
+public:
+	explicit SSAVariable(Declaration const* _decl,
+		smt::SolverInterface& _interface);
+	SSAVariable(SSAVariable const&) = default;
+	SSAVariable(SSAVariable&&) = default;
+	SSAVariable& operator=(SSAVariable const&) = default;
+	SSAVariable& operator=(SSAVariable&&) = default;
+
+	void resetIndex();
+
+	int index() const;
+	int next() const;
+
+	int operator++()
+	{
+		return m_currentSequenceCounter = (*m_nextFreeSequenceCounter)++;
+	}
+
+	smt::Expression operator()() const
+	{
+		return valueAtSequence(index());
+	}
+
+	smt::Expression operator()(int _seq) const
+	{
+		return valueAtSequence(_seq);
+	}
+
+	void setZeroValue();
+	void setUnknownValue();
+
+private:
+	smt::Expression valueAtSequence(int _seq) const
+	{
+		return (*m_symbVar)(_seq);
+	}
+
+	std::shared_ptr<SymbolicVariable> m_symbVar = nullptr;
+	int m_currentSequenceCounter;
+	std::shared_ptr<int> m_nextFreeSequenceCounter;
+};
+
+}
+}
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
new file mode 100644
index 00000000..6ed7037f
--- /dev/null
+++ b/libsolidity/formal/SymbolicIntVariable.cpp
@@ -0,0 +1,54 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/SymbolicIntVariable.h>
+
+#include <libsolidity/ast/AST.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+SymbolicIntVariable::SymbolicIntVariable(Declaration const* _decl,
+	smt::SolverInterface&_interface)
+	: SymbolicVariable(_decl, _interface)
+{
+	solAssert(m_declaration->type()->category() == Type::Category::Integer, "");
+	m_expression = make_shared<smt::Expression>(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Int));
+}
+
+void SymbolicIntVariable::setZeroValue(int _seq)
+{
+	m_interface.addAssertion(valueAtSequence(_seq) == 0);
+}
+
+void SymbolicIntVariable::setUnknownValue(int _seq)
+{
+	auto const& intType = dynamic_cast<IntegerType const&>(*m_declaration->type());
+	m_interface.addAssertion(valueAtSequence(_seq) >= minValue(intType));
+	m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(intType));
+}
+
+smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t) const
+{
+	return smt::Expression(_t.minValue());
+}
+
+smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t) const
+{
+	return smt::Expression(_t.maxValue());
+}
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
new file mode 100644
index 00000000..efe05af8
--- /dev/null
+++ b/libsolidity/formal/SymbolicIntVariable.h
@@ -0,0 +1,51 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <libsolidity/formal/SymbolicVariable.h>
+
+#include <libsolidity/ast/Types.h>
+
+namespace dev
+{
+namespace solidity
+{
+
+/**
+ * Specialization of SymbolicVariable for Integers
+ */
+class SymbolicIntVariable : public SymbolicVariable
+{
+public:
+	explicit SymbolicIntVariable(Declaration const* _decl,
+		smt::SolverInterface& _interface);
+	SymbolicIntVariable(SymbolicIntVariable const&) = default;
+	SymbolicIntVariable(SymbolicIntVariable&&) = default;
+	SymbolicIntVariable& operator=(SymbolicIntVariable const&) = default;
+	SymbolicIntVariable& operator=(SymbolicIntVariable&&) = default;
+
+	void setZeroValue(int _seq);
+	void setUnknownValue(int _seq);
+
+private:
+	smt::Expression minValue(IntegerType const& _t) const;
+	smt::Expression maxValue(IntegerType const& _t) const;
+};
+
+}
+}
diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp
new file mode 100644
index 00000000..13f5d9b6
--- /dev/null
+++ b/libsolidity/formal/SymbolicVariable.cpp
@@ -0,0 +1,38 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/SymbolicVariable.h>
+
+#include <libsolidity/ast/AST.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+SymbolicVariable::SymbolicVariable(Declaration const* _decl,
+	smt::SolverInterface& _interface)
+	: m_declaration(_decl),
+	m_interface(_interface)
+{
+}
+
+string SymbolicVariable::uniqueSymbol() const
+{
+	return m_declaration->name() + "_" + to_string(m_declaration->id());
+}
+
+
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
new file mode 100644
index 00000000..4de59504
--- /dev/null
+++ b/libsolidity/formal/SymbolicVariable.h
@@ -0,0 +1,68 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <libsolidity/formal/SolverInterface.h>
+
+#include <libsolidity/ast/AST.h>
+
+#include <memory>
+
+namespace dev
+{
+namespace solidity
+{
+
+class Declaration;
+
+/**
+ * This class represents the symbolic version of a program variable.
+ */
+class SymbolicVariable
+{
+public:
+	explicit SymbolicVariable(Declaration const* _decl,
+		smt::SolverInterface& _interface);
+	SymbolicVariable(SymbolicVariable const&) = default;
+	SymbolicVariable(SymbolicVariable&&) = default;
+	SymbolicVariable& operator=(SymbolicVariable const&) = default;
+	SymbolicVariable& operator=(SymbolicVariable&&) = default;
+
+	smt::Expression operator()(int _seq) const
+	{
+		return valueAtSequence(_seq);
+	}
+
+	std::string uniqueSymbol() const;
+
+	virtual void setZeroValue(int _seq) = 0;
+	virtual void setUnknownValue(int _seq) = 0;
+
+protected:
+	smt::Expression valueAtSequence(int _seq) const
+	{
+		return (*m_expression)(_seq);
+	}
+
+	Declaration const* m_declaration;
+	std::shared_ptr<smt::Expression> m_expression = nullptr;
+	smt::SolverInterface& m_interface;
+};
+
+}
+}