
AArch64命令エンコーディング全43億通りの網羅的差分検証。
A64命令割り当て判断の網羅的な比較。
Silicaは、4,294,967,296通り存在するA64命令ワードすべてを検査します。 Capstone、LLVM、Unicorn、およびArmのXMLエンコーディング図からコンパイルされたテーブルが、各ワードを受け入れるかどうかを比較します。
デコーダとエンコーディング図は、まったく同じ問いに答えるわけではありません。 CapstoneとLLVMは命令をデコードし、Unicornは実行を試み、SilicaのXML由来テーブルはArmのエンコーディング図における固定ビットと照合します。これらを比較することは有用ですが、不一致が自動的にデコーダのバグであるとは限りません。
A64命令は32ビット幅であるため、割り当ての比較は入力空間全体をカバーできます。以下の有効性カウントは、固定されたバージョンと構成に対して網羅的なものです。命令テキストの分析はサンプリングによるものです。
これらの成果物はISA_A64_xml_A_profile-2026-06_mcと、2³²ワードすべてをカバーする256個のシャードを使用しています。
| XML由来の割り当て結果 | 件数 | 割合 |
|---|---|---|
| 対象範囲内のエンコーディングパターンに一致 | 1,799,435,776 | 41.9% |
| 対象範囲内のエンコーディングパターンに一致しない | 2,495,531,520 | 58.1% |
4つの有効性ビットマップ全体で、723,801,678ワードが少なくとも1つの異なる分類を持っています。これはワード空間全体の16.9%です。これは不一致の件数であり、確認されたバグの件数ではありません。
XML由来の割り当てビットマップとのペアワイズ一致率:
| ツール | 一致率 |
|---|---|
| Capstone | 84.8% |
| LLVM | 87.6% |
| Unicorn | 88.3% |
これらの割合はデコーダの正確性を順位付けするものではありません。特に、コンパイルされたXMLテーブルは命令の擬似コード、機能の可用性、デコード時のすべての制約を評価するものではありません。またUnicornは逆アセンブリではなく、実行とトラップを通じて応答します。それぞれの差異は、上流のバグ報告を裏付ける前に、命令ファミリと構成の分析を必要とします。
Silicaは、4つの有効性チェックすべてで受け入れられた1,266,064,016ワードから、1,000,000ワードの決定論的サンプルを記録しました。出力は対称的ではありません。CapstoneとLLVMは完全な逆アセンブリテキストを返し、XMLテーブルはニーモニックのみを返し、Unicornはプレースホルダ<valid>を返します。
現在の分類器は以下を報告します:
| 分類 | レコード数 | 割合 |
|---|---|---|
| 正規化ニーモニックが同一、完全テキストが異なる | 862,648 | 86.3% |
| 正規化ニーモニックが異なる | 137,352 | 13.7% |
86.3%という値はオペランドエラー率ではありません。ほとんどのレコードでは、完全な命令がニーモニックのみの参照と比較されています。また、XMLのエイリアス条件がレンダリングされたテキストから証明できない場合、エイリアスの扱いは保守的なままです。これらのレコードは分析の手がかりであり、デコーダの正確性に関する知見ではありません。
artifacts/reproducers内のファイルは、最初の5つの適格な不一致シャードから選択された10個の異なるレコードです。選択はテキストカテゴリを優先し、繰り返される(category, spec mnemonic)ペアを上限付きで制限します。現在の10個のファイルはすべて、CapstoneとXML由来のニーモニックを比較しています。
生成されたコーパス内にレコードが存在すること、および1つの命令ワードから再現可能であることを証明している。これらは10件のCapstoneバグとして独立に裁定されたものではなく、LLVMとUnicornがレンダリングされた命令について一致している証拠でもない。3件は明示的にNORMALIZATION_UNCERTAINとマークされている。ジェネレーターと検証器は
g6_reproducers.py と
verify/g6_reproducers.py である。
スイープは大規模なデータセットを生成する。silica-scope はそのターミナルリーダーである。Silicaアーティファクトディレクトリを開き、メトリクスと256シャードマップを表示し、不一致レコードをフィルタリングし、個々のワードを検索する。また、10件のサンプルレコードをその明記された制限事項とともに開くこともできる。
Python 3.11以降を使用してPyPIからインストールする:
pipx install silica-scope
Then run it from a Silica checkout or point it at an artifact directory:
silica-scope
silica-scope /path/to/silica/artifacts
silica-scope --report
silica-scope は純粋な Python 製のリーダーです。スイープを実行したり、ネイティブデコーダライブラリを必要としたりしません。キーボード操作とアーティファクトの検出については、ターミナルリーダーガイドを参照してください。
flowchart LR
XML["Arm XML encoding diagrams"] --> SPEC["compiled allocation matcher"]
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 · examples · result hash"]
大容量パスはRustで書かれており、各デコーダをインプロセスで呼び出します。オラクルごとにエンコーディングあたり1ビットを格納するため、網羅的な比較がコンパクトに保たれ、不一致は直接ビットマップ演算として扱えます。クラッシュは正確な命令ワードまで二分探索されます。
PythonはXMLのコンパイル、正規化、レポート作成、検証を担当します。アーティファクトのスキーマとサンプリング規則は docs/formats.mdに記載されています。各主要な値の出所は次のとおりです:
| 主張 | アーティファクト | 再計算担当 |
|---|---|---|
| XML割り当て数 | artifacts/g1_metrics.json | G1 |
| 網羅的な有効性の差異 | 4つの有効性ビットマップ | G2およびG5 |
| サンプルカテゴリ数 | artifacts/g4_metrics.json | G4 |
| ペアワイズ一致率 | artifacts/report/metrics.json | G5 |
| 選択された10件のサンプルレコード | artifacts/reproducers/*.md | G6 |
| 公開アーティファクトのダイジェスト | artifacts/result_hash.txt | G7 |
固定された環境を作成し、必要なローカル入力が利用可能であることを確認します:
micromamba create -y -p ./.venv -f environment.yml
micromamba run -p ./.venv silica doctor
Arm の XML 仕様はライセンスの都合上、ベンダー化されていません。silica doctor は、Silica がその仕様をどこで見つけることを想定しているか、およびその他の不足している前提条件を報告します。
チェックイン済みの成果物は、スイープを再実行せずに検査できます:
silica-scope artifacts
make all レシピは新規実行のためのステージを列挙しているが、現時点ではターンキーな再現コマンドではない。その G4 ハンドオフでは依然としてリザーバー JSON を単語リストへ変換する必要があり、3 つのコーパス合計値は明示的な引数として渡される。Makefile はそのギャップを直接指摘している。新規の公開実行は、そのハンドオフが自動化され、合計値が生成された出力から流れてくるまでは、再現済みとして扱うべきではない。
silica verify コマンドは、リポジトリが管理する 7 つのゲートを実行する。これらは XML コンパイルメタデータ、シャードカバレッジ、正規化の証跡、コーパス構造、公開されたメトリクス、サンプルレコード、およびアーティファクトハッシュをチェックする。これらをゲートと呼ぶのは意図的である。これらは一貫性チェックを提供するが、独立した実装やデコーダーのバグに対する外部からの確認ではない。
micromamba run -p ./.venv silica verify
G4 と G5 は大規模な不一致コーパスと有効性ビットマップをストリーミングするため、これは手軽なドキュメントチェックではありません。公開前や数値に関する主張を変更する前に実行してください。通常の README 編集では、引用されている JSON アーティファクトを確認し、変更が公開可能な状態になるまで完全な検証ツールの実行を延期してください。
XML マッチャーは、コンパイラのスコープフィルター適用後のベース A64 および Advanced SIMD エンコーディングパターンを含みます。SVE、SVE2、SME、および artifacts/g1_metrics.json に記載されているその他のクラスは除外されます。A32/T32、RISC-V、アセンブラのラウンドトリップ、意味的等価性、および一般的な実行正確性は、この研究の範囲外です。
最も近い着想元は Sandsifter であり、これは x86 の可変長命令空間を探索します。Silica は有限の A64 ワード空間に焦点を当て、後でファミリーごとの裁定に必要となる生の分類結果を公開します。
Apache 2.0 — LICENSE を参照