ityonemo/clrChecker für Lifetimes und andere Refinement types
Checker für
Lebensdauern und andere
Raffinement-Typen
für Zig
Video: https://www.youtube.com/watch?v=mf0WzTOe-40 Sponsoring: https://buymeacoffee.com/dnautics
Diskussion auf HN: https://news.ycombinator.com/item?id=42923829
Diskussion auf lobste.rs: https://lobste.rs/s/9sitsj/clr_checker_for_lifetimes_other
Live-Demo-Video: https://www.youtube.com/watch?v=ZY_Z-aGbYm8
Dieses Projekt erstellt einen Zig-Transpiler für den Zig-Compiler, der AIR (Abstract Intermediate Representation) in Zig-Quellcode umwandelt, der zur Kompilierzeit eine statische Analyse durchführt. Der generierte Analyzer erkennt Speichersicherheitsprobleme wie Verwendung vor Zuweisung, Verwendung nach Freigabe, Stack-Zeiger-Eskapierungen sowie Zig-spezifisches UB wie Nicht-Null-Behauptungen, Verletzungen von getaggten Unions oder Missbrauch von fieldParentPtr.
Das Ziel ist es, Rust-ähnliche Speichersicherheitsgarantien für Zig durch statische Analyse von AIR zu erreichen, ohne die Sprache selbst zu ändern.
CLR hängt von einer geforkten Version des Zig-Compilers ab (als Submodul in zig/ enthalten), die das Routing von AIR an externe Plugins unterstützt. Wenn der Compiler mit -ofmt=air -fair-out=<plugin.so> aufgerufen wird, lädt er die angegebene Shared Library und übergibt das generierte AIR zur Verarbeitung.
CLR soll Programme zu Lebenszyklusmustern führen, die explizit und lokal überprüfbar sind, und nicht einfach jedes technisch gültige Zig-Programm erkennen. Wenn zwei Darstellungen möglich sind, bevorzugt CLR diejenige, die den Ressourcenzustand im Typ und in der Kontrollflussstruktur sichtbar macht.
Vermeiden Sie beispielsweise das bedingte Schließen eines nicht-optionalen Dateideskriptors:
const file = try std.fs.cwd().openFile(path, .{});
if (should_close) {
file.close(); // Schlecht: file ist nach diesem Zweig mehrdeutig offen.
}
Bevorzugen Sie die Darstellung bedingter Eigentümerschaft mit einem Optional:
var file: ?std.fs.File = null;
if (should_open) {
file = try std.fs.cwd().openFile(path, .{});
}
if (file) |open_file| {
open_file.close();
}
Das bedingte Schließen eines nicht-optionalen Deskriptors lässt seinen Lebenszyklus nach dem Zweig mehrdeutig. CLRs beabsichtigte Richtlinie ist es, dieses Muster abzulehnen, anstatt einen permanenten "vielleicht geschlossen"-Zustand zu tragen.
Das gleiche Prinzip gilt für allozierte Zeiger. Geben Sie keinen Speicher über einen abgeleiteten Zeiger frei:
const allocation = try allocator.alloc(u8, size);
const payload = allocation[header_size..];
allocator.free(payload); // Schlecht: payload ist nicht die Allokationsbasis.
Halten Sie den Allokationsbasis-Zeiger für die Freigabe verfügbar und verwenden Sie abgeleitete Zeiger nur für den Zugriff:
const allocation = try allocator.alloc(u8, size);
defer allocator.free(allocation);
const payload = allocation[header_size..];
use(payload);
Das Freigeben eines Feldzeigers, Teil-Slices oder eines durch Arithmetik erzeugten Zeigers wird abgelehnt, es sei denn, eine dokumentierte interne Regel stellt die Herkunft der Allokationsbasis wieder her.
Diese Richtlinien sind standardmäßig streng, da sie Code mit einfacheren, besser überprüfbaren Ressourcenlebenszyklen erzeugen. Ein zukünftiger unsafe-Annotationsmechanismus wird es ausgewählten GIDs oder Operationen ermöglichen, sich von einzelnen Analysen abzumelden. Dies wird Code unterstützen, der bewusst schwächere Prüfungen zugunsten der Leistung akzeptiert, ohne das Standardmodell für den Rest des Programms zu schwächen.
Dies ist eine aktive Neufassung des ursprünglichen auf Elixir basierenden Proof-of-Concept in Zig. Die Zig-Implementierung wird als Compiler-Plugin geladen und analysiert AIR direkt.
Derzeit implementiert:
std.mem.Allocator-Interface:
create/destroy – Allokation einzelner Elementealloc/free – Slice-Allokation (einschließlich alignedAlloc, allocSentinel usw.)realloc/remap – Slice-Neuzuweisung mit Verfolgung alter-freigegebener Slicesdupe/dupeZ – Slice-Duplizierungcreate/destroy vs. alloc/free)init/deinit/allocator – vollständiger Arena-Lebenszyklusdeinit freigegeben (keine falsch positiven Leckmeldungen)deinit, doppeltem deinit, Allokation nach deinitptr_add/ptr_sub auf Einzelelementzeigern)std.process.args,
std.mem.asBytes, std.HashMap und Allokator-/Datei-APIsstd.HashMap-Verfeinerungen mit kanonischer Metadaten-/Schlüssel-/Wert-Speicheridentität über put, get, getPtr und Wertiteration hinwegposix.open/close/dup/dup2/socket/accept/epoll_create/pipeGeplant (Details in LIMITATIONS.md):
sudo apt install bats