From 8d087d1889826271a78ce537b8d1a2ceb11574dd Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 5 Apr 2018 12:20:41 +0200 Subject: [SMTChecker] Removing usage of UFs to access SSA indices --- libsolidity/formal/SymbolicBoolVariable.cpp | 6 +++++- libsolidity/formal/SymbolicBoolVariable.h | 3 +++ libsolidity/formal/SymbolicIntVariable.cpp | 6 +++++- libsolidity/formal/SymbolicIntVariable.h | 3 +++ libsolidity/formal/SymbolicVariable.cpp | 4 ++-- libsolidity/formal/SymbolicVariable.h | 8 ++------ 6 files changed, 20 insertions(+), 10 deletions(-) (limited to 'libsolidity') 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(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(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 m_expression = nullptr; smt::SolverInterface& m_interface; }; -- cgit v1.2.3