diff --git a/Changelog.md b/Changelog.md index 467bca127..627dfc436 100644 --- a/Changelog.md +++ b/Changelog.md @@ -31,6 +31,7 @@ Compiler Features: Bugfixes: * NatSpec: Constructors and functions have consistent userdoc output. * Inheritance: Disallow public state variables overwriting ``pure`` functions. + * SMTChecker: Fix internal error when assigning to a 1-tuple. * State Mutability: Constant public state variables are considered ``pure`` functions. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 417a16921..d690b2b3c 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -425,17 +425,13 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple) auto const& symbTuple = dynamic_pointer_cast(m_context.expression(_tuple)); solAssert(symbTuple, ""); auto const& symbComponents = symbTuple->components(); - auto const* tupleComponents = &_tuple.components(); - while (tupleComponents->size() == 1) - { - auto innerTuple = dynamic_pointer_cast(tupleComponents->front()); - solAssert(innerTuple, ""); - tupleComponents = &innerTuple->components(); - } - solAssert(symbComponents.size() == tupleComponents->size(), ""); + auto const* tuple = dynamic_cast(innermostTuple(_tuple)); + solAssert(tuple, ""); + auto const& tupleComponents = tuple->components(); + solAssert(symbComponents.size() == tupleComponents.size(), ""); for (unsigned i = 0; i < symbComponents.size(); ++i) { - auto tComponent = tupleComponents->at(i); + auto tComponent = tupleComponents.at(i); if (tComponent) { if (auto varDecl = identifierToVariable(*tComponent)) @@ -454,8 +450,7 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple) /// Parenthesized expressions are also TupleExpression regardless their type. auto const& components = _tuple.components(); solAssert(components.size() == 1, ""); - if (smt::isSupportedType(components.front()->annotation().type->category())) - defineExpr(_tuple, expr(*components.front())); + defineExpr(_tuple, expr(*components.front())); } } @@ -729,11 +724,7 @@ void SMTEncoder::visitGasLeft(FunctionCall const& _funCall) void SMTEncoder::endVisit(Identifier const& _identifier) { - if (_identifier.annotation().willBeWrittenTo) - { - // Will be translated as part of the node that requested the lvalue. - } - else if (auto decl = identifierToVariable(_identifier)) + if (auto decl = identifierToVariable(_identifier)) defineExpr(_identifier, currentValue(*decl)); else if (_identifier.annotation().type->category() == Type::Category::Function) visitFunctionIdentifier(_identifier); @@ -1449,10 +1440,14 @@ void SMTEncoder::assignment( "Tuple assignments should be handled by tupleAssignment." ); + Expression const* left = &_left; + if (auto const* tuple = dynamic_cast(left)) + left = innermostTuple(*tuple); + if (!smt::isSupportedType(_type->category())) { // Give it a new index anyway to keep the SSA scheme sound. - if (auto varDecl = identifierToVariable(_left)) + if (auto varDecl = identifierToVariable(*left)) m_context.newValue(*varDecl); m_errorReporter.warning( @@ -1461,10 +1456,10 @@ void SMTEncoder::assignment( "Assertion checker does not yet implement type " + _type->toString() ); } - else if (auto varDecl = identifierToVariable(_left)) + else if (auto varDecl = identifierToVariable(*left)) assignment(*varDecl, _right); - else if (dynamic_cast(&_left)) - arrayIndexAssignment(_left, _right); + else if (dynamic_cast(left)) + arrayIndexAssignment(*left, _right); else m_errorReporter.warning( 8182_error, @@ -1901,6 +1896,20 @@ Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess) return base; } +Expression const* SMTEncoder::innermostTuple(TupleExpression const& _tuple) +{ + solAssert(!_tuple.isInlineArray(), ""); + TupleExpression const* tuple = &_tuple; + Expression const* expr = tuple; + while (tuple && !tuple->isInlineArray() && tuple->components().size() == 1) + { + expr = tuple->components().front().get(); + tuple = dynamic_cast(expr); + } + solAssert(expr, ""); + return expr; +} + set SMTEncoder::touchedVariables(ASTNode const& _node) { vector callStack; diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 92ef0601a..ec097a2c9 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -54,6 +54,9 @@ public: /// @returns the leftmost identifier in a multi-d IndexAccess. static Expression const* leftmostBase(IndexAccess const& _indexAccess); + /// @returns the innermost element in a chain of 1-tuples. + static Expression const* innermostTuple(TupleExpression const& _tuple); + /// @returns the FunctionDefinition of a FunctionCall /// if possible or nullptr. static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall); diff --git a/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol b/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol index d88e553b7..6fc041fb1 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol @@ -132,6 +132,7 @@ contract PropagateThroughReturnValue { // Warning 8182: (539-567): Assertion checker does not yet implement such assignments. // Warning 8115: (629-643): Assertion checker does not yet support the type of this variable. // Warning 8364: (646-668): Assertion checker does not yet implement type struct Reference.St storage ref +// Warning 8364: (700-703): Assertion checker does not yet implement type struct Reference.St storage pointer // Warning 8364: (706-728): Assertion checker does not yet implement type struct Reference.St storage ref // Warning 8364: (700-728): Assertion checker does not yet implement type struct Reference.St storage pointer // Warning 7650: (748-755): Assertion checker does not yet support this expression. diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol index ee6933d17..ff3d584e6 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol @@ -13,7 +13,8 @@ contract C assert(x > 0); } } +// ==== +// SMTSolvers: cvc4 // ---- -// Warning 1218: (296-309): Error trying to invoke SMT solver. // Warning 2661: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4661: (296-309): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/delete_struct.sol b/test/libsolidity/smtCheckerTests/operators/delete_struct.sol index 748fc59ad..e55601219 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_struct.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_struct.sol @@ -22,6 +22,7 @@ contract C // Warning 7650: (117-120): Assertion checker does not yet support this expression. // Warning 8364: (117-118): Assertion checker does not yet implement type struct C.S memory // Warning 8182: (117-124): Assertion checker does not yet implement such assignments. +// Warning 8364: (145-146): Assertion checker does not yet implement type struct C.S memory // Warning 7650: (165-168): Assertion checker does not yet support this expression. // Warning 8364: (165-166): Assertion checker does not yet implement type struct C.S memory // Warning 2683: (158-168): Assertion checker does not yet implement "delete" for this expression. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_1_chain_1.sol b/test/libsolidity/smtCheckerTests/types/tuple_1_chain_1.sol new file mode 100644 index 000000000..eded54d2e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/tuple_1_chain_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function i() public pure returns (uint d) { + if (0==0) + (d) = 13; + assert(d == 13); + } +} +// ---- +// Warning 6838: (96-100): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_1_chain_2.sol b/test/libsolidity/smtCheckerTests/types/tuple_1_chain_2.sol new file mode 100644 index 000000000..e35dff706 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/tuple_1_chain_2.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function i() public pure returns (uint d) { + if (0==0) + ((d)) = 13; + assert(d == 13); + } +} +// ---- +// Warning 6838: (96-100): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_1_chain_n.sol b/test/libsolidity/smtCheckerTests/types/tuple_1_chain_n.sol new file mode 100644 index 000000000..5166ed1b6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/tuple_1_chain_n.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function i() public pure returns (uint d) { + if (0==0) + (((((d))))) = 13; + assert(d == 13); + } +} +// ---- +// Warning 6838: (96-100): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol b/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol index 19b53cc3b..1489eb87f 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol @@ -19,5 +19,6 @@ contract C { // Warning 8364: (137-141): Assertion checker does not yet implement type struct C.S memory // Warning 4639: (137-141): Assertion checker does not yet implement this expression. // Warning 8115: (193-203): Assertion checker does not yet support the type of this variable. +// Warning 8364: (227-228): Assertion checker does not yet implement type struct C.S memory // Warning 4639: (137-141): Assertion checker does not yet implement this expression. // Warning 6191: (227-228): Assertion checker does not yet implement type struct C.S memory