From cdaca583323c2719fc96236d8cb8e4365a232cb1 Mon Sep 17 00:00:00 2001 From: James Parker Date: Tue, 8 Oct 2024 15:38:27 -0400 Subject: [PATCH] Update type of indices to be `u64` --- src/examples/add_two_array.c | 10 +++++----- src/examples/array_load.broken.c | 8 ++++---- src/examples/array_load.c | 13 +++++++------ src/examples/array_load2.c | 8 ++++---- src/examples/init_array.c | 10 +++++----- src/examples/init_array2.c | 12 ++++++------ src/examples/init_array_rev.c | 20 ++++++++++---------- src/examples/swap_array.c | 10 +++++----- src/tutorial.adoc | 20 ++++++++++---------- 9 files changed, 56 insertions(+), 55 deletions(-) diff --git a/src/examples/add_two_array.c b/src/examples/add_two_array.c index 799edaf7..7897fc92 100644 --- a/src/examples/add_two_array.c +++ b/src/examples/add_two_array.c @@ -1,10 +1,10 @@ -unsigned int array_read_two (unsigned int *p, int n, int i, int j) +unsigned int array_read_two (unsigned int *p, unsigned long n, unsigned long i, unsigned long j) /* --BEGIN-- */ -/*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned(array_shift(p,k)) }; - 0i32 <= i && i < n; - 0i32 <= j && j < n; +/*@ requires take a1 = each(u64 k; 0u64 <= k && k < n) { Owned(array_shift(p,k)) }; + 0u64 <= i && i < n; + 0u64 <= j && j < n; j != i; - ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned(array_shift(p,k)) }; + ensures take a2 = each(u64 k; 0u64 <= k && k < n) { Owned(array_shift(p,k)) }; a1 == a2; return == a1[i] + a1[j]; @*/ diff --git a/src/examples/array_load.broken.c b/src/examples/array_load.broken.c index 3f4b6e63..f1e83fc5 100644 --- a/src/examples/array_load.broken.c +++ b/src/examples/array_load.broken.c @@ -1,7 +1,7 @@ -int read (int *p, int n, int i) -/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { Owned(array_shift(p,j)) }; - 0i32 <= i && i < n; - ensures take a2 = each(i32 j; 0i32 <= j && j < n) { Owned(array_shift(p,j)) }; @*/ +int read (int *p, unsigned long n, unsigned long i) +/*@ requires take a1 = each(u64 j; 0u64 <= j && j < n) { Owned(array_shift(p,j)) }; + 0u64 <= i && i < n; + ensures take a2 = each(u64 j; 0u64 <= j && j < n) { Owned(array_shift(p,j)) }; @*/ { return p[i]; } diff --git a/src/examples/array_load.c b/src/examples/array_load.c index eef0dab2..41dde6b3 100644 --- a/src/examples/array_load.c +++ b/src/examples/array_load.c @@ -1,10 +1,11 @@ -int read (int *p, int n, int i) -/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { +int read (int *p, unsigned long n, unsigned long i) +/*@ requires take a1 = each(u64 j; 0u64 <= j && j < n) { Owned(array_shift(p,j)) }; - 0i32 <= i && i < n; - ensures take a2 = each(i32 j; 0i32 <= j && j < n) { + 0u64 <= i && i < n; + n > 0u64; + ensures take a2 = each(u64 j; 0u64 <= j && j < n) { Owned(array_shift(p,j)) }; @*/ { - /*@ extract Owned, i; @*/ - return p[i]; + /*@ extract Owned, 0u64; @*/ + return p[0]; } diff --git a/src/examples/array_load2.c b/src/examples/array_load2.c index 4f38a1f1..6dc2140a 100644 --- a/src/examples/array_load2.c +++ b/src/examples/array_load2.c @@ -1,7 +1,7 @@ -int read (int *p, int n, int i) -/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { Owned(array_shift(p,j)) }; - 0i32 <= i && i < n; - ensures take a2 = each(i32 j; 0i32 <= j && j < n) { Owned(array_shift(p,j)) }; +int read (int *p, unsigned long n, unsigned long i) +/*@ requires take a1 = each(u64 j; 0u64 <= j && j < n) { Owned(array_shift(p,j)) }; + 0u64 <= i && i < n; + ensures take a2 = each(u64 j; 0u64 <= j && j < n) { Owned(array_shift(p,j)) }; a1 == a2; return == a1[i]; @*/ diff --git a/src/examples/init_array.c b/src/examples/init_array.c index 5fb3c97a..3f21b650 100644 --- a/src/examples/init_array.c +++ b/src/examples/init_array.c @@ -1,12 +1,12 @@ -void init_array (char *p, unsigned int n) -/*@ requires take a1 = each(u32 i; i < n) { Owned( array_shift(p, i)) }; - ensures take a2 = each(u32 i; i < n) { Owned( array_shift(p, i)) }; +void init_array (char *p, unsigned long n) +/*@ requires take a1 = each(u64 i; i < n) { Owned( array_shift(p, i)) }; + ensures take a2 = each(u64 i; i < n) { Owned( array_shift(p, i)) }; @*/ { - unsigned int j = 0; + unsigned long j = 0; while (j < n) /* --BEGIN-- */ - /*@ inv take ai = each(u32 i; i < n) { Owned( array_shift(p, i)) }; + /*@ inv take ai = each(u64 i; i < n) { Owned( array_shift(p, i)) }; {p} unchanged; {n} unchanged; @*/ /* --END-- */ diff --git a/src/examples/init_array2.c b/src/examples/init_array2.c index e1217845..f5ea88bc 100644 --- a/src/examples/init_array2.c +++ b/src/examples/init_array2.c @@ -1,13 +1,13 @@ -void init_array2 (char *p, unsigned int n) -/*@ requires take a1 = each(u32 i; i < n) { Block( array_shift(p, i)) }; - ensures take a2 = each(u32 i; i < n) { Owned( array_shift(p, i)) }; +void init_array2 (char *p, unsigned long n) +/*@ requires take a1 = each(u64 i; i < n) { Block( array_shift(p, i)) }; + ensures take a2 = each(u64 i; i < n) { Owned( array_shift(p, i)) }; @*/ { - unsigned int j = 0; + unsigned long j = 0; while (j < n) /* --BEGIN-- */ - /*@ inv take al = each(u32 i; i < j) { Owned( array_shift(p, i)) }; - take ar = each(u32 i; j <= i && i < n) { Block( array_shift(p, i)) }; + /*@ inv take al = each(u64 i; i < j) { Owned( array_shift(p, i)) }; + take ar = each(u64 i; j <= i && i < n) { Block( array_shift(p, i)) }; {p} unchanged; {n} unchanged; j <= n; @*/ diff --git a/src/examples/init_array_rev.c b/src/examples/init_array_rev.c index dd8de2b7..bf10cccd 100644 --- a/src/examples/init_array_rev.c +++ b/src/examples/init_array_rev.c @@ -1,22 +1,22 @@ -void init_array2 (char *p, unsigned int n) -/*@ requires take a1 = each(u32 i; i < n) { Block( array_shift(p, i)) }; - n > 0u32; - ensures take a2 = each(u32 i; i < n) { Owned( array_shift(p, i)) }; +void init_array2 (char *p, unsigned long n) +/*@ requires take a1 = each(u64 i; i < n) { Block( array_shift(p, i)) }; + n > 0u64; + ensures take a2 = each(u64 i; i < n) { Owned( array_shift(p, i)) }; @*/ { - unsigned int j = 0; + unsigned long j = 0; while (j < n) /* --BEGIN-- */ - /*@ inv take al = each(u32 i; i < n-j) { Block( array_shift(p, i)) }; - take ar = each(u32 i; n-j <= i && i < n) { Owned( array_shift(p, i)) }; + /*@ inv take al = each(u64 i; i < n-j) { Block( array_shift(p, i)) }; + take ar = each(u64 i; n-j <= i && i < n) { Owned( array_shift(p, i)) }; {p} unchanged; {n} unchanged; - 0u32 <= j && j <= n; + 0u64 <= j && j <= n; @*/ /* --END-- */ { /* --BEGIN-- */ - /*@ extract Block, n-(j+1u32); @*/ - /*@ extract Owned, n-(j+1u32); @*/ + /*@ extract Block, n-(j+1u64); @*/ + /*@ extract Owned, n-(j+1u64); @*/ /* --END-- */ p[n-(j+1)] = 0; j++; diff --git a/src/examples/swap_array.c b/src/examples/swap_array.c index 8cb18d67..0f5e20fa 100644 --- a/src/examples/swap_array.c +++ b/src/examples/swap_array.c @@ -1,10 +1,10 @@ -void swap_array (int *p, int n, int i, int j) +void swap_array (int *p, unsigned long n, unsigned long i, unsigned long j) /* --BEGIN-- */ -/*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned(array_shift(p,k)) }; - 0i32 <= i && i < n; - 0i32 <= j && j < n; +/*@ requires take a1 = each(u64 k; 0u64 <= k && k < n) { Owned(array_shift(p,k)) }; + 0u64 <= i && i < n; + 0u64 <= j && j < n; j != i; - ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned(array_shift(p,k)) }; + ensures take a2 = each(u64 k; 0u64 <= k && k < n) { Owned(array_shift(p,k)) }; a2 == a1[i: a1[j], j: a1[i]]; @*/ /* --END-- */ diff --git a/src/tutorial.adoc b/src/tutorial.adoc index e641a65c..fa882130 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -443,13 +443,13 @@ To support reasoning about code manipulating arrays and computed pointers, CN ha [source,c] ---- -each (i32 i; 0i32 <= i && i < 10i32) +each (u64 i; 0u64 <= i && i < 10u64) { Owned(array_shift(p,i)) } ---- In detail, this can be read as follows: -* for each integer `+i+` of CN type `+i32+`, … +* for each integer `+i+` of CN type `+u64+`, … * if `+i+` is between `+0+` and `+10+`, … @@ -508,7 +508,7 @@ Here the CN comment `+/*@ extract Owned, i; @*/+` is a CN "`ghost statement [source,c] ---- -each(i32 j; 0i32 <= j && j < n) { Owned(array_shift(p,j)) } +each(u64 j; 0u64 <= j && j < n) { Owned(array_shift(p,j)) } ---- is split into @@ -523,7 +523,7 @@ Owned(array_shift(p,i)) + [source,c] ---- -each(i32 j; 0i32 <= j && j < n && j != i) +each(u64 j; 0u64 <= j && j < n && j != i) { Owned(array_shift(p,j)) } ---- @@ -531,7 +531,7 @@ After this extraction step, CN can use the (former) extracted resource to justif Following an `+extract+` statement, CN moreover remembers the extracted index and can automatically "`reverse`" the extraction when needed: after type checking the access `+p[i]+` CN must ensure the function’s postcondition holds, which needs the full array ownership again (including the extracted index `+i+`); remembering the index `+i+`, CN then automatically merges resources (1) and (2) again to obtain the required full array ownership, and completes the verification of the function. -So far the specification only guarantees safe execution but does not specify the behaviour of `+read+`. To address this, let’s return to the iterated resources in the function specification. When we specify `+take a1 = each ...+` here, what is `+a1+`? In CN, the output of an iterated resource is a _map_ from indices to resource outputs. In this example, where index `+j+` has CN type `+i32+` and the iterated resource is `+Owned+`, the output `+a1+` is a map from `+i32+` indices to `+i32+` values — CN type `+map+`. (If the type of `+j+` was `+i64+` and the resource `+Owned+`, `+a1+` would have type `+map+`.) +So far the specification only guarantees safe execution but does not specify the behaviour of `+read+`. To address this, let’s return to the iterated resources in the function specification. When we specify `+take a1 = each ...+` here, what is `+a1+`? In CN, the output of an iterated resource is a _map_ from indices to resource outputs. In this example, where index `+j+` has CN type `+u64+` and the iterated resource is `+Owned+`, the output `+a1+` is a map from `+u64+` indices to `+i32+` values — CN type `+map+`. We can use this to refine our specification with information about the functional behaviour of `+read+`. @@ -557,14 +557,14 @@ include_example(exercises/swap_array.c) //// TODO: BCP: I wrote this, which seemed natural but did not work -- I still don't fully understand why. I think this section will need some more examples / exercises to be fully digestible, or perhaps this is just yet another symptom of my imperfecdt understanding of how the numeric stuff works. - void swap_array (int *p, int n, int i, int j) - /*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned(array_shift(p,k)) }; - 0i32 <= i && i < n; - 0i32 <= j && j < n; + void swap_array (int *p, unsigned long n, unsigned long i, unsigned long j) + /*@ requires take a1 = each(u64 k; 0u64 <= k && k < n) { Owned(array_shift(p,k)) }; + 0u64 <= i && i < n; + 0u64 <= j && j < n; j != i; take xi = Owned(array_shift(p,i)); take xj = Owned(array_shift(p,j)) - ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned(array_shift(p,k)) }; + ensures take a2 = each(u64 k; 0u64 <= k && k < n) { Owned(array_shift(p,k)) }; a1[i:xj][j:xi] == a2 @*/ {