diff --git a/Changelog.md b/Changelog.md index 64115b520..aa6240f80 100644 --- a/Changelog.md +++ b/Changelog.md @@ -5,6 +5,7 @@ Language Features: Compiler Features: * SMTChecker: Support arithmetic compound assignment operators. + * SMTChecker: Support unary increment and decrement for array and mapping access. * Optimizer: Add rule for shifts by constants larger than 255 for Constantinople. * Optimizer: Add rule to simplify certain ANDs and SHL combinations * Yul: Adds break and continue keywords to for-loop syntax. diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 9de1ac43a..7d2a8c8bb 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -386,7 +386,7 @@ void SMTChecker::endVisit(Assignment const& _assignment) if (identifier) assignment(*decl, _assignment, _assignment.location()); else - arrayIndexAssignment(_assignment, expr(_assignment)); + arrayIndexAssignment(_assignment.leftHandSide(), expr(_assignment)); } else m_errorReporter.warning( @@ -485,21 +485,22 @@ void SMTChecker::endVisit(UnaryOperation const& _op) solAssert(isInteger(_op.annotation().type->category()), ""); solAssert(_op.subExpression().annotation().lValueRequested, ""); - if (Identifier const* identifier = dynamic_cast(&_op.subExpression())) + if (auto identifier = dynamic_cast(&_op.subExpression())) { - VariableDeclaration const& decl = dynamic_cast(*identifier->annotation().referencedDeclaration); - if (knownVariable(decl)) - { - auto innerValue = currentValue(decl); - auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1; - assignment(decl, newValue, _op.location()); - defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue); - } - else - m_errorReporter.warning( - _op.location(), - "Assertion checker does not yet implement such assignments." - ); + auto decl = dynamic_cast(identifier->annotation().referencedDeclaration); + solAssert(decl, ""); + solAssert(knownVariable(*decl), ""); + auto innerValue = currentValue(*decl); + auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1; + defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue); + assignment(*decl, newValue, _op.location()); + } + else if (dynamic_cast(&_op.subExpression())) + { + auto innerValue = expr(_op.subExpression()); + auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1; + defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue); + arrayIndexAssignment(_op.subExpression(), newValue); } else m_errorReporter.warning( @@ -911,9 +912,9 @@ void SMTChecker::arrayAssignment() m_arrayAssignmentHappened = true; } -void SMTChecker::arrayIndexAssignment(Assignment const& _assignment, smt::Expression const& _rightHandSide) +void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide) { - auto const& indexAccess = dynamic_cast(_assignment.leftHandSide()); + auto const& indexAccess = dynamic_cast(_expr); if (auto const& id = dynamic_cast(&indexAccess.baseExpression())) { auto const& varDecl = dynamic_cast(*id->annotation().referencedDeclaration); @@ -968,7 +969,7 @@ void SMTChecker::arrayIndexAssignment(Assignment const& _assignment, smt::Expres ); else m_errorReporter.warning( - _assignment.location(), + _expr.location(), "Assertion checker does not yet implement this expression." ); } diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 4fa1ac2ac..e47bd851c 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -127,7 +127,7 @@ private: /// while aliasing is not supported. void arrayAssignment(); /// Handles assignment to SMT array index. - void arrayIndexAssignment(Assignment const& _assignment, smt::Expression const& _rightHandSide); + void arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide); /// Division expression in the given type. Requires special treatment because /// of rounding for signed division. diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add.sol b/test/libsolidity/smtCheckerTests/operators/unary_add.sol new file mode 100644 index 000000000..9cb463696 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/unary_add.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + uint x = 2; + uint a = ++x; + assert(x == 3); + assert(a == 3); + uint b = x++; + assert(x == 4); + // Should fail. + assert(b < 3); + } +} +// ---- +// Warning: (194-207): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_array.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_array.sol new file mode 100644 index 000000000..c6370b34f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/unary_add_array.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[] array; + function f(uint x) public { + array[x] = 2; + uint a = ++array[x]; + assert(array[x] == 3); + assert(a == 3); + uint b = array[x]++; + assert(array[x] == 4); + // Should fail. + assert(b < 3); + } +} +// ---- +// Warning: (240-253): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_mapping.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_mapping.sol new file mode 100644 index 000000000..e75d5e113 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/unary_add_mapping.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + mapping (uint => uint) map; + function f(uint x) public { + map[x] = 2; + uint a = ++map[x]; + assert(map[x] == 3); + assert(a == 3); + uint b = map[x]++; + assert(map[x] == 4); + // Should fail. + assert(b < 3); + } +} +// ---- +// Warning: (244-257): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/unary_sub.sol b/test/libsolidity/smtCheckerTests/operators/unary_sub.sol new file mode 100644 index 000000000..3a2aaf408 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/unary_sub.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + uint x = 5; + uint a = --x; + assert(x == 4); + assert(a == 4); + uint b = x--; + assert(x == 3); + // Should fail. + assert(b > 4); + } +} +// ---- +// Warning: (194-207): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/unary_sub_array.sol b/test/libsolidity/smtCheckerTests/operators/unary_sub_array.sol new file mode 100644 index 000000000..220ae0a44 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/unary_sub_array.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[] array; + function f(uint x) public { + array[x] = 5; + uint a = --array[x]; + assert(array[x] == 4); + assert(a == 4); + uint b = array[x]--; + assert(array[x] == 3); + // Should fail. + assert(b > 4); + } +} +// ---- +// Warning: (240-253): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol b/test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol new file mode 100644 index 000000000..a1c3df860 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + mapping (uint => uint) map; + function f(uint x) public { + map[x] = 5; + uint a = --map[x]; + assert(map[x] == 4); + assert(a == 4); + uint b = map[x]--; + assert(map[x] == 3); + // Should fail. + assert(b > 4); + } +} +// ---- +// Warning: (244-257): Assertion violation happens here