From 87ceb72b823e25e5cd0a38b5691e205b876aa59f Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 27 May 2020 19:24:48 +0200 Subject: [PATCH] [SMTChecker] Fix internal error in tuples of tuples. --- Changelog.md | 8 ++ libsolidity/formal/SMTEncoder.cpp | 114 ++++++++++-------- libsolidity/formal/SMTEncoder.h | 4 +- .../smtCheckerTests/types/tuple_tuple.sol | 6 + 4 files changed, 80 insertions(+), 52 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/types/tuple_tuple.sol diff --git a/Changelog.md b/Changelog.md index ad9126039..05bc99824 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,13 @@ ### 0.6.10 (unreleased) +Language Features: + + +Compiler Features: + + +Bugfixes: + * SMTChecker: Fix internal error when encoding tuples of tuples. ### 0.6.9 (2020-06-04) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index b06abbe6e..285c64a9b 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -385,44 +385,22 @@ void SMTEncoder::endVisit(Assignment const& _assignment) } else { - auto const& type = _assignment.annotation().type; - vector rightArguments; - if (auto const* tupleTypeRight = dynamic_cast(_assignment.rightHandSide().annotation().type)) - { - auto symbTupleLeft = dynamic_pointer_cast(m_context.expression(_assignment.leftHandSide())); - solAssert(symbTupleLeft, ""); - auto symbTupleRight = dynamic_pointer_cast(m_context.expression(_assignment.rightHandSide())); - solAssert(symbTupleRight, ""); - - auto const& leftComponents = symbTupleLeft->components(); - auto const& rightComponents = symbTupleRight->components(); - solAssert(leftComponents.size() == rightComponents.size(), ""); - - auto tupleTypeLeft = dynamic_cast(_assignment.leftHandSide().annotation().type); - solAssert(tupleTypeLeft, ""); - solAssert(tupleTypeLeft->components().size() == leftComponents.size(), ""); - auto const& typesLeft = tupleTypeLeft->components(); - - solAssert(tupleTypeRight->components().size() == rightComponents.size(), ""); - auto const& typesRight = tupleTypeRight->components(); - - for (unsigned i = 0; i < rightComponents.size(); ++i) - rightArguments.push_back(symbTupleRight->component(i, typesRight.at(i), typesLeft.at(i))); - } + if (dynamic_cast(_assignment.rightHandSide().annotation().type)) + tupleAssignment(_assignment.leftHandSide(), _assignment.rightHandSide()); else { + auto const& type = _assignment.annotation().type; auto rightHandSide = compoundOps.count(op) ? compoundAssignment(_assignment) : expr(_assignment.rightHandSide(), type); defineExpr(_assignment, rightHandSide); - rightArguments.push_back(expr(_assignment, type)); + assignment( + _assignment.leftHandSide(), + expr(_assignment, type), + type, + _assignment.location() + ); } - assignment( - _assignment.leftHandSide(), - rightArguments, - type, - _assignment.location() - ); } } @@ -1422,11 +1400,16 @@ smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Exp void SMTEncoder::assignment( Expression const& _left, - vector const& _right, + smtutil::Expression const& _right, TypePointer const& _type, langutil::SourceLocation const& _location ) { + solAssert( + _left.annotation().type->category() != Type::Category::Tuple, + "Tuple assignments should be handled by tupleAssignment." + ); + if (!smt::isSupportedType(_type->category())) { // Give it a new index anyway to keep the SSA scheme sound. @@ -1440,26 +1423,9 @@ void SMTEncoder::assignment( ); } else if (auto varDecl = identifierToVariable(_left)) - { - solAssert(_right.size() == 1, ""); - assignment(*varDecl, _right.front()); - } + assignment(*varDecl, _right); else if (dynamic_cast(&_left)) - { - solAssert(_right.size() == 1, ""); - arrayIndexAssignment(_left, _right.front()); - } - else if (auto tuple = dynamic_cast(&_left)) - { - auto const& components = tuple->components(); - if (!_right.empty()) - { - solAssert(_right.size() == components.size(), ""); - for (unsigned i = 0; i < _right.size(); ++i) - if (auto component = components.at(i)) - assignment(*component, {_right.at(i)}, component->annotation().type, component->location()); - } - } + arrayIndexAssignment(_left, _right); else m_errorReporter.warning( 8182_error, @@ -1468,6 +1434,52 @@ void SMTEncoder::assignment( ); } +void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _right) +{ + auto lTuple = dynamic_cast(&_left); + solAssert(lTuple, ""); + + auto const& lComponents = lTuple->components(); + + // If both sides are tuple expressions, we individually and potentially + // recursively assign each pair of components. + // This is because of potential type conversion. + if (auto rTuple = dynamic_cast(&_right)) + { + auto const& rComponents = rTuple->components(); + solAssert(lComponents.size() == rComponents.size(), ""); + for (unsigned i = 0; i < lComponents.size(); ++i) + { + if (!lComponents.at(i) || !rComponents.at(i)) + continue; + auto const& lExpr = *lComponents.at(i); + auto const& rExpr = *rComponents.at(i); + if (lExpr.annotation().type->category() == Type::Category::Tuple) + tupleAssignment(lExpr, rExpr); + else + { + auto type = lExpr.annotation().type; + assignment(lExpr, expr(rExpr, type), type, lExpr.location()); + } + } + } + else + { + auto rType = dynamic_cast(_right.annotation().type); + solAssert(rType, ""); + + auto const& rComponents = rType->components(); + solAssert(lComponents.size() == rComponents.size(), ""); + + auto symbRight = expr(_right); + solAssert(symbRight.sort->kind == smtutil::Kind::Tuple, ""); + + for (unsigned i = 0; i < lComponents.size(); ++i) + if (auto component = lComponents.at(i); component && rComponents.at(i)) + assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type, component->location()); + } +} + smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment) { static map const compoundToArithmetic{ diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 0e4c170fc..d90925571 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -157,10 +157,12 @@ protected: /// Will also be used for assignments of tuple components. void assignment( Expression const& _left, - std::vector const& _right, + smtutil::Expression const& _right, TypePointer const& _type, langutil::SourceLocation const& _location ); + /// Handle assignments between tuples. + void tupleAssignment(Expression const& _left, Expression const& _right); /// Computes the right hand side of a compound assignment. smtutil::Expression compoundAssignment(Assignment const& _assignment); diff --git a/test/libsolidity/smtCheckerTests/types/tuple_tuple.sol b/test/libsolidity/smtCheckerTests/types/tuple_tuple.sol new file mode 100644 index 000000000..c12e56a2d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/tuple_tuple.sol @@ -0,0 +1,6 @@ +pragma experimental SMTChecker; +contract C { + function f3() public pure { + ((, ), ) = ((7, 8), 9); + } +}