@@ -168,11 +168,29 @@ impl fmt::Display for MiriMemoryKind {
168
168
/// Pointer provenance.
169
169
#[ derive( Clone , Copy ) ]
170
170
pub enum Provenance {
171
+ /// For pointers with concrete provenance. we exactly know which allocation they are attached to
172
+ /// and what their borrow tag is.
171
173
Concrete {
172
174
alloc_id : AllocId ,
173
175
/// Borrow Tracker tag.
174
176
tag : BorTag ,
175
177
} ,
178
+ /// Pointers with wildcard provenance are created on int-to-ptr casts. According to the
179
+ /// specification, we should at that point angelically "guess" a provenance that will make all
180
+ /// future uses of this pointer work, if at all possible. Of course such a semantics cannot be
181
+ /// actually implemented in Miri. So instead, we approximate this, erroring on the side of
182
+ /// accepting too much code rather than rejecting correct code: a pointer with wildcard
183
+ /// provenance "acts like" any previously exposed pointer. Each time it is used, we check
184
+ /// whether *some* exposed pointer could have done what we want to do, and if the answer is yes
185
+ /// then we allow the access. This allows too much code in two ways:
186
+ /// - The same wildcard pointer can "take the role" of multiple different exposed pointers on
187
+ /// subsequenct memory accesses.
188
+ /// - In the aliasing model, we don't just have to know the borrow tag of the pointer used for
189
+ /// the access, we also have to update the aliasing state -- and that update can be very
190
+ /// different depending on which borrow tag we pick! Stacked Borrows has support for this by
191
+ /// switching to a stack that is only approximately known, i.e. we overapproximate the effect
192
+ /// of using *any* exposed pointer for this access, and only keep information about the borrow
193
+ /// stack that would be true with all possible choices.
176
194
Wildcard ,
177
195
}
178
196
@@ -1122,19 +1140,16 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
1122
1140
_ => { }
1123
1141
}
1124
1142
}
1125
- let absolute_addr = intptrcast:: GlobalStateInner :: rel_ptr_to_addr ( ecx, ptr) ?;
1126
1143
let tag = if let Some ( borrow_tracker) = & ecx. machine . borrow_tracker {
1127
1144
borrow_tracker. borrow_mut ( ) . base_ptr_tag ( ptr. provenance , & ecx. machine )
1128
1145
} else {
1129
1146
// Value does not matter, SB is disabled
1130
1147
BorTag :: default ( )
1131
1148
} ;
1132
- Ok ( Pointer :: new (
1133
- Provenance :: Concrete { alloc_id : ptr. provenance , tag } ,
1134
- Size :: from_bytes ( absolute_addr) ,
1135
- ) )
1149
+ intptrcast:: GlobalStateInner :: ptr_from_rel_ptr ( ecx, ptr, tag)
1136
1150
}
1137
1151
1152
+ /// Called on `usize as ptr` casts.
1138
1153
#[ inline( always) ]
1139
1154
fn ptr_from_addr_cast (
1140
1155
ecx : & MiriInterpCx < ' mir , ' tcx > ,
@@ -1143,6 +1158,9 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
1143
1158
intptrcast:: GlobalStateInner :: ptr_from_addr_cast ( ecx, addr)
1144
1159
}
1145
1160
1161
+ /// Called on `ptr as usize` casts.
1162
+ /// (Actually computing the resulting `usize` doesn't need machine help,
1163
+ /// that's just `Scalar::try_to_int`.)
1146
1164
fn expose_ptr (
1147
1165
ecx : & mut InterpCx < ' mir , ' tcx , Self > ,
1148
1166
ptr : Pointer < Self :: Provenance > ,
@@ -1160,11 +1178,17 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
1160
1178
1161
1179
/// Convert a pointer with provenance into an allocation-offset pair,
1162
1180
/// or a `None` with an absolute address if that conversion is not possible.
1181
+ ///
1182
+ /// This is called when a pointer is about to be used for memory access,
1183
+ /// an in-bounds check, or anything else that requires knowing which allocation it points to.
1184
+ /// The resulting `AllocId` will just be used for that one step and the forgotten again
1185
+ /// (i.e., we'll never turn the data returned here back into a `Pointer` that might be
1186
+ /// stored in machine state).
1163
1187
fn ptr_get_alloc (
1164
1188
ecx : & MiriInterpCx < ' mir , ' tcx > ,
1165
1189
ptr : Pointer < Self :: Provenance > ,
1166
1190
) -> Option < ( AllocId , Size , Self :: ProvenanceExtra ) > {
1167
- let rel = intptrcast:: GlobalStateInner :: abs_ptr_to_rel ( ecx, ptr) ;
1191
+ let rel = intptrcast:: GlobalStateInner :: ptr_get_alloc ( ecx, ptr) ;
1168
1192
1169
1193
rel. map ( |( alloc_id, size) | {
1170
1194
let tag = match ptr. provenance {
0 commit comments