charon_driver/translate/
get_mir.rs

1//! Various utilities to load MIR.
2//! Allow to easily load the MIR code generated by a specific pass.
3use std::panic;
4
5use hax::HasParamEnv;
6use rustc_middle::mir;
7use rustc_middle::ty;
8
9use charon_lib::ast::*;
10use charon_lib::options::MirLevel;
11
12use super::translate_ctx::ItemTransCtx;
13
14impl<'tcx> ItemTransCtx<'tcx, '_> {
15    pub fn get_mir(
16        &mut self,
17        item_ref: &hax::ItemRef,
18        span: Span,
19    ) -> Result<Option<mir::Body<'tcx>>, Error> {
20        // Stopgap measure because there are still many panics in charon and hax.
21        let mut this = panic::AssertUnwindSafe(&mut *self);
22        let res = panic::catch_unwind(move || this.get_mir_inner(item_ref));
23        match res {
24            Ok(Ok(body)) => Ok(body),
25            // Translation error
26            Ok(Err(e)) => Err(e),
27            Err(_) => {
28                raise_error!(self, span, "Thread panicked when extracting body.");
29            }
30        }
31    }
32
33    fn get_mir_inner(&mut self, item_ref: &hax::ItemRef) -> Result<Option<mir::Body<'tcx>>, Error> {
34        let tcx = self.t_ctx.tcx;
35        let mir_level = self.t_ctx.options.mir_level;
36        let def_id = &item_ref.def_id;
37        Ok(match get_mir_for_def_id_and_level(tcx, def_id, mir_level) {
38            Some(body) => {
39                let s = self.hax_state_with_id();
40                Some(if self.monomorphize() {
41                    let typing_env = s.typing_env();
42                    let args = item_ref.rustc_args(s);
43                    hax::substitute(tcx, typing_env, Some(args), body)
44                } else {
45                    body
46                })
47            }
48            None => None,
49        })
50    }
51}
52
53/// Query the MIR for a function at a specific level. Return `None` in the case of a foreign body
54/// with no MIR available.
55#[tracing::instrument(skip(tcx))]
56fn get_mir_for_def_id_and_level<'tcx>(
57    tcx: ty::TyCtxt<'tcx>,
58    def_id: &hax::DefId,
59    level: MirLevel,
60) -> Option<mir::Body<'tcx>> {
61    match def_id.base {
62        hax::DefIdBase::Real(rust_def_id) => {
63            if let Some(local_def_id) = rust_def_id.as_local() {
64                match level {
65                    MirLevel::Built => {
66                        let body = tcx.mir_built(local_def_id);
67                        if !body.is_stolen() {
68                            return Some(body.borrow().clone());
69                        }
70                    }
71                    MirLevel::Promoted => {
72                        let (body, _) = tcx.mir_promoted(local_def_id);
73                        if !body.is_stolen() {
74                            return Some(body.borrow().clone());
75                        }
76                    }
77                    MirLevel::Elaborated => {
78                        let body = tcx.mir_drops_elaborated_and_const_checked(local_def_id);
79                        if !body.is_stolen() {
80                            return Some(body.borrow().clone());
81                        }
82                    }
83                    MirLevel::Optimized => {}
84                }
85                // We fall back to optimized MIR if the requested body was stolen.
86            }
87
88            // There are only two MIRs we can fetch for non-local bodies: CTFE mir for globals and const
89            // fns, and optimized MIR for functions.
90            //
91            // We pass `-Zalways-encode-mir` so that we get MIR for all the dependencies we compiled
92            // ourselves. This doesn't apply to the stdlib; there we only get MIR for const items and
93            // generic or inlineable functions.
94            let is_global = matches!(
95                def_id.kind,
96                hax::DefKind::Const
97                    | hax::DefKind::AnonConst
98                    | hax::DefKind::AssocConst
99                    | hax::DefKind::InlineConst
100            );
101            let mir_available = tcx.is_mir_available(rust_def_id);
102            let ctfe_mir_available = tcx.is_ctfe_mir_available(rust_def_id);
103            // For globals, prefer ctfe_mir when both are available.
104            let body = if mir_available && !(is_global && ctfe_mir_available) {
105                tcx.optimized_mir(rust_def_id).clone()
106            } else if ctfe_mir_available {
107                tcx.mir_for_ctfe(rust_def_id).clone()
108            } else {
109                trace!("no mir available");
110                return None;
111            };
112            Some(body)
113        }
114        hax::DefIdBase::Promoted(rust_def_id, promoted_id) => {
115            Some(hax::get_promoted_mir(tcx, rust_def_id, promoted_id))
116        }
117        _ => unreachable!(),
118    }
119}
charon_driver/translate/get_mir.rs

charon_driver/translate/
get_mir.rs
