Skip to content

Commit

Permalink
use codegen_unimplemented() for the try intrinsic (model-checking#275)
Browse files Browse the repository at this point in the history
* use codegen_unimplemented() for the try intrinsic

* Additional unit test
  • Loading branch information
danielsn authored and tedinski committed Jun 30, 2021
1 parent c50e1cf commit e5837fe
Show file tree
Hide file tree
Showing 4 changed files with 63 additions and 9 deletions.
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"),
);
}
}

0 comments on commit e5837fe

Please sign in to comment.