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 #5209 from ethereum/smt_ssa_refactor

Browse Source 
[SMTChecker] Refactor SSAVariable such that it only uses Type and not Declaration
This commit is contained in:
chriseth 2018-10-15 16:49:47 +02:00 committed by GitHub
commit 2384947521
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 48 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/SMTChecker.cpp
View File

@ -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

11
libsolidity/formal/SSAVariable.cpp
View File

@ -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, "");

7
libsolidity/formal/SSAVariable.h
View File

@ -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
);

7
libsolidity/formal/SymbolicBoolVariable.cpp
View File

@ -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

5
libsolidity/formal/SymbolicBoolVariable.h
View File

@ -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
);

30
libsolidity/formal/SymbolicIntVariable.cpp
View File

@ -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)

5
libsolidity/formal/SymbolicIntVariable.h
View File

@ -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
);

8
libsolidity/formal/SymbolicVariable.cpp
View File

@ -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);
}

10
libsolidity/formal/SymbolicVariable.h
View File

@ -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;
};