Miri : Détecter les Stacked Borrow

Lecture 2 min. ‱


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Ă©. 😟