I am learning about formal verification and using frama-c and the WP plug-in, and after reading some papers and following the WP Tutorial by Allan Blanchard, I decide to try to verify a function not on the tutorial as a practice (verifying a c function that computes the moving average from an array). I am, however, unable to verify the pre-condition for my sum function regarding pointer validity inside my loop, and have been stuck the whole weekend.
#define MAX_VOLTAGE 3300
/*@
logic integer sum_to_index(int* values, integer index) =
(index < 0)? 0:
values[index] + sum_to_index(values, index - 1);
logic integer sum(int* values, integer length) =
sum_to_index(values, length-1);
*/
/*@
requires valid_array: \valid(values+(0..length-1));
requires valid_length: 0<=length<=50;
requires valid_range: \forall integer i; 0<= i < length ==> 0<=values[i]<=MAX_VOLTAGE;
assigns \nothing;
ensures \result == sum(values, length);
*/
int sum(int *values, unsigned int length) {
int result = 0;
/*@
loop invariant 0 <= i <= length;
loop invariant result == (i == 0 ? 0 : sum_to_index(values, i - 1));
loop invariant result <= i * MAX_VOLTAGE;
loop assigns result, i;
loop variant length - i;
*/
for (int i = 0; i < length; i++) {
result += values[i];
}
return result;
}
/*@
predicate valid_array_r(int* array, unsigned int length) =
\valid_read(array+(0..length-1)) && 0<=length<=INT_MAX;
predicate valid_array_rw(int* array, unsigned int length) =
\valid(array+(0..length-1)) && 0<=length<=INT_MAX;
logic integer average(int* array, integer n) = sum(array, n)/n;
*/
/*@
requires valid_window_size: 0 < window_size <= raw_data_length <= 50;
requires valid_buffer_size: filtered_data_length == raw_data_length - window_size + 1;
requires valid_value_range: \forall integer i; 0 <= i < raw_data_length ==> 0 <= raw_data[i] <= MAX_VOLTAGE;
requires mem_separation: \separated(raw_data+(0..raw_data_length-1), filtered_data+(0..filtered_data_length-1));
requires valid_pointers: valid_array_r(raw_data, raw_data_length) &&
valid_array_rw(filtered_data, filtered_data_length);
assigns filtered_data[0..filtered_data_length-1];
ensures \forall integer i; 0<= i < filtered_data_length ==> filtered_data[i] == average(raw_data+i, window_size);
*/
void moving_average_filter(int* raw_data, unsigned int raw_data_length,
int* filtered_data, unsigned int filtered_data_length,
unsigned int window_size){
/*@
loop invariant 0 <= i <= filtered_data_length;
loop invariant \forall integer k; 0 <= k < i ==> filtered_data[k]==average(raw_data+k, window_size);
loop invariant \forall integer k; 0 <= k < i ==> 0 <= filtered_data[k] <= MAX_VOLTAGE;
loop assigns i, filtered_data[0..i];
loop variant filtered_data_length - i;
*/
for (unsigned int i = 0; i < filtered_data_length; i++) {
filtered_data[i] = sum(raw_data+i, window_size)/window_size;
}
}
I tried adding several different loop invariants, but all failed. I originally thought that through my pre-conditions regarding both window_size, raw_data_length and filtered_data_length, as well as the i in the for loop always being smaller than filtered_data_length that it would be straight forward to prove the array slice validity. What am I doing wrong?
I am using both Alt-Ergo 2.6.0 as well as Z3 4.8.12, running on Ubuntu 24.04
In move_average_filter, the precondition is not validated because sum asks for full validity instead of read validity (and we only have that for raw_data). Thus, we can fix it by weakening the precondition of sum since it does not need to modify the array.
/*@ requires valid_array: \valid_read(values+(0..length-1));
...
*/
int sum(int *values, unsigned int length);
Then, something which is not intuitive. I don't remember if the current "stable" version of the tutorial talks about it, but I'm pretty sure that the one on the master branch does. WP is currently not able to use a loop assigns that depends on a variable which is also assigned. Thus, the recommended way of proceeding is to use an upperbound with a variable that is not modified, and then, if needed, to restrict modified values with an additional invariant. Here, in moving_average_filter, we get:
loop assigns i, filtered_data[0..filtered_data_length-1];
And if it would be needed, we could add the invariant:
loop invariant
\forall integer k ; i <= k < filtered_data_length ==>
filtered_data[k] == \at(filtered_data, Pre);
But for this proof, we do not need it.
Now, we come to the hard part.
First, let us focus on the bounds for filtered_data elements. Basically, the solvers are not able to bound the sum. So let us help them with a simple lemma function that we can then use to get this information.
/*@ ghost
/@ requires \forall integer i ; 0 <= i < len ==> 0 <= array[i] <= MAX_VOLTAGE ;
assigns \nothing ;
ensures 0 <= sum(array, len) <= len * MAX_VOLTAGE ;
@/
void lemma_bound_sum(int* array, unsigned len){
/@ loop invariant 0 <= i <= len ;
loop invariant 0 <= sum(array, i) <= i * MAX_VOLTAGE;
loop assigns i ;
loop variant len - i ;
@/
for(unsigned i = 0 ; i < len ; i++);
}
*/
This function guarantees that if the values are in a range 0 .. MAX_VOLTAGE, then summing len elements does not exceed len * MAX_VOLTAGE. We can thus use this function to get this information in the loop.
for (unsigned int i = 0; i < filtered_data_length; i++) {
//@ ghost lemma_bound_sum(raw_data+i, window_size);
filtered_data[i] = sum(raw_data+i, window_size)/window_size;
}
Finally, the hardest part is to prove that the `average is indeed computed. The reason why it is hard is not really a matter of mathematical complexity even if we need to add the following lemma (proved by CVC5):
//@ lemma div_mul: \forall integer a, b, m ; m > 0 ==> 0 <= a <= b * m ==> 0 <= a / m <= b ;
The actual reason why it is hard is that solvers have a hard time dealing with memory separation for raw_data and filtered_data. So we have to help them a lot with that. Either by providing lemmas, or by using more ghost code. Here, I chose to use ghost code:
for (unsigned int i = 0; i < filtered_data_length; i++) {
//@ ghost top_entry: ;
//@ ghost lemma_bound_sum(raw_data+i, window_size);
filtered_data[i] = sum(raw_data+i, window_size)/window_size;
/*@ assert // memory has not been changed
\forall integer k, x ;
0 <= k < i ==>
0 <= x < window_size ==>
\at((raw_data+k)[x], top_entry) == (raw_data+k)[x];
*/
/*@ ghost // so sums for each k have not been changed
/@ loop invariant 0 <= k <= i+1 ;
loop invariant
\forall integer j ; 0 <= j < k ==>
sum(raw_data+j, window_size) ==
sum{top_entry}(raw_data+j, window_size) ;
loop assigns k ;
loop variant (i + 1) - k ;
@/
for(unsigned k = 0 ; k <= i ; k++){
// because for each element of each sum, the element is the same
// so the sum is the same
/@ loop invariant 0 <= e <= window_size ;
loop invariant sum(raw_data+k, e) == sum{top_entry}(raw_data+k, e);
loop assigns e;
loop variant window_size - e ;
@/
for(unsigned e = 0 ; e < window_size ; e++);
}
*/
/*@ assert // what we get from the code above, this assertion is not necessary
\forall integer k ;
0 <= k <= i ==>
sum(raw_data+k, window_size) ==
sum{LoopCurrent}(raw_data+k, window_size) ;
*/
}
Complete code :
#include <limits.h>
#define MAX_VOLTAGE 3300
/*@
logic integer sum_to_index(int* values, integer index) =
(index < 0)? 0:
values[index] + sum_to_index(values, index - 1);
logic integer sum(int* values, integer length) =
sum_to_index(values, length-1);
*/
/*@
requires valid_array: \valid_read(values+(0..length-1));
requires valid_length: 0<=length<=50;
requires valid_range: \forall integer i; 0<= i < length ==> 0<=values[i]<=MAX_VOLTAGE;
assigns \nothing;
ensures \result == sum(values, length);
*/
int sum(int *values, unsigned int length) {
int result = 0;
/*@
loop invariant 0 <= i <= length;
loop invariant result == (i == 0 ? 0 : sum_to_index(values, i - 1));
loop invariant result <= i * MAX_VOLTAGE;
loop assigns result, i;
loop variant length - i;
*/
for (int i = 0; i < length; i++) {
result += values[i];
}
return result;
}
/*@
predicate valid_array_r(int* array, unsigned int length) =
\valid_read(array+(0..length-1)) && 0<=length<=INT_MAX;
predicate valid_array_rw(int* array, unsigned int length) =
\valid(array+(0..length-1)) && 0<=length<=INT_MAX;
logic integer average(int* array, integer n) = sum(array, n)/n;
*/
/*@ ghost
/@ requires \forall integer i ; 0 <= i < len ==> 0 <= array[i] <= MAX_VOLTAGE ;
assigns \nothing ;
ensures 0 <= sum(array, len) <= len * MAX_VOLTAGE ;
@/
void lemma_bound_sum(int* array, unsigned len){
/@ loop invariant 0 <= i <= len ;
loop invariant 0 <= sum(array, i) <= i * MAX_VOLTAGE;
loop assigns i ;
loop variant len - i ;
@/
for(unsigned i = 0 ; i < len ; i++);
}
*/
//@ lemma div_mul: \forall integer a, b, m ; m > 0 ==> 0 <= a <= b * m ==> 0 <= a / m <= b ;
/*@
requires valid_window_size: 0 < window_size <= raw_data_length <= 50;
requires valid_buffer_size: filtered_data_length == raw_data_length - window_size + 1;
requires valid_value_range: \forall integer i; 0 <= i < raw_data_length ==> 0 <= raw_data[i] <= MAX_VOLTAGE;
requires mem_separation: \separated(raw_data+(0..raw_data_length-1), filtered_data+(0..filtered_data_length-1));
requires valid_pointers: valid_array_r(raw_data, raw_data_length) &&
valid_array_rw(filtered_data, filtered_data_length);
assigns filtered_data[0..filtered_data_length-1];
ensures \forall integer i; 0<= i < filtered_data_length ==> filtered_data[i] == average(raw_data+i, window_size);
*/
void moving_average_filter(int* raw_data, unsigned int raw_data_length,
int* filtered_data, unsigned int filtered_data_length,
unsigned int window_size){
/*@
loop invariant 0 <= i <= filtered_data_length;
loop invariant \forall integer k; 0 <= k < i ==> filtered_data[k]==average(raw_data+k, window_size);
loop invariant \forall integer k; 0 <= k < i ==> 0 <= filtered_data[k] <= MAX_VOLTAGE;
loop assigns i, filtered_data[0..filtered_data_length-1];
loop variant filtered_data_length - i;
*/
for (unsigned int i = 0; i < filtered_data_length; i++) {
//@ ghost top_entry: ;
//@ ghost lemma_bound_sum(raw_data+i, window_size);
filtered_data[i] = sum(raw_data+i, window_size)/window_size;
/*@ assert
\forall integer k, x ;
0 <= k < i ==>
0 <= x < window_size ==>
\at((raw_data+k)[x], top_entry) == (raw_data+k)[x];
*/
/*@ ghost
/@ loop invariant 0 <= k <= i+1 ;
loop invariant
\forall integer j ; 0 <= j < k ==>
sum(raw_data+j, window_size) ==
sum{top_entry}(raw_data+j, window_size) ;
loop assigns k ;
loop variant (i + 1) - k ;
@/
for(unsigned k = 0 ; k <= i ; k++){
/@ loop invariant 0 <= e <= window_size ;
loop invariant sum(raw_data+k, e) == sum{top_entry}(raw_data+k, e);
loop assigns e;
loop variant window_size - e ;
@/
for(unsigned e = 0 ; e < window_size ; e++);
}
*/
/*@ assert
\forall integer k ;
0 <= k <= i ==>
sum(raw_data+k, window_size) ==
sum{LoopCurrent}(raw_data+k, window_size) ;
*/
}
}
Proved automatically with (timeout at 10s):
$ frama-c file.c -wp -wp-rte -wp-prover alt-ergo,cvc5 -wp-timeout 10
[kernel] Parsing file.c (with preprocessing)
[rte:annot] annotating function lemma_bound_sum
[rte:annot] annotating function moving_average_filter
[rte:annot] annotating function sum
[wp] 67 goals scheduled
[wp] Proved goals: 71 / 71
Terminating: 2
Unreachable: 2
Qed: 34 (1ms-14ms-66ms)
Alt-Ergo 2.5.4: 31 (8ms-170ms-4.3s)
CVC5 1.1.2: 2 (21ms-80ms)