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;
4use std::rc::Rc;
5
6use hax::{HasParamEnv, 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 ItemTransCtx<'_, '_> {
16    pub fn get_mir(
17        &mut self,
18        item_ref: &hax::ItemRef,
19        span: Span,
20    ) -> Result<Option<hax::MirBody<hax::mir_kinds::Unknown>>, 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, span));
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(
35        &mut self,
36        item_ref: &hax::ItemRef,
37        span: Span,
38    ) -> Result<Option<hax::MirBody<hax::mir_kinds::Unknown>>, 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                let body = 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                // Here, we have to create a MIR state, which contains the body.
53                let body = Rc::new(body);
54                let state = s.with_mir(body.clone());
55                // Translate
56                let body: hax::MirBody<hax::mir_kinds::Unknown> =
57                    self.t_ctx.catch_sinto(&state, span, body.as_ref())?;
58                Some(body)
59            }
60            None => None,
61        })
62    }
63}
64
65/// Query the MIR for a function at a specific level. Return `None` in the case of a foreign body
66/// with no MIR available.
67#[tracing::instrument(skip(tcx))]
68fn get_mir_for_def_id_and_level<'tcx>(
69    tcx: ty::TyCtxt<'tcx>,
70    def_id: &hax::DefId,
71    level: MirLevel,
72) -> Option<mir::Body<'tcx>> {
73    let rust_def_id = def_id.underlying_rust_def_id();
74    match def_id.promoted_id() {
75        None => {
76            if let Some(local_def_id) = rust_def_id.as_local() {
77                match level {
78                    MirLevel::Built => {
79                        let body = tcx.mir_built(local_def_id);
80                        if !body.is_stolen() {
81                            return Some(body.borrow().clone());
82                        }
83                    }
84                    MirLevel::Promoted => {
85                        let (body, _) = tcx.mir_promoted(local_def_id);
86                        if !body.is_stolen() {
87                            return Some(body.borrow().clone());
88                        }
89                    }
90                    MirLevel::Elaborated => {
91                        let body = tcx.mir_drops_elaborated_and_const_checked(local_def_id);
92                        if !body.is_stolen() {
93                            return Some(body.borrow().clone());
94                        }
95                    }
96                    MirLevel::Optimized => {}
97                }
98                // We fall back to optimized MIR if the requested body was stolen.
99            }
100
101            // There are only two MIRs we can fetch for non-local bodies: CTFE mir for globals and const
102            // fns, and optimized MIR for functions.
103            //
104            // We pass `-Zalways-encode-mir` so that we get MIR for all the dependencies we compiled
105            // ourselves. This doesn't apply to the stdlib; there we only get MIR for const items and
106            // generic or inlineable functions.
107            let is_global = matches!(
108                def_id.kind,
109                hax::DefKind::Const
110                    | hax::DefKind::AnonConst
111                    | hax::DefKind::AssocConst
112                    | hax::DefKind::InlineConst
113            );
114            let mir_available = tcx.is_mir_available(rust_def_id);
115            let ctfe_mir_available = tcx.is_ctfe_mir_available(rust_def_id);
116            // For globals, prefer ctfe_mir when both are available.
117            let body = if mir_available && !(is_global && ctfe_mir_available) {
118                tcx.optimized_mir(rust_def_id).clone()
119            } else if ctfe_mir_available {
120                tcx.mir_for_ctfe(rust_def_id).clone()
121            } else {
122                trace!("no mir available");
123                return None;
124            };
125            Some(body)
126        }
127        Some(promoted_id) => {
128            let promoted_id = promoted_id.as_rust_promoted_id();
129            Some(hax::get_promoted_mir(tcx, rust_def_id, promoted_id))
130        }
131    }
132}
charon_driver/translate/get_mir.rs

charon_driver/translate/
get_mir.rs
