aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2018-10-15 22:49:47 +0800
committerGitHub <noreply@github.com>2018-10-15 22:49:47 +0800
commit238494752192a2c834eb8913b244671afb48d693 (patch)
treed3e60cd464a03b98df9141386df9877bf418d577 /libsolidity
parent771de0c5adfe284c3824265999c1b9c07d66d0a1 (diff)
parent4a4620ac955d3c61b4778dfab3a9e05a91e4fc33 (diff)
downloaddexon-solidity-238494752192a2c834eb8913b244671afb48d693.tar.gz
dexon-solidity-238494752192a2c834eb8913b244671afb48d693.tar.zst
dexon-solidity-238494752192a2c834eb8913b244671afb48d693.zip
Merge pull request #5209 from ethereum/smt_ssa_refactor
[SMTChecker] Refactor SSAVariable such that it only uses Type and not Declaration
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/SMTChecker.cpp2
-rw-r--r--libsolidity/formal/SSAVariable.cpp11
-rw-r--r--libsolidity/formal/SSAVariable.h7
-rw-r--r--libsolidity/formal/SymbolicBoolVariable.cpp7
-rw-r--r--libsolidity/formal/SymbolicBoolVariable.h5
-rw-r--r--libsolidity/formal/SymbolicIntVariable.cpp30
-rw-r--r--libsolidity/formal/SymbolicIntVariable.h5
-rw-r--r--libsolidity/formal/SymbolicVariable.cpp8
-rw-r--r--libsolidity/formal/SymbolicVariable.h10
9 files changed, 48 insertions, 37 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 1e27dc33..0cb75530 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -924,7 +924,7 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
else if (SSAVariable::isSupportedType(_varDecl.type()->category()))
{
solAssert(m_variables.count(&_varDecl) == 0, "");
- m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
+ m_variables.emplace(&_varDecl, SSAVariable(*_varDecl.type(), _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface));
return true;
}
else
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
index 4fc2dd45..ceeea49a 100644
--- a/libsolidity/formal/SSAVariable.cpp
+++ b/libsolidity/formal/SSAVariable.cpp
@@ -27,16 +27,17 @@ using namespace dev;
using namespace dev::solidity;
SSAVariable::SSAVariable(
- Declaration const& _decl,
+ Type const& _type,
+ string const& _uniqueName,
smt::SolverInterface& _interface
)
{
resetIndex();
- if (isInteger(_decl.type()->category()))
- m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface);
- else if (isBool(_decl.type()->category()))
- m_symbolicVar = make_shared<SymbolicBoolVariable>(_decl, _interface);
+ if (isInteger(_type.category()))
+ m_symbolicVar = make_shared<SymbolicIntVariable>(_type, _uniqueName, _interface);
+ else if (isBool(_type.category()))
+ m_symbolicVar = make_shared<SymbolicBoolVariable>(_type, _uniqueName, _interface);
else
{
solAssert(false, "");
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
index bf5dae3b..f4a4e93e 100644
--- a/libsolidity/formal/SSAVariable.h
+++ b/libsolidity/formal/SSAVariable.h
@@ -26,18 +26,17 @@ namespace dev
namespace solidity
{
-class Declaration;
-
/**
* This class represents the SSA representation of a program variable.
*/
class SSAVariable
{
public:
- /// @param _decl Used to determine the type and forwarded to the symbolic var.
+ /// @param _type Forwarded to the symbolic var.
/// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver.
SSAVariable(
- Declaration const& _decl,
+ Type const& _type,
+ std::string const& _uniqueName,
smt::SolverInterface& _interface
);
diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp
index 5cf22d7d..5e5aec8f 100644
--- a/libsolidity/formal/SymbolicBoolVariable.cpp
+++ b/libsolidity/formal/SymbolicBoolVariable.cpp
@@ -24,12 +24,13 @@ using namespace dev;
using namespace dev::solidity;
SymbolicBoolVariable::SymbolicBoolVariable(
- Declaration const& _decl,
+ Type const& _type,
+ string const& _uniqueName,
smt::SolverInterface&_interface
):
- SymbolicVariable(_decl, _interface)
+ SymbolicVariable(_type, _uniqueName, _interface)
{
- solAssert(m_declaration.type()->category() == Type::Category::Bool, "");
+ solAssert(_type.category() == Type::Category::Bool, "");
}
smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const
diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h
index 678f97d9..33ac9061 100644
--- a/libsolidity/formal/SymbolicBoolVariable.h
+++ b/libsolidity/formal/SymbolicBoolVariable.h
@@ -19,8 +19,6 @@
#include <libsolidity/formal/SymbolicVariable.h>
-#include <libsolidity/ast/Types.h>
-
namespace dev
{
namespace solidity
@@ -33,7 +31,8 @@ class SymbolicBoolVariable: public SymbolicVariable
{
public:
SymbolicBoolVariable(
- Declaration const& _decl,
+ Type const& _type,
+ std::string const& _uniqueName,
smt::SolverInterface& _interface
);
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
index 4f65b1fd..0adb9d09 100644
--- a/libsolidity/formal/SymbolicIntVariable.cpp
+++ b/libsolidity/formal/SymbolicIntVariable.cpp
@@ -17,21 +17,20 @@
#include <libsolidity/formal/SymbolicIntVariable.h>
-#include <libsolidity/ast/AST.h>
-
using namespace std;
using namespace dev;
using namespace dev::solidity;
SymbolicIntVariable::SymbolicIntVariable(
- Declaration const& _decl,
+ Type const& _type,
+ string const& _uniqueName,
smt::SolverInterface& _interface
):
- SymbolicVariable(_decl, _interface)
+ SymbolicVariable(_type, _uniqueName, _interface)
{
solAssert(
- m_declaration.type()->category() == Type::Category::Integer ||
- m_declaration.type()->category() == Type::Category::Address,
+ _type.category() == Type::Category::Integer ||
+ _type.category() == Type::Category::Address,
""
);
}
@@ -48,11 +47,20 @@ void SymbolicIntVariable::setZeroValue(int _seq)
void SymbolicIntVariable::setUnknownValue(int _seq)
{
- auto intType = dynamic_pointer_cast<IntegerType const>(m_declaration.type());
- if (!intType)
- intType = make_shared<IntegerType>(160);
- m_interface.addAssertion(valueAtSequence(_seq) >= minValue(*intType));
- m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(*intType));
+ if (m_type.category() == Type::Category::Integer)
+ {
+ auto intType = dynamic_cast<IntegerType const*>(&m_type);
+ solAssert(intType, "");
+ m_interface.addAssertion(valueAtSequence(_seq) >= minValue(*intType));
+ m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(*intType));
+ }
+ else
+ {
+ solAssert(m_type.category() == Type::Category::Address, "");
+ IntegerType addrType{160};
+ m_interface.addAssertion(valueAtSequence(_seq) >= minValue(addrType));
+ m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(addrType));
+ }
}
smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t)
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
index d591e8db..92eeb13d 100644
--- a/libsolidity/formal/SymbolicIntVariable.h
+++ b/libsolidity/formal/SymbolicIntVariable.h
@@ -19,8 +19,6 @@
#include <libsolidity/formal/SymbolicVariable.h>
-#include <libsolidity/ast/Types.h>
-
namespace dev
{
namespace solidity
@@ -33,7 +31,8 @@ class SymbolicIntVariable: public SymbolicVariable
{
public:
SymbolicIntVariable(
- Declaration const& _decl,
+ Type const& _type,
+ std::string const& _uniqueName,
smt::SolverInterface& _interface
);
diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp
index caefa3a3..afbc01ba 100644
--- a/libsolidity/formal/SymbolicVariable.cpp
+++ b/libsolidity/formal/SymbolicVariable.cpp
@@ -24,17 +24,19 @@ using namespace dev;
using namespace dev::solidity;
SymbolicVariable::SymbolicVariable(
- Declaration const& _decl,
+ Type const& _type,
+ string const& _uniqueName,
smt::SolverInterface& _interface
):
- m_declaration(_decl),
+ m_type(_type),
+ m_uniqueName(_uniqueName),
m_interface(_interface)
{
}
string SymbolicVariable::uniqueSymbol(int _seq) const
{
- return m_declaration.name() + "_" + to_string(m_declaration.id()) + "_" + to_string(_seq);
+ return m_uniqueName + "_" + to_string(_seq);
}
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
index e29ded26..977515f8 100644
--- a/libsolidity/formal/SymbolicVariable.h
+++ b/libsolidity/formal/SymbolicVariable.h
@@ -19,7 +19,7 @@
#include <libsolidity/formal/SolverInterface.h>
-#include <libsolidity/ast/AST.h>
+#include <libsolidity/ast/Types.h>
#include <memory>
@@ -28,7 +28,7 @@ namespace dev
namespace solidity
{
-class Declaration;
+class Type;
/**
* This class represents the symbolic version of a program variable.
@@ -37,7 +37,8 @@ class SymbolicVariable
{
public:
SymbolicVariable(
- Declaration const& _decl,
+ Type const& _type,
+ std::string const& _uniqueName,
smt::SolverInterface& _interface
);
virtual ~SymbolicVariable() = default;
@@ -58,7 +59,8 @@ public:
protected:
virtual smt::Expression valueAtSequence(int _seq) const = 0;
- Declaration const& m_declaration;
+ Type const& m_type;
+ std::string m_uniqueName;
smt::SolverInterface& m_interface;
};