mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Refactor SymbolicAddressVariable and SymbolicVariable allocation
This commit is contained in:
parent
aa23326e06
commit
afe83cc28b
@ -257,14 +257,14 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
|
||||
void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location)
|
||||
{
|
||||
checkCondition(
|
||||
_value < SymbolicIntVariable::minValue(_type),
|
||||
_value < minValue(_type),
|
||||
_location,
|
||||
"Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
|
||||
"<result>",
|
||||
&_value
|
||||
);
|
||||
checkCondition(
|
||||
_value > SymbolicIntVariable::maxValue(_type),
|
||||
_value > maxValue(_type),
|
||||
_location,
|
||||
"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
|
||||
"<result>",
|
||||
@ -570,7 +570,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
|
||||
smt::Expression right(expr(_op.rightExpression()));
|
||||
Token::Value op = _op.getOperator();
|
||||
shared_ptr<smt::Expression> value;
|
||||
if (isInteger(_op.annotation().commonType->category()))
|
||||
if (isNumber(_op.annotation().commonType->category()))
|
||||
{
|
||||
value = make_shared<smt::Expression>(
|
||||
op == Token::Equal ? (left == right) :
|
||||
|
41
libsolidity/formal/SymbolicAddressVariable.cpp
Normal file
41
libsolidity/formal/SymbolicAddressVariable.cpp
Normal file
@ -0,0 +1,41 @@
|
||||
/*
|
||||
This file is part of solidity.
|
||||
|
||||
solidity is free software: you can redistribute it and/or modify
|
||||
it under the terms of the GNU General Public License as published by
|
||||
the Free Software Foundation, either version 3 of the License, or
|
||||
(at your option) any later version.
|
||||
|
||||
solidity is distributed in the hope that it will be useful,
|
||||
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
GNU General Public License for more details.
|
||||
|
||||
You should have received a copy of the GNU General Public License
|
||||
along with solidity. If not, see <http://www.gnu.org/licenses/>.
|
||||
*/
|
||||
|
||||
#include <libsolidity/formal/SymbolicAddressVariable.h>
|
||||
|
||||
#include <libsolidity/formal/SymbolicTypes.h>
|
||||
|
||||
using namespace std;
|
||||
using namespace dev;
|
||||
using namespace dev::solidity;
|
||||
|
||||
SymbolicAddressVariable::SymbolicAddressVariable(
|
||||
Type const& _type,
|
||||
string const& _uniqueName,
|
||||
smt::SolverInterface& _interface
|
||||
):
|
||||
SymbolicIntVariable(_type, _uniqueName, _interface)
|
||||
{
|
||||
solAssert(isAddress(_type.category()), "");
|
||||
}
|
||||
|
||||
void SymbolicAddressVariable::setUnknownValue()
|
||||
{
|
||||
IntegerType intType{160};
|
||||
m_interface.addAssertion(currentValue() >= minValue(intType));
|
||||
m_interface.addAssertion(currentValue() <= maxValue(intType));
|
||||
}
|
44
libsolidity/formal/SymbolicAddressVariable.h
Normal file
44
libsolidity/formal/SymbolicAddressVariable.h
Normal file
@ -0,0 +1,44 @@
|
||||
/*
|
||||
This file is part of solidity.
|
||||
|
||||
solidity is free software: you can redistribute it and/or modify
|
||||
it under the terms of the GNU General Public License as published by
|
||||
the Free Software Foundation, either version 3 of the License, or
|
||||
(at your option) any later version.
|
||||
|
||||
solidity is distributed in the hope that it will be useful,
|
||||
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
GNU General Public License for more details.
|
||||
|
||||
You should have received a copy of the GNU General Public License
|
||||
along with solidity. If not, see <http://www.gnu.org/licenses/>.
|
||||
*/
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <libsolidity/formal/SymbolicIntVariable.h>
|
||||
|
||||
namespace dev
|
||||
{
|
||||
namespace solidity
|
||||
{
|
||||
|
||||
/**
|
||||
* Specialization of SymbolicVariable for Address
|
||||
*/
|
||||
class SymbolicAddressVariable: public SymbolicIntVariable
|
||||
{
|
||||
public:
|
||||
SymbolicAddressVariable(
|
||||
Type const& _type,
|
||||
std::string const& _uniqueName,
|
||||
smt::SolverInterface& _interface
|
||||
);
|
||||
|
||||
/// Sets the variable to the full valid value range.
|
||||
void setUnknownValue();
|
||||
};
|
||||
|
||||
}
|
||||
}
|
@ -17,6 +17,8 @@
|
||||
|
||||
#include <libsolidity/formal/SymbolicIntVariable.h>
|
||||
|
||||
#include <libsolidity/formal/SymbolicTypes.h>
|
||||
|
||||
using namespace std;
|
||||
using namespace dev;
|
||||
using namespace dev::solidity;
|
||||
@ -28,11 +30,7 @@ SymbolicIntVariable::SymbolicIntVariable(
|
||||
):
|
||||
SymbolicVariable(_type, _uniqueName, _interface)
|
||||
{
|
||||
solAssert(
|
||||
_type.category() == Type::Category::Integer ||
|
||||
_type.category() == Type::Category::Address,
|
||||
""
|
||||
);
|
||||
solAssert(isNumber(_type.category()), "");
|
||||
}
|
||||
|
||||
smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
|
||||
@ -47,28 +45,8 @@ void SymbolicIntVariable::setZeroValue()
|
||||
|
||||
void SymbolicIntVariable::setUnknownValue()
|
||||
{
|
||||
if (m_type.category() == Type::Category::Integer)
|
||||
{
|
||||
auto intType = dynamic_cast<IntegerType const*>(&m_type);
|
||||
solAssert(intType, "");
|
||||
m_interface.addAssertion(currentValue() >= minValue(*intType));
|
||||
m_interface.addAssertion(currentValue() <= maxValue(*intType));
|
||||
}
|
||||
else
|
||||
{
|
||||
solAssert(m_type.category() == Type::Category::Address, "");
|
||||
IntegerType addrType{160};
|
||||
m_interface.addAssertion(currentValue() >= minValue(addrType));
|
||||
m_interface.addAssertion(currentValue() <= maxValue(addrType));
|
||||
}
|
||||
}
|
||||
|
||||
smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t)
|
||||
{
|
||||
return smt::Expression(_t.minValue());
|
||||
}
|
||||
|
||||
smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t)
|
||||
{
|
||||
return smt::Expression(_t.maxValue());
|
||||
auto intType = dynamic_cast<IntegerType const*>(&m_type);
|
||||
solAssert(intType, "");
|
||||
m_interface.addAssertion(currentValue() >= minValue(*intType));
|
||||
m_interface.addAssertion(currentValue() <= maxValue(*intType));
|
||||
}
|
||||
|
@ -39,10 +39,7 @@ public:
|
||||
/// Sets the var to 0.
|
||||
void setZeroValue();
|
||||
/// Sets the variable to the full valid value range.
|
||||
void setUnknownValue();
|
||||
|
||||
static smt::Expression minValue(IntegerType const& _t);
|
||||
static smt::Expression maxValue(IntegerType const& _t);
|
||||
virtual void setUnknownValue();
|
||||
|
||||
protected:
|
||||
smt::Expression valueAtIndex(int _index) const;
|
||||
|
@ -19,6 +19,7 @@
|
||||
|
||||
#include <libsolidity/formal/SymbolicBoolVariable.h>
|
||||
#include <libsolidity/formal/SymbolicIntVariable.h>
|
||||
#include <libsolidity/formal/SymbolicAddressVariable.h>
|
||||
|
||||
#include <libsolidity/ast/Types.h>
|
||||
|
||||
@ -29,7 +30,27 @@ using namespace dev::solidity;
|
||||
|
||||
bool dev::solidity::isSupportedType(Type::Category _category)
|
||||
{
|
||||
return isInteger(_category) || isBool(_category);
|
||||
return isInteger(_category) ||
|
||||
isAddress(_category) ||
|
||||
isBool(_category);
|
||||
}
|
||||
|
||||
shared_ptr<SymbolicVariable> dev::solidity::newSymbolicVariable(
|
||||
Type const& _type,
|
||||
std::string const& _uniqueName,
|
||||
smt::SolverInterface& _solver
|
||||
)
|
||||
{
|
||||
if (!isSupportedType(_type))
|
||||
return nullptr;
|
||||
if (isBool(_type.category()))
|
||||
return make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver);
|
||||
else if (isInteger(_type.category()))
|
||||
return make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
|
||||
else if (isAddress(_type.category()))
|
||||
return make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver);
|
||||
else
|
||||
solAssert(false, "");
|
||||
}
|
||||
|
||||
bool dev::solidity::isSupportedType(Type const& _type)
|
||||
@ -39,7 +60,7 @@ bool dev::solidity::isSupportedType(Type const& _type)
|
||||
|
||||
bool dev::solidity::isInteger(Type::Category _category)
|
||||
{
|
||||
return _category == Type::Category::Integer || _category == Type::Category::Address;
|
||||
return _category == Type::Category::Integer;
|
||||
}
|
||||
|
||||
bool dev::solidity::isInteger(Type const& _type)
|
||||
@ -47,6 +68,27 @@ bool dev::solidity::isInteger(Type const& _type)
|
||||
return isInteger(_type.category());
|
||||
}
|
||||
|
||||
bool dev::solidity::isAddress(Type::Category _category)
|
||||
{
|
||||
return _category == Type::Category::Address;
|
||||
}
|
||||
|
||||
bool dev::solidity::isAddress(Type const& _type)
|
||||
{
|
||||
return isAddress(_type.category());
|
||||
}
|
||||
|
||||
bool dev::solidity::isNumber(Type::Category _category)
|
||||
{
|
||||
return isInteger(_category) ||
|
||||
isAddress(_category);
|
||||
}
|
||||
|
||||
bool dev::solidity::isNumber(Type const& _type)
|
||||
{
|
||||
return isNumber(_type.category());
|
||||
}
|
||||
|
||||
bool dev::solidity::isBool(Type::Category _category)
|
||||
{
|
||||
return _category == Type::Category::Bool;
|
||||
@ -57,16 +99,12 @@ bool dev::solidity::isBool(Type const& _type)
|
||||
return isBool(_type.category());
|
||||
}
|
||||
|
||||
shared_ptr<SymbolicVariable> dev::solidity::newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver)
|
||||
smt::Expression dev::solidity::minValue(IntegerType const& _type)
|
||||
{
|
||||
if (!isSupportedType(_type))
|
||||
return nullptr;
|
||||
if (isBool(_type.category()))
|
||||
return make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver);
|
||||
else if (isInteger(_type.category()))
|
||||
return make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
|
||||
else
|
||||
solAssert(false, "");
|
||||
return smt::Expression(_type.minValue());
|
||||
}
|
||||
|
||||
|
||||
smt::Expression dev::solidity::maxValue(IntegerType const& _type)
|
||||
{
|
||||
return smt::Expression(_type.maxValue());
|
||||
}
|
||||
|
@ -36,10 +36,19 @@ bool isSupportedType(Type const& _type);
|
||||
bool isInteger(Type::Category _category);
|
||||
bool isInteger(Type const& _type);
|
||||
|
||||
bool isAddress(Type::Category _category);
|
||||
bool isAddress(Type const& _type);
|
||||
|
||||
bool isNumber(Type::Category _category);
|
||||
bool isNumber(Type const& _type);
|
||||
|
||||
bool isBool(Type::Category _category);
|
||||
bool isBool(Type const& _type);
|
||||
|
||||
std::shared_ptr<SymbolicVariable> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver);
|
||||
|
||||
smt::Expression minValue(IntegerType const& _type);
|
||||
smt::Expression maxValue(IntegerType const& _type);
|
||||
|
||||
}
|
||||
}
|
||||
|
@ -62,10 +62,11 @@ public:
|
||||
int& index() { return m_ssa->index(); }
|
||||
|
||||
/// Sets the var to the default value of its type.
|
||||
/// Inherited types must implement.
|
||||
virtual void setZeroValue() = 0;
|
||||
/// The unknown value is the full range of valid values,
|
||||
/// and that's sub-type dependent.
|
||||
virtual void setUnknownValue() = 0;
|
||||
/// The unknown value is the full range of valid values.
|
||||
/// It is sub-type dependent, but not mandatory.
|
||||
virtual void setUnknownValue() {}
|
||||
|
||||
protected:
|
||||
std::string uniqueSymbol(int _index) const;
|
||||
|
Loading…
Reference in New Issue
Block a user