From ccc172b29f0caacb6c8fc2350609acf2db34840a Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 21 Oct 2024 00:41:44 -0500 Subject: [PATCH] Update test small_slice_eq (#3618) Update the harness functions with `kani::any` of vectors, and use memory predicates `smae_allocation` in the loop invariants. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../expected/loop-contract/small_slice_eq.rs | 20 ++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/tests/expected/loop-contract/small_slice_eq.rs b/tests/expected/loop-contract/small_slice_eq.rs index a59436122da5..31ae9da8c640 100644 --- a/tests/expected/loop-contract/small_slice_eq.rs +++ b/tests/expected/loop-contract/small_slice_eq.rs @@ -6,20 +6,25 @@ // Modifications Copyright Kani Contributors // See GitHub history for details. -// kani-flags: -Z loop-contracts --enable-unstable --cbmc-args --arrays-uf-always --no-standard-checks --object-bits 8 +// kani-flags: -Z loop-contracts -Z mem-predicates --enable-unstable --cbmc-args --object-bits 8 -//! Check if loop contracts are correctly applied. The flag --no-standard-checks should be -//! removed once same_object predicate is supported in loop contracts. +//! Check if loop contracts are correctly applied. #![feature(stmt_expr_attributes)] #![feature(proc_macro_hygiene)] #![feature(ptr_sub_ptr)] + +extern crate kani; + +use kani::mem::same_allocation; + unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { debug_assert_eq!(x.len(), y.len()); unsafe { let (mut px, mut py) = (x.as_ptr(), y.as_ptr()); let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4)); - #[kani::loop_invariant( px as isize >= x.as_ptr() as isize + #[kani::loop_invariant( same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py) + && px as isize >= x.as_ptr() as isize && py as isize >= y.as_ptr() as isize && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))] while px < pxend { @@ -43,9 +48,10 @@ fn small_slice_eq_harness() { // because DFCC contract enforcement assumes that a definition for `free` // exists. let _ = Box::new(10); - let mut a = [1; 2000]; - let mut b = [1; 2000]; + const ARR_SIZE: usize = 2000; + let x: [u8; ARR_SIZE] = kani::any(); + let y: [u8; ARR_SIZE] = kani::any(); unsafe { - small_slice_eq(&mut a, &mut b); + small_slice_eq(&x, &y); } }