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

charon_driver/translate/
get_mir.rs
