Introduzione al model checking

In generale, per model checking si intende un metodo per verificare che un sistema con stati finiti soddisfi una data proprietà o specifica. Tipicamente, questi modelli sono associati a sistemi hardware o software, dove le proprietà interessanti da verificare sono ad esempio proprietà di safety (il programma non va mai in crash) oppure di liveness (il programma non entra mai in un deadlock). Uno dei principali strumenti che viene usato per far sì che i model checker siano utili nella pratica è la categoria dei risolutori SMT.

Risolutori SMT

Tipicamente queste proprietà sui programmi vengono ridotte a espressioni in un linguaggio logico formale, e poi vengono usati risolutori logici per dimostrarle o falsificarle. In particolare, stanno diventando molto popolari i cosiddetti risolutori SAT e SMT, perché nella pratica funzionano particolarmente bene. Un risolutore SMT risolve il problema della Satisfiability Modulo Theories, ovvero determinare se una formula logica ammette un assegnamento che la rende vera. In particolare sono diventati molto popolari risolutori quali z3 oppure cvc5, che mirano a risolvere SMT su istanze che possono essere trovate nella pratica. Per questa ragione, sono diventati uno dei tasselli per moltissime applicazioni, dalla verifica formale alla dimostrazione automatica di teoremi.

Il risolutore SMT z3

Z3 è uno dei più famosi strumenti che permettono di risolvere il problema SMT. Prima di descrivere il suo funzionamento, consideriamo questa funzione scritta in c

int f(int x) {
    if (x < 0 || (x < 20 && x >= 0) || (x > 20)) {
        return 1;
    }
    return 0;
}

Analizzando il codice potremmo chiederci per quali input la funzione ritorna 0. Potremmo provare a capire e interpretare le condizioni, e in effetti in questo caso è molto semplice, ma in presenza di condizioni più complesse potrebbe non essere ovvio con quali input una condizione viene verificata. Possiamo utilizzare z3 esattamente per risolvere questo problema. In questo esempio, verrà utilizzato z3 con la sua interfaccia in Python, che può essere installato tramite il pacchetto pip z3-solver.

Per prima cosa definiamo un nuovo oggetto Solver

import z3

x = z3.Int('x')
s = z3.Solver()

A questo punto aggiungiamo al solver le condizioni che fanno ritornare 0 alla funzione, e stampiamo un modello

s.add(z3.Not(x < 0))
s.add(z3.Not(z3.And(x < 20, x >= 0)))
s.add(z3.Not(x > 20))
s.check()
print(s.model())

L'output del programma è

[x = 20]

Z3 è riuscito a trovare che 20 è un input valido alla funzione affinché ritorni 0. La cosa molto interessante è che se aggiungiamo al solver la condizione x != 20

s.add(x != 20)
print(s.check())

L'output del programma è

unsat

ovvero z3 ha determinato che nessun assegnamento di x soddisfa tutte le condizioni, ovvero il modello è non soddisfacibile, (unsatisfiable). Da questo si può dedurre quindi che x=20 era anche l'unico valore di input per cui la funzione sarebbe ritornata 0. Di seguito viene riportato lo script completo.

import z3

x = z3.Int('x')
s = z3.Solver()

s.add(z3.Not(x < 0))
s.add(z3.Not(z3.And(x < 20, x >= 0)))
s.add(z3.Not(x > 20))
s.check()
print(s.model())

s.add(x != 20)
print(s.check())

Si deve precisare, però, che l'astrazione utilizzata non è del tutto corretta, in quanto stiamo modellando x come un intero, mentre in c gli interi sono rappresentati su un numero fisso di bit, e sono soggetti a overflow e underflow. Per una rappresentazione più accurata in z3 di questi tipi di dati è possibile utilizzare il costrutto BitVec, che modella anche le operazioni aritmetiche di macchina. Inoltre, è possibile modellare altre strutture, come numeri a virgola mobile, liste, strutture dati, e molto altro. Per la documentazione completa si rimanda alla pagina del progetto.