From fc8cc1423460e51473b78fc91d281baa2c8a27f9 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 1 Dec 2025 12:35:24 +1100 Subject: [PATCH 1/3] Allow field(0) projection as a no-op when target value is a PtrLocal - fixes iter.next() --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 20 +++++++++++++++++++ .../integration/data/prove-rs/iter_next_1.rs | 15 ++++++++++++++ 2 files changed, 35 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/iter_next_1.rs diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 4b0470f02..29ca416c8 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -450,6 +450,26 @@ This is done without consideration of the validity of the Downcast[^downcast]. ``` +In context with pointer casts, the semantics handles the special case of a _transparent wrapper struct_: +A pointer to a struct containing a single element can be cast to a pointer to the single element itself. +While the pointer cast tries to insert and remove field projections to the singleton field, +it is still possible that a field projection occurs on a value which is not an Aggregate (nor a union). +This necessitates a special rule which allows the semantics to perform a field projection to field 0 as a Noop. +The situation typically arises when the stored value is a pointer (`NonNull`), therefore the rule is restricted to this case. +The context is populated with the correct field access data, so that write-backs will correct the stored value to an Aggregate. + +```k + rule #traverseProjection( + DEST, + PtrLocal(_, _, _, _) #as VALUE, + projectionElemField(fieldIdx(0), TY) PROJS, + CTXTS + ) + => #traverseProjection(DEST, VALUE, PROJS, CtxField(variantIdx(0), ListItem(VALUE), 0, TY) CTXTS) ... + [preserves-definedness, priority(100)] +``` + + #### Unions ```k // Case: Union is in same state as field projection diff --git a/kmir/src/tests/integration/data/prove-rs/iter_next_1.rs b/kmir/src/tests/integration/data/prove-rs/iter_next_1.rs new file mode 100644 index 000000000..85190672d --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/iter_next_1.rs @@ -0,0 +1,15 @@ +struct Thing { payload: u16 } + +fn main() { + let a = [Thing{payload: 1}, Thing{payload: 2}, Thing{payload: 3}]; + + let mut i = a.iter(); + let elem = i.next(); + assert!(elem.unwrap().payload == 1); + let elem = i.next(); + assert!(elem.unwrap().payload == 2); + let elem = i.next(); + assert!(elem.unwrap().payload == 3); + // let elem = i.next(); + // assert!(elem.is_none()); +} \ No newline at end of file From 8a25147f2f332e439d2bace46fca00527456de1d Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 1 Dec 2025 13:28:10 +1100 Subject: [PATCH 2/3] add failing test case for next() returning None --- .../integration/data/prove-rs/iter_next_2-fail.rs | 15 +++++++++++++++ .../prove-rs/show/iter_next_2-fail.main.expected | 15 +++++++++++++++ kmir/src/tests/integration/test_integration.py | 1 + 3 files changed, 31 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/iter_next_2-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/iter_next_2-fail.rs b/kmir/src/tests/integration/data/prove-rs/iter_next_2-fail.rs new file mode 100644 index 000000000..70cf419f0 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/iter_next_2-fail.rs @@ -0,0 +1,15 @@ +struct Thing { payload: u16 } + +fn main() { + let a = [Thing{payload: 1}, Thing{payload: 2}, Thing{payload: 3}]; + + let mut i = a.iter(); + let elem = i.next(); + assert!(elem.unwrap().payload == 1); + let elem = i.next(); + assert!(elem.unwrap().payload == 2); + let elem = i.next(); + assert!(elem.unwrap().payload == 3); + let elem = i.next(); + assert!(elem.is_none()); +} \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected new file mode 100644 index 000000000..dcc3159dd --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (1990 steps) +└─ 3 (stuck, leaf) + #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Range ( .List ) , .Projectio + span: 146 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index a62488f8b..d06d597fd 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -58,6 +58,7 @@ 'iterator-simple-fail', 'unions-fail', 'transmute-maybe-uninit-fail', + 'iter_next_2-fail' ] From 8b9009328ee6bed7f473e17ad43450ae0dce1e2c Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 1 Dec 2025 13:50:12 +1100 Subject: [PATCH 3/3] coma --- kmir/src/tests/integration/test_integration.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index d06d597fd..77f181b67 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -58,7 +58,7 @@ 'iterator-simple-fail', 'unions-fail', 'transmute-maybe-uninit-fail', - 'iter_next_2-fail' + 'iter_next_2-fail', ]