Skip to content

Commit caa5994

Browse files
authored
fix(rt): bug fix for castKindPtrToPtr (#974)
This PR addresses an issue that was first identified in solana-token's `test_validate_owner_multisig.rs` proof. `iter_next_3.rs` is a minimized test that reproduces the issue. ### Problem When executing Rust's slice iterator (`core::slice::Iter`), the `Iter::new` function creates two pointers: a start pointer and an end pointer. The `next` method compares these pointers for equality to determine whether iteration is complete. During `Iter::new`, the end pointer undergoes a `PtrToPtr` cast (e.g., from `*const [u8; 32]` to `*mut [u8; 32]`) that changes its initially correct metadata to one that causes the issue. - Initially correct metadata: `metadata(staticSize(32), 3, dynamicSize(3))` - Resulting metadata: `metadata(staticSize(32), 3, staticSize(32))` - Applied `convertMetadata` rule: https://github.com/runtimeverification/mir-semantics/blob/8b331c654d225b13b410970599e559e95947edc5/kmir/src/kmir/kdist/mir-semantics/rt/data.md?plain=1#L1508 This rule sets the origin to `staticSize(32)` (matched with `ORIGIN_SIZE`), discarding the previous correct `dynamicSize(3)`. The start pointer does not undergo this additional cast, and maintains its metadata: `metadata(staticSize(32), 3, dynamicSize(3))`. This causes the two pointers to end up with different metadata: `metadata(staticSize(32), 3, dynamicSize(3))` vs `metadata(staticSize(32), 3, staticSize(32))`. When `Iter::next` compares the pointers for equality at the end of iteration, the comparison evaluates to `false` instead of `true`, causing the proof to take the wrong branch (not-at-the-end) and eventually get stuck on an out-of-bounds access. ### Solution We add a `#cast` rule for `castKindPtrToPtr`, with higher priority, that matches when the source and target pointer types have identical pointee types. This rule preserves the source pointer metadata. This works because when the pointee types are identical, the pointer representation does not need to change. The only reason such a cast exists in MIR is a mutability change, which does not affect the pointer's runtime representation or metadata. When the pointee types are not identical, the rule does not match, and we fallback to the existing rule and handle the cast as before. For casts where both the pointee type and mutability differ (e.g., `*const T1` to `*mut T2`: `T1=/=T2`), I am not sure how MIR is generated for these, but either case is handled correctly: - If it is a single cast, the pointee types differ, so the new rule does not match and the fallback rule handles it as before. Mutability is not involved in type projections or equality checks, so it does not interfere. - If it is two separate casts (one for mutability, one for the pointee type), the new rule matches the mutability cast and the fallback rule handles the pointee type cast. ### Why mutability information was not added It would be possible to thread mutability information through the semantics (from the smir.json, which now includes mutability on `PtrType` and `RefType`, PR [here](runtimeverification/stable-mir-json#127)) and add an explicit check that the cast is indeed a mutability-only change. I chose not to include it, with the following reasoning. The new mutability information would only be used to confirm that the source and target pointer types differ in mutability in the new `#cast` rule. Any other place where the new mutability information would be threaded through would be `_`. At the same time, if the source and target pointer types have identical pointee types, the only possible difference that would have led to a cast is a difference in mutability. Propagating the mutability in the semantics for this check alone seems to add overhead for no benefit, especially considering that mutability is not checked/enforced anywhere else. So, it seems sufficient to just rely on the fact that because the pointee type is the same, we do not need to change the metadata of the pointer, so we simply do not. Mutability does not affect that.
1 parent 022dafb commit caa5994

4 files changed

Lines changed: 51 additions & 0 deletions

File tree

kmir/src/kmir/kdist/mir-semantics/rt/data.md

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1440,6 +1440,20 @@ which have the same representation `Value::Range`.
14401440
Also, casts to and from _transparent wrappers_ (newtypes that just forward field `0`, i.e. `struct Wrapper<T>(T)`)
14411441
are allowed, and supported by a special projection `WrapStruct`.
14421442

1443+
When the source and target types are pointer types with the same pointee type (i.e., differing only in mutability),
1444+
the cast preserves the source pointer and its metadata unchanged.
1445+
1446+
```k
1447+
rule <k> #cast(PtrLocal(OFFSET, PLACE, MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
1448+
=> PtrLocal(OFFSET, PLACE, MUT, META)
1449+
...
1450+
</k>
1451+
requires pointeeTy(lookupTy(TY_SOURCE)) ==K pointeeTy(lookupTy(TY_TARGET))
1452+
[priority(45), preserves-definedness] // valid map lookups checked
1453+
```
1454+
1455+
Otherwise, compute the type projection and convert metadata accordingly.
1456+
14431457
```k
14441458
rule <k> #cast(PtrLocal(OFFSET, place(LOCAL, PROJS), MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
14451459
=>
Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
struct Wrapper {
2+
tag: u8,
3+
a: [[u8; 32]; 3],
4+
}
5+
6+
fn foo(c: &Wrapper) {
7+
for elem in c.a.iter() {
8+
assert!(elem[0] != 0);
9+
}
10+
}
11+
12+
fn main() {
13+
let c = Wrapper {
14+
tag: 42,
15+
a: [[1u8; 32], [2u8; 32], [3u8; 32]],
16+
};
17+
18+
foo(&c);
19+
}
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
6+
│ (2028 steps)
7+
├─ 3 (terminal)
8+
│ #EndProgram ~> .K
9+
│ function: main
10+
11+
┊ constraint: true
12+
┊ subst: ...
13+
└─ 2 (leaf, target, terminal)
14+
#EndProgram ~> .K
15+
16+
17+

kmir/src/tests/integration/test_integration.py

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,7 @@
4343
'local-raw-fail',
4444
'interior-mut-fail',
4545
'interior-mut3-fail',
46+
'iter_next_3',
4647
'assert_eq_exp',
4748
'bitwise-not-shift',
4849
'symbolic-args-fail',

0 commit comments

Comments
 (0)