エンコーディングが有効かどうかに関する仕様との一致:

この大きな有効性のギャップには特定可能な原因がある。Unicornは命令を実行して トラップを観測することで有効性をテストするが、他のオラクルは実行せずにデコードする。 少数の領域は、コンパイル済み仕様オラクルが評価しないデコード時のUNDEFINED 条件の影響も受けている。Silicaはこれらの制限を結果から平滑化するのではなく 記録する。

命令テキスト

レンダリングされたニーモニックとオペランドの比較は、有効性ビットの記録よりも はるかに高コストである。そのためSilicaは、4つのオラクルすべてがエンコーディングを 有効とみなす1,266,064,016個の候補から抽出した1,000,000ワードの決定論的サンプルで テキストを評価する。これはサンプリング結果であり、網羅的な有効性の数値とは 意図的に分けて扱われる。

このサンプルは正規化と表示作業の所在を特定するのに役立つが、 すべてのテキストレンダリングの網羅的なカバレッジを主張するものではない。

結果を探索する

走査エンジンは大規模な研究データセットを生成する。silica-scope は、そのデータセットを扱いやすくするためのコンパニオンターミナルアプリである。 完成したSilicaアーティファクトディレクトリを開き、主要なメトリクスの閲覧、 256シャードのエンコーディングマップの検査、不一致のフィルタリング、 任意の32ビットワードの検索、提出可能な再現プログラムの閲覧を可能にする。

Python 3.11以降でPyPIからインストールする:

次に、Silicaのチェックアウトから実行するか、アーティファクトディレクトリを指定する:

silica-scopeはネイティブデコーダ依存のない純粋なPythonリーダーである。 網羅的な走査を起動することはなく、リポジトリのより小さな公開アーティファクト セットも適切に処理する。ペイン、キーボード操作、アーティファクト検出オプションに ついてはターミナルリーダーガイドを参照。

仕組み

高負荷なパスはRustで書かれており、各デコーダをインプロセスで呼び出す。 オラクルごとにエンコーディングあたり1ビットを格納することで、網羅的な比較を コンパクトに保ち、不一致を直接的なビットマップ演算にする。クラッシュは 正確な命令ワードまで二分探索される。

Pythonは仕様のコンパイル、正規化、レポート、独立検証レイヤーを担当する。 アーティファクトのスキーマ、サンプリング規則、既知の制限は docs/formats.mdに文書化されている。

作業を再現する

固定された環境を作成し、必要なローカル入力が利用可能であることを確認する:

ArmのXML仕様はライセンスのためベンダリングされていない。silica doctorは Silicaがそれをどこで見つけることを期待しているか、およびその他の不足している 前提条件を報告する。

準備されたチェックアウトから完全なパイプラインを実行するには:

これは完全な2³²の走査であり、簡単なスモークテストではない。コンパイル済み オラクル、シャードレコード、有効性ビットマップ、不一致コーパス、公開メトリクス、 再現プログラム、安定したSHA-256結果ハッシュを生成する。

信頼せよ、されど検証せよ

7つの独立した検証器が、生のアーティファクトからプロジェクトの主張を再計算する。 それらは生成されたサマリーを信頼せず、各検証器には、それが防ぐ欠陥を検出する ことを証明するフィクスチャがある。スキップされた状態や暫定的な状態は存在しない。

固定されたデコーダバージョンと新たに再計算された結果ハッシュにより、別々の実行を 比較可能にする。検証目標とその現在のステータスはGOALS.ymlに 記録されている。

スコープ

Silicaは現在、ベースA64とAdvanced SIMDのデコードをカバーしている。SVE、SVE2、SME、 A32/T32、RISC-V、アセンブラのラウンドトリップ、一般的な実行テストはv1の研究の 範囲外である。

最も近いインスピレーションはSandsifterであり、 これはx86の可変長命令空間を探索する。Silicaは同じ系統的な懐疑の精神をAArch64に 適用する。そこでは固定幅エンコーディングと独立した仕様により、完全で裁定された 比較が可能になる。