From bf21cd400c7fa23f6ce1c506038b42d3e794e34e Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Tue, 1 Jun 2021 17:28:41 +0200 Subject: [PATCH] Fix conversion from bytes to fixed bytes --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 30 +++++++++++++++++++ libsolidity/formal/SMTEncoder.h | 5 ++++ .../typecast/bytes_to_fixed_bytes_1.sol | 22 ++++++++++++++ .../typecast/slice_to_fixed_bytes_1.sol | 6 ++++ 5 files changed, 64 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/slice_to_fixed_bytes_1.sol diff --git a/Changelog.md b/Changelog.md index 95fac0730..271c76229 100644 --- a/Changelog.md +++ b/Changelog.md @@ -18,6 +18,7 @@ Bugfixes: * AST: Do not output value of Yul literal if it is not a valid UTF-8 string. * SMTChecker: Fix internal error on struct constructor with fixed bytes member initialized with string literal. * SMTChecker: Fix internal error on external calls from the constructor. + * SMTChecker: Fix internal error on conversion from ``bytes`` to ``fixed bytes``. * Source Locations: Properly set source location of scoped blocks. * Standard JSON: Properly allow the ``inliner`` setting under ``settings.optimizer.details``. * Type Checker: Fix internal compiler error related to having mapping types in constructor parameter for abstract contracts. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index d14d208aa..eb7e2a17e 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1022,6 +1022,17 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall) return; } + ArrayType const* arrayType = dynamic_cast(argType); + if (auto sliceType = dynamic_cast(argType)) + arrayType = &sliceType->arrayType(); + + if (arrayType && arrayType->isByteArray() && smt::isFixedBytes(*funCallType)) + { + auto array = dynamic_pointer_cast(m_context.expression(*argument)); + bytesToFixedBytesAssertions(*array, _funCall); + return; + } + // TODO Simplify this whole thing for 0.8.0 where weird casts are disallowed. unsigned argSize = argType->storageBytes(); @@ -1206,6 +1217,25 @@ void SMTEncoder::addArrayLiteralAssertions( m_context.addAssertion(smtutil::Expression::select(_symArray.elements(), i) == _elementValues[i]); } +void SMTEncoder::bytesToFixedBytesAssertions( + smt::SymbolicArrayVariable& _symArray, + Expression const& _fixedBytes +) +{ + auto const& fixed = dynamic_cast(*_fixedBytes.annotation().type); + auto intType = TypeProvider::uint256(); + string suffix = to_string(_fixedBytes.id()) + "_" + to_string(m_context.newUniqueId()); + smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context); + m_context.addAssertion(k.currentValue() == 0); + size_t n = fixed.numBytes(); + for (size_t i = 0; i < n; i++) + { + auto kPrev = k.currentValue(); + m_context.addAssertion((smtutil::Expression::select(_symArray.elements(), i) * (u256(1) << ((n - i - 1) * 8))) + kPrev == k.increaseIndex()); + } + m_context.addAssertion(expr(_fixedBytes) == k.currentValue()); +} + void SMTEncoder::endVisit(Return const& _return) { if (_return.expression() && m_context.knownExpression(*_return.expression())) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index e8a0588aa..9b8402cc1 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -245,6 +245,11 @@ protected: std::vector const& _elementValues ); + void bytesToFixedBytesAssertions( + smt::SymbolicArrayVariable& _symArray, + Expression const& _fixedBytes + ); + /// @returns a pair of expressions representing _left / _right and _left mod _right, respectively. /// Uses slack variables and additional constraints to express the results using only operations /// more friendly to the SMT solver (multiplication, addition, subtraction and comparison). diff --git a/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol b/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol new file mode 100644 index 000000000..6f2dd33a4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol @@ -0,0 +1,22 @@ +contract C { + function f() external pure { + bytes memory b = hex"00010203040506070809000102030405060708090001020304050607080900010203040506070809"; + bytes8 c = bytes8(b); + assert(c == 0x0001020304050607); // should hold + assert(c == 0x0001020304050608); // should fail + bytes16 d = bytes16(b); + assert(d == 0x00010203040506070809000102030405); + assert(d == 0x00010203040506070809000102030406); // should fail + bytes24 e = bytes24(b); + assert(e == 0x000102030405060708090001020304050607080900010203); // should hold + assert(e == 0x000102030405060708090001020304050607080900010204); // should fail + bytes32 g = bytes32(b); + assert(g == 0x0001020304050607080900010203040506070809000102030405060708090001); // should hold + assert(g == 0x0001020304050607080900010203040506070809000102030405060708090002); // should fail + } +} +// ---- +// Warning 6328: (225-256): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 283686952306183\nd = 0\ne = 0\ng = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (352-399): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 283686952306183\nd = 5233100606242806050944357496980485\ne = 0\ng = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (526-589): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 283686952306183\nd = 5233100606242806050944357496980485\ne = 96533667595335344310996525432040024692804347064549891\ng = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (732-811): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 283686952306183\nd = 5233100606242806050944357496980485\ne = 96533667595335344310996525432040024692804347064549891\ng = 1780731860627700044956966451854862080991451332659079878538166652776284161\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/typecast/slice_to_fixed_bytes_1.sol b/test/libsolidity/smtCheckerTests/typecast/slice_to_fixed_bytes_1.sol new file mode 100644 index 000000000..e1e7ef692 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/slice_to_fixed_bytes_1.sol @@ -0,0 +1,6 @@ +contract C { + function fromSlice(bytes calldata c) external pure returns (bytes32) { + return bytes32(c[0:33]); + } +} +// ----