From 5079c97f616dce96a9899d97536054f3ea635487 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 7 Jan 2022 21:56:26 +0000 Subject: [PATCH 1/3] Handle non returning intrinsics --- .../src/codegen/intrinsic.rs | 19 +++++++++++++- .../rustc_codegen_rmc/src/overrides/hooks.rs | 26 +++++++++---------- src/test/rmc/Intrinsics/NonRet/abort.rs | 18 +++++++++++++ .../rmc/Intrinsics/NonRet/transmute_zst.rs | 13 ++++++++++ src/test/rmc/Intrinsics/abort.rs | 9 ------- 5 files changed, 62 insertions(+), 23 deletions(-) create mode 100644 src/test/rmc/Intrinsics/NonRet/abort.rs create mode 100644 src/test/rmc/Intrinsics/NonRet/transmute_zst.rs delete mode 100644 src/test/rmc/Intrinsics/abort.rs diff --git a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs index ef185b9a305c..6dac67e26292 100644 --- a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs +++ b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs @@ -29,6 +29,24 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_expr_to_place(p, e) } + /// Handles codegen for non returning intrinsics + /// Non returning intrinsics are not associated with a destination + pub fn codegen_nonret_intrinsic( + &mut self, + instance: Instance<'tcx>, + span: Option, + ) -> Stmt { + let intrinsic = self.symbol_name(instance); + let intrinsic = intrinsic.as_str(); + let loc = self.codegen_span_option(span); + debug!("codegen_nonret_intrinsic:\n\tinstance {:?}\n\tspan {:?}", instance, span); + match intrinsic { + "abort" => Stmt::assert_false("reached intrinsic::abort", loc), + "transmute" => Stmt::assert_false("transmuting to uninhabited type", loc), + _ => unimplemented!(), + } + } + /// c.f. rustc_codegen_llvm::intrinsic impl IntrinsicCallMethods<'tcx> for Builder<'a, 'll, 'tcx> /// fn codegen_intrinsic_call /// c.f. https://doc.rust-lang.org/std/intrinsics/index.html @@ -280,7 +298,6 @@ impl<'tcx> GotocCtx<'tcx> { } match intrinsic { - "abort" => Stmt::assert_false("abort intrinsic", loc), "add_with_overflow" => codegen_op_with_overflow!(add_overflow), "arith_offset" => codegen_wrapping_op!(plus), "assert_inhabited" => { diff --git a/src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs b/src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs index 2b08c842ffeb..83811758980e 100644 --- a/src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs +++ b/src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs @@ -260,19 +260,19 @@ impl<'tcx> GotocHook<'tcx> for Intrinsic { target: Option, span: Option, ) -> Stmt { - let loc = tcx.codegen_span_option(span); - if tcx.symbol_name(instance) == "abort" { - Stmt::assert_false("abort intrinsic reached", loc) - } else { - let p = assign_to.unwrap(); - let target = target.unwrap(); - Stmt::block( - vec![ - tcx.codegen_intrinsic(instance, fargs, &p, span), - Stmt::goto(tcx.current_fn().find_label(&target), loc.clone()), - ], - loc, - ) + match assign_to { + None => tcx.codegen_nonret_intrinsic(instance, span), + Some(assign_to) => { + let target = target.unwrap(); + let loc = tcx.codegen_span_option(span); + Stmt::block( + vec![ + tcx.codegen_intrinsic(instance, fargs, &assign_to, span), + Stmt::goto(tcx.current_fn().find_label(&target), loc.clone()), + ], + loc, + ) + } } } } diff --git a/src/test/rmc/Intrinsics/NonRet/abort.rs b/src/test/rmc/Intrinsics/NonRet/abort.rs new file mode 100644 index 000000000000..7d1d6e97bd25 --- /dev/null +++ b/src/test/rmc/Intrinsics/NonRet/abort.rs @@ -0,0 +1,18 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + +#![feature(core_intrinsics)] + +// Aborts the execution of the process +// +// The current implementation in Rust is to invoke an invalid instruction on +// most platforms. On Unix, the process terminates with a signal like `SIGABRT`, +// `SIGILL`, `SIGTRAP`, `SIGSEGV` or `SIGBUS`. +// +// The documentation mentions that `std::process::abort` is preferred if +// possible: https://doc.rust-lang.org/core/intrinsics/fn.abort.html In RMC, +// `std::process::abort` is identified as a panicking function +fn main() { + std::intrinsics::abort(); +} diff --git a/src/test/rmc/Intrinsics/NonRet/transmute_zst.rs b/src/test/rmc/Intrinsics/NonRet/transmute_zst.rs new file mode 100644 index 000000000000..723f1c15fd0a --- /dev/null +++ b/src/test/rmc/Intrinsics/NonRet/transmute_zst.rs @@ -0,0 +1,13 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + +#![feature(never_type)] + +// Transmutes an inhabited ZST into a uninhabited ZST +// +// Handled as a special case of transmute (non returning intrinsic) that +// compiles but crashes at runtime, similar to calling `std::intrinsic::abort` +fn main() { + unsafe { std::mem::transmute::<(), !>(()) }; +} diff --git a/src/test/rmc/Intrinsics/abort.rs b/src/test/rmc/Intrinsics/abort.rs deleted file mode 100644 index fc445524774d..000000000000 --- a/src/test/rmc/Intrinsics/abort.rs +++ /dev/null @@ -1,9 +0,0 @@ -// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 OR MIT -// rmc-verify-fail - -#![feature(core_intrinsics)] -use std::intrinsics; -fn main() { - intrinsics::abort(); -} From 6a6a4a367a0c9f70cd9529ba752411fca61896b1 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 7 Jan 2022 22:38:20 +0000 Subject: [PATCH 2/3] Newline in comment --- src/test/rmc/Intrinsics/NonRet/abort.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/test/rmc/Intrinsics/NonRet/abort.rs b/src/test/rmc/Intrinsics/NonRet/abort.rs index 7d1d6e97bd25..1d39dc6532df 100644 --- a/src/test/rmc/Intrinsics/NonRet/abort.rs +++ b/src/test/rmc/Intrinsics/NonRet/abort.rs @@ -11,8 +11,8 @@ // `SIGILL`, `SIGTRAP`, `SIGSEGV` or `SIGBUS`. // // The documentation mentions that `std::process::abort` is preferred if -// possible: https://doc.rust-lang.org/core/intrinsics/fn.abort.html In RMC, -// `std::process::abort` is identified as a panicking function +// possible: https://doc.rust-lang.org/core/intrinsics/fn.abort.html +// In RMC, `std::process::abort` is identified as a panicking function fn main() { std::intrinsics::abort(); } From 19dc2ed333ea07d0c24a22465f9bbe1a89f5c166 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 10 Jan 2022 14:44:25 +0000 Subject: [PATCH 3/3] Address comments --- .../rustc_codegen_rmc/src/codegen/intrinsic.rs | 11 ++++++----- .../rustc_codegen_rmc/src/overrides/hooks.rs | 2 +- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs index 6dac67e26292..fd1848470ee4 100644 --- a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs +++ b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs @@ -31,18 +31,19 @@ impl<'tcx> GotocCtx<'tcx> { /// Handles codegen for non returning intrinsics /// Non returning intrinsics are not associated with a destination - pub fn codegen_nonret_intrinsic( + pub fn codegen_never_return_intrinsic( &mut self, instance: Instance<'tcx>, span: Option, ) -> Stmt { let intrinsic = self.symbol_name(instance); let intrinsic = intrinsic.as_str(); - let loc = self.codegen_span_option(span); - debug!("codegen_nonret_intrinsic:\n\tinstance {:?}\n\tspan {:?}", instance, span); + + debug!("codegen_never_return_intrinsic:\n\tinstance {:?}\n\tspan {:?}", instance, span); + match intrinsic { - "abort" => Stmt::assert_false("reached intrinsic::abort", loc), - "transmute" => Stmt::assert_false("transmuting to uninhabited type", loc), + "abort" => self.codegen_fatal_error("reached intrinsic::abort", span), + "transmute" => self.codegen_fatal_error("transmuting to uninhabited type", span), _ => unimplemented!(), } } diff --git a/src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs b/src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs index 83811758980e..495b3cbbcfc7 100644 --- a/src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs +++ b/src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs @@ -261,7 +261,7 @@ impl<'tcx> GotocHook<'tcx> for Intrinsic { span: Option, ) -> Stmt { match assign_to { - None => tcx.codegen_nonret_intrinsic(instance, span), + None => tcx.codegen_never_return_intrinsic(instance, span), Some(assign_to) => { let target = target.unwrap(); let loc = tcx.codegen_span_option(span);