Take a ptrace stop where the registers are real

Merged
JS
2mo ago
+1626-110

A PTRACE_INTERRUPT that lands while the tracee is at EL1 inside a shim fast
path stops there, which snapshots shim scratch as the guest's registers and
discards whatever the tracer writes back once the shim restores its own frame.
The host now routes the stop through X7 and HVC #13 so the frame is restored
first, and takes it inline on the two tails that have already rebuilt EL0
state.

Reproduction, before the first commit:

make check
tests/test-ptrace-interrupt.c reports a PC above EL0_PC_CEILING

The branch also carries verification and harness work that came out of
validating the above, and can be split off if that reads better as its own
PR: two Hypervisor stub constants disagreed with the SDK
(HV_EXIT_REASON_CANCELED read 1 where the SDK enumerates 0), the gate that
should have caught them could not see enumerator values, four new stubs bring
syscall/proc.c and syscall/sys.c into the parsing set, and nslookup now skips
rather than fails when the host itself cannot resolve.

Summary by cubic

Fixes PTRACE_INTERRUPT stops taken while the tracee sits inside a shim fast path: they used to snapshot shim scratch as the guest's registers and discard the tracer's writes. Stops are now routed through X7 on the HVC #5 return and HVC #13, so the shim restores its saved SVC frame first; the two tails that rebuild EL0 state stop inline, and an execve re-entry leaves the stop owed for the new image.

Bug fixes

  • An unarmed HVC #13 is now a crash report instead of a thread parked forever.
  • A new check-svc-tails gate holds every HVC #5 tail to the X7 test, with exec_drop_frame as the sole documented exception.

Verification and harness

  • check-stub-constants.py now checks enumerator values by compiling against the SDK, catching HV_EXIT_REASON_CANCELED at 1 where the SDK enumerates 0.
  • New Frama-C stubs (sys/resource.h, libproc.h, sys/sysctl.h, mach/mach.h) bring syscall/proc.c and syscall/sys.c into the parsing set.
  • check-wp-result.py reports prover timeouts and cached verdicts distinctly from real open goals.
  • make indent runs shfmt and black only with FORMAT_SHELL=1 / FORMAT_PY=1.
  • nslookup skips rather than fails when the host resolver cannot reach DNS.
  • test-ptrace-interrupt signals itself so kicks land on the rt_sigreturn tail, and verifies SETREGSET writes survive PTRACE_CONT.
  • test-signal checks X7 survives signal delivery and rt_sigreturn.