From ff0c794674cc1922cf11f3eac1313b554a9f7516 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Thu, 3 Dec 2020 18:22:45 +0100 Subject: [PATCH] [SMTChecker] Fixing conversion from StringLiteral to FixedBytes --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 17 +++++++++++------ libsolidity/formal/SymbolicTypes.cpp | 6 ++++-- .../operators/bitwise_and_fixed_bytes.sol | 10 +++++++--- .../operators/bitwise_not_fixed_bytes.sol | 2 +- .../operators/bitwise_or_fixed_bytes.sol | 10 +++++++--- .../operators/bitwise_xor_fixed_bytes.sol | 11 +++++++---- .../string_literal_to_dynamic_bytes.sol | 12 ++++++++++++ .../string_literal_to_fixed_bytes_upcast.sol | 10 ++++++++++ 9 files changed, 60 insertions(+), 19 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/typecast/string_literal_to_dynamic_bytes.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_upcast.sol diff --git a/Changelog.md b/Changelog.md index 9b9461c5c..2ff704505 100644 --- a/Changelog.md +++ b/Changelog.md @@ -18,6 +18,7 @@ Bugfixes: * SMTChecker: Fix internal compiler error when doing bitwise compound assignment with string literals. * SMTChecker: Fix internal error when trying to generate counterexamples with old z3. * SMTChecker: Fix segmentation fault that could occur on certain SMT-enabled sources when no SMT solver was available. + * SMTChecker: Fix cast string literals to byte arrays. * Type Checker: ``super`` is not available in libraries. * Yul Optimizer: Fix a bug in NameSimplifier where a new name created by NameSimplifier could also be created by NameDispenser. * Yul Optimizer: Removed NameSimplifier from optimization steps available to users. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 273fbebc6..2ff52066d 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -959,16 +959,21 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall) solAssert(_funCall.arguments().size() == 1, ""); auto argument = _funCall.arguments().front(); - auto const& argType = argument->annotation().type; + auto const argType = argument->annotation().type; + auto const funCallType = _funCall.annotation().type; - unsigned argSize = argument->annotation().type->storageBytes(); - unsigned castSize = _funCall.annotation().type->storageBytes(); + auto symbArg = expr(*argument, funCallType); - auto const& funCallType = _funCall.annotation().type; + if (smt::isStringLiteral(*argType) && smt::isFixedBytes(*funCallType)) + { + defineExpr(_funCall, symbArg); + return; + } // TODO Simplify this whole thing for 0.8.0 where weird casts are disallowed. - auto symbArg = expr(*argument, funCallType); + unsigned argSize = argType->storageBytes(); + unsigned castSize = funCallType->storageBytes(); bool castIsSigned = smt::isNumber(*funCallType) && smt::isSigned(funCallType); bool argIsSigned = smt::isNumber(*argType) && smt::isSigned(argType); optional symbMin; @@ -1112,7 +1117,7 @@ void SMTEncoder::endVisit(Literal const& _literal) addArrayLiteralAssertions( *symbArray, - applyMap(_literal.value(), [&](auto const& c) { return smtutil::Expression{size_t(c)}; }) + applyMap(_literal.value(), [](unsigned char c) { return smtutil::Expression{size_t(c)}; }) ); } else diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index e31b81da8..6fdd59d96 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -566,11 +566,13 @@ optional symbolicTypeConversion(TypePointer _from, TypePoin // but they can also be compared/assigned to fixed bytes, in which // case they'd need to be encoded as numbers. if (auto strType = dynamic_cast(_from)) - if (_to->category() == frontend::Type::Category::FixedBytes) + if (auto fixedBytesType = dynamic_cast(_to)) { if (strType->value().empty()) return smtutil::Expression(size_t(0)); - return smtutil::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add))); + auto bytesVec = util::asBytes(strType->value()); + bytesVec.resize(fixedBytesType->numBytes(), 0); + return smtutil::Expression(u256(toHex(bytesVec, 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 index b7e16d346..0f8c65227 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol @@ -1,7 +1,11 @@ pragma experimental SMTChecker; contract C { - function f() public pure returns (byte) { - return (byte("") & ("")); - } + function f() public pure { + assert(byte("") & ("") == byte(0)); // should hold + assert(byte(0xAA) & byte(0x55) == byte(0)); // should hold + assert(byte(0xFF) & byte(0xAA) == byte(0xAA)); // should hold + assert(byte(0xFF) & byte(0xAA) == byte(0)); // should fail + } } // ---- +// Warning 6328: (253-295): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol index 0e6e1642c..96060ac94 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol @@ -9,4 +9,4 @@ contract C { } } // ---- -// Warning 6328: (175-198): CHC: Assertion violation happens here. +// Warning 6328: (133-156): CHC: 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 index 1b937cf9d..a650ff7d9 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol @@ -1,7 +1,11 @@ pragma experimental SMTChecker; contract C { - function f() public pure returns (byte) { - return (byte(0x0F) | (byte(0xF0))); - } + function f() public pure returns (byte) { + byte b = (byte(0x0F) | (byte(0xF0))); + assert(b == byte(0xFF)); // should hold + assert(b == byte(0x00)); // should fail + return b; + } } // ---- +// Warning 6328: (172-195): CHC: 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 69cea474f..c363082cd 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol @@ -1,8 +1,11 @@ pragma experimental SMTChecker; contract Simp { - function f3() public pure returns (byte) { - bytes memory y = "def"; - return y[0] ^ "e"; - } + function f3() public pure returns (byte) { + bytes memory y = "def"; + assert(y[0] ^ "e" != byte(0)); // should hold + assert(y[1] ^ "e" != byte(0)); // should fail + return y[0]; + } } // ---- +// Warning 6328: (168-197): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_dynamic_bytes.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_dynamic_bytes.sol new file mode 100644 index 000000000..89306a0d1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_dynamic_bytes.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + bytes memory b = bytes(hex"ffff"); + assert(b.length == 2); // should hold + assert(b[0] == byte(uint8(255))); // should hold + assert(b[1] == byte(uint8(100))); // should fail + } +} +// ---- +// Warning 6328: (204-236): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_upcast.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_upcast.sol new file mode 100644 index 000000000..c69479302 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_upcast.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + assert(bytes4(hex"0000ffff") == bytes4(hex"ffff")); // should fail + assert(bytes4(hex"ffff0000") == bytes4(hex"ffff")); // should hold + } +} +// ---- +// Warning 6328: (76-126): CHC: Assertion violation happens here.