[BUG] Frame checker retains unproved frame-pointer values across calls and syscalls #8

New issue

Closed

opened 2026-09-16 05:33:21 +02:00 by erikinkinen · 0 comments

erikinkinen commented

2026-09-16 05:33:21 +02:00

Owner

Summary

The cleanup frame checker retains its stack-derived frame-pointer fact across ordinary calls and syscalls without proving that rbp survives. A later mov %rbp,%rsp can therefore report a complete local frame using a stale value. This is a checker defect; the full frame/source gate already remains incomplete, and no accepted guest build is established by these results.

Reproduction

At Exsh 12331e26f3bb7a25c0146c8b314eef46dd451099, analyze literal x86-64 bodies in an original ELF fixture. The caller executes push %rbp; mov %rsp,%rbp; sub $0x20,%rsp; call helper; mov %rbp,%rsp; pop %rbp; ret. Give the helper xor %ebp,%ebp; ret. Also test a helper containing an unknown register call or syscall, and a syscall directly in the caller before restoration. The two regression tests contain four negative assertions, all reproducible against the original published checker source in an isolated interpreter.

Expected and actual behavior

Expected: each negative case discards the saved frame-pointer fact and refuses restoration from unknown rbp. A separately proved untouched callee may retain an existing fact.

Actual: all four negative cases report the caller's local frame as complete. Ordinary GP target facts were already discarded across calls, but the separate stack-derived rbp state survived. Direct syscall handling has the same omission.

Environment and identity

Original published Exsh revision above, Linux x86-64 host, Python warning-denied fixture tests. The regression uses independently specified machine bytes and original ELF metadata; no target binary or guest executes. This is a static-analysis defect, without an observed runtime regression or a last-known-good revision.

Evidence and prior checks

The exact original stack module was captured from the signed revision and its digest retained with the test status. Two tests execute with four expected failures before correction; the original positive untouched-callee control still passes. Full source membership, direct-versus-nested classification, native closure and in-EriX builds remain separate open obligations.

Grounded call-preservation checkpoint — 16 September 2026: signed Exsh 641ac2fc7c3fba3ab351f2863df7e35117b2732a and Docs 7a7c3ff0095de8f008c9b534fd993554df37f976 are pushed on feature/posix-compat. Complete original bodies and earlier callee facts now prove never-written register families. Only existing typed values survive proved calls; live conditions clear. The separate stack-derived rbp fact follows the same rule. This corrects the reproduced stale-frame defect, which stays open pending matching CI. ABI conventions, spill restoration and current kernel behavior supply no preservation mask.

All 213 clean-environment checker tests pass, including 21 new controls, eleven isolated module imports and a 1,200-function grounded dependency chain. All six strict Rust feature/profile configurations pass 961 tests each, with host/native Clippy, private rustdoc and six native builds; no warnings. Original runtime/all artifact pairs retain 65/72 protected register edges and 70/77 load origins, reducing unresolved observations from 156/124 to 107/70. Both workspace mappings pass; full source/frame/direct gates retain actual exit 1. Independent audits bind 7,795/7,503 used-contract instructions and complete earlier-proof closure to the original captured bytes.

Profiling identified unnecessary empty-state scans and rejected-body suffix work. Removing them preserves every paired report decision and reduces total profiled Python calls from 32,160,478 to 26,673,252 and from 30,880,221 to 25,402,446. Single paired timings include observer overhead; they do not establish statistical or guest performance. Original timer, byte and stack budgets remain unchanged.

All 45 Docs tests, formatting, Markdown and canonical checks pass. The 2,379-page manual has 436,058 in-bounds word boxes, zero final warnings and visual review of both changed pages. The physical audit covers 3,693 source/configuration files, all below 1,000 lines. Semantic authority/private-documentation closure, product adoption, complete source/frame admission, runnable realms and both full in-EriX build generations remain open. Automatic CI for both exact signed heads is being followed; local passes are not reported as CI acceptance.

Matching preservation CI — 16 September 2026: Exsh 249 and 250 are fully classified at 641ac2fc7c3fba3ab351f2863df7e35117b2732a. Both pass all 213 checker tests, including eleven isolated imports and the stale-frame controls, all 961 Rust tests and preceding strict host/native Clippy, rustdoc and native build stages. Markdown and all four workspace mappings per run pass. The remaining full frame gate fails as required; original CI artifact observations are 111, 111, 74, 74], [111, 111, 74, 74. All four complete logs total 314,995 bytes without warnings. The independently retained local pairs remain 107/70, with their own original identities.

Docs 909 and 910 pass at 7a7c3ff0095de8f008c9b534fd993554df37f976. All four complete logs total 763,088 bytes; both manual jobs pass 45 tests and render 2,379 pages with zero final warnings after ordinary reference convergence. The corrected frame-pointer issue is closed on this matching evidence; the full source/frame issue remains open. No full confined build, runnable realm or coherent product-catalog adoption is established.

Tracking

Related to frame evidence, shell work and implementation review. Use instruction-derived callee preservation for the stack-derived frame pointer, share explicit/implicit register-family invalidation, and discard it on unknown syscall effects. Keep the before-fix reproduction, validate positive and negative controls plus the original artifact pair, then classify matching signed-source CI before closing this issue.

## Summary The cleanup frame checker retains its stack-derived frame-pointer fact across ordinary calls and syscalls without proving that rbp survives. A later `mov %rbp,%rsp` can therefore report a complete local frame using a stale value. This is a checker defect; the full frame/source gate already remains incomplete, and no accepted guest build is established by these results. ## Reproduction At Exsh `12331e26f3bb7a25c0146c8b314eef46dd451099`, analyze literal x86-64 bodies in an original ELF fixture. The caller executes `push %rbp; mov %rsp,%rbp; sub $0x20,%rsp; call helper; mov %rbp,%rsp; pop %rbp; ret`. Give the helper `xor %ebp,%ebp; ret`. Also test a helper containing an unknown register call or syscall, and a syscall directly in the caller before restoration. The two regression tests contain four negative assertions, all reproducible against the original published checker source in an isolated interpreter. ## Expected and actual behavior Expected: each negative case discards the saved frame-pointer fact and refuses restoration from unknown rbp. A separately proved untouched callee may retain an existing fact. Actual: all four negative cases report the caller's local frame as complete. Ordinary GP target facts were already discarded across calls, but the separate stack-derived rbp state survived. Direct syscall handling has the same omission. ## Environment and identity Original published Exsh revision above, Linux x86-64 host, Python warning-denied fixture tests. The regression uses independently specified machine bytes and original ELF metadata; no target binary or guest executes. This is a static-analysis defect, without an observed runtime regression or a last-known-good revision. ## Evidence and prior checks The exact original stack module was captured from the signed revision and its digest retained with the test status. Two tests execute with four expected failures before correction; the original positive untouched-callee control still passes. Full source membership, direct-versus-nested classification, native closure and in-EriX builds remain separate open obligations. Grounded call-preservation checkpoint — 16 September 2026: signed Exsh `641ac2fc7c3fba3ab351f2863df7e35117b2732a` and Docs `7a7c3ff0095de8f008c9b534fd993554df37f976` are pushed on `feature/posix-compat`. Complete original bodies and earlier callee facts now prove never-written register families. Only existing typed values survive proved calls; live conditions clear. The separate stack-derived rbp fact follows the same rule. This corrects [the reproduced stale-frame defect](https://git.erikinkinen.fi/erix/exsh/issues/8), which stays open pending matching CI. ABI conventions, spill restoration and current kernel behavior supply no preservation mask. All 213 clean-environment checker tests pass, including 21 new controls, eleven isolated module imports and a 1,200-function grounded dependency chain. All six strict Rust feature/profile configurations pass 961 tests each, with host/native Clippy, private rustdoc and six native builds; no warnings. Original runtime/all artifact pairs retain 65/72 protected register edges and 70/77 load origins, reducing unresolved observations from 156/124 to 107/70. Both workspace mappings pass; full source/frame/direct gates retain actual exit 1. Independent audits bind 7,795/7,503 used-contract instructions and complete earlier-proof closure to the original captured bytes. Profiling identified unnecessary empty-state scans and rejected-body suffix work. Removing them preserves every paired report decision and reduces total profiled Python calls from 32,160,478 to 26,673,252 and from 30,880,221 to 25,402,446. Single paired timings include observer overhead; they do not establish statistical or guest performance. Original timer, byte and stack budgets remain unchanged. All 45 Docs tests, formatting, Markdown and canonical checks pass. The 2,379-page manual has 436,058 in-bounds word boxes, zero final warnings and visual review of both changed pages. The physical audit covers 3,693 source/configuration files, all below 1,000 lines. Semantic authority/private-documentation closure, product adoption, complete source/frame admission, runnable realms and both full in-EriX build generations remain open. Automatic CI for both exact signed heads is being followed; local passes are not reported as CI acceptance. Matching preservation CI — 16 September 2026: [Exsh 249](https://git.erikinkinen.fi/erix/exsh/actions/runs/249) and [250](https://git.erikinkinen.fi/erix/exsh/actions/runs/250) are fully classified at `641ac2fc7c3fba3ab351f2863df7e35117b2732a`. Both pass all 213 checker tests, including eleven isolated imports and the stale-frame controls, all 961 Rust tests and preceding strict host/native Clippy, rustdoc and native build stages. Markdown and all four workspace mappings per run pass. The remaining full frame gate fails as required; original CI artifact observations are [[111, 111, 74, 74], [111, 111, 74, 74]]. All four complete logs total 314,995 bytes without warnings. The independently retained local pairs remain 107/70, with their own original identities. [Docs 909](https://git.erikinkinen.fi/erix/docs/actions/runs/909) and [910](https://git.erikinkinen.fi/erix/docs/actions/runs/910) pass at `7a7c3ff0095de8f008c9b534fd993554df37f976`. All four complete logs total 763,088 bytes; both manual jobs pass 45 tests and render 2,379 pages with zero final warnings after ordinary reference convergence. The corrected frame-pointer issue is closed on this matching evidence; the full source/frame issue remains open. No full confined build, runnable realm or coherent product-catalog adoption is established. ## Tracking Related to [frame evidence](https://git.erikinkinen.fi/erix/exsh/issues/4), [shell work](https://git.erikinkinen.fi/erix/exsh/issues/2) and [implementation review](https://git.erikinkinen.fi/erix/exsh/pulls/3). Use instruction-derived callee preservation for the stack-derived frame pointer, share explicit/implicit register-family invalidation, and discard it on unknown syscall effects. Keep the before-fix reproduction, validate positive and negative controls plus the original artifact pair, then classify matching signed-source CI before closing this issue.

erikinkinen added the

bug

phase-6

labels

2026-09-16 05:33:21 +02:00

erikinkinen referenced this issue

2026-09-16 05:46:49 +02:00

[FEATURE] Audit authority, code quality and documentation in exsh #2

erikinkinen referenced this issue

2026-09-16 05:46:50 +02:00

[BUG] Exsh stack proof assumes incidental optimized symbol names #4

erikinkinen referenced this issue from erix/docs