Miri : Détecter les Stacked Borrow

Bonjour à toutes et à tous 😀

Appendum sur l'article sur les unsafe_cell.

Dans une précédente version de celui-ci, j'avais écrit le code suivant.

let cell = UnsafeCell::new(0);
unsafe {

    let ptr1 = &mut *cell.get();
    let ptr2 = &mut *cell.get();

    *cell.get() += 1;
    *ptr1 += 1;
    *ptr2 += 1;
    dbg!(*cell.get()); // 3
}

On m'a fait comprendre et je les remercie chaleureusement que le code du dessus qui bien que compilant n'a pas de sens dans le cadre du borrow checker, ce que je voyais très bien, mais j'étais incapble d'expliquer pourquoi cela compilait.

Maintenant j'ai plus de billes.

Ceci est appelé Stacked Borrow et est une partie cachée de Rust (et non-stabilisée) dont je n'avais pas connaissance.

Pour vérifier ces comportement, on peut utiliser un outil qui se nomme miri qui va semi compiler le code et le faire tourner dans une "VM" pour vérifier les comportement étrange ou non défini de la mémoire.

Pour l'installer

rustup component add miri

Pour vérifier

cargo miri run

Ce qui donne

         *ptr1 += 1;
         ^^^^^^^^^^
         |
         attempting a read access using <1900> at alloc798[0x0], but 
         that tag does not exist in the borrow stack for this location
         this error occurs as part of an access at alloc798[0x0..0x4]

   = help: this indicates a potential bug in the program: it performed 
   an invalid operation, but the Stacked Borrows rules it violated 
   are still experimental
help: <1900> was created by a Unique retag at offsets [0x0..0x4]

Je n'ai pas encore les compétences pour tout comprendre, mais en tout ce sont des comportements bizarres et vérifiables de cette manière.

Ce code par contre ne viole ni le Borrow Checker ni le Stacked Borrow.

let cell = UnsafeCell::new(0);
unsafe {

    let ptr1 = cell.get();
    let ptr2 = cell.get();

    *cell.get() += 1;
    *ptr1 += 1;
    *ptr2 += 1;
    dbg!(*cell.get()); // 3
}

Voilà, mes excuses pour n'avoir pas suffisamment creusé. 😟

Auteur: Akanoa

Je découvre, j'apprends, je comprends et j'explique ce que j'ai compris dans ce blog.

Ce travail est sous licence CC BY-NC-SA 4.0.