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

charon_driver/translate/
get_mir.rs
