nathan-luevano/silicaValidação diferencial exaustiva de todas as 4,3B codificações de instruções AArch64.
Um mapa completo de onde os decodificadores AArch64 divergem da arquitetura.
O Silica percorre cada uma das 4.294.967.296 palavras de instrução A64 possíveis, compara Capstone, LLVM e Unicorn com a especificação legível por máquina da Arm, e transforma as diferenças em evidências reproduzíveis.
Um desassemblador dizer "válido" é fácil. Saber se está correto é mais difícil. A maioria dos testes diferenciais consegue revelar que as ferramentas divergem, mas não consegue identificar a resposta correta sem um oráculo independente. O Silica usa a versão XML da Arm como esse oráculo.
O A64 torna possível um experimento excepcionalmente minucioso: as instruções têm exatamente 32 bits de largura, então todo o espaço de codificação é finito e prático de enumerar. O Silica aproveita essa propriedade. Os resultados de validade abaixo não são uma estimativa nem uma campanha de fuzzing; cada palavra possível foi verificada.
Estes resultados usam ISA_A64_xml_A_profile-2026-06_mc (Armv9.6-A). A varredura foi
dividida em 256 shards verificados independentemente, cobrindo todas as 2³² codificações.
| Resultado | Contagem | Fração do espaço total |
|---|---|---|
| Alocado pela especificação da Arm | 1.799.435.776 | 41,9% |
| Não alocado pela especificação da Arm | 2.495.531.520 | 58,1% |
| Divergências de validade encontradas | 723.801.678 | 16,9% |
| Reproducers mínimos prontos para upstream | 10 | — |
Concordância com a especificação sobre se uma codificação é válida:
| Decodificador | Concordância | Visual |
|---|---|---|
| Capstone | 84,8% | █████████████████████████░░░░░ |
| LLVM | 87,6% | ██████████████████████████░░░░ |
| Unicorn | 88,3% | ██████████████████████████░░░░ |
A grande lacuna de validade tem causas identificáveis. O Unicorn testa a validade
executando uma instrução e observando traps, enquanto os outros oráculos decodificam
sem execução. Um pequeno número de regiões também é afetado por condições
UNDEFINED em tempo de decodificação que o oráculo da especificação compilada não
avalia. O Silica registra essas limitações em vez de suavizá-las no resultado.
Comparar mnemônicos e operandos renderizados é muito mais caro do que registrar um bit de validade. O Silica, portanto, avalia o texto em uma amostra determinística de 1.000.000 de palavras extraídas de 1.266.064.016 candidatas em que todos os quatro oráculos consideram a codificação válida. Este é um resultado amostrado e é deliberadamente mantido separado das cifras exaustivas de validade.
| Classificação dentro da amostra | Registros | Fração |
|---|---|---|
| Renderização de operandos difere | 862.648 | 86,3% |
| Normalização precisa de revisão | 137.352 | 13,7% |
A amostra é útil para localizar trabalho de normalização e apresentação; ela não reivindica cobertura exaustiva de toda renderização textual.
O motor de varredura produz um grande conjunto de dados de pesquisa. silica-scope é o aplicativo de terminal complementar para tornar esse conjunto de dados acessível. Ele abre um diretório de artefatos finalizados do Silica e permite navegar pelas métricas principais, inspecionar o mapa de codificação de 256 shards, filtrar divergências, consultar qualquer palavra de 32 bits e ler os reproducers prontos para registro.
Instale-o do PyPI com Python 3.11 ou mais recente:
pipx install silica-scope
Depois execute-o a partir de um checkout do Silica ou aponte-o para um diretório de artefatos:
silica-scope
silica-scope /path/to/silica/artifacts
silica-scope --report
silica-scope é um leitor em Python puro, sem dependências de decodificadores nativos.
Ele não inicia a varredura exaustiva e lida com o conjunto menor de artefatos
publicados do repositório de forma adequada. Consulte o guia do leitor de terminal
para os painéis, controles de teclado e opções de descoberta de artefatos.
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"]O caminho de alto volume é escrito em Rust e chama cada decodificador em processo. Ele armazena um bit por codificação por oráculo, o que mantém a comparação exaustiva compacta e torna a divergência uma operação direta de bitmap. Crashes são bissectados até a palavra de instrução exata.
O Python cuida da compilação da especificação, normalização, relatórios e da camada de verificação independente. Esquemas de artefatos, regras de amostragem e limitações conhecidas estão documentados em docs/formats.md.
Crie o ambiente fixado e verifique se as entradas locais necessárias estão disponíveis:
micromamba create -y -p ./.venv -f environment.yml
micromamba run -p ./.venv silica doctor
A especificação XML da Arm não é incluída no repositório por causa de sua licença.
silica doctor informa onde o Silica espera encontrá-la e quaisquer outros
pré-requisitos ausentes.
Para executar o pipeline completo a partir de um checkout preparado:
make all
Esta é uma varredura completa de 2³², não um teste rápido de fumaça. Ela produz o oráculo compilado, registros de shards, bitmaps de validade, corpus de divergências, métricas publicadas, reproducers e um hash de resultado SHA-256 estável.
Sete verificadores independentes recalculam as afirmações do projeto a partir de artefatos brutos. Eles não confiam em um resumo gerado, e cada verificador tem um fixture que prova que detecta o defeito contra o qual protege. Não há estado ignorado ou provisório.
micromamba run -p ./.venv silica verify
Versões fixadas dos decodificadores e um hash de resultado recalculado do zero tornam execuções separadas comparáveis. As metas de verificação e seu status atual estão registrados em GOALS.yml.
O Silica atualmente cobre a decodificação de A64 base e Advanced SIMD. SVE, SVE2, SME, A32/T32, RISC-V, idas e voltas pelo assembler e testes gerais de execução estão fora do estudo v1.
A inspiração mais próxima é o Sandsifter, que explora o espaço de instruções de comprimento variável do x86. O Silica aplica o mesmo espírito de ceticismo sistemático ao AArch64, onde codificações de largura fixa e uma especificação independente permitem uma comparação completa e adjudicada.
Apache 2.0 — consulte LICENSE