charon_driver/translate/
get_mir.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
//! Various utilities to load MIR.
//! Allow to easily load the MIR code generated by a specific pass.
use std::rc::Rc;

use hax_frontend_exporter as hax;
use hax_frontend_exporter::{HasMirSetter, HasOwnerIdSetter};
use rustc_hir::def_id::DefId;
use rustc_middle::mir::Body;
use rustc_middle::ty::TyCtxt;

use charon_lib::ast::*;
use charon_lib::options::MirLevel;

use super::translate_ctx::TranslateCtx;

/// Are box manipulations desugared to very low-level code using raw pointers,
/// unique and non-null pointers? See [crate::types::TyKind::RawPtr] for detailed explanations.
pub fn boxes_are_desugared(level: MirLevel) -> bool {
    match level {
        MirLevel::Built => false,
        MirLevel::Promoted => false,
        MirLevel::Optimized => true,
    }
}

impl TranslateCtx<'_> {
    pub fn get_mir(
        &mut self,
        def_id: DefId,
        span: Span,
    ) -> Result<Option<hax::MirBody<()>>, Error> {
        let tcx = self.tcx;
        let mir_level = self.options.mir_level;
        Ok(match get_mir_for_def_id_and_level(tcx, def_id, mir_level) {
            Some(body) => {
                // Here, we have to create a MIR state, which contains the body
                // Yes, we have to clone, this is annoying: we end up cloning the body twice
                let state = self
                    .hax_state
                    .clone()
                    .with_owner_id(def_id)
                    .with_mir(Rc::new(body.clone()));
                // Translate
                let body: hax::MirBody<()> = self.catch_sinto(&state, span, &body)?;
                Some(body)
            }
            None => None,
        })
    }
}

/// Query the MIR for a function at a specific level. Return `None` in the case of a foreign body
/// with no MIR available (e.g. because it is not available for inlining).
fn get_mir_for_def_id_and_level(
    tcx: TyCtxt<'_>,
    def_id: DefId,
    level: MirLevel,
) -> Option<Body<'_>> {
    // Below: we **clone** the bodies to make sure we don't have issues with
    // locked values (we had in the past).
    if let Some(local_def_id) = def_id.as_local() {
        match level {
            MirLevel::Built => {
                let body = tcx.mir_built(local_def_id);
                if !body.is_stolen() {
                    return Some(body.borrow().clone());
                }
            }
            MirLevel::Promoted => {
                let (body, _) = tcx.mir_promoted(local_def_id);
                if !body.is_stolen() {
                    return Some(body.borrow().clone());
                }
            }
            MirLevel::Optimized => {}
        }
        // We fall back to optimized MIR if the requested body was stolen.
    }

    // There are only two MIRs we can fetch for non-local bodies: CTFE mir for globals and
    // const fns, and optimized MIR for inlinable functions. The rest don't have MIR in the
    // rlib.
    let body = if tcx.is_mir_available(def_id) {
        if let Some(local_def_id) = def_id.as_local()
            && !matches!(
                tcx.hir().body_const_context(local_def_id),
                None | Some(rustc_hir::ConstContext::ConstFn)
            )
        {
            tcx.mir_for_ctfe(def_id).clone()
        } else {
            tcx.optimized_mir(def_id).clone()
        }
    } else if tcx.is_ctfe_mir_available(def_id) {
        tcx.mir_for_ctfe(def_id).clone()
    } else {
        return None;
    };
    Some(body)
}