Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
103 changes: 102 additions & 1 deletion kmir/src/kmir/kdist/mir-semantics/kmir.md
Original file line number Diff line number Diff line change
Expand Up @@ -367,7 +367,6 @@ An operand may be a `Reference` (the only way a function could access another fu
=>
ListItem(newLocal(TY, MUT)) #reserveFor(REST)


syntax KItem ::= #setArgsFromStack ( Int, Operands)
| #setArgFromStack ( Int, Operand)
| #execIntrinsic ( MonoItemKind, Operands, Place )
Expand Down Expand Up @@ -410,6 +409,108 @@ An operand may be a `Reference` (the only way a function could access another fu
andBool isTypedValue(CALLERLOCALS[I])
[preserves-definedness] // valid list indexing checked
```

For closures (like `|x,y| { things using x and y }`), a special calling convention is in effect:
The first argument of the closure is its environment.
Its type is currently not extracted (KMIR does not currently support variable-capturing) and it is not initialised.
The second argument is a _tuple_ of all the arguments, however the function body expects these arguments as single locals.

Using this calling convention should be indicated by the `spread_arg` field in the function body.[^spread_arg]
However, this field is usually `None` for _closures_, it is only set for internal functions of the Rust execution mechanism.
Therefore a heuristics is used here:
* The function has two arguments,
* the 1st argument has an unknown type (or refers to one),
* and the 2nd argument is a tuple.

[^spread_arg]: https://doc.rust-lang.org/beta/nightly-rustc/rustc_public/mir/body/struct.Body.html#structfield.spread_arg

```k
// reserve space for local variables and copy/move arguments from a tuple inside the old locals into their place
rule [setupCalleeClosure]: <k> #setUpCalleeData(
monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))),
operandMove(place(local(CLOSURE:Int), .ProjectionElems))
operandMove(place(local(TUPLE), .ProjectionElems))
.Operands
)
=>
#setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST)
// arguments are tuple components, stored as _2 .. _n
...
</k>
<currentFrame>
<currentBody> _ => toKList(BLOCKS) </currentBody>
<locals> LOCALS => #reserveFor(NEWLOCALS) </locals>
<stack>
(ListItem(CALLERFRAME => #updateStackLocal(#updateStackLocal(CALLERFRAME, TUPLE, Moved), CLOSURE, Moved)))
_:List
</stack>
...
</currentFrame>
requires 0 <=Int CLOSURE andBool CLOSURE <Int size(LOCALS)
andBool 0 <=Int TUPLE andBool TUPLE <Int size(LOCALS)
andBool isTypedValue(LOCALS[TUPLE])
andBool isTupleType(lookupTy(tyOfLocal({LOCALS[TUPLE]}:>TypedLocal)))
andBool isTypedLocal(LOCALS[CLOSURE])
andBool typeInfoVoidType ==K lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))
// either the closure ref type is missing from type table
[priority(40), preserves-definedness]

rule [setupCalleeClosure2]: <k> #setUpCalleeData(
monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))),
operandMove(place(local(CLOSURE:Int), .ProjectionElems))
operandMove(place(local(TUPLE), .ProjectionElems))
.Operands
)
=>
#setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST)
// arguments are tuple components, stored as _2 .. _n
...
</k>
<currentFrame>
<currentBody> _ => toKList(BLOCKS) </currentBody>
<locals> LOCALS => #reserveFor(NEWLOCALS) </locals>
<stack>
(ListItem(CALLERFRAME => #updateStackLocal(#updateStackLocal(CALLERFRAME, TUPLE, Moved), CLOSURE, Moved)))
_:List
</stack>
...
</currentFrame>
requires 0 <=Int CLOSURE andBool CLOSURE <Int size(LOCALS)
andBool 0 <=Int TUPLE andBool TUPLE <Int size(LOCALS)
andBool isTypedValue(LOCALS[TUPLE])
andBool isTupleType(lookupTy(tyOfLocal({LOCALS[TUPLE]}:>TypedLocal)))
andBool isTypedLocal(LOCALS[CLOSURE])
// or the closure ref type pointee is missing from the type table
andBool isRefType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))
andBool isTy(pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))))
andBool lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType
[priority(45), preserves-definedness]

syntax Bool ::= isTupleType ( TypeInfo ) [function, total]
| isRefType ( TypeInfo ) [function, total]
// -------------------------------------------------------
rule isTupleType(typeInfoTupleType(_)) => true
rule isTupleType( _ ) => false [owise]
rule isRefType(typeInfoRefType(_)) => true
rule isRefType( _ ) => false [owise]

syntax KItem ::= #setTupleArgs ( Int , Value )
| #setTupleArgs ( Int , List )

// unpack tuple and set arguments individually
rule <k> #setTupleArgs(IDX, Aggregate(variantIdx(0), ARGS)) => #setTupleArgs(IDX, ARGS) ... </k>

rule <k> #setTupleArgs(_, .List ) => .K ... </k>

rule <k> #setTupleArgs(IDX, ListItem(VAL) REST:List)
=> #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(VAL)) ~> #setTupleArgs(IDX +Int 1, REST)
...
</k>
```


#### Assert

The `Assert` terminator checks that an operand holding a boolean value (which has previously been computed, e.g., an overflow flag for arithmetic operations) has the expected value (e.g., that this overflow flag is `false` - a very common case).
If the condition value is as expected, the program proceeds with the given `target` block.
Otherwise the provided message is passed to a `panic!` call, ending the program with an error, modelled as an `AssertError` in the semantics.
Expand Down
24 changes: 0 additions & 24 deletions kmir/src/kmir/kdist/mir-semantics/rt/data.md
Original file line number Diff line number Diff line change
Expand Up @@ -445,30 +445,6 @@ 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
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
┌─ 1 (root, init)
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
│ (730 steps)
│ (727 steps)
├─ 3 (terminal)
│ #EndProgram ~> .K
Expand Down
Copy link
Contributor

Choose a reason for hiding this comment

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

I'd like to use prove-rs folder even for concrete testing. Because it only has one file to be added and one test to be ran. exec-smir eliminates the smir.json generation process, but have to execute both llvm and haskell backend.

Copy link
Member Author

@jberthold jberthold Nov 7, 2025

Choose a reason for hiding this comment

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

All exec_smir tests EDIT: The exec_smir tests that run without step limit
are also run as proofs to prove termination. I thought it is an advantage to run the test in more than one way.

Copy link
Contributor

Choose a reason for hiding this comment

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

Agreed, just think it's a little bit annoying of these file changes (smir.json, .state, test_integration). Additionally, to my experience, the .state only different when there are some issues in the semantics.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I agree with you @Stevengre and I raised it before and @ehildenb and @jberthold convinced my it was safer to have a dump some intermediate state to compare against. It isn't much more overhead to update with the make commands, and it could potentially uncover a bug in our process if we have unexpected diffs in that intermediate state but the proof itself still passes.

Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
fn test_t(x: (u32,)) -> u32 { x.0 } // expects a singleton tuple

fn main() {
let single: u32 = 32;
let tuple: (u32,) = (single,);

test_t(tuple); // gets passed a singleton tuple

let identity = |x| x; // expects a single u32

identity(single); // gets passed a &closure and a singleton tuple!

let twice = (single, single);
let is_equal = |a, b| { assert!(a == b); }; // expects and accesses its arguments as locals _2 and _3 (u32)

// is_equal(twice); // error
is_equal(single, single); // gets passed a &closure and a singleton tuple !!!
}
Loading