Technische Zusammenfassung: Erfüllbarkeit modulo extensionaler konstanter Arrays

Problemstellung

Das Schließen über Array-Datenstrukturen, insbesondere in Kombination mit Maschinen-Integer, ist eine grundlegende Anforderung für die Hardware- und Softwareverifikation. Die Standard-Theorie der Erfüllbarkeit modulo Theorien (SMT) für extensionale Arrays, wie in SMT-LIB definiert und von McCarthy axiomatisiert, bietet die Operatoren select (Lesen) und store (Schreiben) sowie ein Extensionalitätsaxiom. Obwohl diese Theorie für viele Verifikationsaufgaben ausreicht, fehlt ihr die Kompaktheit bei der Modellierung von Arrays, die mit einem Standardwert initialisiert wurden (z. B. speicherbereiche, die mit Null initialisiert sind).

In der Standardtheorie muss eine solche Initialisierung durch tief verschachtelte store-Ausdrücke ausgedrückt werden, die den Standardwert an jeden relevanten Index schreiben. Dies führt zu Modellierungsungenauigkeiten (Indizes können nur explizit überschrieben werden) und zu schweren Ineffizienzen in den Löseverfahren aufgrund der Tiefe der store-Ketten.

Die Erweiterung der Theorie um konstante Arrays – Arrays, die an jedem Index dasselbe Element speichern – bietet eine kompakte Lösung. Bestehende Entscheidungsprozeduren für extensionale konstante Arrays sind jedoch auf unendliche Indexdomänen beschränkt. Für endliche Indexdomänen unterstützen bestehende SMT-Löser entweder nur nicht-extensionale Fragmente oder liefern, im Fall einiger Löser, falsche Antworten beim Schließen über Extensionalität bei konstanten Arrays mit endlichen Indizes. Die Kernherausforderung besteht darin, festzustellen, ob zwei Folgen von store-Operationen über verschiedene konstante Arrays mit endlichen Domänen durch hinreichendes Aktualisieren der Indizes gleich gemacht werden können – ein Problem, das im unendlichen Fall nicht auftritt.

Methodik

Die Autoren stellen ein neuartiges Entscheidungsverfahren für die Theorie extensionaler konstanter Arrays ($T_{\langle A \rangle}$) vor, das beliebige Indexdomänen, einschließlich endlicher, unterstützt. Das Verfahren wird als abstrakter Kalkül CAEXT formalisiert, der das Lemmas-on-Demand-Verfahren (LOD) für extensionale Arrays (DPA) aus früheren Arbeiten verallgemeinert und erweitert.

Der Kalkül CAEXT

Der Kalkül arbeitet auf Konfigurationen $\langle A, I, \pi \rangle$, wobei $A$ eine Menge flacher Literale ist, $I$ eine Interpretation in der leeren Theorie ($T_E$) darstellt und $\pi$ eine Abbildung von Propagierungsschritten ist. Das Verfahren vermeidet die Einführung virtueller Lesevorgänge für alle Indizes (was für unendliche Domänen unpraktikabel und für große endliche Domänen rechenintensiv ist), indem es Standardwerte propagiert und aktualisierte Indizes verfolgt.

Zu den Schlüsselkomponenten des Kalküls gehören:

1. Basis-Kalkül (AEXT): Verallgemeinert das LOD-Verfahren auf beliebige Index- und Elementsorten und entkoppelt es von spezifischen Theoriekombinationen. Es propagiert Leseinformationen basierend auf McCarthys Axiomen für Lesen über Schreiben (row-eq, row-ne) sowie dem Extensionalitätsaxiom (ext).
2. Erweiterung um konstante Arrays:
   • Propagierung von Standardwerten: Anstatt Lesevorgänge für jeden Index zu generieren, propagiert der Kalkül den Standardwert $v$ eines konstanten Arrays $\langle v \rangle$ zu anderen Arrays. Er verwaltet eine Menge aktualisierter Indizes $I(a, \langle v \rangle)$, die die Indizes darstellen, an denen sich das Array $a$ entlang des Propagierungspfads vom Standardwert $\langle v \rangle$ unterscheidet.
   • Konflikterkennung (CongC): Wenn zwei verschiedene Standardwerte $v$ und $w$ zu demselben Array $a$ propagiert werden, prüft der Kalkül, ob die Menge der aktualisierten Indizes $I(a, \langle v \rangle) \cup I(a, \langle w \rangle)$ die gesamte Indexdomäne abdeckt. Ist die Domäne endlich und decken die aktualisierten Indizes nicht alle möglichen Indizes ab, entsteht ein Konflikt, es sei denn, $v \approx w$.
   • DistinctN-Kodierung: Um die quantifizierte Formel $\exists i : \sigma. \bigwedge_{k \in I} i \neq k$ (Prüfung, ob ein nicht aktualisierter Index existiert) effizient zu behandeln, kodiert die Implementierung dies als spezialisierte distinctN-Einschränkung. Dies prüft, ob die Menge der aktualisierten Indizes mindestens $n$ verschiedene Werte enthält, wobei $n$ die Größe der Indexdomäne ist.

Implementierung

Das Entscheidungsverfahren ist im hochmodernen SMT-Löser Bitwuzla implementiert. Es integriert sich nahtlos in die bestehende LOD-Architektur von Bitwuzla, wobei der Bitvektor-Löser die Interpretation $I$ bereitstellt. Die Implementierung umfasst Optimierungen wie die verzögerte Expansion von distinctN-Einschränkungen und eine Breitensuche nach Propagierungspfaden, um den Speicheraufwand zu minimieren.

Hauptbeiträge

1. Verallgemeinerung von LOD: Die Autoren verallgemeinern das LOD-Verfahren für extensionale Arrays mit festgroßen Bitvektoren auf beliebige Index- und Elementsorten.
2. Abstrakter Kalkül AEXT: Sie stellen AEXT als entkoppelten, abstrakten Kalkül für die extensionale Theorie der Arrays vor, unabhängig vom LOD-Lösungsparadigma.
3. Erweiterung um konstante Arrays (CAEXT): Sie erweitern AEXT, um extensionale konstante Arrays zu behandeln, und beweisen widerlegende Korrektheit (wenn Unsat gemeldet wird, ist die Eingabe unerfüllbar) und Erfüllbarkeits-Korrektheit (wenn eine saturierte Konfiguration ohne Unsat erreicht wird, ist die Eingabe erfüllbar).
4. Implementierung und Evaluation: Das Verfahren wurde in Bitwuzla implementiert und an diversen Benchmarks evaluiert, wobei signifikante Leistungsverbesserungen gegenüber dem Basis-Bitwuzla und anderen führenden Lösern (Z3, cvc5, MathSAT5) demonstriert wurden.

Ergebnisse

Die Evaluation wurde an fünf Benchmark-Sets durchgeführt: smtlib (quantifizierte Logiken), mbqi (Teilabfragen aus modellbasierter Quantoren-Instantiierung), k-ind (inkrementelle Hardware-Modellprüfung), hevm (Ethereum-Virtual-Machine) und crafted (synthetische Benchmarks, die speziell entwickelt wurden, um die Extensionalität endlicher konstanter Arrays zu testen).

• Leistung: Bitwuzla mit dem neuen Verfahren (Bitwuzla⟨A⟩) schnitt bei allen anderen Lösern deutlich besser ab. Beim smtlib-Set stieg die Anzahl der gelösten Benchmarks um den Faktor 5 im Vergleich zum Basis-Bitwuzla (3.545 vs. 717). Beim mbqi-Set löste Bitwuzla⟨A⟩ alle 4.147 Abfragen, während das Basis-System nur 4 löste.
• Korrektheit: Beim crafted⟨A⟩-Set, das Gleichheiten über endliche konstante Arrays mit unterschiedlichen Standardwerten kodiert, war Bitwuzla⟨A⟩ der einzige Löser, der für alle Instanzen korrekte Antworten lieferte. Z3 und MathSAT5 akzeptierten die Eingaben, meldeten jedoch für eine signifikante Anzahl von Benchmarks falsche Antworten. cvc5 und das Basis-Bitwuzla lehnten die Eingaben aufgrund fehlender Unterstützung vollständig ab.
• Verifikation der Korrektheit: Die Autoren verifizierten die von den Lösern auf dem crafted⟨A⟩-Set erzeugten Modelle. Nur Bitwuzla⟨A⟩ erzeugte Modelle, die mit seinen eigenen Erfüllbarkeitsbehauptungen konsistent waren. Z3 und MathSAT5 erzeugten Modelle, die, wenn sie wieder in die ursprünglichen Formeln eingesetzt wurden, zu Widersprüchen führten.

Bedeutung

Die Arbeit behauptet, dass das vorgeschlagene Entscheidungsverfahren die Lösfähigkeiten von Bitwuzla signifikant erweitert, indem es die Behandlung von Problemen ermöglicht, die extensionale konstante Arrays mit endlichen Indexdomänen betreffen und die zuvor von anderen Tools unlösbar waren oder fehlerhaft behandelt wurden.

Die Arbeit schließt eine kritische Lücke im SMT-Lösen: Während konstante Arrays ein Standardmodellierungsmuster für Speicherinitialisierung sind, fehlt bestehenden Lösern entweder die Unterstützung für sie in endlichen Domänen, oder sie liefern unkorrekte Ergebnisse. Durch die Bereitstellung eines korrekten und vollständigen Entscheidungsverfahrens für die volle Theorie extensionaler konstanter Arrays (sowohl endlich als auch unendlich) ermöglicht diese Arbeit eine genauere und effizientere Verifikation in Anwendungen wie der Hardware-Modellprüfung und der Verifikation von Smart Contracts (insbesondere für die Ethereum Virtual Machine). Die Autoren weisen darauf hin, dass sich ihre Evaluation zwar auf endliche Domänen konzentrierte, das Verfahren jedoch unabhängig von der zugrunde liegenden Löserarchitektur ist und den Fall unendlicher Domänen ebenfalls vollständig unterstützt.