navicore/patch-seq

Fork 0

phantom stack entries #169

New issue

Closed

opened 2026-01-03 15:27:25 +00:00 by navicore · 2 comments

navicore commented

2026-01-03 15:27:25 +00:00

(Migrated from github.com)

when in the repl, no error is thrown when the repl has 2 stack entries and rot is called.

if the stack has (3 4) and rot is called a 0 is infered and the stack is now (4 0).

if rot is called again the stack becomes (0 3).

if rot is called again the stack becomes (3 4) again.

Is this correct behavior?
is the repl show / display processing correct? the stack deptth of 2 never changed despite rot operates on 3 depth and the display shows the program knew about the stack values that dropped off the stack... that the stack seems to be keeping values that are not displayed. This behavior feels like a bug machine. Lets discuss before implementing any changes.

@claude fyi

when in the repl, no error is thrown when the repl has 2 stack entries and rot is called. if the stack has (3 4) and rot is called a 0 is infered and the stack is now (4 0). if rot is called again the stack becomes (0 3). if rot is called again the stack becomes (3 4) again. 1. Is this correct behavior? 2. is the repl show / display processing correct? the stack deptth of 2 never changed despite rot operates on 3 depth and the display shows the program knew about the stack values that dropped off the stack... that the stack seems to be keeping values that are not displayed. This behavior feels like a bug machine. Lets discuss before implementing any changes. @claude fyi

claude[bot] commented

2026-01-03 15:27:38 +00:00

(Migrated from github.com)

Claude finished @navicore's task in 3m 57s —— View job

Analysis of phantom stack entries

I've thoroughly analyzed this issue and identified two distinct bugs that work together to create the phantom stack behavior.

The Bugs

Bug #1: Type Checker Allows Insufficient Stack Depth ❌

Expected behavior: The type checker should reject rot when there are fewer than 3 values on the stack.

What's happening:

rot has signature ( a T U V -- a U V T ) in crates/compiler/src/builtins.rs:364
This requires at least 3 stack values (T, U, V), with an optional row variable prefix
When the stack has only 2 values (3 4), the type checker should fail during unification
Current stack: Empty ← Int ← Int (2 values)
Expected input: a ← T ← U ← V (row variable + 3 values)
The unifier in crates/compiler/src/unification.rs:238-293 should detect this mismatch and reject it

The type checker is failing to catch this error, allowing code to compile that will access invalid stack positions.

Bug #2: Runtime Accesses Uninitialized Stack Memory 💣

The "phantom stack entries" are actually undefined behavior from reading uninitialized memory.

Looking at crates/runtime/src/stack.rs:653-671:

pub unsafe extern "C" fn patch_seq_rot(stack: Stack) -> Stack {
    unsafe {
        let ptr_c = stack.sub(1);  // Top of stack
        let ptr_b = stack.sub(2);  // Second item
        let ptr_a = stack.sub(3);  // Third item - MAY NOT EXIST!
        let a = *ptr_a;  // ⚠️ Reads potentially uninitialized memory
        let b = *ptr_b;
        let c = *ptr_c;
        *ptr_a = b;
        *ptr_b = c;
        *ptr_c = a;
        stack
    }
}

There are NO bounds checks. When you call rot with only 2 stack items:

ptr_a points to uninitialized stack memory below the logical stack base
*ptr_a reads whatever garbage value happens to be there
The operation writes back to that invalid location

Why you see a 0: The stack buffer is likely zero-initialized when allocated, so uninitialized positions contain StackValue { slot0: 0, slot1: 0, ... } which represents Int(0).

The cycling behavior: Each rot operation rotates 3 positions, including the garbage value:

Start: (3 4) + garbage 0 at position -3
After 1st rot: garbage rotates to position -2 → (4 0)
After 2nd rot: the 3 rotates from position -3 → (0 3)
After 3rd rot: back to (3 4) at positions -2 and -1

Answers to Your Questions

Is this correct behavior?

No. This is undefined behavior caused by insufficient type checking and lack of runtime bounds validation. The program should be rejected at compile time.

Is the repl show/display processing correct?

Yes, the display is correct. It shows exactly what exists on the logical stack (2 values). The "phantom" values you observe during rotation are uninitialized memory being illegally accessed by rot. The stack depth never actually changes - you're seeing the same 2 positions being rotated with garbage data from below the stack base.

Recommendations

This is definitely a bug. Here's what should happen:

Primary Fix: Improve Type Checking (Compile-Time Safety)

The type checker should reject operations that access more stack positions than available:

When checking effects like ( a T U V -- a U V T ), extract minimum required depth (3 values)
Verify the current stack has at least that many concrete values beyond any row variables
Reject at compile time with a clear error: "rot requires 3 stack values, but only 2 are available"

Location: crates/compiler/src/typechecker.rs in the apply_effect method around line 1029.

Optional: Runtime Bounds Checking (Defense-in-Depth)

Add runtime assertions for debugging/safety:

Track stack base pointer (already exists via get_stack_base())
In patch_seq_rot, verify stack - 3 >= base before accessing
Panic with clear error if violated

This has performance implications but would catch bugs that slip through type checking.

Next Steps

Before implementing fixes:

Create a minimal test case to reproduce and verify the bug
Investigate why type checking fails - trace through the unification logic
Decide on fix approach:
- Type checker improvements (necessary)
- Runtime bounds checking (optional, for robustness)
- Debug mode with stricter validation

Would you like me to:

Investigate the type checker more deeply to find why it's not catching this?
Implement a fix with tests?
Create a minimal reproduction case?

Let me know how you'd like to proceed!

**Claude finished @navicore's task in 3m 57s** —— [View job](https://github.com/navicore/patch-seq/actions/runs/20679224918) --- ### Analysis of phantom stack entries I've thoroughly analyzed this issue and identified **two distinct bugs** that work together to create the phantom stack behavior. --- ### The Bugs #### Bug #1: Type Checker Allows Insufficient Stack Depth ❌ **Expected behavior:** The type checker should reject `rot` when there are fewer than 3 values on the stack. **What's happening:** - `rot` has signature `( a T U V -- a U V T )` in `crates/compiler/src/builtins.rs:364` - This requires at least 3 stack values (T, U, V), with an optional row variable prefix - When the stack has only 2 values `(3 4)`, the type checker should fail during unification - Current stack: `Empty ← Int ← Int` (2 values) - Expected input: `a ← T ← U ← V` (row variable + 3 values) - The unifier in `crates/compiler/src/unification.rs:238-293` should detect this mismatch and reject it **The type checker is failing to catch this error**, allowing code to compile that will access invalid stack positions. #### Bug #2: Runtime Accesses Uninitialized Stack Memory 💣 **The "phantom stack entries"** are actually **undefined behavior** from reading uninitialized memory. Looking at `crates/runtime/src/stack.rs:653-671`: ```rust pub unsafe extern "C" fn patch_seq_rot(stack: Stack) -> Stack { unsafe { let ptr_c = stack.sub(1); // Top of stack let ptr_b = stack.sub(2); // Second item let ptr_a = stack.sub(3); // Third item - MAY NOT EXIST! let a = *ptr_a; // ⚠️ Reads potentially uninitialized memory let b = *ptr_b; let c = *ptr_c; *ptr_a = b; *ptr_b = c; *ptr_c = a; stack } } ``` **There are NO bounds checks.** When you call `rot` with only 2 stack items: - `ptr_a` points to uninitialized stack memory below the logical stack base - `*ptr_a` reads whatever garbage value happens to be there - The operation writes back to that invalid location **Why you see a 0:** The stack buffer is likely zero-initialized when allocated, so uninitialized positions contain `StackValue { slot0: 0, slot1: 0, ... }` which represents `Int(0)`. **The cycling behavior:** Each `rot` operation rotates 3 positions, including the garbage value: - Start: `(3 4)` + garbage 0 at position -3 - After 1st `rot`: garbage rotates to position -2 → `(4 0)` - After 2nd `rot`: the 3 rotates from position -3 → `(0 3)` - After 3rd `rot`: back to `(3 4)` at positions -2 and -1 --- ### Answers to Your Questions > 1. Is this correct behavior? **No.** This is undefined behavior caused by insufficient type checking and lack of runtime bounds validation. The program should be rejected at compile time. > 2. Is the repl show/display processing correct? **Yes, the display is correct.** It shows exactly what exists on the logical stack (2 values). The "phantom" values you observe during rotation are uninitialized memory being illegally accessed by `rot`. The stack depth never actually changes - you're seeing the same 2 positions being rotated with garbage data from below the stack base. --- ### Recommendations This is **definitely a bug**. Here's what should happen: #### Primary Fix: Improve Type Checking (Compile-Time Safety) The type checker should reject operations that access more stack positions than available: 1. When checking effects like `( a T U V -- a U V T )`, extract minimum required depth (3 values) 2. Verify the current stack has at least that many concrete values beyond any row variables 3. **Reject at compile time** with a clear error: "rot requires 3 stack values, but only 2 are available" Location: `crates/compiler/src/typechecker.rs` in the `apply_effect` method around line 1029. #### Optional: Runtime Bounds Checking (Defense-in-Depth) Add runtime assertions for debugging/safety: - Track stack base pointer (already exists via `get_stack_base()`) - In `patch_seq_rot`, verify `stack - 3 >= base` before accessing - Panic with clear error if violated This has performance implications but would catch bugs that slip through type checking. --- ### Next Steps Before implementing fixes: 1. **Create a minimal test case** to reproduce and verify the bug 2. **Investigate why type checking fails** - trace through the unification logic 3. **Decide on fix approach**: - Type checker improvements (necessary) - Runtime bounds checking (optional, for robustness) - Debug mode with stricter validation Would you like me to: - Investigate the type checker more deeply to find why it's not catching this? - Implement a fix with tests? - Create a minimal reproduction case? Let me know how you'd like to proceed! ---

navicore commented

2026-01-03 22:03:51 +00:00

(Migrated from github.com)

https://github.com/navicore/patch-seq/pull/170