Variabili non deterministiche

Nel contesto della verifica formale, le variabili non deterministiche giocano un ruolo cruciale, specialmente quando si tratta di esplorare tutte le possibili esecuzioni di un programma. Abbiamo già visto l'uso di variabili non deterministiche, e adesso ne faremo altri esempi

Come abbiamo visto, le variabili non deterministiche sono variabili il cui valore non è fissato durante l'esecuzione dell'analisi. Invece di avere un valore predeterminato, queste variabili possono assumere qualsiasi valore all'interno di un insieme specificato. Questo approccio è utile per simulare una varietà di scenari e per garantire che il programma gestisca correttamente tutti i possibili casi.

Variabili non deterministiche intere

Supponiamo di voler verificare che una funzione che calcola il quadrato di un numero intero non produca un overflow. Utilizziamo una variabile non deterministica per rappresentare l'input della funzione.

#![allow(unused)]
fn main() {
fn square(x: i32) -> i32 {
    x * x
}

#[kani::proof]
fn check_square() {
    let x: i32 = kani::any();
    // Verifica che il risultato sia non negativo e che non ci sia overflow
    let result = square(x);
    assert!(result >= 0, "Result should be non-negative");
}
}

In questo esempio, kani::any() crea una variabile non deterministica x che può assumere qualsiasi valore i32. Kani esplora tutti i valori possibili per x, verificando che la funzione square non produca risultati negativi e non causi overflow. Il codice presenta possibilità di integer overflow, quindi l'analisi fallisce.

SUMMARY:
 ** 1 of 4 failed
Failed Checks: attempt to multiply with overflow
 File: "src/main.rs", line 58, in square

VERIFICATION:- FAILED

Variabili non deterministiche booleane

Consideriamo una funzione che esegue operazioni diverse in base al valore di un flag booleano. Utilizziamo una variabile non deterministica per rappresentare questo flag.

#![allow(unused)]
fn main() {
fn toggle(value: i32, flag: bool) -> i32 {
    if flag {
        value + 1
    } else {
        value - 1
    }
}

#[kani::proof]
fn check_toggle() {
    let value: i32 = kani::any();
    let flag: bool = kani::any();
    let result = toggle(value, flag);
    // Verifica che il risultato sia sempre un valore intero valido
    assert!(result >= i32::MIN && result <= i32::MAX);
}
}

In questo esempio, kani::any() è utilizzato per creare una variabile non deterministica flag di tipo booleano. L'esecuzione di Kani verifica che, indipendentemente dal valore di flag, la funzione toggle produca sempre un valore intero valido. Infatti, questa funzione può dare sia overflow che underflow, a seconda del valore di flag. Il risultato dell'analisi riporta due controlli falliti.

 ** 2 of 3 failed
Failed Checks: attempt to add with overflow
 File: "src/main.rs", line 72, in toggle
Failed Checks: attempt to subtract with overflow
 File: "src/main.rs", line 74, in toggle

VERIFICATION:- FAILED

Variabili non deterministiche di tipo array

Come abbiamo già visto, è possibile creare variabili non deterministiche di tipo array e anche Vec, anche con dimensione anch'essa non deterministica.

#![allow(unused)]
fn main() {
#[cfg(kani)]
#[kani::proof]
fn bound_check() {
    let size: usize = kani::any();
    kani::assume(size < 4096);
    let index: usize = kani::any();
    let array: Vec<u32> = vec![0; size];
    // ...
}
}

Questo proof harness controllerà l'esecuzione per tutti i vettori di dimensione minore di 4096.