co-authored by claude opus 4.6
Summary
The internal_return_copy_forwarding and readonly_invoke_copy_forwarding passes rewrite all downstream uses of a destination alloca alias to use the source alloca pointer instead. This is correct when all uses are memory accesses (MLOAD, MSTORE, etc.), because the forwarding preconditions guarantee the memory content at both pointers is identical. However, if any downstream use performs arithmetic on the pointer value itself (e.g. add %dst, 32 for struct field access), the rewrite changes the computed value.
Details
Consider:
%ret_buf = alloca 64
invoke @f, %ret_buf ; callee writes to ret_buf
mcopy %dst, %ret_buf, 64 ; copy return data
%field_ptr = add %dst, 32 ; pointer arithmetic for field access
%val = mload %field_ptr ; load field
After IRCF forwards:
%ret_buf = alloca 64
invoke @f, %ret_buf
; mcopy NOP'd
%field_ptr = add %ret_buf, 32 ; DIFFERENT result (ret_buf != dst)
%val = mload %field_ptr ; reads from ret_buf+32 (correct content)
The mload still returns the correct value because ret_buf has the data. But %field_ptr now holds a different numeric value (ret_buf_base + 32 vs dst_base + 32). If %field_ptr were used in a non-memory context (e.g. returned, logged, or compared), the program would produce different observable output.
Affected passes
internal_return_copy_forwarding.py — _try_forward_internal_return_copy does not check that downstream uses of dst aliases are at memory-address operand positions
readonly_invoke_copy_forwarding.py — _try_forward_readonly_invoke_copy rewrites INVOKE operands; the callee may perform pointer arithmetic on the received parameter
Current safety
In practice, Vyper-generated code likely only uses alloca pointers for memory access, making this safe for current programs. But the pass does not verify this property, so it could miscompile hand-written or future IR patterns.
Suggested fix
Add a check in _try_forward_internal_return_copy that all downstream uses of dst aliases are at memory-address operand positions (position 0 of MLOAD/MSTORE/MCOPY/SHA3/LOG/RETURN/REVERT/etc.). Reject forwarding if any use computes on the pointer value.
For RICF, a similar check would need to verify the callee only uses the parameter for memory access (interprocedural).
Found during
Formal verification of Venom IR optimization passes in HOL4.
co-authored by claude opus 4.6
Summary
The
internal_return_copy_forwardingandreadonly_invoke_copy_forwardingpasses rewrite all downstream uses of a destination alloca alias to use the source alloca pointer instead. This is correct when all uses are memory accesses (MLOAD, MSTORE, etc.), because the forwarding preconditions guarantee the memory content at both pointers is identical. However, if any downstream use performs arithmetic on the pointer value itself (e.g.add %dst, 32for struct field access), the rewrite changes the computed value.Details
Consider:
After IRCF forwards:
The
mloadstill returns the correct value becauseret_bufhas the data. But%field_ptrnow holds a different numeric value (ret_buf_base + 32vsdst_base + 32). If%field_ptrwere used in a non-memory context (e.g. returned, logged, or compared), the program would produce different observable output.Affected passes
internal_return_copy_forwarding.py—_try_forward_internal_return_copydoes not check that downstream uses of dst aliases are at memory-address operand positionsreadonly_invoke_copy_forwarding.py—_try_forward_readonly_invoke_copyrewrites INVOKE operands; the callee may perform pointer arithmetic on the received parameterCurrent safety
In practice, Vyper-generated code likely only uses alloca pointers for memory access, making this safe for current programs. But the pass does not verify this property, so it could miscompile hand-written or future IR patterns.
Suggested fix
Add a check in
_try_forward_internal_return_copythat all downstream uses of dst aliases are at memory-address operand positions (position 0 of MLOAD/MSTORE/MCOPY/SHA3/LOG/RETURN/REVERT/etc.). Reject forwarding if any use computes on the pointer value.For RICF, a similar check would need to verify the callee only uses the parameter for memory access (interprocedural).
Found during
Formal verification of Venom IR optimization passes in HOL4.