Sintesi Tecnica: Ragionamento Automatizzato con Datatype Annidati

1. Definizione del Problema

La teoria dei datatypes di SMT-LIB fornisce una codifica conveniente per strutture dati come liste e alberi, essenziali per la verifica del software. Tuttavia, la sua espressività è limitata dalla mancanza di operatori di aggiornamento e di capacità di accesso casuale. Per affrontare questo problema, si tenta spesso una combinazione ingenua di datatypes con la teoria degli array.

Il problema centrale identificato in questo lavoro è che tale combinazione ingenua introduce modelli non standard. Nello specifico, il principio di aciclicità — che stabilisce che un valore di datatype non può contenere se stesso — viene eluso quando sono coinvolti gli array. Un valore di datatype può apparire come elemento di un array dove quell'array è, a sua volta, un campo dello stesso valore di datatype. Questo crea un ciclo che la combinazione standard di teorie (tramite Nelson-Oppen) non riesce a rilevare perché il ciclo è "diviso" tra i componenti datatype e array. Questi modelli non standard sono indesiderabili poiché non si allineano con la semantica intuitiva delle strutture dati annidate destinate alla verifica.

2. Metodologia

Gli autori propongono una teoria dei datatypes annidati che esclude esplicitamente questi modelli non standard. La metodologia prevede due componenti principali: una definizione formale della teoria e una procedura decisionale basata sulla riduzione.

2.1. Definizione Formale

La teoria è definita limitando la combinazione standard di datatypes e array.

• Ben fondatezza: Gli autori introducono una nuova definizione di sort ben fondati (Definizione 10) che tiene conto della presenza di sort di array. Ciò assicura che la struttura ricorsiva dei datatypes rimanga ben fondata anche quando sono coinvolti elementi di array.
• Relazione NDT: Per escludere i modelli non standard, gli autori definiscono una relazione $\mathcal{R}_{\mathcal{A}}$ sulle strutture (Definizione 16). Questa relazione collega i termini ai loro sottotermi e gli array ai loro elementi. Una struttura è considerata un valido NDT structure solo se questa relazione è ben fondata. Ciò esclude efficacemente i cicli in cui un valore di datatype riferisce indirettamente a se stesso attraverso un array.

2.2. Procedura Decisionale

Il documento presenta una procedura decisionale che riduce il problema della soddisfacibilità per i datatypes annidati alla combinazione (ingenua) di datatypes, array e funzioni non interpretate (EUF). La procedura opera come segue:

1. Traduzione della Firma: Viene costruita una nuova firma $\Sigma_{\varphi}$.

   • I sort di array sono divisi in due componenti: un sort di datatype ($\sigma^*$) utilizzato per il controllo dei cicli e un sort di array ($\sigma'$) utilizzato per il ragionamento standard sugli array.
   • I costruttori di datatype sono copiati per operare sui nuovi sort.
   • Vengono introdotti costruttori speciali per rappresentare gli array come tuple finite, catturando gli elementi acceduti dagli indici presenti nella formula di input.
   • Funzioni non interpretate ($f_A, g_A$) vengono aggiunte per collegare le rappresentazioni dei sort di array ($\sigma'$) con le rappresentazioni dei sort di datatype ($\sigma^*$).

2. Traduzione della Formula: La formula di input $\varphi$ viene tradotta in $\text{trFormula}(\varphi)$.

   • I letterali standard (ad es. $x = \text{select}(a, i)$) sono mappati nei loro corrispettivi nella nuova firma.
   • Lemmi: Fondamentalmente, la traduzione è aumentata da un insieme di lemmi ($L(\varphi)$) che impongono la corrispondenza tra le operazioni di array nella formula originale e la rappresentazione basata su tuple nella nuova firma. Questi lemmi assicurano che i "cicli nascosti" siano esposti nella formula tradotta.

3. Risoluzione: La formula risultante $\text{trFormula}(\varphi)$ viene controllata per la soddisfacibilità utilizzando esistenti solver SMT in grado di gestire la combinazione di datatypes, array ed EUF (ad es. tramite il metodo Nelson-Oppen).

2.3. Correttezza e Decidibilità

Il documento prova che la traduzione preserva la soddisfacibilità (Teorema 31) sotto l'assunto che la teoria dei datatype sia stabilmente infinita rispetto ai sort condivisi. Di conseguenza, la teoria dei datatypes annidati è decidibile (Teorema 32).

3. Contributi Chiave

Il documento apporta tre contributi primari:

1. Definizione della Teoria: L'introduzione di una precisa teoria dei datatypes annidati che previene modelli ciclici non standard derivanti dall'interazione tra datatypes e array.
2. Procedura Decisionale: Una procedura decisionale basata sulla riduzione che trasforma problemi di datatypes annidati in combinazioni standard di teorie aumentate con funzioni non interpretate.
3. Implementazione e Valutazione: Un'implementazione prototipale all'interno del solver SMT cvc5 e una valutazione empirica che dimostra l'efficacia dell'approccio.

4. Risultati Sperimentali

Gli autori hanno valutato la loro implementazione su due suite di benchmark:

• Benchmark Sintetici: Formule progettate sistematicamente per creare cicli di varie dimensioni tra datatypes e array.
  • Su istanze insoddisfacibili (cicli presenti), cvc5 ha risolto tutti i 500 benchmark, superando Z3 (che ha risolto in media 299,8, sebbene la tabella indichi che Z3 abbia risolto meno istanze totali).
  • Su istanze soddisfacibili (cicli interrotti), cvc5 ha risolto 25 su 50, mentre Z3 ne ha risolti solo 1.
• Benchmark del Mondo Reale: Formule derivate dallo strumento di verifica Move Prover, che utilizza datatypes annidati per modellare strutture dati persistenti in smart contract.
  • Entrambi i solver hanno risolto tutti i benchmark di Move Prover rapidamente.
  • cvc5 è stato comparabile o leggermente più veloce di Z3 sulle istanze soddisfacibili.

5. Significato e Rivendicazioni

Il documento afferma che la teoria proposta e la procedura decisionale affrontano con successo il problema dei modelli non standard nella combinazione di datatypes e array, un problema che gli esistenti solver (come Z3) possono gestire implicitamente ma senza una precisa definizione teorica o una garanzia di correttezza riguardo all'aciclicità.

Gli autori dichiarano che il loro approccio è "promettente", mostrando di essere competitivo con le soluzioni esistenti nei benchmark del mondo reale e superiore nei benchmark sintetici progettati per testare rigorosamente il rilevamento dei cicli. Essi sottolineano che il lavoro è stato motivato dalle necessità di Move Prover, dove tali strutture annidate sono comuni.

Il documento si conclude con modestia, notando che, sebbene l'attuale lavoro risolva il caso specifico degli array, il problema più ampio dei cicli non rilevati esiste per altri datastructure (sequenze, set, ecc.). Gli autori suggeriscono che la loro soluzione per gli array possa servire come base per una soluzione più generale ai problemi di combinazione ingenua delle teorie. Il lavoro futuro è identificato nell'espansione del supporto alla risoluzione incrementale e ai quantificatori.