Riepilogo Tecnico: Soddisfacibilità Modulo Array Costanti Estensionali

Enunciato del Problema

Il ragionamento sulle strutture dati di tipo array, in particolare in combinazione con interi macchina, è un requisito fondamentale per la verifica hardware e software. La teoria standard delle soddisfazioni modulo teorie (SMT) degli array estensionali, definita in SMT-LIB e assiomatizzata da McCarthy, fornisce gli operatori select (lettura) e store (scrittura) insieme a un assioma di estensionalità. Sebbene sufficiente per molte attività di verifica, questa teoria manca di concisione quando si modellano array inizializzati con un valore predefinito (ad esempio, memoria inizializzata a zero).

Nella teoria standard, tale inizializzazione deve essere espressa tramite espressioni store profondamente nidificate che scrivono il valore predefinito su ogni indice rilevante. Ciò porta a imprecisioni nella modellazione (gli indici possono essere sovrascritti solo esplicitamente) e a gravi inefficienze nelle procedure di risoluzione a causa della profondità delle catene di store.

L'estensione della teoria con array costanti—array che memorizzano un singolo elemento su ogni indice—offre una soluzione concisa. Tuttavia, le procedure decisionali esistenti per gli array costanti estensionali sono limitate a domini di indici infiniti. Per i domini di indici finiti, i solver SMT esistenti supportano solo frammenti non estensionali o, nel caso di alcuni solver, producono risposte errate quando ragionano sull'estensionalità su array costanti con indici finiti. La sfida principale risiede nel determinare se due sequenze di operazioni di store su diversi array costanti con domini finiti possano essere rese uguali aggiornando sufficientemente gli indici, un problema che non si presenta nel caso infinito.

Metodologia

Gli autori presentano una nuova procedura decisionale per la teoria degli array costanti estensionali ($T_{\langle A \rangle}$) che supporta domini di indici arbitrari, inclusi quelli finiti. La procedura è formalizzata come un calcolo astratto, CAEXT, che generalizza ed estende la procedura Lemmas on Demand (LOD) per gli array estensionali (DPA) presentata in lavori precedenti.

Il Calcolo CAEXT

Il calcolo opera su configurazioni $\langle A, I, \pi \rangle$, dove $A$ è un insieme di letterali piatti, $I$ è un'interpretazione nella teoria vuota ($T_E$) e $\pi$ è una mappa di passi di propagazione. La procedura evita l'introduzione di letture virtuali per tutti gli indici (il che è impossibile per domini infiniti e computazionalmente costoso per domini finiti di grandi dimensioni) propagando i valori predefiniti e tracciando gli indici aggiornati.

I componenti chiave del calcolo includono:

1. Calcolo di Base (AEXT): Generalizza la procedura LOD a sort arbitrari di indici ed elementi, disaccoppiandola da combinazioni di teorie specifiche. Propaga le informazioni di lettura basandosi sugli assiomi di lettura-sopra-scrittura di McCarthy (row-eq, row-ne) e sull'assioma di estensionalità (ext).
2. Estensione agli Array Costanti:
   • Propagazione dei Valori Predefiniti: Invece di generare letture per ogni indice, il calcolo propaga il valore predefinito $v$ di un array costante $\langle v \rangle$ ad altri array. Mantiene un insieme di indici aggiornati $I(a, \langle v \rangle)$, che rappresentano gli indici in cui l'array $a$ differisce dal valore predefinito $\langle v \rangle$ lungo il percorso di propagazione.
   • Rilevamento dei Conflitti (CongC): Quando due diversi valori predefiniti $v$ e $w$ vengono propagati allo stesso array $a$, il calcolo verifica se l'insieme degli indici aggiornati $I(a, \langle v \rangle) \cup I(a, \langle w \rangle)$ copre l'intero dominio degli indici. Se il dominio è finito e gli indici aggiornati non coprono tutti gli indici possibili, sorge un conflitto a meno che $v \approx w$.
   • Codifica DistinctN: Per gestire in modo efficiente la formula quantificata $\exists i : \sigma. \bigwedge_{k \in I} i \neq k$ (che verifica se esiste un indice non aggiornato), l'implementazione codifica questa come un vincolo specializzato distinctN. Questo verifica se l'insieme degli indici aggiornati contiene almeno $n$ valori distinti, dove $n$ è la dimensione del dominio degli indici.

Implementazione

La procedura decisionale è implementata nel solver SMT all'avanguardia Bitwuzla. Si integra perfettamente con l'architettura LOD esistente di Bitwuzla, dove il solver di bit-vettori fornisce l'interpretazione $I$. L'implementazione include ottimizzazioni come l'espansione lazy dei vincoli distinctN e la ricerca in ampiezza per i percorsi di propagazione per minimizzare il sovraccarico di memoria.

Contributi Chiave

1. Generalizzazione di LOD: Gli autori generalizzano la procedura LOD per gli array estensionali con bit-vettori di dimensione fissa a sort arbitrari di indici ed elementi.
2. Calcolo Astratto AEXT: Presentano AEXT come un calcolo astratto e disaccoppiato per la teoria estensionale degli array, indipendente dal paradigma di risoluzione LOD.
3. Estensione agli Array Costanti (CAEXT): Estendono AEXT per gestire gli array costanti estensionali, dimostrando la correttezza refutazionale (se viene riportato unsat, l'input è insoddisfacibile) e la correttezza di soddisfacibilità (se viene raggiunta una configurazione satura senza unsat, l'input è soddisfacibile).
4. Implementazione e Valutazione: La procedura è implementata in Bitwuzla e valutata su benchmark diversificati, dimostrando significativi miglioramenti delle prestazioni rispetto a Bitwuzla di base e ad altri solver leader (Z3, cvc5, MathSAT5).

Risultati

La valutazione è stata condotta su cinque set di benchmark: smtlib (logiche quantificate), mbqi (sotto-query dall'istanziazione di quantificatori basata su modelli), k-ind (verifica incrementale di modelli hardware), hevm (macchina virtuale Ethereum) e crafted (benchmark sintetici progettati specificamente per testare l'estensionalità degli array costanti finiti).

• Prestazioni: Bitwuzla con la nuova procedura (Bitwuzla⟨A⟩) ha superato significativamente tutti gli altri solver. Sul set smtlib, il numero di benchmark risolti è aumentato di un fattore 5 rispetto a Bitwuzla di base (3.545 contro 717). Sul set mbqi, Bitwuzla⟨A⟩ ha risolto tutte le 4.147 query, mentre la versione di base ne ha risolte solo 4.
• Correttezza: Sul set crafted⟨A⟩, che codifica uguaglianze su array costanti finiti con diversi valori predefiniti, Bitwuzla⟨A⟩ è stato l'unico solver a fornire risposte corrette per tutte le istanze. Z3 e MathSAT5 hanno accettato gli input ma hanno riportato risposte errate per un numero significativo di benchmark. cvc5 e Bitwuzla di base hanno rifiutato completamente gli input a causa della mancanza di supporto.
• Verifica della Correttezza: Gli autori hanno verificato i modelli prodotti dai solver sul set crafted⟨A⟩. Solo Bitwuzla⟨A⟩ ha prodotto modelli coerenti con le proprie affermazioni di soddisfacibilità. Z3 e MathSAT5 hanno prodotto modelli che, quando assertati nuovamente sulle formule originali, hanno portato a contraddizioni.

Significato

Il documento afferma che la procedura decisionale proposta espande significativamente le capacità di risoluzione di Bitwuzla, consentendogli di gestire problemi che coinvolgono array costanti estensionali con domini di indici finiti che in precedenza erano irrisolvibili o gestiti in modo errato da altri strumenti.

Il lavoro affronta una lacuna critica nella risoluzione SMT: mentre gli array costanti sono un pattern di modellazione standard per l'inizializzazione della memoria, i solver esistenti o mancano di supporto per essi nei domini finiti o forniscono risultati insoddisfacenti. Fornendo una procedura decisionale corretta e completa per l'intera teoria degli array costanti estensionali (sia finiti che infiniti), questo lavoro abilita una verifica più accurata ed efficiente in applicazioni come la verifica di modelli hardware e la verifica di contratti intelligenti (in particolare per la Macchina Virtuale Ethereum). Gli autori notano che, sebbene la loro valutazione si sia concentrata sui domini finiti, la procedura è agnostica rispetto all'architettura del solver sottostante e supporta pienamente anche il caso del dominio infinito.