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

charon_driver/translate/
get_mir.rs
