summaryrefslogtreecommitdiff
path: root/tests/src/arrays.rs
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/src/arrays.rs328
1 files changed, 328 insertions, 0 deletions
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_<T>(s: &[T; 32]) -> &[T] {
+ s
+}
+
+// The suffix `_` prevents name collisions in some backends
+pub fn array_to_mut_slice_<T>(s: &mut [T; 32]) -> &mut [T] {
+ s
+}
+
+pub fn array_len<T>(s: [T; 32]) -> usize {
+ s.len()
+}
+
+pub fn shared_array_len<T>(s: &[T; 32]) -> usize {
+ s.len()
+}
+
+pub fn shared_slice_len<T>(s: &[T]) -> usize {
+ s.len()
+}
+
+pub fn index_array_shared<T>(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<T>(s: &mut [T; 32], i: usize) -> &mut T {
+ &mut s[i]
+}
+
+pub fn index_slice<T>(s: &[T], i: usize) -> &T {
+ &s[i]
+}
+
+pub fn index_mut_slice<T>(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<T>(s: &[T]) -> &T {
+ &s[0]
+}
+
+pub fn index_array_0<T>(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<N?
+ update_mut_slice(&mut x[1..3]);
+}
+
+// Nano-tests, with dereferences
+// -----------------------------
+
+pub fn deref_array_borrow(x: &[u32; 2]) -> 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
+}
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 09:30:28 +0000