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

charon_driver/translate/
get_mir.rs
