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

charon_driver/translate/
get_mir.rs
