diff --git a/Changelog.md b/Changelog.md index 04437cd91..b32b6e00b 100644 --- a/Changelog.md +++ b/Changelog.md @@ -44,10 +44,13 @@ Compiler Features: * Code Generator: Avoid memory allocation for default value if it is not used. * SMTChecker: Support named arguments in function calls. * SMTChecker: Support struct constructor. + * SMTChecker: Support getters. Bugfixes: * Code generator: Do not pad empty string literals with a single 32-byte zero field in the ABI coder v1. * SMTChecker: Fix internal compiler error when doing bitwise compound assignment with string literals. + * Yul Optimizer: Fix a bug in NameSimplifier where a new name created by NameSimplifier could also be created by NameDispenser. + * Yul Optimizer: Removed NameSimplifier from optimization steps available to users. ### 0.7.5 (2020-11-18) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index de80dd996..544db45da 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -506,6 +506,11 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall) auto const& funType = dynamic_cast(*_funCall.expression().annotation().type); if (shouldInlineFunctionCall(_funCall)) inlineFunctionCall(_funCall); + else if (isPublicGetter(_funCall.expression())) + { + // Do nothing here. + // The processing happens in SMT Encoder, but we need to prevent the resetting of the state variables. + } else if (funType.kind() == FunctionType::Kind::Internal) m_errorReporter.warning( 5729_error, diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index d977e16f3..036d9ebb8 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -318,18 +318,12 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl) assignment(*declarations.at(i), symbTuple->component(i, components.at(i), declarations.at(i)->type())); } } - else if (m_context.knownVariable(*_varDecl.declarations().front())) + else { + solAssert(m_context.knownVariable(*_varDecl.declarations().front()), ""); if (_varDecl.initialValue()) assignment(*_varDecl.declarations().front(), *_varDecl.initialValue()); } - else - m_errorReporter.warning( - 7186_error, - _varDecl.location(), - "Assertion checker does not yet implement such variable declarations." - ); - } bool SMTEncoder::visit(Assignment const& _assignment) @@ -492,11 +486,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op) indexOrMemberAssignment(*subExpr, newValue); } else - m_errorReporter.warning( - 1950_error, - _op.location(), - "Assertion checker does not yet implement such increments / decrements." - ); + solAssert(false, ""); break; } @@ -530,11 +520,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op) break; } default: - m_errorReporter.warning( - 3682_error, - _op.location(), - "Assertion checker does not yet implement this operator." - ); + solAssert(false, ""); } } @@ -571,11 +557,7 @@ void SMTEncoder::endVisit(BinaryOperation const& _op) else if (TokenTraits::isBitOp(_op.getOperator()) || TokenTraits::isShiftOp(_op.getOperator())) bitwiseOperation(_op); else - m_errorReporter.warning( - 3876_error, - _op.location(), - "Assertion checker does not yet implement this operator." - ); + solAssert(false, ""); } bool SMTEncoder::visit(Conditional const& _op) @@ -634,8 +616,11 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) case FunctionType::Kind::GasLeft: visitGasLeft(_funCall); break; - case FunctionType::Kind::Internal: case FunctionType::Kind::External: + if (isPublicGetter(_funCall.expression())) + visitPublicGetter(_funCall); + break; + case FunctionType::Kind::Internal: case FunctionType::Kind::DelegateCall: case FunctionType::Kind::BareCall: case FunctionType::Kind::BareCallCode: @@ -862,6 +847,98 @@ void SMTEncoder::endVisit(ElementaryTypeNameExpression const& _typeName) m_context.createExpression(_typeName, result.second); } +namespace // helpers for SMTEncoder::visitPublicGetter +{ + +bool isReturnedFromStructGetter(TypePointer _type) +{ + // So far it seems that only Mappings and ordinary Arrays are not returned. + auto category = _type->category(); + if (category == Type::Category::Mapping) + return false; + if (category == Type::Category::Array) + return dynamic_cast(*_type).isByteArray(); + // default + return true; +} + +vector structGetterReturnedMembers(StructType const& _structType) +{ + vector returnedMembers; + for (auto const& member: _structType.nativeMembers(nullptr)) + if (isReturnedFromStructGetter(member.type)) + returnedMembers.push_back(member.name); + return returnedMembers; +} + +} + +void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall) +{ + MemberAccess const& access = dynamic_cast(_funCall.expression()); + auto var = dynamic_cast(access.annotation().referencedDeclaration); + solAssert(var, ""); + solAssert(m_context.knownExpression(_funCall), ""); + auto paramExpectedTypes = FunctionType(*var).parameterTypes(); + auto actualArguments = _funCall.arguments(); + solAssert(actualArguments.size() == paramExpectedTypes.size(), ""); + vector symbArguments; + for (unsigned i = 0; i < paramExpectedTypes.size(); ++i) + symbArguments.push_back(expr(*actualArguments[i], paramExpectedTypes[i])); + + TypePointer type = var->type(); + if ( + type->isValueType() || + (type->category() == Type::Category::Array && dynamic_cast(*type).isByteArray()) + ) + { + solAssert(symbArguments.empty(), ""); + defineExpr(_funCall, currentValue(*var)); + return; + } + switch (type->category()) + { + case Type::Category::Array: + case Type::Category::Mapping: + { + // For nested arrays/mappings, each argument in the call is an index to the next layer. + // We mirror this with `select` after unpacking the SMT-LIB array expression. + smtutil::Expression exprVal = currentValue(*var); + for (auto const& arg: symbArguments) + { + exprVal = smtutil::Expression::select( + smtutil::Expression::tuple_get(exprVal, 0), + arg + ); + } + defineExpr(_funCall, exprVal); + break; + } + case Type::Category::Struct: + { + auto returnedMembers = structGetterReturnedMembers(dynamic_cast(*type)); + solAssert(!returnedMembers.empty(), ""); + auto structVar = dynamic_pointer_cast(m_context.variable(*var)); + solAssert(structVar, ""); + auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) { return structVar->member(memberName); }); + if (returnedValues.size() == 1) + defineExpr(_funCall, returnedValues.front()); + else + { + auto symbTuple = dynamic_pointer_cast(m_context.expression(_funCall)); + solAssert(symbTuple, ""); + symbTuple->increaseIndex(); // Increasing the index explicitly since we cannot use defineExpr in this case. + auto const& symbComponents = symbTuple->components(); + solAssert(symbComponents.size() == returnedValues.size(), ""); + for (unsigned i = 0; i < symbComponents.size(); ++i) + m_context.addAssertion(symbTuple->component(i) == returnedValues.at(i)); + } + break; + } + default: {} // Unsupported cases, do nothing and the getter will be abstracted. + } +} + void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall) { solAssert(*_funCall.annotation().kind == FunctionCallKind::TypeConversion, ""); @@ -1025,15 +1102,7 @@ void SMTEncoder::endVisit(Literal const& _literal) ); } else - { - m_errorReporter.warning( - 7885_error, - _literal.location(), - "Assertion checker does not yet support the type of this literal (" + - _literal.annotation().type->toString() + - ")." - ); - } + solAssert(false, ""); } void SMTEncoder::addArrayLiteralAssertions( @@ -1111,11 +1180,8 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) ); } else - m_errorReporter.warning( - 9551_error, - _memberAccess.location(), - "Assertion checker does not yet support this expression." - ); + solUnimplementedAssert(false, ""); + return false; } else if (smt::isNonRecursiveStruct(*exprType)) @@ -1505,40 +1571,32 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op) { auto type = _op.annotation().commonType; solAssert(type, ""); - if (type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint) + solAssert(type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint, ""); + switch (_op.getOperator()) { - switch (_op.getOperator()) - { - case Token::Add: - case Token::Sub: - case Token::Mul: - case Token::Div: - case Token::Mod: - { - auto values = arithmeticOperation( - _op.getOperator(), - expr(_op.leftExpression()), - expr(_op.rightExpression()), - _op.annotation().commonType, - _op - ); - defineExpr(_op, values.first); - break; - } - default: - m_errorReporter.warning( - 5188_error, - _op.location(), - "Assertion checker does not yet implement this operator." - ); - } - } - else - m_errorReporter.warning( - 9011_error, - _op.location(), - "Assertion checker does not yet implement this operator for type " + type->richIdentifier() + "." + case Token::Add: + case Token::Sub: + case Token::Mul: + case Token::Div: + case Token::Mod: + { + auto values = arithmeticOperation( + _op.getOperator(), + expr(_op.leftExpression()), + expr(_op.rightExpression()), + _op.annotation().commonType, + _op ); + defineExpr(_op, values.first); + break; + } + default: + m_errorReporter.warning( + 5188_error, + _op.location(), + "Assertion checker does not yet implement this operator." + ); + } } pair SMTEncoder::arithmeticOperation( @@ -1727,29 +1785,21 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op) { solAssert(_op.getOperator() == Token::And || _op.getOperator() == Token::Or, ""); solAssert(_op.annotation().commonType, ""); - if (_op.annotation().commonType->category() == Type::Category::Bool) + solAssert(_op.annotation().commonType->category() == Type::Category::Bool, ""); + // @TODO check that both of them are not constant + _op.leftExpression().accept(*this); + if (_op.getOperator() == Token::And) { - // @TODO check that both of them are not constant - _op.leftExpression().accept(*this); - if (_op.getOperator() == Token::And) - { - auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first; - mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); - defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression())); - } - else - { - auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first; - mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); - defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression())); - } + auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first; + mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); + defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression())); } else - m_errorReporter.warning( - 3263_error, - _op.location(), - "Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations" - ); + { + auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first; + mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); + defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression())); + } } void SMTEncoder::bitwiseOperation(BinaryOperation const& _op) @@ -2398,6 +2448,15 @@ MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const return nullptr; } +bool SMTEncoder::isPublicGetter(Expression const& _expr) { + if (!isTrustedExternalCall(&_expr)) + return false; + auto varDecl = dynamic_cast( + dynamic_cast(_expr).annotation().referencedDeclaration + ); + return varDecl != nullptr; +} + bool SMTEncoder::isTrustedExternalCall(Expression const* _expr) { auto memberAccess = dynamic_cast(_expr); if (!memberAccess) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 4c26cb4c8..56cc53938 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -153,6 +153,9 @@ protected: void visitTypeConversion(FunctionCall const& _funCall); void visitStructConstructorCall(FunctionCall const& _funCall); void visitFunctionIdentifier(Identifier const& _identifier); + void visitPublicGetter(FunctionCall const& _funCall); + + bool isPublicGetter(Expression const& _expr); /// Encodes a modifier or function body according to the modifier /// visit depth. diff --git a/libsolidity/interface/OptimiserSettings.h b/libsolidity/interface/OptimiserSettings.h index 1a2095198..4b1cd7c4e 100644 --- a/libsolidity/interface/OptimiserSettings.h +++ b/libsolidity/interface/OptimiserSettings.h @@ -32,7 +32,7 @@ namespace solidity::frontend struct OptimiserSettings { static char constexpr DefaultYulOptimiserSteps[] = - "NdhfoDgvulfnTUtnIf" // None of these can make stack problems worse + "dhfoDgvulfnTUtnIf" // None of these can make stack problems worse "[" "xarrscLM" // Turn into SSA and simplify "cCTUtTOntnfDIul" // Perform structural simplification @@ -47,7 +47,7 @@ struct OptimiserSettings "gvif" // Run full inliner "CTUcarrLsTOtfDncarrIulc" // SSA plus simplify "]" - "jmuljuljul VcTOcul jmulN"; // Make source short and pretty + "jmuljuljul VcTOcul jmul"; // Make source short and pretty /// No optimisations at all - not recommended. static OptimiserSettings none() diff --git a/libyul/AsmParser.cpp b/libyul/AsmParser.cpp index 00cdb4a22..c43066ee0 100644 --- a/libyul/AsmParser.cpp +++ b/libyul/AsmParser.cpp @@ -27,6 +27,7 @@ #include #include #include +#include #include @@ -138,18 +139,18 @@ Statement Parser::parseStatement() default: break; } + // Options left: - // Simple instruction (might turn into functional), - // literal, - // identifier (might turn into label or functional assignment) - ElementaryOperation elementary(parseElementaryOperation()); + // Expression/FunctionCall + // Assignment + variant elementary(parseLiteralOrIdentifier()); switch (currentToken()) { case Token::LParen: { Expression expr = parseCall(std::move(elementary)); - return ExpressionStatement{locationOf(expr), expr}; + return ExpressionStatement{locationOf(expr), move(expr)}; } case Token::Comma: case Token::AssemblyAssign: @@ -184,7 +185,7 @@ Statement Parser::parseStatement() expectToken(Token::Comma); - elementary = parseElementaryOperation(); + elementary = parseLiteralOrIdentifier(); } expectToken(Token::AssemblyAssign); @@ -192,28 +193,15 @@ Statement Parser::parseStatement() assignment.value = make_unique(parseExpression()); assignment.location.end = locationOf(*assignment.value).end; - return Statement{std::move(assignment)}; + return Statement{move(assignment)}; } default: fatalParserError(6913_error, "Call or assignment expected."); break; } - if (holds_alternative(elementary)) - { - Identifier& identifier = std::get(elementary); - return ExpressionStatement{identifier.location, { move(identifier) }}; - } - else if (holds_alternative(elementary)) - { - Expression expr = std::get(elementary); - return ExpressionStatement{locationOf(expr), expr}; - } - else - { - yulAssert(false, "Invalid elementary operation."); - return {}; - } + yulAssert(false, ""); + return {}; } Case Parser::parseCase() @@ -225,7 +213,7 @@ Case Parser::parseCase() else if (currentToken() == Token::Case) { advance(); - ElementaryOperation literal = parseElementaryOperation(); + variant literal = parseLiteralOrIdentifier(); if (!holds_alternative(literal)) fatalParserError(4805_error, "Literal expected."); _case.value = make_unique(std::get(std::move(literal))); @@ -264,38 +252,37 @@ Expression Parser::parseExpression() { RecursionGuard recursionGuard(*this); - ElementaryOperation operation = parseElementaryOperation(); - if (holds_alternative(operation) || currentToken() == Token::LParen) - return parseCall(std::move(operation)); - else if (holds_alternative(operation)) - return std::get(operation); - else - { - yulAssert(holds_alternative(operation), ""); - return std::get(operation); - } + variant operation = parseLiteralOrIdentifier(); + return visit(GenericVisitor{ + [&](Identifier& _identifier) -> Expression + { + if (currentToken() == Token::LParen) + return parseCall(std::move(operation)); + if (m_dialect.builtin(_identifier.name)) + fatalParserError( + 7104_error, + _identifier.location, + "Builtin function \"" + _identifier.name.str() + "\" must be called." + ); + return move(_identifier); + }, + [&](Literal& _literal) -> Expression + { + return move(_literal); + } + }, operation); } -Parser::ElementaryOperation Parser::parseElementaryOperation() +variant Parser::parseLiteralOrIdentifier() { RecursionGuard recursionGuard(*this); - ElementaryOperation ret; switch (currentToken()) { case Token::Identifier: { - YulString literal{currentLiteral()}; - if (m_dialect.builtin(literal)) - { - Identifier identifier{currentLocation(), literal}; - advance(); - expectToken(Token::LParen, false); - return FunctionCall{identifier.location, identifier, {}}; - } - else - ret = Identifier{currentLocation(), literal}; + Identifier identifier{currentLocation(), YulString{currentLiteral()}}; advance(); - break; + return identifier; } case Token::StringLiteral: case Token::Number: @@ -335,8 +322,7 @@ Parser::ElementaryOperation Parser::parseElementaryOperation() literal.type = expectAsmIdentifier(); } - ret = std::move(literal); - break; + return literal; } case Token::HexStringLiteral: fatalParserError(3772_error, "Hex literals are not valid in this context."); @@ -344,7 +330,7 @@ Parser::ElementaryOperation Parser::parseElementaryOperation() default: fatalParserError(1856_error, "Literal or identifier expected."); } - return ret; + return {}; } VariableDeclaration Parser::parseVariableDeclaration() @@ -418,21 +404,17 @@ FunctionDefinition Parser::parseFunctionDefinition() return funDef; } -Expression Parser::parseCall(Parser::ElementaryOperation&& _initialOp) +FunctionCall Parser::parseCall(variant&& _initialOp) { RecursionGuard recursionGuard(*this); - FunctionCall ret; - if (holds_alternative(_initialOp)) - { - ret.functionName = std::move(std::get(_initialOp)); - ret.location = ret.functionName.location; - } - else if (holds_alternative(_initialOp)) - ret = std::move(std::get(_initialOp)); - else + if (!holds_alternative(_initialOp)) fatalParserError(9980_error, "Function name expected."); + FunctionCall ret; + ret.functionName = std::move(std::get(_initialOp)); + ret.location = ret.functionName.location; + expectToken(Token::LParen); if (currentToken() != Token::RParen) { diff --git a/libyul/AsmParser.h b/libyul/AsmParser.h index 705711b52..d1294b111 100644 --- a/libyul/AsmParser.h +++ b/libyul/AsmParser.h @@ -61,8 +61,6 @@ public: std::unique_ptr parse(std::shared_ptr const& _scanner, bool _reuseScanner); protected: - using ElementaryOperation = std::variant; - langutil::SourceLocation currentLocation() const override { return m_locationOverride ? *m_locationOverride : ParserBase::currentLocation(); @@ -84,10 +82,10 @@ protected: Expression parseExpression(); /// Parses an elementary operation, i.e. a literal, identifier, instruction or /// builtin functian call (only the name). - ElementaryOperation parseElementaryOperation(); + std::variant parseLiteralOrIdentifier(); VariableDeclaration parseVariableDeclaration(); FunctionDefinition parseFunctionDefinition(); - Expression parseCall(ElementaryOperation&& _initialOp); + FunctionCall parseCall(std::variant&& _initialOp); TypedName parseTypedName(); YulString expectAsmIdentifier(); diff --git a/libyul/optimiser/NameDispenser.cpp b/libyul/optimiser/NameDispenser.cpp index 7c9fcc6bc..01d33919f 100644 --- a/libyul/optimiser/NameDispenser.cpp +++ b/libyul/optimiser/NameDispenser.cpp @@ -35,8 +35,9 @@ using namespace solidity::yul; using namespace solidity::util; NameDispenser::NameDispenser(Dialect const& _dialect, Block const& _ast, set _reservedNames): - NameDispenser(_dialect, NameCollector(_ast).names() + std::move(_reservedNames)) + NameDispenser(_dialect, NameCollector(_ast).names() + _reservedNames) { + m_reservedNames = move(_reservedNames); } NameDispenser::NameDispenser(Dialect const& _dialect, set _usedNames): @@ -61,3 +62,9 @@ bool NameDispenser::illegalName(YulString _name) { return isRestrictedIdentifier(m_dialect, _name) || m_usedNames.count(_name); } + +void NameDispenser::reset(Block const& _ast) +{ + m_usedNames = NameCollector(_ast).names() + m_reservedNames; + m_counter = 0; +} diff --git a/libyul/optimiser/NameDispenser.h b/libyul/optimiser/NameDispenser.h index e379708d0..6e655e416 100644 --- a/libyul/optimiser/NameDispenser.h +++ b/libyul/optimiser/NameDispenser.h @@ -51,11 +51,19 @@ public: /// return it. void markUsed(YulString _name) { m_usedNames.insert(_name); } -private: + std::set const& usedNames() { return m_usedNames; } + + /// Returns true if `_name` is either used or is a restricted identifier. bool illegalName(YulString _name); + /// Resets `m_usedNames` with *only* the names that are used in the AST. Also resets value of + /// `m_counter` to zero. + void reset(Block const& _ast); + +private: Dialect const& m_dialect; std::set m_usedNames; + std::set m_reservedNames; size_t m_counter = 0; }; diff --git a/libyul/optimiser/NameSimplifier.cpp b/libyul/optimiser/NameSimplifier.cpp index 741280edd..81379297d 100644 --- a/libyul/optimiser/NameSimplifier.cpp +++ b/libyul/optimiser/NameSimplifier.cpp @@ -19,6 +19,8 @@ #include #include #include +#include +#include #include #include @@ -28,19 +30,13 @@ using namespace solidity::yul; using namespace std; -NameSimplifier::NameSimplifier( - OptimiserStepContext& _context, - Block const& _ast -): - m_context(_context), - m_usedNames(_context.reservedIdentifiers) +NameSimplifier::NameSimplifier(OptimiserStepContext& _context, Block const& _ast): + m_context(_context) { - for (YulString name: m_usedNames) + for (YulString name: _context.reservedIdentifiers) m_translations[name] = name; - set allNames = NameCollector(_ast).names(); - m_usedNames += allNames; - for (YulString name: allNames) + for (YulString const& name: NameCollector(_ast).names()) findSimplification(name); } @@ -77,7 +73,7 @@ void NameSimplifier::operator()(FunctionCall& _funCall) ASTModifier::operator()(_funCall); } -void NameSimplifier::findSimplification(YulString _name) +void NameSimplifier::findSimplification(YulString const& _name) { if (m_translations.count(_name)) return; @@ -98,19 +94,19 @@ void NameSimplifier::findSimplification(YulString _name) {regex("index_access_t_array"), "index_access"}, {regex("[0-9]*_$"), ""} }; + for (auto const& [pattern, substitute]: replacements) { string candidate = regex_replace(name, pattern, substitute); - if ( - !isRestrictedIdentifier(m_context.dialect, YulString(candidate)) && - !m_usedNames.count(YulString(candidate)) - ) + if (!m_context.dispenser.illegalName(YulString(candidate))) name = candidate; } + if (name != _name.str()) { - m_usedNames.insert(YulString(name)); - m_translations[_name] = YulString(name); + YulString newName{name}; + m_context.dispenser.markUsed(newName); + m_translations[_name] = move(newName); } } diff --git a/libyul/optimiser/NameSimplifier.h b/libyul/optimiser/NameSimplifier.h index 0edbc595f..34cf69451 100644 --- a/libyul/optimiser/NameSimplifier.h +++ b/libyul/optimiser/NameSimplifier.h @@ -57,19 +57,15 @@ public: void operator()(FunctionDefinition& _funDef) override; private: - NameSimplifier( - OptimiserStepContext& _context, - Block const& _ast - ); + NameSimplifier(OptimiserStepContext& _context, Block const& _ast); /// Tries to rename a list of variables. void renameVariables(std::vector& _variables); - void findSimplification(YulString _name); + void findSimplification(YulString const& _name); void translate(YulString& _name); OptimiserStepContext& m_context; - std::set m_usedNames; std::map m_translations; }; diff --git a/libyul/optimiser/Suite.cpp b/libyul/optimiser/Suite.cpp index 8dcc45616..3f59e89e6 100644 --- a/libyul/optimiser/Suite.cpp +++ b/libyul/optimiser/Suite.cpp @@ -105,6 +105,7 @@ void OptimiserSuite::run( // ForLoopInitRewriter. Run them first to be able to run arbitrary sequences safely. suite.runSequence("hfgo", ast); + NameSimplifier::run(suite.m_context, ast); // Now the user-supplied part suite.runSequence(_optimisationSequence, ast); @@ -140,6 +141,9 @@ void OptimiserSuite::run( if (ast.statements.size() > 1 && std::get(ast.statements.front()).statements.empty()) ast.statements.erase(ast.statements.begin()); } + + suite.m_dispenser.reset(ast); + NameSimplifier::run(suite.m_context, ast); VarNameCleaner::run(suite.m_context, ast); *_object.analysisInfo = AsmAnalyzer::analyzeStrictAssertCorrect(_dialect, _object); @@ -191,7 +195,6 @@ map> const& OptimiserSuite::allSteps() LiteralRematerialiser, LoadResolver, LoopInvariantCodeMotion, - NameSimplifier, RedundantAssignEliminator, ReasoningBasedSimplifier, Rematerialiser, @@ -203,6 +206,7 @@ map> const& OptimiserSuite::allSteps() VarDeclInitializer >(); // Does not include VarNameCleaner because it destroys the property of unique names. + // Does not include NameSimplifier. return instance; } @@ -230,7 +234,6 @@ map const& OptimiserSuite::stepNameToAbbreviationMap() {LiteralRematerialiser::name, 'T'}, {LoadResolver::name, 'L'}, {LoopInvariantCodeMotion::name, 'M'}, - {NameSimplifier::name, 'N'}, {ReasoningBasedSimplifier::name, 'R'}, {RedundantAssignEliminator::name, 'r'}, {Rematerialiser::name, 'm'}, diff --git a/scripts/error_codes.py b/scripts/error_codes.py index 5ae990059..9b106d0c0 100755 --- a/scripts/error_codes.py +++ b/scripts/error_codes.py @@ -220,15 +220,12 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False): return False old_source_only_ids = { - "1123", "1220", "1584", "1823", "1950", - "1988", "2657", "2800", - "3263", "3356", "3682", "3876", + "1123", "1220", "1584", "1823", + "1988", "2657", "2800", "3356", "3893", "3996", "4010", "4802", - "5073", "5188", "5272", - "5622", "6272", "7128", "7186", - "7589", "7593", "7653", "7885", "8065", "8084", "8140", - "8312", "8592", "9011", - "9085", "9390", "9551", + "5073", "5272", "5622", "7128", + "7589", "7593", "7653", "8065", "8084", "8140", + "8312", "8592", "9085", "9390" } new_source_only_ids = source_only_ids - old_source_only_ids diff --git a/scripts/install_deps.sh b/scripts/install_deps.sh index f71434e44..0312db4b3 100755 --- a/scripts/install_deps.sh +++ b/scripts/install_deps.sh @@ -264,7 +264,7 @@ case $(uname -s) in # #------------------------------------------------------------------------------ - Ubuntu|LinuxMint) + Ubuntu|LinuxMint|Pop) #LinuxMint is a distro on top of Ubuntu. #Ubuntu install_z3="" diff --git a/test/libsolidity/smtCheckerTests/functions/getters/address.sol b/test/libsolidity/smtCheckerTests/functions/getters/address.sol new file mode 100644 index 000000000..88b435cb7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/address.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C { + address public x; + address payable public y; + + function f() public view { + address a = this.x(); + address b = this.y(); + assert(a == x); // should hold + assert(a == address(this)); // should fail + assert(b == y); // should hold + assert(y == address(this)); // should fail + } +} +// ---- +// Warning 6328: (204-230): CHC: Assertion violation happens here. +// Warning 6328: (282-308): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol new file mode 100644 index 000000000..c8c0c4675 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + uint[] public a; + + function f() public view { + uint y = this.a(2); + assert(y == a[2]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (153-167): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol new file mode 100644 index 000000000..4d6796dc8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] public a; + + function f() public view { + uint y = this.a(2,3); + assert(y == a[2][3]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (160-174): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/bytes.sol b/test/libsolidity/smtCheckerTests/functions/getters/bytes.sol new file mode 100644 index 000000000..b760cfe21 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/bytes.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + bytes public str2 = 'c'; + + function f() public view { + bytes memory a2 = this.str2(); + assert(keccak256(a2) == keccak256(str2)); // should hold + assert(keccak256(a2) == keccak256('a')); // should fail + } +} +// ---- +// Warning 6328: (195-234): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/contract.sol b/test/libsolidity/smtCheckerTests/functions/getters/contract.sol new file mode 100644 index 000000000..af5f4963e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/contract.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract D {} + +contract C { + D public d; + + function f() public view { + D e = this.d(); + assert(e == d); // should hold + assert(address(e) == address(this)); // should fail + } +} +// ---- +// Warning 6328: (156-191): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/double_access.sol b/test/libsolidity/smtCheckerTests/functions/getters/double_access.sol new file mode 100644 index 000000000..315853245 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/double_access.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint u; + } + + S public s; + + function f() public view { + uint u = this.s(); + uint v = this.s(); + assert(u == s.u); // should hold + assert(u == v); // should hold + assert(u == 1); // should fail + } +} +// ---- +// Warning 6328: (226-240): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/enum.sol b/test/libsolidity/smtCheckerTests/functions/getters/enum.sol new file mode 100644 index 000000000..28a7fd8d9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/enum.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + + +contract C { + enum ActionChoices { GoLeft, GoRight, GoStraight, SitStill } + ActionChoices public choice; + + function f() public view { + ActionChoices e = this.choice(); + assert(e == choice); // should hold + assert(e == ActionChoices.SitStill); // should fail + } +} +// ---- +// Warning 6328: (243-278): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/fixed_bytes.sol b/test/libsolidity/smtCheckerTests/functions/getters/fixed_bytes.sol new file mode 100644 index 000000000..bb7659267 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/fixed_bytes.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C { + byte public x; + bytes3 public y; + + function f() public view { + byte a = this.x(); + bytes3 b = this.y(); + assert(a == x); // should hold + assert(a == 'a'); // should fail + assert(b == y); // should hold + assert(y == "abc"); // should fail + } +} +// ---- +// Warning 6328: (188-204): CHC: Assertion violation happens here. +// Warning 6328: (256-274): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/function.sol b/test/libsolidity/smtCheckerTests/functions/getters/function.sol new file mode 100644 index 000000000..51b5eb2a6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/function.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C { + function () external returns (uint) public g; + + function f() public { + g = this.X; + function () external returns (uint) e = this.g(); + assert(e() == g()); // should hold, but fails because of the lack of support for tracking function pointers + assert(e() == 1); // should fail + } + + function X() public pure returns (uint) { + return 42; + } +} +// ---- +// Warning 6328: (185-203): CHC: Assertion violation happens here. +// Warning 6328: (295-311): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol new file mode 100644 index 000000000..ae7476c0f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => uint) public map; + + function f() public view { + uint y = this.map(2); + assert(y == map[2]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (175-189): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol similarity index 50% rename from test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol rename to test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol index aaa9605cc..905c143bc 100644 --- a/test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol @@ -5,8 +5,9 @@ contract C { function f() public view { uint y = this.map(2, 3); - assert(y == map[2][3]); // This fails as false positive because of lack of support for external getters. + assert(y == map[2][3]); // should hold + assert(y == 1); // should fail } } // ---- -// Warning 6328: (158-180): CHC: Assertion violation happens here. +// Warning 6328: (199-213): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/mapping_with_cast.sol b/test/libsolidity/smtCheckerTests/functions/getters/mapping_with_cast.sol new file mode 100644 index 000000000..f515e1d36 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/mapping_with_cast.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + mapping (bytes16 => uint) public m; + + function f() public view { + uint y = this.m("foo"); + assert(y == m["foo"]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (180-194): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol new file mode 100644 index 000000000..1a39d5d6b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => uint[]) public m; + + constructor() { + m[0].push(); + m[0].push(); + m[0][1] = 42; + } + + function f() public view { + uint y = this.m(0,1); + assert(y == m[0][1]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (243-257): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol new file mode 100644 index 000000000..5d7d75b9f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => uint[])[] public m; + + constructor() { + m.push(); + m[0][1].push(); + m[0][1].push(); + m[0][1].push(); + m[0][1][2] = 42; + } + + function f() public view { + uint y = this.m(0,1,2); + assert(y == m[0][1][2]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (289-303): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol new file mode 100644 index 000000000..2717dac17 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => uint[][]) public m; + + constructor() { + m[0].push(); + m[0].push(); + m[0][1].push(); + m[0][1].push(); + m[0][1].push(); + m[0][1][2] = 42; + } + + function f() public view { + uint y = this.m(0,1,2); + assert(y == m[0][1][2]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (307-321): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol new file mode 100644 index 000000000..422d060f6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => uint[][][]) public m; + + constructor() { + m[0].push(); + m[0].push(); + m[0][1].push(); + m[0][1].push(); + m[0][1].push(); + m[0][1][2].push(); + m[0][1][2].push(); + m[0][1][2].push(); + m[0][1][2].push(); + m[0][1][2][3] = 42; + } + + function f() public view { + uint y = this.m(0,1,2,3); + assert(y == m[0][1][2][3]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (401-415): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol new file mode 100644 index 000000000..2dc53b7e5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => mapping (uint => uint[])) public m; + + constructor() { + m[0][1].push(); + m[0][1].push(); + m[0][1].push(); + m[0][1][2] = 42; + } + + function f() public view { + uint y = this.m(0,1,2); + assert(y == m[0][1][2]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (293-307): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol new file mode 100644 index 000000000..442efc47e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => mapping (uint => uint[][])) public m; + + constructor() { + m[0][1].push(); + m[0][1].push(); + m[0][1].push(); + m[0][1][2].push(); + m[0][1][2].push(); + m[0][1][2].push(); + m[0][1][2].push(); + m[0][1][2][3] = 42; + } + + function f() public view { + uint y = this.m(0,1,2,3); + assert(y == m[0][1][2][3]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (387-401): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol new file mode 100644 index 000000000..df70036df --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => mapping (uint => mapping (uint => uint[]))) public m; + + constructor() { + m[0][1][2].push(); + m[0][1][2].push(); + m[0][1][2].push(); + m[0][1][2].push(); + m[0][1][2][3] = 42; + } + + function f() public view { + uint y = this.m(0,1,2,3); + assert(y == m[0][1][2][3]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (349-363): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol new file mode 100644 index 000000000..a2a18d815 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => uint)[] public m; + + constructor() { + m.push(); + m[0][1] = 42; + } + + function f() public view { + uint y = this.m(0,1); + assert(y == m[0][1]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (225-239): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol new file mode 100644 index 000000000..da0932c21 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => uint)[][] public m; + + constructor() { + m.push(); + m[0].push(); + m[0].push(); + m[0][1][2] = 42; + } + + function f() public view { + uint y = this.m(0,1,2); + assert(y == m[0][1][2]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (265-279): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol new file mode 100644 index 000000000..6e43e3902 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => mapping (uint => uint))[] public m; + + constructor() { + m.push(); + m[0][1][2] = 42; + } + + function f() public view { + uint y = this.m(0,1,2); + assert(y == m[0][1][2]); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (251-265): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol b/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol new file mode 100644 index 000000000..f887e572d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + + +contract C { + + uint[2] public x = [42,1]; + + function f() public view { + assert(this.x(0) == x[0]); // should hold + assert(this.x(1) == x[1]); // should hold + assert(this.x(0) == 0); // should fail + } +} +// ---- +// Warning 6328: (195-217): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/string.sol b/test/libsolidity/smtCheckerTests/functions/getters/string.sol new file mode 100644 index 000000000..6ed52b5a6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/string.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + string public str1 = 'b'; + + function f() public view { + string memory a1 = this.str1(); + assert(keccak256(bytes(a1)) == keccak256(bytes(str1))); // should hold + assert(keccak256(bytes(a1)) == keccak256('a')); // should fail + } +} +// ---- +// Warning 6328: (211-257): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol new file mode 100644 index 000000000..d03617a0a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol @@ -0,0 +1,29 @@ +pragma experimental SMTChecker; +pragma abicoder v2; + +contract C { + struct T { + uint t; + } + struct S { + uint x; + T t; + bool b; + uint[] a; + } + + S public s; + + function f() public view { + uint y; + bool c; + T memory t; + (y,t,c) = this.s(); + assert(y == s.x); // this should hold + assert(c == s.b); // this should hold + assert(t.t == s.t.t); // this should hold + assert(c == true); // this should fail + } +} +// ---- +// Warning 6328: (370-387): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol new file mode 100644 index 000000000..39344c661 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; +//pragma abicoder v2; + +contract C { + struct S { + uint[2] a; + uint u; + } + + S public s; + + function f() public view { + uint u = this.s(); + assert(u == s.u); // should hold + assert(u == 1); // should fail + } +} +// ---- +// Warning 6328: (207-221): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol new file mode 100644 index 000000000..d2f78d333 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + string s; + bytes b; + } + + S public m; + + constructor() { + m.s = "foo"; + m.b = "bar"; + } + + function f() public view { + (string memory s, bytes memory b) = this.m(); + assert(keccak256(bytes(s)) == keccak256(bytes(m.s))); // should hold + assert(b[0] == m.b[0]); // should hold + assert(b[0] == "t"); // should fail + } +} +// ---- +// Warning 6328: (340-359): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol new file mode 100644 index 000000000..709cdf51e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract D { +} + +contract C { + struct S { + D d; + function () external returns (uint) f; + } + + S public s; + + function test() public view { + (D d, function () external returns (uint) f) = this.s(); + assert(d == s.d); // should hold + assert(address(d) == address(this)); // should fail + } +} +// ---- +// Warning 2072: (179-216): Unused local variable. +// Warning 6328: (267-302): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol new file mode 100644 index 000000000..91e685d28 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol @@ -0,0 +1,32 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + bool b; + } + + S public s; + + constructor() { + s.x = 1; + s.b = false; + } + + function f() public { + uint x; + bool b; + (x,b) = this.s(); + assert(x == s.x); // this should hold + assert(b == s.b); // this should hold + assert(b == true); // this should fail + s.x = 42; + (uint y, bool c) = this.s(); + assert(c == b); // this should hold + assert(y == x); // this should fail + + } +} +// ---- +// Warning 6328: (288-305): CHC: Assertion violation happens here. +// Warning 6328: (410-424): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/uint.sol b/test/libsolidity/smtCheckerTests/functions/getters/uint.sol new file mode 100644 index 000000000..8e0b14fe8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/uint.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + uint public x; + + function f() public view { + uint y = this.x(); + assert(y == x); // should hold + assert(y == 1); // should fail + } +} +// ---- +// Warning 6328: (147-161): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol b/test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol deleted file mode 100644 index 60c1a57d5..000000000 --- a/test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol +++ /dev/null @@ -1,12 +0,0 @@ -pragma experimental SMTChecker; - -contract C { - uint public x; - - function f() public view { - uint y = this.x(); - assert(y == x); // This fails as false positive because of lack of support for external getters. - } -} -// ---- -// Warning 6328: (114-128): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol b/test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol deleted file mode 100644 index 5091da3f3..000000000 --- a/test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol +++ /dev/null @@ -1,12 +0,0 @@ -pragma experimental SMTChecker; - -contract C { - mapping (uint => uint) public map; - - function f() public view { - uint y = this.map(2); - assert(y == map[2]); // This fails as false positive because of lack of support for external getters. - } -} -// ---- -// Warning 6328: (137-156): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol index 8682973cd..0e6e1642c 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol @@ -1,7 +1,12 @@ pragma experimental SMTChecker; + contract C { - function f() public pure returns (byte) { - return (~byte(0xFF)); - } + function f() public pure { + // ffff0000 in bytes4 + bytes4 x = ~bytes4(hex"ffff"); + assert(x == 0xffff0000); // should fail + assert(x == 0x0000ffff); // should hold + } } // ---- +// Warning 6328: (175-198): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/exp.sol b/test/libsolidity/smtCheckerTests/operators/exp.sol new file mode 100644 index 000000000..3070f9649 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/exp.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract D { + function f(uint x) public pure { + assert(x**2 == 4); + } +} +// ---- +// Warning 5188: (88-92): Assertion checker does not yet implement this operator. +// Warning 6328: (81-98): CHC: Assertion violation happens here. +// Warning 5188: (88-92): Assertion checker does not yet implement this operator. diff --git a/test/libsolidity/smtCheckerTests/special/ether_units.sol b/test/libsolidity/smtCheckerTests/special/ether_units.sol new file mode 100644 index 000000000..ccb0cee20 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/ether_units.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +contract D { + function f() public pure { + assert(1000000000000000000 wei == 1 ether); + assert(100000000000000000 wei == 1 ether); + assert(1000000000 wei == 1 gwei); + assert(100000000 wei == 1 gwei); + assert(1000000000 gwei == 1 ether); + assert(100000000 gwei == 1 ether); + } +} +// ---- +// Warning 6328: (121-162): CHC: Assertion violation happens here. +// Warning 6328: (202-233): CHC: Assertion violation happens here. +// Warning 6328: (275-308): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/special/time_units.sol b/test/libsolidity/smtCheckerTests/special/time_units.sol new file mode 100644 index 000000000..59bb004b9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/time_units.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; +contract D { + function f() public pure { + assert(1 == 1 seconds); + assert(2 == 1 seconds); + assert(2 minutes == 120 seconds); + assert(3 minutes == 120 seconds); + assert(2 hours == 120 minutes); + assert(3 hours == 120 minutes); + assert(2 days == 48 hours); + assert(4 days == 48 hours); + assert(2 weeks == 14 days); + assert(25 weeks == 14 days); + } +} +// ---- +// Warning 6328: (101-123): CHC: Assertion violation happens here. +// Warning 6328: (163-195): CHC: Assertion violation happens here. +// Warning 6328: (233-263): CHC: Assertion violation happens here. +// Warning 6328: (297-323): CHC: Assertion violation happens here. +// Warning 6328: (357-384): CHC: Assertion violation happens here. diff --git a/test/libsolidity/syntaxTests/inlineAssembly/assignment_from_opcode_like.sol b/test/libsolidity/syntaxTests/inlineAssembly/assignment_from_opcode_like.sol index 3296252ea..cb675ab29 100644 --- a/test/libsolidity/syntaxTests/inlineAssembly/assignment_from_opcode_like.sol +++ b/test/libsolidity/syntaxTests/inlineAssembly/assignment_from_opcode_like.sol @@ -7,4 +7,4 @@ contract C { } } // ---- -// ParserError 2314: (118-119): Expected '(' but got '}' +// ParserError 7104: (104-109): Builtin function "mload" must be called. diff --git a/test/libsolidity/syntaxTests/inlineAssembly/assignment_to_opcode_like.sol b/test/libsolidity/syntaxTests/inlineAssembly/assignment_to_opcode_like.sol index 7a783b9fe..51028e50c 100644 --- a/test/libsolidity/syntaxTests/inlineAssembly/assignment_to_opcode_like.sol +++ b/test/libsolidity/syntaxTests/inlineAssembly/assignment_to_opcode_like.sol @@ -7,4 +7,4 @@ contract C { } } // ---- -// ParserError 2314: (101-103): Expected '(' but got ':=' +// ParserError 6272: (101-103): Cannot assign to builtin function "mload". diff --git a/test/libsolidity/syntaxTests/inlineAssembly/invalid/bare_instructions_disallowed.sol b/test/libsolidity/syntaxTests/inlineAssembly/invalid/bare_instructions_disallowed.sol index a55586af9..87884efee 100644 --- a/test/libsolidity/syntaxTests/inlineAssembly/invalid/bare_instructions_disallowed.sol +++ b/test/libsolidity/syntaxTests/inlineAssembly/invalid/bare_instructions_disallowed.sol @@ -7,4 +7,4 @@ contract C { } } // ---- -// ParserError 2314: (95-98): Expected '(' but got identifier +// ParserError 6913: (95-98): Call or assignment expected. diff --git a/test/libsolidity/syntaxTests/inlineAssembly/invalid/unbalanced_negative_stack.sol b/test/libsolidity/syntaxTests/inlineAssembly/invalid/unbalanced_negative_stack.sol index 3f92beec2..80dd3a587 100644 --- a/test/libsolidity/syntaxTests/inlineAssembly/invalid/unbalanced_negative_stack.sol +++ b/test/libsolidity/syntaxTests/inlineAssembly/invalid/unbalanced_negative_stack.sol @@ -6,4 +6,4 @@ contract test { } } // ---- -// ParserError 2314: (85-86): Expected '(' but got '}' +// ParserError 6913: (85-86): Call or assignment expected. diff --git a/test/libyul/YulInterpreterTest.cpp b/test/libyul/YulInterpreterTest.cpp index 1f1fbccf0..0af79dd9e 100644 --- a/test/libyul/YulInterpreterTest.cpp +++ b/test/libyul/YulInterpreterTest.cpp @@ -87,8 +87,8 @@ bool YulInterpreterTest::parse(ostream& _stream, string const& _linePrefix, bool string YulInterpreterTest::interpret() { InterpreterState state; - state.maxTraceSize = 10000; - state.maxSteps = 10000; + state.maxTraceSize = 32; + state.maxSteps = 512; try { Interpreter::run(state, EVMDialect::strictAssemblyForEVMObjects(langutil::EVMVersion{}), *m_ast); diff --git a/test/libyul/yulInterpreterTests/bounded_recursion.yul b/test/libyul/yulInterpreterTests/bounded_recursion.yul new file mode 100644 index 000000000..ce22638ca --- /dev/null +++ b/test/libyul/yulInterpreterTests/bounded_recursion.yul @@ -0,0 +1,16 @@ +{ + function f(x) -> y { + if lt(x, 150) { + y := f(add(x, 1)) + } + if eq(x, 150) { + y := x + } + } + mstore(0, f(0)) +} +// ---- +// Trace: +// Memory dump: +// 0: 0000000000000000000000000000000000000000000000000000000000000096 +// Storage dump: diff --git a/test/libyul/yulInterpreterTests/infinite_recursion.yul b/test/libyul/yulInterpreterTests/infinite_recursion.yul new file mode 100644 index 000000000..0e3109ab5 --- /dev/null +++ b/test/libyul/yulInterpreterTests/infinite_recursion.yul @@ -0,0 +1,11 @@ +{ + function f() { + f() + } + f() +} +// ---- +// Trace: +// Interpreter execution step limit reached. +// Memory dump: +// Storage dump: diff --git a/test/libyul/yulInterpreterTests/infinite_recursion_tracelimit.yul b/test/libyul/yulInterpreterTests/infinite_recursion_tracelimit.yul new file mode 100644 index 000000000..45d3cc781 --- /dev/null +++ b/test/libyul/yulInterpreterTests/infinite_recursion_tracelimit.yul @@ -0,0 +1,44 @@ +{ + function f() { + log0(0x0, 0x0) + f() + } + f() +} +// ---- +// Trace: +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// LOG0(0, 0) +// Trace size limit reached. +// Memory dump: +// Storage dump: diff --git a/test/libyul/yulSyntaxTests/builtin_identifier_3.yul b/test/libyul/yulSyntaxTests/builtin_identifier_3.yul index 283d64b49..c7969b8ef 100644 --- a/test/libyul/yulSyntaxTests/builtin_identifier_3.yul +++ b/test/libyul/yulSyntaxTests/builtin_identifier_3.yul @@ -2,4 +2,4 @@ function f(x) { f(add) } } // ---- -// ParserError 2314: (24-25): Expected '(' but got ')' +// ParserError 7104: (21-24): Builtin function "add" must be called. diff --git a/test/libyul/yulSyntaxTests/builtin_identifier_6.yul b/test/libyul/yulSyntaxTests/builtin_identifier_6.yul index 8f3395d79..e261354fc 100644 --- a/test/libyul/yulSyntaxTests/builtin_identifier_6.yul +++ b/test/libyul/yulSyntaxTests/builtin_identifier_6.yul @@ -1,6 +1,5 @@ { - // Test for the unreachable 6272_error add := 1 } // ---- -// ParserError 2314: (47-49): Expected '(' but got ':=' +// ParserError 6272: (7-9): Cannot assign to builtin function "add". diff --git a/test/libyul/yulSyntaxTests/builtin_identifier_7.yul b/test/libyul/yulSyntaxTests/builtin_identifier_7.yul index 391b190d9..c34da0363 100644 --- a/test/libyul/yulSyntaxTests/builtin_identifier_7.yul +++ b/test/libyul/yulSyntaxTests/builtin_identifier_7.yul @@ -1,7 +1,6 @@ { - // Test for the unreachable 6272_error function f() -> a, b {} add, mul := f() } // ---- -// ParserError 2314: (71-72): Expected '(' but got ',' +// ParserError 6272: (31-32): Cannot assign to builtin function "add". diff --git a/test/libyul/yulSyntaxTests/for_expr_invalid_5.yul b/test/libyul/yulSyntaxTests/for_expr_invalid_5.yul index acf9be847..5d739e81e 100644 --- a/test/libyul/yulSyntaxTests/for_expr_invalid_5.yul +++ b/test/libyul/yulSyntaxTests/for_expr_invalid_5.yul @@ -2,4 +2,4 @@ for {} mload {} {} } // ---- -// ParserError 2314: (16-17): Expected '(' but got '{' +// ParserError 7104: (10-15): Builtin function "mload" must be called. diff --git a/test/libyul/yulSyntaxTests/functional_partial.yul b/test/libyul/yulSyntaxTests/functional_partial.yul index f66225658..ea28283d4 100644 --- a/test/libyul/yulSyntaxTests/functional_partial.yul +++ b/test/libyul/yulSyntaxTests/functional_partial.yul @@ -2,4 +2,4 @@ let x := byte } // ---- -// ParserError 2314: (20-21): Expected '(' but got '}' +// ParserError 7104: (15-19): Builtin function "byte" must be called. diff --git a/test/libyul/yulSyntaxTests/if_statement_invalid_1.yul b/test/libyul/yulSyntaxTests/if_statement_invalid_1.yul index 5f73fcf2a..0a4f33844 100644 --- a/test/libyul/yulSyntaxTests/if_statement_invalid_1.yul +++ b/test/libyul/yulSyntaxTests/if_statement_invalid_1.yul @@ -2,4 +2,4 @@ if mload {} } // ---- -// ParserError 2314: (15-16): Expected '(' but got '{' +// ParserError 7104: (9-14): Builtin function "mload" must be called. diff --git a/test/libyul/yulSyntaxTests/if_statement_invalid_4.yul b/test/libyul/yulSyntaxTests/if_statement_invalid_4.yul index ed9deeda6..b84004a8d 100644 --- a/test/libyul/yulSyntaxTests/if_statement_invalid_4.yul +++ b/test/libyul/yulSyntaxTests/if_statement_invalid_4.yul @@ -2,4 +2,4 @@ if calldatasize {} } // ---- -// ParserError 2314: (22-23): Expected '(' but got '{' +// ParserError 7104: (9-21): Builtin function "calldatasize" must be called. diff --git a/test/libyul/yulSyntaxTests/switch_invalid_expr_2.yul b/test/libyul/yulSyntaxTests/switch_invalid_expr_2.yul index 842fa02f3..9378297ca 100644 --- a/test/libyul/yulSyntaxTests/switch_invalid_expr_2.yul +++ b/test/libyul/yulSyntaxTests/switch_invalid_expr_2.yul @@ -4,4 +4,4 @@ default {} } // ---- -// ParserError 2314: (23-27): Expected '(' but got reserved keyword 'case' +// ParserError 7104: (13-18): Builtin function "mload" must be called. diff --git a/test/tools/ossfuzz/yulProto_diff_ossfuzz.cpp b/test/tools/ossfuzz/yulProto_diff_ossfuzz.cpp index 1ebacb417..25a2ca95b 100644 --- a/test/tools/ossfuzz/yulProto_diff_ossfuzz.cpp +++ b/test/tools/ossfuzz/yulProto_diff_ossfuzz.cpp @@ -104,12 +104,18 @@ DEFINE_PROTO_FUZZER(Program const& _input) return; stack.optimize(); - yulFuzzerUtil::interpret( + termReason = yulFuzzerUtil::interpret( os2, stack.parserResult()->code, EVMDialect::strictAssemblyForEVMObjects(version) ); + if ( + termReason == yulFuzzerUtil::TerminationReason::StepLimitReached || + termReason == yulFuzzerUtil::TerminationReason::TraceLimitReached + ) + return; + bool isTraceEq = (os1.str() == os2.str()); yulAssert(isTraceEq, "Interpreted traces for optimized and unoptimized code differ."); return; diff --git a/test/yulPhaser/Chromosome.cpp b/test/yulPhaser/Chromosome.cpp index 1f66398be..b42086202 100644 --- a/test/yulPhaser/Chromosome.cpp +++ b/test/yulPhaser/Chromosome.cpp @@ -138,7 +138,7 @@ BOOST_AUTO_TEST_CASE(output_operator_should_create_concise_and_unambiguous_strin BOOST_TEST(chromosome.length() == allSteps.size()); BOOST_TEST(chromosome.optimisationSteps() == allSteps); - BOOST_TEST(toString(chromosome) == "flcCUnDvejsxIOoighTLMNRrmVatpud"); + BOOST_TEST(toString(chromosome) == "flcCUnDvejsxIOoighTLMRrmVatpud"); } BOOST_AUTO_TEST_CASE(optimisationSteps_should_translate_chromosomes_genes_to_optimisation_step_names)