Merge pull request #3406 from leonardoalt/smt_checker

SMTChecker: A little refactoring on SSA vars (preparation for Bool)

libsolidity/formal/SMTChecker.cpp

@@ -23,6 +23,8 @@
 #include <libsolidity/formal/SMTLib2Interface.h>
 #endif
 
+#include <libsolidity/formal/SSAVariable.h>
+#include <libsolidity/formal/SymbolicIntVariable.h>
 #include <libsolidity/formal/VariableUsage.h>
 
 #include <libsolidity/interface/ErrorReporter.h>
@@ -69,8 +71,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 +92,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 +157,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 +168,7 @@ bool SMTChecker::visit(ForStatement const& _node)
 	m_interface->pop();
 
 	m_conditionalExecutionHappened = true;
-	m_currentSequenceCounter = sequenceCountersStart;
+	std::swap(sequenceCountersStart, m_variables);
 
 	resetVariables(touchedVariables);
 
@@ -240,14 +245,14 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
 void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location)
 {
 	checkCondition(
-		_value < minValue(_type),
+		_value < SymbolicIntVariable::minValue(_type),
 		_location,
 		"Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
 		"value",
 		&_value
 	);
 	checkCondition(
-		_value > maxValue(_type),
+		_value > SymbolicIntVariable::maxValue(_type),
 		_location,
 		"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
 		"value",
@@ -365,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()))
 	{
@@ -514,7 +519,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 +528,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 +715,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,
@@ -722,14 +728,10 @@ 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_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 +744,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 +751,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 +829,6 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
 	m_interface->addAssertion(expr(_e) == _value);
 }
 
-smt::Expression SMTChecker::var(Declaration const& _decl)
-{
-	solAssert(m_variables.count(&_decl), "");
-	return m_variables.at(&_decl);
-}
-
 void SMTChecker::popPathCondition()
 {
 	solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty.");

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.
@@ -139,18 +140,12 @@ private:
 	/// Resets the variable to an unknown value (in its range).
 	void setUnknownValue(Declaration const& decl);
 
-	static smt::Expression minValue(IntegerType const& _t);
-	static smt::Expression maxValue(IntegerType const& _t);
-
 	/// Returns the expression corresponding to the AST node. Throws if the expression does not exist.
 	smt::Expression expr(Expression const& _e);
 	/// Creates the expression (value can be arbitrary)
 	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 +161,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;
 

libsolidity/formal/SSAVariable.cpp

@@ -0,0 +1,73 @@
+/*
+	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_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface);
+	else
+	{
+		solAssert(false, "");
+	}
+}
+
+bool SSAVariable::supportedType(Type const* _decl)
+{
+	return dynamic_cast<IntegerType const*>(_decl);
+}
+
+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_symbolicVar->setZeroValue(index());
+}
+
+void SSAVariable::setUnknownValue()
+{
+	m_symbolicVar->setUnknownValue(index());
+}

libsolidity/formal/SSAVariable.h

@@ -0,0 +1,88 @@
+/*
+	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:
+	/// @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.
+	SSAVariable(
+		Declaration const* _decl,
+		smt::SolverInterface& _interface
+	);
+
+	void resetIndex();
+
+	/// This function returns the current index of this SSA variable.
+	int index() const;
+	/// This function returns the next free index of this SSA variable.
+	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);
+	}
+
+	/// 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
+	{
+		return (*m_symbolicVar)(_seq);
+	}
+
+	std::shared_ptr<SymbolicVariable> m_symbolicVar = 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;
+};
+
+}
+}

libsolidity/formal/SymbolicIntVariable.cpp

@@ -0,0 +1,56 @@
+/*
+	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)
+{
+	return smt::Expression(_t.minValue());
+}
+
+smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t)
+{
+	return smt::Expression(_t.maxValue());
+}

libsolidity/formal/SymbolicIntVariable.h

@@ -0,0 +1,50 @@
+/*
+	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:
+	SymbolicIntVariable(
+		Declaration const* _decl,
+		smt::SolverInterface& _interface
+	);
+
+	/// Sets the var to 0.
+	void setZeroValue(int _seq);
+	/// Sets the variable to the full valid value range.
+	void setUnknownValue(int _seq);
+
+	static smt::Expression minValue(IntegerType const& _t);
+	static smt::Expression maxValue(IntegerType const& _t);
+};
+
+}
+}

libsolidity/formal/SymbolicVariable.cpp

@@ -0,0 +1,40 @@
+/*
+	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());
+}
+
+

libsolidity/formal/SymbolicVariable.h

@@ -0,0 +1,69 @@
+/*
+	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:
+	SymbolicVariable(
+		Declaration const* _decl,
+		smt::SolverInterface& _interface
+	);
+
+	smt::Expression operator()(int _seq) const
+	{
+		return valueAtSequence(_seq);
+	}
+
+	std::string uniqueSymbol() const;
+
+	/// Sets the var to the default value of its type.
+	virtual void setZeroValue(int _seq) = 0;
+	/// The unknown value is the full range of valid values,
+	/// and that's sub-type dependent.
+	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;
+};
+
+}
+}