Loop unwinding

I cicli sono trattati in modo particolare da Kani. Prendiamo questo esempio che inizializza un vettore a zero.

#![allow(unused)]
fn main() {
fn initialize_prefix(buffer: &mut [u8], up_to: usize) {
    if up_to > buffer.len() {
        return;
    }

    for i in 0..=up_to {
        buffer[i] = 0;
    }
}
}

Questo codice presenta un errore di tipo off-by-one, possiamo scrivere un proof harness per questa funzione.

#![allow(unused)]
fn main() {
#[cfg(kani)]
#[kani::proof]
fn loop_unwinding() {
    let up_to: usize = kani::any();
    let array = [1; 16];
    initialize_prefix(&mut array, up_to);
}
}

Se proviamo a eseguire così il verificatore non terminerà mai. Questo perché Kani ha l'approccio ai loop chiamato loop unwinding, ovvero mette in sequenza le istruzioni del corpo del ciclo, e verifica ogni possibile caso. Possiamo istruire su quanti cicli espandere tramite la macro kani::unwind.

#![allow(unused)]
fn main() {
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(20)]
fn loop_unwinding() {
    let up_to: usize = kani::any();
    let array = [1; 16];
    initialize_prefix(&mut array, up_to);
}
}

Adesso Kani riesce a eseguire tutto il loop in tempo finito, e trova l'errore.

 ** 1 of 74 failed
Failed Checks: index out of bounds: the length is less than or equal to the given index
 File: "src/main.rs", line 53, in initialize_prefix

VERIFICATION:- FAILED
Verification Time: 0.70454884s

Summary:
Verification failed for - loop_unwinding
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

Risoluzione del problema

Proviamo adesso a risolvere il bug di tipo off-by-one, modificando la condizione all'interno dell'if.

#![allow(unused)]
fn main() {
fn initialize_prefix(buffer: &mut [u8], up_to: usize) {
    if up_to >= buffer.len() {
        return;
    }

    for i in 0..=up_to {
        buffer[i] = 0;
    }
}
}

Eseguendo Kani, la verifica andrà adesso a buon fine, e questo ci garantisce che la funzione non presenterà problemi.

SUMMARY:
 ** 0 of 74 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.6491398s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.