Merge pull request #5482 from ethereum/smt_refactor_sort_patch4

[SMTChecker] Refactor setZeroValue and setUnknownValue

6 files changed, 58 insertions, 44 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index caf7e5fa..bb9b498f 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -409,7 +409,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 	auto const& symbolicVar = m_specialVariables.at(gasLeft);
 	unsigned index = symbolicVar->index();
 	// We set the current value to unknown anyway to add type constraints.
-	symbolicVar->setUnknownValue();
+	setUnknownValue(*symbolicVar);
 	if (index > 0)
 		m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
@@ -597,7 +597,7 @@ void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _e
 	{
 		auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
 		m_specialVariables.emplace(_name, result.second);
-		result.second->setUnknownValue();
+		setUnknownValue(*result.second);
 		if (result.first)
 			m_errorReporter.warning(
 				_expr.location(),
@@ -1071,13 +1071,23 @@ smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl)
 void SMTChecker::setZeroValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	m_variables.at(&_decl)->setZeroValue();
+	setZeroValue(*m_variables.at(&_decl));
+}
+
+void SMTChecker::setZeroValue(SymbolicVariable& _variable)
+{
+	smt::setSymbolicZeroValue(_variable, *m_interface);
 }
 
 void SMTChecker::setUnknownValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	m_variables.at(&_decl)->setUnknownValue();
+	setUnknownValue(*m_variables.at(&_decl));
+}
+
+void SMTChecker::setUnknownValue(SymbolicVariable& _variable)
+{
+	smt::setSymbolicUnknownValue(_variable, *m_interface);
 }
 
 smt::Expression SMTChecker::expr(Expression const& _e)
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 8ead5564..5f51beb7 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -157,8 +157,10 @@ private:
 
 	/// Sets the value of the declaration to zero.
 	void setZeroValue(VariableDeclaration const& _decl);
+	void setZeroValue(SymbolicVariable& _variable);
 	/// Resets the variable to an unknown value (in its range).
 	void setUnknownValue(VariableDeclaration const& decl);
+	void setUnknownValue(SymbolicVariable& _variable);
 
 	/// Returns the expression corresponding to the AST node. Throws if the expression does not exist.
 	smt::Expression expr(Expression const& _e);
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index a12ab142..c297c807 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -169,3 +169,32 @@ smt::Expression dev::solidity::maxValue(IntegerType const& _type)
 {
 	return smt::Expression(_type.maxValue());
 }
+
+void dev::solidity::smt::setSymbolicZeroValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface)
+{
+	setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _interface);
+}
+
+void dev::solidity::smt::setSymbolicZeroValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface)
+{
+	if (isInteger(_type->category()))
+		_interface.addAssertion(_expr == 0);
+	else if (isBool(_type->category()))
+		_interface.addAssertion(_expr == smt::Expression(false));
+}
+
+void dev::solidity::smt::setSymbolicUnknownValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface)
+{
+	setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _interface);
+}
+
+void dev::solidity::smt::setSymbolicUnknownValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface)
+{
+	if (isInteger(_type->category()))
+	{
+		auto intType = dynamic_cast<IntegerType const*>(_type.get());
+		solAssert(intType, "");
+		_interface.addAssertion(_expr >= minValue(*intType));
+		_interface.addAssertion(_expr <= maxValue(*intType));
+	}
+}
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 6af2a0a0..984653b3 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -55,5 +55,15 @@ std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(Type cons
 smt::Expression minValue(IntegerType const& _type);
 smt::Expression maxValue(IntegerType const& _type);
 
+namespace smt
+{
+
+void setSymbolicZeroValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface);
+void setSymbolicZeroValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface);
+void setSymbolicUnknownValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface);
+void setSymbolicUnknownValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface);
+
+}
+
 }
 }
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index 399e18f8..efaeb97a 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -62,15 +62,6 @@ smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
 	return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Bool));
 }
 
-void SymbolicBoolVariable::setZeroValue()
-{
-	m_interface.addAssertion(currentValue() == smt::Expression(false));
-}
-
-void SymbolicBoolVariable::setUnknownValue()
-{
-}
-
 SymbolicIntVariable::SymbolicIntVariable(
 	TypePointer _type,
 	string const& _uniqueName,
@@ -86,19 +77,6 @@ smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
 	return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Int));
 }
 
-void SymbolicIntVariable::setZeroValue()
-{
-	m_interface.addAssertion(currentValue() == 0);
-}
-
-void SymbolicIntVariable::setUnknownValue()
-{
-	auto intType = dynamic_cast<IntegerType const*>(m_type.get());
-	solAssert(intType, "");
-	m_interface.addAssertion(currentValue() >= minValue(*intType));
-	m_interface.addAssertion(currentValue() <= maxValue(*intType));
-}
-
 SymbolicAddressVariable::SymbolicAddressVariable(
 	string const& _uniqueName,
 	smt::SolverInterface& _interface
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index 13b944a5..fcf32760 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -64,20 +64,15 @@ public:
 	unsigned index() const { return m_ssa->index(); }
 	unsigned& index() { return m_ssa->index(); }
 
-	/// Sets the var to the default value of its type.
-	/// Inherited types must implement.
-	virtual void setZeroValue() = 0;
-	/// The unknown value is the full range of valid values.
-	/// It is sub-type dependent, but not mandatory.
-	virtual void setUnknownValue() {}
+	TypePointer const& type() const { return m_type; }
 
 protected:
 	std::string uniqueSymbol(unsigned _index) const;
 
-	TypePointer m_type = nullptr;
+	TypePointer m_type;
 	std::string m_uniqueName;
 	smt::SolverInterface& m_interface;
-	std::shared_ptr<SSAVariable> m_ssa = nullptr;
+	std::shared_ptr<SSAVariable> m_ssa;
 };
 
 /**
@@ -92,11 +87,6 @@ public:
 		smt::SolverInterface& _interface
 	);
 
-	/// Sets the var to false.
-	void setZeroValue();
-	/// Does nothing since the SMT solver already knows the valid values for Bool.
-	void setUnknownValue();
-
 protected:
 	smt::Expression valueAtIndex(int _index) const;
 };
@@ -113,11 +103,6 @@ public:
 		smt::SolverInterface& _interface
 	);
 
-	/// Sets the var to 0.
-	void setZeroValue();
-	/// Sets the variable to the full valid value range.
-	void setUnknownValue();
-
 protected:
 	smt::Expression valueAtIndex(int _index) const;
 };