IRGen: fix EnumConstantDecl miscompile + verifier; symex: structural Concat fold for byte shadows

[pgoodman]

Summary

Two adjacent fixes:

1. IRGen miscompile: DeclRefExpr to an EnumConstantDecl was routed
   through EmitRValue's lvalue fallback, then through EmitLValue's
   local-VarDecl fallback, which silently operator[]-inserted into
   object_to_alloca_ and returned 0 — the entry IMPLICIT_GOTO's slot.
   The resulting MEMORY/LOAD_LE_* [%term] reads address 0x0 at runtime
   with no codegen-time diagnostic. Now lowered to CONST directly, with
   choke-point CHECKs and a post-pass VerifyIR to make a future
   recurrence abort with a live stack.

2. Symex shadow expression bloat: z3.simplify on multi-byte load
   Concats folds the low byte through byte arithmetic asymmetrically (the
   low byte has no incoming borrow; the high bytes do). For len -= p[1]
   with len = 1492, the round-trip yielded
   Concat(Extract(31, 8, X), 212 + 255*b) instead of 1492 - zext_32(b),
   destroying parent identity for downstream loads. Replaced with a
   targeted structural Concat-of-consecutive-Extracts fold.

IRGen changes (bin/Index/IRGen.{cpp,h})

• EmitRValue: handle EnumConstantDecl before the lvalue fallback,
  emitting CONST with the enumerator's APSInt value via
  pasta::EnumConstantDecl::InitializerValue().
• EmitLValue DeclRefExpr arm: explicit decl-kind enumeration; CHECK
  on unknown kinds or missing ALLOCA registration.
• EmitInstruction choke-point CHECK: no non-terminator opcode may
  consume a terminator instruction as a value operand. Aborts at the
  codegen origin, not post-mortem.
• EmitLoadFromLValue: same check at the lvalue site for a tighter stack.
• Generate() parameter ALLOCAs: try_emplace + CHECK(inserted) traps
  duplicate registration.
• New VerifyIR() post-pass after ComputeRPO in both Generate and
  GenerateGlobalInit. LOG(ERROR) (not fatal) for: operand references a
  terminator/scope marker, MEMORY load/store operand-count mismatch,
  SWITCH default to slot 0, missing parent_structure_index. Partial IR
  survives for investigation.

Symex changes (bindings/Python/symex/dispatch.py)

• New _z3_concat_fold(z3, expr) helper. Flattens nested binary Concats
  (z3's internal storage), merges adjacent same-parent Extract ranges,
  collapses a full-width single Extract to its parent. Pure structural
  rewrite — never folds Extract through arithmetic.
• _shadow_write and _shadow_read now call _z3_concat_fold instead of
  z3.simplify. Multi-byte round trips recover the parent expression.

Tests

• tests/symex/c/symex_integration.c: new EnumConstantDecl regression
  corpus (aggregate init, scalar return, comparison, function argument).
• tests/symex/test_irgen_decl_ref.py (8 tests, all green).
• tests/symex/test_concat_fold.py (6 tests, all green) — direct fold
  rules, full-width round trip, partial-overwrite preserving minimal
  Concat, plus an explicit assertion that z3.simplify can't recover
  the parent (so the structural fold is load-bearing).

Test results

• InterpretIR: 35/36 (1 pre-existing failure on main, unrelated).
• Symex: 235/236 (1 pre-existing failure on main, unrelated).
• All 14 new tests pass.

Test plan

• InterpretIR full suite passes (modulo pre-existing failure).
• Symex full suite passes (modulo pre-existing failure).
• New regression tests fail without the IRGen fix (verified by stash).
• New concat-fold tests demonstrate the asymmetric z3.simplify issue
  and that the structural fold recovers parent identity.
• Re-index a representative corpus and confirm VerifyIR emits no
  LOG(ERROR) lines on clean IR.

🤖 Generated with Claude Code