Handle non returning intrinsics (#736)

* Handle non returning intrinsics

* Newline in comment

* Address comments

src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs

@@ -29,6 +29,25 @@ 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_never_return_intrinsic(
+        &mut self,
+        instance: Instance<'tcx>,
+        span: Option<Span>,
+    ) -> Stmt {
+        let intrinsic = self.symbol_name(instance);
+        let intrinsic = intrinsic.as_str();
+
+        debug!("codegen_never_return_intrinsic:\n\tinstance {:?}\n\tspan {:?}", instance, span);
+
+        match intrinsic {
+            "abort" => self.codegen_fatal_error("reached intrinsic::abort", span),
+            "transmute" => self.codegen_fatal_error("transmuting to uninhabited type", span),
+            _ => 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 +299,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" => {

src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs

@@ -255,19 +255,19 @@ impl<'tcx> GotocHook<'tcx> for Intrinsic {
         target: Option<BasicBlock>,
         span: Option<Span>,
     ) -> 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_never_return_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,
+                )
+            }
         }
     }
 }

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();
+}

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::<(), !>(()) };
+}