nathan-luevano/silicaErschöpfende differenzielle Validierung aller 4,3 Mrd. AArch64-Befehlskodierungen.
Eine vollständige Karte davon, wo AArch64-Decoder von der Architektur abweichen.
Silica durchläuft jedes der 4.294.967.296 möglichen A64-Instruktionswörter, vergleicht Capstone, LLVM und Unicorn mit Arms maschinenlesbarer Spezifikation und verwandelt die Unterschiede in reproduzierbare Belege.
Dass ein Disassembler „gültig“ sagt, ist einfach. Zu wissen, ob er recht hat, ist schwieriger. Die meisten differenziellen Tests können aufdecken, dass Tools uneinig sind, aber sie können die richtige Antwort nicht ohne ein unabhängiges Orakel identifizieren. Silica verwendet Arms XML-Release als dieses Orakel.
A64 ermöglicht ein ungewöhnlich gründliches Experiment: Instruktionen sind exakt 32 Bit breit, sodass der gesamte Kodierungsraum endlich und praktisch aufzählbar ist. Silica nutzt diese Eigenschaft. Die untenstehenden Gültigkeitsergebnisse sind keine Schätzung oder ein Fuzzing-Kampagne; jedes mögliche Wort wurde geprüft.
Diese Ergebnisse verwenden ISA_A64_xml_A_profile-2026-06_mc (Armv9.6-A). Der Sweep wurde
in 256 unabhängig verifizierte Shards aufgeteilt, die alle 2³² Kodierungen abdecken.
| Ergebnis | Anzahl | Anteil am gesamten Raum |
|---|---|---|
| Von der Arm-Spezifikation zugewiesen | 1.799.435.776 | 41,9% |
| Von der Arm-Spezifikation nicht zugewiesen | 2.495.531.520 | 58,1% |
| Gefundene Gültigkeitsabweichungen | 723.801.678 | 16,9% |
| Minimale upstream-fähige Reproduzierer | 10 | — |
Übereinstimmung mit der Spezifikation darüber, ob eine Kodierung gültig ist:
| Decoder | Übereinstimmung | Visuell |
|---|---|---|
| Capstone | 84,8% | █████████████████████████░░░░░ |
| LLVM | 87,6% | ██████████████████████████░░░░ |
| Unicorn | 88,3% | ██████████████████████████░░░░ |
Die große Gültigkeitslücke hat identifizierbare Ursachen. Unicorn testet Gültigkeit, indem
es eine Instruktion ausführt und Traps beobachtet, während die anderen Orakel ohne Ausführung
dekodieren. Eine kleine Anzahl von Regionen ist auch von Dekodierungszeit-UNDEFINED-Bedingungen
betroffen, die das kompilierte Spezifikationsorakel nicht auswertet. Silica zeichnet diese
Einschränkungen auf, anstatt sie aus dem Ergebnis herauszuglätten.
Der Vergleich gerenderter Mnemonics und Operanden ist viel teurer als das Aufzeichnen eines Gültigkeitsbits. Silica wertet daher Text anhand einer deterministischen Stichprobe von 1.000.000 Wörtern aus, die aus 1.266.064.016 Kandidaten gezogen wurden, bei denen alle vier Orakel die Kodierung als gültig betrachten. Dies ist ein Stichprobenergebnis und wird bewusst von den erschöpfenden Gültigkeitszahlen getrennt gehalten.
| Klassifizierung innerhalb der Stichprobe | Datensätze | Anteil |
|---|---|---|
| Operanden-Rendering unterscheidet sich | 862.648 | 86,3% |
| Normalisierung muss überprüft werden | 137.352 | 13,7% |
Die Stichprobe ist nützlich, um Normalisierungs- und Darstellungsarbeit zu lokalisieren; sie beansprucht keine erschöpfende Abdeckung jeder textuellen Darstellung.
Die Sweep-Engine erzeugt einen großen Forschungsdatensatz. silica-scope ist die begleitende Terminal-App, die diesen Datensatz zugänglich macht. Sie öffnet ein fertiges Silica-Artefaktverzeichnis und ermöglicht es Ihnen, Kernmetriken zu durchsuchen, die 256-Shard-Kodierungskarte zu inspizieren, Abweichungen zu filtern, jedes 32-Bit-Wort nachzuschlagen und die einreichungsfertigen Reproduzierer zu lesen.
Installieren Sie es von PyPI mit Python 3.11 oder neuer:
pipx install silica-scope
Führen Sie es dann aus einem Silica-Checkout aus oder richten Sie es auf ein Artefaktverzeichnis:
silica-scope
silica-scope /path/to/silica/artifacts
silica-scope --report
silica-scope ist ein reiner Python-Reader ohne native Decoder-Abhängigkeiten. Es
startet nicht den erschöpfenden Sweep und geht mit dem kleineren veröffentlichten
Artefaktsatz des Repositorys problemlos um. Siehe den Terminal-Reader-Leitfaden
für die Bereiche, Tastatursteuerungen und Optionen zur Artefakterkennung.
flowchart LR
XML["Arm XML specification"] --> SPEC["compiled spec oracle"]
SPEC --> SWEEP["parallel 32-bit sweep"]
CAP["Capstone"] --> SWEEP
LLVM["LLVM"] --> SWEEP
UNI["Unicorn"] --> SWEEP
SWEEP --> MAP["validity bitmaps"]
MAP --> DIFF["exhaustive XOR comparison"]
DIFF --> CORPUS["classified disagreement corpus"]
CORPUS --> OUT["metrics · reproducers · result hash"]Der Hochvolumen-Pfad ist in Rust geschrieben und ruft jeden Decoder im Prozess auf. Er speichert ein Bit pro Kodierung pro Orakel, was den erschöpfenden Vergleich kompakt hält und Abweichungen zu einer direkten Bitmap-Operation macht. Abstürze werden bis zum exakten Instruktionswort biseziert.
Python übernimmt die Spezifikationskompilierung, Normalisierung, Berichterstellung und die unabhängige Verifikationsschicht. Artefakt-Schemas, Sampling-Regeln und bekannte Einschränkungen sind in docs/formats.md dokumentiert.
Erstellen Sie die gepinnte Umgebung und prüfen Sie, ob die erforderlichen lokalen Eingaben verfügbar sind:
micromamba create -y -p ./.venv -f environment.yml
micromamba run -p ./.venv silica doctor
Arms XML-Spezifikation wird aufgrund ihrer Lizenz nicht mitgeliefert. silica doctor
meldet, wo Silica sie erwartet und welche anderen Voraussetzungen fehlen.
Um die vollständige Pipeline aus einem vorbereiteten Checkout auszuführen:
make all
Dies ist ein vollständiger 2³²-Sweep, kein schneller Smoke-Test. Er erzeugt das kompilierte Orakel, Shard-Datensätze, Gültigkeits-Bitmaps, den Abweichungskorpus, veröffentlichte Metriken, Reproduzierer und einen stabilen SHA-256-Ergebnis-Hash.
Sieben unabhängige Verifizierer berechnen die Behauptungen des Projekts aus Rohartefakten neu. Sie vertrauen keiner generierten Zusammenfassung, und jeder Verifizierer hat ein Fixture, das beweist, dass er den Defekt erkennt, gegen den er absichert. Es gibt keinen übersprungenen oder vorläufigen Zustand.
micromamba run -p ./.venv silica verify
Gepinnte Decoder-Versionen und ein frisch neu berechneter Ergebnis-Hash machen separate Läufe vergleichbar. Die Verifikationsziele und ihr aktueller Status sind in GOALS.yml festgehalten.
Silica deckt derzeit Basis-A64- und Advanced-SIMD-Dekodierung ab. SVE, SVE2, SME, A32/T32, RISC-V, Assembler-Roundtrips und allgemeine Ausführungstests liegen außerhalb der v1-Studie.
Die nächste Inspiration ist Sandsifter, das den variable-Länge-Instruktionsraum von x86 erkundet. Silica wendet denselben Geist systematischer Skepsis auf AArch64 an, wo feste Kodierungsbreiten und eine unabhängige Spezifikation einen vollständigen, entschiedenen Vergleich ermöglichen.
Apache 2.0 — siehe LICENSE