Skip to content

Commit ad59f75

Browse files
committed
-Zmiri-permissive-provenance and SB wildcard tags
1 parent a25b65e commit ad59f75

File tree

5 files changed

+139
-44
lines changed

5 files changed

+139
-44
lines changed

src/bin/miri.rs

+5
Original file line numberDiff line numberDiff line change
@@ -368,6 +368,11 @@ fn main() {
368368
miri_config.tag_raw = true;
369369
miri_config.check_number_validity = true;
370370
}
371+
"-Zmiri-permissive-provenance" => {
372+
miri_config.permissive_provenance = true;
373+
miri_config.tag_raw = true;
374+
miri_config.check_number_validity = true;
375+
}
371376
"-Zmiri-track-raw-pointers" => {
372377
eprintln!(
373378
"WARNING: -Zmiri-track-raw-pointers has been renamed to -Zmiri-tag-raw-pointers, the old name is deprecated."

src/eval.rs

+4
Original file line numberDiff line numberDiff line change
@@ -112,6 +112,9 @@ pub struct MiriConfig {
112112
pub panic_on_unsupported: bool,
113113
/// Which style to use for printing backtraces.
114114
pub backtrace_style: BacktraceStyle,
115+
/// Whether to enforce "permissive provenance" rules. Enabling this means int2ptr casts return
116+
/// pointers with union provenance of all exposed pointers (and SB tags, if enabled).
117+
pub permissive_provenance: bool,
115118
/// Whether to enforce "strict provenance" rules. Enabling this means int2ptr casts return
116119
/// pointers with an invalid provenance, i.e., not valid for any memory access.
117120
pub strict_provenance: bool,
@@ -140,6 +143,7 @@ impl Default for MiriConfig {
140143
measureme_out: None,
141144
panic_on_unsupported: false,
142145
backtrace_style: BacktraceStyle::Short,
146+
permissive_provenance: false,
143147
strict_provenance: false,
144148
}
145149
}

src/intptrcast.rs

+23-12
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,9 @@ pub struct GlobalStateInner {
2727
/// This is used as a memory address when a new pointer is casted to an integer. It
2828
/// is always larger than any address that was previously made part of a block.
2929
next_base_addr: u64,
30+
/// Whether to enforce "permissive provenance" rules. Enabling this means int2ptr casts return
31+
/// pointers with union provenance of all exposed pointers (and SB tags, if enabled).
32+
permissive_provenance: bool,
3033
/// Whether to enforce "strict provenance" rules. Enabling this means int2ptr casts return
3134
/// pointers with an invalid provenance, i.e., not valid for any memory access.
3235
strict_provenance: bool,
@@ -39,6 +42,7 @@ impl GlobalStateInner {
3942
base_addr: FxHashMap::default(),
4043
exposed: FxHashSet::default(),
4144
next_base_addr: STACK_ADDR,
45+
permissive_provenance: config.permissive_provenance,
4246
strict_provenance: config.strict_provenance,
4347
}
4448
}
@@ -47,7 +51,7 @@ impl GlobalStateInner {
4751
impl<'mir, 'tcx> GlobalStateInner {
4852
// Returns the `AllocId` that corresponds to the specified addr,
4953
// or `None` if the addr is out of bounds
50-
fn alloc_id_from_addr(addr: u64, ecx: &MiriEvalContext<'mir, 'tcx>) -> Option<AllocId> {
54+
fn alloc_id_from_addr(ecx: &MiriEvalContext<'mir, 'tcx>, addr: u64) -> Option<AllocId> {
5155
let global_state = ecx.machine.intptrcast.borrow();
5256

5357
if addr == 0 {
@@ -60,7 +64,7 @@ impl<'mir, 'tcx> GlobalStateInner {
6064
Ok(pos) => {
6165
let (_, alloc_id) = global_state.int_to_ptr_map[pos];
6266

63-
if global_state.exposed.contains(&alloc_id) {
67+
if !global_state.permissive_provenance || global_state.exposed.contains(&alloc_id) {
6468
Some(global_state.int_to_ptr_map[pos].1)
6569
} else {
6670
None
@@ -75,7 +79,7 @@ impl<'mir, 'tcx> GlobalStateInner {
7579
let offset = addr - glb;
7680
// If the offset exceeds the size of the allocation, don't use this `alloc_id`.
7781

78-
if global_state.exposed.contains(&alloc_id)
82+
if (!global_state.permissive_provenance || global_state.exposed.contains(&alloc_id))
7983
&& offset
8084
<= ecx
8185
.get_alloc_size_and_align(alloc_id, AllocCheck::MaybeDead)
@@ -91,13 +95,9 @@ impl<'mir, 'tcx> GlobalStateInner {
9195
}
9296
}
9397

94-
pub fn expose_addr(ecx: &MiriEvalContext<'mir, 'tcx>, ptr: Pointer<Tag>) {
98+
pub fn expose_addr(ecx: &MiriEvalContext<'mir, 'tcx>, alloc_id: AllocId) {
9599
let mut global_state = ecx.machine.intptrcast.borrow_mut();
96-
let (tag, _) = ptr.into_parts();
97-
98-
if let machine::AllocType::Concrete(alloc_id) = tag.alloc_id {
99-
global_state.exposed.insert(alloc_id);
100-
}
100+
global_state.exposed.insert(alloc_id);
101101
}
102102

103103
pub fn abs_ptr_to_rel(
@@ -109,7 +109,7 @@ impl<'mir, 'tcx> GlobalStateInner {
109109
let alloc_id = if let machine::AllocType::Concrete(alloc_id) = tag.alloc_id {
110110
alloc_id
111111
} else {
112-
match GlobalStateInner::alloc_id_from_addr(addr.bytes(), ecx) {
112+
match GlobalStateInner::alloc_id_from_addr(ecx, addr.bytes()) {
113113
Some(alloc_id) => alloc_id,
114114
None => return None,
115115
}
@@ -135,11 +135,22 @@ impl<'mir, 'tcx> GlobalStateInner {
135135
return Pointer::new(None, Size::from_bytes(addr));
136136
}
137137

138-
let alloc_id = GlobalStateInner::alloc_id_from_addr(addr, ecx);
138+
let alloc_id = GlobalStateInner::alloc_id_from_addr(ecx, addr);
139139

140140
// Pointers created from integers are untagged.
141+
142+
let sb = if let Some(stacked_borrows) = &ecx.machine.stacked_borrows {
143+
if global_state.permissive_provenance {
144+
stacked_borrows.borrow_mut().wildcard_tag()
145+
} else {
146+
SbTag::Untagged
147+
}
148+
} else {
149+
SbTag::Untagged
150+
};
151+
141152
Pointer::new(
142-
alloc_id.map(|_| Tag { alloc_id: machine::AllocType::Casted, sb: SbTag::Untagged }),
153+
alloc_id.map(|_| Tag { alloc_id: machine::AllocType::Casted, sb }),
143154
Size::from_bytes(addr),
144155
)
145156
}

src/machine.rs

+46-21
Original file line numberDiff line numberDiff line change
@@ -166,9 +166,6 @@ impl Provenance for Tag {
166166
/// Extra per-allocation data
167167
#[derive(Debug, Clone)]
168168
pub struct AllocExtra {
169-
// TODO: this really doesn't need to be here,
170-
// but we're forced to bodge it here for now
171-
pub alloc_id: AllocId,
172169
/// Stacked Borrows state is only added if it is enabled.
173170
pub stacked_borrows: Option<stacked_borrows::AllocExtra>,
174171
/// Data race detection via the use of a vector-clock,
@@ -579,7 +576,7 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for Evaluator<'mir, 'tcx> {
579576
};
580577
let alloc: Allocation<Tag, Self::AllocExtra> = alloc.convert_tag_add_extra(
581578
&ecx.tcx,
582-
AllocExtra { alloc_id: id, stacked_borrows: stacks, data_race: race_alloc },
579+
AllocExtra { stacked_borrows: stacks, data_race: race_alloc },
583580
|ptr| Evaluator::tag_alloc_base_pointer(ecx, ptr),
584581
);
585582
Cow::Owned(alloc)
@@ -611,15 +608,29 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for Evaluator<'mir, 'tcx> {
611608

612609
/// Convert a pointer with provenance into an allocation-offset pair,
613610
/// or a `None` with an absolute address if that conversion is not possible.
614-
fn ptr_get_alloc(
611+
fn ptr_reify_alloc(
615612
ecx: &MiriEvalContext<'mir, 'tcx>,
616613
ptr: Pointer<Self::PointerTag>,
617-
) -> Option<(AllocId, Size)> {
618-
intptrcast::GlobalStateInner::abs_ptr_to_rel(ecx, ptr)
614+
) -> Option<(AllocId, Size, Pointer<Self::PointerTag>)> {
615+
let rel_ptr = intptrcast::GlobalStateInner::abs_ptr_to_rel(ecx, ptr);
616+
rel_ptr.map(|(alloc_id, size)| {
617+
let new_ptr =
618+
ptr.map_provenance(|t| Tag { alloc_id: AllocType::Concrete(alloc_id), ..t });
619+
620+
(alloc_id, size, new_ptr)
621+
})
619622
}
620623

621-
fn expose_addr(ecx: &MiriEvalContext<'mir, 'tcx>, ptr: Pointer<Self::PointerTag>) {
622-
intptrcast::GlobalStateInner::expose_addr(ecx, ptr)
624+
fn expose_ptr(ecx: &InterpCx<'mir, 'tcx, Self>, ptr: Pointer<Self::PointerTag>) {
625+
let (tag, _) = ptr.into_parts();
626+
627+
if let AllocType::Concrete(alloc_id) = tag.alloc_id {
628+
intptrcast::GlobalStateInner::expose_addr(ecx, alloc_id);
629+
630+
if let Some(stacked_borrows) = &ecx.machine.stacked_borrows {
631+
stacked_borrows.borrow_mut().expose_ptr(tag.sb)
632+
}
633+
}
623634
}
624635

625636
#[inline(always)]
@@ -630,12 +641,18 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for Evaluator<'mir, 'tcx> {
630641
tag: Tag,
631642
range: AllocRange,
632643
) -> InterpResult<'tcx> {
644+
let alloc_id = if let AllocType::Concrete(alloc_id) = tag.alloc_id {
645+
alloc_id
646+
} else {
647+
bug!("`memory_read` called with non-concrete tag")
648+
};
649+
633650
if let Some(data_race) = &alloc_extra.data_race {
634-
data_race.read(alloc_extra.alloc_id, range, machine.data_race.as_ref().unwrap())?;
651+
data_race.read(alloc_id, range, machine.data_race.as_ref().unwrap())?;
635652
}
636653
if let Some(stacked_borrows) = &alloc_extra.stacked_borrows {
637654
stacked_borrows.memory_read(
638-
alloc_extra.alloc_id,
655+
alloc_id,
639656
tag.sb,
640657
range,
641658
machine.stacked_borrows.as_ref().unwrap(),
@@ -653,12 +670,18 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for Evaluator<'mir, 'tcx> {
653670
tag: Tag,
654671
range: AllocRange,
655672
) -> InterpResult<'tcx> {
673+
let alloc_id = if let AllocType::Concrete(alloc_id) = tag.alloc_id {
674+
alloc_id
675+
} else {
676+
bug!("`memory_written` called with non-concrete tag")
677+
};
678+
656679
if let Some(data_race) = &mut alloc_extra.data_race {
657-
data_race.write(alloc_extra.alloc_id, range, machine.data_race.as_mut().unwrap())?;
680+
data_race.write(alloc_id, range, machine.data_race.as_mut().unwrap())?;
658681
}
659682
if let Some(stacked_borrows) = &mut alloc_extra.stacked_borrows {
660683
stacked_borrows.memory_written(
661-
alloc_extra.alloc_id,
684+
alloc_id,
662685
tag.sb,
663686
range,
664687
machine.stacked_borrows.as_mut().unwrap(),
@@ -676,19 +699,21 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for Evaluator<'mir, 'tcx> {
676699
tag: Tag,
677700
range: AllocRange,
678701
) -> InterpResult<'tcx> {
679-
if Some(alloc_extra.alloc_id) == machine.tracked_alloc_id {
680-
register_diagnostic(NonHaltingDiagnostic::FreedAlloc(alloc_extra.alloc_id));
702+
let alloc_id = if let AllocType::Concrete(alloc_id) = tag.alloc_id {
703+
alloc_id
704+
} else {
705+
bug!("`memory_deallocated` called with non-concrete tag")
706+
};
707+
708+
if Some(alloc_id) == machine.tracked_alloc_id {
709+
register_diagnostic(NonHaltingDiagnostic::FreedAlloc(alloc_id));
681710
}
682711
if let Some(data_race) = &mut alloc_extra.data_race {
683-
data_race.deallocate(
684-
alloc_extra.alloc_id,
685-
range,
686-
machine.data_race.as_mut().unwrap(),
687-
)?;
712+
data_race.deallocate(alloc_id, range, machine.data_race.as_mut().unwrap())?;
688713
}
689714
if let Some(stacked_borrows) = &mut alloc_extra.stacked_borrows {
690715
stacked_borrows.memory_deallocated(
691-
alloc_extra.alloc_id,
716+
alloc_id,
692717
tag.sb,
693718
range,
694719
machine.stacked_borrows.as_mut().unwrap(),

0 commit comments

Comments
 (0)