cerc-io/solidity
10
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] Simplify symbolic variables

Browse Source
This commit is contained in:
Leonardo Alt 2018-12-05 09:56:52 +01:00
parent 6efe2a5266
commit b9f424e373
2 changed files with 19 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
libsolidity/formal/SymbolicVariables.cpp
View File

@ -37,16 +37,32 @@ SymbolicVariable::SymbolicVariable(
{ {
} }
smt::Expression SymbolicVariable::currentValue() const
{
return valueAtIndex(m_ssa->index());
}
string SymbolicVariable::currentName() const string SymbolicVariable::currentName() const
{ {
return uniqueSymbol(m_ssa->index()); return uniqueSymbol(m_ssa->index());
} }
smt::Expression SymbolicVariable::valueAtIndex(int _index) const
{
return m_interface.newVariable(uniqueSymbol(_index), smtSort(*m_type));
}
string SymbolicVariable::uniqueSymbol(unsigned _index) const string SymbolicVariable::uniqueSymbol(unsigned _index) const
{ {
return m_uniqueName + "_" + to_string(_index); return m_uniqueName + "_" + to_string(_index);
} }
smt::Expression SymbolicVariable::increaseIndex()
{
++(*m_ssa);
return currentValue();
}
SymbolicBoolVariable::SymbolicBoolVariable( SymbolicBoolVariable::SymbolicBoolVariable(
TypePointer _type, TypePointer _type,
string const& _uniqueName, string const& _uniqueName,
@ -57,11 +73,6 @@ SymbolicBoolVariable::SymbolicBoolVariable(
solAssert(m_type->category() == Type::Category::Bool, ""); solAssert(m_type->category() == Type::Category::Bool, "");
} }
smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
{
return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Bool));
}
SymbolicIntVariable::SymbolicIntVariable( SymbolicIntVariable::SymbolicIntVariable(
TypePointer _type, TypePointer _type,
string const& _uniqueName, string const& _uniqueName,
@ -72,11 +83,6 @@ SymbolicIntVariable::SymbolicIntVariable(
solAssert(isNumber(m_type->category()), ""); solAssert(isNumber(m_type->category()), "");
} }
smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
{
return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Int));
}
SymbolicAddressVariable::SymbolicAddressVariable( SymbolicAddressVariable::SymbolicAddressVariable(
string const& _uniqueName, string const& _uniqueName,
smt::SolverInterface& _interface smt::SolverInterface& _interface

22
libsolidity/formal/SymbolicVariables.h
View File

@ -46,20 +46,10 @@ public:
virtual ~SymbolicVariable() = default; virtual ~SymbolicVariable() = default;
smt::Expression currentValue() const smt::Expression currentValue() const;
{
return valueAtIndex(m_ssa->index());
}
std::string currentName() const; std::string currentName() const;
virtual smt::Expression valueAtIndex(int _index) const;
virtual smt::Expression valueAtIndex(int _index) const = 0; smt::Expression increaseIndex();
smt::Expression increaseIndex()
{
++(*m_ssa);
return currentValue();
}
unsigned index() const { return m_ssa->index(); } unsigned index() const { return m_ssa->index(); }
unsigned& index() { return m_ssa->index(); } unsigned& index() { return m_ssa->index(); }
@ -86,9 +76,6 @@ public:
std::string const& _uniqueName, std::string const& _uniqueName,
smt::SolverInterface& _interface smt::SolverInterface& _interface
); );
protected:
smt::Expression valueAtIndex(int _index) const;
}; };
/** /**
@ -102,9 +89,6 @@ public:
std::string const& _uniqueName, std::string const& _uniqueName,
smt::SolverInterface& _interface smt::SolverInterface& _interface
); );
protected:
smt::Expression valueAtIndex(int _index) const;
}; };
/** /**