Redundant store eliminator.#11352
Conversation
fd742a6 to
4231df3
Compare
|
|
||
| // TODO handle reverts of user-defined functions | ||
|
|
||
| // TODO is this all correct WRT termination side-effects of function |
There was a problem hiding this comment.
Probably not important because all we care about are ExpressionStatements.
| object "C_12" { | ||
| code { | ||
| { | ||
| mstore(64, 128) |
There was a problem hiding this comment.
This removal is what most of the gas savings are about...
There was a problem hiding this comment.
Will that still work with enabled stack-limit-evasion, with which this will have to become mstore(64, memoryguard(128)) and be propagated properly?
There was a problem hiding this comment.
If we replace mstore(64, 128) with mstore(64, memoryguard(128)), then none of the mload(64) would be resolved. Which in turn means that this cannot be removed. I think we cannot use memory optimizations if we need to use stack limit evader.
| code { | ||
| { | ||
| let _1 := 1 | ||
| sstore(_1, _1) |
4231df3 to
76dfd1d
Compare
ff59f4e to
799d907
Compare
|
For this code, it would be very useful to somehow combine |
799d907 to
49df2f2
Compare
cameel
left a comment
There was a problem hiding this comment.
Just a few initial remarks. I'm planning to do a full review later.
| inline bool operator==(State _other) const { return m_value == _other.m_value; } | ||
| inline bool operator!=(State _other) const { return !operator==(_other); } | ||
| static inline void join(State& _a, State const& _b) |
There was a problem hiding this comment.
Does inline make any difference here? These should be considred inline by default.
| inline bool operator==(State _other) const { return m_value == _other.m_value; } | |
| inline bool operator!=(State _other) const { return !operator==(_other); } | |
| static inline void join(State& _a, State const& _b) | |
| bool operator==(State _other) const { return m_value == _other.m_value; } | |
| bool operator!=(State _other) const { return !operator==(_other); } | |
| static void join(State& _a, State const& _b) |
| static inline void join(State& _a, State const& _b) | ||
| { | ||
| // Using "max" works here because of the order of the values in the enum. | ||
| _a.m_value = Value(std::max(int(_a.m_value), int(_b.m_value))); |
There was a problem hiding this comment.
| _a.m_value = Value(std::max(int(_a.m_value), int(_b.m_value))); | |
| _a.m_value = Value(std::max(int(_a.m_value), int(_b.m_value))); |
| /// Joins the assignment mapping of @a _source into @a _target according to the rules laid out | ||
| /// above. | ||
| /// Will destroy @a _source. | ||
| static void merge(TrackedStores& _target, TrackedStores&& _source); | ||
| static void merge(TrackedStores& _target, std::vector<TrackedStores>&& _source); |
There was a problem hiding this comment.
Which rules is this referring to? Was RedundantStoreEliminator meant to have a docstring describing them?
There was a problem hiding this comment.
This is copied from redundant assign eliminator. I guess it is documented there. I still need to combine the code.
| return false; | ||
| if (_covered.start && _covered.length && _covered.start == _covering.start && _covered.length == _covering.length) | ||
| return true; | ||
| if (_covered.location == Location::Storage && _covered.start && _covering.start && *_covered.start == *_covering.start) |
There was a problem hiding this comment.
Why not use knowledge base here to check equality?
There was a problem hiding this comment.
Because the CSE will have done the work for us already.
| if (optional<u256> startDiff = knowledge.differenceIsKnownConstant(*_covered.start, *_covering.start)) | ||
| if (optional<u256> lengthDiff = knowledge.differenceIsKnownConstant(*_covering.length, *_covered.length)) | ||
| if (*startDiff <= *lengthDiff && *startDiff <= largestPositive && *lengthDiff <= largestPositive) | ||
| return true; |
There was a problem hiding this comment.
Maybe you can add a test that would lead to an incorrect removal and mention EIP-1985?
{
let x := 0
calldatacopy(0, 0, 115792089237316195423570985008687907853269984665640564039457584007913129639935)
mstore(x, 20)
return(0, 32)
}
// ----
// step: redundantStoreEliminator
//
// {
// let x := 0
// let _1 := 115792089237316195423570985008687907853269984665640564039457584007913129639935
// let _2 := 0
// let _3 := 0
// mstore(x, 20)
// return(0, 32)
// }
There was a problem hiding this comment.
Interesting! So it seems there is a bug in my code?
There was a problem hiding this comment.
I think it can have bugs like these when writing to locations beyond 2**128 - 1. This is a grey area because of EIP-1985.
49df2f2 to
a86689a
Compare
|
Rebased and added a feature to only ignore memory if msize is found. |
You surely didn't rebase it to the head given all these conflicts displayed 😅 |
|
Now rebased. |
ef143c8 to
0a57b2a
Compare
26c80b8 to
b2d5289
Compare
792e9f0 to
573d3de
Compare
|
Rebased this on top of the refactor. |
9758f5b to
f9bc427
Compare
| // sstore(0, length) | ||
| // mstore(64, newFreePtr) | ||
| // mstore(memPtr, length) | ||
| // extcodecopy(value, add(memPtr, 32), 0, length) |
There was a problem hiding this comment.
I hope we can prove memPtr + 32 <= memPtr + 32 with the linear solver soon...
3b0c244 to
0d0802d
Compare
| optional<u256> startDiff = knowledge.differenceIfKnownConstant(*_covered.start, *_covering.start); | ||
| optional<u256> coveredLength = knowledge.valueIfKnownConstant(*_covered.length); | ||
| optional<u256> lengthDiff = knowledge.differenceIfKnownConstant(*_covering.length, *_covered.length); | ||
| if ( |
There was a problem hiding this comment.
There is no proof for this yet.
|
Note that this step is less powerful than it could be due to the following reason:
This would also more nicely structure the code. |
| if (*length2 <= *diff && *length2 <= largestPositive && *diff <= largestPositive) | ||
| return true; | ||
| } | ||
| // We use diff >= _op1.length && diff <= 2**256 - _op2.length |
There was a problem hiding this comment.
This is so annoying. This is not enough to remove the mstore in
mstore(0, 0)
let length := calldataload(0)
calldatacopy(0x20, 0x20, length)
return(0x20, length)
There was a problem hiding this comment.
Just to check that I understand this thing correctly (which I might not yet)... what currently happens is that both the mstore and the calldatacopy are Undecided when we hit the return and then the return does not know that it won't read from 0 because of the potential overflow?
Couldn't we when hitting the return walk the previous memory writes in backwards order and check for knownCovered writes and if we find one stop?
I.e. return(0x20, length) would first look at calldatacopy(0x20, 0x20, length), realize that its entire read is covered by that write and be satisfied and not even consider earlier writes, i.e. not even consider the mstore(0,0)...
Then the mstore(0,0) would remain Undecided and be removed, right?
There was a problem hiding this comment.
I mean: the reason that we can remove mstore(0,0) is not that the return won't read from offset 0, but that it will only read what calldatacopy wrote, isn't it?
There was a problem hiding this comment.
The order of writes is not preserved in m_stores, though, is it? Hm...
There was a problem hiding this comment.
The reason is that knownUnrelated does not return true for the mstore(0, 0) and return(0x20, length).
There was a problem hiding this comment.
That's one reason why we can remove mstore(0,0)... the other reason is that the memory read by return(0x20, length) is fully covered by calldatacopy(0x20, 0x20, length), so no earlier writes are relevant.
Ideally we'd be able to exploit both of those reasons...
There was a problem hiding this comment.
If you had mstore(0x20, 0) instead, then return(0x20, length) would not be unrelated, but the mstore could still be removed.
There was a problem hiding this comment.
I could actually imagine that that reason is the more useful one in general, since we'll probably rarely just read random stuff that wasn't written specifically... so in general, I think it will more often be the case that something only reads stuff covered by earlier writes rather than that the locations are known to be disjoint...
In general, though, we would have to track this across multiple writes - it's just a coincidence that it's a single write that covers the entire read in this example... i.e. in
mstore(y, 0x42)
mstore(x, 0x20)
mstore(add(x, 0x20), 0x20)
return(x, 0x40)
I'd ideally want to recognize that the last two mstores together cover everything that's read by the return and be able to remove the first mstore without any knowledge about x or y... but yeah, just ideally, this may be infeasible to do...
There was a problem hiding this comment.
Well, actually, probably not infeasible... but at least tricky :-).
There was a problem hiding this comment.
Note from call: maybe it's worth differentiating between diff being positive or negative. So with an s256 diff, it may be
if (diff >= 0 && diff >= length1)
return true;
if (diff < 0 && -diff >= length2)
return true;
But at least I haven't convinced myself yet that there's no other weird overflow cases to consider.
| *instruction == Instruction::EXTCODECOPY || | ||
| *instruction == Instruction::CODECOPY || | ||
| *instruction == Instruction::CALLDATACOPY || | ||
| *instruction == Instruction::RETURNDATACOPY || | ||
| *instruction == Instruction::MSTORE || | ||
| *instruction == Instruction::MSTORE8 |
There was a problem hiding this comment.
Don't we have some abstract semantic property to cover this? Hm, in those "writing to memory" includes the call opcodes...
There was a problem hiding this comment.
You are right, even if we don't have such a property yet, we should create it. "No side effects apart from writing to memory".
| scheduleUnusedForDeletion(); | ||
| } | ||
|
|
||
| vector<UnusedStoreEliminator::Operation> UnusedStoreEliminator::operationsFromFunctionCall( |
There was a problem hiding this comment.
I wonder whether we should move the main part of this to some abstract semantic property as well.
I.e. just have the builtins tell us "I'm reading the memory range [arg0, arg1)" instead of just "I'm reading memory".
There was a problem hiding this comment.
It might be useful to have that information elsewhere and also if e.g. there's ever a new EVM opcode that accesses memory or storage, we'll definitely define its semantic properties, but it's much easier to miss editing stuff elsewhere like here.
There was a problem hiding this comment.
Yep, true! We could use that routine in/as replacement for isSimpleLoad / isSimpleStore
| // sstore(not(gcd(_3, _2)), _1) | ||
| // sstore(2, _1) | ||
| // extcodecopy(_1, msize(), _1, _1) | ||
| // sstore(0, 0) |
There was a problem hiding this comment.
I have NO idea why this was missing before - maybe there is a really bad bug lurking here somewhere...
There was a problem hiding this comment.
That's really a bit weird...
There was a problem hiding this comment.
Or wait... did "before" have the equal store eliminator merged :-)? If so, then that's the reason I guess.
There was a problem hiding this comment.
Yeah, I guess that's it. And the equal store eliminator removes the second copy, while the redundant store eliminator removes the first...
There was a problem hiding this comment.
But even the equal store eliminator cannot remove this, can it?
It might be that the test results were just wrong for an earlier commit...
There was a problem hiding this comment.
ok sure, but you cannot have both of them missing?
By the way, do we actually still need the equal store eliminator?
There was a problem hiding this comment.
The diff I'm seeing merely moves the sstore(0, 0) three lines down...
There was a problem hiding this comment.
The input contains two sstore(0, 0), the output contained one of them before the diff, and still contains one of them after the diff, it just removes the other one.
There was a problem hiding this comment.
But yeah, I didn't get the chance to look at the equal store eliminator, but it did sound redundant to me relative to the redundant store eliminator :-).
|
|
||
| k = Int('k') | ||
| diff = Int('diff') | ||
| solver.add(diff == start2 - start1 + k * 2**n_bits) |
There was a problem hiding this comment.
If we go with the assumption that all memory access is "small", this file needs to be updated to show that the condition is correct under that assumption.
|
Do we want to split this into storage and memory and wait with the memory part until we have the linear solver? |
That may make sense, yes - if only, s.t. it's only one of the two to think about for the first version :-). We can also see what Fe says on Monday about the entire #11352 (comment) discussion... |
4eebb71 to
fdee68f
Compare
|
Replaced by #12672 |
No description provided.