From 760604e8d2fa0e57a06942835f844ab8747e117a Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 29 Jul 2025 14:54:46 -0700 Subject: [PATCH 1/2] add loop_invariant and harness --- library/core/src/slice/mod.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 40602fa4c5a50..78a2eae39f900 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -1008,6 +1008,8 @@ impl [T] { let (b, _) = b.split_at_mut(n); let mut i = 0; + #[safety::loop_invariant(i <= n)] + #[safety::loop_modifies(unsafe {slice::from_raw_parts_mut(a.as_mut_ptr(), n)}, unsafe {slice::from_raw_parts_mut(b.as_mut_ptr(), n)}, &i)] while i < n { mem::swap(&mut a[i], &mut b[n - 1 - i]); i += 1; @@ -5565,4 +5567,10 @@ mod verify { gen_align_to_mut_harnesses!(align_to_mut_from_bool, bool); gen_align_to_mut_harnesses!(align_to_mut_from_char, char); gen_align_to_mut_harnesses!(align_to_mut_from_unit, ()); + + #[kani::proof] + fn check_reverse() { + let a: [u8; 100] = kani::any(); + let b = a.reverse(); + } } From 938c007de94f70e3172d7a0dfc68f8ac31336b16 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 29 Jul 2025 15:11:37 -0700 Subject: [PATCH 2/2] edit harness --- library/core/src/slice/mod.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 78a2eae39f900..fa93767687b99 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -1009,7 +1009,7 @@ impl [T] { let mut i = 0; #[safety::loop_invariant(i <= n)] - #[safety::loop_modifies(unsafe {slice::from_raw_parts_mut(a.as_mut_ptr(), n)}, unsafe {slice::from_raw_parts_mut(b.as_mut_ptr(), n)}, &i)] + #[kani::loop_modifies(unsafe {slice::from_raw_parts_mut(a.as_mut_ptr(), n)}, unsafe {slice::from_raw_parts_mut(b.as_mut_ptr(), n)}, &i)] while i < n { mem::swap(&mut a[i], &mut b[n - 1 - i]); i += 1; @@ -5570,7 +5570,7 @@ mod verify { #[kani::proof] fn check_reverse() { - let a: [u8; 100] = kani::any(); - let b = a.reverse(); + let mut a: [u8; 100] = kani::any(); + a.reverse(); } }