[FIX] Stop taking Z3 unknown for in bounds in the eager sanitizer

[mark14wu]

Summary

The eager sanitizer only reported on sat (sanitizer.py:441, if solver.check() != sat: return), so a query Z3 answered unknown passed as "no out-of-bounds access". The compiled sanitizer already treats unknown as unchecked (decision D11); this PR does the same on the eager side.

Two ways this showed up:

• Z3 gives up (resource limit, incomplete theory): a genuinely out-of-bounds kernel produced records == [] and exit status 0, with or without abort_on_error.
• Ctrl+C during a query: Z3 catches the SIGINT itself and returns unknown with reason "interrupted from keyboard". Python never sees a KeyboardInterrupt, so the check passed silently and the kernel kept running.

What changes:

• An unknown answer creates a new UndecidedAccessRecordZ3 in sanitizer/data.py. It holds the op type, the resolved tensor and its arg name, the source location, and Z3's reason_unknown(). There is no witness address.
  • Without abort_on_error, the record goes into sanitizer.records, so a caller checking not san.records is no longer misled.
  • With abort_on_error, print_undecided_record prints an UNCHECKED MEMORY ACCESS warning and the program keeps running. An undecided access is not a finding, which matches the compiled side, where unknown means unsupported rather than a violation.
• A Ctrl+C that Z3 caught is raised again as KeyboardInterrupt.

Notes for reviewers:

• No timeout added. The persistent eager solver still has no per-solver timeout (the other half of D11). In practice, eager unknown today comes from a Ctrl+C or a resource limit; a hard query hangs instead of returning unknown. Adding a timeout would turn slow queries into "unchecked", so it is left as a separate decision.
• Conflict with the compiled-sanitizer PR stack. UndecidedAccessRecordZ3 is appended at the end of sanitizer/data.py, where the compiled-sanitizer stack also appends CompiledSanitizerRecord. Rebasing that stack onto this PR will hit a small both-sides-added conflict there; keep both.

Test Plan

• New end-to-end tests in tests/end_to_end/test_sanitizer.py. Each makes Z3 answer unknown deterministically: setting rlimit=1 on the solver stands in for any query Z3 gives up on, independent of machine speed.
  • test_solver_unknown_records_access_as_unchecked: an out-of-bounds load plus a deferred in-loop store both become UndecidedAccessRecordZ3, with the right op type, tensor arg and source line.
  • test_solver_unknown_warns_without_aborting: with abort_on_error=True, the warning is printed and there is no SystemExit.
  • test_solver_interrupted_by_ctrl_c_raises_keyboard_interrupt: a Ctrl+C reason raises KeyboardInterrupt.
• All three tests fail on main's sanitizer and pass with this change. Command: pytest tests/end_to_end/test_sanitizer.py -k solver_.
• pre-commit passes (ruff, ruff-format, mypy).
• The rest of the suite was not run locally; that is left to CI.

Related Issues

Follow-up to D11 of the compiled-sanitizer work, which fixed only the compiled side.

Breaking Changes

• SymbolicSanitizer.records can now also contain UndecidedAccessRecordZ3 entries, not only OutOfBoundsRecordZ3.
• With abort_on_error=True, an undecided access now prints a warning. The exit status is unchanged (0).
• A Ctrl+C during a Z3 query now interrupts the program instead of being swallowed.

Checklist

• I added tests to all new functionality I added/bugs I fixed.
• I verified that a human has reviewed all code in this PR.
• I ran npm run build:frontend if the PR modified any TypeScript code. (N/A: no TypeScript changes)
• I made sure that my code is well documented (comments explaining strange code, docstrings for functions, website modified if new functionality added).

[github-actions]

Performance Benchmark

Benchmark	main (min)	PR (min)	Change	Samples
gemm	0.105s	0.105s	-0.1%	20 / 20
gemm_oob	0.117s	0.117s	-0.2%	20 / 20
indirect_load	0.022s	0.022s	+0.5%	20 / 20
nested_loop	0.235s	0.236s	+0.2%	20 / 20
block_pointer_loop_advance	0.125s	0.125s	+0.1%	20 / 20
liger_jsd	0.139s	0.139s	+0.0%	20 / 20
flaggems_layernorm	0.395s	0.396s	+0.3%	20 / 20
swiglu	0.170s	0.171s	+0.5%	20 / 20
cross_entropy	0.976s	0.978s	+0.2%	20 / 20
fused_linear_jsd	0.209s	0.210s	+0.5%	20 / 20
Total	2.491s	2.497s	+0.2%	N/A

Iterations: 1 warmup + 20 measured
Samples are shown as main / PR; long pytest benchmarks may use fewer samples.