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

Make recursive structs unsupported

Browse Source
This commit is contained in:
Leonardo Alt 2020-08-27 15:16:02 +02:00
parent 3093648c05
commit 7b3cd019d4
5 changed files with 134 additions and 127 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/BMC.cpp
View File

@ -580,7 +580,7 @@ pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
auto const& type = var.second->type();
if (
type->isValueType() &&
smt::smtKind(type->category()) != smtutil::Kind::Function
smt::smtKind(*type) != smtutil::Kind::Function
)
{
expressionsToEvaluate.emplace_back(var.second->currentValue());

46
libsolidity/formal/SMTEncoder.cpp
View File

@ -378,7 +378,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
"Assertion checker does not yet implement this assignment operator."
);
}
else if (!smt::isSupportedType(_assignment.annotation().type->category()))
else if (!smt::isSupportedType(*_assignment.annotation().type))
{
// Give it a new index anyway to keep the SSA scheme sound.
@ -462,20 +462,19 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
createExpr(_op);
auto const* subExpr = innermostTuple(_op.subExpression());
auto type = _op.annotation().type;
switch (_op.getOperator())
{
case Token::Not: // !
{
solAssert(smt::isBool(_op.annotation().type->category()), "");
solAssert(smt::isBool(*type), "");
defineExpr(_op, !expr(*subExpr));
break;
}
case Token::Inc: // ++ (pre- or postfix)
case Token::Dec: // -- (pre- or postfix)
{
auto cat = _op.annotation().type->category();
solAssert(smt::isInteger(cat) || smt::isFixedPoint(cat), "");
solAssert(smt::isInteger(*type) || smt::isFixedPoint(*type), "");
solAssert(subExpr->annotation().willBeWrittenTo, "");
if (auto identifier = dynamic_cast<Identifier const*>(subExpr))
{
@ -486,7 +485,10 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
assignment(*decl, newValue);
}
else if (dynamic_cast<IndexAccess const*>(subExpr))
else if (
dynamic_cast<IndexAccess const*>(&_op.subExpression()) ||
dynamic_cast<MemberAccess const*>(&_op.subExpression())
)
{
auto innerValue = expr(*subExpr);
auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
@ -824,11 +826,11 @@ void SMTEncoder::endVisit(Literal const& _literal)
{
solAssert(_literal.annotation().type, "Expected type for AST node");
Type const& type = *_literal.annotation().type;
if (smt::isNumber(type.category()))
if (smt::isNumber(type))
defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal)));
else if (smt::isBool(type.category()))
else if (smt::isBool(type))
defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false));
else if (smt::isStringLiteral(type.category()))
else if (smt::isStringLiteral(type))
createExpr(_literal);
else
{
@ -891,7 +893,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
defineGlobalVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
return false;
}
else if (exprType->category() == Type::Category::Struct)
else if (smt::isNonRecursiveStruct(*exprType))
{
_memberAccess.expression().accept(*this);
auto const& symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(_memberAccess.expression()));
@ -1034,6 +1036,20 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
auto const& base = memberAccess->expression();
if (dynamic_cast<Identifier const*>(&base))
base.accept(*this);
if (
auto const* structType = dynamic_cast<StructType const*>(base.annotation().type);
structType && structType->recursive()
)
{
m_errorReporter.warning(
4375_error,
memberAccess->location(),
"Assertion checker does not support recursive structs."
);
return;
}
auto symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(base));
solAssert(symbStruct, "");
symbStruct->assignMember(memberAccess->memberName(), toStore);
@ -1186,7 +1202,7 @@ void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _ex
m_context.globalSymbol(_name)->increaseIndex();
// The default behavior is not to increase the index since
// most of the global values stay the same throughout a tx.
if (smt::isSupportedType(_expr.annotation().type->category()))
if (smt::isSupportedType(*_expr.annotation().type))
defineExpr(_expr, m_context.globalSymbol(_name)->currentValue());
}
@ -1339,13 +1355,13 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
{
auto const& commonType = _op.annotation().commonType;
solAssert(commonType, "");
if (smt::isSupportedType(commonType->category()))
if (smt::isSupportedType(*commonType))
{
smtutil::Expression left(expr(_op.leftExpression(), commonType));
smtutil::Expression right(expr(_op.rightExpression(), commonType));
Token op = _op.getOperator();
shared_ptr<smtutil::Expression> value;
if (smt::isNumber(commonType->category()))
if (smt::isNumber(*commonType))
{
value = make_shared<smtutil::Expression>(
op == Token::Equal ? (left == right) :
@ -1358,7 +1374,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
}
else // Bool
{
solUnimplementedAssert(smt::isBool(commonType->category()), "Operation not yet supported");
solUnimplementedAssert(smt::isBool(*commonType), "Operation not yet supported");
value = make_shared<smtutil::Expression>(
op == Token::Equal ? (left == right) :
/*op == Token::NotEqual*/ (left != right)
@ -1464,7 +1480,7 @@ void SMTEncoder::assignment(
Expression const* left = innermostTuple(_left);
if (!smt::isSupportedType(_type->category()))
if (!smt::isSupportedType(*_type))
{
// Give it a new index anyway to keep the SSA scheme sound.
if (auto varDecl = identifierToVariable(*left))

167
libsolidity/formal/SymbolicTypes.cpp
View File

@ -33,7 +33,7 @@ namespace solidity::frontend::smt
SortPointer smtSort(frontend::Type const& _type)
{
switch (smtKind(_type.category()))
switch (smtKind(_type))
{
case Kind::Int:
if (auto const* intType = dynamic_cast<IntegerType const*>(&_type))
@ -64,13 +64,13 @@ SortPointer smtSort(frontend::Type const& _type)
case Kind::Array:
{
shared_ptr<ArraySort> array;
if (isMapping(_type.category()))
if (isMapping(_type))
{
auto mapType = dynamic_cast<frontend::MappingType const*>(&_type);
solAssert(mapType, "");
array = make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
}
else if (isStringLiteral(_type.category()))
else if (isStringLiteral(_type))
{
auto stringLitType = dynamic_cast<frontend::StringLiteralType const*>(&_type);
solAssert(stringLitType, "");
@ -144,6 +144,7 @@ SortPointer smtSort(frontend::Type const& _type)
}
else if (auto const* structType = dynamic_cast<frontend::StructType const*>(&_type))
{
solAssert(!structType->recursive(), "");
auto const& structMembers = structType->structDefinition().members();
for (auto member: structMembers)
members.emplace_back(tupleName + "_accessor_" + member->name());
@ -173,7 +174,7 @@ vector<SortPointer> smtSort(vector<frontend::TypePointer> const& _types)
SortPointer smtSortAbstractFunction(frontend::Type const& _type)
{
if (isFunction(_type.category()))
if (isFunction(_type))
return SortProvider::uintSort;
return smtSort(_type);
}
@ -189,36 +190,36 @@ vector<SortPointer> smtSortAbstractFunction(vector<frontend::TypePointer> const&
return sorts;
}
Kind smtKind(frontend::Type::Category _category)
Kind smtKind(frontend::Type const& _type)
{
if (isNumber(_category))
if (isNumber(_type))
return Kind::Int;
else if (isBool(_category))
else if (isBool(_type))
return Kind::Bool;
else if (isFunction(_category))
else if (isFunction(_type))
return Kind::Function;
else if (isMapping(_category) || isArray(_category))
else if (isMapping(_type) || isArray(_type))
return Kind::Array;
else if (isTuple(_category) || isStruct(_category))
else if (isTuple(_type) || isNonRecursiveStruct(_type))
return Kind::Tuple;
// Abstract case.
return Kind::Int;
}
bool isSupportedType(frontend::Type::Category _category)
bool isSupportedType(frontend::Type const& _type)
{
return isNumber(_category) ||
isBool(_category) ||
isMapping(_category) ||
isArray(_category) ||
isTuple(_category) ||
isStruct(_category);
return isNumber(_type) ||
isBool(_type) ||
isMapping(_type) ||
isArray(_type) ||
isTuple(_type) ||
isNonRecursiveStruct(_type);
}
bool isSupportedTypeDeclaration(frontend::Type::Category _category)
bool isSupportedTypeDeclaration(frontend::Type const& _type)
{
return isSupportedType(_category) ||
isFunction(_category);
return isSupportedType(_type) ||
isFunction(_type);
}
pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
@ -235,9 +236,9 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
abstract = true;
var = make_shared<SymbolicIntVariable>(frontend::TypeProvider::uint256(), type, _uniqueName, _context);
}
else if (isBool(_type.category()))
else if (isBool(_type))
var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _context);
else if (isFunction(_type.category()))
else if (isFunction(_type))
{
auto const& fType = dynamic_cast<FunctionType const*>(type);
auto const& paramsIn = fType->parameterTypes();
@ -260,21 +261,21 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
else
var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context);
}
else if (isInteger(_type.category()))
else if (isInteger(_type))
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
else if (isFixedPoint(_type.category()))
else if (isFixedPoint(_type))
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
else if (isFixedBytes(_type.category()))
else if (isFixedBytes(_type))
{
auto fixedBytesType = dynamic_cast<frontend::FixedBytesType const*>(type);
solAssert(fixedBytesType, "");
var = make_shared<SymbolicFixedBytesVariable>(type, fixedBytesType->numBytes(), _uniqueName, _context);
}
else if (isAddress(_type.category()) || isContract(_type.category()))
else if (isAddress(_type) || isContract(_type))
var = make_shared<SymbolicAddressVariable>(_uniqueName, _context);
else if (isEnum(_type.category()))
else if (isEnum(_type))
var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _context);
else if (isRational(_type.category()))
else if (isRational(_type))
{
auto rational = dynamic_cast<frontend::RationalNumberType const*>(&_type);
solAssert(rational, "");
@ -283,113 +284,104 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
else
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
}
else if (isMapping(_type.category()) || isArray(_type.category()))
else if (isMapping(_type) || isArray(_type))
var = make_shared<SymbolicArrayVariable>(type, type, _uniqueName, _context);
else if (isTuple(_type.category()))
else if (isTuple(_type))
var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _context);
else if (isStringLiteral(_type.category()))
else if (isStringLiteral(_type))
{
auto stringType = TypeProvider::stringMemory();
var = make_shared<SymbolicArrayVariable>(stringType, type, _uniqueName, _context);
}
else if (isStruct(_type.category()))
else if (isNonRecursiveStruct(_type))
var = make_shared<SymbolicStructVariable>(type, _uniqueName, _context);
else
solAssert(false, "");
return make_pair(abstract, var);
}
bool isSupportedType(frontend::Type const& _type)
bool isInteger(frontend::Type const& _type)
{
return isSupportedType(_type.category());
return _type.category() == frontend::Type::Category::Integer;
}
bool isSupportedTypeDeclaration(frontend::Type const& _type)
bool isFixedPoint(frontend::Type const& _type)
{
return isSupportedTypeDeclaration(_type.category());
return _type.category() == frontend::Type::Category::FixedPoint;
}
bool isInteger(frontend::Type::Category _category)
bool isRational(frontend::Type const& _type)
{
return _category == frontend::Type::Category::Integer;
return _type.category() == frontend::Type::Category::RationalNumber;
}
bool isFixedPoint(frontend::Type::Category _category)
bool isFixedBytes(frontend::Type const& _type)
{
return _category == frontend::Type::Category::FixedPoint;
return _type.category() == frontend::Type::Category::FixedBytes;
}
bool isRational(frontend::Type::Category _category)
bool isAddress(frontend::Type const& _type)
{
return _category == frontend::Type::Category::RationalNumber;
return _type.category() == frontend::Type::Category::Address;
}
bool isFixedBytes(frontend::Type::Category _category)
bool isContract(frontend::Type const& _type)
{
return _category == frontend::Type::Category::FixedBytes;
return _type.category() == frontend::Type::Category::Contract;
}
bool isAddress(frontend::Type::Category _category)
bool isEnum(frontend::Type const& _type)
{
return _category == frontend::Type::Category::Address;
return _type.category() == frontend::Type::Category::Enum;
}
bool isContract(frontend::Type::Category _category)
bool isNumber(frontend::Type const& _type)
{
return _category == frontend::Type::Category::Contract;
return isInteger(_type) ||
isFixedPoint(_type) ||
isRational(_type) ||
isFixedBytes(_type) ||
isAddress(_type) ||
isContract(_type) ||
isEnum(_type);
}
bool isEnum(frontend::Type::Category _category)
bool isBool(frontend::Type const& _type)
{
return _category == frontend::Type::Category::Enum;
return _type.category() == frontend::Type::Category::Bool;
}
bool isNumber(frontend::Type::Category _category)
bool isFunction(frontend::Type const& _type)
{
return isInteger(_category) ||
isFixedPoint(_category) ||
isRational(_category) ||
isFixedBytes(_category) ||
isAddress(_category) ||
isContract(_category) ||
isEnum(_category);
return _type.category() == frontend::Type::Category::Function;
}
bool isBool(frontend::Type::Category _category)
bool isMapping(frontend::Type const& _type)
{
return _category == frontend::Type::Category::Bool;
return _type.category() == frontend::Type::Category::Mapping;
}
bool isFunction(frontend::Type::Category _category)
bool isArray(frontend::Type const& _type)
{
return _category == frontend::Type::Category::Function;
return _type.category() == frontend::Type::Category::Array ||
_type.category() == frontend::Type::Category::StringLiteral ||
_type.category() == frontend::Type::Category::ArraySlice;
}
bool isMapping(frontend::Type::Category _category)
bool isTuple(frontend::Type const& _type)
{
return _category == frontend::Type::Category::Mapping;
return _type.category() == frontend::Type::Category::Tuple;
}
bool isArray(frontend::Type::Category _category)
bool isStringLiteral(frontend::Type const& _type)
{
return _category == frontend::Type::Category::Array ||
_category == frontend::Type::Category::StringLiteral ||
_category == frontend::Type::Category::ArraySlice;
return _type.category() == frontend::Type::Category::StringLiteral;
}
bool isTuple(frontend::Type::Category _category)
bool isNonRecursiveStruct(frontend::Type const& _type)
{
return _category == frontend::Type::Category::Tuple;
}
bool isStringLiteral(frontend::Type::Category _category)
{
return _category == frontend::Type::Category::StringLiteral;
}
bool isStruct(frontend::Type::Category _category)
{
return _category == frontend::Type::Category::Struct;
auto structType = dynamic_cast<StructType const*>(&_type);
return structType && !structType->recursive();
}
smtutil::Expression minValue(frontend::IntegerType const& _type)
@ -416,13 +408,13 @@ void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const
smtutil::Expression zeroValue(frontend::TypePointer const& _type)
{
solAssert(_type, "");
if (isSupportedType(_type->category()))
if (isSupportedType(*_type))
{
if (isNumber(_type->category()))
if (isNumber(*_type))
return 0;
if (isBool(_type->category()))
if (isBool(*_type))
return smtutil::Expression(false);
if (isArray(_type->category()) || isMapping(_type->category()))
if (isArray(*_type) || isMapping(*_type))
{
auto tupleSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
solAssert(tupleSort, "");
@ -448,10 +440,9 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type)
);
}
if (isStruct(_type->category()))
if (isNonRecursiveStruct(*_type))
{
auto const* structType = dynamic_cast<StructType const*>(_type);
solAssert(structType, "");
auto structSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
return smtutil::Expression::tuple_constructor(
smtutil::Expression(make_shared<SortSort>(structSort), structSort->name),
@ -487,14 +478,14 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext&
void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
{
solAssert(_type, "");
if (isEnum(_type->category()))
if (isEnum(*_type))
{
auto enumType = dynamic_cast<frontend::EnumType const*>(_type);
solAssert(enumType, "");
_context.addAssertion(_expr >= 0);
_context.addAssertion(_expr < enumType->numberOfMembers());
}
else if (isInteger(_type->category()))
else if (isInteger(*_type))
{
auto intType = dynamic_cast<frontend::IntegerType const*>(_type);
solAssert(intType, "");

36
libsolidity/formal/SymbolicTypes.h
View File

@ -34,30 +34,30 @@ std::vector<smtutil::SortPointer> smtSort(std::vector<frontend::TypePointer> con
smtutil::SortPointer smtSortAbstractFunction(frontend::Type const& _type);
std::vector<smtutil::SortPointer> smtSortAbstractFunction(std::vector<frontend::TypePointer> const& _types);
/// Returns the SMT kind that models the Solidity type type category _category.
smtutil::Kind smtKind(frontend::Type::Category _category);
smtutil::Kind smtKind(frontend::Type const& _type);
/// Returns true if type is fully supported (declaration and operations).
bool isSupportedType(frontend::Type::Category _category);
bool isSupportedType(frontend::Type const& _type);
bool isSupportedType(frontend::Type const& _type);
/// Returns true if type is partially supported (declaration).
bool isSupportedTypeDeclaration(frontend::Type::Category _category);
bool isSupportedTypeDeclaration(frontend::Type const& _type);
bool isSupportedTypeDeclaration(frontend::Type const& _type);
bool isInteger(frontend::Type::Category _category);
bool isFixedPoint(frontend::Type::Category _category);
bool isRational(frontend::Type::Category _category);
bool isFixedBytes(frontend::Type::Category _category);
bool isAddress(frontend::Type::Category _category);
bool isContract(frontend::Type::Category _category);
bool isEnum(frontend::Type::Category _category);
bool isNumber(frontend::Type::Category _category);
bool isBool(frontend::Type::Category _category);
bool isFunction(frontend::Type::Category _category);
bool isMapping(frontend::Type::Category _category);
bool isArray(frontend::Type::Category _category);
bool isTuple(frontend::Type::Category _category);
bool isStringLiteral(frontend::Type::Category _category);
bool isStruct(frontend::Type::Category _category);
bool isInteger(frontend::Type const& _type);
bool isFixedPoint(frontend::Type const& _type);
bool isRational(frontend::Type const& _type);
bool isFixedBytes(frontend::Type const& _type);
bool isAddress(frontend::Type const& _type);
bool isContract(frontend::Type const& _type);
bool isEnum(frontend::Type const& _type);
bool isNumber(frontend::Type const& _type);
bool isBool(frontend::Type const& _type);
bool isFunction(frontend::Type const& _type);
bool isMapping(frontend::Type const& _type);
bool isArray(frontend::Type const& _type);
bool isTuple(frontend::Type const& _type);
bool isStringLiteral(frontend::Type const& _type);
bool isNonRecursiveStruct(frontend::Type const& _type);
/// Returns a new symbolic variable, according to _type.
/// Also returns whether the type is abstract or not,

10
libsolidity/formal/SymbolicVariables.cpp
View File

@ -121,7 +121,7 @@ SymbolicIntVariable::SymbolicIntVariable(
):
SymbolicVariable(_type, _originalType, move(_uniqueName), _context)
{
solAssert(isNumber(m_type->category()), "");
solAssert(isNumber(*m_type), "");
}
SymbolicAddressVariable::SymbolicAddressVariable(
@ -221,7 +221,7 @@ SymbolicEnumVariable::SymbolicEnumVariable(
):
SymbolicVariable(_type, _type, move(_uniqueName), _context)
{
solAssert(isEnum(m_type->category()), "");
solAssert(isEnum(*m_type), "");
}
SymbolicTupleVariable::SymbolicTupleVariable(
@ -231,7 +231,7 @@ SymbolicTupleVariable::SymbolicTupleVariable(
):
SymbolicVariable(_type, _type, move(_uniqueName), _context)
{
solAssert(isTuple(m_type->category()), "");
solAssert(isTuple(*m_type), "");
}
SymbolicTupleVariable::SymbolicTupleVariable(
@ -277,7 +277,7 @@ SymbolicArrayVariable::SymbolicArrayVariable(
m_context
)
{
solAssert(isArray(m_type->category()) || isMapping(m_type->category()), "");
solAssert(isArray(*m_type) || isMapping(*m_type), "");
}
SymbolicArrayVariable::SymbolicArrayVariable(
@ -330,7 +330,7 @@ SymbolicStructVariable::SymbolicStructVariable(
):
SymbolicVariable(_type, _type, move(_uniqueName), _context)
{
solAssert(isStruct(m_type->category()), "");
solAssert(isNonRecursiveStruct(*m_type), "");
auto const* structType = dynamic_cast<StructType const*>(_type);
solAssert(structType, "");
auto const& members = structType->structDefinition().members();