charon_driver/hax/types/
mir.rs

1//! Copies of the relevant `MIR` types. MIR represents a rust (function) body as a CFG. It's a
2//! semantically rich representation that contains no high-level control-flow operations like loops
3//! or patterns; instead the control flow is entirely described by gotos and switches on integer
4//! values.
5use crate::hax::prelude::*;
6use rustc_middle::{mir, ty};
7
8sinto_reexport!(rustc_abi::FieldIdx);
9
10impl<S> SInto<S, u64> for rustc_middle::mir::interpret::AllocId {
11    fn sinto(&self, _: &S) -> u64 {
12        self.0.get()
13    }
14}
15
16pub fn name_of_local(
17    local: rustc_middle::mir::Local,
18    var_debug_info: &Vec<mir::VarDebugInfo>,
19) -> Option<String> {
20    var_debug_info
21        .iter()
22        .find(|info| {
23            if let mir::VarDebugInfoContents::Place(place) = info.value {
24                place.projection.is_empty() && place.local == local
25            } else {
26                false
27            }
28        })
29        .map(|dbg| dbg.name.to_string())
30}
31
32/// Enumerates the kinds of Mir bodies. TODO: use const generics
33/// instead of an open list of types.
34pub mod mir_kinds {
35    #[derive(Clone, Copy, Debug)]
36    pub struct Optimized;
37
38    #[derive(Clone, Copy, Debug)]
39    pub struct CTFE;
40
41    /// MIR of unknown origin. `body()` returns `None`; this is used to get the bodies provided via
42    /// `from_mir` but not attempt to get MIR for functions etc.
43    #[derive(Clone, Copy, Debug)]
44    pub struct Unknown;
45
46    pub use rustc::*;
47    mod rustc {
48        use super::*;
49        use rustc_middle::mir::Body;
50        use rustc_middle::ty::TyCtxt;
51        use rustc_span::def_id::DefId;
52
53        pub trait IsMirKind: Clone + std::fmt::Debug {
54            // CPS to deal with stealable bodies cleanly.
55            fn get_mir<'tcx, T>(
56                tcx: TyCtxt<'tcx>,
57                id: DefId,
58                f: impl FnOnce(&Body<'tcx>) -> T,
59            ) -> Option<T>;
60        }
61
62        impl IsMirKind for Optimized {
63            fn get_mir<'tcx, T>(
64                tcx: TyCtxt<'tcx>,
65                id: DefId,
66                f: impl FnOnce(&Body<'tcx>) -> T,
67            ) -> Option<T> {
68                tcx.is_mir_available(id).then(|| f(tcx.optimized_mir(id)))
69            }
70        }
71
72        impl IsMirKind for CTFE {
73            fn get_mir<'tcx, T>(
74                tcx: TyCtxt<'tcx>,
75                id: DefId,
76                f: impl FnOnce(&Body<'tcx>) -> T,
77            ) -> Option<T> {
78                (!tcx.is_trivial_const(id)).then(|| f(tcx.mir_for_ctfe(id)))
79            }
80        }
81
82        impl IsMirKind for Unknown {
83            fn get_mir<'tcx, T>(
84                _tcx: TyCtxt<'tcx>,
85                _id: DefId,
86                _f: impl FnOnce(&Body<'tcx>) -> T,
87            ) -> Option<T> {
88                None
89            }
90        }
91    }
92}
93
94pub use mir_kinds::IsMirKind;
95
96/// The contents of `Operand::Const`.
97
98#[derive(Clone, Debug)]
99pub struct ConstOperand {
100    pub span: Span,
101    pub ty: Ty,
102    pub kind: ConstOperandKind,
103}
104
105#[derive(Clone, Debug)]
106pub enum ConstOperandKind {
107    /// An evaluated constant represented as an expression.
108    Value(ConstantExpr),
109    /// Part of a MIR body that was promoted to be a constant. May not be evaluatable because of
110    /// generics.
111    /// It's a reference to the `DefId` of the constant. Note that rustc does not give a `DefId` to
112    /// promoted constants, but we do in hax.
113    Promoted(ItemRef),
114}
115
116impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstOperand> for mir::ConstOperand<'tcx> {
117    fn sinto(&self, s: &S) -> ConstOperand {
118        let kind = translate_mir_const(s, self.span, self.const_);
119        ConstOperand {
120            span: self.span.sinto(s),
121            ty: self.const_.ty().sinto(s),
122            kind,
123        }
124    }
125}
126
127/// Retrieve the MIR for a promoted body.
128pub fn get_promoted_mir<'tcx>(
129    tcx: ty::TyCtxt<'tcx>,
130    def_id: RDefId,
131    promoted_id: mir::Promoted,
132) -> mir::Body<'tcx> {
133    if let Some(local_def_id) = def_id.as_local() {
134        let (_, promoteds) = tcx.mir_promoted(local_def_id);
135        if !promoteds.is_stolen() {
136            promoteds.borrow()[promoted_id].clone()
137        } else {
138            tcx.promoted_mir(def_id)[promoted_id].clone()
139        }
140    } else {
141        tcx.promoted_mir(def_id)[promoted_id].clone()
142    }
143}
144
145/// Translate a MIR constant.
146fn translate_mir_const<'tcx, S: UnderOwnerState<'tcx>>(
147    s: &S,
148    span: rustc_span::Span,
149    konst: mir::Const<'tcx>,
150) -> ConstOperandKind {
151    use ConstOperandKind::{Promoted, Value};
152    use rustc_middle::mir::Const;
153    let tcx = s.base().tcx;
154    match konst {
155        Const::Val(const_value, ty) => {
156            let evaluated = const_value_to_constant_expr(s, ty, const_value, span);
157            match evaluated.report_err() {
158                Ok(val) => Value(val),
159                Err(err) => {
160                    warning!(
161                        s[span], "Couldn't convert constant back to an expression";
162                        {const_value, ty, err}
163                    );
164                    Value(
165                        ConstantExprKind::Todo("ConstEvalVal".into())
166                            .decorate(ty.sinto(s), span.sinto(s)),
167                    )
168                }
169            }
170        }
171        Const::Ty(_ty, c) => Value(c.sinto(s)),
172        Const::Unevaluated(ucv, _) => {
173            match ucv.promoted {
174                Some(promoted) => {
175                    let def_id = ucv.def.sinto(s).make_promoted_child(s, promoted);
176                    // The def_id is not the real one: we don't want trait resolution to happen.
177                    let item = ItemRef::translate_maybe_resolve_impl(s, false, def_id, ucv.args);
178                    assert!(item.in_trait.is_none());
179                    Promoted(item)
180                }
181                None => {
182                    let ucv = ucv.shrink();
183                    // We go through a `ty::Const`. This loses info that `ValTree`s don't capture
184                    // such as data in padding bytes.
185                    let val = ty::Const::new(tcx, ty::ConstKind::Unevaluated(ucv)).sinto(s);
186                    Value(val)
187                }
188            }
189        }
190    }
191}
charon_driver/hax/types/mir.rs

charon_driver/hax/types/
mir.rs
