argotorg / argotorg/hevm

`bytes public data` getter loops forever for equivalence checking

Open
#697 6 comments 0 reactions 0 assignees View on GitHub
blocked enhancement
Dominant language
Haskell
Stars
358
Forks
79
Avg merge
1d 1h
Merged PRs (30d)
6

Description

For a trivial contract:

```solidity
contract A {
bytes public data;
function stuff(uint a, uint b) public pure returns (uint) {
unchecked {
uint c = a + b/2;
return c;
}
}
}
```

we loop forever when we want to check equivalence:

```
$EXPSOLC --bin-runtime --via-ir --optimize --ssa-cfg-codegen $FILE | tail -n1 > with.s
$EXPSOLC --bin-runtime --via-ir --optimize $FILE | tail -n1 > without.s
cabal run exe:hevm -- equivalence --code-a-file with.s --code-b-file without.s
```

The two contracts are slightly different, so they don't compare byte-for-byte, and the getter for `bytes public data` loops forever for copying.

To get to the reason, let's compile a much simpler code:

```solidity
contract A {
bytes public data;
}
```

Which , when compiled with: `$EXPSOLC --bin-runtime --via-ir --ir --ir-optimized $FILE` we get:

```
function abi_encode_t_bytes_storage_to_t_bytes_memory_ptr(value, pos) -> ret {
let slotValue := sload(value)
let length := extract_byte_array_length(slotValue)
pos := array_storeLengthForEncoding_t_bytes_memory_ptr(pos, length)
switch and(slotValue, 1)
case 0 {
// short byte array
mstore(pos, and(slotValue, not(0xff)))
ret := add(pos, mul(0x20, iszero(iszero(length))))
}
case 1 {
// long byte array
let dataPos := array_dataslot_t_bytes_storage(value)
let i := 0
for { } lt(i, length) { i := add(i, 0x20) } {
mstore(add(pos, i), sload(dataPos))
dataPos := add(dataPos, 1)
}
ret := add(pos, i)
}
}
```

In the yul, which copies the `data` when `data()` is called. The actual bytecode is:

`6080366004111561000f575b5f5ffd5b5f3560e01c6373d4a13a14610022575f5ffd5b3461000b5736600319015f1361000b575f548060011c60018216801561016557905b60208110821461014d5780845290929190602083018415610131575f94919250906001146100de57919290505b829003601f01601f1916820167ffffffffffffffff8111838210176100c75780604052602081529091516020820181905260408201928192935e8082016040015f9052601f1990601f0116810181900360400190f35b505050634e487b7160e01b5f52604160045260245ffd5b9091925f525f7f290decd9548b62a8d60345a988386fc84ba6bc95484008f6362f93160ef3e5635b83821061011b57509091508201602001610071565b8054828601602001526001019060200190610106565b60ff19909216825291925090602090151560051b830101610071565b50505050634e487b7160e01b5f52602260045260245ffd5b90607f1661004456fea2646970667358221220c358b298b021ffba5627329c90c144b0c2f38566274acc652027a14dcbcad16d64736f6c637827302e382e32392d646576656c6f702e323032352e342e322b636f6d6d69742e32653937356361320058`

which decompiles to these interesting parts:

```
[106] JUMPDEST
[107] DUP4
[108] DUP3
[109] LT
[10a] PUSH2 011b
[10d] JUMPI

[11b] JUMPDEST
[11c] DUP1
[11d] SLOAD
[11e] DUP3
[11f] DUP7
[120] ADD
[121] PUSH1 20
[123] ADD
[124] MSTORE
[125] PUSH1 01
[127] ADD
[128] SWAP1
[129] PUSH1 20
[12b] ADD
[12c] SWAP1
[12d] PUSH2 0106
[130] JUMP
```

where the `LT` checks the loop condition, and the `SLOAD ... MSTORE` does the copy.

Contributor guide

No contributing guide indexed for this repository

Research direction

Reproduce the issue with the provided Solidity contracts and the `exe:hevm` equivalence commands, comparing the optimized and SSA-CFG-codegen outputs. Start by tracing the `bytes public data` getter's generated copying loop and the equivalence execution around it. Done means the equivalence check terminates instead of looping forever while handling the getter correctly.

Written by the indexing model from the issue text.

Assessment

Tech stack
haskell, solidity
Domain
compilers, reverse-engineering
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Needs clarification
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.