error: Undefined Behavior: attempting a write access using <288> at alloc124[0x0], but that tag does not exist in the borrow stack for this location
MIRI においてスタックのアイテムが削除済だった場合のエラー。
まず、ポインタ (参照や生ポインタ) の作成時にその参照先と参照元とを紐づける。そして、ポインタの利用時にはその紐づけが残っている事を確認する。ただし、各ポインタはその利用時に競合する紐づけがあると勝手にそれらを外してしまう。そのため、紐づけが外されたポインタを使うと UB となる。
上記の実現のために、メモリや変数には以下のメタ情報が付加される。
ここで、スタックのアイテムには現在の参照元の情報が、タグを含め保管される仕組となる。なお、参照用のタグではそれぞれに固有のものを使うが、生ポインタ用のタグでは個々を区別しないため共通のタグ (記号⊥) を使う。
スタックのアイテムには以下の種類がある (t はタグ)。
上記の構造を利用して、以下のアルゴリズムが適用される。
変数 var を生ポインタ var_mtp と可変参照 var_mut から参照する。
この場合、メモリの各アドレスの値、そしてスタックは以下のようになる。
ここで、var_mtp を使うには SharedRW(⊥) が必要になる。
しかし、その上には Unique(t1) があり邪魔なのでポップする。
すると、それに紐づいていた var_mut は使えなくなってしまう。
以上をソースコードにすると以下のようになる。
fn main() {
let mut var = 0;
let var_mtp = &mut var as *mut _;
let var_mut = unsafe { &mut *var_mtp };
unsafe { *var_mtp = 1 };
*var_mut = 2;
}
error: Undefined Behavior: attempting a write access using <288> at alloc124[0x0], but that tag does not exist in the borrow stack for this location
--> src\main.rs:6:5
|
6 | *var_mut = 2;
| ^^^^^^^^^^^^ this error occurs as part of an access at alloc124[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: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <288> was created by a Unique retag at offsets [0x0..0x4]
--> src\main.rs:4:28
|
4 | let var_mut = unsafe { &mut *var_mtp };
| ^^^^^^^^^^^^^
help: <288> was later invalidated at offsets [0x0..0x4] by a write access
--> src\main.rs:5:14
|
5 | unsafe { *var_mtp = 1 };
| ^^^^^^^^^^^^
= note: BACKTRACE (of the first span):
= note: inside `main` at src\main.rs:6:5: 6:17