(core rewrite) Mem2reg

[dc-mak]

This PR adds support for an analysis which determines which function-local variables don't have their addresses escaped and are sequentialisable (with respect to weak- and un-sequenced races), and a transform which replaces the create, store, load and kill actions on those variables with pure variable and expression rebindings instead.

Though each commit is self-contained, the code changed a lot during this process and so it's probably worth just reviewing it as a whole and squashing it rather than merging each commit (which can be kept for posterity). I'll write a proper commit message in the case of a squash.

[kmemarian]

why do you say that PEcall always returns a tuple?

[dc-mak]

(Off by one line?) My comment is slightly misleading because I was being too brief. I think I just want to say something like

• Propagating a call might duplicate a lot of work
• It may (but is not guaranteed) to return a tuple.

[dc-mak]

Although I did just realise, it's unsound to propagate error and UB and maybe even catch_exceptional_condition values since they need to be evaluated strictly.

[dc-mak]

#1006 I've fixed the copy-prop issues here

[kmemarian]

The function name and comment is misleading, it seems to collect all symbols (including with shadowing when symbol ids are reused in different scopes?). Even if (for now?) the caller doesn't care about variables bound in pexpr I'd rather have all binders properly handled here.

[kmemarian]

the same for action_escaping_syms with symbol bound in SeqRMW?

[kmemarian]

why isn't the first operand of Load0 (ctype of lvalue) used, unlike similar operands for Store0 and others?

[dc-mak]

That's an oversight, it should be used for completeness.

[kmemarian]

don't we care about expressions like let x = y in x?

[dc-mak]

copy_propagation will have taken care of it (let _ = unit in y)

[kmemarian]

Presumable the same happens when the Option.get fails?

[dc-mak]

Surprisingly, no. I was confused by this as well. I can try debug it if you want to get to the bottom of it.

[dc-mak]

So I asked Claude to investigate - at first it seemed reasonable, but then I asked it to provide a C source and then it realised that wasn't quite right. After it did a few experiments, it concluded at Pmap is not compiled with debug info, and that's the root cause.

First response, incorrect

Short version

Not_found is a constant (argument-less) exception constructor, so OCaml
allocates it once as a shared singleton. Every raise Not_found in the
entire program raises the same physical value. The runtime's backtrace buffer
only resets when the raised value is different from the last one it recorded —
so a fresh raise Not_found from your Pmap.find doesn't clear the stale trace
left over from parse-time Not_found raises.

Invalid_argument "option is None" carries a string payload → freshly allocated,
distinct value every time → buffer resets → correct location.

The mechanism in detail

The backtrace isn't attached to the exception value; it's a single per-domain
mutable buffer in the runtime. On a normal (trace-recording) raise, the unwinder
calls caml_stash_backtrace, which is roughly:

void caml_stash_backtrace(value exn, ...) {
  if (exn != Caml_state->backtrace_last_exn) {   /* physical comparison */
    Caml_state->backtrace_pos = 0;               /* reset only if different exn */
    caml_modify_..._root(&Caml_state->backtrace_last_exn, exn);
  }
  /* append frames as we unwind */
}

That exn != backtrace_last_exn guard exists so a genuine re-raise
(with e -> ... raise e) appends to the existing trace instead of clobbering
it. But it keys off physical identity of the exception value.

Now combine that with two facts confirmed in your tree:

1. parsers/c/c_lexer.mll:671 does try Hashtbl.find lexicon id with Not_found -> ...
   on every identifier — i.e. the lexer raises and catches Not_found
   constantly while parsing.
2. Stdlib.Hashtbl.find_rec (hashtbl.ml:536) and Pmap.find (lem's pmap.ml:81)
   both raise Not_found with a plain raise, not raise_notrace.

So the timeline is:

• During lexing, Hashtbl.find raises the Not_found singleton. It's a new
  value vs. whatever came before → buffer reset → records
  hashtbl.ml:536 / c_lexer.mll:671. backtrace_last_exn := Not_found. The
  lexer catches it; catching does not reset backtrace_last_exn.
• Long later, your Pmap.find in mem2reg raises Not_found — the same
  singleton. exn == backtrace_last_exn, so the buffer is not reset. You
  get the stale lexer location.

That's why the trace is both wrong and points at "the lexer of all places" —
that's just the last place a Not_found got a fresh recording.

With Pmap.lookup + Option.get, the internal Not_found is caught by
lookup's try ... with Not_found -> None, and the exception that actually
escapes is Invalid_argument "..." — a distinct, payload-carrying value →
buffer reset → clean mem2reg.ml:114.

Re: your hypothesis

It's not really about installing/removing try/with handlers (those only
determine where unwinding stops). The confusing backtrace comes from the global
buffer's reset condition interacting with constant-constructor sharing. Handlers
matter only insofar as the lexer's handler is what let that stale Not_found
trace survive to be reused.

Practical takeaways

• The current code (Option.get @@ Pmap.lookup ...) is the right call precisely
  for this reason — keep it. The comment is essentially correct, just slightly
  mis-attributes it to "a handler" rather than the shared-value buffer.
• If you ever want an informative trace and a useful message, raise a custom
  exception with a payload, e.g. exception Mem2reg_internal of string /
  ... of Symbol.sym. Because it's a distinct allocated value, it always resets
  the buffer and points at the real site.
• This is a general OCaml gotcha for any argument-less exception (Not_found,
  Exit, End_of_file, Stack_overflow): treat their backtraces with suspicion.

[dc-mak]

I've opened a PR on Lem, rems-project/lem#41 but for now I've figured out a slightly better work-around.

[kmemarian]

ok, tangentially why aren't you using Stdlib.Map here? We only have Pmap in the Lem generated code because it matches the typeclass codegen.

[dc-mak]

No particular reason tbh; I do the same in const-prop too. Want me to change it to Stdlib.Map?

[kmemarian]

pmap_find sym val_env fails when there is a declaration under an if, e.g.

int main(void)
{
  if (1) {
    int x;
  }
}

(the same if the declaration is in the else branch)

[dc-mak]

Good spot! Fixed in subsequent commits.

[kmemarian]

you asked me to remind you to investigate why locals inside a branch are still not leaking (despite block-scope kills)

[kmemarian]

don't look at the ctype_pe syms

[kmemarian]

same in later cases

[kmemarian]

can you add a related comment in the elaboration file

[dc-mak]

I addressed the comments and added a flag to enforce UB if strict_reads is enabled. I also added an analysis for checking for use-after-free errors.

Two things I need to do to tidy up the new commits:

• Remove/move the top-level C files
• Add some tests for the use-after-free analysis based on handwritten Core.