Mid-object pointer loses its offset across a non-inlined call, causing false valid-deref alarms (31 tasks, -496)

[leventeBajczi]

A mid-object pointer passed across a real (non-inlined) call boundary loses its offset, and the
callee's dereference checks then report a spurious valid-deref violation. This is the largest
wrong-verdict family in the latest full run: 31 of 68 wrong verdicts, worth −496 score.

Reproducer

// a mid-object heap pointer crossing a real (non-inlined, because recursive) call boundary
#include <stdlib.h>
void peek(char *p, int n) {
  if (n == 0) return;
  char c = *p;        // always within the 5-byte buffer
  (void)c;
  peek(p + 1, n - 1);
}
int main() {
  char *s = malloc(5);
  peek(s, 5);         // touches s[0..4] only
  free(s);
  return 0;
}

peek(s, 5) touches s[0..4] of a 5-byte buffer and never leaves it, yet:

--backend CEGAR -> (Property valid-deref) (SafetyResult Unsafe)

Isolation

The failure needs both pointer arithmetic and a call boundary — either alone is handled correctly:

variant	pointer arithmetic	call boundary	verdict	truth
reproducer above	yes	yes	Unsafe	SAFE
peek(p, n-1) — pointer never advances	no	yes	Safe	SAFE
same walk written as a loop in main	yes	no	Safe	SAFE

The call boundary has to be real: a non-recursive helper gets inlined and the problem disappears.
Recursion is simply the cheapest way to keep a call un-inlined, since InlineProceduresPass refuses
a procedure that transitively reaches recursion. The recursion bound is not involved — the false
alarm is identical at --force-unroll-recursion −1, 3, 10 and 20.

Confirmed on the real task termination-recursive-malloc/rec_strcopy_malloc (expected true,
reported false(valid-deref)): rewriting its recursive rec_strcopy_helper as an equivalent loop,
with everything else unchanged, flips the verdict from Unsafe to Safe.

Affected families in the last full run

31 tasks: termination-15 (14), ldv-memsafety (4), list-ext-properties (2), memsafety (2),
uthash-2.0.2 (2), termination-memory-alloca, termination-recursive-malloc, memsafety-ext3.

Relation to the split model

ReferenceElimination.seedSplitParams seeds a callee's split pointer parameter as
p_base := p; p_offset := 0, which presumes the caller passed a plain offset-0 pointer. For
address-taken locals that case is refused loudly (see
PointerArithmeticTest."passing a split pointer as a function argument is still refused"). The
reproducer above uses heap pointers, which do not go through the split path — so here the same
wrong premise produces a silent false alarm instead of an exception.

Scope

Not a regression against 7.3.0: these tasks were TIMEOUT or ERROR there, so the family predates the
8.x line. Filed out of #564, where it accounts for most of the remaining wrong verdicts.

[leventeBajczi]

Root cause: the multi model has nowhere to put the offset

The family is specific to --memory-model multi, which is the default
(XcfaConfig.effectiveMemoryModel falls back to multi, and no COMPLEX27 config overrides it).

On the reproducer:

--memory-model flat   -> (SafetyResult Safe)     correct
--memory-model multi  -> (SafetyResult Unsafe)   false alarm

FlatMemoryPass.flatBaseValue is the reason. Under flat an object base is minted as
id * FLAT_STRIDE, so each object owns a disjoint slice of one address line and a pointer is a
single scalar base + offset — the offset rides inside the value, and MemsafetyPass recovers the
base by truncating to the stride slice (the sizeKey/indexInObject computation already has this,
guarded by flatAddressing()).

Under multi the base is the bare id, so bases are consecutive small integers. base + 1 is
numerically the next object's base: a scalar pointer value simply has no room to carry a non-zero
offset. That is why the failure needs a real call boundary — passing the pointer by value is exactly
where the (base, offset) pair has to collapse to one scalar.

So this is not a missing guard in MemsafetyPass; the multi representation cannot express the value
being passed. The same premise is what ReferenceElimination.seedSplitParams encodes when it seeds a
callee parameter at offset 0.

Switching the default to flat is a candidate, but not free

Flat removes the unsoundness by construction, but on the affected tasks it did not simply become
correct locally — five *_alloca tasks under --memory-model flat with a single CEGAR config
(420 s) all timed out rather than false-alarming. Converting a wrong answer (−16) into a timeout (0)
is still worth +496 across the family, but flat may also lose currently-correct results elsewhere,
and the flat stride bounds both object size and object count.

That trade-off needs a cluster A/B (flat vs multi, full COMPLEX27) before changing the default —
worth doing, since flat is also reported to sidestep the multi-only split-variable crash.