Miri est un outil de détection de comportement non défini pour Rust. Il peut exécuter des binaires et tester des suites de projets cargo et détecter les codes dangereux qui ne respectent pas ses exigences de sécurité. Par exemple:
unreachable_unchecked atteint, appelant copy_nonoverlapping avec des plages qui se chevauchent, ...)bool qui n'est pas 0 ou 1, par exemple, ou un discriminant d'énumération non valide) En plus de cela, Miri vous informera également des fuites de mémoire : lorsqu'il reste de la mémoire allouée à la fin de l'exécution, et que cette mémoire n'est pas accessible depuis un static global, Miri générera une erreur.
Vous pouvez utiliser Miri pour émuler des programmes sur d'autres cibles, par exemple pour garantir que la manipulation des données au niveau octet fonctionne correctement à la fois sur les systèmes small-endian et big-endian. Voir l’interprétation croisée ci-dessous.
Miri a déjà découvert de nombreux bugs du monde réel. Si vous avez trouvé un bug avec Miri, nous apprécierions que vous nous le disiez et nous l'ajouterons à la liste !
Par défaut, Miri assure une exécution entièrement déterministe et isole le programme du système hôte. Certaines API qui accèderaient habituellement à l'hôte, telles que la collecte d'entropie pour les générateurs de nombres aléatoires, les variables d'environnement et les horloges, sont remplacées par de « fausses » implémentations déterministes. Définissez MIRIFLAGS="-Zmiri-disable-isolation" pour accéder aux véritables API du système. (En particulier, les "fausses" API RNG du système rendent Miri impropre à une utilisation cryptographique ! Ne générez pas de clés à l'aide de Miri.)
Cela dit, sachez que Miri ne détecte pas toutes les violations de la spécification Rust dans votre programme, notamment parce qu'une telle spécification n'existe pas. Miri utilise sa propre approximation de ce qui est et n'est pas un comportement indéfini dans Rust. Au meilleur de nos connaissances, tous les comportements non définis susceptibles d'affecter l'exactitude d'un programme sont détectés par Miri (bugs modulo), mais vous devriez consulter la référence pour la définition officielle du comportement non défini. Miri sera mis à jour avec le compilateur Rust pour se protéger contre UB tel que le comprend le compilateur actuel, mais il ne fait aucune promesse concernant les futures versions de rustc.
Autres mises en garde dont les utilisateurs de Miri doivent être conscients :
-Zrandomize-layout pour détecter certains de ces cas.)-Zmiri-seed , mais cela n'explorera toujours pas toutes les exécutions possibles.--target x86_64-unknown-linux-gnu pour obtenir une meilleure assistance.SeqCst sont utilisées qui ne sont pas réellement autorisées par le modèle de mémoire Rust, et elle ne peut pas produire tous les comportements éventuellement observables sur le matériel réel.De plus, Miri ne peut fondamentalement pas garantir que votre code est correct . La solidité est la propriété de ne jamais provoquer de comportement indéfini lorsqu'elle est invoquée à partir d'un code arbitraire sécurisé, même en combinaison avec un autre code sonore. En revanche, Miri peut simplement vous dire si une manière particulière d'interagir avec votre code (par exemple, une suite de tests) provoque un comportement indéfini dans une exécution particulière (il peut y en avoir plusieurs, par exemple lorsque la concurrence ou d'autres formes de non-déterminisme sont impliqués). Lorsque Miri trouve UB, votre code n'est définitivement pas solide, mais lorsque Miri ne trouve pas UB, vous devrez peut-être simplement tester plus d'entrées ou plus de choix non déterministes possibles.
Installez Miri sur Rust tous les soirs via rustup :
rustup +nightly component add miri Toutes les commandes suivantes supposent que la chaîne d'outils nocturnes est épinglée via rustup override set nightly . Vous pouvez également utiliser cargo +nightly pour chacune des commandes suivantes.
Vous pouvez maintenant exécuter votre projet dans Miri :
cargo miri test .cargo miri run .La première fois que vous exécuterez Miri, il effectuera une configuration supplémentaire et installera certaines dépendances. Il vous demandera une confirmation avant d'installer quoi que ce soit.
cargo miri run/test prend en charge exactement les mêmes indicateurs que cargo run/test . Par exemple, cargo miri test filter exécute uniquement les tests contenant filter dans leur nom.
Vous pouvez transmettre des drapeaux à Miri via MIRIFLAGS . Par exemple, MIRIFLAGS="-Zmiri-disable-stacked-borrows" cargo miri run exécute le programme sans vérifier l'alias des références.
Lors de la compilation du code via cargo miri , l'indicateur de configuration cfg(miri) est défini pour le code qui sera interprété sous Miri. Vous pouvez l'utiliser pour ignorer les cas de test qui échouent sous Miri car ils font des choses que Miri ne prend pas en charge :
# [ test ]
# [ cfg_attr ( miri , ignore ) ]
fn does_not_work_on_miri ( ) {
tokio :: run ( futures :: future :: ok :: < _ , ( ) > ( ( ) ) ) ;
}Il n'y a aucun moyen de lister toutes les choses infinies que Miri ne peut pas faire, mais l'interprète vous le dira explicitement lorsqu'il trouvera quelque chose qui n'est pas pris en charge :
error: unsupported operation: can't call foreign function: bind
...
= help: this is likely not a bug in the program; it indicates that the program
performed an operation that Miri does not support
Miri peut non seulement exécuter un binaire ou une suite de tests pour votre cible hôte, il peut également effectuer une interprétation croisée pour des cibles étrangères arbitraires : cargo miri run --target x86_64-unknown-linux-gnu exécutera votre programme comme s'il s'agissait d'un Linux. programme, quel que soit votre système d’exploitation hôte. Ceci est particulièrement utile si vous utilisez Windows, car la cible Linux est bien mieux prise en charge que les cibles Windows.
Vous pouvez également l'utiliser pour tester des plates-formes avec des propriétés différentes de celles de votre plate-forme hôte. Par exemple cargo miri test --target s390x-unknown-linux-gnu exécutera votre suite de tests sur une cible big-endian, ce qui est utile pour tester le code sensible endian.
Certaines parties de l'exécution sont sélectionnées de manière aléatoire par Miri, telles que les allocations d'adresses de base exactes qui sont stockées et l'entrelacement des threads s'exécutant simultanément. Parfois, il peut être utile d'explorer plusieurs exécutions différentes, par exemple pour vous assurer que votre code ne dépend pas d'un "super-alignement" accidentel de nouvelles allocations et pour tester différents entrelacements de threads. Cela peut être fait avec l'indicateur --many-seeds :
cargo miri test --many-seeds # tries the seeds in 0..64
cargo miri test --many-seeds=0..16
La valeur par défaut de 64 valeurs initiales différentes est assez lente, vous souhaiterez donc probablement spécifier une plage plus petite.
Lorsque vous exécutez Miri sur CI, utilisez l'extrait suivant pour installer une chaîne d'outils nocturne avec le composant Miri :
rustup toolchain install nightly --component miri
rustup override set nightly
cargo miri testVoici un exemple de tâche pour les actions GitHub :
miri :
name : " Miri "
runs-on : ubuntu-latest
steps :
- uses : actions/checkout@v4
- name : Install Miri
run : |
rustup toolchain install nightly --component miri
rustup override set nightly
cargo miri setup
- name : Test with Miri
run : cargo miri test La cargo miri setup permet de garder la sortie de l'étape de test réelle propre.
Miri ne prend pas en charge toutes les cibles prises en charge par Rust. La bonne nouvelle, cependant, est que quel que soit votre système d'exploitation/plate-forme hôte, il est facile d'exécuter du code pour n'importe quelle cible en utilisant --target !
Les cibles suivantes sont testées sur CI et devraient donc toujours fonctionner (dans le degré documenté ci-dessous) :
s390x-unknown-linux-gnu est pris en charge comme notre « cible big-endian de choix ».linux , macos ou windows , Miri devrait généralement fonctionner, mais nous ne faisons aucune promesse et nous n'exécutons pas de tests pour de telles cibles.solaris / illumos : maintenu par @devnexen. Prend en charge std::{env, thread, sync} , mais pas std::fs .freebsd : responsable recherché . Prend en charge std::env et certaines parties de std::{thread, fs} , mais pas std::sync .android : mainteneur recherché . Support très incomplet, mais un "hello world" basique fonctionne.wasi : mainteneur recherché . Support très incomplet, même la sortie standard ne fonctionne pas, mais une fonction main vide fonctionne.main .Cependant, même pour les cibles que nous prenons en charge, le degré de prise en charge de l'accès aux API de la plate-forme (telles que le système de fichiers) diffère d'une cible à l'autre : généralement, les cibles Linux bénéficient du meilleur support et les cibles macOS sont généralement à égalité. Windows est moins bien supporté.
Bien qu'il implémente le thread Rust, Miri lui-même est un interpréteur monothread. Cela signifie que lors de l'exécution cargo miri test , vous constaterez probablement une augmentation spectaculaire du temps nécessaire pour exécuter l'ensemble de votre suite de tests en raison du ralentissement inhérent de l'interprète et d'une perte de parallélisme.
Vous pouvez récupérer le parallélisme de votre suite de tests en exécutant cargo miri nextest run -jN (notez que vous aurez besoin d'installer cargo-nextest ). Cela fonctionne car cargo-nextest collecte une liste de tous les tests, puis lance une cargo miri run distincte pour chaque test. Vous devrez spécifier un -j ou --test-threads ; par défaut, cargo miri nextest run exécute un test à la fois. Pour plus de détails, consultez la documentation cargo-nextest Miri.
Remarque : ce modèle à un test par processus signifie que cargo miri test est capable de détecter des courses de données lorsque deux tests s'exécutent sur une ressource partagée, mais cargo miri nextest run ne détectera pas de telles courses.
Remarque : cargo-nextest ne prend pas en charge les doctests, voir nextest-rs/nextest#16
Lorsque vous utilisez les instructions ci-dessus, vous pouvez rencontrer un certain nombre d'erreurs de compilation déroutantes.
RUST_BACKTRACE=1 pour afficher une trace" Vous pouvez voir cela lorsque vous essayez de demander à Miri d'afficher une trace. Par défaut, Miri n'expose aucun environnement au programme, donc exécuter RUST_BACKTRACE=1 cargo miri test ne fera pas ce que vous attendez.
Pour obtenir une trace, vous devez désactiver l'isolation en utilisant -Zmiri-disable-isolation :
RUST_BACKTRACE=1 MIRIFLAGS= " -Zmiri-disable-isolation " cargo miri test std compilé par une version incompatible de rustc" Vous exécutez peut-être cargo miri avec une version de compilateur différente de celle utilisée pour créer la libstd personnalisée utilisée par Miri, et Miri n'a pas réussi à le détecter. Essayez d'exécuter cargo miri clean .
-Z et variables d'environnement Miri ajoute son propre ensemble d'indicateurs -Z , qui sont généralement définis via la variable d'environnement MIRIFLAGS . Nous documentons d’abord les indicateurs les plus pertinents et les plus couramment utilisés :
-Zmiri-address-reuse-rate= modifie la probabilité qu'une allocation hors pile libérée soit ajoutée au pool pour la réutilisation d'adresses, et la probabilité qu'une nouvelle allocation hors pile soit extraite du pool. Les allocations de pile ne sont jamais ajoutées ou retirées du pool. La valeur par défaut est 0.5 .-Zmiri-address-reuse-cross-thread-rate= modifie la probabilité qu'une allocation qui tente de réutiliser un bloc de mémoire précédemment libéré prenne également en compte les blocs libérés par d'autres threads . La valeur par défaut est 0.1 , ce qui signifie que par défaut, dans 90 % des cas où une tentative de réutilisation d'adresse est effectuée, seules les adresses du même thread seront prises en compte. La réutilisation d'une adresse d'un autre thread induit une synchronisation entre ces threads, ce qui peut masquer des courses de données et des bugs de mémoire faibles.-Zmiri-compare-exchange-weak-failure-rate= modifie le taux d'échec des opérations compare_exchange_weak . La valeur par défaut est 0.8 (donc 4 opérations faibles sur 5 échoueront). Vous pouvez le remplacer par n'importe quelle valeur comprise entre 0.0 et 1.0 , où 1.0 signifie qu'il échouera toujours et 0.0 signifie qu'il n'échouera jamais. Notez que le définir sur 1.0 entraînera probablement des blocages, car cela signifie que les programmes utilisant compare_exchange_weak ne pourront pas progresser.-Zmiri-disable-isolation désactive l'isolation de l'hôte. En conséquence, le programme a accès aux ressources de l'hôte telles que les variables d'environnement, les systèmes de fichiers et le caractère aléatoire.-Zmiri-disable-leak-backtraces désactive les rapports de backtraces pour les fuites de mémoire. Par défaut, une trace est capturée pour chaque allocation lors de sa création, juste en cas de fuite. Cela entraîne une surcharge de mémoire pour stocker des données qui ne sont presque jamais utilisées. Ce drapeau est impliqué par -Zmiri-ignore-leaks .-Zmiri-env-forward= transmet la variable d'environnement var au programme interprété. Peut être utilisé plusieurs fois pour transmettre plusieurs variables. L'exécution sera toujours déterministe si la valeur des variables transmises reste la même. N'a aucun effet si -Zmiri-disable-isolation est défini.-Zmiri-env-set== définit la variable d'environnement var sur value dans le programme interprété. Il peut être utilisé pour transmettre des variables d'environnement sans avoir besoin de modifier l'environnement hôte. Il peut être utilisé plusieurs fois pour définir plusieurs variables. Si -Zmiri-disable-isolation ou -Zmiri-env-forward est défini, les valeurs définies avec cette option auront la priorité sur les valeurs de l'environnement hôte.-Zmiri-ignore-leaks désactive le vérificateur de fuite de mémoire et permet également à certains threads restants d'exister lorsque le thread principal se termine.-Zmiri-isolation-error= configure la réponse de Miri aux opérations nécessitant un accès à l'hôte lorsque l'isolation est activée. abort , hide , warn et warn-nobacktrace sont les actions prises en charge. La valeur par défaut est abort , ce qui arrête la machine. Certaines opérations (mais pas toutes) prennent également en charge la poursuite de l'exécution avec une erreur « autorisation refusée » renvoyée au programme. warn imprime une trace complète à chaque fois que cela se produit ; warn-nobacktrace est moins verbeux et affiché au plus une fois par opération. hide masque entièrement l'avertissement.-Zmiri-num-cpus indique le nombre de processeurs disponibles qui doivent être signalés par miri. Par défaut, le nombre de processeurs disponibles est 1 . Notez que cet indicateur n'affecte en aucune façon la façon dont miri gère les threads.-Zmiri-permissive-provenance désactive l'avertissement pour les conversions d'entier en pointeur et ptr::with_exposed_provenance . Cela manquera nécessairement certains bugs car ces opérations ne sont pas implémentables de manière efficace et précise dans un désinfectant, mais cela ne manquera que les bugs qui concernent la mémoire/les pointeurs soumis à ces opérations.-Zmiri-preemption-rate configure la probabilité qu'à la fin d'un bloc de base, le thread actif soit préempté. La valeur par défaut est 0.01 (soit 1 %). Le définir sur 0 désactive la préemption.-Zmiri-report-progress oblige Miri à imprimer de temps en temps la trace de pile actuelle, afin que vous puissiez savoir ce qu'il fait lorsqu'un programme continue de s'exécuter. Vous pouvez personnaliser la fréquence d'impression du rapport via -Zmiri-report-progress= , qui imprime le rapport tous les N blocs de base.-Zmiri-seed= configure la graine du RNG que Miri utilise pour résoudre le non-déterminisme. Ce RNG est utilisé pour sélectionner les adresses de base pour les allocations, pour déterminer la préemption et l'échec de compare_exchange_weak et pour contrôler la mise en mémoire tampon du magasin pour une émulation de mémoire faible. Lorsque l'isolation est activée (valeur par défaut), elle est également utilisée pour émuler l'entropie du système. La valeur de départ par défaut est 0. Vous pouvez augmenter la couverture des tests en exécutant Miri plusieurs fois avec des valeurs de départ différentes.-Zmiri-strict-provenance permet une vérification stricte de la provenance dans Miri. Cela signifie que convertir un entier en pointeur donne un résultat avec une provenance « invalide », c'est-à-dire avec une provenance qui ne peut être utilisée pour aucun accès à la mémoire.-Zmiri-symbolic-alignment-check rend la vérification de l'alignement plus stricte. Par défaut, l'alignement est vérifié en convertissant le pointeur en un entier et en s'assurant qu'il s'agit d'un multiple de l'alignement. Cela peut conduire à des cas où un programme réussit le contrôle d'alignement par pur hasard, parce que les choses "s'avèrent être" suffisamment alignées - il n'y a pas d'UB dans cette exécution mais il y en aurait dans d'autres. Pour éviter de tels cas, la vérification de l'alignement symbolique prend uniquement en compte l'alignement demandé de l'allocation concernée et le décalage dans cette allocation. Cela évite de manquer de tels bogues, mais cela entraîne également des faux positifs lorsque le code effectue une arithmétique manuelle des entiers pour garantir l'alignement. (La méthode align_to de la bibliothèque standard fonctionne correctement dans les deux modes ; sous alignement symbolique, elle ne remplit la tranche centrale que lorsque l'allocation garantit un alignement suffisant.)Les indicateurs restants sont destinés à un usage avancé uniquement et sont plus susceptibles d'être modifiés ou supprimés. Certains d'entre eux ne sont pas fiables , ce qui signifie qu'ils peuvent empêcher Miri de détecter des cas de comportement indéfini dans un programme.
-Zmiri-disable-alignment-check désactive la vérification de l'alignement du pointeur, afin que vous puissiez vous concentrer sur d'autres échecs, mais cela signifie que Miri peut manquer des bogues dans votre programme. Utiliser ce drapeau n'est pas judicieux .-Zmiri-disable-data-race-detector désactive la vérification des courses de données. Utiliser ce drapeau n'est pas judicieux . Cela implique -Zmiri-disable-weak-memory-emulation .-Zmiri-disable-stacked-borrows désactive la vérification des règles d'alias expérimentales pour suivre les emprunts (emprunts empilés et emprunts d'arbres). Cela peut permettre à Miri de fonctionner plus rapidement, mais cela signifie également qu'aucune violation d'alias ne sera détectée. L'utilisation de cet indicateur n'est pas judicieuse (mais les règles de solidité affectées sont expérimentales). Les indicateurs ultérieurs sont prioritaires : le suivi des emprunts peut être réactivé par -Zmiri-tree-borrows .-Zmiri-disable-validation désactive l'application des invariants de validité, qui sont appliqués par défaut. Ceci est surtout utile pour se concentrer d'abord sur d'autres échecs (tels que les accès hors limites). Définir cet indicateur signifie que Miri peut manquer des bogues dans votre programme. Cependant, cela peut également aider Miri à courir plus vite. Utiliser ce drapeau n'est pas judicieux .-Zmiri-disable-weak-memory-emulation désactive l'émulation de certains effets de mémoire faible C++11.-Zmiri-native-lib= est un indicateur expérimental permettant de prendre en charge l'appel de fonctions natives depuis l'interpréteur via FFI. Les fonctions non fournies par ce fichier sont toujours exécutées via les cales Miri habituelles. AVERTISSEMENT : si un fichier .so invalide/incorrect est spécifié, cela peut provoquer un comportement non défini dans Miri lui-même ! Et bien sûr, Miri ne peut effectuer aucune vérification sur les actions entreprises par le code natif. Notez que Miri a sa propre gestion des descripteurs de fichiers, donc si vous souhaitez remplacer certaines fonctions travaillant sur les descripteurs de fichiers, vous devrez toutes les remplacer, sinon les deux types de descripteurs de fichiers seront mélangés. C'est un travail en cours ; actuellement, seuls les arguments entiers et les valeurs de retour sont pris en charge (et non, les conversions de pointeur/entier pour contourner cette limitation ne fonctionneront pas ; elles échoueront horriblement). Cela ne fonctionne également que sur les hôtes Unix pour le moment.-Zmiri-measureme= active le profilage measureme pour le programme interprété. Cela peut être utilisé pour trouver quelles parties de votre programme s'exécutent lentement sous Miri. Le profil est écrit dans un fichier dans un répertoire appelé -Zmiri-mute-stdout-stderr ignore silencieusement toutes les écritures sur stdout et stderr, mais signale au programme qu'il a réellement écrit. Ceci est utile lorsque vous n'êtes pas intéressé par la sortie réelle du programme, mais que vous souhaitez uniquement voir les erreurs et les avertissements de Miri.-Zmiri-recursive-validation est un indicateur hautement expérimental qui rend la vérification de validité récursive sous les références.-Zmiri-retag-fields[=] contrôle le moment où les emprunts empilés ré-étiquetent les récursions dans les champs. all signifie qu'il est toujours récursif (la valeur par défaut et équivalent à -Zmiri-retag-fields sans valeur explicite), none signifie qu'il ne récurre jamais, scalar signifie qu'il ne récurre que pour les types où nous émettrions également des annotations noalias dans l'IR LLVM généré ( types transmis sous forme de scalaires individuels ou de paires de scalaires). Définir cette valeur sur none n'est pas judicieux .-Zmiri-provenance-gc= configure la fréquence d'exécution du garbage collector de provenance du pointeur. La valeur par défaut est de rechercher et de supprimer la provenance inaccessible une fois tous les 10000 blocs de base. Définir cette valeur sur 0 désactive le garbage collector, ce qui entraîne une utilisation explosive de la mémoire et/ou un temps d'exécution super-linéaire pour certains programmes.-Zmiri-track-alloc-accesses affiche non seulement les allocations et les événements gratuits pour les allocations suivies, mais également les lectures et les écritures.-Zmiri-track-alloc-id=,,... affiche une trace lorsque les allocations données sont allouées ou libérées. Cela aide à déboguer les fuites de mémoire et à utiliser après des bugs gratuits. La spécification de cet argument plusieurs fois n'écrase pas les valeurs précédentes, mais ajoute ses valeurs à la liste. Répertorier un identifiant plusieurs fois n'a aucun effet.-Zmiri-track-pointer-tag=,,... affiche une trace lorsqu'une balise de pointeur donnée est créée et quand (le cas échéant) elle est extraite d'une pile d'emprunt (c'est là que la balise devient invalide et toute utilisation future entraînera une erreur). Cela vous aide à découvrir pourquoi UB se produit et où dans votre code serait un bon endroit pour le rechercher. La spécification de cet argument plusieurs fois n'écrase pas les valeurs précédentes, mais ajoute ses valeurs à la liste. Répertorier une balise plusieurs fois n'a aucun effet.-Zmiri-track-weak-memory-loads affiche une trace lorsque l'émulation de mémoire faible renvoie une valeur obsolète à partir d'un chargement. Cela peut aider à diagnostiquer les problèmes qui disparaissent sous -Zmiri-disable-weak-memory-emulation .-Zmiri-tree-borrows remplace les emprunts empilés par les règles des emprunts d'arbres. Tree Borrows est encore plus expérimental que Stacked Borrows. Bien que Tree Borrows soit toujours valable dans le sens de détecter toutes les violations d'alias que les versions actuelles du compilateur pourraient exploiter, il est probable que l'éventuel modèle d'alias final de Rust sera plus strict que Tree Borrows. En d’autres termes, si vous utilisez Tree Borrows, même si votre code est accepté aujourd’hui, il pourrait être déclaré UB à l’avenir. C’est beaucoup moins probable avec les emprunts empilés.-Zmiri-force-page-size= remplace la taille de page par défaut pour une architecture, par multiples de 1 ko. 4 est la valeur par défaut pour la plupart des cibles. Cette valeur doit toujours être une puissance de 2 et non nulle.-Zmiri-unique-is-unique effectue des vérifications d'alias supplémentaires pour core::ptr::Unique pour s'assurer qu'il pourrait théoriquement être considéré noalias . Cet indicateur est expérimental et n'a d'effet que lorsqu'il est utilisé avec -Zmiri-tree-borrows . Certains drapeaux natifs rustc -Z sont également très pertinents pour Miri :
-Zmir-opt-level contrôle le nombre d'optimisations MIR effectuées. Miri remplace la valeur par défaut par 0 ; Sachez que l'utilisation d'un niveau supérieur peut faire manquer à Miri des bogues dans votre programme, car ils ont été optimisés.-Zalways-encode-mir permet à rustc de vider MIR même pour des fonctions complètement monomorphes. Ceci est nécessaire pour que Miri puisse exécuter de telles fonctions, donc Miri définit cet indicateur par défaut.-Zmir-emit-retag contrôle si les instructions Retag sont émises. Miri active cela par défaut car cela est nécessaire pour les emprunts empilés et les emprunts d'arbres.De plus, Miri reconnaît certaines variables d'environnement :
MIRIFLAGS définit des indicateurs supplémentaires à transmettre à Miri.MIRI_LIB_SRC définit le répertoire dans lequel Miri attend les sources de la bibliothèque standard qu'elle va construire et utiliser pour l'interprétation. Ce répertoire doit pointer vers le sous-répertoire library d'une extraction de référentiel rust-lang/rust .MIRI_SYSROOT indique la racine système à utiliser. Lorsque vous utilisez cargo miri test / cargo miri run , cela ignore la configuration automatique - ne définissez cette option que si vous ne souhaitez pas utiliser la racine système créée automatiquement. Lors de l'appel cargo miri setup , cela indique où la racine système sera placée.MIRI_NO_STD s'assure que la racine système de la cible est construite sans libstd. Cela permet de tester et d'exécuter des programmes no_std. Ceci ne devrait généralement pas être utilisé ; Miri a une heuristique pour détecter les cibles sans norme en fonction du nom de la cible. Définir cela sur une cible prenant en charge libstd peut conduire à des résultats confus. extern de Miri Miri fournit des fonctions extern que les programmes peuvent importer pour accéder aux fonctionnalités spécifiques à Miri. Ils sont déclarés dans /tests/utils/miri_extern.rs.
Les binaires qui n'utilisent pas la bibliothèque standard sont censés déclarer une fonction comme celle-ci afin que Miri sache où elle est censée commencer son exécution :
# [ cfg ( miri ) ]
# [ no_mangle ]
fn miri_start ( argc : isize , argv : * const * const u8 ) -> isize {
// Call the actual start function that your project implements, based on your target's conventions.
} Si vous souhaitez contribuer à Miri, super ! Veuillez consulter notre guide de contribution.
Pour obtenir de l'aide sur l'exécution de Miri, vous pouvez ouvrir un problème ici sur GitHub ou utiliser le flux Miri sur Rust Zulip.
Ce projet a débuté dans le cadre d'un cours de recherche de premier cycle en 2015 par @solson à l'Université de la Saskatchewan. Des diapositives et un rapport sont disponibles pour ce projet. En 2016, @oli-obk s'est joint pour préparer Miri à être éventuellement utilisé comme évaluateur const dans le compilateur Rust lui-même (essentiellement, pour les éléments const et static ), en remplacement de l'ancien évaluateur qui travaillait directement sur l'AST. En 2017, @RalfJung a effectué un stage chez Mozilla et a commencé à développer Miri vers un outil de détection de comportement indéfini, et également à utiliser Miri comme moyen d'explorer les conséquences de diverses définitions possibles d'un comportement indéfini dans Rust. Le transfert par @oli-obk du moteur Miri dans le compilateur s'est finalement achevé début 2018. Pendant ce temps, plus tard cette année-là, @RalfJung a effectué un deuxième stage, développant davantage Miri avec la prise en charge de la vérification des invariants de type de base et de la vérification que les références sont utilisées conformément à leurs restrictions d'alias.
Miri a déjà trouvé un certain nombre de bugs dans la bibliothèque standard de Rust et au-delà, dont nous rassemblons certains ici. Si Miri vous a aidé à trouver un bug UB subtil dans votre code, nous apprécierions qu'un PR l'ajoute à la liste !
Bugs définitifs trouvés :
Debug for vec_deque::Iter accédant à la mémoire non initialiséeVec::into_iter effectuant une lecture ZST non alignéeFrom<&[T]> for Rc créant une référence pas suffisamment alignéeBTreeMap créant une référence partagée pointant vers une allocation trop petiteVec::append créant une référence pendantestr transformer une référence partagée en une référence mutablerand effectue des lectures non alignéesposix_memalign de manière non validegetrandom appelle l'appel système getrandom d'une manière non valideVec et BTreeMap perdent de la mémoire dans certaines conditions (paniques)beefEbrCell utilise incorrectement la mémoire non initialiséeservo_arc créant une référence partagée pendanteencoding_rs effectuant une arithmétique de pointeur hors limitesVec::from_raw_partsAtomicPtr et Box::from_raw_inThinVeccrossbeam-epoch appelant assume_init sur un MaybeUninit partiellement initialiséinteger-encoding déréférençant un pointeur mal alignérkyv construisant un Box<[u8]> à partir d'une allocation suralignéearc-swapthread::scoperegex ne gère pas correctement les tampons Vec non alignéscompare_exchange_weak dans once_cellvec::IntoIterIterator::collect sur placeportable-atomic-utilstd::mpsc (code d'origine dans crossbeam)Les violations des emprunts empilés trouvées sont probablement des bugs (mais les emprunts empilés ne sont actuellement qu'une expérience) :
VecDeque::drain créant des références mutables qui se chevauchentBTreeMapBTreeMap créant des références mutables qui chevauchent des références partagéesBTreeMap::iter_mut créant des références mutables qui se chevauchentBTreeMap à l'aide de pointeurs bruts en dehors de leur zone mémoire valideLinkedList créant des références mutables qui se chevauchentVec::push invalidant les références existantes dans le vecteuralign_to_mut violant l'unicité des références mutablessized-chunks créant des références mutables d'aliasString::push_str invalidant les références existantes dans la chaîneryu utilisant des pointeurs bruts en dehors de leur zone de mémoire valideEnv utilisant un pointeur brut en dehors de sa zone mémoire valideVecDeque::iter_mut créant des références mutables qui se chevauchent<[T]>::copy_within utilisant un prêt après l'avoir invalidé Autorisé sous l'un ou l'autre des
à votre choix.
Sauf indication contraire explicite de votre part, toute contribution que vous soumettez intentionnellement pour être incluse dans l'œuvre bénéficiera d'une double licence comme ci-dessus, sans termes ou conditions supplémentaires.
