File tree 2 files changed +32
-3
lines changed
2 files changed +32
-3
lines changed Original file line number Diff line number Diff line change @@ -2426,15 +2426,20 @@ impl<T> [T] {
2426
2426
where
2427
2427
F : FnMut ( & ' a T ) -> Ordering ,
2428
2428
{
2429
+ // INVARIANTS:
2430
+ // - 0 <= left <= left + size = right <= self.len()
2431
+ // - f returns Less for everything in self[..left]
2432
+ // - f returns Greater for everything in self[right..]
2429
2433
let mut size = self . len ( ) ;
2430
2434
let mut left = 0 ;
2431
2435
let mut right = size;
2432
2436
while left < right {
2433
2437
let mid = left + size / 2 ;
2434
2438
2435
- // SAFETY: the call is made safe by the following invariants:
2436
- // - `mid >= 0`
2437
- // - `mid < size`: `mid` is limited by `[left; right)` bound.
2439
+ // SAFETY: the while condition means `size` is strictly positive, so
2440
+ // `size/2 < size`. Thus `left + size/2 < left + size`, which
2441
+ // coupled with the `left + size <= self.len()` invariant means
2442
+ // we have `left + size/2 < self.len()`, and this is in-bounds.
2438
2443
let cmp = f ( unsafe { self . get_unchecked ( mid) } ) ;
2439
2444
2440
2445
// The reason why we use if/else control flow rather than match
@@ -2452,6 +2457,10 @@ impl<T> [T] {
2452
2457
2453
2458
size = right - left;
2454
2459
}
2460
+
2461
+ // SAFETY: directly true from the overall invariant.
2462
+ // Note that this is `<=`, unlike the assume in the `Ok` path.
2463
+ unsafe { crate :: intrinsics:: assume ( left <= self . len ( ) ) } ;
2455
2464
Err ( left)
2456
2465
}
2457
2466
Original file line number Diff line number Diff line change @@ -16,3 +16,23 @@ pub fn binary_search_index_no_bounds_check(s: &[u8]) -> u8 {
16
16
42
17
17
}
18
18
}
19
+
20
+ // Similarly, check that `partition_point` is known to return a valid fencepost.
21
+
22
+ // CHECK-LABEL: @unknown_split
23
+ #[ no_mangle]
24
+ pub fn unknown_split ( x : & [ i32 ] , i : usize ) -> ( & [ i32 ] , & [ i32 ] ) {
25
+ // This just makes sure that the subsequent function is looking for the
26
+ // absence of something that might actually be there.
27
+
28
+ // CHECK: call core::panicking::panic
29
+ x. split_at ( i)
30
+ }
31
+
32
+ // CHECK-LABEL: @partition_point_split_no_bounds_check
33
+ #[ no_mangle]
34
+ pub fn partition_point_split_no_bounds_check ( x : & [ i32 ] , needle : i32 ) -> ( & [ i32 ] , & [ i32 ] ) {
35
+ // CHECK-NOT: call core::panicking::panic
36
+ let i = x. partition_point ( |p| p < & needle) ;
37
+ x. split_at ( i)
38
+ }
You can’t perform that action at this time.
0 commit comments