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 alloc/free)init/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 prematurosPlanejado (veja LIMITATIONS.md para detalhes):
sudo apt install bats