Skip to content

Add support for accessing single-element aggregates in #traverseProjection #657

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Aug 25, 2025
+68 −1
Merged

Add support for accessing single-element aggregates in #traverseProjection #657

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c443686
Update .gitignore to include .DS_Store and proof/ directory
Stevengre Aug 20, 2025
ef8ea24
Add support for accessing single-element aggregates in #traverseProje…
Stevengre Aug 21, 2025
0f1346e
Enhance documentation for single-element aggregate handling in #trave…
Stevengre Aug 25, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,4 +4,5 @@ __pycache__/
/deps/.stable-mir-json
/.vscode/
kmir/src/tests/integration/data/**/target
.DS_Store
.DS_Store
proof/
24 changes: 24 additions & 0 deletions kmir/src/kmir/kdist/mir-semantics/rt/data.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -418,6 +418,30 @@ This is done without consideration of the validity of the Downcast[^downcast].
</k>
```

If an Aggregate contains only one element and #traverseProjection becomes stuck, you can directly access this element.

Without this rule, the test `closure_access_struct-fail.rs` demonstrates the following behavior:
- The execution gets stuck after 192 steps at `#traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( ... ) ) , ... )`
- The stuck state occurs because there's a Deref projection that needs to be applied to the single element of this Aggregate, but the existing Deref rules only handle pointers and references, not Aggregates

With this rule enabled:
- The execution progresses further to 277 steps before getting stuck
- It gets stuck at a different location: `#traverseProjection ( toLocal ( 19 ) , thunk ( #decodeConstant ( constantKindAll ... ) ) , ... )`
- The rule automatically unwraps the single-element Aggregate, allowing the field access to proceed

This rule is essential for handling closures that access struct fields, as MIR represents certain struct accesses through single-element Aggregates that need to be unwrapped.

```k
rule <k> #traverseProjection(
DEST,
Aggregate(_, ARGS),
PROJS,
CTXTS
)
=> #traverseProjection(DEST, getValue(ARGS, 0), PROJS, CTXTS) ... </k>
requires size(ARGS) ==Int 1 [preserves-definedness, priority(100)]
```

#### Ranges

An `Index` projection operates on an array or slice (`Range`) value, to access an element of the array.
Expand Down
25 changes: 25 additions & 0 deletions kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
struct MyStruct {
data: i32
}

fn main() {
// List of MyStruct instances
let struct_list = [
MyStruct { data: 10 },
MyStruct { data: 20 },
MyStruct { data: 30 },
MyStruct { data: 40 },
MyStruct { data: 50 }
];

// Closure function that takes &MyStruct reference
let get_value = |struct_ref: &MyStruct| {
struct_ref.data
};
Comment on lines +15 to +18
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(probably off-topic)
While reading this code, I was thinking, what if we were using the struct_list in scope (capturing the variable in the closure), like this:

let get_value = | i: usize | { struct_list[i].data }

We should investigate closures a bit more (but unrelated to p-token)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Provided an issue here: #660


// Use list call style, passing reference
let result = get_value(&struct_list[2]);

// Verify result
assert_eq!(result, 30);
}
16 changes: 16 additions & 0 deletions kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@

┌─ 1 (root, init)
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
│ span: 0
│
│ (277 steps)
└─ 3 (stuck, leaf)
#traverseProjection ( toLocal ( 19 ) , thunk ( #decodeConstant ( constantKindAll
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we write the test program in a way that avoids this constant allocation?
Maybe using a literal array of i32 and producing the struct_list via into_iter, map, and collect?
Would be nicer to have a test that terminates with the fix.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is that something like:

struct MyStruct {
    data: i32
}

fn main() {
    // Create data dynamically using iterator pattern to avoid constant allocation
    let data = vec![10, 20, 30, 40, 50];
    let struct_list: Vec<MyStruct> = data.into_iter()
        .map(|d| MyStruct { data: d })
        .collect();
    
    // Closure function that takes &MyStruct reference
    let get_value = |struct_ref: &MyStruct| {
        struct_ref.data
    };
    
    // Use closure to access struct field
    let result = get_value(&struct_list[2]);
    
    // Verify result
    assert!(result == 30);
}

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  1. Initial Attempt: The new test avoided constant allocation but failed with TypeError: 'NoneType' object is not subscriptable in KMIR's smir.py:183.
  2. First Bug Fix: Found that some functions have body: None (specifically alloc::alloc::__rust_no_alloc_shim_is_unstable). Fixed by adding null check in call_edges property.
  3. Second Bug Fix: Encountered KeyError: 131 in reduce_to method. Fixed by filtering out non-existent types from the reachable set.
  4. Root Cause Discovery: Investigated what "type 131" actually is. Found that 131 is not a function type but a span ID (source location identifier) that appears in a StorageLive statement:
    {'kind': {'StorageLive': 15}, 'span': 131}.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It encounters a more weird issue than before.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK nevermind, then we keep this test for now .
The type 131 still exists, IDs of types and spans are disjoint so a span 131 does not mean there is no type 131. (BTW type and function IDs aren't disjoint).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you. I'm still learning. So it is a bug in smir-json?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not a bug, just that we don't extract all types. (take a look at the TyVisitor https://github.com/runtimeverification/stable-mir-json/blob/master/src/printer.rs#L520)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you. Let me learn about this.

function: main
span: 106


┌─ 2 (root, leaf, target, terminal)
│ #EndProgram ~> .K


1 change: 1 addition & 0 deletions kmir/src/tests/integration/test_integration.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@
'checked_arithmetic-fail',
'offset-u8-fail',
'pointer-cast-length-test-fail',
'closure_access_struct-fail',
]


Expand Down