I am attempting to add ACSL annotations to some classic algorithms from Introduction to Algorithms and verify their correctness using Frama-C's WP plugin, but I have encountered some issues.
Here is my code:
/*@
requires n > 0;
requires \valid(a + (0 .. n-1));
ensures \result >= 0 ==> 0 <= \result < n && a[\result] == key;
ensures \result < 0 ==> \forall integer j; 0 <= j < n ==> a[j] != key;
*/
int LinearSearch(int a[], int n, int key) {
int ret = -1;
int i = 0;
/*@
loop invariant ret >= 0 ==> 0 <= ret < n && a[ret] == key;
loop invariant ret < 0 ==> 0 <= i <= n && \forall integer j; 0 <= j < i ==> a[j] != key;
loop assigns i,ret;
*/
while (ret == -1 && i < n)
{
if (a[i] == key) { ret = i; }
else { i = i + 1; }
}
return ret;
}
When I run frama-c -wp -wp-prover Alt-Ergo,Z3 -wp-print -wp-timeout 20 _linear_select.c I am getting the following error:
[kernel] Parsing Benchmark/acsl-algorithms_verified/_select.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
[wp] [Qed] Goal typed_LinearSearch_ensures : Valid (9ms)
[wp] [Alt-Ergo ] Goal typed_LinearSearch_loop_invariant_preserved : Valid (Qed:4ms) (17ms) (55)
[wp] [Qed] Goal typed_LinearSearch_loop_invariant_established : Valid
[wp] [Alt-Ergo ] Goal typed_LinearSearch_loop_invariant_2_preserved : Valid (Qed:5ms) (23ms) (188)
[wp] [Qed] Goal typed_LinearSearch_loop_invariant_2_established : Valid (1ms)
[wp] [Qed] Goal typed_LinearSearch_loop_assigns : Valid
[wp] [Failed] Goal typed_LinearSearch_ensures_2
Z3 4.8.6: Timeout (Qed:12ms) (20s)
Alt-Ergo : Timeout (Qed:12ms) (20s)
[wp] Proved goals: 6 / 7
Qed: 4 (0.26ms-4ms-9ms)
Alt-Ergo : 2 (17ms-23ms) (188) (interrupted: 1)
Z3 4.8.6: 1 (80ms) (467460) (interrupted: 1)
------------------------------------------------------------
Function LinearSearch
------------------------------------------------------------
Goal Post-condition (file Benchmark/acsl-algorithms_verified/_select.c, line 4) in 'LinearSearch':
Prove: true.
Prover Qed returns Valid (9ms)
------------------------------------------------------------
Goal Post-condition (file Benchmark/acsl-algorithms_verified/_select.c, line 5) in 'LinearSearch':
Let x = Mint_0[shift_sint32(a, ret_0)].
Assume {
Type: is_sint32(LinearSearch_0) /\ is_sint32(i_1) /\ is_sint32(key_0) /\
is_sint32(n) /\ is_sint32(ret_0) /\
is_sint32(Mint_0[shift_sint32(a, -1)]) /\
is_sint32(Mint_0[shift_sint32(a, LinearSearch_0)]) /\ is_sint32(x).
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: (LinearSearch_0 < 0) /\ (0 <= i) /\ (i < n).
(* Pre-condition *)
Have: 0 < n.
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(a, 0), n).
(* Invariant *)
Have: ((0 <= ret_0) -> ((x = key_0) /\ (ret_0 < n))).
(* Invariant *)
Have: ((ret_0 < 0) ->
((0 <= i_1) /\ (i_1 <= n) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(Mint_0[shift_sint32(a, i_2)] != key_0)))))).
If ret_0 = (-1)
Then { (* Else *) Have: n <= i_1. Have: LinearSearch_0 = (-1). }
Else { Have: ret_0 = LinearSearch_0. }
}
Prove: Mint_0[shift_sint32(a, i)] != key_0.
Prover Z3 4.8.6 returns Timeout (Qed:12ms) (20s)
Prover Alt-Ergo returns Timeout (Qed:12ms) (20s)
------------------------------------------------------------
Goal Preservation of Invariant (file Benchmark/acsl-algorithms_verified/_select.c, line 11):
Let x = Mint_0[shift_sint32(a, i_1)].
Let x_1 = Mint_0[shift_sint32(a, ret_0)].
Assume {
Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(key_0) /\ is_sint32(n) /\
is_sint32(ret_0) /\ is_sint32(Mint_0[shift_sint32(a, -1)]) /\
is_sint32(x) /\ is_sint32(x_1).
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: 0 <= ret_0.
(* Pre-condition *)
Have: 0 < n.
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(a, 0), n).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= n) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(Mint_0[shift_sint32(a, i_2)] != key_0)))).
(* Then *)
Have: i_1 < n.
If x = key_0
Then { Have: (i_1 = i) /\ (ret_0 = i) /\ (ret_0 = i_1). }
Else { Have: ret_0 = (-1). }
}
Prove: (x_1 = key_0) /\ (ret_0 < n).
Prover Z3 4.8.6 returns Valid (Qed:4ms) (80ms) (467460)
Prover Alt-Ergo returns Valid (Qed:4ms) (17ms) (55)
------------------------------------------------------------
Goal Establishment of Invariant (file Benchmark/acsl-algorithms_verified/_select.c, line 11):
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
Goal Preservation of Invariant (file Benchmark/acsl-algorithms_verified/_select.c, line 12):
Let x = Mint_0[shift_sint32(a, i_2)].
Assume {
Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(i_2) /\
is_sint32(key_0) /\ is_sint32(n) /\ is_sint32(ret_0) /\
is_sint32(Mint_0[shift_sint32(a, -1)]) /\ is_sint32(x) /\
is_sint32(Mint_0[shift_sint32(a, ret_0)]).
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: ret_0 < 0.
(* Pre-condition *)
Have: 0 < n.
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(a, 0), n).
(* Invariant *)
Have: (0 <= i_2) /\ (i_2 <= n) /\
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_2) ->
(Mint_0[shift_sint32(a, i_3)] != key_0)))).
(* Then *)
Have: i_2 < n.
If x = key_0
Then { Have: i_2 = i. Have: ret_0 = i. }
Else { Have: (i_2 = i_1) /\ (ret_0 = (-1)). Have: (1 + i_1) = i. }
}
Prove: (0 <= i) /\ (i <= n) /\
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i) ->
(Mint_0[shift_sint32(a, i_3)] != key_0)))).
Prover Alt-Ergo returns Valid (Qed:5ms) (23ms) (188)
------------------------------------------------------------
Goal Establishment of Invariant (file Benchmark/acsl-algorithms_verified/_select.c, line 12):
Prove: true.
Prover Qed returns Valid (1ms)
------------------------------------------------------------
Goal Loop assigns (file Benchmark/acsl-algorithms_verified/_select.c, line 13):
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
[wp:pedantic-assigns] Benchmark/acsl-algorithms_verified/_select.c:7: Warning:
No 'assigns' specification for function 'LinearSearch'.
Callers assumptions might be imprecise.
I want to understand what led to this outcome. My Frama-C version is 25.0 (Manganese).
Additionally, I attempted to verify semantically equivalent annotations and code using Dafny. The code is as follows:
method LinearSearch(a: array<int>, key: int) returns (ret: int)
requires a.Length > 0
ensures ret >= 0 ==> 0 <= ret < a.Length && a[ret] == key
ensures ret < 0 ==> forall j :: 0 <= j < a.Length ==> a[j] != key
{
ret := -1;
var i := 0;
while (ret == -1 && i < a.Length)
invariant ret >= 0 ==> 0 <= ret < a.Length && a[ret] == key
invariant ret < 0 ==> 0 <= i <= a.Length && forall j :: 0 <= j < i ==> a[j] != key
{
if (a[i] == key) { ret := i; }
else { i := i + 1; }
}
return ret;
}
Dafny successfully verified the aforementioned algorithm. I wish to understand what differences between Frama-C and Dafny led to this discrepancy in verification results.
I haven't checked with 25.0 Manganese, but with 31.0-beta Gallium, it seems indeed that Frama-C/WP and/or the Alt-Ergo prover has trouble determining that if you exit the loop while ret is still -1 it implies that i==n (from which the second ensures follows easily from the second loop invariant). If you explicitly add another invariant, namely loop invariant -1 <= ret < n;, then all proof obligations gets discharged.
Full file (notice that I added a loop variant as well since newer Frama-C version (>= 30.0 IIRC) will by default attempt to prove termination as well):
/*@
requires n > 0;
requires \valid(a + (0 .. n-1));
ensures \result >= 0 ==> 0 <= \result < n && a[\result] == key;
ensures \result < 0 ==> \forall integer j; 0 <= j < n ==> a[j] != key;
*/
int LinearSearch(int a[], int n, int key) {
int ret = -1;
int i = 0;
/*@
loop invariant -1 <= ret < n;
loop invariant ret >= 0 ==> 0 <= ret < n && a[ret] == key;
loop invariant ret == -1 ==> 0 <= i <= n && \forall integer j; 0 <= j < i ==> a[j] != key;
loop assigns i,ret;
loop variant n - i - ret ;
*/
while (ret == -1 && i < n)
{
if (a[i] == key) { ret = i; }
else { i = i + 1; }
}
return ret;
}
frama-c -wp -wp-rte linear_search.c then gives:
[kernel] Parsing linear_search.c (with preprocessing)
[rte:annot] annotating function LinearSearch
[wp] 13 goals scheduled
[wp] [Cache] found:7
[wp] Proved goals: 15 / 15
Terminating: 1
Unreachable: 1
Qed: 6 (4ms-6ms-21ms)
Alt-Ergo 2.6.2: 7 (12ms-16ms-23ms)
[wp:pedantic-assigns] linear_search.c:7: Warning:
No 'assigns' specification for function 'LinearSearch'.
Callers assumptions might be imprecise.