[WP] [RTE] Unable to verify valid memory access in array using bitwise-ANDed index when array is function parameter
Steps to reproduce the issue
With Alt-Ergo 2.4.1 installed:
frama-c -wp -wp-rte poc.c
/ frama-c-gui -wp -wp-rte poc.c
using poc.c :
/*@
requires \valid_read(arr + (0 .. 3));
assigns \nothing;
*/
int foo(const int arr[const static 4]) {
const unsigned int h = 7 & 0b11;
//@ assert 0 <= h < 4;
const int hvalue = arr[h];
const unsigned int i = 7 % 4;
//@ assert 0 <= i < 4;
const int ivalue = arr[i];
/*@
loop invariant 0 <= s <= 8;
loop assigns s;
loop variant 8 - s;
*/
for (unsigned int s = 0; s < 8; s += 1) {
const unsigned int j = s & 0b11;
//@ assert 0 <= j < 4;
const int jvalue = arr[j];
const unsigned int k = s % 4;
//@ assert 0 <= k < 4;
const int kvalue = arr[k];
}
return 0;
}
/*@
assigns \nothing;
*/
int main(void) {
const int arr[4] = {0, 1, 2, 3};
const unsigned int h = 7 & 0b11;
//@ assert 0 <= h < 4;
const int hvalue = arr[h];
const unsigned int i = 7 % 4;
//@ assert 0 <= i < 4;
const int ivalue = arr[i];
/*@
loop invariant 0 <= s <= 8;
loop assigns s;
loop variant 8 - s;
*/
for (unsigned int s = 0; s < 8; s += 1) {
const unsigned int j = s & 0b11;
//@ assert 0 <= j < 4;
const int jvalue = arr[j];
const unsigned int k = s % 4;
//@ assert 0 <= k < 4;
const int kvalue = arr[k];
}
foo(arr);
return 0;
}
Expected behaviour
All goals proved.
Actual behaviour
$ frama-c -wp -wp-rte poc.c
[kernel] Parsing poc.c (with preprocessing)
[rte] annotating function foo
[rte] annotating function main
[wp] 34 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_foo_assert_rte_mem_access_3 : Timeout (Qed:9ms) (10s)
[wp] Proved goals: 33 / 34
Qed: 23 (2ms-5ms-14ms)
Alt-Ergo 2.4.1: 10 (7ms-17ms-30ms) (556) (interrupted: 1)
33/34 goals proved.
The verification of /*@ assert rte: mem_access: \valid_read(arr + j); */
for code const int jvalue = arr[j];
in function foo
is not successful.
From a naive perspective, the arr[j]
accesses in main and foo are equivalent, so the assert in foo should be verifiable if the assert in main is.
(I am aware that a different assert is generated in main: /*@ assert rte: index_bound: j < 4; */
)
Also, the //@ assert 0 <= j < 4;
immediately before the access can be verified, both in main and foo, so it seems the rte assert should be able to be verified also.
Contextual information
- Frama-C installation mode: opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP, RTE
- OS name: Manjaro Linux
- OS version: Qonos 21.2.4
Additional information (optional)
The poc.c is a simplified proof of concept, but I did hit this situation when working on a real program.
To be explicit about the provers involved:
$ why3 config detect
Found prover Alt-Ergo version 2.4.1, OK.
1 prover(s) added
Save config to /home/user/.why3.conf
I was uncertain whether to submit this here or at the alt-ergo issues.
Apologies if this is the wrong place. Let me know if I should post there instead.