
모든 43억 개의 AArch64 명령어 인코딩에 대한 철저한 차등 검증.
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% |
네 개의 유효성 비트맵 전체에서 723,801,678개의 워드가 최소 하나의 서로 다른 분류를 가집니다. 이는 전체 워드 공간의 16.9%입니다. 이는 불일치 개수이며, 확인된 버그의 개수가 아닙니다.
XML에서 파생된 할당 비트맵과의 쌍별 일치율:
| 도구 | 일치율 |
|---|---|
| Capstone | 84.8% |
| LLVM | 87.6% |
| Unicorn | 88.3% |
이 백분율은 디코더 정확성을 순위 매기지 않습니다. 특히, 컴파일된 XML 테이블은 명령어 의사코드, 기능 가용성, 또는 모든 디코드 시점 제약을 평가하지 않습니다. Unicorn 또한 디스어셈블리가 아닌 실행과 트랩을 통해 답합니다. 각 차이는 업스트림 버그 보고를 뒷받침하기 전에 명령어 계열과 구성 분석이 필요합니다.
Silica는 네 가지 유효성 검사 모두에서 허용된 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에 있는 파일들은 처음 다섯 개의
적격 불일치 샤드에서 선택된 열 개의 서로 다른 레코드입니다. 선택은 텍스트
카테고리를 우선하고 반복되는 (category, spec mnemonic) 쌍을 제한합니다.
현재 열 개의 파일 모두 Capstone을 XML에서 파생된 니모닉과 비교합니다.
생성된 코퍼스에 레코드가 존재하며 하나의 명령어 워드에서 재현될 수 있음을 입증한다. 이들은 열 개의 Capstone 버그로 독립적으로 판정된 것이 아니며, LLVM과 Unicorn이 렌더링된 명령어에 대해 일치한다는 증거도 아니다. 세 개는 명시적으로 NORMALIZATION_UNCERTAIN으로 표시되어 있다. 생성기와 검증기는
g6_reproducers.py와
verify/g6_reproducers.py이다.
이 스윕은 대규모 데이터셋을 생성한다. **silica-scope**는 그 터미널 리더이다. Silica 아티팩트 디렉터리를 열어 메트릭과 256-샤드 맵을 표시하고, 불일치 레코드를 필터링하며, 개별 워드를 조회한다. 또한 명시된 한계와 함께 열 개의 예시 레코드를 열 수도 있다.
Python 3.11 이상과 함께 PyPI에서 설치한다:
pipx install silica-scope
그런 다음 Silica 체크아웃에서 실행하거나 아티팩트 디렉터리를 지정하여 실행하세요:
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 |
| 전체 유효성 차이 | 네 개의 유효성 비트맵 | 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 핸드오프는 여전히 reservoir JSON을 단어 목록으로 변환해야 하며, 세 개의 코퍼스 총계가 명시적 인수로 전달됩니다. Makefile은 이 격차를 직접 지적합니다. 새 출판 실행은 해당 핸드오프가 자동화되고 총계가 생성된 출력에서 흘러나오기 전까지 재현된 것으로 표현되어서는 안 됩니다.
silica verify 명령은 저장소가 소유한 일곱 개의 게이트를 실행합니다. 이들은 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, 어셈블러 왕복, 의미론적 동등성, 일반 실행 정확성은 이 연구의 범위 밖입니다.
가장 가까운 영감은 x86의 가변 길이 명령어 공간을 탐구하는 Sandsifter입니다. Silica는 유한한 A64 워드 공간에 초점을 맞추고 이후 패밀리별 판정에 필요한 원시 분류를 게시합니다.
Apache 2.0 — LICENSE 참조