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

Supported types listed in SSAVariable

Browse Source
This commit is contained in:
Leonardo Alt 2018-02-17 09:35:37 +01:00
parent 3b2851ee41
commit 21c6b80fc9
4 changed files with 20 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsolidity/formal/SMTChecker.cpp
View File

@ -370,7 +370,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
{ {
// Will be translated as part of the node that requested the lvalue. // Will be translated as part of the node that requested the lvalue.
} }
else if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get())) else if (SSAVariable::supportedType(_identifier.annotation().type.get()))
defineExpr(_identifier, currentValue(*decl)); defineExpr(_identifier, currentValue(*decl));
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get())) else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{ {
@ -728,7 +728,7 @@ void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, sm
bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
{ {
if (dynamic_cast<IntegerType const*>(_varDecl.type().get())) if (SSAVariable::supportedType(_varDecl.type().get()))
{ {
solAssert(m_variables.count(&_varDecl) == 0, ""); solAssert(m_variables.count(&_varDecl) == 0, "");
m_variables.emplace(&_varDecl, SSAVariable(&_varDecl, *m_interface)); m_variables.emplace(&_varDecl, SSAVariable(&_varDecl, *m_interface));

7
libsolidity/formal/SSAVariable.cpp
View File

@ -34,10 +34,15 @@ SSAVariable::SSAVariable(Declaration const* _decl,
m_symbVar = make_shared<SymbolicIntVariable>(_decl, _interface); m_symbVar = make_shared<SymbolicIntVariable>(_decl, _interface);
else else
{ {
//solAssert(false, ""); solAssert(false, "");
} }
} }
bool SSAVariable::supportedType(Type const* _decl)
{
return dynamic_cast<IntegerType const*>(_decl);
}
void SSAVariable::resetIndex() void SSAVariable::resetIndex()
{ {
m_currentSequenceCounter = 0; m_currentSequenceCounter = 0;

9
libsolidity/formal/SSAVariable.h
View File

@ -34,6 +34,8 @@ class Declaration;
class SSAVariable class SSAVariable
{ {
public: public:
/// @param _decl Used to determine the type and forwarded to the symbolic var.
/// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver.
explicit SSAVariable(Declaration const* _decl, explicit SSAVariable(Declaration const* _decl,
smt::SolverInterface& _interface); smt::SolverInterface& _interface);
SSAVariable(SSAVariable const&) = default; SSAVariable(SSAVariable const&) = default;
@ -61,9 +63,14 @@ public:
return valueAtSequence(_seq); return valueAtSequence(_seq);
} }
/// These two functions forward the call to the symbolic var
/// which generates the constraints according to the type.
void setZeroValue(); void setZeroValue();
void setUnknownValue(); void setUnknownValue();
/// So far Int is supported.
static bool supportedType(Type const* _decl);
private: private:
smt::Expression valueAtSequence(int _seq) const smt::Expression valueAtSequence(int _seq) const
{ {
@ -72,6 +79,8 @@ private:
std::shared_ptr<SymbolicVariable> m_symbVar = nullptr; std::shared_ptr<SymbolicVariable> m_symbVar = nullptr;
int m_currentSequenceCounter; int m_currentSequenceCounter;
/// The next free sequence counter is a shared pointer because we want
/// the copy and the copied to share it.
std::shared_ptr<int> m_nextFreeSequenceCounter; std::shared_ptr<int> m_nextFreeSequenceCounter;
}; };

3
libsolidity/formal/SymbolicVariable.h
View File

@ -50,7 +50,10 @@ public:
std::string uniqueSymbol() const; std::string uniqueSymbol() const;
/// Sets the var to the default value of its type.
virtual void setZeroValue(int _seq) = 0; virtual void setZeroValue(int _seq) = 0;
/// The unknown value depends on the type. For example, an interval is set for Integers.
/// This is decided by the subclasses.
virtual void setUnknownValue(int _seq) = 0; virtual void setUnknownValue(int _seq) = 0;
protected: protected: