TB: integration

This commit is contained in:
Neven Villani 2023-03-16 14:47:44 +01:00
parent 0afab595b4
commit 8bbb0404f8
6 changed files with 54 additions and 16 deletions

View File

@ -32,7 +32,7 @@
}; };
use rustc_session::{config::CrateType, search_paths::PathKind, CtfeBacktrace}; use rustc_session::{config::CrateType, search_paths::PathKind, CtfeBacktrace};
use miri::{BacktraceStyle, ProvenanceMode, RetagFields}; use miri::{BacktraceStyle, BorrowTrackerMethod, ProvenanceMode, RetagFields};
struct MiriCompilerCalls { struct MiriCompilerCalls {
miri_config: miri::MiriConfig, miri_config: miri::MiriConfig,
@ -317,6 +317,8 @@ fn main() {
miri_config.validate = false; miri_config.validate = false;
} else if arg == "-Zmiri-disable-stacked-borrows" { } else if arg == "-Zmiri-disable-stacked-borrows" {
miri_config.borrow_tracker = None; miri_config.borrow_tracker = None;
} else if arg == "-Zmiri-tree-borrows" {
miri_config.borrow_tracker = Some(BorrowTrackerMethod::TreeBorrows);
} else if arg == "-Zmiri-disable-data-race-detector" { } else if arg == "-Zmiri-disable-data-race-detector" {
miri_config.data_race_detector = false; miri_config.data_race_detector = false;
miri_config.weak_memory_emulation = false; miri_config.weak_memory_emulation = false;

View File

@ -22,6 +22,10 @@ pub enum TerminationInfo {
help: Option<String>, help: Option<String>,
history: Option<TagHistory>, history: Option<TagHistory>,
}, },
TreeBorrowsUb {
msg: String,
// FIXME: incomplete
},
Int2PtrWithStrictProvenance, Int2PtrWithStrictProvenance,
Deadlock, Deadlock,
MultipleSymbolDefinitions { MultipleSymbolDefinitions {
@ -61,6 +65,7 @@ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
"integer-to-pointer casts and `ptr::from_exposed_addr` are not supported with `-Zmiri-strict-provenance`" "integer-to-pointer casts and `ptr::from_exposed_addr` are not supported with `-Zmiri-strict-provenance`"
), ),
StackedBorrowsUb { msg, .. } => write!(f, "{msg}"), StackedBorrowsUb { msg, .. } => write!(f, "{msg}"),
TreeBorrowsUb { msg } => write!(f, "{msg}"),
Deadlock => write!(f, "the evaluated program deadlocked"), Deadlock => write!(f, "the evaluated program deadlocked"),
MultipleSymbolDefinitions { link_name, .. } => MultipleSymbolDefinitions { link_name, .. } =>
write!(f, "multiple definitions of symbol `{link_name}`"), write!(f, "multiple definitions of symbol `{link_name}`"),
@ -184,7 +189,8 @@ pub fn report_error<'tcx, 'mir>(
Abort(_) => Some("abnormal termination"), Abort(_) => Some("abnormal termination"),
UnsupportedInIsolation(_) | Int2PtrWithStrictProvenance => UnsupportedInIsolation(_) | Int2PtrWithStrictProvenance =>
Some("unsupported operation"), Some("unsupported operation"),
StackedBorrowsUb { .. } | DataRace { .. } => Some("Undefined Behavior"), StackedBorrowsUb { .. } | TreeBorrowsUb { .. } | DataRace { .. } =>
Some("Undefined Behavior"),
Deadlock => Some("deadlock"), Deadlock => Some("deadlock"),
MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. } => None, MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. } => None,
}; };
@ -212,6 +218,12 @@ pub fn report_error<'tcx, 'mir>(
} }
} }
helps helps
},
TreeBorrowsUb { .. } => {
let helps = vec![
(None, format!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental")),
];
helps
} }
MultipleSymbolDefinitions { first, first_crate, second, second_crate, .. } => MultipleSymbolDefinitions { first, first_crate, second, second_crate, .. } =>
vec![ vec![

View File

@ -87,7 +87,7 @@ pub struct MiriConfig {
pub env: Vec<(OsString, OsString)>, pub env: Vec<(OsString, OsString)>,
/// Determine if validity checking is enabled. /// Determine if validity checking is enabled.
pub validate: bool, pub validate: bool,
/// Determines if Stacked Borrows is enabled. /// Determines if Stacked Borrows or Tree Borrows is enabled.
pub borrow_tracker: Option<BorrowTrackerMethod>, pub borrow_tracker: Option<BorrowTrackerMethod>,
/// Controls alignment checking. /// Controls alignment checking.
pub check_alignment: AlignmentCheck, pub check_alignment: AlignmentCheck,
@ -134,7 +134,7 @@ pub struct MiriConfig {
pub preemption_rate: f64, pub preemption_rate: f64,
/// Report the current instruction being executed every N basic blocks. /// Report the current instruction being executed every N basic blocks.
pub report_progress: Option<u32>, pub report_progress: Option<u32>,
/// Whether Stacked Borrows retagging should recurse into fields of datatypes. /// Whether Stacked Borrows and Tree Borrows retagging should recurse into fields of datatypes.
pub retag_fields: RetagFields, pub retag_fields: RetagFields,
/// The location of a shared object file to load when calling external functions /// The location of a shared object file to load when calling external functions
/// FIXME! consider allowing users to specify paths to multiple SO files, or to a directory /// FIXME! consider allowing users to specify paths to multiple SO files, or to a directory

View File

@ -95,6 +95,7 @@
pub use crate::borrow_tracker::stacked_borrows::{ pub use crate::borrow_tracker::stacked_borrows::{
EvalContextExt as _, Item, Permission, Stack, Stacks, EvalContextExt as _, Item, Permission, Stack, Stacks,
}; };
pub use crate::borrow_tracker::tree_borrows::{EvalContextExt as _, Tree};
pub use crate::borrow_tracker::{ pub use crate::borrow_tracker::{
BorTag, BorrowTrackerMethod, CallId, EvalContextExt as _, RetagFields, BorTag, BorrowTrackerMethod, CallId, EvalContextExt as _, RetagFields,
}; };

View File

@ -38,7 +38,7 @@
/// Extra data stored with each stack frame /// Extra data stored with each stack frame
pub struct FrameExtra<'tcx> { pub struct FrameExtra<'tcx> {
/// Extra data for Stacked Borrows. /// Extra data for the Borrow Tracker.
pub borrow_tracker: Option<borrow_tracker::FrameState>, pub borrow_tracker: Option<borrow_tracker::FrameState>,
/// If this is Some(), then this is a special "catch unwind" frame (the frame of `try_fn` /// If this is Some(), then this is a special "catch unwind" frame (the frame of `try_fn`
@ -146,7 +146,7 @@ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
pub enum Provenance { pub enum Provenance {
Concrete { Concrete {
alloc_id: AllocId, alloc_id: AllocId,
/// Stacked Borrows tag. /// Borrow Tracker tag.
tag: BorTag, tag: BorTag,
}, },
Wildcard, Wildcard,
@ -195,7 +195,7 @@ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
} else { } else {
write!(f, "[{alloc_id:?}]")?; write!(f, "[{alloc_id:?}]")?;
} }
// Print Stacked Borrows tag. // Print Borrow Tracker tag.
write!(f, "{tag:?}")?; write!(f, "{tag:?}")?;
} }
Provenance::Wildcard => { Provenance::Wildcard => {

View File

@ -232,6 +232,19 @@ fn lookup_exported_symbol(
} }
} }
/// Read bytes from a `(ptr, len)` argument
fn read_byte_slice<'i>(&'i self, bytes: &OpTy<'tcx, Provenance>) -> InterpResult<'tcx, &'i [u8]>
where
'mir: 'i,
{
let this = self.eval_context_ref();
let (ptr, len) = this.read_immediate(bytes)?.to_scalar_pair();
let ptr = ptr.to_pointer(this)?;
let len = len.to_target_usize(this)?;
let bytes = this.read_bytes_ptr_strip_provenance(ptr, Size::from_bytes(len))?;
Ok(bytes)
}
/// Emulates calling a foreign item, failing if the item is not supported. /// Emulates calling a foreign item, failing if the item is not supported.
/// This function will handle `goto_block` if needed. /// This function will handle `goto_block` if needed.
/// Returns Ok(None) if the foreign item was completely handled /// Returns Ok(None) if the foreign item was completely handled
@ -427,13 +440,27 @@ fn emulate_foreign_item_by_name(
})?; })?;
this.write_scalar(Scalar::from_u64(alloc_id.0.get()), dest)?; this.write_scalar(Scalar::from_u64(alloc_id.0.get()), dest)?;
} }
"miri_print_borrow_stacks" => { "miri_print_borrow_state" => {
let [id] = this.check_shim(abi, Abi::Rust, link_name, args)?; let [id, show_unnamed] = this.check_shim(abi, Abi::Rust, link_name, args)?;
let id = this.read_scalar(id)?.to_u64()?; let id = this.read_scalar(id)?.to_u64()?;
let show_unnamed = this.read_scalar(show_unnamed)?.to_bool()?;
if let Some(id) = std::num::NonZeroU64::new(id) { if let Some(id) = std::num::NonZeroU64::new(id) {
this.print_stacks(AllocId(id))?; this.print_borrow_state(AllocId(id), show_unnamed)?;
} }
} }
"miri_pointer_name" => {
// This associates a name to a tag. Very useful for debugging, and also makes
// tests more strict.
let [ptr, nth_parent, name] = this.check_shim(abi, Abi::Rust, link_name, args)?;
let ptr = this.read_pointer(ptr)?;
let nth_parent = this.read_scalar(nth_parent)?.to_u8()?;
let name = this.read_byte_slice(name)?;
// We must make `name` owned because we need to
// end the shared borrow from `read_byte_slice` before we can
// start the mutable borrow for `give_pointer_debug_name`.
let name = String::from_utf8_lossy(name).into_owned();
this.give_pointer_debug_name(ptr, nth_parent, &name)?;
}
"miri_static_root" => { "miri_static_root" => {
let [ptr] = this.check_shim(abi, Abi::Rust, link_name, args)?; let [ptr] = this.check_shim(abi, Abi::Rust, link_name, args)?;
let ptr = this.read_pointer(ptr)?; let ptr = this.read_pointer(ptr)?;
@ -487,12 +514,8 @@ fn emulate_foreign_item_by_name(
// Writes some bytes to the interpreter's stdout/stderr. See the // Writes some bytes to the interpreter's stdout/stderr. See the
// README for details. // README for details.
"miri_write_to_stdout" | "miri_write_to_stderr" => { "miri_write_to_stdout" | "miri_write_to_stderr" => {
let [bytes] = this.check_shim(abi, Abi::Rust, link_name, args)?; let [msg] = this.check_shim(abi, Abi::Rust, link_name, args)?;
let (ptr, len) = this.read_immediate(bytes)?.to_scalar_pair(); let msg = this.read_byte_slice(msg)?;
let ptr = ptr.to_pointer(this)?;
let len = len.to_target_usize(this)?;
let msg = this.read_bytes_ptr_strip_provenance(ptr, Size::from_bytes(len))?;
// Note: we're ignoring errors writing to host stdout/stderr. // Note: we're ignoring errors writing to host stdout/stderr.
let _ignore = match link_name.as_str() { let _ignore = match link_name.as_str() {
"miri_write_to_stdout" => std::io::stdout().write_all(msg), "miri_write_to_stdout" => std::io::stdout().write_all(msg),