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
26 changes: 18 additions & 8 deletions compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,14 @@ impl<'tcx> GotocCtx<'tcx> {
let intrinsic = self.symbol_name(instance);
let intrinsic = intrinsic.as_str();
let loc = self.codegen_span_option2(span);
debug!(
"codegen_intrinsic:\n\tinstance {:?}\n\tfargs {:?}\n\tp {:?}\n\tspan {:?}",
instance, fargs, p, span
);
let sig = instance.ty(self.tcx, ty::ParamEnv::reveal_all()).fn_sig(self.tcx);
let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig);
let ret_ty = self.monomorphize(sig.output());
let cbmc_ret_ty = self.codegen_ty(ret_ty);

/// https://doc.rust-lang.org/core/intrinsics/fn.copy.html
/// https://doc.rust-lang.org/core/intrinsics/fn.copy_nonoverlapping.html
Expand Down Expand Up @@ -171,6 +179,13 @@ impl<'tcx> GotocCtx<'tcx> {
}};
}

macro_rules! codegen_unimplemented_intrinsic {
($url: expr) => {{
let e = self.codegen_unimplemented(intrinsic, cbmc_ret_ty, loc, $url);
self.codegen_expr_to_place(p, e)
}};
}

// Most atomic intrinsics do:
// 1. Perform an operation on a primary argument (e.g., addition)
// 2. Return the previous value of the primary argument
Expand Down Expand Up @@ -202,14 +217,6 @@ impl<'tcx> GotocCtx<'tcx> {
}};
}

debug!(
"codegen_intrinsic:\n\tinstance {:?}\n\tfargs {:?}\n\tp {:?}\n\tspan {:?}",
instance, fargs, p, span
);
let sig = instance.ty(self.tcx, ty::ParamEnv::reveal_all()).fn_sig(self.tcx);
let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig);
let ret_ty = self.monomorphize(sig.output());

match intrinsic {
"abort" => Stmt::assert_false("abort intrinsic", loc),
"add_with_overflow" => codegen_op_with_overflow!(add_overflow),
Expand Down Expand Up @@ -394,6 +401,9 @@ impl<'tcx> GotocCtx<'tcx> {
"transmute" => self.codegen_intrinsic_transmute(fargs, ret_ty, p),
"truncf32" => codegen_simple_intrinsic!(Truncf),
"truncf64" => codegen_simple_intrinsic!(Trunc),
"try" => {
codegen_unimplemented_intrinsic!("https://github.com/model-checking/rmc/issues/267")
}
"type_id" => codegen_intrinsic_const!(),
"type_name" => codegen_intrinsic_const!(),
"unaligned_volatile_load" => {
Expand Down
10 changes: 9 additions & 1 deletion compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -628,7 +628,15 @@ impl<'tcx> GotocCtx<'tcx> {
match k {
PointerCast::ReifyFnPointer => self.codegen_operand(o).address_of(),
PointerCast::UnsafeFnPointer => self.codegen_operand(o),
PointerCast::ClosureFnPointer(_) => unimplemented!(),
PointerCast::ClosureFnPointer(_) => {
let dest_typ = self.codegen_ty(t);
self.codegen_unimplemented(
"PointerCast::ClosureFnPointer",
dest_typ,
Location::none(),
"https://github.com/model-checking/rmc/issues/274",
)
}
PointerCast::MutToConstPointer => self.codegen_operand(o),
PointerCast::ArrayToPointer => {
// TODO: I am not sure whether it is correct or not.
Expand Down
18 changes: 18 additions & 0 deletions src/test/cbmc/Intrinsics/fixme_catch_unwind.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

// https://doc.rust-lang.org/std/panic/fn.catch_unwind.html
// Stable way of calling the `try` intrinsic.
use std::panic;

fn main() {
let result = panic::catch_unwind(|| {
println!("hello!");
});
assert!(result.is_ok());

let result = panic::catch_unwind(|| {
panic!("oh no!");
});
assert!(result.is_err());
}
18 changes: 18 additions & 0 deletions src/test/cbmc/Intrinsics/fixme_try.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

// See discussion on https://github.com/model-checking/rmc/issues/267
#![feature(core_intrinsics)]
use std::intrinsics::r#try;

fn main() {
unsafe {
// Rust will make a best-effort to swallow the panic, and then execute the cleanup function.
// However, my understanding is that failure is still possible, since its just a best-effort
r#try(
|_a: *mut u8| panic!("foo"),
std::ptr::null_mut(),
|_a: *mut u8, _b: *mut u8| println!("bar"),
);
}
}