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

Merge pull request #7041 from ethereum/smt_function_sort

Browse Source 
[SMTChecker] Allow symbolic functions to be created via Sort
This commit is contained in:
chriseth 2019-07-08 12:33:38 +02:00 committed by GitHub
commit aac226f7c1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 23 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
libsolidity/formal/SymbolicVariables.cpp
View File

@ -68,6 +68,11 @@ Expression SymbolicVariable::valueAtIndex(int _index) const
return m_context.newVariable(uniqueSymbol(_index), m_sort); return m_context.newVariable(uniqueSymbol(_index), m_sort);
} }
string SymbolicVariable::nameAtIndex(int _index) const
{
return uniqueSymbol(_index);
}
string SymbolicVariable::uniqueSymbol(unsigned _index) const string SymbolicVariable::uniqueSymbol(unsigned _index) const
{ {
return m_uniqueName + "_" + to_string(_index); return m_uniqueName + "_" + to_string(_index);
@ -127,6 +132,17 @@ SymbolicFunctionVariable::SymbolicFunctionVariable(
solAssert(m_type->category() == solidity::Type::Category::Function, ""); solAssert(m_type->category() == solidity::Type::Category::Function, "");
} }
SymbolicFunctionVariable::SymbolicFunctionVariable(
SortPointer _sort,
string _uniqueName,
EncodingContext& _context
):
SymbolicVariable(move(_sort), move(_uniqueName), _context),
m_declaration(m_context.newVariable(currentName(), m_sort))
{
solAssert(m_sort->kind == Kind::Function, "");
}
void SymbolicFunctionVariable::resetDeclaration() void SymbolicFunctionVariable::resetDeclaration()
{ {
m_declaration = m_context.newVariable(currentName(), m_sort); m_declaration = m_context.newVariable(currentName(), m_sort);

7
libsolidity/formal/SymbolicVariables.h
View File

@ -54,6 +54,7 @@ public:
Expression currentValue() const; Expression currentValue() const;
std::string currentName() const; std::string currentName() const;
virtual Expression valueAtIndex(int _index) const; virtual Expression valueAtIndex(int _index) const;
virtual std::string nameAtIndex(int _index) const;
virtual Expression increaseIndex(); virtual Expression increaseIndex();
virtual Expression operator()(std::vector<Expression> /*_arguments*/) const virtual Expression operator()(std::vector<Expression> /*_arguments*/) const
{ {
@ -63,6 +64,7 @@ public:
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(); }
SortPointer const& sort() const { return m_sort; }
solidity::TypePointer const& type() const { return m_type; } solidity::TypePointer const& type() const { return m_type; }
protected: protected:
@ -139,6 +141,11 @@ public:
std::string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
); );
SymbolicFunctionVariable(
SortPointer _sort,
std::string _uniqueName,
EncodingContext& _context
);
Expression increaseIndex(); Expression increaseIndex();
Expression operator()(std::vector<Expression> _arguments) const; Expression operator()(std::vector<Expression> _arguments) const;