Add support for accessing single-element aggregates in #traverseProjection

[Stevengre]

• Updated documentation to explain how to directly access elements of an Aggregate when #traverseProjection becomes stuck.
• Introduced a new rule for handling single-element aggregates in the semantics.
• Added a new test case for closure access to a struct, ensuring correct behavior.
• Updated integration tests to include the new failure case for closure access to structs.

[jberthold]

(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)

[Stevengre]

Provided an issue here: #660

[jberthold]

Maybe add text describing what we would see in that test when removing the rule.
Anyone who reads it will understand better without having to repeat your experiments.

[Stevengre]

Updated the description!

[jberthold]

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.

[Stevengre]

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);
}

[Stevengre]

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}.

[Stevengre]

It encounters a more weird issue than before.

[jberthold]

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).

[Stevengre]

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

[jberthold]

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)

[Stevengre]

Thank you. Let me learn about this.

[jberthold]

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).