Add option to extract opaque bodies

charon/src/cli_options.rs

@@ -11,7 +11,7 @@ use std::path::PathBuf;
 // Note that because we need to transmit the options to the charon driver,
 // we store them in a file before calling this driver (hence the `Serialize`,
 // `Deserialize` options).
-#[derive(Parser, Default, Serialize, Deserialize)]
+#[derive(Debug, Default, Clone, Parser, Serialize, Deserialize)]
 #[clap(name = "Charon")]
 pub struct CliOpts {
     /// Extract the unstructured LLBC (i.e., don't reconstruct the control-flow)
@@ -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,26 @@ 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> {
+    /// Translate a function body if we can (it has MIR) and we want to (we don't translate bodies
+    /// declared opaque, and only translate non-local bodies if `extract_opaque_bodies` is set).
+    fn translate_body(
+        mut self,
+        rust_id: DefId,
+        arg_count: usize,
+    ) -> Result<Option<ExprBody>, Error> {
         let tcx = self.t_ctx.tcx;
 
+        if !self.t_ctx.id_is_transparent(rust_id)? {
+            return Ok(None);
+        }
+        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 +1467,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 +1493,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
@@ -1766,7 +1771,6 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
     pub fn translate_function_aux(&mut self, rust_id: DefId) -> Result<(), Error> {
         trace!("About to translate function:\n{:?}", rust_id);
         let def_id = self.translate_fun_decl_id(&None, rust_id);
-        let is_transparent = self.id_is_transparent(rust_id)?;
         let def_span = self.tcx.def_span(rust_id);
 
         // Compute the meta information
@@ -1794,19 +1798,16 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
         trace!("Translating function signature");
         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_trait_method_decl {
+            // Translate the body. This returns `None` if we can't/decide not to translate this
+            // body.
+            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 +1817,7 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
                 meta,
                 def_id,
                 rust_id,
-                is_local,
+                is_local: rust_id.is_local(),
                 name,
                 signature,
                 kind,
@@ -1854,7 +1855,6 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
 
         // Compute the meta information
         let meta = self.translate_meta_from_rid(rust_id);
-        let is_transparent = self.id_is_transparent(rust_id)?;
 
         // Initialize the body translation context
         let mut bt_ctx = BodyTransCtx::new(rust_id, self);
@@ -1887,18 +1887,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),
-            }
-        } else {
-            // Otherwise do nothing
-            None
+        // Translate its body like the body of a function. This returns `None` if we can't/decide
+        // not to translate this body.
+        let body = match bt_ctx.translate_body(rust_id, 0) {
+            Ok(body) => body,
+            // Error case: we could have a specific variant
+            Err(_) => None,
         };
 
         // Save the new global

charon/src/translate_traits.rs

@@ -301,10 +301,10 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
                     let span = tcx.def_span(rust_id);
                     let method_name = bt_ctx.t_ctx.translate_trait_item_name(item.def_id)?;
                     // Skip the provided methods for the *external* trait declarations,
-                    // but still remember their name.
+                    // but still remember their name (unless `extract_opaque_bodies` is set).
                     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(),