NY: keep loop-carried memory offsets dynamic in the heap analysis

[xermicus]

Loop variables and outputs inherited the initializer's static offset, so every iteration resolved to the first address and later words stayed eligible for native byte order. The FMP propagation now also invalidates on unresolvable mstore and mstore8 inside regions, which the reporter's mstore8 loop needed.

[elle-j]

Looks like this change regressed mstores (the ones using the loop counter) where the first iteration writes the fmp word (either from 0x40, inside the word, or starting before it while still overlapping). E.g.:

for { let p := 0x40 } ... { mstore(p, v) }

In those cases the loaded value would be truncated. Before the change, fmp_could_be_unbounded was eventually set in this case since the counter's first value was checked. Now it's no longer set so the range proof is still enabled.

Also, mstore using loop counters has the same issue for counters reaching the fmp word at a later iteration. E.g. when decrementing:

for { let p := 0x80 } ... { p := sub(p, 0x20) } { mstore(p, v) }

[elle-j]

Copies also seem to have regressed where the length is the loop counter:

for { let n := 0x40 } lt(n, end) { n := add(n, 1) } { calldatacopy(0, 0, n) }

Only the start word will be tainted now and fmp_could_be_unbounded won't be set for copies starting below the fmp word but reaches it due to the length. Before, the length at the first iteration was evaluated.

[elle-j]

This also turns every function with an unresolvable store into an fmp writer, so calling a require string helper or an event-emitting function now drops the propagated free pointer. Those functions only store at or above the fmp (with add(mload(0x40), small_literal), which can't reach the fmp word while the pointer is at least 0x60.

The previous implementation incorrectly ignored every unresolved store in a callee (e.g. f(p, v) { mstore(p, v) } called with p = 0x40), which your changes fix, but a side effect of that previous behavior was that the above issue couldn't exist either.

We could probably fix it by not counting stores at add(mload(0x40), small_literal) as fmp writes (when the fmp is known by the propagation and is at least 0x60).

[xermicus]

The regression does not seem to be significant (+36 bytes over the OZ test contracts). This could be a follow-up instead.

[elle-j]

Scratch only means a store starts below 0x40, so a full-word store starting below it (but still within reach) still overwrites part of the fmp word. This change (and in preexisting propagate_statements()) makes unresolved Scratch stores be treated as if they can never touch the fmp.

For instance, in this example the offset is bound outside the branch, so the walk inside the branch can't resolve it, and mload(0x40) returns the stale 0x80:

mstore(0x40, 0x80)
let offset := 0x30
if calldataload(64) {
    mstore(offset, calldataload(0))
    mstore(0, mload(0x40))
    return(0, 32)
}

[elle-j]

Suggested change

	- `--newyork`: a memory offset carried by a loop counter resolved to its first iteration address on every iteration, leaving words written by later iterations eligible for native byte order, and a stale free memory pointer survived an unresolvable store inside a branch.
	- `--newyork`: a memory offset carried by a loop counter resolved to its first iteration address on every iteration, leaving words written by later iterations eligible for native byte order, and a stale free memory pointer survived an unresolvable `mstore8`, or an unresolvable `mstore` inside a branch, loop, or called function. [#612](https://github.com/paritytech/revive/pull/612)

[xermicus]

Thanks for the very thorough review @elle-j! All findings should be fixed now

[elle-j]

Great thanks! Some issues still exist, I've opened PR 617 as feedback targeting this branch that addresses the remaining comments below. Should be good to go after that.

[elle-j]

Some corrections for how we can determine whether the counter is ascending and what the lower bound is:

(PR 617 has updates and tests that fix these various scenarios, feel free to merge it into this PR and change anything in there if needed 👍)

1. loop_counter_ascends() currently only checks that the post region adds something to the counter, but not what it adds. So an add(pointer, not(31)) (which is solc's optimized version of sub(pointer, 0x20)) counts as ascending. The LoopStoreFmpDescending.yul loop mstore test (which uses sub) would still be miscompiled if that Yul was instead written as inline assembly in Solidity since it'd go through the solc optimizer. And the following copy will overwrite the fmp word but still keep the range proof:

mstore(0x40, 0x80)
for { let pointer := 0x80 } gt(pointer, 0x20) { pointer := add(pointer, not(0x1f)) } {
    calldatacopy(pointer, 0, 0x20)
}
mstore(0, mload(0x40))
return(0, 32)

2. A counter step that counts down gets lower bound 0 here (which is correct), but the lower bound of add(0x80, step) is then calculated as 0x80 + 0 = 0x80, so the mstore below looks like it never writes below 0x80. But after the first sub, step wraps and becomes huge, so add(0x80, step) overflows and also wraps to 0x60, then 0x40 (i.e. it does get smaller than 0x80):

for { let step := 0 } sgt(step, sub(0, 0x60)) { step := sub(step, 0x20) } {
    mstore(add(0x80, step), value)
}

3. Only literals, loop counters, and add/mul of values that have a lower bound get a lower bound. Other operations (like shl and sub) currently don't get one. Without one, fmp_could_be_unbounded is not set for an mstore destination. So this includes mul by a power of two, because newyork rewrites it into shl before this analysis runs. The mul(index, 0x20) below becomes shl(5, index), and the third iteration's mstore will be to 0x40:

for { let index := 0 } lt(index, 3) { index := add(index, 1) } {
    mstore(mul(index, 0x20), value)
}

4. Currently write pointers that advance inside the body are not counted as ascending (e.g. the loop solc emits that copies a storage array into memory, like mpos := add(mpos, 32)). Detected in T3rminalBulletinIndex that returns a string[] from storage, which grows about +18% (at -Oz) due to losing the range proof. Part of that emitted Yul is this:

let i := 0
for { } lt(i, length_2) { i := add(i, 1) }
{
    mstore(mpos, copy_array_from_storage_to_memory_string(spos))
    mpos := add(mpos, 32)
    spos := add(spos, 1)
}

[elle-j]

The stale forward from my earlier comment is gone now 👍, but when fuzzy dedup merges helpers and turns a Scratch offset into a parameter, a store through that parameter never sets fmp_could_be_unbounded, so the range proof stays and a later load value is truncated.

This check could look for MemoryRegion::Scratch as well since that tag only says that the store starts below 0x40 (but it could still reach into the fmp word):

- if static_offset.is_none() && self.loop_offset_may_reach_fmp_word(offset) {
+ if static_offset.is_none() && (*region == MemoryRegion::Scratch || self.loop_offset_may_reach_fmp_word(offset))
  {
      self.fmp_could_be_unbounded = true;
  }

(This change is also part of the feedback PR.)