moved the gotoc functionality out of mod.rs

Author: danielsn

compiler/rustc_codegen_llvm/src/gotoc/backend.rs

@@ -3,6 +3,15 @@
 
 //! This file contains functionality that makes RMC easier to debug
 
+use super::metadata::*;
+use rustc_middle::mir::Body;
+use rustc_middle::ty::print::with_no_trimmed_paths;
+use rustc_middle::ty::Instance;
+use std::cell::RefCell;
+use std::lazy::SyncLazy;
+use std::panic;
+use tracing::debug;
+
 // Use a thread-local global variable to track the current codegen item for debugging.
 // If RMC panics during codegen, we can grab this item to include the problematic
 // codegen item in the panic trace.
@@ -12,43 +21,43 @@ thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<Option<String>> = RefCell::ne
 const BUG_REPORT_URL: &str =
     "https://github.com/model-checking/rmc/issues/new?labels=bug&template=bug_report.md";
 
-    // Custom panic hook.
-static DEFAULT_HOOK: SyncLazy<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
-SyncLazy::new(|| {
-    let hook = panic::take_hook();
-    panic::set_hook(Box::new(|info| {
-        // Invoke the default handler, which prints the actual panic message and
-        // optionally a backtrace. This also prints Rustc's "file a bug here" message:
-        // it seems like the only way to remove that is to use rustc_driver::report_ice;
-        // however, adding that dependency to this crate causes a circular dependency.
-        // For now, just print our message after the Rust one and explicitly point to
-        // our bug template form.
-        (*DEFAULT_HOOK)(info);
+// Custom panic hook.
+pub static DEFAULT_HOOK: SyncLazy<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
+    SyncLazy::new(|| {
+        let hook = panic::take_hook();
+        panic::set_hook(Box::new(|info| {
+            // Invoke the default handler, which prints the actual panic message and
+            // optionally a backtrace. This also prints Rustc's "file a bug here" message:
+            // it seems like the only way to remove that is to use rustc_driver::report_ice;
+            // however, adding that dependency to this crate causes a circular dependency.
+            // For now, just print our message after the Rust one and explicitly point to
+            // our bug template form.
+            (*DEFAULT_HOOK)(info);
 
-        // Separate the output with an empty line
-        eprintln!();
+            // Separate the output with an empty line
+            eprintln!();
 
-        // Print the current function if available
-        CURRENT_CODEGEN_ITEM.with(|cell| {
-            if let Some(current_item) = cell.borrow().clone() {
-                eprintln!("[RMC] current codegen item: {}", current_item);
-            } else {
-                eprintln!("[RMC] no current codegen item.");
-            }
-        });
+            // Print the current function if available
+            CURRENT_CODEGEN_ITEM.with(|cell| {
+                if let Some(current_item) = cell.borrow().clone() {
+                    eprintln!("[RMC] current codegen item: {}", current_item);
+                } else {
+                    eprintln!("[RMC] no current codegen item.");
+                }
+            });
 
-        // Separate the output with an empty line
-        eprintln!();
+            // Separate the output with an empty line
+            eprintln!();
 
-        // Print the RMC message
-        eprintln!("RMC unexpectedly panicked during code generation.\n");
-        eprintln!(
-            "If you are seeing this message, please file an issue here instead of on the Rust compiler: {}",
-            BUG_REPORT_URL
-        );
-    }));
-    hook
-});
+            // Print the RMC message
+            eprintln!("RMC unexpectedly panicked during code generation.\n");
+            eprintln!(
+                "If you are seeing this message, please file an issue here instead of on the Rust compiler: {}",
+                BUG_REPORT_URL
+            );
+        }));
+        hook
+    });
 
 impl<'tcx> GotocCtx<'tcx> {
     // Calls the closure while updating the tracked global variable marking the
@@ -65,7 +74,7 @@ impl<'tcx> GotocCtx<'tcx> {
         });
     }
 
-    fn print_instance(&self, instance: Instance<'_>, mir: &'tcx Body<'tcx>) {
+    pub fn print_instance(&self, instance: Instance<'_>, mir: &'tcx Body<'tcx>) {
         if cfg!(debug_assertions) {
             debug!(
                 "handling {}, {}",
@@ -85,5 +94,4 @@ impl<'tcx> GotocCtx<'tcx> {
             }
         }
     }
-
 }

compiler/rustc_codegen_llvm/src/gotoc/debug.rs

@@ -2,34 +2,29 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use bitflags::_core::any::Any;
 use cbmc::goto_program::symtab_transformer;
-use cbmc::goto_program::{Stmt, Symbol, SymbolTable};
+use cbmc::goto_program::{Stmt, SymbolTable};
 use cbmc::{MachineModel, RoundingMode};
 use metadata::*;
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_errors::ErrorReported;
-use rustc_hir::def_id::DefId;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
 use rustc_middle::middle::cstore::{EncodedMetadata, MetadataLoaderDyn};
 use rustc_middle::mir::mono::{CodegenUnit, MonoItem};
-use rustc_middle::mir::Body;
-use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::query::Providers;
-use rustc_middle::ty::{self, Instance, TyCtxt};
+use rustc_middle::ty::{self, TyCtxt};
 use rustc_serialize::json::ToJson;
 use rustc_session::config::{OutputFilenames, OutputType};
 use rustc_session::Session;
 use rustc_target::abi::Endian;
-use std::cell::RefCell;
 use std::lazy::SyncLazy;
-use std::panic;
 use tracing::{debug, warn};
 
 mod assumptions;
-mod backend;
 mod block;
 pub mod cbmc;
 mod current_fn;
+mod debug;
 mod function;
 mod hooks;
 mod intrinsic;
@@ -50,8 +45,6 @@ pub struct GotocCodegenResult {
     pub crate_name: rustc_span::Symbol,
 }
 
-
-
 #[derive(Clone)]
 pub struct GotocCodegenBackend();
 
@@ -73,7 +66,6 @@ impl<'tcx> GotocCtx<'tcx> {
             _ => false,
         }
     }
-
 }
 
 impl GotocCodegenBackend {
@@ -155,7 +147,7 @@ impl CodegenBackend for GotocCodegenBackend {
         use rustc_hir::def_id::LOCAL_CRATE;
 
         // Install panic hook
-        SyncLazy::force(&DEFAULT_HOOK); // Install ice hook
+        SyncLazy::force(&debug::DEFAULT_HOOK); // Install ice hook
 
         let codegen_units: &'tcx [CodegenUnit<'_>] = tcx.collect_and_partition_mono_items(()).1;
         let mm = machine_model_from_session(&tcx.sess);

compiler/rustc_codegen_llvm/src/gotoc/mod.rs

@@ -3,6 +3,12 @@
 
 //! This file contains functions related to codegenning MIR static variables into gotoc
 
+use super::cbmc::goto_program::Symbol;
+use super::metadata::*;
+use rustc_hir::def_id::DefId;
+use rustc_middle::mir::mono::MonoItem;
+use tracing::debug;
+
 impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_static(&mut self, def_id: DefId, item: MonoItem<'tcx>) {
         debug!("codegen_static");
@@ -11,7 +17,7 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_allocation(alloc, |_| symbol_name.clone(), Some(symbol_name.clone()));
     }
 
-    fn declare_static(&mut self, def_id: DefId, item: MonoItem<'tcx>) {
+    pub fn declare_static(&mut self, def_id: DefId, item: MonoItem<'tcx>) {
         debug!("declare_static {:?}", def_id);
         let symbol_name = item.symbol_name(self.tcx).to_string();
         let typ = self.codegen_ty(self.tcx.type_of(def_id));