From 11a7763f492411d1fb77841caa48fd918dca64d4 Mon Sep 17 00:00:00 2001 From: Djordje Mijovic Date: Sun, 23 Aug 2020 21:21:45 +0200 Subject: [PATCH] [SMTChecker] Support bitwise or, xor and not. --- Changelog.md | 1 + libsmtutil/CVC4Interface.cpp | 6 +++ libsmtutil/SolverInterface.h | 18 +++++++++ libsmtutil/Z3Interface.cpp | 6 +++ libsolidity/formal/SMTEncoder.cpp | 39 +++++++++---------- libsolidity/formal/SMTEncoder.h | 1 + libsolidity/formal/SymbolicTypes.cpp | 12 ++++++ libsolidity/formal/SymbolicTypes.h | 2 + .../operators/bitwise_combo.sol | 12 ++++++ .../operators/bitwise_not_fixed_bytes.sol | 8 ++++ .../operators/bitwise_not_int.sol | 21 ++++++++++ .../operators/bitwise_not_uint.sol | 15 +++++++ .../operators/bitwise_or_fixed_bytes.sol | 9 +++++ .../operators/bitwise_or_int.sol | 21 ++++++++++ .../operators/bitwise_or_uint.sol | 17 ++++++++ .../operators/bitwise_xor_fixed_bytes.sol | 1 - .../operators/bitwise_xor_int.sol | 19 +++++++++ .../operators/bitwise_xor_uint.sol | 17 ++++++++ 18 files changed, 203 insertions(+), 22 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_combo.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_not_int.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_not_uint.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_or_int.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_or_uint.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_xor_int.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_xor_uint.sol diff --git a/Changelog.md b/Changelog.md index 64c2de607..8a43bce46 100644 --- a/Changelog.md +++ b/Changelog.md @@ -10,6 +10,7 @@ Compiler Features: * Yul: Report error when using non-string literals for ``datasize()``, ``dataoffset()``, ``linkersymbol()``, ``loadimmutable()``, ``setimmutable()``. * Yul Optimizer: LoopInvariantCodeMotion can move reading operations outside for-loops as long as the affected area is not modified inside the loop. * SMTChecker: Support conditional operator. + * SMTChecker: Support bitwise or, xor and not operators. Bugfixes: * Optimizer: Keep side-effects of ``x`` in ``byte(a, shr(b, x))`` even if the constants ``a`` and ``b`` would make the expression zero unconditionally. This optimizer rule is very hard if not impossible to trigger in a way that it can result in invalid code, though. diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp index 2a795d827..40526306f 100644 --- a/libsmtutil/CVC4Interface.cpp +++ b/libsmtutil/CVC4Interface.cpp @@ -188,8 +188,14 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]); else if (n == "mod") return m_context.mkExpr(CVC4::kind::INTS_MODULUS, arguments[0], arguments[1]); + else if (n == "bvnot") + return m_context.mkExpr(CVC4::kind::BITVECTOR_NOT, arguments[0]); else if (n == "bvand") return m_context.mkExpr(CVC4::kind::BITVECTOR_AND, arguments[0], arguments[1]); + else if (n == "bvor") + return m_context.mkExpr(CVC4::kind::BITVECTOR_OR, arguments[0], arguments[1]); + else if (n == "bvxor") + return m_context.mkExpr(CVC4::kind::BITVECTOR_XOR, arguments[0], arguments[1]); else if (n == "int2bv") { size_t size = std::stoul(_expr.arguments[1].name); diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index d4c4d7fef..c45ebd77b 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -95,7 +95,10 @@ public: {"*", 2}, {"/", 2}, {"mod", 2}, + {"bvnot", 1}, {"bvand", 2}, + {"bvor", 2}, + {"bvxor", 2}, {"int2bv", 2}, {"bv2int", 1}, {"select", 2}, @@ -286,11 +289,26 @@ public: auto intSort = _a.sort; return Expression("mod", {std::move(_a), std::move(_b)}, intSort); } + friend Expression operator~(Expression _a) + { + auto bvSort = _a.sort; + return Expression("bvnot", {std::move(_a)}, bvSort); + } friend Expression operator&(Expression _a, Expression _b) { auto bvSort = _a.sort; return Expression("bvand", {std::move(_a), std::move(_b)}, bvSort); } + friend Expression operator^(Expression _a, Expression _b) + { + auto bvSort = _a.sort; + return Expression("bvxor", {std::move(_a), std::move(_b)}, bvSort); + } + friend Expression operator|(Expression _a, Expression _b) + { + auto bvSort = _a.sort; + return Expression("bvor", {std::move(_a), std::move(_b)}, bvSort); + } Expression operator()(std::vector _arguments) const { smtAssert( diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp index 501446553..909a5cde2 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -181,8 +181,14 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) return arguments[0] / arguments[1]; else if (n == "mod") return z3::mod(arguments[0], arguments[1]); + else if (n == "bvnot") + return ~arguments[0]; else if (n == "bvand") return arguments[0] & arguments[1]; + else if (n == "bvor") + return arguments[0] | arguments[1]; + else if (n == "bvxor") + return arguments[0] ^ arguments[1]; else if (n == "int2bv") { size_t size = std::stoul(_expr.arguments[1].name); diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 53f390902..7088f485d 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -456,6 +456,8 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple) void SMTEncoder::endVisit(UnaryOperation const& _op) { + if (TokenTraits::isBitOp(_op.getOperator())) + return bitwiseNotOperation(_op); if (_op.annotation().type->category() == Type::Category::RationalNumber) return; @@ -1406,20 +1408,7 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op) auto commonType = _op.annotation().commonType; solAssert(commonType, ""); - unsigned bvSize = 256; - bool isSigned = false; - if (auto const* intType = dynamic_cast(commonType)) - { - bvSize = intType->numBits(); - isSigned = intType->isSigned(); - } - else if (auto const* fixedType = dynamic_cast(commonType)) - { - bvSize = fixedType->numBits(); - isSigned = fixedType->isSigned(); - } - else if (auto const* fixedBytesType = dynamic_cast(commonType)) - bvSize = fixedBytesType->numBytes() * 8; + 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); @@ -1427,18 +1416,26 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op) optional result; if (_op.getOperator() == Token::BitAnd) result = bvLeft & bvRight; - // TODO implement the other operators - else - m_errorReporter.warning( - 1093_error, - _op.location(), - "Assertion checker does not yet implement this bitwise operator." - ); + else if (_op.getOperator() == Token::BitOr) + result = bvLeft | bvRight; + else if (_op.getOperator() == Token::BitXor) + result = bvLeft ^ bvRight; + solAssert(result, ""); if (result) defineExpr(_op, smtutil::Expression::bv2int(*result, isSigned)); } +void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op) +{ + solAssert(_op.getOperator() == Token::BitNot, ""); + + auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_op.annotation().type); + + auto bvOperand = smtutil::Expression::int2bv(expr(_op.subExpression(), _op.annotation().type), bvSize); + defineExpr(_op, smtutil::Expression::bv2int(~bvOperand, isSigned)); +} + smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type) { // Signed division in SMTLIB2 rounds differently for negative division. diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 4eb5ce965..122c8544f 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -115,6 +115,7 @@ protected: void compareOperation(BinaryOperation const& _op); void booleanOperation(BinaryOperation const& _op); void bitwiseOperation(BinaryOperation const& _op); + void bitwiseNotOperation(UnaryOperation const& _op); void initContract(ContractDefinition const& _contract); void initFunction(FunctionDefinition const& _function); diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 568368054..965130bb7 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -432,6 +432,18 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type) return 0; } +pair typeBvSizeAndSignedness(frontend::TypePointer const& _type) +{ + if (auto const* intType = dynamic_cast(_type)) + return {intType->numBits(), intType->isSigned()}; + else if (auto const* fixedType = dynamic_cast(_type)) + return {fixedType->numBits(), fixedType->isSigned()}; + else if (auto const* fixedBytesType = dynamic_cast(_type)) + return {fixedBytesType->numBytes() * 8, false}; + else + solAssert(false, ""); +} + void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context) { setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _context); diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 401c9f0b6..8e08783d8 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -67,6 +67,8 @@ smtutil::Expression minValue(frontend::IntegerType const& _type); smtutil::Expression maxValue(frontend::IntegerType const& _type); smtutil::Expression zeroValue(frontend::TypePointer const& _type); +std::pair typeBvSizeAndSignedness(frontend::TypePointer const& type); + void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context); void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context); void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context); diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_combo.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_combo.sol new file mode 100644 index 000000000..dc1d8f206 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_combo.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + uint8 x = 0xff; + uint8 y = ~x; + assert(x & y == 0); + assert(x | y == 0xff); + assert(x ^ y == 0xff); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol new file mode 100644 index 000000000..1431fb248 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f() public pure returns (byte) { + return (~byte(0xFF)); + } +} +// ---- +// Warning 5084: (102-112): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_not_int.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_not_int.sol new file mode 100644 index 000000000..d879f8ee7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_not_int.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + int16 x = 1; + assert(~x == 0); + x = 0xff; + assert(~x == 0); + x = 0x0f; + assert(~x == 0xf0); + x = -1; + assert(~x != 0); + x = -2; + assert(~x == 1); + } +} +// ---- +// Warning 6328: (91-106): Assertion violation happens here +// Warning 6328: (122-137): Assertion violation happens here +// Warning 6328: (153-171): Assertion violation happens here +// Warning 6328: (185-200): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_not_uint.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_not_uint.sol new file mode 100644 index 000000000..8b733de18 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_not_uint.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + uint8 x = 0xff; + assert(~x == 0x00); + uint16 y = 0xff00; + assert(~y == 0xff); + assert(~y == 0xffff); + assert(~y == 0x0000); + } +} +// ---- +// Warning 6328: (159-179): Assertion violation happens here +// Warning 6328: (183-203): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol new file mode 100644 index 000000000..4dad0286e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + function f() public pure returns (byte) { + return (byte(0x0F) | (byte(0xF0))); + } +} +// ---- +// Warning 5084: (101-111): Type conversion is not yet fully supported and might yield false positives. +// Warning 5084: (115-125): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_or_int.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_or_int.sol new file mode 100644 index 000000000..140c255c6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_or_int.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + int16 x = 1; + int16 y = 0; + assert(x | y == 1); + x = 0; y = 0; + assert(x | y != 0); + y = 240; + x = 15; + int16 z = x | y; + assert(z == 255); + x = -1; y = 200; + assert(x | y == x); + assert(x | z != -1); + } +} +// ---- +// Warning 6328: (144-162): Assertion violation happens here +// Warning 6328: (267-286): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_or_uint.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_or_uint.sol new file mode 100644 index 000000000..f93c59a69 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_or_uint.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + uint8 x = 1; + uint16 y = 0; + assert(x | y != 0); + x = 0xff; + y = 0xff00; + assert(x | y == 0xff); + assert(x | y == 0xffff); + assert(x | y == 0x0000); + } +} +// ---- +// Warning 6328: (155-176): Assertion violation happens here +// Warning 6328: (207-230): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol index 3852563be..69cea474f 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol @@ -6,4 +6,3 @@ contract Simp { } } // ---- -// Warning 1093: (142-152): Assertion checker does not yet implement this bitwise operator. diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_xor_int.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_int.sol new file mode 100644 index 000000000..87bdd7f8d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_int.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + int8 x = 1; + int16 y = 0; + assert(x ^ y == 1); + int16 z = -1; + assert(x ^ z == -2); + assert(y ^ z == -1); + assert(y ^ z > 0); + x = 7; y = 3; + assert(x ^ y < 5); + assert(x ^ y > 5); + } +} +// ---- +// Warning 6328: (189-206): Assertion violation happens here +// Warning 6328: (247-264): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_xor_uint.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_uint.sol new file mode 100644 index 000000000..70ae0eac6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_uint.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + uint8 x = 1; + uint16 y = 0; + assert(x ^ y != 0); + x = 0xff; + y = 0xff00; + assert(x ^ y == 0xff); + assert(x ^ y == 0xffff); + assert(x ^ y == 0x0000); + } +} +// ---- +// Warning 6328: (155-176): Assertion violation happens here +// Warning 6328: (207-230): Assertion violation happens here