polonius

Il s'agit d'une bibliothèque principale qui modélise le chèque d'emprunt. Il met en œuvre l'analyse décrite dans cet article de blog et dans cet exposé. Les détails sont dans le livre de Polonius.

Pourquoi le nom « Polonius » ?

Le nom vient de la célèbre citation « Ni emprunteur ni prêteur », qui vient du personnage de Polonius dans Hamlet de Shakespeare.

Voulez-vous exécuter le code ?

L'un des objectifs de ce dépôt est d'expérimenter et de comparer différentes implémentations du même algorithme. Vous pouvez exécuter l'analyse en utilisant cargo run et vous pouvez choisir l'analyse avec -a . Ainsi, par exemple, pour exécuter un exemple d'extrait de clap, vous pouvez faire :

 > cargo +nightly run --release -- -a DatafrogOpt inputs/clap-rs/app-parser-{{impl}}-add_defaults/
    Finished release [optimized] target(s) in 0.05 secs
     Running ` target/release/borrow-check ' inputs/clap-rs/app-parser-{{impl}}-add_defaults/ ' `
--------------------------------------------------
Directory: inputs/clap-rs/app-parser-{{impl}}-add_defaults/
Time: 3.856s

Vous pouvez également essayer -a Naive pour obtenir les règles naïves (plus lisibles, plus lentes) - ce sont les règles exactes décrites dans le billet de blog. Vous pouvez également utiliser -a LocationInsensitive pour utiliser une analyse insensible à l'emplacement (plus rapide, mais peut générer des erreurs parasites).

Par défaut, cargo run imprime simplement le timing. Si vous souhaitez également voir les résultats, essayez --show-tuples (qui affichera les erreurs) et peut-être -v (pour afficher des calculs plus intermédiaires). Vous pouvez fournir --help pour obtenir plus de documents.

Comment générer vos propres entrées

Pour exécuter le vérificateur d'emprunt sur une entrée, vous devez d'abord générer les faits d'entrée. Pour cela, vous devrez exécuter rustc avec l'option -Znll-facts :

 > rustc -Znll-facts inputs/issue-47680/issue-47680.rs

Ou, pour générer les faits d'entrée d'une caisse à l'aide de l'indicateur #![feature(nll)] :

 > cargo rustc -- -Znll-facts

Cela générera un répertoire nll-facts avec un sous-répertoire par fonction :

 > ls -F nll-facts
{{impl}}-maybe_next/  main/

Vous pouvez ensuite exécuter sur ces répertoires.