diff --git a/Changelog.md b/Changelog.md index 3cab5b5b8..865e3320a 100644 --- a/Changelog.md +++ b/Changelog.md @@ -8,6 +8,7 @@ Compiler Features: * SMTChecker: Support events and low-level logs. * SMTChecker: Support ``revert()``. * SMTChecker: Support shifts. + * SMTChecker: Support compound and, or, and xor operators. * SMTChecker: Support structs. * SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``. * SMTChecker: Support ``address`` type conversion with literals, e.g. ``address(0)``. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 9113f526f..a446e47bf 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -352,31 +352,10 @@ void SMTEncoder::endVisit(Assignment const& _assignment) { createExpr(_assignment); - static set const compoundOps{ - Token::AssignAdd, - Token::AssignSub, - Token::AssignMul, - Token::AssignDiv, - Token::AssignMod - }; Token op = _assignment.assignmentOperator(); - if (op != Token::Assign && !compoundOps.count(op)) - { - Expression const* identifier = &_assignment.leftHandSide(); - if (auto const* indexAccess = dynamic_cast(identifier)) - identifier = leftmostBase(*indexAccess); - // Give it a new index anyway to keep the SSA scheme sound. - solAssert(identifier, ""); - if (auto varDecl = identifierToVariable(*identifier)) - m_context.newValue(*varDecl); + solAssert(TokenTraits::isAssignmentOp(op), ""); - m_errorReporter.warning( - 9149_error, - _assignment.location(), - "Assertion checker does not yet implement this assignment operator." - ); - } - else if (!smt::isSupportedType(*_assignment.annotation().type)) + if (!smt::isSupportedType(*_assignment.annotation().type)) { // Give it a new index anyway to keep the SSA scheme sound. @@ -394,9 +373,9 @@ void SMTEncoder::endVisit(Assignment const& _assignment) else { auto const& type = _assignment.annotation().type; - auto rightHandSide = compoundOps.count(op) ? - compoundAssignment(_assignment) : - expr(_assignment.rightHandSide(), type); + auto rightHandSide = op == Token::Assign ? + expr(_assignment.rightHandSide(), type) : + compoundAssignment(_assignment); defineExpr(_assignment, rightHandSide); assignment( _assignment.leftHandSide(), @@ -1388,6 +1367,59 @@ pair SMTEncoder::arithmeticOperation( return {value, valueUnbounded}; } +smtutil::Expression SMTEncoder::bitwiseOperation( + Token _op, + smtutil::Expression const& _left, + smtutil::Expression const& _right, + TypePointer const& _commonType +) +{ + static set validOperators{ + Token::BitAnd, + Token::BitOr, + Token::BitXor, + Token::SHL, + Token::SHR, + Token::SAR + }; + solAssert(validOperators.count(_op), ""); + solAssert(_commonType, ""); + + auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_commonType); + + auto bvLeft = smtutil::Expression::int2bv(_left, bvSize); + auto bvRight = smtutil::Expression::int2bv(_right, bvSize); + + optional result; + switch (_op) + { + case Token::BitAnd: + result = bvLeft & bvRight; + break; + case Token::BitOr: + result = bvLeft | bvRight; + break; + case Token::BitXor: + result = bvLeft ^ bvRight; + break; + case Token::SHL: + result = bvLeft << bvRight; + break; + case Token::SHR: + solAssert(false, ""); + case Token::SAR: + result = isSigned ? + smtutil::Expression::ashr(bvLeft, bvRight) : + bvLeft >> bvRight; + break; + default: + solAssert(false, ""); + } + + solAssert(result.has_value(), ""); + return smtutil::Expression::bv2int(*result, isSigned); +} + void SMTEncoder::compareOperation(BinaryOperation const& _op) { auto const& commonType = _op.annotation().commonType; @@ -1464,39 +1496,12 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op) auto commonType = _op.annotation().commonType; solAssert(commonType, ""); - auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(commonType); - - auto bvLeft = smtutil::Expression::int2bv(expr(_op.leftExpression(), commonType), bvSize); - auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression(), commonType), bvSize); - - optional result; - switch (op) - { - case Token::BitAnd: - result = bvLeft & bvRight; - break; - case Token::BitOr: - result = bvLeft | bvRight; - break; - case Token::BitXor: - result = bvLeft ^ bvRight; - break; - case Token::SHL: - result = bvLeft << bvRight; - break; - case Token::SHR: - solAssert(false, ""); - case Token::SAR: - result = isSigned ? - smtutil::Expression::ashr(bvLeft, bvRight) : - bvLeft >> bvRight; - break; - default: - solAssert(false, ""); - } - - solAssert(result, ""); - defineExpr(_op, smtutil::Expression::bv2int(*result, isSigned)); + defineExpr(_op, bitwiseOperation( + _op.getOperator(), + expr(_op.leftExpression(), commonType), + expr(_op.rightExpression(), commonType), + commonType + )); } void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op) @@ -1604,9 +1609,27 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment {Token::AssignDiv, Token::Div}, {Token::AssignMod, Token::Mod} }; + static map const compoundToBitwise{ + {Token::AssignBitAnd, Token::BitAnd}, + {Token::AssignBitOr, Token::BitOr}, + {Token::AssignBitXor, Token::BitXor}, + {Token::AssignShl, Token::SHL}, + {Token::AssignShr, Token::SHR}, + {Token::AssignSar, Token::SAR} + }; Token op = _assignment.assignmentOperator(); - solAssert(compoundToArithmetic.count(op), ""); + solAssert(compoundToArithmetic.count(op) || compoundToBitwise.count(op), ""); + auto decl = identifierToVariable(_assignment.leftHandSide()); + + if (compoundToBitwise.count(op)) + return bitwiseOperation( + compoundToBitwise.at(op), + decl ? currentValue(*decl) : expr(_assignment.leftHandSide()), + expr(_assignment.rightHandSide()), + _assignment.annotation().type + ); + auto values = arithmeticOperation( compoundToArithmetic.at(op), decl ? currentValue(*decl) : expr(_assignment.leftHandSide()), diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 9bb7b81ce..454f8777c 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -119,6 +119,14 @@ protected: TypePointer const& _commonType, Expression const& _expression ); + + smtutil::Expression bitwiseOperation( + Token _op, + smtutil::Expression const& _left, + smtutil::Expression const& _right, + TypePointer const& _commonType + ); + void compareOperation(BinaryOperation const& _op); void booleanOperation(BinaryOperation const& _op); void bitwiseOperation(BinaryOperation const& _op); diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol deleted file mode 100644 index d80dbb90a..000000000 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol +++ /dev/null @@ -1,13 +0,0 @@ -pragma experimental SMTChecker; - -contract C { - function f(bool b) public pure { - uint v = 1; - if (b) - v &= 1; - assert(v == 1); - } -} -// ---- -// Warning 6328: (116-130): Assertion violation happens here. -// Warning 9149: (106-112): Assertion checker does not yet implement this assignment operator. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol new file mode 100644 index 000000000..1f733c429 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract C { + function f() public pure returns (byte) { + byte a = 0xff; + byte b = 0xf0; + a &= b; + assert(a == b); + + a &= ~b; + assert(a != 0); // fails + } +} +// ---- +// Warning 6328: (203-217): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol new file mode 100644 index 000000000..309fa64c0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + int8 x = 1; + int8 y = 0; + x &= y; + assert(x != 0); // fails + x = -1; y = 3; + y &= x; + assert(y == 3); + y = -1; + y &= x; + assert(y == -1); + y = 127; + x &= y; + assert(x == 127); + } +} +// ---- +// Warning 6328: (114-128): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol new file mode 100644 index 000000000..33da9936f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol @@ -0,0 +1,33 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + uint v = 1; + v &= 1; + assert(v == 1); + + v = 7; + v &= 3; + assert(v != 3); // fails, as 7 & 3 = 3 + + uint c = 0; + c &= v; + assert(c == 0); + + uint8 x = 0xff; + uint16 y = 0xffff; + y &= x; + assert(y == 0xff); + assert(y == 0xffff); // fails + + y = 0xffff; + x = 0xff; + y &= y | x; + assert(y == 0xffff); + assert(y == 0xff); // fails + } +} +// ---- +// Warning 6328: (177-191): Assertion violation happens here. +// Warning 6328: (380-399): Assertion violation happens here. +// Warning 6328: (506-523): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol deleted file mode 100644 index 24e61cf58..000000000 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol +++ /dev/null @@ -1,10 +0,0 @@ -pragma experimental SMTChecker; -contract C { - int[1] c; - function f(bool b) public { - if (b) - c[0] |= 1; - } -} -// ---- -// Warning 9149: (97-106): Assertion checker does not yet implement this assignment operator. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol deleted file mode 100644 index 4569afa88..000000000 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol +++ /dev/null @@ -1,10 +0,0 @@ -pragma experimental SMTChecker; -contract C { - int[1][20] c; - function f(bool b) public { - if (b) - c[10][0] |= 1; - } -} -// ---- -// Warning 9149: (101-114): Assertion checker does not yet implement this assignment operator. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol deleted file mode 100644 index fdcfa3e14..000000000 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol +++ /dev/null @@ -1,13 +0,0 @@ -pragma experimental SMTChecker; -contract C { - struct S { - uint x; - } - S s; - function f(bool b) public { - if (b) - s.x |= 1; - } -} -// ---- -// Warning 9149: (117-125): Assertion checker does not yet implement this assignment operator. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol deleted file mode 100644 index 00e32d0d1..000000000 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol +++ /dev/null @@ -1,13 +0,0 @@ -pragma experimental SMTChecker; -contract C { - struct S { - uint[] x; - } - S s; - function f(bool b) public { - if (b) - s.x[2] |= 1; - } -} -// ---- -// Warning 9149: (119-130): Assertion checker does not yet implement this assignment operator. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol new file mode 100644 index 000000000..8be3855b0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract C { + function f() public pure returns (byte) { + byte a = 0xff; + byte b = 0xf0; + b |= a; + assert(a == b); + + a |= ~b; + assert(a == 0); // fails + } +} +// ---- +// Warning 6328: (203-217): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol new file mode 100644 index 000000000..b6fd90ce7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + int8 x = 1; + int8 y = 0; + x |= y; + assert(x == 0); // fails + x = -1; y = 3; + x |= y; + assert(x == -1); + x = 4; + y |= x; + assert(y == 7); + y = 127; + x |= y; + assert(x == 127); + } +} +// ---- +// Warning 6328: (114-128): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol new file mode 100644 index 000000000..e25ae354d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +contract C { + int[1][20] c; + function f(bool b) public { + require(c[10][0] == 0); + if (b) + c[10][0] |= 1; + assert(c[10][0] == 0 || c[10][0] == 1); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol new file mode 100644 index 000000000..ddc0c4376 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol @@ -0,0 +1,29 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + uint v = 7; + v |= 3; + assert(v != 7); // fails, as 7 | 3 = 7 + + uint c = 0; + c |= v; + assert(c == 7); + + uint16 x = 0xff; + uint16 y = 0xffff; + y |= x; + assert(y == 0xff); // fails + assert(y == 0xffff); + + y = 0xf1ff; + x = 0xff00; + x |= y & x; + assert(y == 0xffff); // fails + assert(x == 0xff00); + } +} +// ---- +// Warning 6328: (121-135): Assertion violation happens here. +// Warning 6328: (298-315): Assertion violation happens here. +// Warning 6328: (424-443): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol new file mode 100644 index 000000000..790d30a76 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +contract C { + uint[1] c; + function f(bool b) public { + require(c[0] == 0); + if (b) + c[0] |= 1; + assert(c[0] <= 1); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol new file mode 100644 index 000000000..04d907cf4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract C { + struct S { + uint[] x; + } + S s; + function f(bool b) public { + if (b) + s.x[2] |= 1; + assert(s.x[2] != 1); + } +} +// ---- +// Warning 6328: (173-192): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol new file mode 100644 index 000000000..8132ae773 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol deleted file mode 100644 index 22d3a5836..000000000 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol +++ /dev/null @@ -1,13 +0,0 @@ -pragma experimental SMTChecker; - -contract C { - function f(bool b) public pure { - uint v = 0; - if (b) - v ^= 1; - assert(v == 1); - } -} -// ---- -// Warning 6328: (116-130): Assertion violation happens here. -// Warning 9149: (106-112): Assertion checker does not yet implement this assignment operator. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol new file mode 100644 index 000000000..fe60d8621 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract C { + function f() public pure returns (byte) { + byte a = 0xff; + byte b = 0xf0; + a ^= ~b; + assert(a == b); + + a ^= ~b; + assert(a != 0xff); // fails + } +} +// ---- +// Warning 6328: (204-221): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol new file mode 100644 index 000000000..fc7dc19f7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + int8 x = 1; + int8 y = 0; + x ^= y; + assert(x != 1); // fails + x = -1; y = 1; + x ^= y; + assert(x == -2); + x = 4; + y ^= x; + assert(y == 5); + } +} +// ---- +// Warning 6328: (114-128): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol new file mode 100644 index 000000000..684e9fc01 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol @@ -0,0 +1,29 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + uint v = 7; + v ^= 3; + assert(v != 4); // fails, as 7 ^ 3 = 4 + + uint c = 0; + c ^= v; + assert(c == 4); + + uint16 x = 0xff; + uint16 y = 0xffff; + y ^= x; + assert(y == 0xff); // fails + assert(y == 0xff00); + + y = 0xf1; + x = 0xff00; + y ^= x | y; + assert(y == 0xffff); // fails + assert(x == 0xff00); + } +} +// ---- +// Warning 6328: (121-135): Assertion violation happens here. +// Warning 6328: (298-315): Assertion violation happens here. +// Warning 6328: (422-441): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol index 9b7a264d6..8ccc8a800 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol @@ -9,5 +9,3 @@ contract C { } } // ---- -// Warning 6328: (123-136): Assertion violation happens here. -// Warning 9149: (112-119): Assertion checker does not yet implement this assignment operator. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol index 3887f3e5e..e54344d2d 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol @@ -10,4 +10,3 @@ contract C { } // ---- // Warning 6328: (117-130): Assertion violation happens here. -// Warning 9149: (106-113): Assertion checker does not yet implement this assignment operator. diff --git a/test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_left.sol b/test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_left.sol new file mode 100644 index 000000000..442bd3a77 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_left.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C { + function f(uint256 a, uint256 b) internal pure returns (uint256) { + a <<= b; + return a; + } + function t() public pure { + assert(f(0x4266, 0x0) == 0x4266); + assert(f(0x4266, 0x8) == 0x426600); + assert(f(0x4266, 0xf0) == 0x4266000000000000000000000000000000000000000000000000000000000000); + assert(f(0x4266, 0x4266) == 0); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_right.sol b/test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_right.sol new file mode 100644 index 000000000..75dc0fe0d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_right.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C { + function f(uint256 a, uint256 b) internal pure returns (uint256) { + a >>= b; + return a; + } + function t() public pure { + assert(f(0x4266, 0) == 0x4266); + assert(f(0x4266, 0x8) == 0x42); + assert(f(0x4266, 0x11) == 0); + assert(f(57896044618658097711785492504343953926634992332820282019728792003956564819968, 5) == 1809251394333065553493296640760748560207343510400633813116524750123642650624); + } +} +// ----