From 46653b2d434f026933aa4a8a244a1152ceb7009d Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 15 Jul 2020 18:10:14 +0200 Subject: [PATCH] Fix ICE when bitwise operator on fixed bytes --- Changelog.md | 1 + libsmtutil/SolverInterface.h | 23 +++++++++++-------- libsolidity/formal/SMTEncoder.cpp | 6 +++-- libsolidity/formal/SymbolicTypes.cpp | 4 ++++ .../operators/bitwise_and_fixed_bytes.sol | 8 +++++++ .../operators/bitwise_xor_fixed_bytes.sol | 9 ++++++++ 6 files changed, 40 insertions(+), 11 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol diff --git a/Changelog.md b/Changelog.md index 047b06ddf..4953a4e49 100644 --- a/Changelog.md +++ b/Changelog.md @@ -9,6 +9,7 @@ Compiler Features: * Yul EVM Code Transform: Free stack slots directly after visiting the right-hand-side of variable declarations instead of at the end of the statement only. Bugfixes: + * SMTChecker: Fix internal error when using bitwise operators on fixed bytes type. * Type Checker: Fix overload resolution in combination with ``{value: ...}``. * Type Checker: Fix internal compiler error related to oversized types. diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index be12c3a80..a62a39b37 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -59,10 +59,10 @@ class Expression public: explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {} explicit Expression(std::shared_ptr _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {} - Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {} - Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {} - Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {} - Expression(bigint const& _number): Expression(_number.str(), Kind::Int) {} + Expression(size_t _number): Expression(std::to_string(_number), {}, SortProvider::sintSort) {} + Expression(u256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {} + Expression(s256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {} + Expression(bigint const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {} Expression(Expression const&) = default; Expression(Expression&&) = default; @@ -262,23 +262,28 @@ public: } friend Expression operator+(Expression _a, Expression _b) { - return Expression("+", std::move(_a), std::move(_b), Kind::Int); + auto intSort = _a.sort; + return Expression("+", {std::move(_a), std::move(_b)}, intSort); } friend Expression operator-(Expression _a, Expression _b) { - return Expression("-", std::move(_a), std::move(_b), Kind::Int); + auto intSort = _a.sort; + return Expression("-", {std::move(_a), std::move(_b)}, intSort); } friend Expression operator*(Expression _a, Expression _b) { - return Expression("*", std::move(_a), std::move(_b), Kind::Int); + auto intSort = _a.sort; + return Expression("*", {std::move(_a), std::move(_b)}, intSort); } friend Expression operator/(Expression _a, Expression _b) { - return Expression("/", std::move(_a), std::move(_b), Kind::Int); + auto intSort = _a.sort; + return Expression("/", {std::move(_a), std::move(_b)}, intSort); } friend Expression operator%(Expression _a, Expression _b) { - return Expression("mod", std::move(_a), std::move(_b), Kind::Int); + auto intSort = _a.sort; + return Expression("mod", {std::move(_a), std::move(_b)}, intSort); } friend Expression operator&(Expression _a, Expression _b) { diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index eea0b24e5..6a4030511 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1376,9 +1376,11 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op) bvSize = fixedType->numBits(); isSigned = fixedType->isSigned(); } + else if (auto const* fixedBytesType = dynamic_cast(commonType)) + bvSize = fixedBytesType->numBytes() * 8; - auto bvLeft = smtutil::Expression::int2bv(expr(_op.leftExpression()), bvSize); - auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression()), bvSize); + auto bvLeft = smtutil::Expression::int2bv(expr(_op.leftExpression(), commonType), bvSize); + auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression(), commonType), bvSize); optional result; if (_op.getOperator() == Token::BitAnd) diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index a46b88e03..096f496c4 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -441,7 +441,11 @@ optional symbolicTypeConversion(TypePointer _from, TypePoin // case they'd need to be encoded as numbers. if (auto strType = dynamic_cast(_from)) if (_to->category() == frontend::Type::Category::FixedBytes) + { + if (strType->value().empty()) + return smtutil::Expression(size_t(0)); return smtutil::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add))); + } return std::nullopt; } diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol new file mode 100644 index 000000000..c3212bb23 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f() public pure returns (byte) { + return (byte("") & ("")); + } +} +// ---- +// Warning 5084: (101-109): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol new file mode 100644 index 000000000..3852563be --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract Simp { + function f3() public pure returns (byte) { + bytes memory y = "def"; + return y[0] ^ "e"; + } +} +// ---- +// Warning 1093: (142-152): Assertion checker does not yet implement this bitwise operator.