Translate promoted constants inline

charon/src/ast/ullbc_ast_utils.rs

@@ -39,9 +39,20 @@ impl Terminator {
             comments_before: vec![],
         }
     }
+    pub fn goto(span: Span, target: BlockId) -> Self {
+        Self::new(span, RawTerminator::Goto { target })
+    }
 }
 
 impl BlockData {
+    /// Build a block that's just a goto terminator.
+    pub fn new_goto(span: Span, target: BlockId) -> Self {
+        BlockData {
+            statements: vec![],
+            terminator: Terminator::goto(span, target),
+        }
+    }
+
     pub fn targets(&self) -> Vec<BlockId> {
         match &self.terminator.content {
             RawTerminator::Goto { target } => {

charon/src/ast/visitor.rs

@@ -141,7 +141,7 @@ impl<K: Any, T: AstVisitable> AstVisitable for IndexMap<K, T> {
     // Types that are ignored when encountered.
     skip(
         AbortKind, BinOp, BorrowKind, ConstantExpr, ConstGeneric, FieldId, FieldProjKind,
-        FunDeclId, FunIdOrTraitMethodRef, GenericArgs, GlobalDeclRef, IntegerTy, Locals,
+        FunDeclId, FunIdOrTraitMethodRef, GenericArgs, GlobalDeclRef, IntegerTy,
         NullOp, RefKind, ScalarValue, Span, Ty, TypeDeclId, TypeId, UnOp, VariantId, LocalId,
     ),
     // Types that we unconditionally explore.
@@ -150,7 +150,7 @@ impl<K: Any, T: AstVisitable> AstVisitable for IndexMap<K, T> {
         llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Switch,
         ullbc_ast::BlockData, ullbc_ast::ExprBody, ullbc_ast::RawStatement,
         ullbc_ast::RawTerminator, ullbc_ast::SwitchTargets,
-        Body, Opaque,
+        Body, Opaque, Locals, Local,
         for<T: BodyVisitable> Box<T>,
         for<T: BodyVisitable> Option<T>,
         for<T: BodyVisitable, E: BodyVisitable> Result<T, E>,

charon/src/bin/charon-driver/translate/get_mir.rs

@@ -5,7 +5,6 @@ use std::rc::Rc;
 use hax_frontend_exporter as hax;
 use hax_frontend_exporter::{HasMirSetter, HasOwnerIdSetter};
 use rustc_hir as hir;
-use rustc_hir::def_id::DefId;
 use rustc_middle::mir::Body;
 use rustc_middle::ty::TyCtxt;
 
@@ -17,14 +16,15 @@ use super::translate_ctx::TranslateCtx;
 impl TranslateCtx<'_> {
     pub fn get_mir(
         &mut self,
-        def_id: DefId,
+        def_id: &hax::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.
+                let def_id = def_id.underlying_rust_def_id();
                 let body = Rc::new(body);
                 let state = self
                     .hax_state
@@ -42,50 +42,59 @@ impl TranslateCtx<'_> {
 
 /// Query the MIR for a function at a specific level. Return `None` in the case of a foreign body
 /// with no MIR available.
-fn get_mir_for_def_id_and_level(
-    tcx: TyCtxt<'_>,
-    def_id: DefId,
+fn get_mir_for_def_id_and_level<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    def_id: &hax::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());
+) -> Option<Body<'tcx>> {
+    let rust_def_id = def_id.underlying_rust_def_id();
+    match def_id.promoted_id() {
+        None => {
+            // 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) = rust_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.
             }
-            MirLevel::Promoted => {
-                let (body, _) = tcx.mir_promoted(local_def_id);
-                if !body.is_stolen() {
-                    return Some(body.borrow().clone());
-                }
-            }
-            MirLevel::Optimized => {}
+
+            // There are only two MIRs we can fetch for non-local bodies: CTFE mir for globals and const
+            // fns, and optimized MIR for functions.
+            //
+            // We pass `-Zalways-encode-mir` so that we get MIR for all the dependencies we compiled
+            // ourselves. This doesn't apply to the stdlib; there we only get MIR for const items and
+            // generic or inlineable functions.
+            let is_global = rust_def_id.as_local().is_some_and(|local_def_id| {
+                matches!(
+                    tcx.hir_body_owner_kind(local_def_id),
+                    hir::BodyOwnerKind::Const { .. } | hir::BodyOwnerKind::Static(_)
+                )
+            });
+            let body = if tcx.is_mir_available(rust_def_id) && !is_global {
+                tcx.optimized_mir(rust_def_id).clone()
+            } else if tcx.is_ctfe_mir_available(rust_def_id) {
+                tcx.mir_for_ctfe(rust_def_id).clone()
+            } else {
+                return None;
+            };
+            Some(body)
+        }
+        Some(promoted_id) => {
+            let promoted_id = promoted_id.as_rust_promoted_id();
+            Some(hax::get_promoted_mir(tcx, rust_def_id, promoted_id))
         }
-        // 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 functions.
-    //
-    // We pass `-Zalways-encode-mir` so that we get MIR for all the dependencies we compiled
-    // ourselves. This doesn't apply to the stdlib; there we only get MIR for const items and
-    // generic or inlineable functions.
-    let is_global = def_id.as_local().is_some_and(|local_def_id| {
-        matches!(
-            tcx.hir_body_owner_kind(local_def_id),
-            hir::BodyOwnerKind::Const { .. } | hir::BodyOwnerKind::Static(_)
-        )
-    });
-    let body = if tcx.is_mir_available(def_id) && !is_global {
-        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)
 }

charon/src/bin/charon-driver/translate/resolve_path.rs

@@ -84,11 +84,11 @@ pub fn def_path_def_ids<'a, 'tcx>(
             items = items
                 .into_iter()
                 .flat_map(|def_id| {
-                    let hax_def: Arc<hax::FullDef> = def_id.sinto(s);
+                    let hax_def: Arc<hax::FullDef> = def_id.sinto(s).full_def(s);
                     hax_def.nameable_children(s)
                 })
                 .filter(|(child_name, _)| *child_name == segment_str)
-                .map(|(_, def_id)| def_id.to_rust_def_id())
+                .filter_map(|(_, def_id)| def_id.as_rust_def_id())
                 .collect();
         }
         if items.is_empty() {

charon/src/bin/charon-driver/translate/translate_bodies.rs

@@ -358,23 +358,33 @@ impl BodyTransCtx<'_, '_, '_> {
                 Ok((Operand::Move(p), ty))
             }
             hax::Operand::Constant(const_op) => match &const_op.kind {
-                hax::ConstOperandKind::Value(constant)
-                | hax::ConstOperandKind::Promoted(_, Some(constant)) => {
+                hax::ConstOperandKind::Value(constant) => {
                     let constant = self.translate_constant_expr_to_constant_expr(span, constant)?;
                     let ty = constant.ty.clone();
                     Ok((Operand::Const(constant), ty))
                 }
-                hax::ConstOperandKind::Promoted(promoted, None) => {
+                hax::ConstOperandKind::Promoted {
+                    def_id,
+                    args,
+                    impl_exprs,
+                } => {
+                    let ty = self.translate_ty(span, &const_op.ty)?;
                     // A promoted constant that could not be evaluated.
-                    // TODO: translate as a Global, then inline in a pass. will need to shift
-                    // locals and block ids.
-                    // TODO: disable hax's `inline_anon_const` so we also get that for inline
-                    // consts too.
-                    raise_error!(
-                        self,
-                        span,
-                        "Cannot translate unevaluated constant: {promoted:?}"
-                    )
+                    let global_id = self.register_global_decl_id(span, def_id);
+                    let constant = ConstantExpr {
+                        value: RawConstantExpr::Global(GlobalDeclRef {
+                            id: global_id,
+                            generics: self.translate_generic_args(
+                                span,
+                                args,
+                                impl_exprs,
+                                None,
+                                GenericsSource::item(global_id),
+                            )?,
+                        }),
+                        ty: ty.clone(),
+                    };
+                    Ok((Operand::Const(constant), ty))
                 }
             },
         }
@@ -1107,8 +1117,7 @@ impl BodyTransCtx<'_, '_, '_> {
         span: Span,
     ) -> Result<Result<Body, Opaque>, Error> {
         // Retrieve the body
-        let rust_id = def.rust_def_id();
-        let Some(body) = self.t_ctx.get_mir(rust_id, span)? else {
+        let Some(body) = self.t_ctx.get_mir(&def.def_id, span)? else {
             return Ok(Err(Opaque));
         };
 

charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs

@@ -5,7 +5,6 @@ use charon_lib::transform::TransformCtx;
 use hax::FullDefKind;
 use hax_frontend_exporter::{self as hax, SInto};
 use itertools::Itertools;
-use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use std::cell::RefCell;
 use std::path::PathBuf;
@@ -59,6 +58,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             | Ctor { .. }
             | Field { .. }
             | InlineConst { .. }
+            | PromotedConst { .. }
             | LifetimeParam { .. }
             | OpaqueTy { .. }
             | SyntheticCoroutineBody { .. }
@@ -105,40 +105,40 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         Ok(())
     }
 
-    pub(crate) fn translate_item(&mut self, item_src: TransItemSource) {
+    pub(crate) fn translate_item(&mut self, item_src: &TransItemSource) {
         let trans_id = self.id_map.get(&item_src).copied();
-        let rust_id = item_src.to_def_id();
-        self.with_def_id(rust_id, trans_id, |mut ctx| {
-            let span = ctx.def_span(rust_id);
+        let def_id = item_src.as_def_id();
+        self.with_def_id(def_id, trans_id, |mut ctx| {
+            let span = ctx.def_span(def_id);
             // Catch cycles
             let res = {
                 // Stopgap measure because there are still many panics in charon and hax.
                 let mut ctx = std::panic::AssertUnwindSafe(&mut ctx);
-                std::panic::catch_unwind(move || ctx.translate_item_aux(rust_id, trans_id))
+                std::panic::catch_unwind(move || ctx.translate_item_aux(def_id, trans_id))
             };
             match res {
                 Ok(Ok(())) => return,
                 // Translation error
                 Ok(Err(_)) => {
-                    register_error!(ctx, span, "Item `{rust_id:?}` caused errors; ignoring.")
+                    register_error!(ctx, span, "Item `{def_id:?}` caused errors; ignoring.")
                 }
                 // Panic
                 Err(_) => register_error!(
                     ctx,
                     span,
-                    "Thread panicked when extracting item `{rust_id:?}`."
+                    "Thread panicked when extracting item `{def_id:?}`."
                 ),
             };
         })
     }
 
     pub(crate) fn translate_item_aux(
         &mut self,
-        rust_id: DefId,
+        def_id: &hax::DefId,
         trans_id: Option<AnyTransId>,
     ) -> Result<(), Error> {
         // Translate the meta information
-        let name = self.def_id_to_name(rust_id)?;
+        let name = self.hax_def_id_to_name(def_id)?;
         if let Some(trans_id) = trans_id {
             self.translated.item_names.insert(trans_id, name.clone());
         }
@@ -147,11 +147,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             // Don't even start translating the item. In particular don't call `hax_def` on it.
             return Ok(());
         }
-        let def = self.hax_def(rust_id)?;
+        let def = self.hax_def(def_id)?;
         let item_meta = self.translate_item_meta(&def, name, opacity);
 
         // Initialize the body translation context
-        let bt_ctx = ItemTransCtx::new(rust_id, trans_id, self);
+        let bt_ctx = ItemTransCtx::new(def_id.clone(), trans_id, self);
         match trans_id {
             Some(AnyTransId::Type(id)) => {
                 let ty = bt_ctx.translate_type(id, item_meta, &def)?;
@@ -265,8 +265,8 @@ pub fn translate<'tcx, 'ctx>(
     // from Rust ids to translated ids.
     while let Some(item_src) = ctx.items_to_translate.pop_first() {
         trace!("About to translate item: {:?}", item_src);
-        if ctx.processed.insert(item_src) {
-            ctx.translate_item(item_src);
+        if ctx.processed.insert(item_src.clone()) {
+            ctx.translate_item(&item_src);
         }
     }