[DRAFT] [pulse] forget pure unknown calls when the memory they read is written

[VladimirMakaev]

Pulse records ret = f(args) for unknown calls that havoc none of their arguments, such as const methods. The equality survived writes to that memory, so repeated calls had to agree and loops could not exit:

struct Queue {
  bool empty() const;
  void pop();
};

int drain_bad(Queue& q) {
  if (q.empty()) return 0;
  while (!q.empty()) q.pop();
  int* p = nullptr;
  return *p; // Infer missed: null dereference
}

In C-family languages, forget these equalities when a store, an unknown call or a callee writes memory reachable from their arguments. The heap is only walked when such equalities exist. Results computed on the entry state become f@pre(args), which callers equate with their own f calls. Arithmetic facts about the old results remain valid.

Summary compaction runs only on C-family summaries retaining an entry-state function application. It substitutes existing canonical linear definitions under explicit work and size checks, and retains the original integer-range atoms that define the tightest bounds. It preserves conditions, finite integer ranges and divisibility. Transformations requiring new equations, capped-coefficient overflow, or increased counted formula size are skipped.

Performance and limitations

This is partial compaction, not a universal summary-size bound or a guarantee of linear analysis time.

• A paired, three-run scaled-return test at depth 80 improved from median 18.47 to 3.07 user CPU seconds and from 670.1 to 343.6 MiB peak RSS, compared with the original PR.
• Zlib 1.3.1 was neutral: median total CPU 8.40 seconds for both the original PR and this version, with identical reports. The PR parent took 8.34 seconds. This is one project, not a corpus-wide result.
• In a 24-shape screen at depths 40/80/160, eight depth-160 candidate runs still reached the 30-second limit. Some smaller mixed-arithmetic cases are slower, and some depth-320 mixed cases use up to 27% more peak memory. Local compaction does not guarantee smaller aggregate summaries or cheaper caller analysis.
• Whole-object invalidation can decorrelate queries after an unrelated field write; an FP_ regression records this behavior.
• Hidden global dependencies of zero-argument queries remain unsupported; three FN_ regressions record direct writes, callee writes and unknown mutation.

The reproducible generator, complete measurements and implementation constraints are documented in the benchmark README. The remaining pathological cases are documented for review; this PR does not claim to satisfy a universal performance bound.

Validation

Passed locally:

• Native optimized build and OCaml @runtest, including caller-import checks for signed/unsigned bounds, mixed integer kinds, divisibility and actual definition elimination.
• c/pulse, cpp/pulse, and cpp/pulse-11, including the existing drain-loop and correlation regressions. Existing reports and traces are unchanged; expectations add the reports from the new regression files.
• OCaml formatting, diff checks and benchmark Python compilation.
• Synthetic before/after measurements and the zlib comparison described above.

ObjC/ObjC++ validation with the Xcode SDK and integration measurements stacked with #2158, #2176, #2178 and #2197 remain outstanding. The review's #2202-before-#2177 landing order is unchanged. This PR remains a draft.