Add option to extract opaque bodies

charon/src/cli_options.rs

@@ -110,6 +110,11 @@ performs: `y := (x as E2).1`). Producing a better reconstruction is non-trivial.
     #[clap(long = "opaque")]
     #[serde(default)]
     pub opaque_modules: Vec<String>,
+    /// Usually we skip the bodies of foreign methods and structs with private fields. When this
+    /// flag is on, we don't.
+    #[clap(long = "extract-opaque-bodies")]
+    #[serde(default)]
+    pub extract_opaque_bodies: bool,
     /// Do not provide a Rust version argument to Cargo (e.g., `+nightly-2022-01-29`).
     /// This is for Nix: outside of Nix, we use Rustup to call the proper version
     /// of Cargo (and thus need this argument), but within Nix we build and call a very

charon/src/get_mir.rs

@@ -1,7 +1,7 @@
 //! Various utilities to load MIR.
 //! Allow to easily load the MIR code generated by a specific pass.
 
-use rustc_hir::def_id::{DefId, LocalDefId};
+use rustc_hir::def_id::DefId;
 use rustc_middle::mir::Body;
 use rustc_middle::ty::TyCtxt;
 
@@ -39,32 +39,40 @@ pub fn boxes_are_desugared(level: MirLevel) -> bool {
     }
 }
 
-/// Query the MIR for a function at a specific level
+/// 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).
 pub fn get_mir_for_def_id_and_level(
     tcx: TyCtxt<'_>,
-    def_id: LocalDefId,
+    def_id: DefId,
     level: MirLevel,
-) -> Body<'_> {
+) -> Option<Body<'_>> {
     // Below: we **clone** the bodies to make sure we don't have issues with
     // locked values (we had in the past).
-    match level {
-        MirLevel::Built => {
-            let body = tcx.mir_built(def_id);
-            // We clone to be sure there are no problems with locked values
-            body.borrow().clone()
-        }
-        MirLevel::Promoted => {
-            let (body, _) = tcx.mir_promoted(def_id);
-            // We clone to be sure there are no problems with locked values
-            body.borrow().clone()
+    let body = if let Some(local_def_id) = def_id.as_local() {
+        match level {
+            MirLevel::Built => {
+                let body = tcx.mir_built(local_def_id);
+                // We clone to be sure there are no problems with locked values
+                body.borrow().clone()
+            }
+            MirLevel::Promoted => {
+                let (body, _) = tcx.mir_promoted(local_def_id);
+                // We clone to be sure there are no problems with locked values
+                body.borrow().clone()
+            }
+            MirLevel::Optimized => tcx.optimized_mir(def_id).clone(),
         }
-        MirLevel::Optimized => {
-            let def_id = DefId {
-                krate: rustc_hir::def_id::LOCAL_CRATE,
-                index: def_id.local_def_index,
-            };
-            // We clone to be sure there are no problems with locked values
+    } else {
+        // 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.
+        if tcx.is_mir_available(def_id) {
             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/translate_crate_to_ullbc.rs

@@ -255,6 +255,7 @@ pub fn translate<'tcx, 'ctx>(
         errors_as_warnings: options.errors_as_warnings,
         error_count: 0,
         no_code_duplication: options.no_code_duplication,
+        extract_opaque_bodies: options.extract_opaque_bodies,
         all_ids: LinkedHashSet::new(),
         stack: BTreeSet::new(),
         def_id: None,

charon/src/translate_ctx.rs

@@ -218,6 +218,8 @@ pub struct TransCtx<'tcx, 'ctx> {
     /// reconstruction (note that because several patterns in a match may lead
     /// to the same branch, it is node always possible not to duplicate code).
     pub no_code_duplication: bool,
+    /// Whether to extract the bodies of foreign methods and structs with private fields.
+    pub extract_opaque_bodies: bool,
     /// All the ids, in the order in which we encountered them
     pub all_ids: LinkedHashSet<AnyTransId>,
     /// The declarations we came accross and which we haven't translated yet.

charon/src/translate_functions_to_ullbc.rs

@@ -15,7 +15,7 @@ use crate::ullbc_ast::*;
 use crate::values::*;
 use hax_frontend_exporter as hax;
 use hax_frontend_exporter::SInto;
-use rustc_hir::def_id::{DefId, LocalDefId};
+use rustc_hir::def_id::DefId;
 use rustc_middle::mir::START_BLOCK;
 use rustc_middle::ty;
 use translate_types::translate_bound_region_kind_name;
@@ -1429,16 +1429,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
         let mut t_args: Vec<Operand> = Vec::new();
         for arg in args {
-            // There should only be moved arguments, or constants
-            match arg {
-                hax::Operand::Move(_) | hax::Operand::Constant(_) => {
-                    // OK
-                }
-                hax::Operand::Copy(_) => {
-                    unreachable!();
-                }
-            }
-
             // Translate
             let op = self.translate_operand(span, arg)?;
             t_args.push(op);
@@ -1447,11 +1437,21 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         Ok(t_args)
     }
 
-    fn translate_body(mut self, local_id: LocalDefId, arg_count: usize) -> Result<ExprBody, Error> {
+    fn translate_body(
+        mut self,
+        rust_id: DefId,
+        arg_count: usize,
+    ) -> Result<Option<ExprBody>, Error> {
         let tcx = self.t_ctx.tcx;
 
+        if !rust_id.is_local() && !self.t_ctx.extract_opaque_bodies {
+            // We only extract non-local bodies if the `extract_opaque_bodies` option is set.
+            return Ok(None);
+        }
+
         // Retrive the body
-        let body = get_mir_for_def_id_and_level(tcx, local_id, self.t_ctx.mir_level);
+        let Some(body) = get_mir_for_def_id_and_level(tcx, rust_id, self.t_ctx.mir_level)
+        else { return Ok(None) };
 
         // Here, we have to create a MIR state, which contains the body
         let state = hax::state::State::new_from_mir(
@@ -1462,7 +1462,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             // Yes, we have to clone, this is annoying: we end up cloning the body twice
             body.clone(),
             // Owner id
-            local_id.to_def_id(),
+            rust_id,
         );
         // Translate
         let body: hax::MirBody<()> = body.sinto(&state);
@@ -1488,12 +1488,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         }
 
         // Create the body
-        Ok(ExprBody {
+        Ok(Some(ExprBody {
             meta,
             arg_count,
             locals: self.vars,
             body: blocks,
-        })
+        }))
     }
 
     /// Translate a function's signature, and initialize a body translation context
@@ -1795,18 +1795,14 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
         let signature = bt_ctx.translate_function_signature(rust_id)?;
 
         // Check if the type is opaque or transparent
-        let is_local = rust_id.is_local();
-
-        let body = if !is_transparent || !is_local || is_trait_method_decl {
-            None
-        } else {
-            match bt_ctx.translate_body(rust_id.expect_local(), signature.inputs.len()) {
-                Ok(body) => Some(body),
-                Err(_) => {
-                    // Error case: we could have a variant for this
-                    None
-                }
+        let body = if is_transparent && !is_trait_method_decl {
+            match bt_ctx.translate_body(rust_id, signature.inputs.len()) {
+                Ok(body) => body,
+                // Error case: we could have a variant for this
+                Err(_) => None,
             }
+        } else {
+            None
         };
 
         // Save the new function
@@ -1816,7 +1812,7 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
                 meta,
                 def_id,
                 rust_id,
-                is_local,
+                is_local: rust_id.is_local(),
                 name,
                 signature,
                 kind,
@@ -1887,14 +1883,12 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
         let generics = bt_ctx.get_generics();
         let preds = bt_ctx.get_predicates();
 
-        let body = if rust_id.is_local() && is_transparent {
-            // It's a local and transparent global: we extract its body as for functions.
-            match bt_ctx.translate_body(rust_id.expect_local(), 0) {
-                Err(_) => {
-                    // Error case: we could have a specific variant
-                    None
-                }
-                Ok(body) => Some(body),
+        let body = if is_transparent {
+            // It's a transparent global: we extract its body as for functions.
+            match bt_ctx.translate_body(rust_id, 0) {
+                Ok(body) => body,
+                // Error case: we could have a specific variant
+                Err(_) => None,
             }
         } else {
             // Otherwise do nothing

charon/src/translate_traits.rs

@@ -304,7 +304,7 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
                     // but still remember their name.
                     if has_default_value {
                         // This is a *provided* method
-                        if rust_id.is_local() {
+                        if rust_id.is_local() || bt_ctx.t_ctx.extract_opaque_bodies {
                             let fun_id = bt_ctx.translate_fun_decl_id(span, item.def_id);
                             provided_methods.push((method_name, Some(fun_id)));
                         } else {

charon/src/translate_types.rs

@@ -500,11 +500,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
     /// struct with only public fields).
     fn translate_type_body(
         &mut self,
-        is_local: bool,
         trans_id: TypeDeclId::Id,
         rust_id: DefId,
     ) -> Result<TypeDeclKind, Error> {
         use rustc_middle::ty::AdtKind;
+        let is_local = rust_id.is_local();
         let def_span = self.t_ctx.tcx.def_span(rust_id);
         // Don't use `hax::AdtDef` because it loses `VariantIdx` information.
         let adt: rustc_middle::ty::AdtDef = self.t_ctx.tcx.adt_def(rust_id);
@@ -514,7 +514,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         // transparent (i.e., extract its body). If it is an enumeration, then yes
         // (because the variants of public enumerations are public, together with their
         // fields). If it is a structure, we check if all the fields are public.
-        let is_transparent = is_local
+        let is_transparent = self.t_ctx.extract_opaque_bodies
+            || is_local
             || match adt.adt_kind() {
                 AdtKind::Enum => true,
                 AdtKind::Struct => {
@@ -717,7 +718,6 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
     fn translate_type_aux(&mut self, rust_id: DefId) -> Result<(), Error> {
         let trans_id = self.translate_type_decl_id(&None, rust_id);
         let is_transparent = self.id_is_transparent(rust_id)?;
-
         let mut bt_ctx = BodyTransCtx::new(rust_id, self);
 
         // Check and translate the generics
@@ -733,11 +733,10 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
         // For instance, because `core::option::Option` is public, we can
         // manipulate its variants. If we encounter this type, we must retrieve
         // its definition.
-        let is_local = rust_id.is_local();
         let kind = if !is_transparent {
             TypeDeclKind::Opaque
         } else {
-            match bt_ctx.translate_type_body(is_local, trans_id, rust_id) {
+            match bt_ctx.translate_type_body(trans_id, rust_id) {
                 Ok(kind) => kind,
                 Err(err) => TypeDeclKind::Error(err.msg),
             }
@@ -753,7 +752,7 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
         let type_def = TypeDecl {
             def_id: trans_id,
             meta,
-            is_local,
+            is_local: rust_id.is_local(),
             name,
             generics,
             preds: bt_ctx.get_predicates(),

charon/tests/ui/.gitignore

@@ -0,0 +1 @@
+*.rlib

charon/tests/ui/issue-114-opaque-bodies-aux.rs

@@ -0,0 +1,21 @@
+//@ skip
+#[inline(always)]
+pub fn inline_always() -> u32 {
+    42
+}
+
+#[inline]
+pub fn inline_sometimes() -> u32 {
+    42
+}
+
+#[inline(never)]
+pub fn inline_never() -> u32 {
+    42
+}
+
+// Generics always have MIR in the crate data.
+#[inline(never)]
+pub fn inline_generic<T>() -> u32 {
+    42
+}