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

charon_driver/translate/
get_mir.rs
