ityonemo/clrVerificador para Lifetimes e outros tipos de Refinement
Checkador de
Lifetimes e outros
Refinement types
para Zig
Vídeo: https://www.youtube.com/watch?v=mf0WzTOe-40 Patrocínio: https://buymeacoffee.com/dnautics
discuta no hn: https://news.ycombinator.com/item?id=42923829
discuta no lobste.rs: https://lobste.rs/s/9sitsj/clr_checker_for_lifetimes_other
vídeo de demonstração ao vivo: https://www.youtube.com/watch?v=ZY_Z-aGbYm8
Este projeto cria um transpilador Zig para o compilador Zig, que transforma AIR (Abstract Intermediate Representation) em código fonte Zig que realiza análise estática em tempo de compilação. O analisador gerado captura problemas de segurança de memória como uso antes da atribuição, uso após liberação, escapes de ponteiro de pilha, bem como UB específicos do Zig, como asserções de não nulidade, violações de união marcada ou uso indevido de fieldParentPtr.
O objetivo é trazer garantias de segurança de memória no nível do Rust para o Zig por meio de análise estática do AIR, sem alterar a linguagem em si.
CLR depende de uma versão bifurcada do compilador Zig (incluída como submódulo em zig/) que adiciona suporte para roteamento do AIR a plugins externos. Quando invocado com -ofmt=air -fair-out=<plugin.so>, o compilador carrega a biblioteca compartilhada especificada e passa o AIR gerado para processamento.
CLR pretende guiar programas para padrões de ciclo de vida que sejam explícitos e localmente verificáveis, não apenas reconhecer todo programa Zig tecnicamente válido. Quando duas representações são possíveis, CLR prefere aquela que torna o estado do recurso visível no tipo e na estrutura de fluxo de controle.
Por exemplo, evite fechar condicionalmente um descritor de arquivo não opcional:
const file = try std.fs.cwd().openFile(path, .{});
if (should_close) {
file.close(); // Ruim: arquivo fica ambiguamente aberto após este ramo.
}
Prefira representar propriedade condicional com um opcional:
var file: ?std.fs.File = null;
if (should_open) {
file = try std.fs.cwd().openFile(path, .{});
}
if (file) |open_file| {
open_file.close();
}
Fechar condicionalmente um descritor não opcional deixa seu ciclo de vida ambíguo após o ramo. A política pretendida do CLR é rejeitar esse padrão em vez de carregar um estado permanente de "talvez fechado".
O mesmo princípio se aplica a ponteiros alocados. Não libere através de um ponteiro derivado:
const allocation = try allocator.alloc(u8, size);
const payload = allocation[header_size..];
allocator.free(payload); // Ruim: payload não é a base da alocação.
Mantenha o ponteiro de base de alocação disponível para desalocação e use ponteiros derivados apenas para acesso:
const allocation = try allocator.alloc(u8, size);
defer allocator.free(allocation);
const payload = allocation[header_size..];
use(payload);
Liberar um ponteiro de campo, sub-slice ou ponteiro produzido por aritmética é rejeitado a menos que uma regra interna documentada restabeleça a proveniência da base de alocação.
Essas políticas são estritas por padrão porque produzem código com ciclos de vida
de recursos mais simples e revisáveis. Um mecanismo futuro de anotação unsafe permitirá
que GIDs ou operações selecionadas optem por não participar de análises individuais.
Isso suportará código que deliberadamente aceita verificação mais fraca em troca de
desempenho, sem enfraquecer o modelo padrão para o resto do programa.
Esta é uma reescrita ativa do conceito original baseado em Elixir para Zig. A implementação em Zig carrega como um plugin do compilador e analisa o AIR diretamente.
Atualmente implementado:
std.mem.Allocator:
create/destroy - alocação de item únicoalloc/free - alocação de slice (incluindo alignedAlloc, allocSentinel, etc.)realloc/remap - realocação de slice com rastreamento de slice antigo liberadodupe/dupeZ - duplicação de slicecreate/destroy vs /)Planejado (veja LIMITATIONS.md para detalhes):
sudo apt install batsO compilador Zig fornecido e o plugin libclr devem ser compilados com níveis de otimização correspondentes. Níveis de otimização incompatíveis causarão segfaults.
# Compilar o compilador Zig personalizado com ReleaseFast (primeira vez apenas, ou após alterações no submódulo)
cd zig && zig build --zig-lib-dir lib -Doptimize=ReleaseFast && cd ..
# Compilar o plugin CLR com otimização correspondente
zig build -Doptimize=ReleaseFast
Para desenvolvimento/depuração, use ReleaseSafe ou Debug para ambos:
# ReleaseSafe (com verificações de segurança, ligeiramente mais lento)
cd zig && zig build --zig-lib-dir lib -Doptimize=ReleaseSafe && cd ..
zig build -Doptimize=ReleaseSafe
# Debug (informações completas de depuração, mais lento)
cd zig && zig build --zig-lib-dir lib && cd ..
zig build
# Compilar um arquivo Zig usando o backend AIR
zig/zig-out/bin/zig build-exe -fair-out=zig-out/lib/libclr.so -ofmt=air -femit-bin=output.air.zig seu_arquivo.zig
# Executar o analisador gerado
zig run --dep clr -Mroot=output.air.zig -Mclr=lib/lib.zig
A saída vai para stderr.
# Testes unitários (codegen/DLL)
zig build test
# Testes unitários (biblioteca de tempo de execução)
zig test lib/lib.zig
# Um arquivo de teste de integração focado
bats test/integration/fd.bats
# Testes de integração (requer BATS)
# Padrão é ReleaseFast; substitua com OPTIMIZE=ReleaseSafe ou OPTIMIZE=Debug
./run_integration.sh
# Teste manual de um único arquivo
./run_one.sh test/cases/undefined/use_before_assign.zig
Nota: Testes de integração recompilam libclr com o nível de otimização especificado (padrão: ReleaseFast). Certifique-se de que seu compilador Zig fornecido foi compilado com um nível de otimização correspondente.
clr/
├── src/ # Código DLL/plugin (gera .air.zig)
│ ├── clr.zig # Ponto de entrada principal do plugin CLR
│ ├── codegen.zig # Gera código fonte .air.zig a partir de instruções AIR
│ └── allocator.zig # Wrapper de alocador seguro para DLL
├── lib/ # Biblioteca de análise de tempo de execução
│ ├── lib.zig # Ponto de entrada da biblioteca
│ ├── tag.zig # União AnyTag, Type, manipuladores de tag, despacho splat
│ ├── Inst.zig # Resultados de instrução e análise interprocedimental
│ ├── Refinements.zig # Tipos de refinamento (ponteiro, struct, opcional, etc.)
│ ├── Analyte.zig # Contêiner de estado de análise
│ ├── Context.zig # Contexto de execução (metadados, relatório de erros)
│ └── analysis/ # Módulos de análise
│ ├── undefined_safety.zig # Rastreamento de uso antes da atribuição
│ ├── memory_safety.zig # Rastreamento de alocação/liberação
│ ├── null_safety.zig # Verificação de desempacotamento opcional
│ ├── variant_safety.zig # Acesso a campos de união marcada
│ └── fd_safety.zig # Rastreamento de descritor de arquivo
├── test/
│ ├── integration/ # Testes de integração BATS
│ │ ├── test_helper.bash
│ │ └── *.bats
│ └── cases/ # Arquivos de entrada de teste (.zig)
├── zig/ # Submódulo do compilador Zig (fork instrumentado)
├── build.zig # Configuração de compilação
└── build.zig.zon # Dependências do pacote
Zig é uma linguagem famosamente "insegura". O gerenciamento de memória é feito manualmente, o que abre a possibilidade de erros de implementação. Embora o Zig reduza problemas de segurança em relação ao C ao eliminar acesso fora dos limites de array e desreferenciamento de ponteiro nulo em código com verificações de segurança, ainda é menos seguro que o Rust, que elimina uso após liberação, liberação dupla e condições de corrida através de análise estática.
Inspirado pelo projeto MIRI do Rust, o CLR realiza análise estática na representação intermediária AIR do Zig para alcançar um grau maior de segurança do que o Zig oferece por padrão. Ao contrário do MIRI, que interpreta o MIR do Rust em um pseudo-runtime em sandbox, o CLR transpila o AIR em código fonte Zig que executa a análise estaticamente. Observe que o código zig de saída air do CLR poderia, em princípio, ser executado em tempo de compilação, mas ao passar por um intermediário zig, produzimos um fluxo lógico fácil de entender e depurar. Uma pessoa ambiciosa poderia usar essa abordagem geral para emitir um alvo de saída diferente, como uma linguagem de assistente de prova, ou refatorá-lo para ser executado inteiramente no compilador zig!
A ideia chave: se você precisa de MIRI para projetos Rust que exigem segurança, por que não escolher uma linguagem mais simples e fazer análise no estilo MIRI para obter verificação de empréstimo e outros tipos de análise de refinamento? Este projeto mostra que tal futuro é uma possibilidade real para o Zig.
O pipeline de compilação do Zig é:
AIR é o nível ideal para análise porque é tipado, interpretável como uma lista "mínima viável" de instruções de programação generalizadas e permite estender tipos com metadados de refinamento.
Para uma análise aprofundada de como o AIR do Zig funciona, veja o post do blog de Mitchell Hashimoto: https://mitchellh.com/zig/sema
Licença MIT - veja LICENSE para detalhes.
allocfreeinit/deinit/allocator - ciclo de vida completo da arenadeinit (sem falsos positivos de vazamento)deinit, duplo deinit, alocação após deinitptr_add/ptr_sub em ponteiros de item único)fieldParentPtr (detecção de recuperação inválida de contêiner a partir de ponteiros de campo)try, empacotar/desempacotar payload)std.process.args,
std.mem.asBytes, std.HashMap e APIs de alocador/arquivostd.HashMap com identidade de metadados/chave/valor canônicos
entre put, get, getPtr e iteração de valorposix.open/close/dup/dup2/socket/accept/epoll_create/pipedescoped para que aliases que permanecem vivos suprimam relatórios de vazamento prematuros