@@ -19,6 +19,9 @@ use rustc_serialize::json::ToJson;
1919use rustc_session:: config:: { OutputFilenames , OutputType } ;
2020use rustc_session:: Session ;
2121use rustc_target:: abi:: Endian ;
22+ use std:: cell:: RefCell ;
23+ use std:: lazy:: SyncLazy ;
24+ use std:: panic;
2225use tracing:: { debug, warn} ;
2326
2427mod assumptions;
@@ -36,10 +39,70 @@ pub mod stubs;
3639mod typ;
3740mod utils;
3841
42+ // Use a thread-local global variable to track the current codegen item for debugging.
43+ // If RMC panics during codegen, we can grab this item to include the problematic
44+ // codegen item in the panic trace.
45+ thread_local ! ( static CURRENT_CODEGEN_ITEM : RefCell <Option <String >> = RefCell :: new( None ) ) ;
46+
47+ // Include RMC's bug reporting URL in our panics.
48+ const BUG_REPORT_URL : & str =
49+ "https://github.com/model-checking/rmc/issues/new?labels=bug&template=bug_report.md" ;
50+
51+ // Custom panic hook.
52+ static DEFAULT_HOOK : SyncLazy < Box < dyn Fn ( & panic:: PanicInfo < ' _ > ) + Sync + Send + ' static > > =
53+ SyncLazy :: new ( || {
54+ let hook = panic:: take_hook ( ) ;
55+ panic:: set_hook ( Box :: new ( |info| {
56+ // Invoke the default handler, which prints the actual panic message and
57+ // optionally a backtrace. This also prints Rustc's "file a bug here" message:
58+ // it seems like the only way to remove that is to use rustc_driver::report_ice;
59+ // however, adding that dependency to this crate causes a circular dependency.
60+ // For now, just print our message after the Rust one and explicitly point to
61+ // our bug template form.
62+ ( * DEFAULT_HOOK ) ( info) ;
63+
64+ // Separate the output with an empty line
65+ eprintln ! ( ) ;
66+
67+ // Print the current function if available
68+ CURRENT_CODEGEN_ITEM . with ( |cell| {
69+ if let Some ( current_item) = cell. borrow ( ) . clone ( ) {
70+ eprintln ! ( "[RMC] current codegen item: {}" , current_item) ;
71+ } else {
72+ eprintln ! ( "[RMC] no current codegen item." ) ;
73+ }
74+ } ) ;
75+
76+ // Separate the output with an empty line
77+ eprintln ! ( ) ;
78+
79+ // Print the RMC message
80+ eprintln ! ( "RMC unexpectedly panicked during code generation.\n " ) ;
81+ eprintln ! (
82+ "If you are seeing this message, please file an issue here instead of on the Rust compiler: {}" ,
83+ BUG_REPORT_URL
84+ ) ;
85+ } ) ) ;
86+ hook
87+ } ) ;
88+
3989#[ derive( Clone ) ]
4090pub struct GotocCodegenBackend ( ) ;
4191
4292impl < ' tcx > GotocCtx < ' tcx > {
93+ // Calls the closure while updating the tracked global variable marking the
94+ // codegen item for panic debugging.
95+ pub fn call_with_panic_debug_info < F : FnOnce ( & mut GotocCtx < ' tcx > ) -> ( ) > (
96+ & mut self ,
97+ call : F ,
98+ panic_debug : String ,
99+ ) {
100+ CURRENT_CODEGEN_ITEM . with ( |odb_cell| {
101+ odb_cell. replace ( Some ( panic_debug) ) ;
102+ call ( self ) ;
103+ odb_cell. replace ( None ) ;
104+ } ) ;
105+ }
43106 pub fn codegen_block ( & mut self , bb : BasicBlock , bbd : & BasicBlockData < ' tcx > ) {
44107 self . current_fn_mut ( ) . set_current_bb ( bb) ;
45108 let label: String = self . current_fn ( ) . find_label ( & bb) ;
@@ -285,6 +348,9 @@ impl CodegenBackend for GotocCodegenBackend {
285348 ) -> Box < dyn Any > {
286349 use rustc_hir:: def_id:: LOCAL_CRATE ;
287350
351+ // Install panic hook
352+ SyncLazy :: force ( & DEFAULT_HOOK ) ; // Install ice hook
353+
288354 let codegen_units: & ' tcx [ CodegenUnit < ' _ > ] = tcx. collect_and_partition_mono_items ( ( ) ) . 1 ;
289355 let mm = machine_model_from_session ( & tcx. sess ) ;
290356 let mut c = GotocCtx :: new ( tcx, SymbolTable :: new ( mm) ) ;
@@ -294,8 +360,18 @@ impl CodegenBackend for GotocCodegenBackend {
294360 let items = cgu. items_in_deterministic_order ( tcx) ;
295361 for ( item, _) in items {
296362 match item {
297- MonoItem :: Fn ( instance) => c. declare_function ( instance) ,
298- MonoItem :: Static ( def_id) => c. declare_static ( def_id, item) ,
363+ MonoItem :: Fn ( instance) => {
364+ c. call_with_panic_debug_info (
365+ |ctx| ctx. declare_function ( instance) ,
366+ format ! ( "declare_function: {}" , c. readable_instance_name( instance) ) ,
367+ ) ;
368+ }
369+ MonoItem :: Static ( def_id) => {
370+ c. call_with_panic_debug_info (
371+ |ctx| ctx. declare_static ( def_id, item) ,
372+ format ! ( "declare_static: {:?}" , def_id) ,
373+ ) ;
374+ }
299375 MonoItem :: GlobalAsm ( _) => {
300376 warn ! (
301377 "Crate {} contains global ASM, which is not handled by RMC" ,
@@ -311,8 +387,18 @@ impl CodegenBackend for GotocCodegenBackend {
311387 let items = cgu. items_in_deterministic_order ( tcx) ;
312388 for ( item, _) in items {
313389 match item {
314- MonoItem :: Fn ( instance) => c. codegen_function ( instance) ,
315- MonoItem :: Static ( def_id) => c. codegen_static ( def_id, item) ,
390+ MonoItem :: Fn ( instance) => {
391+ c. call_with_panic_debug_info (
392+ |ctx| ctx. codegen_function ( instance) ,
393+ format ! ( "codegen_function: {}" , c. readable_instance_name( instance) ) ,
394+ ) ;
395+ }
396+ MonoItem :: Static ( def_id) => {
397+ c. call_with_panic_debug_info (
398+ |ctx| ctx. codegen_static ( def_id, item) ,
399+ format ! ( "codegen_static: {:?}" , def_id) ,
400+ ) ;
401+ }
316402 MonoItem :: GlobalAsm ( _) => { } // We have already warned above
317403 }
318404 }
0 commit comments