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

charon_driver/translate/
get_mir.rs
