cerc-io/solidity
16
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 #5614 from ethereum/smt_symb_function

Browse Source 
[SMTChecker] Introduce SymbolicFunctionVariable
This commit is contained in:
Leonardo 2018-12-10 12:57:07 +01:00 committed by GitHub
commit 0300e09d3e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 56 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
libsolidity/formal/SymbolicVariables.cpp
View File

@ -99,3 +99,31 @@ SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
SymbolicIntVariable(make_shared<IntegerType>(_numBytes * 8), _uniqueName, _interface) SymbolicIntVariable(make_shared<IntegerType>(_numBytes * 8), _uniqueName, _interface)
{ {
} }
SymbolicFunctionVariable::SymbolicFunctionVariable(
TypePointer _type,
string const& _uniqueName,
smt::SolverInterface&_interface
):
SymbolicVariable(move(_type), _uniqueName, _interface),
m_declaration(m_interface.newVariable(currentName(), smtSort(*m_type)))
{
solAssert(m_type->category() == Type::Category::Function, "");
}
void SymbolicFunctionVariable::resetDeclaration()
{
m_declaration = m_interface.newVariable(currentName(), smtSort(*m_type));
}
smt::Expression SymbolicFunctionVariable::increaseIndex()
{
++(*m_ssa);
resetDeclaration();
return currentValue();
}
smt::Expression SymbolicFunctionVariable::operator()(vector<smt::Expression> _arguments) const
{
return m_declaration(_arguments);
}

29
libsolidity/formal/SymbolicVariables.h
View File

@ -49,7 +49,11 @@ public:
smt::Expression currentValue() const; smt::Expression currentValue() const;
std::string currentName() const; std::string currentName() const;
virtual smt::Expression valueAtIndex(int _index) const; virtual smt::Expression valueAtIndex(int _index) const;
smt::Expression increaseIndex(); virtual smt::Expression increaseIndex();
virtual smt::Expression operator()(std::vector<smt::Expression> /*_arguments*/) const
{
solAssert(false, "Function application to non-function.");
}
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(); }
@ -116,5 +120,28 @@ public:
); );
}; };
/**
* Specialization of SymbolicVariable for FunctionType
*/
class SymbolicFunctionVariable: public SymbolicVariable
{
public:
SymbolicFunctionVariable(
TypePointer _type,
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
smt::Expression increaseIndex();
smt::Expression operator()(std::vector<smt::Expression> _arguments) const;
private:
/// Creates a new function declaration.
void resetDeclaration();
/// Stores the current function declaration.
smt::Expression m_declaration;
};
} }
} }