From 760604e8d2fa0e57a06942835f844ab8747e117a Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 29 Jul 2025 14:54:46 -0700 Subject: [PATCH 1/3] 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/3] 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(); } } From fc6416470e812914074b46188b19c8f71b604c09 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 Aug 2025 11:48:52 +0200 Subject: [PATCH 3/3] Put loop_modifies in cfg_attr(kani) --- library/core/src/slice/mod.rs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 79abd3228ae11..65169601154d2 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -1012,7 +1012,12 @@ impl [T] { let mut i = 0; #[safety::loop_invariant(i <= n)] - #[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)] + #[cfg_attr(kani, + 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;