From 4ce3e9c7c11744abae52d7a3ae1a3962395784be Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 10:41:10 +0200 Subject: Import test suite from charon --- tests/src/arrays.rs | 328 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 328 insertions(+) create mode 100644 tests/src/arrays.rs (limited to 'tests/src/arrays.rs') diff --git a/tests/src/arrays.rs b/tests/src/arrays.rs new file mode 100644 index 00000000..1f094541 --- /dev/null +++ b/tests/src/arrays.rs @@ -0,0 +1,328 @@ +//! Exercise the translation of arrays, with features supported by Eurydice + +pub enum AB { + A, + B, +} + +pub fn incr(x: &mut u32) { + *x += 1; +} + +// Nano-tests +// ---------- + +// The suffix `_` prevents name collisions in some backends +pub fn array_to_shared_slice_(s: &[T; 32]) -> &[T] { + s +} + +// The suffix `_` prevents name collisions in some backends +pub fn array_to_mut_slice_(s: &mut [T; 32]) -> &mut [T] { + s +} + +pub fn array_len(s: [T; 32]) -> usize { + s.len() +} + +pub fn shared_array_len(s: &[T; 32]) -> usize { + s.len() +} + +pub fn shared_slice_len(s: &[T]) -> usize { + s.len() +} + +pub fn index_array_shared(s: &[T; 32], i: usize) -> &T { + &s[i] +} + +// Remark: can't move out of an array +// Also: can't move out of a slice. + +pub fn index_array_u32(s: [u32; 32], i: usize) -> u32 { + s[i] +} + +pub fn index_array_copy(x: &[u32; 32]) -> u32 { + x[0] +} + +pub fn index_mut_array(s: &mut [T; 32], i: usize) -> &mut T { + &mut s[i] +} + +pub fn index_slice(s: &[T], i: usize) -> &T { + &s[i] +} + +pub fn index_mut_slice(s: &mut [T], i: usize) -> &mut T { + &mut s[i] +} + +pub fn slice_subslice_shared_(x: &[u32], y: usize, z: usize) -> &[u32] { + &x[y..z] +} + +pub fn slice_subslice_mut_(x: &mut [u32], y: usize, z: usize) -> &mut [u32] { + &mut x[y..z] +} + +pub fn array_to_slice_shared_(x: &[u32; 32]) -> &[u32] { + x +} + +pub fn array_to_slice_mut_(x: &mut [u32; 32]) -> &mut [u32] { + x +} + +pub fn array_subslice_shared_(x: &[u32; 32], y: usize, z: usize) -> &[u32] { + &x[y..z] +} + +pub fn array_subslice_mut_(x: &mut [u32; 32], y: usize, z: usize) -> &mut [u32] { + &mut x[y..z] +} + +pub fn index_slice_0(s: &[T]) -> &T { + &s[0] +} + +pub fn index_array_0(s: &[T; 32]) -> &T { + &s[0] +} + +/* +// Unsupported by Aeneas for now +pub fn index_index_slice<'a, T>(s: &'a [&[T]], i: usize, j: usize) -> &'a T { + &s[i][j] +} +*/ + +pub fn index_index_array(s: [[u32; 32]; 32], i: usize, j: usize) -> u32 { + s[i][j] +} + +/* +// Unsupported by Aeneas for now +pub fn update_update_slice(s: &mut [&mut [u32]], i: usize, j: usize) { + s[i][j] = 0; +} +*/ + +pub fn update_update_array(mut s: [[u32; 32]; 32], i: usize, j: usize) { + s[i][j] = 0; +} + +pub fn array_local_deep_copy(x: &[u32; 32]) { + let _y = *x; +} + +pub fn take_array(_: [u32; 2]) {} +pub fn take_array_borrow(_: &[u32; 2]) {} +pub fn take_slice(_: &[u32]) {} +pub fn take_mut_slice(_: &mut [u32]) {} + +pub fn const_array() -> [u32; 2] { + [0, 0] +} + +pub fn const_slice() { + let _: &[u32] = &[0, 0]; +} + +/* +// This triggers a special case in the constant expressions +pub fn const_string() { + let _ = "hello"; +}*/ + +pub fn take_all() { + let mut x: [u32; 2] = [0, 0]; + // x is deep copied (copy node appears in Charon, followed by a move) + take_array(x); + take_array(x); + // x passed by address, there is a reborrow here + take_array_borrow(&x); + // automatic cast from array to slice (spanning entire array) + take_slice(&x); + // note that both appear as SliceNew expressions, meaning the SliceNew UnOp is overloaded for + // mut and non-mut cases + take_mut_slice(&mut x); +} + +pub fn index_array(x: [u32; 2]) -> u32 { + x[0] +} +pub fn index_array_borrow(x: &[u32; 2]) -> u32 { + x[0] +} + +pub fn index_slice_u32_0(x: &[u32]) -> u32 { + x[0] +} + +pub fn index_mut_slice_u32_0(x: &mut [u32]) -> u32 { + x[0] +} + +pub fn index_all() -> u32 { + let mut x: [u32; 2] = [0, 0]; + if true { + let _y: [u32; 2] = [0, 0]; + } else { + let _z: [u32; 1] = [0]; + } + index_array(x) + + index_array(x) + + index_array_borrow(&x) + + index_slice_u32_0(&x) + + index_mut_slice_u32_0(&mut x) +} + +pub fn update_array(mut x: [u32; 2]) { + x[0] = 1 +} +pub fn update_array_mut_borrow(x: &mut [u32; 2]) { + x[0] = 1 +} +pub fn update_mut_slice(x: &mut [u32]) { + x[0] = 1 +} + +pub fn update_all() { + let mut x: [u32; 2] = [0, 0]; + update_array(x); + update_array(x); + update_array_mut_borrow(&mut x); + update_mut_slice(&mut x); +} + +// Nano-tests, with ranges +// ----------------------- + +pub fn range_all() { + let mut x: [u32; 4] = [0, 0, 0, 0]; + // CONFIRM: there is no way to shrink [T;N] into [T;M] with M u32 { + let x: [u32; 2] = *x; + x[0] +} + +pub fn deref_array_mut_borrow(x: &mut [u32; 2]) -> u32 { + let x: [u32; 2] = *x; + x[0] +} + +// Non-copiable arrays +// ------------------- + +pub fn take_array_t(_: [AB; 2]) {} + +pub fn non_copyable_array() { + let x: [AB; 2] = [AB::A, AB::B]; + // x is moved (not deep copied!) + // TODO: determine whether the translation needs to be aware of that and pass by ref instead of by copy + take_array_t(x); + + // this fails, naturally: + // take_array_t(x); +} + +// Larger, random tests +// -------------------- + +pub fn sum(s: &[u32]) -> u32 { + let mut sum = 0; + let mut i = 0; + while i < s.len() { + sum += s[i]; + i += 1; + } + sum +} + +pub fn sum2(s: &[u32], s2: &[u32]) -> u32 { + let mut sum = 0; + assert!(s.len() == s2.len()); + let mut i = 0; + while i < s.len() { + sum += s[i] + s2[i]; + i += 1; + } + sum +} + +pub fn f0() { + let s: &mut [u32] = &mut [1, 2]; + s[0] = 1; +} + +pub fn f1() { + let mut s: [u32; 2] = [1, 2]; + s[0] = 1; +} + +pub fn f2(_: u32) {} + +pub fn f3() -> u32 { + let a: [u32; 2] = [1, 2]; + f2(a[0]); + let b = [0; 32]; + sum2(&a, f4(&b, 16, 18)) +} + +pub fn f4(x: &[u32; 32], y: usize, z: usize) -> &[u32] { + &x[y..z] +} + +pub const SZ: usize = 32; + +// There is something slightly annoying here: the SZ constant gets inlined +pub fn f5(x: &[u32; SZ]) -> u32 { + x[0] +} + +// To avoid lifetime shortening +pub fn ite() { + let mut x: [u32; 2] = [0, 0]; + if true { + let mut y: [u32; 2] = [0, 0]; + index_mut_slice_u32_0(&mut x); + index_mut_slice_u32_0(&mut y); + } +} + +pub fn zero_slice(a: &mut [u8]) { + let mut i: usize = 0; + let len = a.len(); + while i < len { + a[i] = 0; + i += 1; + } +} + +pub fn iter_mut_slice(a: &mut [u8]) { + let len = a.len(); + let mut i = 0; + while i < len { + i += 1; + } +} + +pub fn sum_mut_slice(a: &mut [u32]) -> u32 { + let mut i = 0; + let mut s = 0; + while i < a.len() { + s += a[i]; + i += 1; + } + s +} -- cgit v1.2.3