Skip to content

ptr_offset_from intrinsics #885

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
jberthold merged 3 commits into from
Dec 9, 2025
Merged

ptr_offset_from intrinsics #885

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
74b4115
WIP implement ptr_offset_from and ptr_offset_from_unsigned
jberthold Dec 9, 2025
c62c59d
Terminate with dedicated error on UB by offset_from
jberthold Dec 9, 2025
50075eb
add new offset_from test to 'show' set (fails with undesired outcome)
jberthold Dec 9, 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
49 changes: 49 additions & 0 deletions kmir/src/kmir/kdist/mir-semantics/intrinsics.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,55 @@ Execution gets stuck (no matching rule) when operands have different types or un
rule #extractOperandType(_, _) => TyUnknown [owise]
```

#### Ptr Offset Computations (`std::intrinsics::ptr_offset_from`, `std::intrinsics::ptr_offset_from_unsigned`)

The `ptr_offset_from[_unsigned]` calculates the distance between two pointers within the same allocation,
i.e., pointers that refer to the same place and only differ in their offset from a given base.

Additionally, for `ptr_offset_from_unsigned`, it is _known_ that the first argument has a greater offset than
the second argument, so the returned difference is always positive.


```k
rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from")), ARG1:Operand ARG2:Operand .Operands, DEST)
=> #ptrOffsetDiff(ARG1, ARG2, true, DEST)
...
</k>

rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from_unsigned")), ARG1:Operand ARG2:Operand .Operands, DEST)
=> #ptrOffsetDiff(ARG1, ARG2, false, DEST)
...
</k>

syntax KItem ::= #ptrOffsetDiff ( Evaluation , Evaluation , Bool , Place ) [seqstrict(1,2)]

syntax MIRError ::= UBPtrOffsetDiff

syntax UBPtrOffsetDiff ::= #UBErrorPtrOffsetDiff( Value , Value , Bool )

rule <k>
#ptrOffsetDiff(
PtrLocal(HEIGHT, PLACE, _, metadata( _ , OFF1, _)),
PtrLocal(HEIGHT, PLACE, _, metadata( _ , OFF2, _)),
SIGNED_FLAG,
DEST
) => #setLocalValue(DEST, Integer(OFF1 -Int OFF2, 64, SIGNED_FLAG))
...
</k>
requires (SIGNED_FLAG orBool OFF1 >=Int OFF2)

rule <k>
#ptrOffsetDiff(
PtrLocal(_, _, _, _) #as PTR1,
PtrLocal(_, _, _, _) #as PTR2,
SIGNED_FLAG,
_DEST
) => #UBErrorPtrOffsetDiff(PTR1, PTR2, SIGNED_FLAG)
...
</k>
[priority(100)]
```

```k
endmodule
```
137 changes: 137 additions & 0 deletions kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,137 @@

┌─ 1 (root, init)
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
│ span: 0
│
│ (296 steps)
├─ 3 (split)
│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) )
┃
┃ (branch)
┣━━┓ subst: .Subst
┃ ┃ constraint:
┃ ┃ 0 ==Int ARG_INT1:Int &Int 18446744073709551615
┃ │
┃ ├─ 4
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) )
┃ │
┃ │ (582 steps)
┃ ├─ 6 (terminal)
┃ │ #EndProgram ~> .K
┃ │
┃ ┊ constraint: true
┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ #EndProgram ~> .K
┃
┗━━┓ subst: .Subst
┃ constraint:
┃ notBool 0 ==Int ARG_INT1:Int &Int 18446744073709551615
│
├─ 5
│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) )
│
│ (1 step)
├─ 7 (split)
│ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) )
┃
┃ (branch)
┣━━┓ subst: .Subst
┃ ┃ constraint:
┃ ┃ 1 ==Int ARG_INT1:Int &Int 18446744073709551615
┃ │
┃ ├─ 8
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) )
┃ │
┃ │ (99 steps)
┃ └─ 10 (stuck, leaf)
┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 1 , place ( ... local: local
Comment on lines +46 to +48
Copy link
Member Author

@jberthold jberthold Dec 9, 2025

Choose a reason for hiding this comment

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

The test program uncovered a problem caused by making a pointer from a reference with offset:

let a = [1,2,3];
let a1_p: *const i32 = &a[1];

yields a pointer without size information nor offset in the metadata.

PtrLocal ( 
    0 ,
    place ( ... 
        local: local ( 2 ) ,
        projection: projectionElemConstantIndex ( ... offset: 1 , minLength: 0 , fromEnd: false )  .ProjectionElems ) ,
    mutabilityNot ,
    metadata ( noMetadataSize , 0 , noMetadataSize ) )

One would instead expect a pointer where the ConstantIndex projection is replaced by an offset, and the metadata indicates the original size of the array.
The test program fails here because the two pointers have different projection instead of different offsets. It would be possible to add a rule to the intrinsic for this case but the problem lies deeper.

This should be addressed when working on #784 .

┃
┗━━┓ subst: .Subst
┃ constraint:
┃ notBool 1 ==Int ARG_INT1:Int &Int 18446744073709551615
│
├─ 9
│ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) )
│
│ (1 step)
├─ 11 (split)
│ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) )
┃
┃ (branch)
┣━━┓ subst: .Subst
┃ ┃ constraint:
┃ ┃ 2 ==Int ARG_INT1:Int &Int 18446744073709551615
┃ │
┃ ├─ 12
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) )
┃ │
┃ │ (99 steps)
┃ └─ 14 (stuck, leaf)
┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 1 , place ( ... local: local
┃
┗━━┓ subst: .Subst
┃ constraint:
┃ notBool 2 ==Int ARG_INT1:Int &Int 18446744073709551615
│
├─ 13
│ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) )
│
│ (1 step)
├─ 15 (split)
│ #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) )
┃
┃ (branch)
┣━━┓ subst: .Subst
┃ ┃ constraint:
┃ ┃ 3 ==Int ARG_INT1:Int &Int 18446744073709551615
┃ │
┃ ├─ 16
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) )
┃ │
┃ │ (16 steps)
┃ └─ 18 (stuck, leaf)
┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 0 , place ( ... local: local
┃
┗━━┓ subst: .Subst
┃ constraint:
┃ notBool 3 ==Int ARG_INT1:Int &Int 18446744073709551615
│
├─ 17
│ #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) )
│
│ (1 step)
├─ 19 (split)
│ #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) )
┃
┃ (branch)
┣━━┓ subst: .Subst
┃ ┃ constraint:
┃ ┃ 4 ==Int ARG_INT1:Int &Int 18446744073709551615
┃ │
┃ ├─ 20
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) )
┃ │
┃ │ (68 steps)
┃ └─ 22 (stuck, leaf)
┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
┃ span: 32
┃
┗━━┓ subst: .Subst
┃ constraint:
┃ notBool 4 ==Int ARG_INT1:Int &Int 18446744073709551615
│
├─ 21
│ #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) )
│
│ (6 steps)
├─ 23 (terminal)
│ #EndProgram ~> .K
│
┊ constraint: true
┊ subst: ...
└─ 2 (leaf, target, terminal)
#EndProgram ~> .K



43 changes: 43 additions & 0 deletions kmir/src/tests/integration/data/prove-rs/test_offset_from-fail.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
#![feature(core_intrinsics)]
use std::intrinsics::ptr_offset_from_unsigned; // core::ptr variant since 1.87.0, not for us

fn testing(mode: isize) {
let a = [1, 2, 3, 4, 5];
let b = [6, 7, 8, 9, 10];
let a_p = &a as *const i32;
let b_p = &b as *const i32;
let a1: *const i32 = &a[1];
let a3: *const i32 = &a[3];
let b1: *const i32 = &b[1];

match mode {
0 => unsafe { // correct and expected operation on pointers with offset
let a1_p = a_p.add(1);
assert_eq!(a1_p.offset_from(a_p), 1);
assert_eq!(a_p.offset_from(a1_p), -1);
assert_eq!(ptr_offset_from_unsigned(a1_p, a_p), 1);
},
1 => unsafe { // correct and expected operation on addresses within arrays
assert_eq!(a3.offset_from(a1), 2);
Copy link
Member Author

@jberthold jberthold Dec 9, 2025

Choose a reason for hiding this comment

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

This operation should pass but fails because of the problem with ConstantIndex vs PointerOffset

Copy link
Collaborator

@dkcumming dkcumming Dec 9, 2025

Choose a reason for hiding this comment

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

Others are passing all good? I see some other stuck branches in the proof tree above

Copy link
Member Author

@jberthold jberthold Dec 9, 2025

Choose a reason for hiding this comment

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

Cases 2..4 are intended to become stuck because they are undefined behaviour (although the rustc compiled program executes the function calls in 2 and 3 - the random addresses are of course unlikely to produce 0xdeadbeef).

assert_eq!(a1.offset_from(a3), -2);
},
2 => unsafe { // different allocation
assert_eq!(a1.offset_from(b1), 0xdeadbeef); // UB
},
3 => unsafe {
// violating assumption of a3 > a1
assert_eq!(ptr_offset_from_unsigned(a1, a3), 0xdeadbeef); // UB
},
4 => unsafe {
let unit_p: *const () = &();
assert_eq!(unit_p.offset_from(unit_p), 0xdeadbeef); // panics
},
_ => ()
}
}


fn main() {
testing(0);
testing(4);
}
2 changes: 2 additions & 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 @@ -37,6 +37,7 @@
'assume-cheatcode': ['check_assume'],
'assume-cheatcode-conflict-fail': ['check_assume_conflict'],
'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'],
'test_offset_from-fail': ['testing'],
}
PROVE_RS_SHOW_SPECS = [
'local-raw-fail',
Expand All @@ -59,6 +60,7 @@
'unions-fail',
'transmute-maybe-uninit-fail',
'iter_next_2-fail',
'test_offset_from-fail',
]


Expand Down