cerc-io/solidity
15
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Removing usage of UFs to access SSA indices

Browse Source
This commit is contained in:
Leonardo Alt 2018-04-05 12:20:41 +02:00
parent 36d6c27e68
commit 8d087d1889
6 changed files with 20 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libsolidity/formal/SymbolicBoolVariable.cpp
View File

@ -30,7 +30,11 @@ SymbolicBoolVariable::SymbolicBoolVariable(
SymbolicVariable(_decl, _interface) SymbolicVariable(_decl, _interface)
{ {
solAssert(m_declaration.type()->category() == Type::Category::Bool, ""); 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) void SymbolicBoolVariable::setZeroValue(int _seq)

3
libsolidity/formal/SymbolicBoolVariable.h
View File

@ -41,6 +41,9 @@ public:
void setZeroValue(int _seq); void setZeroValue(int _seq);
/// Does nothing since the SMT solver already knows the valid values. /// Does nothing since the SMT solver already knows the valid values.
void setUnknownValue(int _seq); void setUnknownValue(int _seq);
protected:
smt::Expression valueAtSequence(int _seq) const;
}; };
} }

6
libsolidity/formal/SymbolicIntVariable.cpp
View File

@ -30,7 +30,11 @@ SymbolicIntVariable::SymbolicIntVariable(
SymbolicVariable(_decl, _interface) SymbolicVariable(_decl, _interface)
{ {
solAssert(m_declaration.type()->category() == Type::Category::Integer, ""); 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) void SymbolicIntVariable::setZeroValue(int _seq)

3
libsolidity/formal/SymbolicIntVariable.h
View File

@ -44,6 +44,9 @@ public:
static smt::Expression minValue(IntegerType const& _t); static smt::Expression minValue(IntegerType const& _t);
static smt::Expression maxValue(IntegerType const& _t); static smt::Expression maxValue(IntegerType const& _t);
protected:
smt::Expression valueAtSequence(int _seq) const;
}; };
} }

4
libsolidity/formal/SymbolicVariable.cpp
View File

@ -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);
} }

8
libsolidity/formal/SymbolicVariable.h
View File

@ -46,7 +46,7 @@ public:
return valueAtSequence(_seq); return valueAtSequence(_seq);
} }
std::string uniqueSymbol() const; std::string uniqueSymbol(int _seq) const;
/// Sets the var to the default value of its type. /// Sets the var to the default value of its type.
virtual void setZeroValue(int _seq) = 0; virtual void setZeroValue(int _seq) = 0;
@ -55,13 +55,9 @@ public:
virtual void setUnknownValue(int _seq) = 0; virtual void setUnknownValue(int _seq) = 0;
protected: protected:
smt::Expression valueAtSequence(int _seq) const virtual smt::Expression valueAtSequence(int _seq) const = 0;
{
return (*m_expression)(_seq);
}
Declaration const& m_declaration; Declaration const& m_declaration;
std::shared_ptr<smt::Expression> m_expression = nullptr;
smt::SolverInterface& m_interface; smt::SolverInterface& m_interface;
}; };