Merge pull request #3829 from ethereum/smt_remove_uf

[SMTChecker] Remove usage of UFs to access SSA vars

6 files changed, 20 insertions, 10 deletions

diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp
index e5c56e46..5cf22d7d 100644
--- a/libsolidity/formal/SymbolicBoolVariable.cpp
+++ b/libsolidity/formal/SymbolicBoolVariable.cpp
@@ -30,7 +30,11 @@ SymbolicBoolVariable::SymbolicBoolVariable(
 	SymbolicVariable(_decl, _interface)
 {
 	solAssert(m_declaration.type()->category() == Type::Category::Bool, "");
-	m_expression = make_shared<smt::Expression>(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Bool));
+}
+
+smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const
+{
+	return m_interface.newBool(uniqueSymbol(_seq));
 }
 
 void SymbolicBoolVariable::setZeroValue(int _seq)
diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h
index 3510b770..678f97d9 100644
--- a/libsolidity/formal/SymbolicBoolVariable.h
+++ b/libsolidity/formal/SymbolicBoolVariable.h
@@ -41,6 +41,9 @@ public:
 	void setZeroValue(int _seq);
 	/// Does nothing since the SMT solver already knows the valid values.
 	void setUnknownValue(int _seq);
+
+protected:
+	smt::Expression valueAtSequence(int _seq) const;
 };
 
 }
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
index eb7b1c17..5e71fdcc 100644
--- a/libsolidity/formal/SymbolicIntVariable.cpp
+++ b/libsolidity/formal/SymbolicIntVariable.cpp
@@ -30,7 +30,11 @@ SymbolicIntVariable::SymbolicIntVariable(
 	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));
+}
+
+smt::Expression SymbolicIntVariable::valueAtSequence(int _seq) const
+{
+	return m_interface.newInteger(uniqueSymbol(_seq));
 }
 
 void SymbolicIntVariable::setZeroValue(int _seq)
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
index eb36b899..d591e8db 100644
--- a/libsolidity/formal/SymbolicIntVariable.h
+++ b/libsolidity/formal/SymbolicIntVariable.h
@@ -44,6 +44,9 @@ public:
 
 	static smt::Expression minValue(IntegerType const& _t);
 	static smt::Expression maxValue(IntegerType const& _t);
+
+protected:
+	smt::Expression valueAtSequence(int _seq) const;
 };
 
 }
diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp
index d59b55b1..caefa3a3 100644
--- a/libsolidity/formal/SymbolicVariable.cpp
+++ b/libsolidity/formal/SymbolicVariable.cpp
@@ -32,9 +32,9 @@ SymbolicVariable::SymbolicVariable(
 {
 }
 
-string SymbolicVariable::uniqueSymbol() const
+string SymbolicVariable::uniqueSymbol(int _seq) const
 {
-	return m_declaration.name() + "_" + to_string(m_declaration.id());
+	return m_declaration.name() + "_" + to_string(m_declaration.id()) + "_" + to_string(_seq);
 }
 
 
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
index 75eb9fa5..e4e4ea8d 100644
--- a/libsolidity/formal/SymbolicVariable.h
+++ b/libsolidity/formal/SymbolicVariable.h
@@ -46,7 +46,7 @@ public:
 		return valueAtSequence(_seq);
 	}
 
-	std::string uniqueSymbol() const;
+	std::string uniqueSymbol(int _seq) const;
 
 	/// Sets the var to the default value of its type.
 	virtual void setZeroValue(int _seq) = 0;
@@ -55,13 +55,9 @@ public:
 	virtual void setUnknownValue(int _seq) = 0;
 
 protected:
-	smt::Expression valueAtSequence(int _seq) const
-	{
-		return (*m_expression)(_seq);
-	}
+	virtual smt::Expression valueAtSequence(int _seq) const = 0;
 
 	Declaration const& m_declaration;
-	std::shared_ptr<smt::Expression> m_expression = nullptr;
 	smt::SolverInterface& m_interface;
 };