SMTChecker: Fix equality of array literals #15050
Conversation
blishko
force-pushed
the
smt-fix-bytearray-equality
branch
5 times, most recently
from
86862ce
to
024ecfb
Compare
| // ---- | ||
| // Warning 9302: (212-228): Return value of low-level calls not used. | ||
| // Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, lock = false\n_a = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.set(1)\nState: x = 1, lock = false\nC.f(0x0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(0) -- reentrant call | ||
| // Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0x0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0x0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(1) -- reentrant call |
There was a problem hiding this comment.
Both counterexamples are valid, but it keeps changing with changes in the encoding, so I am setting the option to ignore CEX her.
| @@ -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) | |||
There was a problem hiding this comment.
The order of the conjuncts changed, but the formula is equivalent.
| assert(s1 == s2); | ||
| } | ||
|
|
||
| function c3() public pure { |
There was a problem hiding this comment.
Pleae add a negative example like
function c4() public pure {
bytes32 s1 = sha256("110");
bytes32 s2 = sha256("100");
assert(s1 == s2); // should fail
}
and similar for array literal case
There was a problem hiding this comment.
Hmm, so I tried to add a negative example and it added 7 seconds to the runtime of the test.
For that reason I would prefer not adding the negative test, as I don't think it adds much value.
There are other tests that compare keccak of different bytes, so maybe we don't need the same for string literals, considering the trade-off?
| // 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 = [&]() { |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Right. I never thought about this like that. Makes sense.
blishko
force-pushed
the
smt-fix-bytearray-equality
branch
from
024ecfb
to
05ac8c3
Compare
There are two kinds of array literals in Solidity: string literals (arrays of characters/bytes) and proper array literals (e.g., [1,2,3]). While array literals cannot be directly tested for equality in Solidity, it is possible to compute hash of these values and compare hashes. The expectation is that hashes of the same array literals would be the same, but previously SMTChecker returned false positive in this case, saying that they don't have to be equal. The reason for the false positive was the following. We represent Solidity array literal as a tuple `(elements, length)` where `length` is an integer representing the actualy length of the array literal, and `elements` are an SMT-LIB array, where the first `length` elements represent the actual content of the array literal. However, SMT-LIB arrays are infinite objects (more like functions from indices to elements). Previously, we left the part after `length`-th element unspecified. For the solver this meant that two array literals equal at the Solidity level were represented with two different SMT-LIB arrays. The proposed solution is to always start from a constant-zero array, and use store operations to build an SMT-LIB array that matches the Solidity array literal.
blishko
force-pushed
the
smt-fix-bytearray-equality
branch
from
05ac8c3
to
2572e13
Compare
|
|
||
| bytes memory b3 = abi.encodePacked(bytes("")); | ||
| assert(b1.length == b3.length); // should fail | ||
| assert(b1.length == b3.length); // should hold |
There was a problem hiding this comment.
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);There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There are two kinds of array literals in Solidity: string literals (arrays of characters/bytes) and proper array literals (e.g., [1,2,3]). While array literals cannot be directly tested for equality in Solidity, it is possible to compute hash of these values and compare hashes. The expectation is that hashes of the same array literals would be the same, but previously SMTChecker returned false positive in this case, saying that they don't have to be equal.
The reason for the false positive was the following. We represent Solidity array literal as a tuple
(elements, length)wherelengthis an integer representing the actualy length of the array literal, andelementsare an SMT-LIB array, where the firstlengthelements represent the actual content of the array literal. However, SMT-LIB arrays are infinite objects (more like functions from indices to elements). Previously, we left the part afterlength-th element unspecified. For the solver this meant that two array literals equal at the Solidity level were represented with two different SMT-LIB arrays.The proposed solution is to always start from a constant-zero array, and use store operations to build an SMT-LIB array that matches the Solidity array literal.
Fixes #14983.