Propriété et sécurité de la mémoire

<!-- verified-against: seed-llvm; examples: docs-examples-test -->

seed utilise la propriété, les ressources de déplacement uniquement, le lexical loans/provenance, capacités structurelles, nettoyage déterministe, linear t, et les régions. Il n'a pas de GC, de syntaxe de durée de vie du vérificateur d'emprunt ou de déroulement d'exception. Les règles sémantiques faisant autorité sont en seed/compiler/llvm/SEMANTIC_RULES.md; les limites actuelles sont suivies dans État actuel.

Copier, déplacer, emprunter, cloner

Les scalaires et les agrégats contenant uniquement des champs de copie copient. string, bytes, shared_bytes, propriétaires d'utilisateurs-destructeurs, agrégats de ressources et linear t obéir à leur move/clone/cleanup capacités.

shared_bytes n'est pas copiable au niveau du bit : .clone() conserve explicitement un autre handle sans copier la charge utile. Le clonage appartenant à string/bytes ou aux agrégats les contenant peut être attribué. Les effets et les capacités d'allocation de clone survivent à la compilation .sdi sans source.

Places et propriété partielle

Le compilateur suit les éléments locaux, les champs et les champs imbriqués, les index de tableau fixe connus, les charges utiles ADT actives, les champs d'union brute, tuple/array/nominal agrégats, instances génériques, option/result, valeurs de fonction, channels/tasks, alias, blocs, appels, retours et jointures de flux de contrôle.

Un déménagement partiel rend le lieu déplacé indisponible et empêche son utilisation par le propriétaire entier lorsque l'intégralité est requise. Les champs restants indépendants restent utilisables lorsqu'un destructeur d'utilisateur ne nécessite pas de propriétaire complet. Les mouvements d'index dynamique des éléments de ressource restent rejetés car l'ensemble de nettoyage dépendrait de l'exécution.

Nettoyage

Le nettoyage est planifié à partir des faits de propriété saisis par HIR, vérifiés séparément et abaissés sur des sorties structurées normales. Les propriétaires en direct nettoient exactement une fois dans l’ordre inverse d’initialisation réussie. La réaffectation nettoie le propriétaire actif précédent avant de stocker le remplacement. Les boucles utilisent des points fixes de flux de données entre l’entrée, les bords arrière, la pause, la suite et le retour.

La panique, le piège et l'abandon se terminent sans se dérouler. Ils n'exécutent pas de nettoyage lexical ni de destructeurs d'utilisateurs.

Destructeurs

fn TypeName.drop() reçoit une consommation implicite self. Il doit être unique et renvoyer void. L'appel manuel de value.drop() consomme le propriétaire, empêchant ainsi un deuxième appel automatique. Les propriétaires restitués transfèrent leur obligation de nettoyage à l'appelant. Les globaux Cleanup/resource sont rejetés car le démontage global n'est pas un service de langage implicite.

Le nettoyage ADT est distribué uniquement sur la variante active. Les syndicats bruts exigent une discipline dangereuse sur le terrain ; Les alternatives étiquetées sûres doivent utiliser des ADT ou un wrapper audité.

Propriété de la fermeture

Une simple fermeture |...| possède un stockage de capture de pile généré par le compilateur. L'initialisation de la capture suit le premier ordre d'utilisation lexicale : les valeurs compatibles avec la copie sont copiées et les autres valeurs possédées sont déplacées. Les captures sont immuables ; une capture de ressource déplacée rend la fermeture elle-même uniquement en mouvement. Le propriétaire supprime les captures en direct exactement une fois dans l'ordre d'initialisation inverse.

Les fermetures simples sont réutilisables et ne s'échappent pas. Ils ne peuvent pas capturer les valeurs qui ne peuvent pas rester stockées en toute sécurité après un appel, notamment les vues, les captures mutables, les valeurs liées à une région, raw/reference des valeurs, format_args, ou des lieux déjà déplacés. Ils ne peuvent pas être renvoyés, conservés dans une portée externe, envoyés à une tâche ou transmis à travers une limite de pointeur de fonction de plateforme.

box |...| alloue explicitement le stockage de capture et renvoie Result<box fn(...) -> T, alloc_error>. Le propriétaire en boîte peut être renvoyé ou stocké mais reste uniquement mobile, non clonable et non envoyable. L’échec de l’allocation supprime les captures transférées une fois ; un drop réussi exécute le drop de capture et libère l'environnement une fois. Une fermeture en boîte allouée sous region(...) ne peut pas échapper à cette région.

Valeurs linéaires

linear t préserve tet ajoute une obligation d'une seule fois. Il supprime copy/clone/shared capacité tout en conservant les faits valides de déplacement, d’emprunt, d’envoi, de synchronisation et de nettoyage. L'implémentation propage l'obligation à travers des alias, des blocs, des agrégats, option/result, ADT, génériques, canaux, valeurs de fonction et appels indirects, capture de tâches, parameters/returns, et schéma-17 .sdi.

Laisser une valeur linéaire active à la sortie de l'étendue, la consommer deux fois, la cloner, la supprimer, l'écraser ou la stocker dans un stockage non linéaire préexistant est rejetée.

Texte, tampons et vues

• le texte littéral est emprunté de manière statique str;
• string appartient à UTF-8 valide et se déplace ;
• bytes est un propriétaire et des mouvements binaires mutables uniques ;
• shared_bytes est un handle partagé en lecture seule avec un clone explicite ;
• le string détenu emprunte automatiquement sous le nom de str lorsque prévu ;
• dérivé du propriétaire str, []t, et mut []t les vues portent la provenance ;
• une vue en direct empêche les conflits de déplacement, d'écrasement, de libération, de réaffectation ou mutation de son propriétaire adossant ; une écriture est vérifiée uniquement par rapport aux prêts étrangers, donc l'écriture via la vue exclusive en direct qui possède le lieu (ou via une partition sœur du même groupe de partition) est la propre autorité de cette vue, tandis que tout autre prêt actif se chevauchant rend l'écriture illégale même lorsque l'élément écrit est une copie ;
• mut []t.split_at_mut(index) vérifie index <= len, n'attribue rien et renvoie deux vues lexicales exclusives ; match les liaisons peuvent utiliser mut name;
• le propriétaire du support ne peut pas être lu, déplacé, redimensionné ou libéré pendant que le Le tuple de partition est actif ; les partitions imbriquées restent confinées à leur parent ;
• le retour ou le stockage d'une vue n'est autorisé que lorsque son static/input/receiver la provenance prouve une durée de vie suffisante ;
• la sélection conditionnelle porte l'union finie de toutes les origines possibles ; l'implémentation limite cet ensemble à huit origines et transforme le débordement ou la provenance indirecte non prise en charge en unknown, jamais en preuve à vie ;
• les résumés d'appels directs .sdi préservent ces origines symboliques à travers les modules ; Le schéma de cache HIR 9 stocke les mêmes enregistrements indépendants de la cible, tandis que chaque famille de sécurité est réexécutée après la réutilisation du cache ;
• local/temporary-derived les vues ne peuvent pas s'échapper via les retours, les globals, conteneurs, tâches ou bibliothèque dynamique ABI.

Il n'y a pas de syntaxe à vie. @borrow les méthodes de réception créent des emprunts lexicaux partagés ; les vues renvoyées restent liées au récepteur via .sdi résumés. Les fonctions gratuites peuvent également renvoyer des données statiques ou dérivées d'entrées. str/vues en tranches ; une vue dérivée du propriétaire d'un local string/bytes reste un V001 s'échapper. @mut Les méthodes de réception créent un prêt exclusif limité à l'appel et modifient directement la place de l'appelant. Les récepteurs immuables et les vues en direct qui se chevauchent sont rejetés ; aucun mouvement ou clone n'est masqué par l'appel.

Régions

fn work() -> Result<i64, alloc_error> {
    region(4096) {
        // allocating operations use the active checked bump allocator
        Ok(42)
    }
}

La capacité est évaluée une fois, l'allocation alignée est vérifiée en cas de débordement et l'épuisement est renvoyé sous la forme alloc_error par les API faillibles. Les régions imbriquées sont LIFO. Les ressources du corps sont nettoyées avant que le stockage de sauvegarde ne soit libéré. Les propriétaires, vues et pointeurs sécurisés liés à une région ne peuvent pas s'échapper via un résultat, un retour ou une affectation à une liaison externe.

Le travail généré capture le contexte de l’allocateur. Les tâches liées à la région restent structurées et se rejoignent avant le nettoyage de la région.

Transfert de tâches

spawn enregistrements copy/move mode capture. Conserver l'original et une valeur de tâche nécessite un clone explicite. Franchir les limites d'une tâche nécessite send; l'accès partagé nécessite également sync. L’état global mutable ne peut pas être capturé. Chaque groupe de tâches se vide avant que son propriétaire lexical ne nettoie les ressources.

if let et while let sont des formes de surface sur match: les deux se transforment en un match à deux bras dont le deuxième bras est le complément, donc la liaison, le transfert de propriété, l'exhaustivité et le nettoyage sont exactement les règles du match. if let Some(x) = e nomme son complément None; une autre variante de modèle conserve un bras générique, qui est rejeté lorsque le candidat transporte une charge utile de déplacement uniquement, car un bras générique ne remplit pas l'obligation de propriété de cette charge utile - écrivez l'explicite match des armes là-bas. Un schéma irréfutable rend le bras complémentaire inaccessible et est rejeté. Un littéral de tableau répété [value; count] s'étend à count éléments d'une valeur littérale et prend son type d'élément du type de tableau attendu, donc let slots: [4]usize = [0; 4] n'a pas besoin de plâtre ; la valeur doit être un littéral, une conversion d'un littéral ou un tableau de ceux-ci, et le nombre est un littéral entier positif d'au plus 65 536.

Limite dangereuse

L'allocation brute, l'accès au pointeur, le FFI, les appels système, l'atomique, l'accès volatile, les conversions d'espace d'adressage, l'accès brut à l'union et l'assemblage brut nécessitent unsafe. Le code non sécurisé ne désactive pas la propriété des valeurs sûres environnantes ; il suppose des obligations spécifiques qui devraient être cachées derrière des enveloppes de sécurité étroites et auditées.

unsafe struct paramètres : un unsafe struct avec un champ de pointeur brut et @repr("null_niche") est un type de ressource qui ne peut pas être transmis par valeur en tant que paramètre de fonction. Le transmettre par valeur déplace le propriétaire sous-jacent, le rendant indisponible pour une utilisation ultérieure. Méthodes avec @mut Le récepteur nécessite un emplacement mutable et ne peut pas être appelé sur une valeur déplacée. Pour utiliser un tel type au-delà des limites des fonctions, insérez la logique ou renvoyez le propriétaire à côté du résultat.

Quelles versions changent

--release et --release-small optimisent la même sémantique sécurisée. Les contrôles de limites, discriminants, de provenance, de propriété et de nettoyage restent en vigueur à moins qu'ils ne soient prouvés redondants. Aucun profil de version non vérifié n'est implémenté.

Livre de recettes de propriété

Ce sont les vingt modèles de construction récurrents utilisés par le Grove et les appareils du compilateur. La partie importante de chaque modèle est l’invariant qu’il préserve ; lorsqu'une valeur ne peut pas satisfaire cet invariant, conservez l'opération dans un adaptateur unsafe étroit au lieu d'affaiblir le modèle propriétaire.

Pour un exemple de diagnostic fonctionnel, commencez par la durée de consommation dans S001, puis appliquez le plus petit modèle ci-dessus qui restaure un seul propriétaire. Le compilateur doit continuer à rejeter les mouvements dynamiques, les échappements de régions, les rappels dangereux et les nettoyages manquants, même lorsqu'une construction différente serait plus courte.

Exemple de travail S001 (se déplacer entre un appel et une branche)

Un nouvel utilisateur déplace title vers report lors de la construction de la structure, puis consomme la liaison déplacée dans une branche ultérieure :

struct Report {
    title: string
}

fn main() -> Result<i64, alloc_error> {
    let title = "quarterly".to_string()?
    let report = Report { title: title }
    if len(report.title) == 9 as usize {
        let again = title
        Ok(0)
    } else {
        Ok(1)
    }
}

Le compilateur résout ce problème à partir du diagnostic seul : error[S001] nomme le chemin de propriété (title), un note: ownership path declared here pointe sur la liaison, un note: move occurred here pointe sur la construction de la structure consommatrice et la ligne help: indique la direction de réparation (clone 'title' explicitly before moving). Le plus petit correctif clone le titre dans le rapport et déplace l'original vers son propriétaire final avant la branche, de sorte que chaque branche se termine avec la même disponibilité de ressources :

struct Report {
    title: string
}

fn main() -> Result<i64, alloc_error> {
    let title = "quarterly".to_string()?
    let report = Report { title: title.clone() }
    let again = title
    if len(report.title) == 9 as usize {
        let total = len(again) + len(report.title)
        Ok(if total == 18 as usize { 0 } else { 1 })
    } else {
        let rest = len(again)
        Ok(if rest == 9 as usize { 2 } else { 3 })
    }
}

Chaque modèle ci-dessus (et les deux moitiés de cet exemple concret) est un programme de corpus exécutable vérifié par make -C seed/compiler/llvm gate47-cookbook-test; le corpus vit dans seed/compiler/llvm/tests/cookbook/.