std: add safety comments · model-checking/verify-rust-std@d6fadf5 (original) (raw)
`@@ -50,6 +50,7 @@ unsafe impl Sync for Storage {}
`
50
50
``
51
51
`struct Value<T: 'static> {
`
52
52
`value: T,
`
``
53
`` +
// INVARIANT: if this value is stored under a TLS key, key must be that key.
``
53
54
`key: Key,
`
54
55
`}
`
55
56
``
`@@ -73,10 +74,14 @@ impl<T: 'static> Storage {
`
73
74
`// is not running) + it is coming from a trusted source (self).
`
74
75
`unsafe { &(*ptr).value }
`
75
76
`} else {
`
``
77
`+
// SAFETY: trivially correct.
`
76
78
`unsafe { Self::try_initialize(key, ptr, i, f) }
`
77
79
`}
`
78
80
`}
`
79
81
``
``
82
`+
/// # Safety
`
``
83
`` +
/// * key must be the result of calling self.key.force()
``
``
84
`` +
/// * ptr must be the current value associated with key.
``
80
85
`unsafe fn try_initialize(
`
81
86
`key: Key,
`
82
87
`ptr: *mut Value,
`
`@@ -91,11 +96,16 @@ impl<T: 'static> Storage {
`
91
96
`let value = Box::new(Value { value: i.and_then(Option::take).unwrap_or_else(f), key });
`
92
97
`let ptr = Box::into_raw(value);
`
93
98
``
94
``
`-
let old = unsafe { get(key) as *mut Value };
`
95
``
`` -
// SAFETY: ptr is a correct pointer that can be destroyed by the key destructor.
``
96
``
`-
unsafe {
`
``
99
`+
// SAFETY:
`
``
100
`` +
// * key came from a LazyKey and is thus correct.
``
``
101
`` +
// * ptr is a correct pointer that can be destroyed by the key destructor.
``
``
102
`+
// * the value is stored under the key that it contains.
`
``
103
`+
let old = unsafe {
`
``
104
`+
let old = get(key) as *mut Value;
`
97
105
`set(key, ptr as *mut u8);
`
98
``
`-
}
`
``
106
`+
old
`
``
107
`+
};
`
``
108
+
99
109
`if !old.is_null() {
`
100
110
`// If the variable was recursively initialized, drop the old value.
`
101
111
`` // SAFETY: We cannot be inside a LocalKey::with scope, as the
``
`@@ -123,8 +133,10 @@ unsafe extern "C" fn destroy_value<T: 'static>(ptr: *mut u8) {
`
123
133
`abort_on_dtor_unwind(|| {
`
124
134
`let ptr = unsafe { Box::from_raw(ptr as *mut Value) };
`
125
135
`let key = ptr.key;
`
``
136
`` +
// SAFETY: key is the TLS key ptr was stored under.
``
126
137
`unsafe { set(key, ptr::without_provenance_mut(1)) };
`
127
138
`drop(ptr);
`
``
139
`` +
// SAFETY: key is the TLS key ptr was stored under.
``
128
140
`unsafe { set(key, ptr::null_mut()) };
`
129
141
`});
`
130
142
`}
`