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(Debug, Copy, Clone)]
36    pub struct Optimized;
37
38    #[derive(Debug, Copy, Clone)]
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(Debug, Copy, Clone)]
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#[derive(Debug, Clone)]
98pub struct ConstOperand<'tcx> {
99    pub span: Span,
100    pub ty: Ty<'tcx>,
101    pub kind: ConstOperandKind<'tcx>,
102}
103
104#[derive(Debug, Clone)]
105pub enum ConstOperandKind<'tcx> {
106    /// An evaluated constant represented as an expression.
107    Value(ConstantExpr<'tcx>),
108    /// Part of a MIR body that was promoted to be a constant. May not be evaluatable because of
109    /// generics.
110    /// It's a reference to the `DefId` of the constant. Note that rustc does not give a `DefId` to
111    /// promoted constants, but we do in hax.
112    Promoted(ItemRef<'tcx>),
113}
114
115impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstOperand<'tcx>> for mir::ConstOperand<'tcx> {
116    fn sinto(&self, s: &S) -> ConstOperand<'tcx> {
117        let kind = translate_mir_const(s, self.span, self.const_);
118        ConstOperand {
119            span: self.span.sinto(s),
120            ty: self.const_.ty().sinto(s),
121            kind,
122        }
123    }
124}
125
126/// Translate a MIR constant.
127fn translate_mir_const<'tcx, S: UnderOwnerState<'tcx>>(
128    s: &S,
129    span: rustc_span::Span,
130    konst: mir::Const<'tcx>,
131) -> ConstOperandKind<'tcx> {
132    use ConstOperandKind::{Promoted, Value};
133    use rustc_middle::mir::Const;
134    let tcx = s.base().tcx;
135    match konst {
136        Const::Val(const_value, ty) => {
137            let src = ConstSource::Value(const_value, ty);
138            Value(
139                read_const(s, span, src, ReadMode::Structured).unwrap_or_else(|| {
140                    ConstantExpr::new(ConstantExprKind::Todo("ConstEvalVal".into()), ty.sinto(s))
141                }),
142            )
143        }
144        Const::Ty(_ty, c) => Value(c.sinto(s)),
145        Const::Unevaluated(ucv, _) => {
146            match ucv.promoted {
147                Some(promoted) => {
148                    let def_id = ucv.def.sinto(s).make_promoted_child(s, promoted);
149                    let item = ItemRef::translate_from_hax_def_id(s, def_id, ucv.args);
150                    assert!(item.in_trait.is_none());
151                    Promoted(item)
152                }
153                None => {
154                    let ucv = ucv.shrink(tcx);
155                    // We go through a `ty::Const`. This loses info that `ValTree`s don't capture
156                    // such as data in padding bytes.
157                    let val =
158                        ty::Const::new(tcx, ty::ConstKind::Alias(ty::IsRigid::No, ucv)).sinto(s);
159                    Value(val)
160                }
161            }
162        }
163    }
164}
charon_driver/hax/types/mir.rs

charon_driver/hax/types/
mir.rs
