MODREACH: a modification of a call result that is part of a parameter leaves the parameter unmodified (#80's other half) #98

Under MODREACH (the CLI's default), a method that modifies a call's result is non-modifying for its parameter when that result is a field of the parameter, or of an object reachable from it. The default mode (fixpoint) calls the same parameter modified. This is the MODREACH side of #80: the link engine has carried the modification since #80, but the reachability pass re-derives the parameter from the statements and loses it.

Shape

From TestCallResultFieldOfReceiver (link module):

static class Node {
    Wrapper wrapper; int type; Node parent;
    Wrapper getWrapper() { Node node = this; while (node.type == 1) node = node.parent; return node.wrapper; }
}
static void viaLoop(Node parent)      { Wrapper w = parent.getWrapper(); w.x = 1; }
static void viaLocalCall(Node parent) { Wrapper w = parent.getWrapper(); w.set(1); }
static void viaGetter(N2 parent)      { parent.getWrapper().getH().list.clear(); }

Cause

Two gaps in ShadowModificationPass.project:

1. A local holding the result is linked to the receiver by w ≺ 0:parent (kept as genuine containment since Modification through a call result that is a field of the receiver (≺) does not reach the receiver #80), but the walk follows a local only through assigned-from links.
2. A field whose scope is a call (parent.getWrapper().getH().list) projects the field and stops; MODREACH: assigning a field of a call's result (requireNonNull(tail).next = x) leaves the method non-modifying #71 added the receiver chain for an assignment target only, not for a receiver or argument.

How it was found

The rust-llvm experiment (#167 in maddi): rustc rejected via_loop(parent: &CNode), via_local_call and via_getter writing through a shared borrow.

To do

• Follow a local's real ≺ links to the container in project, and project the receiver chain of a field whose scope is an expression.
• Test both modes on the shapes above (TestShadowCallResultFieldOfReceiver).

viaElement (an element of a list on the result, held in a local) stays the known gap pinned in TestCallResultFieldOfReceiver.deeper, in both modes.

🤖 Generated with Claude Code