cerc-io/solidity
11
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

libsolidity: Introducing TypeProvider API, for clear type system ownership.

Browse Source
This commit is contained in:
Christian Parpart
2019-04-16 18:26:45 +02:00
committed by chriseth
parent 862d798047
commit bf43eebea9
38 changed files with 1489 additions and 837 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTChecker.cpp
+12 -11
View File
@@ -17,6 +17,7 @@
#include <libsolidity/formal/SMTChecker.h>
#include <libsolidity/ast/TypeProvider.h>
#include <libsolidity/formal/SMTPortfolio.h>
#include <libsolidity/formal/SymbolicTypes.h>
@@ -447,7 +448,7 @@ void SMTChecker::checkUnderOverflow()
void SMTChecker::checkUnderflow(OverflowTarget& _target)
{
solAssert(_target.type != OverflowTarget::Type::Overflow, "");
auto intType = dynamic_cast<IntegerType const*>(_target.intType.get());
auto intType = dynamic_cast<IntegerType const*>(_target.intType);
checkCondition(
_target.path && _target.value < minValue(*intType),
_target.location,
@@ -460,7 +461,7 @@ void SMTChecker::checkUnderflow(OverflowTarget& _target)
void SMTChecker::checkOverflow(OverflowTarget& _target)
{
solAssert(_target.type != OverflowTarget::Type::Underflow, "");
auto intType = dynamic_cast<IntegerType const*>(_target.intType.get());
auto intType = dynamic_cast<IntegerType const*>(_target.intType);
checkCondition(
_target.path && _target.value > maxValue(*intType),
_target.location,
@@ -681,7 +682,7 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
{
vector<smt::Expression> funArgs;
Expression const* calledExpr = &_funCall.expression();
auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type.get());
auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
solAssert(funType, "");
if (funType->bound())
{
@@ -803,8 +804,8 @@ void SMTChecker::endVisit(Literal const& _literal)
{
if (type.category() == Type::Category::StringLiteral)
{
auto stringType = make_shared<ArrayType>(DataLocation::Memory, true);
auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type.get());
auto stringType = TypeProvider::stringMemoryType();
auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type);
solAssert(stringLit, "");
auto result = newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface);
m_expressions.emplace(&_literal, result.second);
@@ -859,7 +860,7 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
{
if (identifier && dynamic_cast<EnumDefinition const*>(identifier->annotation().referencedDeclaration))
{
auto enumType = dynamic_cast<EnumType const*>(accessType.get());
auto enumType = dynamic_cast<EnumType const*>(accessType);
solAssert(enumType, "");
defineExpr(_memberAccess, enumType->memberValue(_memberAccess.memberName()));
}
@@ -939,13 +940,13 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c
return true;
if (prefix->category() == Type::Category::Mapping)
{
auto mapPrefix = dynamic_cast<MappingType const*>(prefix.get());
auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
solAssert(mapPrefix, "");
prefix = mapPrefix->valueType();
}
else
{
auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix.get());
auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
solAssert(arrayPrefix, "");
prefix = arrayPrefix->baseType();
}
@@ -1017,7 +1018,7 @@ bool SMTChecker::shortcutRationalNumber(Expression const& _expr)
{
if (_expr.annotation().type->category() == Type::Category::RationalNumber)
{
auto rationalType = dynamic_cast<RationalNumberType const*>(_expr.annotation().type.get());
auto rationalType = dynamic_cast<RationalNumberType const*>(_expr.annotation().type);
solAssert(rationalType, "");
if (rationalType->isNegative())
defineExpr(_expr, smt::Expression(u2s(rationalType->literalValue(nullptr))));
@@ -1205,7 +1206,7 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio
if (type->category() == Type::Category::Integer)
addOverflowTarget(OverflowTarget::Type::All, type, _value, _location);
else if (type->category() == Type::Category::Address)
addOverflowTarget(OverflowTarget::Type::All, make_shared<IntegerType>(160), _value, _location);
addOverflowTarget(OverflowTarget::Type::All, TypeProvider::integerType(160), _value, _location);
else if (type->category() == Type::Category::Mapping)
arrayAssignment();
m_interface->addAssertion(newValue(_variable) == _value);
@@ -1522,7 +1523,7 @@ void SMTChecker::resetVariables(function<bool(VariableDeclaration const&)> const
TypePointer SMTChecker::typeWithoutPointer(TypePointer const& _type)
{
if (auto refType = dynamic_cast<ReferenceType const*>(_type.get()))
if (auto refType = dynamic_cast<ReferenceType const*>(_type))
return ReferenceType::copyForLocationIfReference(refType->location(), _type);
return _type;
}
libsolidity/formal/SMTChecker.h
+1 -1
View File
@@ -178,7 +178,7 @@ private:
location(_location),
callStack(move(_callStack))
{
solAssert(dynamic_cast<IntegerType const*>(intType.get()), "");
solAssert(dynamic_cast<IntegerType const*>(intType), "");
}
};
libsolidity/formal/SymbolicTypes.cpp
+7 -6
View File
@@ -17,6 +17,7 @@
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/ast/TypeProvider.h>
#include <libsolidity/ast/Types.h>
#include <memory>
@@ -115,11 +116,11 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
{
bool abstract = false;
shared_ptr<SymbolicVariable> var;
TypePointer type = _type.shared_from_this();
TypePointer type = &_type;
if (!isSupportedTypeDeclaration(_type))
{
abstract = true;
var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
var = make_shared<SymbolicIntVariable>(TypeProvider::integerType(256), _uniqueName, _solver);
}
else if (isBool(_type.category()))
var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _solver);
@@ -129,7 +130,7 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
else if (isFixedBytes(_type.category()))
{
auto fixedBytesType = dynamic_cast<FixedBytesType const*>(type.get());
auto fixedBytesType = dynamic_cast<FixedBytesType const*>(type);
solAssert(fixedBytesType, "");
var = make_shared<SymbolicFixedBytesVariable>(fixedBytesType->numBytes(), _uniqueName, _solver);
}
@@ -142,7 +143,7 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
auto rational = dynamic_cast<RationalNumberType const*>(&_type);
solAssert(rational, "");
if (rational->isFractional())
var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
var = make_shared<SymbolicIntVariable>(TypeProvider::integerType(256), _uniqueName, _solver);
else
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
}
@@ -253,14 +254,14 @@ void dev::solidity::smt::setSymbolicUnknownValue(smt::Expression _expr, TypePoin
solAssert(_type, "");
if (isEnum(_type->category()))
{
auto enumType = dynamic_cast<EnumType const*>(_type.get());
auto enumType = dynamic_cast<EnumType const*>(_type);
solAssert(enumType, "");
_interface.addAssertion(_expr >= 0);
_interface.addAssertion(_expr < enumType->numberOfMembers());
}
else if (isInteger(_type->category()))
{
auto intType = dynamic_cast<IntegerType const*>(_type.get());
auto intType = dynamic_cast<IntegerType const*>(_type);
solAssert(intType, "");
_interface.addAssertion(_expr >= minValue(*intType));
_interface.addAssertion(_expr <= maxValue(*intType));
libsolidity/formal/SymbolicVariables.cpp
+3 -2
View File
@@ -19,6 +19,7 @@
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/ast/AST.h>
#include <libsolidity/ast/TypeProvider.h>
using namespace std;
using namespace dev;
@@ -102,7 +103,7 @@ SymbolicAddressVariable::SymbolicAddressVariable(
string _uniqueName,
smt::SolverInterface& _interface
):
SymbolicIntVariable(make_shared<IntegerType>(160), move(_uniqueName), _interface)
SymbolicIntVariable(TypeProvider::integerType(160), move(_uniqueName), _interface)
{
}
@@ -111,7 +112,7 @@ SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
string _uniqueName,
smt::SolverInterface& _interface
):
SymbolicIntVariable(make_shared<IntegerType>(_numBytes * 8), move(_uniqueName), _interface)
SymbolicIntVariable(TypeProvider::integerType(_numBytes * 8), move(_uniqueName), _interface)
{
}