Translate drop glue for poly types

charon-ml/src/generated/Generated_GAst.ml

@@ -431,15 +431,21 @@ type cli_options = {
           break this mutual recursion. *)
   precise_drops : bool;
       (** Whether to precisely translate drops and drop-related code. For this,
-          we add explicit [Destruct] bounds to all generic parameters, and set
-          the MIR level to at least [elaborated].
+          we add explicit [Destruct] bounds to all generic parameters, set the
+          MIR level to at least [elaborated], and attempt to retrieve drop glue
+          for all types.
+
+          This option is known to cause panics inside rustc, because their drop
+          handling is not design to work on polymorphic types. To silence the
+          warning, pass appropriate
+          [--opaque '{impl core::marker::Destruct for some::Type}'] options.
 
           Without this option, drops may be "conditional" and we may lack
           information about what code is run on drop in a given polymorphic
           function body. *)
   desugar_drops : bool;
-      (** If activated, transform [Drop(p)] to [Call drop_in_place(&raw mut p)].
-      *)
+      (** Transform precise drops to the equivalent [drop_in_place(&raw mut p)]
+          call. *)
   start_from : string list;
       (** A list of item paths to use as starting points for the translation. We
           will translate these items and any items they refer to, according to

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

@@ -1,22 +1,54 @@
 use crate::translate::translate_crate::TransItemSourceKind;
 
 use super::translate_ctx::*;
-use charon_lib::ast::*;
+use charon_lib::{ast::*, formatter::IntoFormatter, pretty::FmtWithCtx};
 use hax::FullDefKind;
 
 impl ItemTransCtx<'_, '_> {
     fn translate_drop_in_place_method_body(
         &mut self,
         span: Span,
         def: &hax::FullDef,
+        self_ty: &Ty,
     ) -> Result<Body, Error> {
         let (hax::FullDefKind::Adt { drop_glue, .. } | hax::FullDefKind::Closure { drop_glue, .. }) =
             def.kind()
         else {
-            return Ok(Body::Opaque);
+            return Ok(Body::Missing);
         };
-        let Some(body) = drop_glue else {
-            return Ok(Body::Opaque);
+
+        let tmp_body;
+        let body = match drop_glue {
+            Some(body) => body,
+            None if self.options.translate_poly_drop_glue => {
+                let ctx = std::panic::AssertUnwindSafe(&mut *self);
+                // This is likely to panic, see the docs of `--precise-drops`.
+                let Ok(body) =
+                    std::panic::catch_unwind(move || def.this().drop_glue_shim(ctx.hax_state()))
+                else {
+                    let self_ty_name = if let TyKind::Adt(TypeDeclRef {
+                        id: TypeId::Adt(type_id),
+                        ..
+                    }) = self_ty.kind()
+                        && let Some(name) = self.translated.item_name(*type_id)
+                    {
+                        name.to_string_with_ctx(&self.into_fmt())
+                    } else {
+                        "crate::the::Type".to_string()
+                    };
+                    raise_error!(
+                        self,
+                        span,
+                        "rustc panicked while retrieving drop glue. \
+                        This is known to happen with `--precise-drops`; to silence this warning, \
+                        pass `--opaque '{{impl core::marker::Destruct for {}}}'` to charon",
+                        self_ty_name
+                    )
+                };
+                tmp_body = body;
+                &tmp_body
+            }
+            None => return Ok(Body::Missing),
         };
 
         Ok(self.translate_body(span, body, &def.source_text))
@@ -82,7 +114,7 @@ impl ItemTransCtx<'_, '_> {
         let body = if item_meta.opacity.with_private_contents().is_opaque() {
             Body::Opaque
         } else {
-            self.translate_drop_in_place_method_body(span, def)?
+            self.translate_drop_in_place_method_body(span, def, &self_ty)?
         };
 
         let input = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();

charon/src/options.rs

@@ -180,15 +180,19 @@ pub struct CliOpts {
     #[serde(default)]
     pub remove_unused_self_clauses: bool,
     /// Whether to precisely translate drops and drop-related code. For this, we add explicit
-    /// `Destruct` bounds to all generic parameters, and set the MIR level to at least
-    /// `elaborated`.
+    /// `Destruct` bounds to all generic parameters, set the MIR level to at least `elaborated`,
+    /// and attempt to retrieve drop glue for all types.
+    ///
+    /// This option is known to cause panics inside rustc, because their drop handling is not
+    /// design to work on polymorphic types. To silence the warning, pass appropriate `--opaque
+    /// '{impl core::marker::Destruct for some::Type}'` options.
     ///
     /// Without this option, drops may be "conditional" and we may lack information about what code
     /// is run on drop in a given polymorphic function body.
     #[clap(long)]
     #[serde(default)]
     pub precise_drops: bool,
-    /// If activated, transform `Drop(p)` to `Call drop_in_place(&raw mut p)`.
+    /// Transform precise drops to the equivalent `drop_in_place(&raw mut p)` call.
     #[clap(long)]
     #[serde(default)]
     pub desugar_drops: bool,
@@ -490,7 +494,10 @@ pub struct TranslateOptions {
     pub remove_associated_types: Vec<NamePattern>,
     /// Transform Drop to Call drop_in_place
     pub desugar_drops: bool,
+    /// Add `Destruct` bounds to all generic params.
     pub add_destruct_bounds: bool,
+    /// Translate drop glue for poly types, knowing that this may cause ICEs.
+    pub translate_poly_drop_glue: bool,
 }
 
 impl TranslateOptions {
@@ -575,8 +582,9 @@ impl TranslateOptions {
             raw_boxes: options.raw_boxes,
             remove_associated_types,
             translate_all_methods: options.translate_all_methods,
-            add_destruct_bounds: options.precise_drops,
             desugar_drops: options.desugar_drops,
+            add_destruct_bounds: options.precise_drops,
+            translate_poly_drop_glue: options.precise_drops,
         }
     }
 

charon/tests/help-output.txt

@@ -112,12 +112,14 @@ Options:
           Trait method declarations take a `Self: Trait` clause as parameter, so that they can be reused by multiple trait impls. This however causes trait definitions to be mutually recursive with their method declarations. This flag removes `Self` clauses that aren't used to break this mutual recursion
 
       --precise-drops
-          Whether to precisely translate drops and drop-related code. For this, we add explicit `Destruct` bounds to all generic parameters, and set the MIR level to at least `elaborated`.
+          Whether to precisely translate drops and drop-related code. For this, we add explicit `Destruct` bounds to all generic parameters, set the MIR level to at least `elaborated`, and attempt to retrieve drop glue for all types.
+
+          This option is known to cause panics inside rustc, because their drop handling is not design to work on polymorphic types. To silence the warning, pass appropriate `--opaque '{impl core::marker::Destruct for some::Type}'` options.
 
           Without this option, drops may be "conditional" and we may lack information about what code is run on drop in a given polymorphic function body.
 
       --desugar-drops
-          If activated, transform `Drop(p)` to `Call drop_in_place(&raw mut p)`
+          Transform precise drops to the equivalent `drop_in_place(&raw mut p)` call
 
       --start-from <START_FROM>
           A list of item paths to use as starting points for the translation. We will translate these items and any items they refer to, according to the opacity rules. When absent, we start from the path `crate` (which translates the whole crate)

charon/tests/ui/arrays.out

@@ -298,7 +298,49 @@ const UNIT_METADATA: () = @Fun0()
 fn {impl Destruct for Array<T, N>}::drop_in_place<T, const N : usize>(@1: *mut Array<T, N>)
 where
     [@TraitClause0]: Sized<T>,
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut Array<T, N>; // arg #1
+    let @2: &'_ mut (Array<T, N>); // anonymous local
+    let @3: *mut Array<T, N>; // anonymous local
+    let @4: *mut Slice<T>; // anonymous local
+    let @5: usize; // anonymous local
+    let @6: usize; // anonymous local
+    let @7: *mut T; // anonymous local
+    let @8: bool; // anonymous local
+    let @9: &'_ mut (Slice<T>); // anonymous local
+    let @10: &'_ mut (T); // anonymous local
+
+    storage_live(@2)
+    storage_live(@3)
+    storage_live(@4)
+    storage_live(@5)
+    storage_live(@6)
+    storage_live(@7)
+    storage_live(@8)
+    @0 := ()
+    @2 := &mut *(@1)
+    @3 := &raw mut *(@2)
+    @4 := unsize_cast<*mut Array<T, N>, *mut Slice<T>, N>(move (@3))
+    @5 := copy (@4.metadata)
+    @6 := const (0 : usize)
+    loop {
+        @8 := copy (@6) == copy (@5)
+        if move (@8) {
+            break 0
+        } else {
+            storage_live(@9)
+            @9 := &mut *(@4) with_metadata(copy (@4.metadata))
+            storage_live(@10)
+            @10 := @SliceIndexMut<'_, T>(move (@9), copy (@6))
+            @7 := &raw mut *(@10)
+            @6 := move (@6) wrap.+ const (1 : usize)
+            drop[{built_in impl Destruct for T}] *(@7)
+            continue 0
+        }
+    }
+    return
+}
 
 // Full name: test_crate::<array>::{impl Destruct for Array<T, N>}
 impl<T, const N : usize> Destruct for Array<T, N>

charon/tests/ui/closure-as-fn.out

@@ -129,7 +129,7 @@ fn {impl FnMut<()> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: ())
 
 // Full name: test_crate::main::closure::{impl Destruct for closure}::drop_in_place
 fn {impl Destruct for closure}::drop_in_place(@1: *mut closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::main::closure::{impl Destruct for closure}
 impl Destruct for closure {

charon/tests/ui/closures.out

@@ -154,7 +154,17 @@ const UNIT_METADATA: () = @Fun0()
 
 // Full name: test_crate::<tuple_1>::{impl Destruct for (A)}::drop_in_place
 fn {impl Destruct for (A)}::drop_in_place<A>(@1: *mut (A))
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut (A); // arg #1
+    let @2: &'_ mut ((A)); // anonymous local
+
+    storage_live(@2)
+    @0 := ()
+    @2 := &mut *(@1) with_metadata(copy (@1.metadata))
+    drop[{built_in impl Destruct for A}] (*(@2)).0
+    return
+}
 
 // Full name: test_crate::<tuple_1>::{impl Destruct for (A)}
 impl<A> Destruct for (A) {
@@ -311,7 +321,7 @@ fn {impl FnMut<(u32), u32> for test_crate::test_closure_u32::closure}::call_mut<
 
 // Full name: test_crate::test_closure_u32::closure::{impl Destruct for test_crate::test_closure_u32::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_closure_u32::closure}::drop_in_place(@1: *mut test_crate::test_closure_u32::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_u32::closure::{impl Destruct for test_crate::test_closure_u32::closure}
 impl Destruct for test_crate::test_closure_u32::closure {
@@ -451,7 +461,7 @@ fn {impl FnMut<(u32, u32), u32> for test_crate::test_closure_u32s::closure}::cal
 
 // Full name: test_crate::test_closure_u32s::closure::{impl Destruct for test_crate::test_closure_u32s::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_closure_u32s::closure}::drop_in_place(@1: *mut test_crate::test_closure_u32s::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_u32s::closure::{impl Destruct for test_crate::test_closure_u32s::closure}
 impl Destruct for test_crate::test_closure_u32s::closure {
@@ -582,7 +592,7 @@ fn {impl FnMut<(&'_ (u32)), &'_ (u32)> for test_crate::test_closure_ref_u32::clo
 
 // Full name: test_crate::test_closure_ref_u32::closure::{impl Destruct for test_crate::test_closure_ref_u32::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_closure_ref_u32::closure}::drop_in_place(@1: *mut test_crate::test_closure_ref_u32::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_ref_u32::closure::{impl Destruct for test_crate::test_closure_ref_u32::closure}
 impl Destruct for test_crate::test_closure_ref_u32::closure {
@@ -721,7 +731,7 @@ where
 fn {impl Destruct for test_crate::test_closure_ref_param::closure<T>[@TraitClause0]}::drop_in_place<T>(@1: *mut test_crate::test_closure_ref_param::closure<T>[@TraitClause0])
 where
     [@TraitClause0]: Sized<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_ref_param::closure::{impl Destruct for test_crate::test_closure_ref_param::closure<T>[@TraitClause0]}
 impl<T> Destruct for test_crate::test_closure_ref_param::closure<T>[@TraitClause0]
@@ -889,7 +899,7 @@ fn {impl Destruct for test_crate::test_closure_ref_early_bound::closure<'_, T>[@
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Trait<'a, T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_ref_early_bound::closure::{impl Destruct for test_crate::test_closure_ref_early_bound::closure<'_, T>[@TraitClause0, @TraitClause1]}
 impl<'a, T> Destruct for test_crate::test_closure_ref_early_bound::closure<'_, T>[@TraitClause0, @TraitClause1]
@@ -1051,7 +1061,7 @@ fn {impl FnMut<(u32), u32> for test_crate::test_map_option2::closure}::call_mut<
 
 // Full name: test_crate::test_map_option2::closure::{impl Destruct for test_crate::test_map_option2::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_map_option2::closure}::drop_in_place(@1: *mut test_crate::test_map_option2::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_map_option2::closure::{impl Destruct for test_crate::test_map_option2::closure}
 impl Destruct for test_crate::test_map_option2::closure {
@@ -1313,7 +1323,7 @@ fn {impl FnMut<(u32), u32> for test_crate::test_map_option3::closure}::call_mut<
 
 // Full name: test_crate::test_map_option3::closure::{impl Destruct for test_crate::test_map_option3::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_map_option3::closure}::drop_in_place(@1: *mut test_crate::test_map_option3::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_map_option3::closure::{impl Destruct for test_crate::test_map_option3::closure}
 impl Destruct for test_crate::test_map_option3::closure {
@@ -1446,7 +1456,7 @@ fn {impl FnMut<(&'_ (&'_ (u32))), u32> for test_crate::test_regions::closure}::c
 
 // Full name: test_crate::test_regions::closure::{impl Destruct for test_crate::test_regions::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_regions::closure}::drop_in_place(@1: *mut test_crate::test_regions::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_regions::closure::{impl Destruct for test_crate::test_regions::closure}
 impl Destruct for test_crate::test_regions::closure {
@@ -1531,7 +1541,7 @@ fn {impl FnMut<(&'_ (&'_ (u32))), u32> for test_crate::test_regions_casted::clos
 
 // Full name: test_crate::test_regions_casted::closure::{impl Destruct for test_crate::test_regions_casted::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_regions_casted::closure}::drop_in_place(@1: *mut test_crate::test_regions_casted::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_regions_casted::closure::{impl Destruct for test_crate::test_regions_casted::closure}
 impl Destruct for test_crate::test_regions_casted::closure {
@@ -1721,7 +1731,7 @@ fn {impl FnMut<(u32), u32> for test_crate::test_closure_capture::closure<'_0, '_
 
 // Full name: test_crate::test_closure_capture::closure::{impl Destruct for test_crate::test_closure_capture::closure<'_0, '_1>}::drop_in_place
 fn {impl Destruct for test_crate::test_closure_capture::closure<'_0, '_1>}::drop_in_place<'_0, '_1>(@1: *mut test_crate::test_closure_capture::closure<'_0, '_1>)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_capture::closure::{impl Destruct for test_crate::test_closure_capture::closure<'_0, '_1>}
 impl<'_0, '_1> Destruct for test_crate::test_closure_capture::closure<'_0, '_1> {
@@ -1859,7 +1869,7 @@ fn {impl Destruct for test_crate::test_closure_clone::closure<T>[@TraitClause0,
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Clone<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_clone::closure::{impl Destruct for test_crate::test_closure_clone::closure<T>[@TraitClause0, @TraitClause1]}
 impl<T> Destruct for test_crate::test_closure_clone::closure<T>[@TraitClause0, @TraitClause1]
@@ -1949,7 +1959,7 @@ fn {impl FnMut<(i32), i32> for test_crate::test_array_map::closure}::call_mut<'_
 
 // Full name: test_crate::test_array_map::closure::{impl Destruct for test_crate::test_array_map::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_array_map::closure}::drop_in_place(@1: *mut test_crate::test_array_map::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_array_map::closure::{impl Destruct for test_crate::test_array_map::closure}
 impl Destruct for test_crate::test_array_map::closure {
@@ -2090,7 +2100,7 @@ fn test_fnmut_with_ref()
 
 // Full name: test_crate::test_fnmut_with_ref::closure::{impl Destruct for test_crate::test_fnmut_with_ref::closure<'_0>}::drop_in_place
 fn {impl Destruct for test_crate::test_fnmut_with_ref::closure<'_0>}::drop_in_place<'_0>(@1: *mut test_crate::test_fnmut_with_ref::closure<'_0>)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_fnmut_with_ref::closure::{impl Destruct for test_crate::test_fnmut_with_ref::closure<'_0>}
 impl<'_0> Destruct for test_crate::test_fnmut_with_ref::closure<'_0> {

charon/tests/ui/closures_with_where.out

@@ -132,7 +132,7 @@ fn {impl Destruct for closure<T, K>[@TraitClause0, @TraitClause1]}::drop_in_plac
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Ops<T, K>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test::closure::{impl Destruct for closure<T, K>[@TraitClause0, @TraitClause1]}
 impl<T, const K : usize> Destruct for closure<T, K>[@TraitClause0, @TraitClause1]

charon/tests/ui/impl-trait.out

@@ -327,7 +327,7 @@ where
 fn {impl Destruct for closure<U>[@TraitClause0]}::drop_in_place<U>(@1: *mut closure<U>[@TraitClause0])
 where
     [@TraitClause0]: Sized<U>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::wrap::closure::{impl Destruct for closure<U>[@TraitClause0]}
 impl<U> Destruct for closure<U>[@TraitClause0]