Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

SMTChecker: Fix equality of array literals #15050

Merged
merged 1 commit into from May 8, 2024
+116 −74
Merged

SMTChecker: Fix equality of array literals #15050

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions Changelog.md
View file
Open in desktop
Expand Up @@ -9,6 +9,7 @@ Compiler Features:

Bugfixes:
* Commandline Interface: Fix ICE when the optimizer is disabled and an empty/blank string is used for ``--yul-optimizations`` sequence.
* SMTChecker: Fix false positive when comparing hashes of same array or string literals.
* SMTChecker: Fix internal error on mapping access caused by too strong requirements on sort compatibility of the index and mapping domain.
* SMTChecker: Fix internal error when using an empty tuple in a conditional operator.
* SMTChecker: Fix internal error when using bitwise operators with an array element as argument.
Expand Down
21 changes: 20 additions & 1 deletion libsolidity/formal/SMTEncoder.cpp
View file
Open in desktop
Expand Up @@ -1296,8 +1296,27 @@ void SMTEncoder::addArrayLiteralAssertions(
)
{
m_context.addAssertion(_symArray.length() == _elementValues.size());

// Assert to the solver that _elementValues are exactly the elements at the beginning of the array.
// Since we create new symbolic representation for every array literal in the source file, we want to ensure that
// representations of two equal literals are also equal. For this reason we always start from constant-zero array.
// This ensures SMT-LIB arrays (which are infinite) are also equal beyond the length of the Solidity array literal.
auto type = _symArray.type();
smtAssert(type);
auto valueType = [&]() {
Copy link
Collaborator

@pgebal pgebal Apr 25, 2024 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can leave it like it is but I think that first declaring a var
and then using if statements to assign to it is more straightforward.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I actually disagree with that, splitting the declaration and initialization is often considered an anti-pattern.
See for example Core Guidelines ES 22, ES 28, or this talk.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right. I never thought about this like that. Makes sense.

if (auto const* arrayType = dynamic_cast<ArrayType const*>(type))
return arrayType->baseType();
if (smt::isStringLiteral(*type))
return TypeProvider::stringMemory()->baseType();
smtAssert(false);
}();
auto tupleSort = std::dynamic_pointer_cast<smtutil::TupleSort>(smt::smtSort(*type));
auto sortSort = std::make_shared<smtutil::SortSort>(tupleSort->components.front());
smtutil::Expression arrayExpr = smtutil::Expression::const_array(smtutil::Expression(sortSort), smt::zeroValue(valueType));
smtAssert(arrayExpr.sort->kind == smtutil::Kind::Array);
for (size_t i = 0; i < _elementValues.size(); i++)
m_context.addAssertion(smtutil::Expression::select(_symArray.elements(), i) == _elementValues[i]);
arrayExpr = smtutil::Expression::store(arrayExpr, smtutil::Expression(i), _elementValues[i]);
m_context.addAssertion(_symArray.elements() == arrayExpr);
}

void SMTEncoder::bytesToFixedBytesAssertions(
Expand Down
2 changes: 1 addition & 1 deletion test/cmdlineTests/model_checker_invariants_all/err
View file
Open in desktop
Expand Up @@ -9,6 +9,6 @@ Info: CHC: 1 verification condition(s) proved safe! Enable the model checker opt
Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test:
(!(x >= 1) || true)
Reentrancy property(ies) for model_checker_invariants_all/input.sol:test:
(((!(x <= 0) || !(x' >= 1)) && (!(x <= 0) || !(<errorCode> >= 1))) || true)
(((!(x <= 0) || !(<errorCode> >= 1)) && (!(x <= 0) || !(x' >= 1))) || true)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The order of the conjuncts changed, but the formula is equivalent.

<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x == 0)
2 changes: 1 addition & 1 deletion test/cmdlineTests/model_checker_invariants_contract_reentrancy/err
View file
Open in desktop
Expand Up @@ -9,6 +9,6 @@ Info: CHC: 1 verification condition(s) proved safe! Enable the model checker opt
Info: Contract invariant(s) for model_checker_invariants_contract_reentrancy/input.sol:test:
(!(x >= 1) || true)
Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
(((!(x <= 0) || !(x' >= 1)) && (!(x <= 0) || !(<errorCode> >= 1))) || true)
(((!(x <= 0) || !(<errorCode> >= 1)) && (!(x <= 0) || !(x' >= 1))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x == 0)
20 changes: 8 additions & 12 deletions test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol
View file
Open in desktop
Expand Up @@ -2,29 +2,25 @@ contract C {
function abiencodePackedStringLiteral() public pure {
bytes memory b1 = abi.encodePacked("");
bytes memory b2 = abi.encodePacked("");
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b2.length);
assert(b1.length == b2.length); // should hold

bytes memory b3 = abi.encodePacked(bytes(""));
assert(b1.length == b3.length); // should fail
assert(b1.length == b3.length); // should hold
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we also have assertions for cases such as the one below?

		bytes memory a = abi.encodePacked(bytes(""));
		bytes memory b = abi.encodePacked(bytes(""));
		assert(a.length == b.length);

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't what we have now more general?

I think I was asking about it and "" should behave the same as bytes("") when fed to abi.encode* functions, no?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes. But I was just wondering if we should have such assertions as well. Because they should also hold. But maybe this is already tested.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In principle, you are right, but it feels like we could have many more tests like that, and these are not exactly cheap.
In my opinion, the basic functionality (given the same arguments, the result is the same) is already sufficiently covered.


bytes memory b4 = abi.encodePacked(bytes24(""));
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b4.length);
assert(b1.length == b4.length); // should fail

bytes memory b5 = abi.encodePacked(string(""));
assert(b1.length == b5.length); // should fail
assert(b1.length == b5.length); // should hold, but currently fails due to abstraction

bytes memory b6 = abi.encode("");
assert(b1.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (226-256): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = [0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (310-340): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (483-513): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (568-598): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (654-684): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a]\nb6 = [0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117]\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (354-384): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (454-484): CHC: Assertion violation happens here.\nCounterexample:\n\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (580-610): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
20 changes: 8 additions & 12 deletions test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol
View file
Open in desktop
Expand Up @@ -2,18 +2,16 @@ contract C {
function abiencodePackedStringLiteral() public pure {
bytes memory b1 = abi.encodePacked("");
bytes memory b2 = abi.encodePacked("");
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b2.length);
assert(b1.length == b2.length); // should hold

bytes memory b3 = abi.encodePacked(bytes(""));
assert(b1.length == b3.length); // should fail
assert(b1.length == b3.length); // should hold

bytes memory b4 = abi.encodePacked(bytes24(""));
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b4.length);
assert(b1.length == b4.length); // should fail

bytes memory b5 = abi.encodePacked(string(""));
assert(b1.length == b5.length); // should fail
assert(b1.length == b5.length); // should hold, but fails due to abstraction

bytes memory b6 = abi.encode("");
assert(b1.length == b6.length); // should fail
Expand All @@ -22,10 +20,8 @@ contract C {
// ====
// SMTEngine: all
// SMTShowUnproved: no
// SMTIgnoreOS: macos
// ----
// Warning 6328: (226-256): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = [0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (310-340): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (483-513): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (568-598): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (654-684): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a]\nb6 = [0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117]\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (354-384): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (454-484): CHC: Assertion violation happens here.\nCounterexample:\n\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (570-600): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
17 changes: 7 additions & 10 deletions test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
View file
Open in desktop
Expand Up @@ -2,25 +2,22 @@ contract C {
function abiEncodeStringLiteral() public pure {
bytes memory b1 = abi.encode("");
bytes memory b2 = abi.encode("");
// should hold, but currently fails due to string literal abstraction
// should hold
assert(b1.length == b2.length);

bytes memory b3 = abi.encode(bytes(""));
assert(b1.length == b3.length); // should fail
assert(b1.length == b3.length); // should hold

bytes memory b4 = abi.encode(bytes24(""));
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b4.length);
assert(b1.length == b4.length); // should fail

bytes memory b5 = abi.encode(string(""));
assert(b1.length == b5.length); // should fail
assert(b1.length == b5.length); // should hold, but currently fails due to abstraction
}
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (208-238): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = []\nb4 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
// Warning 6328: (286-316): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d]\nb3 = [0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d]\nb4 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
// Warning 6328: (453-483): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
// Warning 6328: (532-562): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca]\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
// Warning 6328: (326-356): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
// Warning 6328: (420-450): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
21 changes: 9 additions & 12 deletions test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol
View file
Open in desktop
Expand Up @@ -2,29 +2,26 @@ contract C {
function abiEncodeStringLiteral(bytes4 sel) public pure {
bytes memory b1 = abi.encodeWithSelector(sel, "");
bytes memory b2 = abi.encodeWithSelector(sel, "");
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b2.length);

assert(b1.length == b2.length); // should hold

bytes memory b3 = abi.encodeWithSelector(sel, bytes(""));
assert(b1.length == b3.length); // should fail
assert(b1.length == b3.length); // should hold

bytes memory b4 = abi.encodeWithSelector(sel, bytes24(""));
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b4.length);
assert(b1.length == b4.length); // should fail

bytes memory b5 = abi.encodeWithSelector(sel, string(""));
assert(b1.length == b5.length); // should fail
assert(b1.length == b5.length); // should hold, but currently fails due to abstraction

bytes memory b6 = abi.encodeWithSelector(0xcafecafe, bytes24(""));
assert(b4.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (252-282): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb1 = [0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
// Warning 6328: (347-377): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb3 = [0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
// Warning 6328: (531-561): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb1 = [0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90]\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
// Warning 6328: (627-657): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb5 = [0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
// Warning 6328: (746-776): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb2 = []\nb5 = [0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2]\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
// Warning 6328: (403-433): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
// Warning 6328: (514-544): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
// Warning 6328: (673-703): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.