Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 8 additions & 2 deletions compiler/rustc_codegen_llvm/src/gotoc/current_fn.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,10 @@

use crate::gotoc::GotocCtx;
use crate::gotoc::Stmt;
use rustc_hir::def_id::DefId;
use rustc_middle::mir::BasicBlock;
use rustc_middle::mir::Body;
use rustc_middle::ty::Instance;
use rustc_middle::ty::PolyFnSig;
use rustc_middle::ty::TyCtxt;

/// This structure represents useful data about the function we are currently compiling.
pub struct CurrentFnCtx<'tcx> {
Expand All @@ -24,6 +22,8 @@ pub struct CurrentFnCtx<'tcx> {
mir: &'tcx Body<'tcx>,
/// The symbol name of the current function
name: String,
/// A human readable pretty name for the current function
readable_name: String,
/// The signature of the current function
sig: PolyFnSig<'tcx>,
/// A counter to enable creating temporary variables
Expand All @@ -40,6 +40,7 @@ impl CurrentFnCtx<'tcx> {
labels: vec![],
mir: gcx.tcx.instance_mir(instance.def),
name: gcx.symbol_name(instance),
readable_name: gcx.readable_instance_name(instance),
sig: gcx.fn_sig_of_instance(instance),
temp_var_counter: 0,
}
Expand Down Expand Up @@ -104,6 +105,11 @@ impl CurrentFnCtx<'tcx> {
self.name.clone()
}

/// The pretty name of the function we are currently compiling
pub fn readable_name(&self) -> &str {
&self.readable_name
}

/// The signature of the function we are currently compiling
pub fn sig(&self) -> PolyFnSig<'tcx> {
self.sig
Expand Down
2 changes: 1 addition & 1 deletion compiler/rustc_codegen_llvm/src/gotoc/hooks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -224,7 +224,7 @@ impl<'tcx> GotocHook<'tcx> for Intrinsic {
span: Option<Span>,
) -> Stmt {
let loc = tcx.codegen_span_option2(span);
if (tcx.symbol_name(instance) == "abort") {
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🎉

if tcx.symbol_name(instance) == "abort" {
Stmt::assert_false("abort intrinsic reached", loc)
} else {
let p = assign_to.unwrap();
Expand Down
8 changes: 7 additions & 1 deletion compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -255,6 +255,7 @@ impl<'tcx> GotocCtx<'tcx> {
"atomic_load" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
"atomic_load_acq" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
"atomic_load_relaxed" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
"atomic_load_unordered" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
"atomic_or" => codegen_atomic_binop!(bitor),
"atomic_or_acq" => codegen_atomic_binop!(bitor),
"atomic_or_acqrel" => codegen_atomic_binop!(bitor),
Expand All @@ -263,6 +264,7 @@ impl<'tcx> GotocCtx<'tcx> {
"atomic_store" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_store_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_store_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_store_unordered" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_xadd" => codegen_atomic_binop!(plus),
"atomic_xadd_acq" => codegen_atomic_binop!(plus),
"atomic_xadd_acqrel" => codegen_atomic_binop!(plus),
Expand Down Expand Up @@ -434,7 +436,11 @@ impl<'tcx> GotocCtx<'tcx> {
"va_start" => unimplemented!(),
"volatile_set_memory" => unimplemented!(),
"volatile_store" => unimplemented!(),
_ => unimplemented!("unsupported intrinsic: {}", intrinsic),
_ => unimplemented!(
"unsupported intrinsic: {}\n\tin function {}",
intrinsic,
self.current_fn().readable_name()
),
}
}

Expand Down
43 changes: 39 additions & 4 deletions compiler/rustc_codegen_llvm/src/gotoc/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -97,13 +97,46 @@ impl<'tcx> GotocCtx<'tcx> {
self.current_fn().mir().basic_blocks().indices().map(|bb| format!("{:?}", bb)).collect()
}

fn should_skip_current_fn(&self) -> bool {
match self.current_fn().readable_name() {
// https://github.com/model-checking/rmc/issues/202
"fmt::ArgumentV1::<'a>::as_usize" => true,
// https://github.com/model-checking/rmc/issues/203
"<(dyn core::any::Any + core::marker::Send + 'static)>::downcast_ref" => true,
// https://github.com/model-checking/rmc/issues/204
x if x.ends_with("__getit") => true,
// https://github.com/model-checking/rmc/issues/205
"panic::Location::<'a>::caller" => true,
// https://github.com/model-checking/rmc/issues/206
"core::sync::atomic::atomic_swap" => true,
// https://github.com/model-checking/rmc/issues/207
"core::slice::<impl [T]>::split_first" => true,
// https://github.com/model-checking/rmc/issues/208
"panicking::take_hook" => true,
// https://github.com/model-checking/rmc/issues/209
"panicking::r#try" => true,
_ => false,
}
}

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It might be nice in the future to read these from a single file, that the README can then point to to document what's skipped.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good idea

pub fn codegen_function(&mut self, instance: Instance<'tcx>) {
self.set_current_fn(instance);
let name = self.current_fn().name();
let old_sym = self.symbol_table.lookup(&name).unwrap();
assert!(old_sym.is_function());
if old_sym.is_function_definition() {
warn!("Double codegen of {:?}", old_sym);
} else if self.should_skip_current_fn() {
debug!("Skipping function {}", self.current_fn().readable_name());
let loc = self.codegen_span2(&self.current_fn().mir().span);
let body = Stmt::assert_false(
&format!(
"The function {} is not currently supported by RMC",
self.current_fn().readable_name()
),
loc,
);
self.symbol_table.update_fn_declaration_with_definition(&name, body);
} else {
let mir = self.current_fn().mir();
self.print_instance(instance, mir);
Expand Down Expand Up @@ -170,7 +203,7 @@ impl<'tcx> GotocCtx<'tcx> {
fname,
ctx.fn_typ(),
None,
Some(ctx.readable_instance_name(instance)),
Some(ctx.current_fn().readable_name().to_string()),
ctx.codegen_span2(&mir.span),
)
});
Expand Down Expand Up @@ -268,8 +301,10 @@ impl CodegenBackend for GotocCodegenBackend {
MonoItem::Fn(instance) => c.declare_function(instance),
MonoItem::Static(def_id) => c.declare_static(def_id, item),
MonoItem::GlobalAsm(_) => {
tcx.sess.err("does not support assembly code");
tcx.sess.abort_if_errors()
warn!(
"Crate {} contains global ASM, which is not handled by RMC",
c.crate_name()
);
}
}
}
Expand All @@ -282,7 +317,7 @@ impl CodegenBackend for GotocCodegenBackend {
match item {
MonoItem::Fn(instance) => c.codegen_function(instance),
MonoItem::Static(def_id) => c.codegen_static(def_id, item),
MonoItem::GlobalAsm(_) => unreachable!(), // we have aborted above
MonoItem::GlobalAsm(_) => {} // We have already warned above
}
}
}
Expand Down
7 changes: 6 additions & 1 deletion compiler/rustc_codegen_llvm/src/gotoc/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,12 @@ impl<'tcx> ProjectedPlace<'tcx> {
let mir_typ_or_variant = mir_typ_or_variant.monomorphize(ctx);
let fat_ptr_mir_typ = fat_ptr_mir_typ.map(|t| ctx.monomorphize(t));
if let Some(fat_ptr) = &fat_ptr_goto_expr {
assert!(fat_ptr.typ().is_rust_fat_ptr(&ctx.symbol_table));
assert!(
fat_ptr.typ().is_rust_fat_ptr(&ctx.symbol_table),
"Expected fat pointer, got {:?} in function {}",
fat_ptr.typ(),
ctx.current_fn().readable_name()
);
}
// TODO: these assertions fail on a few regressions. Figure out why.
// I think it may have to do with boxed fat pointers.
Expand Down
12 changes: 9 additions & 3 deletions compiler/rustc_codegen_llvm/src/gotoc/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -486,7 +486,9 @@ impl<'tcx> GotocCtx<'tcx> {

final_fields
}
_ => unreachable!(),
// Primitives, such as NEVER, have no fields
FieldsShape::Primitive => vec![],
_ => unreachable!("{}\n{:?}", self.current_fn().readable_name(), layout.fields),
}
}

Expand Down Expand Up @@ -576,14 +578,18 @@ impl<'tcx> GotocCtx<'tcx> {
| ty::Uint(_) => self.codegen_ty(pointee_type).to_pointer(),

// These types were blocking firecracker. Doing the default thing to unblock.
// TODO, determine if this is the right course of action
// https://github.com/model-checking/rmc/issues/215
// https://github.com/model-checking/rmc/issues/216
ty::FnDef(_, _) | ty::Never => self.codegen_ty(pointee_type).to_pointer(),

// These types were blocking stdlib. Doing the default thing to unblock.
// https://github.com/model-checking/rmc/issues/214
ty::FnPtr(_) => self.codegen_ty(pointee_type).to_pointer(),

// These types have no regression tests for them.
// For soundess, hold off on generating them till we have test-cases.
ty::Bound(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::Error(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::FnPtr(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::Generator(_, _, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::GeneratorWitness(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::Infer(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
Expand Down
11 changes: 9 additions & 2 deletions compiler/rustc_codegen_llvm/src/gotoc/utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,12 @@ impl<'tcx> GotocCtx<'tcx> {
assert!(e.typ().is_rust_box(), "expected rust box {:?}", e);
let unique_ptr_typ =
self.symbol_table.lookup_field_type_in_type(e.typ(), "0").unwrap().clone();
assert!(unique_ptr_typ.is_rust_unique_pointer());
assert!(
unique_ptr_typ.is_rust_unique_pointer(),
"{:?}\n\t{}",
unique_ptr_typ,
self.current_fn().readable_name()
);
e.member("0", &self.symbol_table).member("pointer", &self.symbol_table)
}

Expand Down Expand Up @@ -133,7 +138,9 @@ impl Type {
/// Checks if the struct represents a Rust "Unique"
pub fn is_rust_unique_pointer(&self) -> bool {
self.type_name().map_or(false, |name| {
name.starts_with("tag-std::ptr::Unique") || name.starts_with("tag-core::ptr::Unique")
name.starts_with("tag-std::ptr::Unique")
|| name.starts_with("tag-core::ptr::Unique")
|| name.starts_with("tag-rustc_std_workspace_core::ptr::Unique")
Comment on lines 141 to 143
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not use name.ends_with("::ptr::Unique") here? It seems you are trying to match the full name anyway.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The name then ends with some monomorphized etc

})
}

Expand Down