aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLeonardo Alt <leonardoaltt@gmail.com>2018-02-17 16:35:37 +0800
committerLeonardo Alt <leonardoaltt@gmail.com>2018-03-01 01:05:20 +0800
commit21c6b80fc98f6d584f240a47d4a01827768f18f3 (patch)
treebdd168818053f5d983fb57bcef9c36f2738541cb
parent3b2851ee4163bcfbca9e4e23650dfeee1a06653a (diff)
downloaddexon-solidity-21c6b80fc98f6d584f240a47d4a01827768f18f3.tar.gz
dexon-solidity-21c6b80fc98f6d584f240a47d4a01827768f18f3.tar.zst
dexon-solidity-21c6b80fc98f6d584f240a47d4a01827768f18f3.zip
Supported types listed in SSAVariable
-rw-r--r--libsolidity/formal/SMTChecker.cpp4
-rw-r--r--libsolidity/formal/SSAVariable.cpp7
-rw-r--r--libsolidity/formal/SSAVariable.h9
-rw-r--r--libsolidity/formal/SymbolicVariable.h3
4 files changed, 20 insertions, 3 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index ad42c105..1da5b291 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -370,7 +370,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
{
// 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));
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)
{
- if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
+ if (SSAVariable::supportedType(_varDecl.type().get()))
{
solAssert(m_variables.count(&_varDecl) == 0, "");
m_variables.emplace(&_varDecl, SSAVariable(&_varDecl, *m_interface));
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
index d6e97a8d..7f214687 100644
--- a/libsolidity/formal/SSAVariable.cpp
+++ b/libsolidity/formal/SSAVariable.cpp
@@ -34,10 +34,15 @@ SSAVariable::SSAVariable(Declaration const* _decl,
m_symbVar = make_shared<SymbolicIntVariable>(_decl, _interface);
else
{
- //solAssert(false, "");
+ solAssert(false, "");
}
}
+bool SSAVariable::supportedType(Type const* _decl)
+{
+ return dynamic_cast<IntegerType const*>(_decl);
+}
+
void SSAVariable::resetIndex()
{
m_currentSequenceCounter = 0;
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
index 3d7eb80c..b87693c2 100644
--- a/libsolidity/formal/SSAVariable.h
+++ b/libsolidity/formal/SSAVariable.h
@@ -34,6 +34,8 @@ class Declaration;
class SSAVariable
{
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,
smt::SolverInterface& _interface);
SSAVariable(SSAVariable const&) = default;
@@ -61,9 +63,14 @@ public:
return valueAtSequence(_seq);
}
+ /// These two functions forward the call to the symbolic var
+ /// which generates the constraints according to the type.
void setZeroValue();
void setUnknownValue();
+ /// So far Int is supported.
+ static bool supportedType(Type const* _decl);
+
private:
smt::Expression valueAtSequence(int _seq) const
{
@@ -72,6 +79,8 @@ private:
std::shared_ptr<SymbolicVariable> m_symbVar = nullptr;
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;
};
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
index 4de59504..66633b73 100644
--- a/libsolidity/formal/SymbolicVariable.h
+++ b/libsolidity/formal/SymbolicVariable.h
@@ -50,7 +50,10 @@ public:
std::string uniqueSymbol() const;
+ /// Sets the var to the default value of its type.
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;
protected: