Skip to content

Commit e42fd70

Browse files
jbertholdjberthold
authored
ptr_offset_from intrinsics (#885)
Implements the `ptr_offset_from[_unsigned]` intrinsics for pointers with offset, basic case only.
1 parent 4da0440 commit e42fd70

File tree

4 files changed

+231
-0
lines changed

4 files changed

+231
-0
lines changed

‎kmir/src/kmir/kdist/mir-semantics/intrinsics.md‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -125,6 +125,55 @@ Execution gets stuck (no matching rule) when operands have different types or un
125125
rule #extractOperandType(_, _) => TyUnknown [owise]
126126
```
127127

128+
#### Ptr Offset Computations (`std::intrinsics::ptr_offset_from`, `std::intrinsics::ptr_offset_from_unsigned`)
129+
130+
The `ptr_offset_from[_unsigned]` calculates the distance between two pointers within the same allocation,
131+
i.e., pointers that refer to the same place and only differ in their offset from a given base.
132+
133+
Additionally, for `ptr_offset_from_unsigned`, it is _known_ that the first argument has a greater offset than
134+
the second argument, so the returned difference is always positive.
135+
136+
137+
```k
138+
rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from")), ARG1:Operand ARG2:Operand .Operands, DEST)
139+
=> #ptrOffsetDiff(ARG1, ARG2, true, DEST)
140+
...
141+
</k>
142+
143+
rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from_unsigned")), ARG1:Operand ARG2:Operand .Operands, DEST)
144+
=> #ptrOffsetDiff(ARG1, ARG2, false, DEST)
145+
...
146+
</k>
147+
148+
syntax KItem ::= #ptrOffsetDiff ( Evaluation , Evaluation , Bool , Place ) [seqstrict(1,2)]
149+
150+
syntax MIRError ::= UBPtrOffsetDiff
151+
152+
syntax UBPtrOffsetDiff ::= #UBErrorPtrOffsetDiff( Value , Value , Bool )
153+
154+
rule <k>
155+
#ptrOffsetDiff(
156+
PtrLocal(HEIGHT, PLACE, _, metadata( _ , OFF1, _)),
157+
PtrLocal(HEIGHT, PLACE, _, metadata( _ , OFF2, _)),
158+
SIGNED_FLAG,
159+
DEST
160+
) => #setLocalValue(DEST, Integer(OFF1 -Int OFF2, 64, SIGNED_FLAG))
161+
...
162+
</k>
163+
requires (SIGNED_FLAG orBool OFF1 >=Int OFF2)
164+
165+
rule <k>
166+
#ptrOffsetDiff(
167+
PtrLocal(_, _, _, _) #as PTR1,
168+
PtrLocal(_, _, _, _) #as PTR2,
169+
SIGNED_FLAG,
170+
_DEST
171+
) => #UBErrorPtrOffsetDiff(PTR1, PTR2, SIGNED_FLAG)
172+
...
173+
</k>
174+
[priority(100)]
175+
```
176+
128177
```k
129178
endmodule
130179
```

‎kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected‎

Lines changed: 137 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,137 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
│
6+
│ (296 steps)
7+
├─ 3 (split)
8+
│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) )
9+
┃
10+
┃ (branch)
11+
┣━━┓ subst: .Subst
12+
┃ ┃ constraint:
13+
┃ ┃ 0 ==Int ARG_INT1:Int &Int 18446744073709551615
14+
┃ │
15+
┃ ├─ 4
16+
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) )
17+
┃ │
18+
┃ │ (582 steps)
19+
┃ ├─ 6 (terminal)
20+
┃ │ #EndProgram ~> .K
21+
┃ │
22+
┃ ┊ constraint: true
23+
┃ ┊ subst: ...
24+
┃ └─ 2 (leaf, target, terminal)
25+
┃ #EndProgram ~> .K
26+
┃
27+
┗━━┓ subst: .Subst
28+
┃ constraint:
29+
┃ notBool 0 ==Int ARG_INT1:Int &Int 18446744073709551615
30+
│
31+
├─ 5
32+
│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) )
33+
│
34+
│ (1 step)
35+
├─ 7 (split)
36+
│ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) )
37+
┃
38+
┃ (branch)
39+
┣━━┓ subst: .Subst
40+
┃ ┃ constraint:
41+
┃ ┃ 1 ==Int ARG_INT1:Int &Int 18446744073709551615
42+
┃ │
43+
┃ ├─ 8
44+
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) )
45+
┃ │
46+
┃ │ (99 steps)
47+
┃ └─ 10 (stuck, leaf)
48+
┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 1 , place ( ... local: local
49+
┃
50+
┗━━┓ subst: .Subst
51+
┃ constraint:
52+
┃ notBool 1 ==Int ARG_INT1:Int &Int 18446744073709551615
53+
│
54+
├─ 9
55+
│ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) )
56+
│
57+
│ (1 step)
58+
├─ 11 (split)
59+
│ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) )
60+
┃
61+
┃ (branch)
62+
┣━━┓ subst: .Subst
63+
┃ ┃ constraint:
64+
┃ ┃ 2 ==Int ARG_INT1:Int &Int 18446744073709551615
65+
┃ │
66+
┃ ├─ 12
67+
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) )
68+
┃ │
69+
┃ │ (99 steps)
70+
┃ └─ 14 (stuck, leaf)
71+
┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 1 , place ( ... local: local
72+
┃
73+
┗━━┓ subst: .Subst
74+
┃ constraint:
75+
┃ notBool 2 ==Int ARG_INT1:Int &Int 18446744073709551615
76+
│
77+
├─ 13
78+
│ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) )
79+
│
80+
│ (1 step)
81+
├─ 15 (split)
82+
│ #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) )
83+
┃
84+
┃ (branch)
85+
┣━━┓ subst: .Subst
86+
┃ ┃ constraint:
87+
┃ ┃ 3 ==Int ARG_INT1:Int &Int 18446744073709551615
88+
┃ │
89+
┃ ├─ 16
90+
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) )
91+
┃ │
92+
┃ │ (16 steps)
93+
┃ └─ 18 (stuck, leaf)
94+
┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 0 , place ( ... local: local
95+
┃
96+
┗━━┓ subst: .Subst
97+
┃ constraint:
98+
┃ notBool 3 ==Int ARG_INT1:Int &Int 18446744073709551615
99+
│
100+
├─ 17
101+
│ #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) )
102+
│
103+
│ (1 step)
104+
├─ 19 (split)
105+
│ #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) )
106+
┃
107+
┃ (branch)
108+
┣━━┓ subst: .Subst
109+
┃ ┃ constraint:
110+
┃ ┃ 4 ==Int ARG_INT1:Int &Int 18446744073709551615
111+
┃ │
112+
┃ ├─ 20
113+
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) )
114+
┃ │
115+
┃ │ (68 steps)
116+
┃ └─ 22 (stuck, leaf)
117+
┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
118+
┃ span: 32
119+
┃
120+
┗━━┓ subst: .Subst
121+
┃ constraint:
122+
┃ notBool 4 ==Int ARG_INT1:Int &Int 18446744073709551615
123+
│
124+
├─ 21
125+
│ #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) )
126+
│
127+
│ (6 steps)
128+
├─ 23 (terminal)
129+
│ #EndProgram ~> .K
130+
│
131+
┊ constraint: true
132+
┊ subst: ...
133+
└─ 2 (leaf, target, terminal)
134+
#EndProgram ~> .K
135+
136+
137+

‎kmir/src/tests/integration/data/prove-rs/test_offset_from-fail.rs‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
#![feature(core_intrinsics)]
2+
use std::intrinsics::ptr_offset_from_unsigned; // core::ptr variant since 1.87.0, not for us
3+
4+
fn testing(mode: isize) {
5+
let a = [1, 2, 3, 4, 5];
6+
let b = [6, 7, 8, 9, 10];
7+
let a_p = &a as *const i32;
8+
let b_p = &b as *const i32;
9+
let a1: *const i32 = &a[1];
10+
let a3: *const i32 = &a[3];
11+
let b1: *const i32 = &b[1];
12+
13+
match mode {
14+
0 => unsafe { // correct and expected operation on pointers with offset
15+
let a1_p = a_p.add(1);
16+
assert_eq!(a1_p.offset_from(a_p), 1);
17+
assert_eq!(a_p.offset_from(a1_p), -1);
18+
assert_eq!(ptr_offset_from_unsigned(a1_p, a_p), 1);
19+
},
20+
1 => unsafe { // correct and expected operation on addresses within arrays
21+
assert_eq!(a3.offset_from(a1), 2);
22+
assert_eq!(a1.offset_from(a3), -2);
23+
},
24+
2 => unsafe { // different allocation
25+
assert_eq!(a1.offset_from(b1), 0xdeadbeef); // UB
26+
},
27+
3 => unsafe {
28+
// violating assumption of a3 > a1
29+
assert_eq!(ptr_offset_from_unsigned(a1, a3), 0xdeadbeef); // UB
30+
},
31+
4 => unsafe {
32+
let unit_p: *const () = &();
33+
assert_eq!(unit_p.offset_from(unit_p), 0xdeadbeef); // panics
34+
},
35+
_ => ()
36+
}
37+
}
38+
39+
40+
fn main() {
41+
testing(0);
42+
testing(4);
43+
}

‎kmir/src/tests/integration/test_integration.py‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,7 @@
3737
'assume-cheatcode': ['check_assume'],
3838
'assume-cheatcode-conflict-fail': ['check_assume_conflict'],
3939
'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'],
40+
'test_offset_from-fail': ['testing'],
4041
}
4142
PROVE_RS_SHOW_SPECS = [
4243
'local-raw-fail',
@@ -59,6 +60,7 @@
5960
'unions-fail',
6061
'transmute-maybe-uninit-fail',
6162
'iter_next_2-fail',
63+
'test_offset_from-fail',
6264
]
6365

6466

0 commit comments

Comments
 (0)