mirror of
https://github.com/rust-lang/rust.git
synced 2026-04-27 18:57:42 +03:00
Auto merge of #155567 - JonathanBrouwer:rollup-0zpjwMk, r=JonathanBrouwer
Rollup of 7 pull requests Successful merges: - rust-lang/rust#155556 (`rust-analyzer` subtree update) - rust-lang/rust#152162 (Suggest returning a reference for unsized place from a closure) - rust-lang/rust#155389 (Simplify macros for target-modifier and mitigation flags) - rust-lang/rust#155553 (miri subtree update) - rust-lang/rust#153546 (tests/ui/extern: add annotations for reference rules) - rust-lang/rust#155475 (Make reparsed guard metavars collect tokens) - rust-lang/rust#155560 (Remove `AttributeLintKind` variants - part 4)
This commit is contained in:
@@ -15,7 +15,8 @@
|
||||
use crate::context::{AcceptContext, FinalizeContext, Stage};
|
||||
use crate::errors::{
|
||||
DocAliasDuplicated, DocAutoCfgExpectsHideOrShow, DocAutoCfgHideShowExpectsList,
|
||||
DocAutoCfgHideShowUnexpectedItem, DocUnknownInclude, IllFormedAttributeInput,
|
||||
DocAutoCfgHideShowUnexpectedItem, DocAutoCfgWrongLiteral, DocUnknownAny, DocUnknownInclude,
|
||||
DocUnknownPasses, DocUnknownPlugins, DocUnknownSpotlight, IllFormedAttributeInput,
|
||||
};
|
||||
use crate::parser::{ArgParser, MetaItemOrLitParser, MetaItemParser, OwnedPathParser};
|
||||
use crate::session_diagnostics::{
|
||||
@@ -442,9 +443,9 @@ fn parse_auto_cfg<S: Stage>(
|
||||
ArgParser::NameValue(nv) => {
|
||||
let MetaItemLit { kind: LitKind::Bool(bool_value), span, .. } = nv.value_as_lit()
|
||||
else {
|
||||
cx.emit_lint(
|
||||
cx.emit_dyn_lint(
|
||||
rustc_session::lint::builtin::INVALID_DOC_ATTRIBUTES,
|
||||
AttributeLintKind::DocAutoCfgWrongLiteral,
|
||||
move |dcx, level| DocAutoCfgWrongLiteral.into_diag(dcx, level),
|
||||
nv.value_span,
|
||||
);
|
||||
return;
|
||||
@@ -613,10 +614,11 @@ macro_rules! string_arg_and_crate_level {
|
||||
}
|
||||
}
|
||||
Some(sym::spotlight) => {
|
||||
cx.emit_lint(
|
||||
let span = path.span();
|
||||
cx.emit_dyn_lint(
|
||||
rustc_session::lint::builtin::INVALID_DOC_ATTRIBUTES,
|
||||
AttributeLintKind::DocUnknownSpotlight { span: path.span() },
|
||||
path.span(),
|
||||
move |dcx, level| DocUnknownSpotlight { sugg_span: span }.into_diag(dcx, level),
|
||||
span,
|
||||
);
|
||||
}
|
||||
Some(sym::include) if let Some(nv) = args.name_value() => {
|
||||
@@ -640,32 +642,37 @@ macro_rules! string_arg_and_crate_level {
|
||||
);
|
||||
}
|
||||
Some(name @ (sym::passes | sym::no_default_passes)) => {
|
||||
cx.emit_lint(
|
||||
let span = path.span();
|
||||
cx.emit_dyn_lint(
|
||||
rustc_session::lint::builtin::INVALID_DOC_ATTRIBUTES,
|
||||
AttributeLintKind::DocUnknownPasses { name, span: path.span() },
|
||||
path.span(),
|
||||
move |dcx, level| {
|
||||
DocUnknownPasses { name, note_span: span }.into_diag(dcx, level)
|
||||
},
|
||||
span,
|
||||
);
|
||||
}
|
||||
Some(sym::plugins) => {
|
||||
cx.emit_lint(
|
||||
let span = path.span();
|
||||
cx.emit_dyn_lint(
|
||||
rustc_session::lint::builtin::INVALID_DOC_ATTRIBUTES,
|
||||
AttributeLintKind::DocUnknownPlugins { span: path.span() },
|
||||
path.span(),
|
||||
move |dcx, level| DocUnknownPlugins { label_span: span }.into_diag(dcx, level),
|
||||
span,
|
||||
);
|
||||
}
|
||||
Some(name) => {
|
||||
cx.emit_lint(
|
||||
cx.emit_dyn_lint(
|
||||
rustc_session::lint::builtin::INVALID_DOC_ATTRIBUTES,
|
||||
AttributeLintKind::DocUnknownAny { name },
|
||||
move |dcx, level| DocUnknownAny { name }.into_diag(dcx, level),
|
||||
path.span(),
|
||||
);
|
||||
}
|
||||
None => {
|
||||
let full_name =
|
||||
path.segments().map(|s| s.as_str()).intersperse("::").collect::<String>();
|
||||
cx.emit_lint(
|
||||
let name = Symbol::intern(&full_name);
|
||||
cx.emit_dyn_lint(
|
||||
rustc_session::lint::builtin::INVALID_DOC_ATTRIBUTES,
|
||||
AttributeLintKind::DocUnknownAny { name: Symbol::intern(&full_name) },
|
||||
move |dcx, level| DocUnknownAny { name }.into_diag(dcx, level),
|
||||
path.span(),
|
||||
);
|
||||
}
|
||||
|
||||
@@ -205,3 +205,50 @@ pub(crate) struct DocUnknownInclude {
|
||||
)]
|
||||
pub sugg: (Span, Applicability),
|
||||
}
|
||||
|
||||
#[derive(Diagnostic)]
|
||||
#[diag("unknown `doc` attribute `spotlight`")]
|
||||
#[note("`doc(spotlight)` was renamed to `doc(notable_trait)`")]
|
||||
#[note("`doc(spotlight)` is now a no-op")]
|
||||
pub(crate) struct DocUnknownSpotlight {
|
||||
#[suggestion(
|
||||
"use `notable_trait` instead",
|
||||
style = "short",
|
||||
applicability = "machine-applicable",
|
||||
code = "notable_trait"
|
||||
)]
|
||||
pub sugg_span: Span,
|
||||
}
|
||||
|
||||
#[derive(Diagnostic)]
|
||||
#[diag("unknown `doc` attribute `{$name}`")]
|
||||
#[note(
|
||||
"`doc` attribute `{$name}` no longer functions; see issue #44136 <https://github.com/rust-lang/rust/issues/44136>"
|
||||
)]
|
||||
#[note("`doc({$name})` is now a no-op")]
|
||||
pub(crate) struct DocUnknownPasses {
|
||||
pub name: Symbol,
|
||||
#[label("no longer functions")]
|
||||
pub note_span: Span,
|
||||
}
|
||||
|
||||
#[derive(Diagnostic)]
|
||||
#[diag("unknown `doc` attribute `plugins`")]
|
||||
#[note(
|
||||
"`doc` attribute `plugins` no longer functions; see issue #44136 <https://github.com/rust-lang/rust/issues/44136> and CVE-2018-1000622 <https://nvd.nist.gov/vuln/detail/CVE-2018-1000622>"
|
||||
)]
|
||||
#[note("`doc(plugins)` is now a no-op")]
|
||||
pub(crate) struct DocUnknownPlugins {
|
||||
#[label("no longer functions")]
|
||||
pub label_span: Span,
|
||||
}
|
||||
|
||||
#[derive(Diagnostic)]
|
||||
#[diag("unknown `doc` attribute `{$name}`")]
|
||||
pub(crate) struct DocUnknownAny {
|
||||
pub name: Symbol,
|
||||
}
|
||||
|
||||
#[derive(Diagnostic)]
|
||||
#[diag("expected boolean for `#[doc(auto_cfg = ...)]`")]
|
||||
pub(crate) struct DocAutoCfgWrongLiteral;
|
||||
|
||||
@@ -43,26 +43,6 @@ fn into_diag(self, dcx: DiagCtxtHandle<'a>, level: Level) -> Diag<'a, ()> {
|
||||
.into_diag(dcx, level)
|
||||
}
|
||||
|
||||
&AttributeLintKind::DocUnknownSpotlight { span } => {
|
||||
lints::DocUnknownSpotlight { sugg_span: span }.into_diag(dcx, level)
|
||||
}
|
||||
|
||||
&AttributeLintKind::DocUnknownPasses { name, span } => {
|
||||
lints::DocUnknownPasses { name, note_span: span }.into_diag(dcx, level)
|
||||
}
|
||||
|
||||
&AttributeLintKind::DocUnknownPlugins { span } => {
|
||||
lints::DocUnknownPlugins { label_span: span }.into_diag(dcx, level)
|
||||
}
|
||||
|
||||
&AttributeLintKind::DocUnknownAny { name } => {
|
||||
lints::DocUnknownAny { name }.into_diag(dcx, level)
|
||||
}
|
||||
|
||||
&AttributeLintKind::DocAutoCfgWrongLiteral => {
|
||||
lints::DocAutoCfgWrongLiteral.into_diag(dcx, level)
|
||||
}
|
||||
|
||||
&AttributeLintKind::DocTestTakesList => lints::DocTestTakesList.into_diag(dcx, level),
|
||||
|
||||
&AttributeLintKind::DocTestUnknown { name } => {
|
||||
|
||||
@@ -3303,53 +3303,6 @@ fn add_to_diag<G: EmissionGuarantee>(self, diag: &mut Diag<'_, G>) {
|
||||
)]
|
||||
pub(crate) struct ExpectedNameValue;
|
||||
|
||||
#[derive(Diagnostic)]
|
||||
#[diag("unknown `doc` attribute `spotlight`")]
|
||||
#[note("`doc(spotlight)` was renamed to `doc(notable_trait)`")]
|
||||
#[note("`doc(spotlight)` is now a no-op")]
|
||||
pub(crate) struct DocUnknownSpotlight {
|
||||
#[suggestion(
|
||||
"use `notable_trait` instead",
|
||||
style = "short",
|
||||
applicability = "machine-applicable",
|
||||
code = "notable_trait"
|
||||
)]
|
||||
pub sugg_span: Span,
|
||||
}
|
||||
|
||||
#[derive(Diagnostic)]
|
||||
#[diag("unknown `doc` attribute `{$name}`")]
|
||||
#[note(
|
||||
"`doc` attribute `{$name}` no longer functions; see issue #44136 <https://github.com/rust-lang/rust/issues/44136>"
|
||||
)]
|
||||
#[note("`doc({$name})` is now a no-op")]
|
||||
pub(crate) struct DocUnknownPasses {
|
||||
pub name: Symbol,
|
||||
#[label("no longer functions")]
|
||||
pub note_span: Span,
|
||||
}
|
||||
|
||||
#[derive(Diagnostic)]
|
||||
#[diag("unknown `doc` attribute `plugins`")]
|
||||
#[note(
|
||||
"`doc` attribute `plugins` no longer functions; see issue #44136 <https://github.com/rust-lang/rust/issues/44136> and CVE-2018-1000622 <https://nvd.nist.gov/vuln/detail/CVE-2018-1000622>"
|
||||
)]
|
||||
#[note("`doc(plugins)` is now a no-op")]
|
||||
pub(crate) struct DocUnknownPlugins {
|
||||
#[label("no longer functions")]
|
||||
pub label_span: Span,
|
||||
}
|
||||
|
||||
#[derive(Diagnostic)]
|
||||
#[diag("unknown `doc` attribute `{$name}`")]
|
||||
pub(crate) struct DocUnknownAny {
|
||||
pub name: Symbol,
|
||||
}
|
||||
|
||||
#[derive(Diagnostic)]
|
||||
#[diag("expected boolean for `#[doc(auto_cfg = ...)]`")]
|
||||
pub(crate) struct DocAutoCfgWrongLiteral;
|
||||
|
||||
#[derive(Diagnostic)]
|
||||
#[diag("`#[doc(test(...)]` takes a list of attributes")]
|
||||
pub(crate) struct DocTestTakesList;
|
||||
|
||||
@@ -656,11 +656,6 @@ pub enum DeprecatedSinceKind {
|
||||
pub enum AttributeLintKind {
|
||||
UnexpectedCfgName((Symbol, Span), Option<(Symbol, Span)>),
|
||||
UnexpectedCfgValue((Symbol, Span), Option<(Symbol, Span)>),
|
||||
DocUnknownSpotlight { span: Span },
|
||||
DocUnknownPasses { name: Symbol, span: Span },
|
||||
DocUnknownPlugins { span: Span },
|
||||
DocUnknownAny { name: Symbol },
|
||||
DocAutoCfgWrongLiteral,
|
||||
DocTestTakesList,
|
||||
DocTestUnknown { name: Symbol },
|
||||
DocTestLiteral,
|
||||
|
||||
@@ -3464,7 +3464,9 @@ pub(super) fn parse_arm(&mut self) -> PResult<'a, Arm> {
|
||||
}
|
||||
|
||||
pub(crate) fn eat_metavar_guard(&mut self) -> Option<Box<Guard>> {
|
||||
self.eat_metavar_seq(MetaVarKind::Guard, |this| this.parse_match_arm_guard()).flatten()
|
||||
self.eat_metavar_seq(MetaVarKind::Guard, |this| {
|
||||
this.expect_match_arm_guard(ForceCollect::Yes)
|
||||
})
|
||||
}
|
||||
|
||||
fn parse_match_arm_guard(&mut self) -> PResult<'a, Option<Box<Guard>>> {
|
||||
|
||||
@@ -2641,7 +2641,7 @@ pub fn build_session_options(early_dcx: &mut EarlyDiagCtxt, matches: &getopts::M
|
||||
if unstable_opts.retpoline_external_thunk {
|
||||
unstable_opts.retpoline = true;
|
||||
collected_options.target_modifiers.insert(
|
||||
OptionsTargetModifiers::UnstableOptions(UnstableOptionsTargetModifiers::retpoline),
|
||||
OptionsTargetModifiers::UnstableOptions(UnstableOptionsTargetModifiers::Retpoline),
|
||||
"true".to_string(),
|
||||
);
|
||||
}
|
||||
|
||||
@@ -5,6 +5,7 @@
|
||||
#![feature(default_field_values)]
|
||||
#![feature(iter_intersperse)]
|
||||
#![feature(macro_derive)]
|
||||
#![feature(macro_metavar_expr)]
|
||||
#![feature(rustc_attrs)]
|
||||
// To generate CodegenOptionsTargetModifiers and UnstableOptionsTargetModifiers enums
|
||||
// with macro_rules, it is necessary to use recursive mechanic ("Incremental TT Munchers").
|
||||
|
||||
@@ -141,10 +141,10 @@ pub fn consistent(&self, sess: &Session, other: Option<&TargetModifier>) -> bool
|
||||
assert!(other.is_none() || self.opt == other.unwrap().opt);
|
||||
match self.opt {
|
||||
OptionsTargetModifiers::UnstableOptions(unstable) => match unstable {
|
||||
UnstableOptionsTargetModifiers::sanitizer => {
|
||||
UnstableOptionsTargetModifiers::Sanitizer => {
|
||||
return target_modifier_consistency_check::sanitizer(self, other);
|
||||
}
|
||||
UnstableOptionsTargetModifiers::sanitizer_cfi_normalize_integers => {
|
||||
UnstableOptionsTargetModifiers::SanitizerCfiNormalizeIntegers => {
|
||||
return target_modifier_consistency_check::sanitizer_cfi_normalize_integers(
|
||||
sess, self, other,
|
||||
);
|
||||
@@ -170,164 +170,52 @@ fn tmod_push_impl(
|
||||
}
|
||||
}
|
||||
|
||||
macro_rules! tmod_push {
|
||||
($struct_name:ident, $tmod_enum_name:ident, $opt_name:ident, $opt_expr:expr, $init:expr, $mods:expr, $tmod_vals:expr) => {
|
||||
if *$opt_expr != $init {
|
||||
tmod_push_impl(
|
||||
OptionsTargetModifiers::$struct_name($tmod_enum_name::$opt_name),
|
||||
$tmod_vals,
|
||||
$mods,
|
||||
);
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
macro_rules! gather_tmods {
|
||||
($struct_name:ident, $tmod_enum_name:ident, $opt_name:ident, $opt_expr:expr, $init:expr, $mods:expr, $tmod_vals:expr,
|
||||
[SUBSTRUCT], [TARGET_MODIFIER]) => {
|
||||
compile_error!("SUBSTRUCT can't be target modifier");
|
||||
};
|
||||
($struct_name:ident, $tmod_enum_name:ident, $opt_name:ident, $opt_expr:expr, $init:expr, $mods:expr, $tmod_vals:expr,
|
||||
[UNTRACKED], [TARGET_MODIFIER]) => {
|
||||
tmod_push!($struct_name, $tmod_enum_name, $opt_name, $opt_expr, $init, $mods, $tmod_vals)
|
||||
};
|
||||
($struct_name:ident, $tmod_enum_name:ident, $opt_name:ident, $opt_expr:expr, $init:expr, $mods:expr, $tmod_vals:expr,
|
||||
[TRACKED], [TARGET_MODIFIER]) => {
|
||||
tmod_push!($struct_name, $tmod_enum_name, $opt_name, $opt_expr, $init, $mods, $tmod_vals)
|
||||
};
|
||||
($struct_name:ident, $tmod_enum_name:ident, $opt_name:ident, $opt_expr:expr, $init:expr, $mods:expr, $tmod_vals:expr,
|
||||
[TRACKED_NO_CRATE_HASH], [TARGET_MODIFIER]) => {
|
||||
tmod_push!($struct_name, $tmod_enum_name, $opt_name, $opt_expr, $init, $mods, $tmod_vals)
|
||||
};
|
||||
($struct_name:ident, $tmod_enum_name:ident, $opt_name:ident, $opt_expr:expr, $init:expr, $mods:expr, $tmod_vals:expr,
|
||||
[SUBSTRUCT], [$(MITIGATION)?]) => {
|
||||
$opt_expr.gather_target_modifiers($mods, $tmod_vals);
|
||||
};
|
||||
($struct_name:ident, $tmod_enum_name:ident, $opt_name:ident, $opt_expr:expr, $init:expr, $mods:expr, $tmod_vals:expr,
|
||||
[UNTRACKED], [$(MITIGATION)?]) => {{}};
|
||||
($struct_name:ident, $tmod_enum_name:ident, $opt_name:ident, $opt_expr:expr, $init:expr, $mods:expr, $tmod_vals:expr,
|
||||
[TRACKED], [$(MITIGATION)?]) => {{}};
|
||||
($struct_name:ident, $tmod_enum_name:ident, $opt_name:ident, $opt_expr:expr, $init:expr, $mods:expr, $tmod_vals:expr,
|
||||
[TRACKED_NO_CRATE_HASH], [$(MITIGATION)?]) => {{}};
|
||||
}
|
||||
|
||||
macro_rules! gather_tmods_top_level {
|
||||
($_opt_name:ident, $opt_expr:expr, $mods:expr, $tmod_vals:expr, [SUBSTRUCT $substruct_enum:ident]) => {
|
||||
$opt_expr.gather_target_modifiers($mods, $tmod_vals);
|
||||
};
|
||||
($opt_name:ident, $opt_expr:expr, $mods:expr, $tmod_vals:expr, [$non_substruct:ident TARGET_MODIFIER]) => {
|
||||
compile_error!("Top level option can't be target modifier");
|
||||
};
|
||||
($opt_name:ident, $opt_expr:expr, $mods:expr, $tmod_vals:expr, [$non_substruct:ident $(MITIGATION)?]) => {};
|
||||
}
|
||||
|
||||
/// Macro for generating OptionsTargetsModifiers top-level enum with impl.
|
||||
/// Will generate something like:
|
||||
/// ```rust,ignore (illustrative)
|
||||
/// pub enum OptionsTargetModifiers {
|
||||
/// CodegenOptions(CodegenOptionsTargetModifiers),
|
||||
/// UnstableOptions(UnstableOptionsTargetModifiers),
|
||||
/// }
|
||||
/// impl OptionsTargetModifiers {
|
||||
/// pub fn reparse(&self, user_value: &str) -> ExtendedTargetModifierInfo {
|
||||
/// match self {
|
||||
/// Self::CodegenOptions(v) => v.reparse(user_value),
|
||||
/// Self::UnstableOptions(v) => v.reparse(user_value),
|
||||
/// }
|
||||
/// }
|
||||
/// pub fn is_target_modifier(flag_name: &str) -> bool {
|
||||
/// CodegenOptionsTargetModifiers::is_target_modifier(flag_name) ||
|
||||
/// UnstableOptionsTargetModifiers::is_target_modifier(flag_name)
|
||||
/// }
|
||||
/// }
|
||||
/// ```
|
||||
macro_rules! top_level_tmod_enum {
|
||||
($( {$($optinfo:tt)*} ),* $(,)*) => {
|
||||
top_level_tmod_enum! { @parse {}, (user_value){}; $($($optinfo)*|)* }
|
||||
};
|
||||
// Termination
|
||||
(
|
||||
@parse
|
||||
{$($variant:tt($substruct_enum:tt))*},
|
||||
($user_value:ident){$($pout:tt)*};
|
||||
) => {
|
||||
#[allow(non_camel_case_types)]
|
||||
#[derive(PartialEq, Eq, PartialOrd, Ord, Debug, Copy, Clone, Encodable, BlobDecodable)]
|
||||
pub enum OptionsTargetModifiers {
|
||||
$($variant($substruct_enum)),*
|
||||
}
|
||||
impl OptionsTargetModifiers {
|
||||
#[allow(unused_variables)]
|
||||
pub fn reparse(&self, $user_value: &str) -> ExtendedTargetModifierInfo {
|
||||
#[allow(unreachable_patterns)]
|
||||
match self {
|
||||
$($pout)*
|
||||
_ => panic!("unknown target modifier option: {:?}", *self)
|
||||
}
|
||||
}
|
||||
pub fn is_target_modifier(flag_name: &str) -> bool {
|
||||
$($substruct_enum::is_target_modifier(flag_name))||*
|
||||
}
|
||||
}
|
||||
};
|
||||
// Adding SUBSTRUCT option group into $eout
|
||||
(
|
||||
@parse {$($eout:tt)*}, ($puser_value:ident){$($pout:tt)*};
|
||||
[SUBSTRUCT $substruct_enum:ident $variant:ident] |
|
||||
$($tail:tt)*
|
||||
) => {
|
||||
top_level_tmod_enum! {
|
||||
@parse
|
||||
{
|
||||
$($eout)*
|
||||
$variant($substruct_enum)
|
||||
},
|
||||
($puser_value){
|
||||
$($pout)*
|
||||
Self::$variant(v) => v.reparse($puser_value),
|
||||
};
|
||||
$($tail)*
|
||||
}
|
||||
};
|
||||
// Skipping non-target-modifier and non-substruct
|
||||
(
|
||||
@parse {$($eout:tt)*}, ($puser_value:ident){$($pout:tt)*};
|
||||
[$non_substruct:ident] |
|
||||
$($tail:tt)*
|
||||
) => {
|
||||
top_level_tmod_enum! {
|
||||
@parse
|
||||
{
|
||||
$($eout)*
|
||||
},
|
||||
($puser_value){
|
||||
$($pout)*
|
||||
};
|
||||
$($tail)*
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
macro_rules! top_level_options {
|
||||
(
|
||||
$(#[$top_level_attr:meta])*
|
||||
pub struct Options {
|
||||
$(
|
||||
$(#[$attr:meta])*
|
||||
$opt:ident : $t:ty [
|
||||
$dep_tracking_marker:ident
|
||||
$( $tmod:ident $variant:ident )?
|
||||
],
|
||||
$opt:ident : $t:ty
|
||||
[$dep_tracking_marker:ident]
|
||||
$( { TARGET_MODIFIER: $tmod_variant:ident($tmod_enum:ident) } )?
|
||||
,
|
||||
)*
|
||||
}
|
||||
) => {
|
||||
top_level_tmod_enum!(
|
||||
{
|
||||
#[derive(PartialEq, Eq, PartialOrd, Ord, Debug, Copy, Clone, Encodable, BlobDecodable)]
|
||||
pub enum OptionsTargetModifiers {
|
||||
$(
|
||||
$(
|
||||
[$dep_tracking_marker $($tmod $variant),*]
|
||||
)|*
|
||||
$tmod_variant($tmod_enum),
|
||||
)?
|
||||
)*
|
||||
}
|
||||
|
||||
impl OptionsTargetModifiers {
|
||||
pub fn reparse(&self, user_value: &str) -> ExtendedTargetModifierInfo {
|
||||
match self {
|
||||
$(
|
||||
$(
|
||||
Self::$tmod_variant(v) => v.reparse(user_value),
|
||||
)?
|
||||
)*
|
||||
#[allow(unreachable_patterns)]
|
||||
_ => panic!("unknown target modifier option: {self:?}"),
|
||||
}
|
||||
}
|
||||
);
|
||||
|
||||
pub fn is_target_modifier(flag_name: &str) -> bool {
|
||||
$(
|
||||
$(
|
||||
if $tmod_enum::is_target_modifier(flag_name) {
|
||||
return true
|
||||
}
|
||||
)?
|
||||
)*
|
||||
false
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone)]
|
||||
$(#[$top_level_attr])*
|
||||
@@ -375,13 +263,11 @@ pub fn dep_tracking_hash(&self, for_crate_hash: bool) -> Hash64 {
|
||||
pub fn gather_target_modifiers(&self) -> Vec<TargetModifier> {
|
||||
let mut mods = Vec::<TargetModifier>::new();
|
||||
$(
|
||||
gather_tmods_top_level!(
|
||||
$opt,
|
||||
&self.$opt,
|
||||
&mut mods,
|
||||
&self.target_modifiers,
|
||||
[$dep_tracking_marker $($tmod),*]
|
||||
);
|
||||
$(
|
||||
// Only expand for flags that have `TARGET_MODIFIER`.
|
||||
${ignore($tmod_enum)}
|
||||
self.$opt.gather_target_modifiers(&mut mods, &self.target_modifiers);
|
||||
)?
|
||||
)*
|
||||
mods.sort_by(|a, b| a.opt.cmp(&b.opt));
|
||||
mods
|
||||
@@ -451,9 +337,9 @@ pub struct Options {
|
||||
#[rustc_lint_opt_deny_field_access("should only be used via `Config::track_state`")]
|
||||
untracked_state_hash: Hash64 [TRACKED_NO_CRATE_HASH],
|
||||
|
||||
unstable_opts: UnstableOptions [SUBSTRUCT UnstableOptionsTargetModifiers UnstableOptions],
|
||||
unstable_opts: UnstableOptions [SUBSTRUCT] { TARGET_MODIFIER: UnstableOptions(UnstableOptionsTargetModifiers) },
|
||||
prints: Vec<PrintRequest> [UNTRACKED],
|
||||
cg: CodegenOptions [SUBSTRUCT CodegenOptionsTargetModifiers CodegenOptions],
|
||||
cg: CodegenOptions [SUBSTRUCT] { TARGET_MODIFIER: CodegenOptions(CodegenOptionsTargetModifiers) },
|
||||
externs: Externs [UNTRACKED],
|
||||
crate_name: Option<String> [TRACKED],
|
||||
/// Indicates how the compiler should treat unstable features.
|
||||
@@ -530,108 +416,6 @@ pub struct Options {
|
||||
}
|
||||
);
|
||||
|
||||
macro_rules! mitigation_enum_opt {
|
||||
($opt:ident, MITIGATION) => {
|
||||
Some(mitigation_coverage::DeniedPartialMitigationKind::$opt)
|
||||
};
|
||||
($opt:ident, $(TARGET_MODIFIER)?) => {
|
||||
None
|
||||
};
|
||||
}
|
||||
|
||||
macro_rules! tmod_enum_opt {
|
||||
($struct_name:ident, $tmod_enum_name:ident, $opt:ident, TARGET_MODIFIER) => {
|
||||
Some(OptionsTargetModifiers::$struct_name($tmod_enum_name::$opt))
|
||||
};
|
||||
($struct_name:ident, $tmod_enum_name:ident, $opt:ident, $(MITIGATION)?) => {
|
||||
None
|
||||
};
|
||||
}
|
||||
|
||||
macro_rules! tmod_enum {
|
||||
($tmod_enum_name:ident, $prefix:expr, $( {$($optinfo:tt)*} ),* $(,)*) => {
|
||||
tmod_enum! { $tmod_enum_name, $prefix, @parse {}, (user_value){}; $($($optinfo)*|)* }
|
||||
};
|
||||
// Termination
|
||||
(
|
||||
$tmod_enum_name:ident, $prefix:expr,
|
||||
@parse
|
||||
{$($eout:tt)*},
|
||||
($user_value:ident){$($pout:tt)*};
|
||||
) => {
|
||||
#[allow(non_camel_case_types)]
|
||||
#[derive(PartialEq, Eq, PartialOrd, Ord, Debug, Copy, Clone, Encodable, BlobDecodable)]
|
||||
pub enum $tmod_enum_name {
|
||||
$($eout),*
|
||||
}
|
||||
impl $tmod_enum_name {
|
||||
#[allow(unused_variables)]
|
||||
pub fn reparse(&self, $user_value: &str) -> ExtendedTargetModifierInfo {
|
||||
#[allow(unreachable_patterns)]
|
||||
match self {
|
||||
$($pout)*
|
||||
_ => panic!("unknown target modifier option: {:?}", *self)
|
||||
}
|
||||
}
|
||||
pub fn is_target_modifier(flag_name: &str) -> bool {
|
||||
match flag_name.replace('-', "_").as_str() {
|
||||
$(stringify!($eout) => true,)*
|
||||
_ => false,
|
||||
}
|
||||
}
|
||||
}
|
||||
};
|
||||
// Adding target-modifier option into $eout
|
||||
(
|
||||
$tmod_enum_name:ident, $prefix:expr,
|
||||
@parse {$($eout:tt)*}, ($puser_value:ident){$($pout:tt)*};
|
||||
$opt:ident, $parse:ident, $t:ty, [TARGET_MODIFIER] |
|
||||
$($tail:tt)*
|
||||
) => {
|
||||
tmod_enum! {
|
||||
$tmod_enum_name, $prefix,
|
||||
@parse
|
||||
{
|
||||
$($eout)*
|
||||
$opt
|
||||
},
|
||||
($puser_value){
|
||||
$($pout)*
|
||||
Self::$opt => {
|
||||
let mut parsed : $t = Default::default();
|
||||
let val = if $puser_value.is_empty() { None } else { Some($puser_value) };
|
||||
parse::$parse(&mut parsed, val);
|
||||
ExtendedTargetModifierInfo {
|
||||
prefix: $prefix.to_string(),
|
||||
name: stringify!($opt).to_string().replace('_', "-"),
|
||||
tech_value: format!("{:?}", parsed),
|
||||
}
|
||||
},
|
||||
};
|
||||
$($tail)*
|
||||
}
|
||||
};
|
||||
// Skipping non-target-modifier
|
||||
(
|
||||
$tmod_enum_name:ident, $prefix:expr,
|
||||
@parse {$($eout:tt)*}, ($puser_value:ident){$($pout:tt)*};
|
||||
$opt:ident, $parse:ident, $t:ty, [$(MITIGATION)?] |
|
||||
$($tail:tt)*
|
||||
) => {
|
||||
tmod_enum! {
|
||||
$tmod_enum_name, $prefix,
|
||||
@parse
|
||||
{
|
||||
$($eout)*
|
||||
},
|
||||
($puser_value){
|
||||
$($pout)*
|
||||
};
|
||||
$($tail)*
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
#[derive(Default)]
|
||||
pub struct CollectedOptions {
|
||||
pub target_modifiers: BTreeMap<OptionsTargetModifiers, String>,
|
||||
@@ -684,7 +468,7 @@ pub(super) fn $opt(
|
||||
macro_rules! options {
|
||||
(
|
||||
$struct_name:ident,
|
||||
$tmod_enum_name:ident,
|
||||
$tmod_enum:ident,
|
||||
$stat:ident,
|
||||
$optmod:ident,
|
||||
$prefix:expr,
|
||||
@@ -695,8 +479,11 @@ macro_rules! options {
|
||||
$opt:ident : $t:ty = (
|
||||
$init:expr,
|
||||
$parse:ident,
|
||||
[$dep_tracking_marker:ident $( $modifier_kind:ident )?],
|
||||
$desc:expr
|
||||
[$dep_tracking_marker:ident]
|
||||
$( { TARGET_MODIFIER: $tmod_variant:ident } )?
|
||||
$( { MITIGATION: $mitigation_variant:ident } )?
|
||||
,
|
||||
$desc:literal
|
||||
$(, removed: $removed:ident )?
|
||||
),
|
||||
)*
|
||||
@@ -710,15 +497,49 @@ pub struct $struct_name {
|
||||
)*
|
||||
}
|
||||
|
||||
tmod_enum!(
|
||||
$tmod_enum_name,
|
||||
$prefix,
|
||||
{
|
||||
$(
|
||||
$opt, $parse, $t, [$($modifier_kind),*]
|
||||
)|*
|
||||
#[derive(PartialEq, Eq, PartialOrd, Ord, Debug, Copy, Clone, Encodable, BlobDecodable)]
|
||||
pub enum $tmod_enum {
|
||||
$(
|
||||
$( $tmod_variant, )?
|
||||
)*
|
||||
}
|
||||
|
||||
impl $tmod_enum {
|
||||
pub fn reparse(&self, _user_value: &str) -> ExtendedTargetModifierInfo {
|
||||
match self {
|
||||
$(
|
||||
$(
|
||||
Self::$tmod_variant => {
|
||||
let mut parsed: $t = Default::default();
|
||||
let val = if _user_value.is_empty() { None } else { Some(_user_value) };
|
||||
parse::$parse(&mut parsed, val);
|
||||
ExtendedTargetModifierInfo {
|
||||
prefix: $prefix.to_string(),
|
||||
name: stringify!($opt).to_string().replace('_', "-"),
|
||||
tech_value: format!("{:?}", parsed),
|
||||
}
|
||||
}
|
||||
)?
|
||||
)*
|
||||
|
||||
#[allow(unreachable_patterns)]
|
||||
_ => panic!("unknown target modifier option: {:?}", *self)
|
||||
}
|
||||
}
|
||||
);
|
||||
|
||||
pub fn is_target_modifier(flag_name: &str) -> bool {
|
||||
match flag_name.replace('-', "_").as_str() {
|
||||
$(
|
||||
$(
|
||||
// Only expand for flags that have `TARGET_MODIFIER`.
|
||||
${ignore($tmod_variant)}
|
||||
stringify!($opt) => true,
|
||||
)?
|
||||
)*
|
||||
_ => false,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Default for $struct_name {
|
||||
fn default() -> $struct_name {
|
||||
@@ -770,17 +591,15 @@ pub fn gather_target_modifiers(
|
||||
_tmod_vals: &BTreeMap<OptionsTargetModifiers, String>,
|
||||
) {
|
||||
$(
|
||||
gather_tmods!(
|
||||
$struct_name,
|
||||
$tmod_enum_name,
|
||||
$opt,
|
||||
&self.$opt,
|
||||
$init,
|
||||
_mods,
|
||||
_tmod_vals,
|
||||
[$dep_tracking_marker],
|
||||
[$($modifier_kind),*]
|
||||
);
|
||||
$(
|
||||
if self.$opt != $init {
|
||||
tmod_push_impl(
|
||||
OptionsTargetModifiers::$struct_name($tmod_enum::$tmod_variant),
|
||||
_tmod_vals,
|
||||
_mods,
|
||||
);
|
||||
}
|
||||
)?
|
||||
)*
|
||||
}
|
||||
}
|
||||
@@ -793,8 +612,12 @@ pub fn gather_target_modifiers(
|
||||
type_desc: desc::$parse,
|
||||
desc: $desc,
|
||||
removed: None $( .or(Some(RemovedOption::$removed)) )?,
|
||||
tmod: tmod_enum_opt!($struct_name, $tmod_enum_name, $opt, $($modifier_kind),*),
|
||||
mitigation: mitigation_enum_opt!($opt, $($modifier_kind),*),
|
||||
tmod: None $( .or(Some(
|
||||
OptionsTargetModifiers::$struct_name($tmod_enum::$tmod_variant)
|
||||
)))?,
|
||||
mitigation: None $( .or(Some(
|
||||
mitigation_coverage::DeniedPartialMitigationKind::$mitigation_variant
|
||||
)))?,
|
||||
},
|
||||
)*
|
||||
];
|
||||
@@ -2230,7 +2053,7 @@ pub(crate) fn parse_assert_incr_state(
|
||||
collapse_macro_debuginfo: CollapseMacroDebuginfo = (CollapseMacroDebuginfo::Unspecified,
|
||||
parse_collapse_macro_debuginfo, [TRACKED],
|
||||
"set option to collapse debuginfo for macros"),
|
||||
control_flow_guard: CFGuard = (CFGuard::Disabled, parse_cfguard, [TRACKED MITIGATION],
|
||||
control_flow_guard: CFGuard = (CFGuard::Disabled, parse_cfguard, [TRACKED] { MITIGATION: ControlFlowGuard },
|
||||
"use Windows Control Flow Guard (default: no)"),
|
||||
debug_assertions: Option<bool> = (None, parse_opt_bool, [TRACKED],
|
||||
"explicitly enable the `cfg(debug_assertions)` directive"),
|
||||
@@ -2409,7 +2232,7 @@ pub(crate) fn parse_assert_incr_state(
|
||||
(default: no)"),
|
||||
box_noalias: bool = (true, parse_bool, [TRACKED],
|
||||
"emit noalias metadata for box (default: yes)"),
|
||||
branch_protection: Option<BranchProtection> = (None, parse_branch_protection, [TRACKED TARGET_MODIFIER],
|
||||
branch_protection: Option<BranchProtection> = (None, parse_branch_protection, [TRACKED] { TARGET_MODIFIER: BranchProtection },
|
||||
"set options for branch target identification and pointer authentication on AArch64"),
|
||||
build_sdylib_interface: bool = (false, parse_bool, [UNTRACKED],
|
||||
"whether the stable interface is being built"),
|
||||
@@ -2510,7 +2333,7 @@ pub(crate) fn parse_assert_incr_state(
|
||||
fewer_names: Option<bool> = (None, parse_opt_bool, [TRACKED],
|
||||
"reduce memory use by retaining fewer names within compilation artifacts (LLVM-IR) \
|
||||
(default: no)"),
|
||||
fixed_x18: bool = (false, parse_bool, [TRACKED TARGET_MODIFIER],
|
||||
fixed_x18: bool = (false, parse_bool, [TRACKED] { TARGET_MODIFIER: FixedX18 },
|
||||
"make the x18 register reserved on AArch64 (default: no)"),
|
||||
flatten_format_args: bool = (true, parse_bool, [TRACKED],
|
||||
"flatten nested format_args!() and literals into a simplified format_args!() call \
|
||||
@@ -2554,7 +2377,7 @@ pub(crate) fn parse_assert_incr_state(
|
||||
- hashes of green query instances
|
||||
- hash collisions of query keys
|
||||
- hash collisions when creating dep-nodes"),
|
||||
indirect_branch_cs_prefix: bool = (false, parse_bool, [TRACKED TARGET_MODIFIER],
|
||||
indirect_branch_cs_prefix: bool = (false, parse_bool, [TRACKED] { TARGET_MODIFIER: IndirectBranchCsPrefix },
|
||||
"add `cs` prefix to `call` and `jmp` to indirect thunks (default: no)"),
|
||||
inline_llvm: bool = (true, parse_bool, [TRACKED],
|
||||
"enable LLVM inlining (default: yes)"),
|
||||
@@ -2749,10 +2572,10 @@ pub(crate) fn parse_assert_incr_state(
|
||||
"enable queries of the dependency graph for regression testing (default: no)"),
|
||||
randomize_layout: bool = (false, parse_bool, [TRACKED],
|
||||
"randomize the layout of types (default: no)"),
|
||||
reg_struct_return: bool = (false, parse_bool, [TRACKED TARGET_MODIFIER],
|
||||
reg_struct_return: bool = (false, parse_bool, [TRACKED] { TARGET_MODIFIER: RegStructReturn },
|
||||
"On x86-32 targets, it overrides the default ABI to return small structs in registers.
|
||||
It is UNSOUND to link together crates that use different values for this flag!"),
|
||||
regparm: Option<u32> = (None, parse_opt_number, [TRACKED TARGET_MODIFIER],
|
||||
regparm: Option<u32> = (None, parse_opt_number, [TRACKED] { TARGET_MODIFIER: Regparm },
|
||||
"On x86-32 targets, setting this to N causes the compiler to pass N arguments \
|
||||
in registers EAX, EDX, and ECX instead of on the stack for\
|
||||
\"C\", \"cdecl\", and \"stdcall\" fn.\
|
||||
@@ -2764,19 +2587,19 @@ pub(crate) fn parse_assert_incr_state(
|
||||
remark_dir: Option<PathBuf> = (None, parse_opt_pathbuf, [UNTRACKED],
|
||||
"directory into which to write optimization remarks (if not specified, they will be \
|
||||
written to standard error output)"),
|
||||
retpoline: bool = (false, parse_bool, [TRACKED TARGET_MODIFIER],
|
||||
retpoline: bool = (false, parse_bool, [TRACKED] { TARGET_MODIFIER: Retpoline },
|
||||
"enables retpoline-indirect-branches and retpoline-indirect-calls target features (default: no)"),
|
||||
retpoline_external_thunk: bool = (false, parse_bool, [TRACKED TARGET_MODIFIER],
|
||||
retpoline_external_thunk: bool = (false, parse_bool, [TRACKED] { TARGET_MODIFIER: RetpolineExternalThunk },
|
||||
"enables retpoline-external-thunk, retpoline-indirect-branches and retpoline-indirect-calls \
|
||||
target features (default: no)"),
|
||||
#[rustc_lint_opt_deny_field_access("use `Session::sanitizers()` instead of this field")]
|
||||
sanitizer: SanitizerSet = (SanitizerSet::empty(), parse_sanitizers, [TRACKED TARGET_MODIFIER],
|
||||
sanitizer: SanitizerSet = (SanitizerSet::empty(), parse_sanitizers, [TRACKED] { TARGET_MODIFIER: Sanitizer },
|
||||
"use a sanitizer"),
|
||||
sanitizer_cfi_canonical_jump_tables: Option<bool> = (Some(true), parse_opt_bool, [TRACKED],
|
||||
"enable canonical jump tables (default: yes)"),
|
||||
sanitizer_cfi_generalize_pointers: Option<bool> = (None, parse_opt_bool, [TRACKED],
|
||||
"enable generalizing pointer types (default: no)"),
|
||||
sanitizer_cfi_normalize_integers: Option<bool> = (None, parse_opt_bool, [TRACKED TARGET_MODIFIER],
|
||||
sanitizer_cfi_normalize_integers: Option<bool> = (None, parse_opt_bool, [TRACKED] { TARGET_MODIFIER: SanitizerCfiNormalizeIntegers },
|
||||
"enable normalizing integer types (default: no)"),
|
||||
sanitizer_dataflow_abilist: Vec<String> = (Vec::new(), parse_comma_list, [TRACKED],
|
||||
"additional ABI list files that control how shadow parameters are passed (comma separated)"),
|
||||
@@ -2836,7 +2659,7 @@ pub(crate) fn parse_assert_incr_state(
|
||||
src_hash_algorithm: Option<SourceFileHashAlgorithm> = (None, parse_src_file_hash, [TRACKED],
|
||||
"hash algorithm of source files in debug info (`md5`, `sha1`, or `sha256`)"),
|
||||
#[rustc_lint_opt_deny_field_access("use `Session::stack_protector` instead of this field")]
|
||||
stack_protector: StackProtector = (StackProtector::None, parse_stack_protector, [TRACKED MITIGATION],
|
||||
stack_protector: StackProtector = (StackProtector::None, parse_stack_protector, [TRACKED] { MITIGATION: StackProtector },
|
||||
"control stack smash protection strategy (`rustc --print stack-protector-strategies` for details)"),
|
||||
staticlib_allow_rdylib_deps: bool = (false, parse_bool, [TRACKED],
|
||||
"allow staticlibs to have rust dylib dependencies"),
|
||||
|
||||
@@ -133,7 +133,6 @@ macro_rules! intersperse {
|
||||
|
||||
macro_rules! denied_partial_mitigations {
|
||||
([$self:ident] enum $kind:ident {$(($name:ident, $text:expr, $since:ident, $code:expr)),*}) => {
|
||||
#[allow(non_camel_case_types)]
|
||||
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord, Encodable, BlobDecodable)]
|
||||
pub enum DeniedPartialMitigationKind {
|
||||
$($name),*
|
||||
@@ -204,8 +203,8 @@ pub fn gather_enabled_denied_partial_mitigations(&$self) -> Vec<DeniedPartialMit
|
||||
enum DeniedPartialMitigationKind {
|
||||
// The mitigation name should match the option name in rustc_session::options,
|
||||
// to allow for resetting the mitigation
|
||||
(stack_protector, "stack-protector", EditionFuture, self.stack_protector()),
|
||||
(control_flow_guard, "control-flow-guard", EditionFuture, self.opts.cg.control_flow_guard == CFGuard::Checks)
|
||||
(StackProtector, "stack-protector", EditionFuture, self.stack_protector()),
|
||||
(ControlFlowGuard, "control-flow-guard", EditionFuture, self.opts.cg.control_flow_guard == CFGuard::Checks)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -2748,6 +2748,11 @@ pub fn note_obligation_cause(
|
||||
obligation.param_env,
|
||||
obligation.cause.code(),
|
||||
);
|
||||
self.suggest_borrow_for_unsized_closure_return(
|
||||
obligation.cause.body_id,
|
||||
err,
|
||||
obligation.predicate,
|
||||
);
|
||||
self.suggest_unsized_bound_if_applicable(err, obligation);
|
||||
if let Some(span) = err.span.primary_span()
|
||||
&& let Some(mut diag) =
|
||||
|
||||
@@ -2196,6 +2196,60 @@ pub(super) fn suggest_semicolon_removal(
|
||||
false
|
||||
}
|
||||
|
||||
pub(super) fn suggest_borrow_for_unsized_closure_return<G: EmissionGuarantee>(
|
||||
&self,
|
||||
body_id: LocalDefId,
|
||||
err: &mut Diag<'_, G>,
|
||||
predicate: ty::Predicate<'tcx>,
|
||||
) {
|
||||
let Some(pred) = predicate.as_trait_clause() else {
|
||||
return;
|
||||
};
|
||||
if !self.tcx.is_lang_item(pred.def_id(), LangItem::Sized) {
|
||||
return;
|
||||
}
|
||||
|
||||
let Some(span) = err.span.primary_span() else {
|
||||
return;
|
||||
};
|
||||
let Some(node_body_id) = self.tcx.hir_node_by_def_id(body_id).body_id() else {
|
||||
return;
|
||||
};
|
||||
let body = self.tcx.hir_body(node_body_id);
|
||||
let mut expr_finder = FindExprBySpan::new(span, self.tcx);
|
||||
expr_finder.visit_expr(body.value);
|
||||
let Some(expr) = expr_finder.result else {
|
||||
return;
|
||||
};
|
||||
|
||||
let closure = match expr.kind {
|
||||
hir::ExprKind::Call(_, args) => args.iter().find_map(|arg| match arg.kind {
|
||||
hir::ExprKind::Closure(closure) => Some(closure),
|
||||
_ => None,
|
||||
}),
|
||||
hir::ExprKind::MethodCall(_, _, args, _) => {
|
||||
args.iter().find_map(|arg| match arg.kind {
|
||||
hir::ExprKind::Closure(closure) => Some(closure),
|
||||
_ => None,
|
||||
})
|
||||
}
|
||||
_ => None,
|
||||
};
|
||||
let Some(closure) = closure else {
|
||||
return;
|
||||
};
|
||||
if !matches!(closure.fn_decl.output, hir::FnRetTy::DefaultReturn(_)) {
|
||||
return;
|
||||
}
|
||||
|
||||
err.span_suggestion_verbose(
|
||||
self.tcx.hir_body(closure.body).value.span.shrink_to_lo(),
|
||||
"consider borrowing the value",
|
||||
"&",
|
||||
Applicability::MaybeIncorrect,
|
||||
);
|
||||
}
|
||||
|
||||
pub(super) fn return_type_span(&self, obligation: &PredicateObligation<'tcx>) -> Option<Span> {
|
||||
let hir::Node::Item(hir::Item { kind: hir::ItemKind::Fn { sig, .. }, .. }) =
|
||||
self.tcx.hir_node_by_def_id(obligation.cause.body_id)
|
||||
|
||||
@@ -1162,9 +1162,9 @@ checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f"
|
||||
|
||||
[[package]]
|
||||
name = "rand"
|
||||
version = "0.9.2"
|
||||
version = "0.9.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6db2770f06117d490610c7488547d543617b21bfa07796d7a12f6f1bd53850d1"
|
||||
checksum = "7ec095654a25171c2124e9e3393a930bddbffdc939556c914957a4c3e0a87166"
|
||||
dependencies = [
|
||||
"rand_chacha",
|
||||
"rand_core",
|
||||
|
||||
@@ -87,7 +87,9 @@ pub fn phase_cargo_miri(mut args: impl Iterator<Item = String>) {
|
||||
println!("`cargo miri {verb}` supports the same flags as `cargo {verb}`:\n");
|
||||
let mut cmd = cargo();
|
||||
cmd.arg(verb);
|
||||
cmd.arg("--help");
|
||||
// Forward all arguments (some of them can influence the help output, e.g.
|
||||
// the nextest verb).
|
||||
cmd.args(args);
|
||||
exec(cmd);
|
||||
}
|
||||
_ => {
|
||||
|
||||
@@ -28,7 +28,7 @@ mod downloading {
|
||||
/// The GenMC repository the we get our commit from.
|
||||
pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/MPI-SWS/genmc.git";
|
||||
/// The GenMC commit we depend on. It must be available on the specified GenMC repository.
|
||||
pub(crate) const GENMC_COMMIT: &str = "22d3d0b44dedb4e8e1aae3330e546465e4664529";
|
||||
pub(crate) const GENMC_COMMIT: &str = "29b03a66402c4453fc77901ef3be90bb55707cd4";
|
||||
|
||||
/// Ensure that a local GenMC repo is present and set to the correct commit.
|
||||
/// Return the path of the GenMC repo clone.
|
||||
@@ -159,6 +159,7 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
|
||||
.out_dir(genmc_build_dir)
|
||||
.profile(GENMC_CMAKE_PROFILE)
|
||||
.define("BUILD_LLI", "OFF")
|
||||
.define("EMIT_NA_LABELS", "OFF")
|
||||
.define("GENMC_DEBUG", if enable_genmc_debug { "ON" } else { "OFF" });
|
||||
|
||||
// The actual compilation happens here:
|
||||
@@ -172,7 +173,7 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
|
||||
// Part 2:
|
||||
// Compile the cxx_bridge (the link between the Rust and C++ code).
|
||||
|
||||
let genmc_include_dir = genmc_install_dir.join("include").join("genmc");
|
||||
let genmc_include_dir = genmc_install_dir.join("include");
|
||||
|
||||
// These are all the C++ files we need to compile, which needs to be updated if more C++ files are added to Miri.
|
||||
// We use absolute paths since relative paths can confuse IDEs when attempting to go-to-source on a path in a compiler error.
|
||||
@@ -181,10 +182,6 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
|
||||
.map(|file| std::path::absolute(cpp_files_base_path.join(file)).unwrap());
|
||||
|
||||
let mut bridge = cxx_build::bridge("src/lib.rs");
|
||||
// FIXME(genmc,cmake): Remove once the GenMC debug setting is available in the config.h file.
|
||||
if enable_genmc_debug {
|
||||
bridge.define("ENABLE_GENMC_DEBUG", None);
|
||||
}
|
||||
bridge
|
||||
.opt_level(2)
|
||||
.debug(true) // Same settings that GenMC uses (default for cmake `RelWithDebInfo`)
|
||||
|
||||
@@ -5,17 +5,17 @@
|
||||
#include "rust/cxx.h"
|
||||
|
||||
// GenMC generated headers:
|
||||
#include "config.h"
|
||||
#include "genmc/config.h"
|
||||
|
||||
// Miri `genmc-sys/src_cpp` headers:
|
||||
#include "ResultHandling.hpp"
|
||||
|
||||
// GenMC headers:
|
||||
#include "ExecutionGraph/EventLabel.hpp"
|
||||
#include "Support/MemOrdering.hpp"
|
||||
#include "Support/RMWOps.hpp"
|
||||
#include "Verification/Config.hpp"
|
||||
#include "Verification/GenMCDriver.hpp"
|
||||
#include "genmc/Execution/EventLabel.hpp"
|
||||
#include "genmc/Support/MemOrdering.hpp"
|
||||
#include "genmc/Support/RMWOps.hpp"
|
||||
#include "genmc/Verification/Config.hpp"
|
||||
#include "genmc/Verification/GenMCDriver.hpp"
|
||||
|
||||
// C++ headers:
|
||||
#include <cstdint>
|
||||
@@ -36,6 +36,7 @@ struct StoreResult;
|
||||
struct ReadModifyWriteResult;
|
||||
struct CompareExchangeResult;
|
||||
struct MutexLockResult;
|
||||
struct MallocResult;
|
||||
|
||||
// GenMC uses `int` for its thread IDs.
|
||||
using ThreadId = int;
|
||||
@@ -86,13 +87,15 @@ struct MiriGenmcShim : private GenMCDriver {
|
||||
|
||||
/**** Memory access handling ****/
|
||||
|
||||
[[nodiscard]] LoadResult handle_load(
|
||||
[[nodiscard]] LoadResult handle_atomic_load(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
uint64_t size,
|
||||
MemOrdering ord,
|
||||
GenmcScalar old_val
|
||||
);
|
||||
[[nodiscard]] LoadResult
|
||||
handle_non_atomic_load(ThreadId thread_id, uint64_t address, uint64_t size);
|
||||
[[nodiscard]] ReadModifyWriteResult handle_read_modify_write(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
@@ -113,7 +116,7 @@ struct MiriGenmcShim : private GenMCDriver {
|
||||
MemOrdering fail_load_ordering,
|
||||
bool can_fail_spuriously
|
||||
);
|
||||
[[nodiscard]] StoreResult handle_store(
|
||||
[[nodiscard]] StoreResult handle_atomic_store(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
uint64_t size,
|
||||
@@ -121,12 +124,14 @@ struct MiriGenmcShim : private GenMCDriver {
|
||||
GenmcScalar old_val,
|
||||
MemOrdering ord
|
||||
);
|
||||
[[nodiscard]] StoreResult
|
||||
handle_non_atomic_store(ThreadId thread_id, uint64_t address, uint64_t size);
|
||||
|
||||
void handle_fence(ThreadId thread_id, MemOrdering ord);
|
||||
|
||||
/**** Memory (de)allocation ****/
|
||||
|
||||
auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> uint64_t;
|
||||
auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> MallocResult;
|
||||
|
||||
/** Returns null on success, or an error string if an error occurs. */
|
||||
auto handle_free(ThreadId thread_id, uint64_t address) -> std::unique_ptr<std::string>;
|
||||
@@ -203,33 +208,15 @@ struct MiriGenmcShim : private GenMCDriver {
|
||||
auto get_estimation_results() const -> EstimationResult;
|
||||
|
||||
private:
|
||||
/** Increment the event index in the given thread by 1 and return the new event. */
|
||||
[[nodiscard]] inline auto inc_pos(ThreadId tid) -> Event {
|
||||
/** Returns the current event for a given thread. */
|
||||
inline auto curr_pos(ThreadId tid) -> Event {
|
||||
ERROR_ON(tid >= threads_action_.size(), "ThreadId out of bounds");
|
||||
return ++threads_action_[tid].event;
|
||||
return threads_action_[tid].event;
|
||||
}
|
||||
/** Decrement the event index in the given thread by 1 and return the new event. */
|
||||
inline auto dec_pos(ThreadId tid) -> Event {
|
||||
/** Increment the event index in the given thread by `count`. */
|
||||
inline void inc_pos(ThreadId tid, unsigned int count) {
|
||||
ERROR_ON(tid >= threads_action_.size(), "ThreadId out of bounds");
|
||||
return --threads_action_[tid].event;
|
||||
}
|
||||
|
||||
/**
|
||||
* Helper function for loads that need to reset the event counter when no value is returned.
|
||||
* Same syntax as `GenMCDriver::handleLoad`, but this takes a thread id instead of an Event.
|
||||
* Automatically calls `inc_pos` and `dec_pos` where needed for the given thread.
|
||||
*/
|
||||
template <EventLabel::EventLabelKind k, typename... Ts>
|
||||
auto handle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
|
||||
-> HandleResult<SVal> {
|
||||
const auto pos = inc_pos(tid);
|
||||
const auto ret =
|
||||
GenMCDriver::handleLoad<k>(nullptr, pos, old_val, std::forward<Ts>(params)...);
|
||||
// If we didn't get a value, we have to reset the index of the current thread.
|
||||
if (!std::holds_alternative<SVal>(ret)) {
|
||||
dec_pos(tid);
|
||||
}
|
||||
return ret;
|
||||
threads_action_[tid].event.index += count;
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -293,40 +280,55 @@ inline std::optional<SVal> try_to_sval(GenmcScalar scalar) {
|
||||
namespace LoadResultExt {
|
||||
inline LoadResult no_value() {
|
||||
return LoadResult {
|
||||
.invalid = false,
|
||||
.error = std::unique_ptr<std::string>(nullptr),
|
||||
.has_value = false,
|
||||
.read_value = GenmcScalarExt::uninit(),
|
||||
};
|
||||
}
|
||||
|
||||
inline LoadResult from_value(SVal read_value) {
|
||||
return LoadResult { .error = std::unique_ptr<std::string>(nullptr),
|
||||
.has_value = true,
|
||||
return LoadResult { .invalid = false,
|
||||
.error = std::unique_ptr<std::string>(nullptr),
|
||||
.read_value = GenmcScalarExt::from_sval(read_value) };
|
||||
}
|
||||
|
||||
inline LoadResult from_error(std::unique_ptr<std::string> error) {
|
||||
return LoadResult { .error = std::move(error),
|
||||
.has_value = false,
|
||||
return LoadResult { .invalid = false,
|
||||
.error = std::move(error),
|
||||
.read_value = GenmcScalarExt::uninit() };
|
||||
}
|
||||
|
||||
inline LoadResult from_invalid() {
|
||||
return LoadResult { .invalid = true, .error = nullptr, .read_value = GenmcScalarExt::uninit() };
|
||||
}
|
||||
|
||||
} // namespace LoadResultExt
|
||||
|
||||
namespace StoreResultExt {
|
||||
inline StoreResult ok(bool is_coherence_order_maximal_write) {
|
||||
return StoreResult { /* error: */ std::unique_ptr<std::string>(nullptr),
|
||||
is_coherence_order_maximal_write };
|
||||
return StoreResult { .invalid = false,
|
||||
.error = std::unique_ptr<std::string>(nullptr),
|
||||
.is_coherence_order_maximal_write = is_coherence_order_maximal_write };
|
||||
}
|
||||
|
||||
inline StoreResult from_error(std::unique_ptr<std::string> error) {
|
||||
return StoreResult { .error = std::move(error), .is_coherence_order_maximal_write = false };
|
||||
return StoreResult { .invalid = false,
|
||||
.error = std::move(error),
|
||||
.is_coherence_order_maximal_write = false };
|
||||
}
|
||||
|
||||
inline StoreResult from_invalid() {
|
||||
return StoreResult { .invalid = true,
|
||||
.error = nullptr,
|
||||
.is_coherence_order_maximal_write = false };
|
||||
}
|
||||
} // namespace StoreResultExt
|
||||
|
||||
namespace ReadModifyWriteResultExt {
|
||||
inline ReadModifyWriteResult
|
||||
ok(SVal old_value, SVal new_value, bool is_coherence_order_maximal_write) {
|
||||
return ReadModifyWriteResult { .error = std::unique_ptr<std::string>(nullptr),
|
||||
return ReadModifyWriteResult { .invalid = false,
|
||||
.error = std::unique_ptr<std::string>(nullptr),
|
||||
.old_value = GenmcScalarExt::from_sval(old_value),
|
||||
.new_value = GenmcScalarExt::from_sval(new_value),
|
||||
.is_coherence_order_maximal_write =
|
||||
@@ -334,7 +336,16 @@ ok(SVal old_value, SVal new_value, bool is_coherence_order_maximal_write) {
|
||||
}
|
||||
|
||||
inline ReadModifyWriteResult from_error(std::unique_ptr<std::string> error) {
|
||||
return ReadModifyWriteResult { .error = std::move(error),
|
||||
return ReadModifyWriteResult { .invalid = false,
|
||||
.error = std::move(error),
|
||||
.old_value = GenmcScalarExt::uninit(),
|
||||
.new_value = GenmcScalarExt::uninit(),
|
||||
.is_coherence_order_maximal_write = false };
|
||||
}
|
||||
|
||||
inline ReadModifyWriteResult from_invalid() {
|
||||
return ReadModifyWriteResult { .invalid = true,
|
||||
.error = nullptr,
|
||||
.old_value = GenmcScalarExt::uninit(),
|
||||
.new_value = GenmcScalarExt::uninit(),
|
||||
.is_coherence_order_maximal_write = false };
|
||||
@@ -343,7 +354,8 @@ inline ReadModifyWriteResult from_error(std::unique_ptr<std::string> error) {
|
||||
|
||||
namespace CompareExchangeResultExt {
|
||||
inline CompareExchangeResult success(SVal old_value, bool is_coherence_order_maximal_write) {
|
||||
return CompareExchangeResult { .error = nullptr,
|
||||
return CompareExchangeResult { .invalid = false,
|
||||
.error = nullptr,
|
||||
.old_value = GenmcScalarExt::from_sval(old_value),
|
||||
.is_success = true,
|
||||
.is_coherence_order_maximal_write =
|
||||
@@ -351,14 +363,24 @@ inline CompareExchangeResult success(SVal old_value, bool is_coherence_order_max
|
||||
}
|
||||
|
||||
inline CompareExchangeResult failure(SVal old_value) {
|
||||
return CompareExchangeResult { .error = nullptr,
|
||||
return CompareExchangeResult { .invalid = false,
|
||||
.error = nullptr,
|
||||
.old_value = GenmcScalarExt::from_sval(old_value),
|
||||
.is_success = false,
|
||||
.is_coherence_order_maximal_write = false };
|
||||
}
|
||||
|
||||
inline CompareExchangeResult from_error(std::unique_ptr<std::string> error) {
|
||||
return CompareExchangeResult { .error = std::move(error),
|
||||
return CompareExchangeResult { .invalid = false,
|
||||
.error = std::move(error),
|
||||
.old_value = GenmcScalarExt::uninit(),
|
||||
.is_success = false,
|
||||
.is_coherence_order_maximal_write = false };
|
||||
}
|
||||
|
||||
inline CompareExchangeResult from_invalid() {
|
||||
return CompareExchangeResult { .invalid = true,
|
||||
.error = nullptr,
|
||||
.old_value = GenmcScalarExt::uninit(),
|
||||
.is_success = false,
|
||||
.is_coherence_order_maximal_write = false };
|
||||
@@ -367,20 +389,42 @@ inline CompareExchangeResult from_error(std::unique_ptr<std::string> error) {
|
||||
|
||||
namespace MutexLockResultExt {
|
||||
inline MutexLockResult ok(bool is_lock_acquired) {
|
||||
return MutexLockResult { /* error: */ nullptr, /* is_reset: */ false, is_lock_acquired };
|
||||
return MutexLockResult { .invalid = false,
|
||||
.error = nullptr,
|
||||
.is_reset = false,
|
||||
.is_lock_acquired = is_lock_acquired };
|
||||
}
|
||||
|
||||
inline MutexLockResult reset() {
|
||||
return MutexLockResult { /* error: */ nullptr,
|
||||
/* is_reset: */ true,
|
||||
/* is_lock_acquired: */ false };
|
||||
return MutexLockResult { .invalid = false,
|
||||
.error = nullptr,
|
||||
.is_reset = true,
|
||||
.is_lock_acquired = false };
|
||||
}
|
||||
|
||||
inline MutexLockResult from_error(std::unique_ptr<std::string> error) {
|
||||
return MutexLockResult { /* error: */ std::move(error),
|
||||
/* is_reset: */ false,
|
||||
/* is_lock_acquired: */ false };
|
||||
return MutexLockResult { .invalid = false,
|
||||
.error = std::move(error),
|
||||
.is_reset = false,
|
||||
.is_lock_acquired = false };
|
||||
}
|
||||
|
||||
inline MutexLockResult from_invalid() {
|
||||
return MutexLockResult { .invalid = true,
|
||||
.error = nullptr,
|
||||
.is_reset = false,
|
||||
.is_lock_acquired = false };
|
||||
}
|
||||
} // namespace MutexLockResultExt
|
||||
|
||||
namespace MallocResultExt {
|
||||
inline MallocResult ok(SVal addr) {
|
||||
return MallocResult { .error = nullptr, .address = addr.get() };
|
||||
}
|
||||
|
||||
inline MallocResult from_error(std::unique_ptr<std::string> error) {
|
||||
return MallocResult { .error = std::move(error), .address = 0UL };
|
||||
}
|
||||
} // namespace MallocResultExt
|
||||
|
||||
#endif /* GENMC_MIRI_INTERFACE_HPP */
|
||||
|
||||
@@ -5,7 +5,7 @@
|
||||
#include "rust/cxx.h"
|
||||
|
||||
// GenMC headers:
|
||||
#include "Verification/VerificationError.hpp"
|
||||
#include "genmc/Verification/VerificationError.hpp"
|
||||
|
||||
#include <format>
|
||||
#include <memory>
|
||||
|
||||
@@ -7,22 +7,22 @@
|
||||
#include "genmc-sys/src/lib.rs.h"
|
||||
|
||||
// GenMC headers:
|
||||
#include "ADT/value_ptr.hpp"
|
||||
#include "ExecutionGraph/EventLabel.hpp"
|
||||
#include "ExecutionGraph/LoadAnnotation.hpp"
|
||||
#include "Runtime/InterpreterEnumAPI.hpp"
|
||||
#include "Static/ModuleID.hpp"
|
||||
#include "Support/ASize.hpp"
|
||||
#include "Support/Error.hpp"
|
||||
#include "Support/Logger.hpp"
|
||||
#include "Support/MemAccess.hpp"
|
||||
#include "Support/RMWOps.hpp"
|
||||
#include "Support/SAddr.hpp"
|
||||
#include "Support/SVal.hpp"
|
||||
#include "Support/ThreadInfo.hpp"
|
||||
#include "Support/Verbosity.hpp"
|
||||
#include "Verification/GenMCDriver.hpp"
|
||||
#include "Verification/MemoryModel.hpp"
|
||||
#include "genmc/ADT/value_ptr.hpp"
|
||||
#include "genmc/Execution/EventLabel.hpp"
|
||||
#include "genmc/Execution/LoadAnnotation.hpp"
|
||||
#include "genmc/Support/ASize.hpp"
|
||||
#include "genmc/Support/ActionEnums.hpp"
|
||||
#include "genmc/Support/Error.hpp"
|
||||
#include "genmc/Support/Logger.hpp"
|
||||
#include "genmc/Support/MemAccess.hpp"
|
||||
#include "genmc/Support/ModuleVarID.hpp"
|
||||
#include "genmc/Support/RMWOps.hpp"
|
||||
#include "genmc/Support/SAddr.hpp"
|
||||
#include "genmc/Support/SVal.hpp"
|
||||
#include "genmc/Support/ThreadInfo.hpp"
|
||||
#include "genmc/Support/Verbosity.hpp"
|
||||
#include "genmc/Verification/GenMCDriver.hpp"
|
||||
#include "genmc/Verification/MemoryModel.hpp"
|
||||
|
||||
// C++ headers:
|
||||
#include <cmath>
|
||||
@@ -47,13 +47,13 @@ auto MiriGenmcShim::schedule_next(
|
||||
[](auto&& arg) {
|
||||
using T = std::decay_t<decltype(arg)>;
|
||||
if constexpr (std::is_same_v<T, int>)
|
||||
return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(arg) };
|
||||
return SchedulingResult { ExecutionStatus::Ok, static_cast<int32_t>(arg) };
|
||||
else if constexpr (std::is_same_v<T, Blocked>)
|
||||
return SchedulingResult { ExecutionState::Blocked, 0 };
|
||||
return SchedulingResult { ExecutionStatus::Blocked, 0 };
|
||||
else if constexpr (std::is_same_v<T, Error>)
|
||||
return SchedulingResult { ExecutionState::Error, 0 };
|
||||
return SchedulingResult { ExecutionStatus::Error, 0 };
|
||||
else if constexpr (std::is_same_v<T, Finished>)
|
||||
return SchedulingResult { ExecutionState::Finished, 0 };
|
||||
return SchedulingResult { ExecutionStatus::Finished, 0 };
|
||||
else
|
||||
static_assert(false, "non-exhaustive visitor!");
|
||||
},
|
||||
@@ -75,39 +75,66 @@ auto MiriGenmcShim::handle_execution_end() -> std::unique_ptr<std::string> {
|
||||
/**** Blocking instructions ****/
|
||||
|
||||
void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) {
|
||||
BUG_ON(getExec().getGraph().isThreadBlocked(thread_id));
|
||||
GenMCDriver::handleAssume(nullptr, inc_pos(thread_id), assume_type);
|
||||
auto ret = GenMCDriver::handleAssume(nullptr, curr_pos(thread_id), assume_type);
|
||||
inc_pos(thread_id, ret.count);
|
||||
}
|
||||
|
||||
/**** Memory access handling ****/
|
||||
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_load(
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_atomic_load(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
uint64_t size,
|
||||
MemOrdering ord,
|
||||
GenmcScalar old_val
|
||||
) -> LoadResult {
|
||||
// `type` is only used for printing.
|
||||
const auto type = AType::Unsigned;
|
||||
const auto ret = handle_load_reset_if_none<EventLabel::EventLabelKind::Read>(
|
||||
thread_id,
|
||||
const auto ret = GenMCDriver::handleRead(
|
||||
nullptr,
|
||||
curr_pos(thread_id),
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
ord,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
type
|
||||
nullptr,
|
||||
std::nullopt,
|
||||
EventDeps()
|
||||
);
|
||||
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret))
|
||||
inc_pos(thread_id, ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret.result))
|
||||
return LoadResultExt::from_error(format_error(*err));
|
||||
const auto* ret_val = std::get_if<SVal>(&ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
ERROR_ON(!ret_val, "Unimplemented: load returned unexpected result.");
|
||||
if (std::holds_alternative<Invalid>(ret.result))
|
||||
return LoadResultExt::from_invalid();
|
||||
const auto* ret_val = std::get_if<SVal>(&ret.result);
|
||||
// FIXME(genmc): handle `HandleResult::Reset` return value.
|
||||
ERROR_ON(!ret_val, "Unimplemented: atomic load returned unexpected result.");
|
||||
return LoadResultExt::from_value(*ret_val);
|
||||
}
|
||||
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_store(
|
||||
[[nodiscard]] auto
|
||||
MiriGenmcShim::handle_non_atomic_load(ThreadId thread_id, uint64_t address, uint64_t size)
|
||||
-> LoadResult {
|
||||
const auto ret = GenMCDriver::handleNALoad(
|
||||
nullptr,
|
||||
curr_pos(thread_id),
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
EventDeps()
|
||||
);
|
||||
inc_pos(thread_id, ret.count);
|
||||
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret.result))
|
||||
return LoadResultExt::from_error(format_error(*err));
|
||||
if (std::holds_alternative<Invalid>(ret.result))
|
||||
return LoadResultExt::from_invalid();
|
||||
// FIXME(genmc): handle `HandleResult::Reset` return value.
|
||||
ERROR_ON(
|
||||
!std::holds_alternative<std::monostate>(ret.result),
|
||||
"Unimplemented: non-atomic load returned unexpected result."
|
||||
);
|
||||
return LoadResultExt::no_value();
|
||||
}
|
||||
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_atomic_store(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
uint64_t size,
|
||||
@@ -115,31 +142,57 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
|
||||
GenmcScalar old_val,
|
||||
MemOrdering ord
|
||||
) -> StoreResult {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
|
||||
const auto ret = GenMCDriver::handleWrite(
|
||||
nullptr,
|
||||
pos,
|
||||
curr_pos(thread_id),
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
ord,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
/* type */ AType::Unsigned, // `type` is only used for printing.
|
||||
GenmcScalarExt::to_sval(value),
|
||||
WriteAttr(),
|
||||
EventDeps()
|
||||
);
|
||||
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret))
|
||||
inc_pos(thread_id, ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret.result))
|
||||
return StoreResultExt::from_error(format_error(*err));
|
||||
if (std::holds_alternative<Invalid>(ret.result))
|
||||
return StoreResultExt::from_invalid();
|
||||
|
||||
const auto* is_co_max = std::get_if<bool>(&ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
ERROR_ON(!is_co_max, "Unimplemented: Store returned unexpected result.");
|
||||
const auto* is_co_max = std::get_if<bool>(&ret.result);
|
||||
// FIXME(genmc): handle `HandleResult::Reset` return value.
|
||||
ERROR_ON(!is_co_max, "Unimplemented: atomic store returned unexpected result.");
|
||||
return StoreResultExt::ok(*is_co_max);
|
||||
}
|
||||
|
||||
[[nodiscard]] auto
|
||||
MiriGenmcShim::handle_non_atomic_store(ThreadId thread_id, uint64_t address, uint64_t size)
|
||||
-> StoreResult {
|
||||
const auto ret = GenMCDriver::handleNAStore(
|
||||
nullptr,
|
||||
curr_pos(thread_id),
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
EventDeps()
|
||||
);
|
||||
inc_pos(thread_id, ret.count);
|
||||
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret.result))
|
||||
return StoreResultExt::from_error(format_error(*err));
|
||||
if (std::holds_alternative<Invalid>(ret.result))
|
||||
return StoreResultExt::from_invalid();
|
||||
// FIXME(genmc): handle `HandleResult::Reset` return value.
|
||||
ERROR_ON(
|
||||
!std::holds_alternative<std::monostate>(ret.result),
|
||||
"Unimplemented: non-atomic store returned unexpected result."
|
||||
);
|
||||
return StoreResultExt::ok(true);
|
||||
}
|
||||
|
||||
void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
|
||||
auto ret = GenMCDriver::handleFence(nullptr, curr_pos(thread_id), ord, EventDeps());
|
||||
inc_pos(thread_id, ret.count);
|
||||
}
|
||||
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_read_modify_write(
|
||||
@@ -155,45 +208,52 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
|
||||
// into a load and a store component. This means we can have for example `AcqRel` loads and
|
||||
// stores, but this is intended for RMW operations.
|
||||
|
||||
// Somewhat confusingly, the GenMC term for RMW read/write labels is
|
||||
// `FaiRead` and `FaiWrite`.
|
||||
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::FaiRead>(
|
||||
thread_id,
|
||||
const auto load_ret = GenMCDriver::handleFaiRead(
|
||||
nullptr,
|
||||
curr_pos(thread_id),
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
ordering,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Unsigned, // The type is only used for printing.
|
||||
rmw_op,
|
||||
GenmcScalarExt::to_sval(rhs_value),
|
||||
WriteAttr(),
|
||||
nullptr,
|
||||
std::nullopt,
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret))
|
||||
inc_pos(thread_id, load_ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret.result))
|
||||
return ReadModifyWriteResultExt::from_error(format_error(*err));
|
||||
if (std::holds_alternative<GenMCDriver::Invalid>(load_ret.result))
|
||||
return ReadModifyWriteResultExt::from_invalid();
|
||||
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret.result);
|
||||
// FIXME(genmc): handle `HandleResult::Reset` return values.
|
||||
ERROR_ON(!ret_val, "Unimplemented: read-modify-write returned unexpected result.");
|
||||
const auto read_old_val = *ret_val;
|
||||
const auto new_value =
|
||||
executeRMWBinOp(read_old_val, GenmcScalarExt::to_sval(rhs_value), size, rmw_op);
|
||||
|
||||
const auto storePos = inc_pos(thread_id);
|
||||
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
|
||||
const auto store_ret = GenMCDriver::handleFaiWrite(
|
||||
nullptr,
|
||||
storePos,
|
||||
curr_pos(thread_id),
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
ordering,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Unsigned, // The type is only used for printing.
|
||||
new_value
|
||||
new_value,
|
||||
WriteAttr(),
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret))
|
||||
inc_pos(thread_id, store_ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret.result))
|
||||
return ReadModifyWriteResultExt::from_error(format_error(*err));
|
||||
if (std::holds_alternative<GenMCDriver::Invalid>(store_ret.result))
|
||||
return ReadModifyWriteResultExt::from_invalid();
|
||||
|
||||
const auto* is_co_max = std::get_if<bool>(&store_ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
const auto* is_co_max = std::get_if<bool>(&store_ret.result);
|
||||
// FIXME(genmc): handle `HandleResult::Reset` return values.
|
||||
ERROR_ON(!is_co_max, "Unimplemented: RMW store returned unexpected result.");
|
||||
return ReadModifyWriteResultExt::ok(
|
||||
/* old_value: */ read_old_val,
|
||||
@@ -222,20 +282,28 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
|
||||
auto expectedVal = GenmcScalarExt::to_sval(expected_value);
|
||||
auto new_val = GenmcScalarExt::to_sval(new_value);
|
||||
|
||||
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::CasRead>(
|
||||
thread_id,
|
||||
const auto load_ret = GenMCDriver::handleCasRead(
|
||||
nullptr,
|
||||
curr_pos(thread_id),
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
success_ordering,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Unsigned, // The type is only used for printing.
|
||||
expectedVal,
|
||||
new_val
|
||||
new_val,
|
||||
WriteAttr(),
|
||||
nullptr,
|
||||
std::nullopt,
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret))
|
||||
inc_pos(thread_id, load_ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret.result))
|
||||
return CompareExchangeResultExt::from_error(format_error(*err));
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
if (std::holds_alternative<GenMCDriver::Invalid>(load_ret.result))
|
||||
return CompareExchangeResultExt::from_invalid();
|
||||
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret.result);
|
||||
// FIXME(genmc): handle `HandleResult::Reset` return values.
|
||||
ERROR_ON(nullptr == ret_val, "Unimplemented: load returned unexpected result.");
|
||||
const auto read_old_val = *ret_val;
|
||||
if (read_old_val != expectedVal)
|
||||
@@ -243,21 +311,25 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
|
||||
|
||||
// FIXME(GenMC): Add support for modelling spurious failures.
|
||||
|
||||
const auto storePos = inc_pos(thread_id);
|
||||
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
|
||||
const auto store_ret = GenMCDriver::handleCasWrite(
|
||||
nullptr,
|
||||
storePos,
|
||||
curr_pos(thread_id),
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
success_ordering,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Unsigned, // The type is only used for printing.
|
||||
new_val
|
||||
new_val,
|
||||
WriteAttr(),
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret))
|
||||
inc_pos(thread_id, store_ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret.result))
|
||||
return CompareExchangeResultExt::from_error(format_error(*err));
|
||||
const auto* is_co_max = std::get_if<bool>(&store_ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
if (std::holds_alternative<GenMCDriver::Invalid>(store_ret.result))
|
||||
return CompareExchangeResultExt::from_invalid();
|
||||
|
||||
const auto* is_co_max = std::get_if<bool>(&store_ret.result);
|
||||
// FIXME(genmc): handle `HandleResult::Reset` return values.
|
||||
ERROR_ON(!is_co_max, "Unimplemented: compare-exchange store returned unexpected result.");
|
||||
return CompareExchangeResultExt::success(read_old_val, *is_co_max);
|
||||
}
|
||||
@@ -265,33 +337,45 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
|
||||
/**** Memory (de)allocation ****/
|
||||
|
||||
auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment)
|
||||
-> uint64_t {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
|
||||
-> MallocResult {
|
||||
// These are only used for printing and features Miri-GenMC doesn't support (yet).
|
||||
const auto storage_duration = StorageDuration::SD_Heap;
|
||||
// Volatile, as opposed to "persistent" (i.e., non-volatile memory that persists over reboots)
|
||||
const auto storage_type = StorageType::ST_Volatile;
|
||||
const auto address_space = AddressSpace::AS_User;
|
||||
|
||||
const SVal ret_val = GenMCDriver::handleMalloc(
|
||||
const auto ret = GenMCDriver::handleMalloc(
|
||||
nullptr,
|
||||
pos,
|
||||
curr_pos(thread_id),
|
||||
size,
|
||||
alignment,
|
||||
storage_duration,
|
||||
storage_type,
|
||||
address_space,
|
||||
nullptr,
|
||||
"",
|
||||
EventDeps()
|
||||
);
|
||||
return ret_val.get();
|
||||
inc_pos(thread_id, ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret.result))
|
||||
return MallocResultExt::from_error(format_error(*err));
|
||||
const auto* addr = std::get_if<SVal>(&ret.result);
|
||||
ERROR_ON(!addr, "Unimplemented: malloc returned unexpected result.");
|
||||
return MallocResultExt::ok(*addr);
|
||||
}
|
||||
|
||||
auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address)
|
||||
-> std::unique_ptr<std::string> {
|
||||
auto pos = inc_pos(thread_id);
|
||||
auto ret = GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps());
|
||||
return ret.has_value() ? format_error(*ret) : nullptr;
|
||||
auto ret = GenMCDriver::handleFree(nullptr, curr_pos(thread_id), SAddr(address), EventDeps());
|
||||
inc_pos(thread_id, ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret.result))
|
||||
return format_error(*err);
|
||||
|
||||
ERROR_ON(
|
||||
!std::holds_alternative<std::monostate>(ret.result),
|
||||
"Unimplemented: free returned unexpected result."
|
||||
);
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
/**** Estimation mode result ****/
|
||||
@@ -325,12 +409,12 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
|
||||
const auto annot = std::move(Annotation(
|
||||
AssumeType::Spinloop,
|
||||
Annotation::ExprVP(
|
||||
NeExpr<ModuleID::ID>::create(
|
||||
NeExpr<ModuleVarID>::create(
|
||||
// `RegisterExpr` marks the value of the current expression, i.e., the loaded value.
|
||||
// The `id` is ignored by GenMC; it is only used by the LLI frontend to substitute
|
||||
// other variables from previous expressions that may be used here.
|
||||
RegisterExpr<ModuleID::ID>::create(size_bits, /* id */ 0),
|
||||
ConcreteExpr<ModuleID::ID>::create(size_bits, MutexState::LOCKED)
|
||||
RegisterExpr<ModuleVarID>::create(size_bits, /* id */ 0),
|
||||
ConcreteExpr<ModuleVarID>::create(size_bits, MutexState::LOCKED)
|
||||
)
|
||||
.release()
|
||||
)
|
||||
@@ -340,26 +424,34 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
|
||||
// access, if there previously was a non-atomic initializing access. We set the initial state of
|
||||
// a mutex to be "unlocked".
|
||||
const auto old_val = MutexState::UNLOCKED;
|
||||
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::LockCasRead>(
|
||||
thread_id,
|
||||
const auto load_ret = GenMCDriver::handleLockCasRead(
|
||||
nullptr,
|
||||
curr_pos(thread_id),
|
||||
old_val,
|
||||
address,
|
||||
size,
|
||||
annot,
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret))
|
||||
inc_pos(thread_id, load_ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret.result))
|
||||
return MutexLockResultExt::from_error(format_error(*err));
|
||||
if (std::holds_alternative<GenMCDriver::Invalid>(load_ret.result))
|
||||
return MutexLockResultExt::from_invalid();
|
||||
// If we get a `Reset`, GenMC decided that this lock operation should not yet run, since it
|
||||
// would not acquire the mutex. Like the handling of the case further down where we read a `1`
|
||||
// ("Mutex already locked"), Miri should call the handle function again once the current thread
|
||||
// is scheduled by GenMC the next time.
|
||||
if (std::holds_alternative<Reset>(load_ret))
|
||||
if (std::holds_alternative<Reset>(load_ret.result))
|
||||
return MutexLockResultExt::reset();
|
||||
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret);
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret.result);
|
||||
ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result.");
|
||||
ERROR_ON(!MutexState::isValid(*ret_val), "Mutex read value was neither 0 nor 1");
|
||||
ERROR_ON(
|
||||
!MutexState::isValid(*ret_val),
|
||||
"Mutex read value was neither 0 nor 1 ({})",
|
||||
std::to_string(ret_val->get())
|
||||
);
|
||||
if (*ret_val == MutexState::LOCKED) {
|
||||
// We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire
|
||||
// it. GenMC determines this based on the annotation we pass with the load further up in
|
||||
@@ -368,69 +460,72 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
|
||||
return MutexLockResultExt::ok(false);
|
||||
}
|
||||
|
||||
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
|
||||
nullptr,
|
||||
inc_pos(thread_id),
|
||||
old_val,
|
||||
address,
|
||||
size,
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret))
|
||||
const auto store_ret =
|
||||
GenMCDriver::handleLockCasWrite(nullptr, curr_pos(thread_id), address, size, EventDeps());
|
||||
inc_pos(thread_id, store_ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret.result))
|
||||
return MutexLockResultExt::from_error(format_error(*err));
|
||||
if (std::holds_alternative<GenMCDriver::Invalid>(store_ret.result))
|
||||
return MutexLockResultExt::from_invalid();
|
||||
// We don't update Miri's memory for this operation so we don't need to know if the store
|
||||
// was the co-maximal store, but we still check that we at least get a boolean as the result
|
||||
// of the store.
|
||||
const auto* is_co_max = std::get_if<bool>(&store_ret);
|
||||
const auto* is_co_max = std::get_if<bool>(&store_ret.result);
|
||||
ERROR_ON(!is_co_max, "Unimplemented: mutex_try_lock store returned unexpected result.");
|
||||
return MutexLockResultExt::ok(true);
|
||||
}
|
||||
|
||||
auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size)
|
||||
-> MutexLockResult {
|
||||
auto& currPos = threads_action_[thread_id].event;
|
||||
// As usual, we need to tell GenMC which value was stored at this location before this atomic
|
||||
// access, if there previously was a non-atomic initializing access. We set the initial state of
|
||||
// a mutex to be "unlocked".
|
||||
const auto old_val = MutexState::UNLOCKED;
|
||||
const auto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
|
||||
const auto load_ret = GenMCDriver::handleTrylockCasRead(
|
||||
nullptr,
|
||||
++currPos,
|
||||
curr_pos(thread_id),
|
||||
old_val,
|
||||
SAddr(address),
|
||||
ASize(size)
|
||||
ASize(size),
|
||||
std::nullopt,
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret))
|
||||
inc_pos(thread_id, load_ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret.result))
|
||||
return MutexLockResultExt::from_error(format_error(*err));
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret);
|
||||
if (std::holds_alternative<GenMCDriver::Invalid>(load_ret.result))
|
||||
return MutexLockResultExt::from_invalid();
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret.result);
|
||||
ERROR_ON(!ret_val, "Unimplemented: mutex trylock load returned unexpected result.");
|
||||
|
||||
ERROR_ON(!MutexState::isValid(*ret_val), "Mutex read value was neither 0 nor 1");
|
||||
if (*ret_val == MutexState::LOCKED)
|
||||
return MutexLockResultExt::ok(false); /* Lock already held. */
|
||||
|
||||
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
|
||||
const auto store_ret = GenMCDriver::handleTrylockCasWrite(
|
||||
nullptr,
|
||||
++currPos,
|
||||
old_val,
|
||||
curr_pos(thread_id),
|
||||
SAddr(address),
|
||||
ASize(size)
|
||||
ASize(size),
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret))
|
||||
inc_pos(thread_id, store_ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret.result))
|
||||
return MutexLockResultExt::from_error(format_error(*err));
|
||||
if (std::holds_alternative<GenMCDriver::Invalid>(store_ret.result))
|
||||
return MutexLockResultExt::from_invalid();
|
||||
// We don't update Miri's memory for this operation so we don't need to know if the store was
|
||||
// co-maximal, but we still check that we get a boolean result.
|
||||
const auto* is_co_max = std::get_if<bool>(&store_ret);
|
||||
const auto* is_co_max = std::get_if<bool>(&store_ret.result);
|
||||
ERROR_ON(!is_co_max, "Unimplemented: store part of mutex try_lock returned unexpected result.");
|
||||
return MutexLockResultExt::ok(true);
|
||||
}
|
||||
|
||||
auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size)
|
||||
-> StoreResult {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
|
||||
const auto ret = GenMCDriver::handleUnlockWrite(
|
||||
nullptr,
|
||||
pos,
|
||||
curr_pos(thread_id),
|
||||
// As usual, we need to tell GenMC which value was stored at this location before this
|
||||
// atomic access, if there previously was a non-atomic initializing access. We set the
|
||||
// initial state of a mutex to be "unlocked".
|
||||
@@ -438,13 +533,16 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
|
||||
MemOrdering::Release,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Signed,
|
||||
/* store_value */ MutexState::UNLOCKED,
|
||||
WriteAttr(),
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret))
|
||||
inc_pos(thread_id, ret.count);
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret.result))
|
||||
return StoreResultExt::from_error(format_error(*err));
|
||||
const auto* is_co_max = std::get_if<bool>(&ret);
|
||||
if (std::holds_alternative<GenMCDriver::Invalid>(ret.result))
|
||||
return StoreResultExt::from_invalid();
|
||||
const auto* is_co_max = std::get_if<bool>(&ret.result);
|
||||
ERROR_ON(!is_co_max, "Unimplemented: store part of mutex unlock returned unexpected result.");
|
||||
return StoreResultExt::ok(*is_co_max);
|
||||
}
|
||||
@@ -452,40 +550,62 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
|
||||
/** Thread creation/joining */
|
||||
|
||||
void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id) {
|
||||
// NOTE: The threadCreate event happens in the parent:
|
||||
const auto pos = inc_pos(parent_id);
|
||||
// FIXME(genmc): for supporting symmetry reduction, these will need to be properly set:
|
||||
const unsigned fun_id = 0;
|
||||
const SVal arg = SVal(0);
|
||||
const ThreadInfo child_info =
|
||||
ThreadInfo { thread_id, parent_id, fun_id, arg, "unknown thread" };
|
||||
|
||||
const auto child_tid = GenMCDriver::handleThreadCreate(nullptr, pos, child_info, EventDeps());
|
||||
// NOTE: The threadCreate event happens in the parent:
|
||||
const auto ret =
|
||||
GenMCDriver::handleThreadCreate(nullptr, curr_pos(parent_id), child_info, EventDeps());
|
||||
inc_pos(parent_id, ret.count);
|
||||
ERROR_ON(
|
||||
!std::holds_alternative<int>(ret.result),
|
||||
"Unimplemented: unexpected return value for thread create"
|
||||
);
|
||||
auto child_tid = std::get<int>(ret.result);
|
||||
|
||||
// Sanity check the thread id, which is the index in the `threads_action_` array.
|
||||
BUG_ON(child_tid != thread_id || child_tid <= 0 || child_tid != threads_action_.size());
|
||||
VERIFY(child_tid == thread_id && child_tid > 0 && child_tid == threads_action_.size());
|
||||
threads_action_.push_back(Action(ActionKind::Load, Event(child_tid, 0)));
|
||||
}
|
||||
|
||||
void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
|
||||
// The thread join event happens in the parent.
|
||||
const auto pos = inc_pos(thread_id);
|
||||
|
||||
const auto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
|
||||
// If the join failed, decrease the event index again:
|
||||
if (!std::holds_alternative<SVal>(ret)) {
|
||||
dec_pos(thread_id);
|
||||
}
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset, VerificationError}` return values.
|
||||
const auto ret =
|
||||
GenMCDriver::handleThreadJoin(nullptr, curr_pos(thread_id), child_id, EventDeps());
|
||||
inc_pos(thread_id, ret.count);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, VerificationError}` return values.
|
||||
ERROR_ON(
|
||||
!std::holds_alternative<SVal>(ret.result) && !std::holds_alternative<Reset>(ret.result),
|
||||
"Unimplemented: unexpected return value for thread join"
|
||||
);
|
||||
// FIXME(genmc): Here Reset{} is silently accepted. Double-check why that is.
|
||||
// The reason is likely that, although GenMC wants to re-run the join instruction,
|
||||
// when GenMC deems that the join has executed, it will also deem it successful,
|
||||
// i.e., the return value is guaranteed to be 0 (or at least we assume that).
|
||||
// In this case, it doesn't matter that we don't re-run the instruction, since
|
||||
// Miri sets the correct return value, and GenMC will only schedule this thread
|
||||
// when it knows the child has terminated.
|
||||
|
||||
// NOTE: Thread return value is ignored, since Miri doesn't need it.
|
||||
}
|
||||
|
||||
void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
GenMCDriver::handleThreadFinish(nullptr, pos, SVal(ret_val));
|
||||
auto ret = GenMCDriver::handleThreadFinish(nullptr, curr_pos(thread_id), SVal(ret_val));
|
||||
inc_pos(thread_id, ret.count);
|
||||
ERROR_ON(
|
||||
!std::holds_alternative<std::monostate>(ret.result),
|
||||
"Unimplemented: unexpected return value for thread finish"
|
||||
);
|
||||
}
|
||||
|
||||
void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
GenMCDriver::handleThreadKill(nullptr, pos);
|
||||
auto ret = GenMCDriver::handleThreadKill(nullptr, curr_pos(thread_id));
|
||||
inc_pos(thread_id, ret.count);
|
||||
ERROR_ON(
|
||||
!std::holds_alternative<std::monostate>(ret.result),
|
||||
"Unimplemented: unexpected return value for thread kill"
|
||||
);
|
||||
}
|
||||
|
||||
@@ -7,9 +7,8 @@
|
||||
#include "genmc-sys/src/lib.rs.h"
|
||||
|
||||
// GenMC headers:
|
||||
#include "Support/Error.hpp"
|
||||
#include "Support/Verbosity.hpp"
|
||||
#include "Verification/InterpreterCallbacks.hpp"
|
||||
#include "genmc/Support/Error.hpp"
|
||||
#include "genmc/Support/Verbosity.hpp"
|
||||
|
||||
// C++ headers:
|
||||
#include <cstdint>
|
||||
@@ -113,6 +112,13 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
|
||||
// value written by the skipped thread.
|
||||
conf->replayCompletedThreads = true;
|
||||
|
||||
// Initialization checking is done by Miri; GenMC's checks are incorrect for Rust.
|
||||
conf->disableInitializationChecks = true;
|
||||
|
||||
// Don't check static-address validity as it's incompatible with Miri's
|
||||
// dynamic discovery of static variables.
|
||||
conf->disableStaticValidityChecks = true;
|
||||
|
||||
// FIXME(genmc): implement symmetry reduction.
|
||||
ERROR_ON(
|
||||
params.do_symmetry_reduction,
|
||||
@@ -160,45 +166,5 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
|
||||
|
||||
// Create the actual driver and Miri-GenMC communication shim.
|
||||
auto driver = std::make_unique<MiriGenmcShim>(std::move(conf), mode);
|
||||
|
||||
// FIXME(genmc,HACK): Until a proper solution is implemented in GenMC, these callbacks will
|
||||
// allow Miri to return information about global allocations and override uninitialized memory
|
||||
// checks for non-atomic loads (Miri handles those without GenMC, so the error would be wrong).
|
||||
auto interpreter_callbacks = InterpreterCallbacks {
|
||||
// Miri already ensures that memory accesses are valid, so this check doesn't matter.
|
||||
// We check that the address is static, but skip checking if it is part of an actual
|
||||
// allocation.
|
||||
.isStaticallyAllocated = [](SAddr addr) { return addr.isStatic(); },
|
||||
// FIXME(genmc,error reporting): Once a proper a proper API for passing such information is
|
||||
// implemented in GenMC, Miri should use it to improve the produced error messages.
|
||||
.getStaticName = [](SAddr addr) { return "[UNKNOWN STATIC]"; },
|
||||
// This function is called to get the initial value stored at the given address.
|
||||
//
|
||||
// From a Miri perspective, this API doesn't work very well: most memory starts out
|
||||
// "uninitialized";
|
||||
// only statics have an initial value. And their initial value is just a sequence of bytes,
|
||||
// but GenMC expect this to be already split into separate atomic variables. So we return a
|
||||
// dummy value.
|
||||
// This value should never be visible to the interpreted program.
|
||||
// GenMC does not understand uninitialized memory the same way Miri does, which may cause
|
||||
// this function to be called. The returned value can be visible to Miri or the user:
|
||||
// - Printing the execution graph may contain this value in place of uninitialized values.
|
||||
// FIXME(genmc): NOTE: printing the execution graph is not yet implemented.
|
||||
// - Non-atomic loads may return this value, but Miri ignores values of non-atomic loads.
|
||||
// - Atomic loads will *not* see this value once mixed atomic-non-atomic support is added.
|
||||
// Currently, atomic loads can see this value, unless initialized by an *atomic* store.
|
||||
// FIXME(genmc): update this comment once mixed atomic-non-atomic support is added.
|
||||
//
|
||||
// FIXME(genmc): implement proper support for uninitialized memory in GenMC.
|
||||
// Ideally, the initial value getter would return an `optional<SVal>`, since the memory
|
||||
// location may be uninitialized.
|
||||
.initValGetter = [](const AAccess& a) { return SVal(0xDEAD); },
|
||||
// Miri serves non-atomic loads from its own memory and these GenMC checks are wrong in that
|
||||
// case. This should no longer be required with proper mixed-size access support.
|
||||
.skipUninitLoadChecks = [](const MemAccessLabel* access_label
|
||||
) { return access_label->getOrdering() == MemOrdering::NotAtomic; },
|
||||
};
|
||||
driver->setInterpCallbacks(std::move(interpreter_callbacks));
|
||||
|
||||
return driver;
|
||||
}
|
||||
|
||||
@@ -140,15 +140,15 @@ enum LogLevel {
|
||||
/// Log errors, warnings and tips.
|
||||
Tip,
|
||||
/// Debug print considered revisits.
|
||||
/// Downgraded to `Tip` if `GENMC_DEBUG` is not enabled.
|
||||
/// Downgraded to `Tip` if `ENABLE_GENMC_DEBUG` is not enabled.
|
||||
Debug1Revisits,
|
||||
/// Print the execution graph after every memory access.
|
||||
/// Also includes the previous debug log level.
|
||||
/// Downgraded to `Tip` if `GENMC_DEBUG` is not enabled.
|
||||
/// Downgraded to `Tip` if `ENABLE_GENMC_DEBUG` is not enabled.
|
||||
Debug2MemoryAccesses,
|
||||
/// Print reads-from values considered by GenMC.
|
||||
/// Also includes the previous debug log level.
|
||||
/// Downgraded to `Tip` if `GENMC_DEBUG` is not enabled.
|
||||
/// Downgraded to `Tip` if `ENABLE_GENMC_DEBUG` is not enabled.
|
||||
Debug3ReadsFrom,
|
||||
}
|
||||
|
||||
@@ -182,7 +182,7 @@ struct GenmcScalar {
|
||||
|
||||
#[must_use]
|
||||
#[derive(Debug, Clone, Copy)]
|
||||
enum ExecutionState {
|
||||
enum ExecutionStatus {
|
||||
Ok,
|
||||
Error,
|
||||
Blocked,
|
||||
@@ -192,7 +192,7 @@ enum ExecutionState {
|
||||
#[must_use]
|
||||
#[derive(Debug)]
|
||||
struct SchedulingResult {
|
||||
exec_state: ExecutionState,
|
||||
exec_status: ExecutionStatus,
|
||||
next_thread: i32,
|
||||
}
|
||||
|
||||
@@ -212,10 +212,10 @@ struct EstimationResult {
|
||||
#[must_use]
|
||||
#[derive(Debug)]
|
||||
struct LoadResult {
|
||||
/// If `true`, exploration should be dropped, **and all other fields are invalid**.
|
||||
invalid: bool,
|
||||
/// If not null, contains the error encountered during the handling of the load.
|
||||
error: UniquePtr<CxxString>,
|
||||
/// Indicates whether a value was read or not.
|
||||
has_value: bool,
|
||||
/// The value that was read. Should not be used if `has_value` is `false`.
|
||||
read_value: GenmcScalar,
|
||||
}
|
||||
@@ -223,6 +223,8 @@ struct LoadResult {
|
||||
#[must_use]
|
||||
#[derive(Debug)]
|
||||
struct StoreResult {
|
||||
/// If `true`, exploration should be dropped, **and all other fields are invalid**.
|
||||
invalid: bool,
|
||||
/// If not null, contains the error encountered during the handling of the store.
|
||||
error: UniquePtr<CxxString>,
|
||||
/// `true` if the write should also be reflected in Miri's memory representation.
|
||||
@@ -232,6 +234,8 @@ struct StoreResult {
|
||||
#[must_use]
|
||||
#[derive(Debug)]
|
||||
struct ReadModifyWriteResult {
|
||||
/// If `true`, exploration should be dropped, **and all other fields are invalid**.
|
||||
invalid: bool,
|
||||
/// If there was an error, it will be stored in `error`, otherwise it is `None`.
|
||||
error: UniquePtr<CxxString>,
|
||||
/// The value that was read by the RMW operation as the left operand.
|
||||
@@ -245,6 +249,8 @@ struct ReadModifyWriteResult {
|
||||
#[must_use]
|
||||
#[derive(Debug)]
|
||||
struct CompareExchangeResult {
|
||||
/// If `true`, exploration should be dropped, **and all other fields are invalid**.
|
||||
invalid: bool,
|
||||
/// If there was an error, it will be stored in `error`, otherwise it is `None`.
|
||||
error: UniquePtr<CxxString>,
|
||||
/// The value that was read by the compare-exchange.
|
||||
@@ -258,6 +264,8 @@ struct CompareExchangeResult {
|
||||
#[must_use]
|
||||
#[derive(Debug)]
|
||||
struct MutexLockResult {
|
||||
/// If `true`, exploration should be dropped, **and all other fields are invalid**.
|
||||
invalid: bool,
|
||||
/// If there was an error, it will be stored in `error`, otherwise it is `None`.
|
||||
error: UniquePtr<CxxString>,
|
||||
/// If true, GenMC determined that we should retry the mutex lock operation once the thread attempting to lock is scheduled again.
|
||||
@@ -266,6 +274,15 @@ struct MutexLockResult {
|
||||
is_lock_acquired: bool,
|
||||
}
|
||||
|
||||
#[must_use]
|
||||
#[derive(Debug)]
|
||||
struct MallocResult {
|
||||
/// If not null, contains the error encountered during the handling of malloc.
|
||||
error: UniquePtr<CxxString>,
|
||||
/// The allocated address.
|
||||
address: u64,
|
||||
}
|
||||
|
||||
/**** These are GenMC types that we have to copy-paste here since cxx does not support
|
||||
"importing" externally defined C++ types. ****/
|
||||
|
||||
@@ -385,7 +402,7 @@ unsafe fn create_handle(
|
||||
/***** Functions for handling events encountered during program execution. *****/
|
||||
|
||||
/**** Memory access handling ****/
|
||||
fn handle_load(
|
||||
fn handle_atomic_load(
|
||||
self: Pin<&mut MiriGenmcShim>,
|
||||
thread_id: i32,
|
||||
address: u64,
|
||||
@@ -393,6 +410,12 @@ fn handle_load(
|
||||
memory_ordering: MemOrdering,
|
||||
old_value: GenmcScalar,
|
||||
) -> LoadResult;
|
||||
fn handle_non_atomic_load(
|
||||
self: Pin<&mut MiriGenmcShim>,
|
||||
thread_id: i32,
|
||||
address: u64,
|
||||
size: u64,
|
||||
) -> LoadResult;
|
||||
fn handle_read_modify_write(
|
||||
self: Pin<&mut MiriGenmcShim>,
|
||||
thread_id: i32,
|
||||
@@ -415,7 +438,7 @@ fn handle_compare_exchange(
|
||||
fail_load_ordering: MemOrdering,
|
||||
can_fail_spuriously: bool,
|
||||
) -> CompareExchangeResult;
|
||||
fn handle_store(
|
||||
fn handle_atomic_store(
|
||||
self: Pin<&mut MiriGenmcShim>,
|
||||
thread_id: i32,
|
||||
address: u64,
|
||||
@@ -424,6 +447,12 @@ fn handle_store(
|
||||
old_value: GenmcScalar,
|
||||
memory_ordering: MemOrdering,
|
||||
) -> StoreResult;
|
||||
fn handle_non_atomic_store(
|
||||
self: Pin<&mut MiriGenmcShim>,
|
||||
thread_id: i32,
|
||||
address: u64,
|
||||
size: u64,
|
||||
) -> StoreResult;
|
||||
fn handle_fence(
|
||||
self: Pin<&mut MiriGenmcShim>,
|
||||
thread_id: i32,
|
||||
@@ -436,7 +465,7 @@ fn handle_malloc(
|
||||
thread_id: i32,
|
||||
size: u64,
|
||||
alignment: u64,
|
||||
) -> u64;
|
||||
) -> MallocResult;
|
||||
/// Returns true if an error was found.
|
||||
fn handle_free(
|
||||
self: Pin<&mut MiriGenmcShim>,
|
||||
|
||||
@@ -1 +1 @@
|
||||
4c4205163abcbd08948b3efab796c543ba1ea687
|
||||
e22c616e4e87914135c1db261a03e0437255335e
|
||||
|
||||
@@ -170,7 +170,9 @@ fn addr_from_alloc_id_uncached(
|
||||
{
|
||||
let fn_sig = this.tcx.instantiate_bound_regions_with_erased(
|
||||
this.tcx
|
||||
.fn_sig(instance.def_id()).instantiate(*this.tcx, instance.args).skip_norm_wip(),
|
||||
.fn_sig(instance.def_id())
|
||||
.instantiate(*this.tcx, instance.args)
|
||||
.skip_norm_wip(),
|
||||
);
|
||||
let fn_ptr = crate::shims::native_lib::build_libffi_closure(this, fn_sig)?;
|
||||
|
||||
|
||||
@@ -4,7 +4,6 @@
|
||||
use rustc_middle::mir;
|
||||
use rustc_middle::mir::interpret;
|
||||
use rustc_middle::ty::ScalarInt;
|
||||
use tracing::debug;
|
||||
|
||||
use super::GenmcScalar;
|
||||
use crate::alloc_addresses::EvalContextExt as _;
|
||||
@@ -13,33 +12,6 @@
|
||||
|
||||
/// Maximum size memory access in bytes that GenMC supports.
|
||||
pub(super) const MAX_ACCESS_SIZE: u64 = 8;
|
||||
|
||||
/// This function is used to split up a large memory access into aligned, non-overlapping chunks of a limited size.
|
||||
/// Returns an iterator over the chunks, yielding `(base address, size)` of each chunk, ordered by address.
|
||||
pub fn split_access(address: Size, size: Size) -> impl Iterator<Item = (u64, u64)> {
|
||||
let start_address = address.bytes();
|
||||
let end_address = start_address + size.bytes();
|
||||
|
||||
let start_address_aligned = start_address.next_multiple_of(MAX_ACCESS_SIZE);
|
||||
let end_address_aligned = (end_address / MAX_ACCESS_SIZE) * MAX_ACCESS_SIZE; // prev_multiple_of
|
||||
|
||||
debug!(
|
||||
"GenMC: splitting NA memory access into {MAX_ACCESS_SIZE} byte chunks: {}B + {} * {MAX_ACCESS_SIZE}B + {}B = {size:?}",
|
||||
start_address_aligned - start_address,
|
||||
(end_address_aligned - start_address_aligned) / MAX_ACCESS_SIZE,
|
||||
end_address - end_address_aligned,
|
||||
);
|
||||
|
||||
// FIXME(genmc): could make remaining accesses powers-of-2, instead of 1 byte.
|
||||
let start_chunks = (start_address..start_address_aligned).map(|address| (address, 1));
|
||||
let aligned_chunks = (start_address_aligned..end_address_aligned)
|
||||
.step_by(MAX_ACCESS_SIZE.try_into().unwrap())
|
||||
.map(|address| (address, MAX_ACCESS_SIZE));
|
||||
let end_chunks = (end_address_aligned..end_address).map(|address| (address, 1));
|
||||
|
||||
start_chunks.chain(aligned_chunks).chain(end_chunks)
|
||||
}
|
||||
|
||||
/// Inverse function to `scalar_to_genmc_scalar`.
|
||||
///
|
||||
/// Convert a Miri `Scalar` to a `GenmcScalar`.
|
||||
|
||||
@@ -19,7 +19,6 @@
|
||||
};
|
||||
use self::run::GenmcMode;
|
||||
use self::thread_id_map::ThreadIdMap;
|
||||
use crate::concurrency::genmc::helper::split_access;
|
||||
use crate::diagnostics::SpanDedupDiagnostic;
|
||||
use crate::intrinsics::AtomicRmwOp;
|
||||
use crate::*;
|
||||
@@ -267,8 +266,13 @@ pub(crate) fn atomic_load<'tcx>(
|
||||
} else {
|
||||
GenmcScalar::UNINIT
|
||||
};
|
||||
let read_value =
|
||||
self.handle_load(&ecx.machine, address, size, ordering.to_genmc(), genmc_old_value)?;
|
||||
let read_value = self.handle_atomic_load(
|
||||
&ecx.machine,
|
||||
address,
|
||||
size,
|
||||
ordering.to_genmc(),
|
||||
genmc_old_value,
|
||||
)?;
|
||||
genmc_scalar_to_scalar(ecx, self, read_value, size)
|
||||
}
|
||||
|
||||
@@ -292,7 +296,7 @@ pub(crate) fn atomic_store<'tcx>(
|
||||
} else {
|
||||
GenmcScalar::UNINIT
|
||||
};
|
||||
self.handle_store(
|
||||
self.handle_atomic_store(
|
||||
&ecx.machine,
|
||||
address,
|
||||
size,
|
||||
@@ -447,6 +451,9 @@ pub(crate) fn atomic_compare_exchange<'tcx>(
|
||||
can_fail_spuriously,
|
||||
);
|
||||
|
||||
if cas_result.invalid {
|
||||
throw_machine_stop!(TerminationInfo::GenmcSkip);
|
||||
}
|
||||
if let Some(error) = cas_result.error.as_ref() {
|
||||
// FIXME(genmc): error handling
|
||||
throw_ub_format!("{}", error.to_string_lossy());
|
||||
@@ -488,32 +495,7 @@ pub(crate) fn memory_load<'tcx>(
|
||||
return interp_ok(());
|
||||
}
|
||||
|
||||
let handle_load = |address, size| {
|
||||
// NOTE: Values loaded non-atomically are still handled by Miri, so we discard whatever we get from GenMC
|
||||
let _read_value = self.handle_load(
|
||||
machine,
|
||||
address,
|
||||
size,
|
||||
MemOrdering::NotAtomic,
|
||||
// This value is used to update the co-maximal store event to the same location.
|
||||
// We don't need to update that store, since if it is ever read by any atomic loads, the value will be updated then.
|
||||
// We use uninit for lack of a better value, since we don't know whether the location we currently load from is initialized or not.
|
||||
GenmcScalar::UNINIT,
|
||||
)?;
|
||||
interp_ok(())
|
||||
};
|
||||
|
||||
// This load is small enough so GenMC can handle it.
|
||||
if size.bytes() <= MAX_ACCESS_SIZE {
|
||||
return handle_load(address, size);
|
||||
}
|
||||
|
||||
// This load is too big to be a single GenMC access, we have to split it.
|
||||
// FIXME(genmc): This will misbehave if there are non-64bit-atomics in there.
|
||||
// Needs proper support on the GenMC side for large and mixed atomic accesses.
|
||||
for (address, size) in split_access(address, size) {
|
||||
handle_load(Size::from_bytes(address), Size::from_bytes(size))?;
|
||||
}
|
||||
self.handle_non_atomic_load(machine, address, size)?;
|
||||
interp_ok(())
|
||||
}
|
||||
|
||||
@@ -540,40 +522,7 @@ pub(crate) fn memory_store<'tcx>(
|
||||
return interp_ok(());
|
||||
}
|
||||
|
||||
let handle_store = |address, size| {
|
||||
// We always write the the stored values to Miri's memory, whether GenMC says the write is co-maximal or not.
|
||||
// The GenMC scheduler ensures that replaying an execution happens in porf-respecting order (po := program order, rf: reads-from order).
|
||||
// This means that for any non-atomic read Miri performs, the corresponding write has already been replayed.
|
||||
let _is_co_max_write = self.handle_store(
|
||||
machine,
|
||||
address,
|
||||
size,
|
||||
// We don't know the value that this store will write, but GenMC expects that we give it an actual value.
|
||||
// Unfortunately, there are situations where this value can actually become visible
|
||||
// to the program: when there is an atomic load reading from a non-atomic store.
|
||||
// FIXME(genmc): update once mixed atomic-non-atomic support is added. Afterwards, this value should never be readable.
|
||||
GenmcScalar::from_u64(0xDEADBEEF),
|
||||
// This value is used to update the co-maximal store event to the same location.
|
||||
// This old value cannot be read anymore by any future loads, since we are doing another non-atomic store to the same location.
|
||||
// Any future load will either see the store we are adding now, or we have a data race (there can only be one possible non-atomic value to read from at any time).
|
||||
// We use uninit for lack of a better value, since we don't know whether the location we currently write to is initialized or not.
|
||||
GenmcScalar::UNINIT,
|
||||
MemOrdering::NotAtomic,
|
||||
)?;
|
||||
interp_ok(())
|
||||
};
|
||||
|
||||
// This store is small enough so GenMC can handle it.
|
||||
if size.bytes() <= MAX_ACCESS_SIZE {
|
||||
return handle_store(address, size);
|
||||
}
|
||||
|
||||
// This store is too big to be a single GenMC access, we have to split it.
|
||||
// FIXME(genmc): This will misbehave if there are non-64bit-atomics in there.
|
||||
// Needs proper support on the GenMC side for large and mixed atomic accesses.
|
||||
for (address, size) in split_access(address, size) {
|
||||
handle_store(Size::from_bytes(address), Size::from_bytes(size))?;
|
||||
}
|
||||
self.handle_non_atomic_store(machine, address, size)?;
|
||||
interp_ok(())
|
||||
}
|
||||
|
||||
@@ -599,14 +548,15 @@ pub(crate) fn handle_alloc<'tcx>(
|
||||
}
|
||||
// GenMC doesn't support ZSTs, so we set the minimum size to 1 byte
|
||||
let genmc_size = size.bytes().max(1);
|
||||
let chosen_address = self.handle.borrow_mut().pin_mut().handle_malloc(
|
||||
let malloc_result = self.handle.borrow_mut().pin_mut().handle_malloc(
|
||||
self.active_thread_genmc_tid(machine),
|
||||
genmc_size,
|
||||
alignment.bytes(),
|
||||
);
|
||||
if chosen_address == 0 {
|
||||
if let Some(_error) = malloc_result.error.as_ref() {
|
||||
throw_exhaust!(AddressSpaceFull);
|
||||
}
|
||||
let chosen_address = malloc_result.address;
|
||||
|
||||
// Non-global addresses should not be in the global address space.
|
||||
assert_eq!(0, chosen_address & GENMC_GLOBAL_ADDRESSES_MASK);
|
||||
@@ -735,9 +685,9 @@ pub(crate) fn handle_exit<'tcx>(
|
||||
}
|
||||
|
||||
impl GenmcCtx {
|
||||
/// Inform GenMC about a load (atomic or non-atomic).
|
||||
/// Inform GenMC about an atomic load.
|
||||
/// Returns the value that GenMC wants this load to read.
|
||||
fn handle_load<'tcx>(
|
||||
fn handle_atomic_load<'tcx>(
|
||||
&self,
|
||||
machine: &MiriMachine<'tcx>,
|
||||
address: Size,
|
||||
@@ -758,7 +708,7 @@ fn handle_load<'tcx>(
|
||||
"GenMC: load, address: {addr} == {addr:#x}, size: {size:?}, ordering: {memory_ordering:?}, old_value: {genmc_old_value:x?}",
|
||||
addr = address.bytes()
|
||||
);
|
||||
let load_result = self.handle.borrow_mut().pin_mut().handle_load(
|
||||
let load_result = self.handle.borrow_mut().pin_mut().handle_atomic_load(
|
||||
self.active_thread_genmc_tid(machine),
|
||||
address.bytes(),
|
||||
size.bytes(),
|
||||
@@ -766,23 +716,51 @@ fn handle_load<'tcx>(
|
||||
genmc_old_value,
|
||||
);
|
||||
|
||||
if load_result.invalid {
|
||||
throw_machine_stop!(TerminationInfo::GenmcSkip);
|
||||
}
|
||||
if let Some(error) = load_result.error.as_ref() {
|
||||
// FIXME(genmc): error handling
|
||||
throw_ub_format!("{}", error.to_string_lossy());
|
||||
}
|
||||
|
||||
if !load_result.has_value {
|
||||
// FIXME(GenMC): Implementing certain GenMC optimizations will lead to this.
|
||||
unimplemented!("GenMC: load returned no value.");
|
||||
}
|
||||
|
||||
debug!("GenMC: load returned value: {:?}", load_result.read_value);
|
||||
interp_ok(load_result.read_value)
|
||||
}
|
||||
|
||||
/// Inform GenMC about a store (atomic or non-atomic).
|
||||
/// Inform GenMC about a non-atomic load.
|
||||
fn handle_non_atomic_load<'tcx>(
|
||||
&self,
|
||||
machine: &MiriMachine<'tcx>,
|
||||
address: Size,
|
||||
size: Size,
|
||||
) -> InterpResult<'tcx> {
|
||||
assert!(size.bytes() != 0);
|
||||
debug!(
|
||||
"GenMC: NA load, address: {addr} == {addr:#x}, size: {size:?}",
|
||||
addr = address.bytes()
|
||||
);
|
||||
let load_result = self.handle.borrow_mut().pin_mut().handle_non_atomic_load(
|
||||
self.active_thread_genmc_tid(machine),
|
||||
address.bytes(),
|
||||
size.bytes(),
|
||||
);
|
||||
|
||||
if load_result.invalid {
|
||||
throw_machine_stop!(TerminationInfo::GenmcSkip);
|
||||
}
|
||||
if let Some(error) = load_result.error.as_ref() {
|
||||
// FIXME(genmc): error handling
|
||||
throw_ub_format!("{}", error.to_string_lossy());
|
||||
}
|
||||
// `load_result.read_value` is just a dummy for non-atomic loads. And anyway Miri doesn't
|
||||
// give us a chance to change the value here, it'll always use the one from its memory.
|
||||
interp_ok(())
|
||||
}
|
||||
|
||||
/// Inform GenMC about an atomic store.
|
||||
/// Returns true if the store is co-maximal, i.e., it should be written to Miri's memory too.
|
||||
fn handle_store<'tcx>(
|
||||
fn handle_atomic_store<'tcx>(
|
||||
&self,
|
||||
machine: &MiriMachine<'tcx>,
|
||||
address: Size,
|
||||
@@ -804,7 +782,7 @@ fn handle_store<'tcx>(
|
||||
"GenMC: store, address: {addr} = {addr:#x}, size: {size:?}, ordering {memory_ordering:?}, value: {genmc_value:?}",
|
||||
addr = address.bytes()
|
||||
);
|
||||
let store_result = self.handle.borrow_mut().pin_mut().handle_store(
|
||||
let store_result = self.handle.borrow_mut().pin_mut().handle_atomic_store(
|
||||
self.active_thread_genmc_tid(machine),
|
||||
address.bytes(),
|
||||
size.bytes(),
|
||||
@@ -813,6 +791,9 @@ fn handle_store<'tcx>(
|
||||
memory_ordering,
|
||||
);
|
||||
|
||||
if store_result.invalid {
|
||||
throw_machine_stop!(TerminationInfo::GenmcSkip);
|
||||
}
|
||||
if let Some(error) = store_result.error.as_ref() {
|
||||
// FIXME(genmc): error handling
|
||||
throw_ub_format!("{}", error.to_string_lossy());
|
||||
@@ -821,6 +802,36 @@ fn handle_store<'tcx>(
|
||||
interp_ok(store_result.is_coherence_order_maximal_write)
|
||||
}
|
||||
|
||||
/// Inform GenMC about a non-atomic store.
|
||||
fn handle_non_atomic_store<'tcx>(
|
||||
&self,
|
||||
machine: &MiriMachine<'tcx>,
|
||||
address: Size,
|
||||
size: Size,
|
||||
) -> InterpResult<'tcx> {
|
||||
assert!(size.bytes() != 0);
|
||||
debug!(
|
||||
"GenMC: NA store, address: {addr} = {addr:#x}, size: {size:?}",
|
||||
addr = address.bytes()
|
||||
);
|
||||
let store_result = self.handle.borrow_mut().pin_mut().handle_non_atomic_store(
|
||||
self.active_thread_genmc_tid(machine),
|
||||
address.bytes(),
|
||||
size.bytes(),
|
||||
);
|
||||
|
||||
if store_result.invalid {
|
||||
throw_machine_stop!(TerminationInfo::GenmcSkip);
|
||||
}
|
||||
if let Some(error) = store_result.error.as_ref() {
|
||||
// FIXME(genmc): error handling
|
||||
throw_ub_format!("{}", error.to_string_lossy());
|
||||
}
|
||||
// Miri will always write non-atomic stores to memory. Make sure GenMC agrees with that.
|
||||
assert!(store_result.is_coherence_order_maximal_write);
|
||||
interp_ok(())
|
||||
}
|
||||
|
||||
/// Inform GenMC about an atomic read-modify-write operation.
|
||||
/// This includes atomic swap (also often called "exchange"), but does *not*
|
||||
/// include compare-exchange (see `RMWBinOp` for full list of operations).
|
||||
@@ -859,6 +870,9 @@ fn handle_atomic_rmw_op<'tcx>(
|
||||
genmc_old_value,
|
||||
);
|
||||
|
||||
if rmw_result.invalid {
|
||||
throw_machine_stop!(TerminationInfo::GenmcSkip);
|
||||
}
|
||||
if let Some(error) = rmw_result.error.as_ref() {
|
||||
// FIXME(genmc): error handling
|
||||
throw_ub_format!("{}", error.to_string_lossy());
|
||||
|
||||
@@ -1,4 +1,4 @@
|
||||
use genmc_sys::{ActionKind, ExecutionState};
|
||||
use genmc_sys::{ActionKind, ExecutionStatus};
|
||||
use rustc_data_structures::either::Either;
|
||||
use rustc_middle::mir::TerminatorKind;
|
||||
use rustc_middle::ty::{self, Ty};
|
||||
@@ -117,9 +117,9 @@ pub(crate) fn schedule_thread<'tcx>(
|
||||
|
||||
let result = self.handle.borrow_mut().pin_mut().schedule_next(genmc_tid, atomic_kind);
|
||||
// Depending on the exec_state, we either schedule the given thread, or we are finished with this execution.
|
||||
match result.exec_state {
|
||||
ExecutionState::Ok => interp_ok(Some(thread_infos.get_miri_tid(result.next_thread))),
|
||||
ExecutionState::Blocked => {
|
||||
match result.exec_status {
|
||||
ExecutionStatus::Ok => interp_ok(Some(thread_infos.get_miri_tid(result.next_thread))),
|
||||
ExecutionStatus::Blocked => {
|
||||
// This execution doesn't need further exploration. We treat this as "success, no
|
||||
// leak check needed", which makes it a NOP in the big outer loop.
|
||||
throw_machine_stop!(TerminationInfo::Exit {
|
||||
@@ -127,7 +127,7 @@ pub(crate) fn schedule_thread<'tcx>(
|
||||
leak_check: false,
|
||||
});
|
||||
}
|
||||
ExecutionState::Finished => {
|
||||
ExecutionStatus::Finished => {
|
||||
let exit_status = self.exec_state.exit_status.get().expect(
|
||||
"If the execution is finished, we should have a return value from the program.",
|
||||
);
|
||||
@@ -136,7 +136,7 @@ pub(crate) fn schedule_thread<'tcx>(
|
||||
leak_check: matches!(exit_status.exit_type, super::ExitType::MainThreadFinish),
|
||||
});
|
||||
}
|
||||
ExecutionState::Error => {
|
||||
ExecutionStatus::Error => {
|
||||
// GenMC found an error in one of the `handle_*` functions, but didn't return the detected error from the function immediately.
|
||||
// This is still an bug in the user program, so we print the error string.
|
||||
panic!(
|
||||
|
||||
@@ -96,10 +96,7 @@ fn get_or<E>(&self, k: K, vacant: impl FnOnce() -> Result<V, E>) -> Result<&V, E
|
||||
|
||||
/// Read-only lookup (avoid read-acquiring the RefCell).
|
||||
fn get(&self, k: K) -> Option<&V> {
|
||||
let val: *const V = match self.0.borrow().get(&k) {
|
||||
Some(v) => &**v,
|
||||
None => return None,
|
||||
};
|
||||
let val: *const V = &**self.0.borrow().get(&k)?;
|
||||
// This is safe because `val` points into a `Box`, that we know will not move and
|
||||
// will also not be dropped as long as the shared reference `self` is live.
|
||||
unsafe { Some(&*val) }
|
||||
|
||||
@@ -18,7 +18,7 @@ pub enum TerminationInfo {
|
||||
leak_check: bool,
|
||||
},
|
||||
Abort(String),
|
||||
/// Miri was interrupted by a Ctrl+C from the user
|
||||
/// Miri was interrupted by a Ctrl+C from the user.
|
||||
Interrupted,
|
||||
UnsupportedInIsolation(String),
|
||||
StackedBorrowsUb {
|
||||
@@ -32,6 +32,8 @@ pub enum TerminationInfo {
|
||||
history: tree_diagnostics::HistoryData,
|
||||
},
|
||||
Int2PtrWithStrictProvenance,
|
||||
/// GenMC determined that the execution should stop.
|
||||
GenmcSkip,
|
||||
/// All threads are blocked.
|
||||
GlobalDeadlock,
|
||||
/// Some thread discovered a deadlock condition (e.g. in a mutex with reentrancy checking).
|
||||
@@ -81,6 +83,7 @@ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||
TreeBorrowsUb { title, .. } => write!(f, "{title}"),
|
||||
GlobalDeadlock => write!(f, "the evaluated program deadlocked"),
|
||||
LocalDeadlock => write!(f, "a thread deadlocked"),
|
||||
GenmcSkip => write!(f, "GenMC wants to skip this execution"),
|
||||
MultipleSymbolDefinitions { link_name, .. } =>
|
||||
write!(f, "multiple definitions of symbol `{link_name}`"),
|
||||
SymbolShimClashing { link_name, .. } =>
|
||||
@@ -240,6 +243,10 @@ pub fn report_result<'tcx>(
|
||||
Some("unsupported operation"),
|
||||
StackedBorrowsUb { .. } | TreeBorrowsUb { .. } | DataRace { .. } =>
|
||||
Some("Undefined Behavior"),
|
||||
GenmcSkip => {
|
||||
assert!(ecx.machine.data_race.as_genmc_ref().is_some());
|
||||
return Some((0, false));
|
||||
}
|
||||
LocalDeadlock => {
|
||||
labels.push(format!("thread got stuck here"));
|
||||
None
|
||||
|
||||
@@ -21,6 +21,10 @@ fn visit_provenance(&self, _visit: &mut VisitWith<'_>) {}
|
||||
}
|
||||
no_provenance!(i8 i16 i32 i64 isize u8 u16 u32 u64 usize bool ThreadId);
|
||||
|
||||
impl VisitProvenance for &'static str {
|
||||
fn visit_provenance(&self, _visit: &mut VisitWith<'_>) {}
|
||||
}
|
||||
|
||||
impl<T: VisitProvenance> VisitProvenance for Option<T> {
|
||||
fn visit_provenance(&self, visit: &mut VisitWith<'_>) {
|
||||
if let Some(x) = self {
|
||||
|
||||
@@ -62,6 +62,20 @@ fn flock<'tcx>(
|
||||
throw_unsup_format!("cannot flock {}", self.name());
|
||||
}
|
||||
|
||||
/// Modifies device parameters.
|
||||
/// `op` is the device-dependent operation code. It's either a `c_long` or `c_int`, depending on
|
||||
/// the target and whether it uses glibc or musl.
|
||||
/// `arg` is the optional third argument which exists depending on the operation code. It's either
|
||||
/// an integer or a pointer.
|
||||
fn ioctl<'tcx>(
|
||||
&self,
|
||||
_op: Scalar,
|
||||
_arg: Option<&OpTy<'tcx>>,
|
||||
_ecx: &mut MiriInterpCx<'tcx>,
|
||||
) -> InterpResult<'tcx, i32> {
|
||||
throw_unsup_format!("cannot use ioctl on {}", self.name());
|
||||
}
|
||||
|
||||
/// Return which epoll events are currently active.
|
||||
fn epoll_active_events<'tcx>(&self) -> InterpResult<'tcx, EpollEvents> {
|
||||
throw_unsup_format!("{}: epoll does not support this file description", self.name());
|
||||
@@ -129,6 +143,39 @@ fn flock(&mut self, fd_num: i32, op: i32) -> InterpResult<'tcx, Scalar> {
|
||||
interp_ok(Scalar::from_i32(this.try_unwrap_io_result(result)?))
|
||||
}
|
||||
|
||||
fn ioctl(
|
||||
&mut self,
|
||||
fd: &OpTy<'tcx>,
|
||||
op: &OpTy<'tcx>,
|
||||
varargs: &[OpTy<'tcx>],
|
||||
) -> InterpResult<'tcx, Scalar> {
|
||||
let this = self.eval_context_mut();
|
||||
|
||||
let fd = this.read_scalar(fd)?.to_i32()?;
|
||||
let op = this.read_scalar(op)?;
|
||||
// There is at most one relevant variadic argument.
|
||||
// It exists depending on the device and the opcode and thus we can't
|
||||
// use `check_min_vararg_count` here.
|
||||
let arg = varargs.first();
|
||||
|
||||
let Some(fd) = this.machine.fds.get(fd) else {
|
||||
return this.set_last_error_and_return_i32(LibcError("EBADF"));
|
||||
};
|
||||
|
||||
// Handle common opcodes.
|
||||
let fioclex = this.eval_libc("FIOCLEX");
|
||||
let fionclex = this.eval_libc("FIONCLEX");
|
||||
if op == fioclex || op == fionclex {
|
||||
// Since we don't support `exec`, those are NOPs.
|
||||
return interp_ok(Scalar::from_i32(0));
|
||||
}
|
||||
|
||||
// Since some ioctl operations use the return value as an output parameter, we cannot strictly use the convention of
|
||||
// zero indicating success and -1 indicating an error.
|
||||
let return_value = fd.as_unix(this).ioctl(op, arg, this)?;
|
||||
interp_ok(Scalar::from_i32(return_value))
|
||||
}
|
||||
|
||||
fn fcntl(
|
||||
&mut self,
|
||||
fd_num: &OpTy<'tcx>,
|
||||
|
||||
@@ -307,6 +307,12 @@ fn emulate_foreign_item_inner(
|
||||
let result = this.flock(fd, op)?;
|
||||
this.write_scalar(result, dest)?;
|
||||
}
|
||||
"ioctl" => {
|
||||
let ([fd, op], varargs) =
|
||||
this.check_shim_sig_variadic_lenient(abi, CanonAbi::C, link_name, args)?;
|
||||
let result = this.ioctl(fd, op, varargs)?;
|
||||
this.write_scalar(result, dest)?;
|
||||
}
|
||||
|
||||
// File and file system access
|
||||
"open" => {
|
||||
@@ -658,8 +664,7 @@ fn emulate_foreign_item_inner(
|
||||
abi,
|
||||
args,
|
||||
)?;
|
||||
let result = this.getpeername(socket, address, address_len)?;
|
||||
this.write_scalar(result, dest)?;
|
||||
this.getpeername(socket, address, address_len, dest)?;
|
||||
}
|
||||
|
||||
// Time
|
||||
|
||||
@@ -80,12 +80,6 @@ fn emulate_foreign_item_inner(
|
||||
let result = this.realpath(path, resolved_path)?;
|
||||
this.write_scalar(result, dest)?;
|
||||
}
|
||||
"ioctl" => {
|
||||
let ([fd_num, cmd], varargs) =
|
||||
this.check_shim_sig_variadic_lenient(abi, CanonAbi::C, link_name, args)?;
|
||||
let result = this.ioctl(fd_num, cmd, varargs)?;
|
||||
this.write_scalar(result, dest)?;
|
||||
}
|
||||
|
||||
// Environment related shims
|
||||
"_NSGetEnviron" => {
|
||||
@@ -341,30 +335,4 @@ fn emulate_foreign_item_inner(
|
||||
|
||||
interp_ok(EmulateItemResult::NeedsReturn)
|
||||
}
|
||||
|
||||
fn ioctl(
|
||||
&mut self,
|
||||
fd_num: &OpTy<'tcx>,
|
||||
cmd: &OpTy<'tcx>,
|
||||
_varargs: &[OpTy<'tcx>],
|
||||
) -> InterpResult<'tcx, Scalar> {
|
||||
let this = self.eval_context_mut();
|
||||
|
||||
let fioclex = this.eval_libc_u64("FIOCLEX");
|
||||
|
||||
let fd_num = this.read_scalar(fd_num)?.to_i32()?;
|
||||
let cmd = this.read_scalar(cmd)?.to_u64()?;
|
||||
|
||||
if cmd == fioclex {
|
||||
// Since we don't support `exec`, this is a NOP. However, we want to
|
||||
// return EBADF if the FD is invalid.
|
||||
if this.machine.fds.is_fd_num(fd_num) {
|
||||
interp_ok(Scalar::from_i32(0))
|
||||
} else {
|
||||
this.set_last_error_and_return_i32(LibcError("EBADF"))
|
||||
}
|
||||
} else {
|
||||
throw_unsup_format!("ioctl: unsupported command {cmd:#x}");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,6 +1,7 @@
|
||||
use std::cell::{Cell, RefCell};
|
||||
use std::io::Read;
|
||||
use std::net::{Ipv4Addr, Ipv6Addr, SocketAddr, SocketAddrV4, SocketAddrV6};
|
||||
use std::time::Duration;
|
||||
use std::{io, iter};
|
||||
|
||||
use mio::Interest;
|
||||
@@ -12,8 +13,10 @@
|
||||
use rustc_middle::throw_unsup_format;
|
||||
use rustc_target::spec::Os;
|
||||
|
||||
use crate::concurrency::blocking_io::InterestReceiver;
|
||||
use crate::shims::files::{EvalContextExt as _, FdId, FileDescription, FileDescriptionRef};
|
||||
use crate::{OpTy, Scalar, *};
|
||||
use crate::shims::unix::UnixFileDescription;
|
||||
use crate::*;
|
||||
|
||||
#[derive(Debug, PartialEq)]
|
||||
enum SocketFamily {
|
||||
@@ -23,22 +26,6 @@ enum SocketFamily {
|
||||
IPv6,
|
||||
}
|
||||
|
||||
enum SocketIoError {
|
||||
/// The socket is not yet ready. Either EINPROGRESS or ENOTCONNECTED occurred.
|
||||
NotReady,
|
||||
/// Any other kind of I/O error.
|
||||
Other(io::Error),
|
||||
}
|
||||
|
||||
impl From<io::Error> for SocketIoError {
|
||||
fn from(value: io::Error) -> Self {
|
||||
match value.kind() {
|
||||
io::ErrorKind::InProgress | io::ErrorKind::NotConnected => Self::NotReady,
|
||||
_ => Self::Other(value),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug)]
|
||||
enum SocketState {
|
||||
/// No syscall after `socket` has been made.
|
||||
@@ -61,59 +48,6 @@ enum SocketState {
|
||||
Connected(TcpStream),
|
||||
}
|
||||
|
||||
impl SocketState {
|
||||
/// If the socket is currently in [`SocketState::Connecting`], try to ensure
|
||||
/// that the connection is established by first checking that [`TcpStream::take_error`]
|
||||
/// doesn't return an error and then by checking that [`TcpStream::peer_addr`]
|
||||
/// returns the address of the connected peer.
|
||||
///
|
||||
/// If the connection is established or the socket is in any other state,
|
||||
/// [`Ok`] is returned.
|
||||
///
|
||||
/// **Important**: On Windows hosts this function can only be used to ensure a socket is connected
|
||||
/// _after_ a [`Interest::WRITABLE`] event was received.
|
||||
pub fn try_set_connected(&mut self) -> Result<(), SocketIoError> {
|
||||
// Further explanation of the limitation on Windows hosts:
|
||||
// Windows treats sockets which are connecting as connected until either the connection timeout hits
|
||||
// or an error occurs. Thus, the [`TcpStream::peer_addr`] method returns [`Ok`] with the provided peer
|
||||
// address even when the connection might not yet be established.
|
||||
|
||||
let SocketState::Connecting(stream) = self else { return Ok(()) };
|
||||
|
||||
if let Ok(Some(e)) = stream.take_error() {
|
||||
// There was an error whilst connecting.
|
||||
let e = SocketIoError::from(e);
|
||||
// We won't get EINPROGRESS or ENOTCONNECTED here
|
||||
// so we need to reset the state.
|
||||
assert!(matches!(e, SocketIoError::Other(_)));
|
||||
// Go back to initial state as the only way of getting into the
|
||||
// `Connecting` state is from the `Initial` state.
|
||||
*self = SocketState::Initial;
|
||||
return Err(e);
|
||||
}
|
||||
|
||||
if let Err(e) = stream.peer_addr() {
|
||||
let e = SocketIoError::from(e);
|
||||
if let SocketIoError::Other(_) = &e {
|
||||
// All other errors are fatal for a socket and thus the state needs to be reset.
|
||||
*self = SocketState::Initial;
|
||||
}
|
||||
return Err(e);
|
||||
};
|
||||
|
||||
// We just read the peer address without an error so we can be
|
||||
// sure that the connection is established.
|
||||
|
||||
// Temporarily use dummy state to take ownership of the stream.
|
||||
let SocketState::Connecting(stream) = std::mem::replace(self, SocketState::Initial) else {
|
||||
// At the start of the function we ensured that we're currently connecting.
|
||||
unreachable!()
|
||||
};
|
||||
*self = SocketState::Connected(stream);
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug)]
|
||||
struct Socket {
|
||||
/// Family of the socket, used to ensure socket only binds/connects to address of
|
||||
@@ -151,17 +85,40 @@ fn read<'tcx>(
|
||||
) -> InterpResult<'tcx> {
|
||||
assert!(communicate_allowed, "cannot have `Socket` with isolation enabled!");
|
||||
|
||||
if !matches!(&*self.state.borrow(), SocketState::Connected(_)) {
|
||||
// We can only receive from connected sockets. For all other
|
||||
// states we return a not connected error.
|
||||
return finish.call(ecx, Err(LibcError("ENOTCONN")));
|
||||
}
|
||||
let socket = self;
|
||||
|
||||
// Since `read` is the same as `recv` with no flags, we just treat
|
||||
// the `read` as a `recv` here.
|
||||
ecx.block_for_recv(self, ptr, len, /* should_peek */ false, finish);
|
||||
ecx.ensure_connected(
|
||||
socket.clone(),
|
||||
!socket.is_non_block.get(),
|
||||
"read",
|
||||
callback!(
|
||||
@capture<'tcx> {
|
||||
socket: FileDescriptionRef<Socket>,
|
||||
ptr: Pointer,
|
||||
len: usize,
|
||||
finish: DynMachineCallback<'tcx, Result<usize, IoError>>,
|
||||
} |this, result: Result<(), ()>| {
|
||||
if result.is_err() {
|
||||
return finish.call(this, Err(LibcError("ENOTCONN")))
|
||||
}
|
||||
|
||||
interp_ok(())
|
||||
// Since `read` is the same as `recv` with no flags, we just treat
|
||||
// the `read` as a `recv` here.
|
||||
|
||||
if socket.is_non_block.get() {
|
||||
// We have a non-blocking socket and thus don't want to block until
|
||||
// we can read.
|
||||
let result = this.try_non_block_recv(&socket, ptr, len, /* should_peek */ false)?;
|
||||
finish.call(this, result)
|
||||
} else {
|
||||
// The socket is in blocking mode and thus the read call should block
|
||||
// until we can read some bytes from the socket.
|
||||
this.block_for_recv(socket, ptr, len, /* should_peek */ false, finish);
|
||||
interp_ok(())
|
||||
}
|
||||
}
|
||||
),
|
||||
)
|
||||
}
|
||||
|
||||
fn write<'tcx>(
|
||||
@@ -174,17 +131,40 @@ fn write<'tcx>(
|
||||
) -> InterpResult<'tcx> {
|
||||
assert!(communicate_allowed, "cannot have `Socket` with isolation enabled!");
|
||||
|
||||
if !matches!(&*self.state.borrow(), SocketState::Connected(_)) {
|
||||
// We can only send with connected sockets. For all other
|
||||
// states we return a not connected error.
|
||||
return finish.call(ecx, Err(LibcError("ENOTCONN")));
|
||||
}
|
||||
let socket = self;
|
||||
|
||||
// Since `write` is the same as `send` with no flags, we just treat
|
||||
// the `write` as a `send` here.
|
||||
ecx.block_for_send(self, ptr, len, finish);
|
||||
ecx.ensure_connected(
|
||||
socket.clone(),
|
||||
!socket.is_non_block.get(),
|
||||
"write",
|
||||
callback!(
|
||||
@capture<'tcx> {
|
||||
socket: FileDescriptionRef<Socket>,
|
||||
ptr: Pointer,
|
||||
len: usize,
|
||||
finish: DynMachineCallback<'tcx, Result<usize, IoError>>
|
||||
} |this, result: Result<(), ()>| {
|
||||
if result.is_err() {
|
||||
return finish.call(this, Err(LibcError("ENOTCONN")))
|
||||
}
|
||||
|
||||
interp_ok(())
|
||||
// Since `write` is the same as `send` with no flags, we just treat
|
||||
// the `write` as a `send` here.
|
||||
|
||||
if socket.is_non_block.get() {
|
||||
// We have a non-blocking socket and thus don't want to block until
|
||||
// we can write.
|
||||
let result = this.try_non_block_send(&socket, ptr, len)?;
|
||||
return finish.call(this, result)
|
||||
} else {
|
||||
// The socket is in blocking mode and thus the write call should block
|
||||
// until we can write some bytes into the socket.
|
||||
this.block_for_send(socket, ptr, len, finish);
|
||||
interp_ok(())
|
||||
}
|
||||
}
|
||||
),
|
||||
)
|
||||
}
|
||||
|
||||
fn short_fd_operations(&self) -> bool {
|
||||
@@ -192,6 +172,10 @@ fn short_fd_operations(&self) -> bool {
|
||||
true
|
||||
}
|
||||
|
||||
fn as_unix<'tcx>(&self, _ecx: &MiriInterpCx<'tcx>) -> &dyn UnixFileDescription {
|
||||
self
|
||||
}
|
||||
|
||||
fn get_flags<'tcx>(&self, ecx: &mut MiriInterpCx<'tcx>) -> InterpResult<'tcx, Scalar> {
|
||||
let mut flags = ecx.eval_libc_i32("O_RDWR");
|
||||
|
||||
@@ -204,10 +188,64 @@ fn get_flags<'tcx>(&self, ecx: &mut MiriInterpCx<'tcx>) -> InterpResult<'tcx, Sc
|
||||
|
||||
fn set_flags<'tcx>(
|
||||
&self,
|
||||
mut _flag: i32,
|
||||
_ecx: &mut MiriInterpCx<'tcx>,
|
||||
mut flag: i32,
|
||||
ecx: &mut MiriInterpCx<'tcx>,
|
||||
) -> InterpResult<'tcx, Scalar> {
|
||||
throw_unsup_format!("fcntl: socket flags aren't supported")
|
||||
let o_nonblock = ecx.eval_libc_i32("O_NONBLOCK");
|
||||
|
||||
// O_NONBLOCK flag can be set / unset by user.
|
||||
if flag & o_nonblock == o_nonblock {
|
||||
self.is_non_block.set(true);
|
||||
flag &= !o_nonblock;
|
||||
} else {
|
||||
self.is_non_block.set(false);
|
||||
}
|
||||
|
||||
// Throw error if there is any unsupported flag.
|
||||
if flag != 0 {
|
||||
throw_unsup_format!("fcntl: only O_NONBLOCK is supported for sockets")
|
||||
}
|
||||
|
||||
interp_ok(Scalar::from_i32(0))
|
||||
}
|
||||
}
|
||||
|
||||
impl UnixFileDescription for Socket {
|
||||
fn ioctl<'tcx>(
|
||||
&self,
|
||||
op: Scalar,
|
||||
arg: Option<&OpTy<'tcx>>,
|
||||
ecx: &mut MiriInterpCx<'tcx>,
|
||||
) -> InterpResult<'tcx, i32> {
|
||||
assert!(ecx.machine.communicate(), "cannot have `Socket` with isolation enabled!");
|
||||
|
||||
let fionbio = ecx.eval_libc("FIONBIO");
|
||||
|
||||
if op == fionbio {
|
||||
// On these OSes, Rust uses the ioctl, so we trust that it is reasonable and controls
|
||||
// the same internal flag as fcntl.
|
||||
if !matches!(ecx.tcx.sess.target.os, Os::Linux | Os::Android | Os::MacOs | Os::FreeBsd)
|
||||
{
|
||||
// FIONBIO cannot be used to change the blocking mode of a socket on solarish targets:
|
||||
// <https://github.com/rust-lang/rust/commit/dda5c97675b4f5b1f6fdab64606c8a1f21021b0a>
|
||||
// Since there might be more targets which do weird things with this option, we use
|
||||
// an allowlist instead of just denying solarish targets.
|
||||
throw_unsup_format!(
|
||||
"ioctl: setting FIONBIO on sockets is unsupported on target {}",
|
||||
ecx.tcx.sess.target.os
|
||||
);
|
||||
}
|
||||
|
||||
let Some(value_ptr) = arg else {
|
||||
throw_ub_format!("ioctl: setting FIONBIO on sockets requires a third argument");
|
||||
};
|
||||
let value = ecx.deref_pointer_as(value_ptr, ecx.machine.layouts.i32)?;
|
||||
let non_block = ecx.read_scalar(&value)?.to_i32()? != 0;
|
||||
self.is_non_block.set(non_block);
|
||||
return interp_ok(0);
|
||||
}
|
||||
|
||||
throw_unsup_format!("ioctl: unsupported operation {op:#x} on socket");
|
||||
}
|
||||
}
|
||||
|
||||
@@ -469,19 +507,35 @@ fn accept4(
|
||||
}
|
||||
|
||||
if socket.is_non_block.get() {
|
||||
throw_unsup_format!("accept4: non-blocking accept is unsupported")
|
||||
// We have a non-blocking socket and thus don't want to block until
|
||||
// we can accept an incoming connection.
|
||||
match this.try_non_block_accept(
|
||||
&socket,
|
||||
address_ptr,
|
||||
address_len_ptr,
|
||||
is_client_sock_nonblock,
|
||||
)? {
|
||||
Ok(sockfd) => {
|
||||
// We need to create the scalar using the destination size since
|
||||
// `syscall(SYS_accept4, ...)` returns a long which doesn't match
|
||||
// the int returned from the `accept`/`accept4` syscalls.
|
||||
// See <https://man7.org/linux/man-pages/man2/syscall.2.html>.
|
||||
this.write_scalar(Scalar::from_int(sockfd, dest.layout.size), dest)
|
||||
}
|
||||
Err(e) => this.set_last_error_and_return(e, dest),
|
||||
}
|
||||
} else {
|
||||
// The socket is in blocking mode and thus the accept call should block
|
||||
// until an incoming connection is ready.
|
||||
this.block_for_accept(
|
||||
socket,
|
||||
address_ptr,
|
||||
address_len_ptr,
|
||||
is_client_sock_nonblock,
|
||||
dest.clone(),
|
||||
);
|
||||
interp_ok(())
|
||||
}
|
||||
|
||||
// The socket is in blocking mode and thus the accept call should block
|
||||
// until an incoming connection is ready.
|
||||
this.block_for_accept(
|
||||
address_ptr,
|
||||
address_len_ptr,
|
||||
is_client_sock_nonblock,
|
||||
socket,
|
||||
dest.clone(),
|
||||
);
|
||||
interp_ok(())
|
||||
}
|
||||
|
||||
fn connect(
|
||||
@@ -530,22 +584,44 @@ fn connect(
|
||||
// Mio returns a potentially unconnected stream.
|
||||
// We can be ensured that the connection is established when
|
||||
// [`TcpStream::take_err`] and [`TcpStream::peer_addr`] both
|
||||
// don't return errors.
|
||||
// For non-blocking sockets we need to check that for every
|
||||
// [`Interest::WRITEABLE`] event on the stream.
|
||||
// don't return an error after receiving an [`Interest::WRITEABLE`]
|
||||
// event on the stream.
|
||||
match TcpStream::connect(address) {
|
||||
Ok(stream) => *socket.state.borrow_mut() = SocketState::Connecting(stream),
|
||||
Err(e) => return this.set_last_error_and_return(e, dest),
|
||||
};
|
||||
|
||||
if socket.is_non_block.get() {
|
||||
throw_unsup_format!("connect: non-blocking connect is unsupported");
|
||||
}
|
||||
// We have a non-blocking socket and thus don't want to block until
|
||||
// the connection is established.
|
||||
|
||||
// The socket is in blocking mode and thus the connect call should block
|
||||
// until the connection with the server is established.
|
||||
this.block_for_connect(socket, dest.clone());
|
||||
interp_ok(())
|
||||
// Since the [`TcpStream::connect`] function of mio hides the EINPROGRESS
|
||||
// we just always return EINPROGRESS and check whether the connection succeeded
|
||||
// once we want to use the connected socket.
|
||||
this.set_last_error_and_return(LibcError("EINPROGRESS"), dest)
|
||||
} else {
|
||||
// The socket is in blocking mode and thus the connect call should block
|
||||
// until the connection with the server is established.
|
||||
|
||||
let dest = dest.clone();
|
||||
|
||||
this.ensure_connected(
|
||||
socket,
|
||||
/* should_wait */ true,
|
||||
"connect",
|
||||
callback!(
|
||||
@capture<'tcx> {
|
||||
dest: MPlaceTy<'tcx>
|
||||
} |this, result: Result<(), ()>| {
|
||||
if result.is_err() {
|
||||
this.set_last_error_and_return(LibcError("ENOTCONN"), &dest)
|
||||
} else {
|
||||
this.write_scalar(Scalar::from_i32(0), &dest)
|
||||
}
|
||||
}
|
||||
),
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
fn send(
|
||||
@@ -576,12 +652,6 @@ fn send(
|
||||
return this.set_last_error_and_return(LibcError("ENOTSOCK"), dest);
|
||||
};
|
||||
|
||||
if !matches!(&*socket.state.borrow(), SocketState::Connected(_)) {
|
||||
// We can only send with connected sockets. For all other
|
||||
// states we return a not connected error.
|
||||
return this.set_last_error_and_return(LibcError("ENOTCONN"), dest);
|
||||
}
|
||||
|
||||
// Non-deterministically decide to further reduce the length, simulating a partial send.
|
||||
// We avoid reducing the write size to 0: the docs seem to be entirely fine with that,
|
||||
// but the standard library is not (https://github.com/rust-lang/rust/issues/145959).
|
||||
@@ -594,50 +664,86 @@ fn send(
|
||||
length
|
||||
};
|
||||
|
||||
let mut is_op_non_block = false;
|
||||
|
||||
// Interpret the flag. Every flag we recognize is "subtracted" from `flags`, so
|
||||
// if there is anything left at the end, that's an unsupported flag.
|
||||
if matches!(
|
||||
this.tcx.sess.target.os,
|
||||
Os::Linux | Os::Android | Os::FreeBsd | Os::Solaris | Os::Illumos
|
||||
) {
|
||||
// MSG_NOSIGNAL only exists on Linux, Android, FreeBSD,
|
||||
// MSG_NOSIGNAL and MSG_DONTWAIT only exist on Linux, Android, FreeBSD,
|
||||
// Solaris, and Illumos targets.
|
||||
let msg_nosignal = this.eval_libc_i32("MSG_NOSIGNAL");
|
||||
let msg_dontwait = this.eval_libc_i32("MSG_DONTWAIT");
|
||||
if flags & msg_nosignal == msg_nosignal {
|
||||
// This is only needed to ensure that no EPIPE signal is sent when
|
||||
// trying to send into a stream which is no longer connected.
|
||||
// Since we don't support signals, we can ignore this.
|
||||
flags &= !msg_nosignal;
|
||||
}
|
||||
if flags & msg_dontwait == msg_dontwait {
|
||||
flags &= !msg_dontwait;
|
||||
is_op_non_block = true;
|
||||
}
|
||||
}
|
||||
|
||||
if flags != 0 {
|
||||
throw_unsup_format!(
|
||||
"send: flag {flags:#x} is unsupported, only MSG_NOSIGNAL is allowed",
|
||||
"send: flag {flags:#x} is unsupported, only MSG_NOSIGNAL and MSG_DONTWAIT are allowed",
|
||||
);
|
||||
}
|
||||
|
||||
// If either the operation or the socket is non-blocking, we don't want
|
||||
// to wait until the connection is established.
|
||||
let should_wait = !is_op_non_block && !socket.is_non_block.get();
|
||||
let dest = dest.clone();
|
||||
|
||||
this.block_for_send(
|
||||
socket,
|
||||
buffer_ptr,
|
||||
length,
|
||||
callback!(@capture<'tcx> {
|
||||
dest: MPlaceTy<'tcx>
|
||||
} |this, result: Result<usize, IoError>| {
|
||||
match result {
|
||||
Ok(read_size) => {
|
||||
let read_size: u64 = read_size.try_into().unwrap();
|
||||
let ssize_layout = this.libc_ty_layout("ssize_t");
|
||||
this.write_scalar(Scalar::from_int(read_size, ssize_layout.size), &dest)
|
||||
this.ensure_connected(
|
||||
socket.clone(),
|
||||
should_wait,
|
||||
"send",
|
||||
callback!(
|
||||
@capture<'tcx> {
|
||||
socket: FileDescriptionRef<Socket>,
|
||||
flags: i32,
|
||||
buffer_ptr: Pointer,
|
||||
length: usize,
|
||||
is_op_non_block: bool,
|
||||
dest: MPlaceTy<'tcx>,
|
||||
} |this, result: Result<(), ()>| {
|
||||
if result.is_err() {
|
||||
return this.set_last_error_and_return(LibcError("ENOTCONN"), &dest)
|
||||
}
|
||||
Err(e) => this.set_last_error_and_return(e, &dest)
|
||||
}
|
||||
}),
|
||||
);
|
||||
|
||||
interp_ok(())
|
||||
if is_op_non_block || socket.is_non_block.get() {
|
||||
// We have a non-blocking operation or a non-blocking socket and
|
||||
// thus don't want to block until we can send.
|
||||
match this.try_non_block_send(&socket, buffer_ptr, length)? {
|
||||
Ok(size) => this.write_scalar(Scalar::from_target_isize(size.try_into().unwrap(), this), &dest),
|
||||
Err(e) => this.set_last_error_and_return(e, &dest),
|
||||
}
|
||||
} else {
|
||||
// The socket is in blocking mode and thus the send call should block
|
||||
// until we can send some bytes into the socket.
|
||||
this.block_for_send(
|
||||
socket,
|
||||
buffer_ptr,
|
||||
length,
|
||||
callback!(@capture<'tcx> {
|
||||
dest: MPlaceTy<'tcx>
|
||||
} |this, result: Result<usize, IoError>| {
|
||||
match result {
|
||||
Ok(size) => this.write_scalar(Scalar::from_target_isize(size.try_into().unwrap(), this), &dest),
|
||||
Err(e) => this.set_last_error_and_return(e, &dest)
|
||||
}
|
||||
}),
|
||||
);
|
||||
interp_ok(())
|
||||
}
|
||||
}
|
||||
),
|
||||
)
|
||||
}
|
||||
|
||||
fn recv(
|
||||
@@ -668,12 +774,6 @@ fn recv(
|
||||
return this.set_last_error_and_return(LibcError("ENOTSOCK"), dest);
|
||||
};
|
||||
|
||||
if !matches!(&*socket.state.borrow(), SocketState::Connected(_)) {
|
||||
// We can only receive from connected sockets. For all other
|
||||
// states we return a not connected error.
|
||||
return this.set_last_error_and_return(LibcError("ENOTCONN"), dest);
|
||||
}
|
||||
|
||||
// Non-deterministically decide to further reduce the length, simulating a partial receive.
|
||||
// We don't simulate partial receives for lengths < 2 because the man page states that a
|
||||
// return value of zero can only be returned in some special cases:
|
||||
@@ -690,6 +790,7 @@ fn recv(
|
||||
};
|
||||
|
||||
let mut should_peek = false;
|
||||
let mut is_op_non_block = false;
|
||||
|
||||
// Interpret the flag. Every flag we recognize is "subtracted" from `flags`, so
|
||||
// if there is anything left at the end, that's an unsupported flag.
|
||||
@@ -710,35 +811,77 @@ fn recv(
|
||||
}
|
||||
}
|
||||
|
||||
if matches!(
|
||||
this.tcx.sess.target.os,
|
||||
Os::Linux | Os::Android | Os::FreeBsd | Os::Solaris | Os::Illumos
|
||||
) {
|
||||
// MSG_DONTWAIT only exists on Linux, Android, FreeBSD,
|
||||
// Solaris, and Illumos targets.
|
||||
let msg_dontwait = this.eval_libc_i32("MSG_DONTWAIT");
|
||||
if flags & msg_dontwait == msg_dontwait {
|
||||
flags &= !msg_dontwait;
|
||||
is_op_non_block = true;
|
||||
}
|
||||
}
|
||||
|
||||
if flags != 0 {
|
||||
throw_unsup_format!(
|
||||
"recv: flag {flags:#x} is unsupported, only MSG_PEEK \
|
||||
"recv: flag {flags:#x} is unsupported, only MSG_PEEK, MSG_DONTWAIT \
|
||||
and MSG_CMSG_CLOEXEC are allowed",
|
||||
);
|
||||
}
|
||||
|
||||
// If either the operation or the socket is non-blocking, we don't want
|
||||
// to wait until the connection is established.
|
||||
let should_wait = !is_op_non_block && !socket.is_non_block.get();
|
||||
let dest = dest.clone();
|
||||
|
||||
this.block_for_recv(
|
||||
socket,
|
||||
buffer_ptr,
|
||||
length,
|
||||
should_peek,
|
||||
callback!(@capture<'tcx> {
|
||||
dest: MPlaceTy<'tcx>
|
||||
} |this, result: Result<usize, IoError>| {
|
||||
match result {
|
||||
Ok(read_size) => {
|
||||
let read_size: u64 = read_size.try_into().unwrap();
|
||||
let ssize_layout = this.libc_ty_layout("ssize_t");
|
||||
this.write_scalar(Scalar::from_int(read_size, ssize_layout.size), &dest)
|
||||
this.ensure_connected(
|
||||
socket.clone(),
|
||||
should_wait,
|
||||
"recv",
|
||||
callback!(
|
||||
@capture<'tcx> {
|
||||
socket: FileDescriptionRef<Socket>,
|
||||
buffer_ptr: Pointer,
|
||||
length: usize,
|
||||
should_peek: bool,
|
||||
is_op_non_block: bool,
|
||||
dest: MPlaceTy<'tcx>,
|
||||
} |this, result: Result<(), ()>| {
|
||||
if result.is_err() {
|
||||
return this.set_last_error_and_return(LibcError("ENOTCONN"), &dest)
|
||||
}
|
||||
Err(e) => this.set_last_error_and_return(e, &dest)
|
||||
}
|
||||
}),
|
||||
);
|
||||
|
||||
interp_ok(())
|
||||
if is_op_non_block || socket.is_non_block.get() {
|
||||
// We have a non-blocking operation or a non-blocking socket and
|
||||
// thus don't want to block until we can receive.
|
||||
match this.try_non_block_recv(&socket, buffer_ptr, length, should_peek)? {
|
||||
Ok(size) => this.write_scalar(Scalar::from_target_isize(size.try_into().unwrap(), this), &dest),
|
||||
Err(e) => this.set_last_error_and_return(e, &dest),
|
||||
}
|
||||
} else {
|
||||
// The socket is in blocking mode and thus the receive call should block
|
||||
// until we can receive some bytes from the socket.
|
||||
this.block_for_recv(
|
||||
socket,
|
||||
buffer_ptr,
|
||||
length,
|
||||
should_peek,
|
||||
callback!(@capture<'tcx> {
|
||||
dest: MPlaceTy<'tcx>
|
||||
} |this, result: Result<usize, IoError>| {
|
||||
match result {
|
||||
Ok(size) => this.write_scalar(Scalar::from_target_isize(size.try_into().unwrap(), this), &dest),
|
||||
Err(e) => this.set_last_error_and_return(e, &dest)
|
||||
}
|
||||
}),
|
||||
);
|
||||
interp_ok(())
|
||||
}
|
||||
}
|
||||
),
|
||||
)
|
||||
}
|
||||
|
||||
fn setsockopt(
|
||||
@@ -871,7 +1014,9 @@ fn getpeername(
|
||||
socket: &OpTy<'tcx>,
|
||||
address: &OpTy<'tcx>,
|
||||
address_len: &OpTy<'tcx>,
|
||||
) -> InterpResult<'tcx, Scalar> {
|
||||
// Location where the output scalar is written to.
|
||||
dest: &MPlaceTy<'tcx>,
|
||||
) -> InterpResult<'tcx> {
|
||||
let this = self.eval_context_mut();
|
||||
|
||||
let socket = this.read_scalar(socket)?.to_i32()?;
|
||||
@@ -880,32 +1025,56 @@ fn getpeername(
|
||||
|
||||
// Get the file handle
|
||||
let Some(fd) = this.machine.fds.get(socket) else {
|
||||
return this.set_last_error_and_return_i32(LibcError("EBADF"));
|
||||
return this.set_last_error_and_return(LibcError("EBADF"), dest);
|
||||
};
|
||||
|
||||
let Some(socket) = fd.downcast::<Socket>() else {
|
||||
// Man page specifies to return ENOTSOCK if `fd` is not a socket.
|
||||
return this.set_last_error_and_return_i32(LibcError("ENOTSOCK"));
|
||||
return this.set_last_error_and_return(LibcError("ENOTSOCK"), dest);
|
||||
};
|
||||
|
||||
assert!(this.machine.communicate(), "cannot have `Socket` with isolation enabled!");
|
||||
|
||||
let state = socket.state.borrow();
|
||||
let dest = dest.clone();
|
||||
|
||||
let SocketState::Connected(stream) = &*state else {
|
||||
// We can only read the peer address of connected sockets.
|
||||
return this.set_last_error_and_return_i32(LibcError("ENOTCONN"));
|
||||
};
|
||||
// It's only safe to call [`TcpStream::peer_addr`] after the socket is connected since
|
||||
// UNIX targets should return ENOTCONN when the connection is not yet established.
|
||||
this.ensure_connected(
|
||||
socket.clone(),
|
||||
/* should_wait */ false,
|
||||
"getpeername",
|
||||
callback!(
|
||||
@capture<'tcx> {
|
||||
socket: FileDescriptionRef<Socket>,
|
||||
address_ptr: Pointer,
|
||||
address_len_ptr: Pointer,
|
||||
dest: MPlaceTy<'tcx>,
|
||||
} |this, result: Result<(), ()>| {
|
||||
if result.is_err() {
|
||||
return this.set_last_error_and_return(LibcError("ENOTCONN"), &dest)
|
||||
};
|
||||
|
||||
let address = match stream.peer_addr() {
|
||||
Ok(address) => address,
|
||||
Err(e) => return this.set_last_error_and_return_i32(e),
|
||||
};
|
||||
let SocketState::Connected(stream) = &*socket.state.borrow() else {
|
||||
unreachable!()
|
||||
};
|
||||
|
||||
match this.write_socket_address(&address, address_ptr, address_len_ptr, "getpeername")? {
|
||||
Ok(_) => interp_ok(Scalar::from_i32(0)),
|
||||
Err(e) => this.set_last_error_and_return_i32(e),
|
||||
}
|
||||
let address = match stream.peer_addr() {
|
||||
Ok(address) => address,
|
||||
Err(e) => return this.set_last_error_and_return(e, &dest),
|
||||
};
|
||||
|
||||
match this.write_socket_address(
|
||||
&address,
|
||||
address_ptr,
|
||||
address_len_ptr,
|
||||
"getpeername",
|
||||
)? {
|
||||
Ok(_) => this.write_scalar(Scalar::from_i32(0), &dest),
|
||||
Err(e) => this.set_last_error_and_return(e, &dest),
|
||||
}
|
||||
}
|
||||
),
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1182,12 +1351,15 @@ fn write_socket_address(
|
||||
/// Block the thread until there's an incoming connection or an error occurred.
|
||||
///
|
||||
/// This recursively calls itself should the operation still block for some reason.
|
||||
///
|
||||
/// **Note**: This function is only safe to call when having previously ensured
|
||||
/// that the socket is in [`SocketState::Listening`].
|
||||
fn block_for_accept(
|
||||
&mut self,
|
||||
socket: FileDescriptionRef<Socket>,
|
||||
address_ptr: Pointer,
|
||||
address_len_ptr: Pointer,
|
||||
is_client_sock_nonblock: bool,
|
||||
socket: FileDescriptionRef<Socket>,
|
||||
dest: MPlaceTy<'tcx>,
|
||||
) {
|
||||
let this = self.eval_context_mut();
|
||||
@@ -1204,89 +1376,83 @@ fn block_for_accept(
|
||||
} |this, kind: UnblockKind| {
|
||||
assert_eq!(kind, UnblockKind::Ready);
|
||||
|
||||
let state = socket.state.borrow();
|
||||
|
||||
let SocketState::Listening(listener) = &*state else {
|
||||
// We checked that the socket is in listening state before blocking
|
||||
// and since there is no outgoing transition from that state this
|
||||
// should be unreachable.
|
||||
unreachable!()
|
||||
};
|
||||
|
||||
let (stream, addr) = match listener.accept() {
|
||||
Ok(peer) => peer,
|
||||
Err(e) if e.kind() == io::ErrorKind::WouldBlock => {
|
||||
// We need to block the thread again as it would still block.
|
||||
drop(state);
|
||||
this.block_for_accept(address_ptr, address_len_ptr, is_client_sock_nonblock, socket, dest);
|
||||
return interp_ok(())
|
||||
match this.try_non_block_accept(&socket, address_ptr, address_len_ptr, is_client_sock_nonblock)? {
|
||||
Ok(sockfd) => {
|
||||
// We need to create the scalar using the destination size since
|
||||
// `syscall(SYS_accept4, ...)` returns a long which doesn't match
|
||||
// the int returned from the `accept`/`accept4` syscalls.
|
||||
// See <https://man7.org/linux/man-pages/man2/syscall.2.html>.
|
||||
this.write_scalar(Scalar::from_int(sockfd, dest.layout.size), &dest)
|
||||
},
|
||||
Err(e) => return this.set_last_error_and_return(e, &dest),
|
||||
};
|
||||
|
||||
let family = match addr {
|
||||
SocketAddr::V4(_) => SocketFamily::IPv4,
|
||||
SocketAddr::V6(_) => SocketFamily::IPv6,
|
||||
};
|
||||
|
||||
if address_ptr != Pointer::null() {
|
||||
// We only attempt a write if the address pointer is not a null pointer.
|
||||
// If the address pointer is a null pointer the user isn't interested in the
|
||||
// address and we don't need to write anything.
|
||||
if let Err(e) = this.write_socket_address(&addr, address_ptr, address_len_ptr, "accept4")? {
|
||||
return this.set_last_error_and_return(e, &dest);
|
||||
};
|
||||
Err(IoError::HostError(e)) if e.kind() == io::ErrorKind::WouldBlock => {
|
||||
// We need to block the thread again as it would still block.
|
||||
this.block_for_accept(socket, address_ptr, address_len_ptr, is_client_sock_nonblock, dest);
|
||||
interp_ok(())
|
||||
}
|
||||
Err(e) => this.set_last_error_and_return(e, &dest),
|
||||
}
|
||||
|
||||
let fd = this.machine.fds.new_ref(Socket {
|
||||
family,
|
||||
state: RefCell::new(SocketState::Connected(stream)),
|
||||
is_non_block: Cell::new(is_client_sock_nonblock),
|
||||
});
|
||||
let sockfd = this.machine.fds.insert(fd);
|
||||
// We need to create the scalar using the destination size since
|
||||
// `syscall(SYS_accept4, ...)` returns a long which doesn't match
|
||||
// the int returned from the `accept`/`accept4` syscalls.
|
||||
// See <https://man7.org/linux/man-pages/man2/syscall.2.html>.
|
||||
this.write_scalar(Scalar::from_int(sockfd, dest.layout.size), &dest)
|
||||
}),
|
||||
);
|
||||
}
|
||||
|
||||
/// Block the thread until the stream is connected or an error occurred.
|
||||
fn block_for_connect(&mut self, socket: FileDescriptionRef<Socket>, dest: MPlaceTy<'tcx>) {
|
||||
/// Attempt to accept an incoming connection on the listening socket in a
|
||||
/// non-blocking manner.
|
||||
///
|
||||
/// **Note**: This function is only safe to call when having previously ensured
|
||||
/// that the socket is in [`SocketState::Listening`].
|
||||
fn try_non_block_accept(
|
||||
&mut self,
|
||||
socket: &FileDescriptionRef<Socket>,
|
||||
address_ptr: Pointer,
|
||||
address_len_ptr: Pointer,
|
||||
is_client_sock_nonblock: bool,
|
||||
) -> InterpResult<'tcx, Result<i32, IoError>> {
|
||||
let this = self.eval_context_mut();
|
||||
this.block_thread_for_io(
|
||||
socket.clone(),
|
||||
Interest::WRITABLE,
|
||||
None,
|
||||
callback!(@capture<'tcx> {
|
||||
socket: FileDescriptionRef<Socket>,
|
||||
dest: MPlaceTy<'tcx>,
|
||||
} |this, kind: UnblockKind| {
|
||||
assert_eq!(kind, UnblockKind::Ready);
|
||||
|
||||
let mut state = socket.state.borrow_mut();
|
||||
let state = socket.state.borrow();
|
||||
let SocketState::Listening(listener) = &*state else {
|
||||
panic!(
|
||||
"try_non_block_accept must only be called when socket is in `SocketState::Listening`"
|
||||
)
|
||||
};
|
||||
|
||||
// We received a "writable" event so `try_set_connected` is safe to call.
|
||||
match state.try_set_connected() {
|
||||
Ok(_) => this.write_scalar(Scalar::from_i32(0), &dest),
|
||||
Err(SocketIoError::NotReady) => {
|
||||
// We need to block the thread again as the connection is still not yet ready.
|
||||
drop(state);
|
||||
this.block_for_connect(socket, dest);
|
||||
return interp_ok(())
|
||||
},
|
||||
Err(SocketIoError::Other(e)) => return this.set_last_error_and_return(e, &dest)
|
||||
}
|
||||
}),
|
||||
);
|
||||
let (stream, addr) = match listener.accept() {
|
||||
Ok(peer) => peer,
|
||||
Err(e) => return interp_ok(Err(IoError::HostError(e))),
|
||||
};
|
||||
|
||||
let family = match addr {
|
||||
SocketAddr::V4(_) => SocketFamily::IPv4,
|
||||
SocketAddr::V6(_) => SocketFamily::IPv6,
|
||||
};
|
||||
|
||||
if address_ptr != Pointer::null() {
|
||||
// We only attempt a write if the address pointer is not a null pointer.
|
||||
// If the address pointer is a null pointer the user isn't interested in the
|
||||
// address and we don't need to write anything.
|
||||
if let Err(e) =
|
||||
this.write_socket_address(&addr, address_ptr, address_len_ptr, "accept4")?
|
||||
{
|
||||
return interp_ok(Err(e));
|
||||
};
|
||||
}
|
||||
|
||||
let fd = this.machine.fds.new_ref(Socket {
|
||||
family,
|
||||
state: RefCell::new(SocketState::Connected(stream)),
|
||||
is_non_block: Cell::new(is_client_sock_nonblock),
|
||||
});
|
||||
let sockfd = this.machine.fds.insert(fd);
|
||||
interp_ok(Ok(sockfd))
|
||||
}
|
||||
|
||||
/// Block the thread until we can send bytes into the connected socket
|
||||
/// or an error occurred.
|
||||
///
|
||||
/// This recursively calls itself should the operation still block for some reason.
|
||||
///
|
||||
/// **Note**: This function is only safe to call when having previously ensured
|
||||
/// that the socket is in [`SocketState::Connected`].
|
||||
fn block_for_send(
|
||||
&mut self,
|
||||
socket: FileDescriptionRef<Socket>,
|
||||
@@ -1307,18 +1473,8 @@ fn block_for_send(
|
||||
} |this, kind: UnblockKind| {
|
||||
assert_eq!(kind, UnblockKind::Ready);
|
||||
|
||||
let mut state = socket.state.borrow_mut();
|
||||
let SocketState::Connected(stream) = &mut*state else {
|
||||
// We ensured that the socket is connected before blocking.
|
||||
unreachable!()
|
||||
};
|
||||
|
||||
// This is a *non-blocking* write.
|
||||
let result = this.write_to_host(stream, length, buffer_ptr)?;
|
||||
match result {
|
||||
match this.try_non_block_send(&socket, buffer_ptr, length)? {
|
||||
Err(IoError::HostError(e)) if e.kind() == io::ErrorKind::WouldBlock => {
|
||||
// We need to block the thread again as it would still block.
|
||||
drop(state);
|
||||
this.block_for_send(socket, buffer_ptr, length, finish);
|
||||
interp_ok(())
|
||||
},
|
||||
@@ -1328,10 +1484,41 @@ fn block_for_send(
|
||||
);
|
||||
}
|
||||
|
||||
/// Attempt to send bytes into the connected socket in a non-blocking manner.
|
||||
///
|
||||
/// **Note**: This function is only safe to call when having previously ensured
|
||||
/// that the socket is in [`SocketState::Connected`].
|
||||
fn try_non_block_send(
|
||||
&mut self,
|
||||
socket: &FileDescriptionRef<Socket>,
|
||||
buffer_ptr: Pointer,
|
||||
length: usize,
|
||||
) -> InterpResult<'tcx, Result<usize, IoError>> {
|
||||
let this = self.eval_context_mut();
|
||||
|
||||
let SocketState::Connected(stream) = &mut *socket.state.borrow_mut() else {
|
||||
panic!("try_non_block_send must only be called when the socket is connected")
|
||||
};
|
||||
|
||||
// This is a *non-blocking* write.
|
||||
let result = this.write_to_host(stream, length, buffer_ptr)?;
|
||||
match result {
|
||||
Err(IoError::HostError(e)) if e.kind() == io::ErrorKind::NotConnected => {
|
||||
// On Windows hosts, `send` can return WSAENOTCONN where EAGAIN or EWOULDBLOCK
|
||||
// would be returned on UNIX-like systems. We thus remap this error to an EWOULDBLOCK.
|
||||
interp_ok(Err(IoError::HostError(io::ErrorKind::WouldBlock.into())))
|
||||
}
|
||||
result => interp_ok(result),
|
||||
}
|
||||
}
|
||||
|
||||
/// Block the thread until we can receive bytes from the connected socket
|
||||
/// or an error occurred.
|
||||
///
|
||||
/// This recursively calls itself should the operation still block for some reason.
|
||||
///
|
||||
/// **Note**: This function is only safe to call when having previously ensured
|
||||
/// that the socket is in [`SocketState::Connected`].
|
||||
fn block_for_recv(
|
||||
&mut self,
|
||||
socket: FileDescriptionRef<Socket>,
|
||||
@@ -1354,24 +1541,9 @@ fn block_for_recv(
|
||||
} |this, kind: UnblockKind| {
|
||||
assert_eq!(kind, UnblockKind::Ready);
|
||||
|
||||
let mut state = socket.state.borrow_mut();
|
||||
let SocketState::Connected(stream) = &mut*state else {
|
||||
// We ensured that the socket is connected before blocking.
|
||||
unreachable!()
|
||||
};
|
||||
|
||||
// This is a *non-blocking* read/peek.
|
||||
let result = this.read_from_host(|buf| {
|
||||
if should_peek {
|
||||
stream.peek(buf)
|
||||
} else {
|
||||
stream.read(buf)
|
||||
}
|
||||
}, length, buffer_ptr)?;
|
||||
match result {
|
||||
match this.try_non_block_recv(&socket, buffer_ptr, length, should_peek)? {
|
||||
Err(IoError::HostError(e)) if e.kind() == io::ErrorKind::WouldBlock => {
|
||||
// We need to block the thread again as it would still block.
|
||||
drop(state);
|
||||
this.block_for_recv(socket, buffer_ptr, length, should_peek, finish);
|
||||
interp_ok(())
|
||||
},
|
||||
@@ -1380,6 +1552,178 @@ fn block_for_recv(
|
||||
}),
|
||||
);
|
||||
}
|
||||
|
||||
/// Attempt to receive bytes from the connected socket in a non-blocking manner.
|
||||
///
|
||||
/// **Note**: This function is only safe to call when having previously ensured
|
||||
/// that the socket is in [`SocketState::Connected`].
|
||||
fn try_non_block_recv(
|
||||
&mut self,
|
||||
socket: &FileDescriptionRef<Socket>,
|
||||
buffer_ptr: Pointer,
|
||||
length: usize,
|
||||
should_peek: bool,
|
||||
) -> InterpResult<'tcx, Result<usize, IoError>> {
|
||||
let this = self.eval_context_mut();
|
||||
|
||||
let SocketState::Connected(stream) = &mut *socket.state.borrow_mut() else {
|
||||
panic!("try_non_block_recv must only be called when the socket is connected")
|
||||
};
|
||||
|
||||
// This is a *non-blocking* read/peek.
|
||||
let result = this.read_from_host(
|
||||
|buf| {
|
||||
if should_peek { stream.peek(buf) } else { stream.read(buf) }
|
||||
},
|
||||
length,
|
||||
buffer_ptr,
|
||||
)?;
|
||||
match result {
|
||||
Err(IoError::HostError(e)) if e.kind() == io::ErrorKind::NotConnected => {
|
||||
// On Windows hosts, `recv` can return WSAENOTCONN where EAGAIN or EWOULDBLOCK
|
||||
// would be returned on UNIX-like systems. We thus remap this error to an EWOULDBLOCK.
|
||||
interp_ok(Err(IoError::HostError(io::ErrorKind::WouldBlock.into())))
|
||||
}
|
||||
result => interp_ok(result),
|
||||
}
|
||||
}
|
||||
|
||||
// Execute the provided callback function when the socket is either in
|
||||
// [`SocketState::Connected`] or an error occurred.
|
||||
/// If the socket is currently neither in the [`SocketState::Connecting`] nor
|
||||
/// the [`SocketState::Connecting`] state, an ENOTCONN error is returned.
|
||||
/// When the callback function is called with `Ok(_)`, then we're guaranteed
|
||||
/// that the socket is in the [`SocketState::Connected`] state.
|
||||
///
|
||||
/// This function can optionally also block until either an error occurred or
|
||||
/// the socket reached the [`SocketState::Connected`] state.
|
||||
fn ensure_connected(
|
||||
&mut self,
|
||||
socket: FileDescriptionRef<Socket>,
|
||||
should_wait: bool,
|
||||
foreign_name: &'static str,
|
||||
action: DynMachineCallback<'tcx, Result<(), ()>>,
|
||||
) -> InterpResult<'tcx> {
|
||||
let this = self.eval_context_mut();
|
||||
|
||||
let state = socket.state.borrow();
|
||||
match &*state {
|
||||
SocketState::Connecting(_) => { /* fall-through to below */ }
|
||||
SocketState::Connected(_) => {
|
||||
drop(state);
|
||||
return action.call(this, Ok(()));
|
||||
}
|
||||
_ => {
|
||||
drop(state);
|
||||
return action.call(this, Err(()));
|
||||
}
|
||||
};
|
||||
|
||||
drop(state);
|
||||
|
||||
// We're currently connecting. Since the underlying mio socket is non-blocking,
|
||||
// the only way to determine whether we are done connecting is by polling.
|
||||
// If we should wait until the connection is established, the timeout is `None`.
|
||||
// Otherwise, we use a zero duration timeout, i.e. we return immediately
|
||||
// (but we still go through the scheduler once -- which is fine).
|
||||
let timeout = if should_wait {
|
||||
None
|
||||
} else {
|
||||
Some((TimeoutClock::Monotonic, TimeoutAnchor::Absolute, Duration::ZERO))
|
||||
};
|
||||
|
||||
this.block_thread_for_io(
|
||||
socket.clone(),
|
||||
Interest::WRITABLE,
|
||||
timeout,
|
||||
callback!(
|
||||
@capture<'tcx> {
|
||||
socket: FileDescriptionRef<Socket>,
|
||||
should_wait: bool,
|
||||
foreign_name: &'static str,
|
||||
action: DynMachineCallback<'tcx, Result<(), ()>>,
|
||||
} |this, kind: UnblockKind| {
|
||||
if UnblockKind::TimedOut == kind {
|
||||
// We can only time out when `should_wait` is false.
|
||||
// This then means that the socket is not yet connected.
|
||||
assert!(!should_wait);
|
||||
this.machine.blocking_io.deregister(socket.id(), InterestReceiver::UnblockThread(this.active_thread()));
|
||||
return action.call(this, Err(()))
|
||||
}
|
||||
|
||||
// The thread woke up because it's ready, indicating a writeable or error event.
|
||||
|
||||
let mut state = socket.state.borrow_mut();
|
||||
let stream = match &*state {
|
||||
SocketState::Connecting(stream) => stream,
|
||||
SocketState::Connected(_) => {
|
||||
drop(state);
|
||||
// This can happen because we blocked the thread:
|
||||
// maybe another thread "upgraded" the connection in the meantime.
|
||||
return action.call(this, Ok(()))
|
||||
},
|
||||
_ => {
|
||||
drop(state);
|
||||
// We ensured that we only block when we're currently connecting.
|
||||
// Since this thread just got rescheduled, it could be that another
|
||||
// thread realized that the connection failed and we're thus in
|
||||
// an "invalid state".
|
||||
return action.call(this, Err(()))
|
||||
}
|
||||
};
|
||||
|
||||
// Manually check whether there were any errors since calling `connect`.
|
||||
if let Ok(Some(_)) = stream.take_error() {
|
||||
// There was an error during connecting and thus we
|
||||
// return ENOTCONN. It's the program's responsibility
|
||||
// to read SO_ERROR itself.
|
||||
//
|
||||
// Go back to initial state since the only way of getting into the
|
||||
// `Connecting` state is from the `Initial` state and at this point
|
||||
// we know that the connection won't be established anymore.
|
||||
//
|
||||
// FIXME: We're currently just dropping the error information. Eventually
|
||||
// we'll have to store it so that it can be recovered by the user.
|
||||
*state = SocketState::Initial;
|
||||
drop(state);
|
||||
return action.call(this, Err(()))
|
||||
}
|
||||
|
||||
// There was no error during connecting. We still need to ensure that
|
||||
// the wakeup wasn't spurious. We do this by attempting to read the
|
||||
// peer address of the socket (following the advice given by mio):
|
||||
// <https://docs.rs/mio/latest/mio/net/struct.TcpStream.html#notes>
|
||||
|
||||
match stream.peer_addr() {
|
||||
Ok(_) => { /* fall-through to below */},
|
||||
Err(e) if matches!(e.kind(), io::ErrorKind::NotConnected | io::ErrorKind::InProgress) => {
|
||||
// We received a spurious wakeup from the OS. This should be considered an OS bug:
|
||||
// <https://github.com/tokio-rs/mio/issues/1942#issuecomment-4169378308>
|
||||
panic!("{foreign_name}: received writable event from OS but socket is not yet connected")
|
||||
},
|
||||
Err(_) => {
|
||||
// For all other errors the socket is connected. Since we're not interested in the
|
||||
// peer address and only want to know whether the socket is connected, we can ignore
|
||||
// the error and continue.
|
||||
}
|
||||
}
|
||||
|
||||
// The connection is established.
|
||||
|
||||
// Temporarily use dummy state to take ownership of the stream.
|
||||
let SocketState::Connecting(stream) = std::mem::replace(&mut*state, SocketState::Initial) else {
|
||||
// At the start of the function we ensured that we're currently connecting.
|
||||
unreachable!()
|
||||
};
|
||||
*state = SocketState::Connected(stream);
|
||||
drop(state);
|
||||
action.call(this, Ok(()))
|
||||
}
|
||||
),
|
||||
);
|
||||
|
||||
interp_ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl VisitProvenance for FileDescriptionRef<Socket> {
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Test that we can detect a double-free bug across two threads, which only shows up if the second thread reads an atomic pointer at a very specific moment.
|
||||
// GenMC can detect this error consistently, without having to run the buggy code with multiple RNG seeds or in a loop.
|
||||
|
||||
|
||||
@@ -1,5 +1,4 @@
|
||||
//@revisions: send make
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Test that we can distinguish two pointers with the same address, but different provenance, after they are sent to GenMC and back.
|
||||
// We have two variants, one where we send such a pointer to GenMC, and one where we make it on the GenMC side.
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
Running GenMC Verification...
|
||||
error: Undefined Behavior: Attempt to access freed memory
|
||||
error: Undefined Behavior: Attempt to access non-allocated memory
|
||||
--> tests/genmc/fail/data_race/atomic_ptr_alloc_race.rs:LL:CC
|
||||
|
|
||||
LL | dealloc(b as *mut u8, Layout::new::<u64>());
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
//@revisions: write dealloc
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows -Zmiri-ignore-leaks
|
||||
//@compile-flags: -Zmiri-ignore-leaks
|
||||
|
||||
// Test that we can detect data races between an allocation and an unsynchronized action in another thread.
|
||||
// We have two variants, an alloc-dealloc race and an alloc-write race.
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Test that use-after-free bugs involving atomic pointers are detected in GenMC mode.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Test that use-after-free bugs involving atomic pointers are detected in GenMC mode.
|
||||
// Compared to `atomic_ptr_dealloc_write_race.rs`, this variant checks that the data race is still detected, even if the write happens before the free.
|
||||
//
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's test `wrong/racy/MPU2+rels+rlx`.
|
||||
// Test if Miri with GenMC can detect the data race on `X`.
|
||||
// The data race only occurs if thread 1 finishes, then threads 3 and 4 run, then thread 2.
|
||||
|
||||
@@ -1,4 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
//@revisions: rlx_rlx rlx_acq rel_rlx
|
||||
|
||||
// Translated from GenMC's test `wrong/racy/MP+rel+rlx`, `MP+rlx+acq` and `MP+rlx+rlx`.
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// SPDX-License-Identifier: MIT
|
||||
// SPDX-FileCopyrightText: Copyright (c) 2019 Carl Lerche
|
||||
|
||||
|
||||
@@ -1,12 +0,0 @@
|
||||
error: abnormal termination: the program aborted execution
|
||||
--> tests/genmc/fail/loom/store_buffering.rs:LL:CC
|
||||
|
|
||||
LL | std::process::abort();
|
||||
| ^^^^^^^^^^^^^^^^^^^^^ abnormal termination occurred here
|
||||
|
|
||||
= note: this is on thread `main`
|
||||
|
||||
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
|
||||
|
||||
error: aborting due to 1 previous error
|
||||
|
||||
@@ -1,15 +1,9 @@
|
||||
//@ revisions: non_genmc genmc
|
||||
//@[genmc] compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// SPDX-License-Identifier: MIT
|
||||
// SPDX-FileCopyrightText: Copyright (c) 2019 Carl Lerche
|
||||
|
||||
// This is the test `store_buffering` from `loom/test/litmus.rs`, adapted for Miri-GenMC.
|
||||
// https://github.com/tokio-rs/loom/blob/dbf32b04bae821c64be44405a0bb72ca08741558/tests/litmus.rs
|
||||
|
||||
// This test shows the comparison between running Miri with or without GenMC.
|
||||
// Without GenMC, Miri requires multiple iterations of the loop to detect the error.
|
||||
|
||||
#![no_main]
|
||||
|
||||
#[path = "../../../utils/genmc.rs"]
|
||||
@@ -23,30 +17,27 @@
|
||||
#[unsafe(no_mangle)]
|
||||
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
|
||||
// For normal Miri, we need multiple repetitions, but GenMC should find the bug with only 1.
|
||||
const REPS: usize = if cfg!(non_genmc) { 128 } else { 1 };
|
||||
for _ in 0..REPS {
|
||||
// New atomics every iterations, so they don't influence each other.
|
||||
let x = AtomicUsize::new(0);
|
||||
let y = AtomicUsize::new(0);
|
||||
|
||||
let mut a: usize = 1234;
|
||||
let mut b: usize = 1234;
|
||||
unsafe {
|
||||
let ids = [
|
||||
spawn_pthread_closure(|| {
|
||||
x.store(1, Relaxed);
|
||||
a = y.load(Relaxed)
|
||||
}),
|
||||
spawn_pthread_closure(|| {
|
||||
y.store(1, Relaxed);
|
||||
b = x.load(Relaxed)
|
||||
}),
|
||||
];
|
||||
join_pthreads(ids);
|
||||
}
|
||||
if (a, b) == (0, 0) {
|
||||
std::process::abort(); //~ ERROR: abnormal termination
|
||||
}
|
||||
let x = AtomicUsize::new(0);
|
||||
let y = AtomicUsize::new(0);
|
||||
|
||||
let mut a: usize = 1234;
|
||||
let mut b: usize = 1234;
|
||||
unsafe {
|
||||
let ids = [
|
||||
spawn_pthread_closure(|| {
|
||||
x.store(1, Relaxed);
|
||||
a = y.load(Relaxed)
|
||||
}),
|
||||
spawn_pthread_closure(|| {
|
||||
y.store(1, Relaxed);
|
||||
b = x.load(Relaxed)
|
||||
}),
|
||||
];
|
||||
join_pthreads(ids);
|
||||
}
|
||||
if (a, b) == (0, 0) {
|
||||
std::process::abort(); //~ ERROR: abnormal termination
|
||||
}
|
||||
|
||||
0
|
||||
|
||||
+2
-2
@@ -2,8 +2,8 @@ Running GenMC Verification...
|
||||
error: abnormal termination: the program aborted execution
|
||||
--> tests/genmc/fail/loom/store_buffering.rs:LL:CC
|
||||
|
|
||||
LL | std::process::abort();
|
||||
| ^^^^^^^^^^^^^^^^^^^^^ abnormal termination occurred here
|
||||
LL | std::process::abort();
|
||||
| ^^^^^^^^^^^^^^^^^^^^^ abnormal termination occurred here
|
||||
|
|
||||
= note: this is on thread `main`
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@ compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
fn main() {
|
||||
std::thread::spawn(|| {
|
||||
unsafe { std::hint::unreachable_unchecked() }; //~ERROR: entering unreachable code
|
||||
|
||||
@@ -1,4 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
//@error-in-other-file: Undefined Behavior
|
||||
|
||||
// Test that GenMC throws an error if a `std::sync::Mutex` is unlocked from a different thread than the one that locked it.
|
||||
|
||||
@@ -1,4 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
//@error-in-other-file: Undefined Behavior
|
||||
|
||||
// Test that GenMC can detect a double unlock of a mutex.
|
||||
|
||||
@@ -1,4 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
//@revisions: sc3_rel1 release4 relaxed4
|
||||
|
||||
// The pass tests "2w2w_3sc_1rel.rs", "2w2w_4rel" and "2w2w_4sc" and the fail test "2w2w_weak.rs" are related.
|
||||
|
||||
@@ -1,5 +1,4 @@
|
||||
//@revisions: single multiple
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
//@error-in-other-file: resource exhaustion
|
||||
|
||||
// Ensure that we emit a proper error if GenMC fails to fulfill an allocation.
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Test several operations on atomic pointers.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Test that we can send pointers with any alignment to GenMC and back, even across threads.
|
||||
// After a round-trip, the pointers should still work properly (no missing provenance).
|
||||
|
||||
|
||||
@@ -1,4 +1,4 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows -Zmiri-ignore-leaks
|
||||
//@compile-flags: -Zmiri-ignore-leaks
|
||||
|
||||
// Adapted from: `impl LazyKey`, `fn lazy_init`: rust/library/std/src/sys/thread_local/key/racy.rs
|
||||
// Two threads race to initialize a key, which is just an index into an array in this test.
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Test the basic functionality of compare_exchange.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Test that we can read the value of a non-atomic store atomically and an of an atomic value non-atomically.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Test that we can read the initial value of global, heap and stack allocations in GenMC mode.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// This test check for correct handling of atomic read-modify-write operations for all integer sizes.
|
||||
// Atomic max and min should return the previous value, and store the result in the atomic.
|
||||
// Atomic addition and subtraction should have wrapping semantics.
|
||||
|
||||
@@ -0,0 +1,22 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Tests mixed-size non-atomic accesses.
|
||||
|
||||
#![no_main]
|
||||
|
||||
use std::sync::atomic::*;
|
||||
|
||||
#[unsafe(no_mangle)]
|
||||
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
|
||||
let mut data = 0u64;
|
||||
// Treat this like an array of two AtomicI32.
|
||||
let atomics = unsafe { &*(&raw mut data as *mut u64 as *mut [AtomicI32; 2]) };
|
||||
|
||||
atomics[0].load(Ordering::SeqCst);
|
||||
atomics[1].store(-1, Ordering::SeqCst);
|
||||
atomics[0].store(-1, Ordering::Relaxed);
|
||||
|
||||
assert_eq!(data, u64::MAX);
|
||||
|
||||
0
|
||||
}
|
||||
@@ -0,0 +1,2 @@
|
||||
Running GenMC Verification...
|
||||
Verification complete with 1 executions. No errors found.
|
||||
@@ -1,5 +1,5 @@
|
||||
//@ revisions: default_R1W1 default_R1W2 spinloop_assume_R1W1 spinloop_assume_R1W2
|
||||
//@compile-flags: -Zmiri-ignore-leaks -Zmiri-genmc -Zmiri-disable-stacked-borrows -Zmiri-genmc-verbose
|
||||
//@compile-flags: -Zmiri-ignore-leaks -Zmiri-genmc-verbose
|
||||
//@normalize-stderr-test: "Verification took .*s" -> "Verification took [TIME]s"
|
||||
|
||||
// This test is a translations of the GenMC test `ms-queue-dynamic`, but with all code related to GenMC's hazard pointer API removed.
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
//@ revisions: default_R1W1 default_R1W2 default_R1W3 spinloop_assume_R1W1 spinloop_assume_R1W2 spinloop_assume_R1W3
|
||||
//@compile-flags: -Zmiri-ignore-leaks -Zmiri-genmc -Zmiri-disable-stacked-borrows -Zmiri-genmc-verbose
|
||||
//@compile-flags: -Zmiri-ignore-leaks -Zmiri-genmc-verbose
|
||||
//@normalize-stderr-test: "Verification took .*s" -> "Verification took [TIME]s"
|
||||
|
||||
// This test is a translations of the GenMC test `treiber-stack-dynamic`, but with all code related to GenMC's hazard pointer API removed.
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's test "2CoWR".
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's test "2+2W+2sc+scf".
|
||||
// It tests correct handling of SeqCst fences combined with relaxed accesses.
|
||||
|
||||
|
||||
@@ -1,4 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
//@revisions: release1 release2
|
||||
|
||||
// Translated from GenMC's test "2+2W+3sc+rel1" and "2+2W+3sc+rel2" (two variants that swap which store is `Release`).
|
||||
|
||||
@@ -1,5 +1,4 @@
|
||||
//@revisions: weak sc
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
//@[sc]compile-flags: -Zmiri-disable-weak-memory-emulation
|
||||
|
||||
// Translated from GenMC's test "2+2W".
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's test "2+2W+4c".
|
||||
//
|
||||
// The pass tests "2w2w_3sc_1rel.rs", "2w2w_4rel" and "2w2w_4sc" and the fail test "2w2w_weak.rs" are related.
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/IRIW-acq-sc" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/IRIWish" test.
|
||||
// This test prints the values read by the different threads to check that we get all the values we expect.
|
||||
|
||||
|
||||
@@ -1,30 +1,30 @@
|
||||
Running GenMC Verification...
|
||||
[1, 1, 1, 1, 1]
|
||||
[1, 1, 1, 0, 1]
|
||||
[1, 1, 1, 0, 0]
|
||||
[1, 1, 0, 1, 1]
|
||||
[1, 1, 0, 0, 1]
|
||||
[1, 1, 0, 0, 0]
|
||||
[1, 0, 1, 1, 1]
|
||||
[1, 0, 1, 0, 1]
|
||||
[1, 0, 1, 0, 0]
|
||||
[1, 0, 0, 1, 1]
|
||||
[1, 0, 0, 0, 1]
|
||||
[0, 0, 0, 0, 0]
|
||||
[0, 0, 0, 0, 1]
|
||||
[0, 0, 0, 0, 0]
|
||||
[0, 0, 0, 0, 1]
|
||||
[0, 0, 0, 0, 0]
|
||||
[0, 0, 0, 0, 1]
|
||||
[0, 0, 0, 0, 0]
|
||||
[0, 0, 0, 0, 1]
|
||||
[0, 1, 0, 0, 0]
|
||||
[0, 1, 0, 0, 1]
|
||||
[0, 1, 0, 0, 0]
|
||||
[0, 1, 0, 0, 1]
|
||||
[0, 1, 0, 0, 0]
|
||||
[0, 1, 0, 0, 1]
|
||||
[0, 1, 0, 0, 0]
|
||||
[0, 1, 0, 0, 1]
|
||||
[1, 0, 0, 0, 0]
|
||||
[0, 1, 0, 0, 1]
|
||||
[0, 1, 0, 0, 0]
|
||||
[0, 1, 0, 0, 1]
|
||||
[0, 1, 0, 0, 0]
|
||||
[0, 1, 0, 0, 1]
|
||||
[0, 1, 0, 0, 0]
|
||||
[0, 1, 0, 0, 1]
|
||||
[0, 1, 0, 0, 0]
|
||||
[0, 0, 0, 0, 1]
|
||||
[0, 0, 0, 0, 0]
|
||||
[0, 0, 0, 0, 1]
|
||||
[0, 0, 0, 0, 0]
|
||||
[0, 0, 0, 0, 1]
|
||||
[0, 0, 0, 0, 0]
|
||||
[0, 0, 0, 0, 1]
|
||||
[0, 0, 0, 0, 0]
|
||||
[1, 0, 0, 0, 1]
|
||||
[1, 0, 0, 1, 1]
|
||||
[1, 0, 1, 0, 0]
|
||||
[1, 0, 1, 0, 1]
|
||||
[1, 0, 1, 1, 1]
|
||||
[1, 1, 0, 0, 0]
|
||||
[1, 1, 0, 0, 1]
|
||||
[1, 1, 0, 1, 1]
|
||||
[1, 1, 1, 0, 0]
|
||||
[1, 1, 1, 0, 1]
|
||||
[1, 1, 1, 1, 1]
|
||||
Verification complete with 28 executions. No errors found.
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/LB" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/LB+incMPs" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/MP" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/MPU2+rels+acqf" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,38 +1,38 @@
|
||||
Running GenMC Verification...
|
||||
X=1, Y=2, a=Err(1), b=Ok(1), c=2
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=1
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=1
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=0
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=0
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=1
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=2
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=1
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=1
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=0
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=0
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=1
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=2
|
||||
X=1, Y=1, a=Err(1), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(1), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(1), b=Err(0), c=1
|
||||
X=1, Y=1, a=Err(1), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(1), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(1), b=Err(0), c=1
|
||||
X=1, Y=2, a=Err(1), b=Ok(1), c=0
|
||||
X=1, Y=2, a=Err(1), b=Ok(1), c=0
|
||||
X=1, Y=2, a=Err(1), b=Ok(1), c=1
|
||||
X=1, Y=2, a=Err(1), b=Ok(1), c=0
|
||||
X=1, Y=2, a=Err(1), b=Ok(1), c=0
|
||||
X=1, Y=2, a=Err(1), b=Ok(1), c=2
|
||||
X=1, Y=3, a=Ok(2), b=Ok(1), c=0
|
||||
X=1, Y=3, a=Ok(2), b=Ok(1), c=0
|
||||
X=1, Y=3, a=Ok(2), b=Ok(1), c=1
|
||||
X=1, Y=3, a=Ok(2), b=Ok(1), c=2
|
||||
X=2, Y=3, a=Ok(2), b=Ok(1), c=3
|
||||
X=1, Y=3, a=Ok(2), b=Ok(1), c=3
|
||||
X=1, Y=3, a=Ok(2), b=Ok(1), c=2
|
||||
X=1, Y=3, a=Ok(2), b=Ok(1), c=1
|
||||
X=1, Y=3, a=Ok(2), b=Ok(1), c=0
|
||||
X=1, Y=3, a=Ok(2), b=Ok(1), c=0
|
||||
X=1, Y=1, a=Err(1), b=Err(0), c=1
|
||||
X=1, Y=1, a=Err(1), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(1), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(1), b=Err(0), c=1
|
||||
X=1, Y=1, a=Err(1), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(1), b=Err(0), c=0
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=2
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=1
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=0
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=1
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=1
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=2
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=1
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=0
|
||||
X=1, Y=2, a=Err(0), b=Ok(1), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=1
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=1
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
X=1, Y=1, a=Err(0), b=Err(0), c=0
|
||||
Verification complete with 36 executions. No errors found.
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/MPU+rels+acq" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/MP+incMP" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/MP+rels+acqf" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/SB" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/SB+2sc+scf" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,4 @@
|
||||
//@revisions: weak sc
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
//@[sc]compile-flags: -Zmiri-disable-weak-memory-emulation
|
||||
|
||||
// Translated from GenMC's "litmus/Z6.U" test.
|
||||
|
||||
@@ -1,20 +1,20 @@
|
||||
Running GenMC Verification...
|
||||
a=1, b=1, X=1, Y=3
|
||||
a=1, b=0, X=1, Y=1
|
||||
a=1, b=1, X=1, Y=1
|
||||
a=1, b=1, X=1, Y=3
|
||||
a=3, b=1, X=1, Y=3
|
||||
a=1, b=0, X=1, Y=1
|
||||
a=1, b=1, X=1, Y=1
|
||||
a=3, b=0, X=1, Y=1
|
||||
a=3, b=1, X=1, Y=1
|
||||
a=2, b=1, X=1, Y=3
|
||||
a=4, b=1, X=1, Y=4
|
||||
a=3, b=1, X=1, Y=3
|
||||
a=2, b=1, X=1, Y=2
|
||||
a=2, b=0, X=1, Y=2
|
||||
a=1, b=1, X=1, Y=1
|
||||
a=1, b=0, X=1, Y=1
|
||||
a=4, b=1, X=1, Y=1
|
||||
a=2, b=1, X=1, Y=2
|
||||
a=4, b=0, X=1, Y=1
|
||||
a=1, b=1, X=1, Y=3
|
||||
a=3, b=1, X=1, Y=3
|
||||
a=1, b=1, X=1, Y=1
|
||||
a=4, b=1, X=1, Y=1
|
||||
a=1, b=0, X=1, Y=1
|
||||
a=3, b=1, X=1, Y=1
|
||||
a=3, b=0, X=1, Y=1
|
||||
a=1, b=1, X=1, Y=3
|
||||
a=1, b=1, X=1, Y=1
|
||||
a=1, b=0, X=1, Y=1
|
||||
Verification complete with 18 executions. No errors found.
|
||||
|
||||
@@ -1,24 +1,24 @@
|
||||
Running GenMC Verification...
|
||||
a=2, b=1, X=1, Y=3
|
||||
a=4, b=1, X=1, Y=4
|
||||
a=4, b=0, X=1, Y=4
|
||||
a=3, b=1, X=1, Y=3
|
||||
a=2, b=1, X=1, Y=2
|
||||
a=2, b=0, X=1, Y=2
|
||||
a=1, b=1, X=1, Y=1
|
||||
a=1, b=0, X=1, Y=1
|
||||
a=4, b=1, X=1, Y=1
|
||||
a=4, b=0, X=1, Y=1
|
||||
a=1, b=1, X=1, Y=3
|
||||
a=1, b=0, X=1, Y=3
|
||||
a=3, b=1, X=1, Y=3
|
||||
a=1, b=1, X=1, Y=3
|
||||
a=1, b=0, X=1, Y=1
|
||||
a=1, b=1, X=1, Y=1
|
||||
a=1, b=0, X=1, Y=3
|
||||
a=1, b=1, X=1, Y=3
|
||||
a=3, b=0, X=1, Y=3
|
||||
a=1, b=1, X=1, Y=1
|
||||
a=3, b=1, X=1, Y=3
|
||||
a=1, b=0, X=1, Y=1
|
||||
a=3, b=1, X=1, Y=1
|
||||
a=1, b=1, X=1, Y=1
|
||||
a=3, b=0, X=1, Y=1
|
||||
a=1, b=1, X=1, Y=3
|
||||
a=1, b=0, X=1, Y=3
|
||||
a=1, b=1, X=1, Y=1
|
||||
a=3, b=1, X=1, Y=1
|
||||
a=2, b=1, X=1, Y=3
|
||||
a=4, b=0, X=1, Y=4
|
||||
a=4, b=1, X=1, Y=4
|
||||
a=3, b=1, X=1, Y=3
|
||||
a=2, b=0, X=1, Y=2
|
||||
a=2, b=1, X=1, Y=2
|
||||
a=4, b=0, X=1, Y=1
|
||||
a=4, b=1, X=1, Y=1
|
||||
a=1, b=0, X=1, Y=1
|
||||
a=1, b=1, X=1, Y=1
|
||||
Verification complete with 22 executions. No errors found.
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/Z6+acq" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's test "litmus/atomicpo".
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's test "litmus/casdep".
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's test "litmus/ccr".
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's test "litmus/cii".
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "CoRR" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "CoRR0" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "CoRR1" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "CoRR2" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "CoRW" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "CoWR" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's test "litmus/cumul-release".
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/default" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,4 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
//@revisions: join no_join
|
||||
|
||||
// Translated from GenMC's "litmus/detour" test.
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "fr+w+w+w+reads" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's test "litmus/inc2w".
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
#![no_main]
|
||||
|
||||
#[path = "../../../utils/genmc.rs"]
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
|
||||
|
||||
// Translated from GenMC's "litmus/riwi" test.
|
||||
|
||||
#![no_main]
|
||||
|
||||
@@ -1,4 +1,4 @@
|
||||
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows -Zmiri-genmc-estimate
|
||||
//@compile-flags: -Zmiri-genmc-estimate
|
||||
|
||||
// Translated from GenMC's "litmus/viktor-relseq" test.
|
||||
//
|
||||
|
||||
Some files were not shown because too many files have changed in this diff Show More
Reference in New Issue
Block a user