drop shim debug & regions added

ssyram · ssyram · commit ec7b41b8d756 · 2025-09-03T14:47:15.000+08:00
diff --git a/charon/src/transform/compute_vtable_metadata.rs b/charon/src/transform/compute_vtable_metadata.rs
@@ -661,11 +661,15 @@ impl<'a> VtableMetadataComputer<'a> {
             self.impl_ref.id.with_ctx(&self.ctx.into_fmt())
         );
         // Get the generics from the trait impl - drop shims should have the same generics
-        let generics = self.get_trait_impl_generics()?;
+        let generics = self.get_drop_shim_generic_params()?;
 
         // Create the dyn trait type for the parameter
         // For the drop shim, we need &mut (dyn Trait<...>)
         let dyn_trait_param_ty = self.get_drop_receiver()?;
+        let dyn_trait_param_ty = match dyn_trait_param_ty.kind() {
+            TyKind::Ref(_,ty,_) => Ty::new(TyKind::Ref(Region::Var(DeBruijnVar::new_at_zero(RegionId::ZERO)), ty.clone(), RefKind::Mut)),
+            _ => unreachable!(),
+        };
 
         // Create function signature with proper generics
         let signature = FunSig {
@@ -675,9 +679,7 @@ impl<'a> VtableMetadataComputer<'a> {
             output: Ty::mk_unit(),
         };
 
-        let body = DropShimCtx::create_drop_shim_body(self, &self.get_drop_receiver()?, concrete_ty, drop_case)?;
-        
-        // let body = self.old_create_drop_shim_body(&self.get_drop_receiver()?, concrete_ty, drop_case)?;
+        let body = DropShimCtx::create_drop_shim_body(self, &dyn_trait_param_ty, concrete_ty, drop_case)?;
 
         // Create item meta
         let item_meta = ItemMeta {
@@ -770,7 +772,7 @@ impl<'a> VtableMetadataComputer<'a> {
         }
     }
 
-    fn get_trait_impl_generics(&self) -> Result<GenericParams, Error> {
+    fn get_drop_shim_generic_params(&self) -> Result<GenericParams, Error> {
         let Some(trait_impl) = self.ctx.translated.trait_impls.get(self.impl_ref.id) else {
             raise_error!(
                 self.ctx,
@@ -784,13 +786,9 @@ impl<'a> VtableMetadataComputer<'a> {
         // but with at least one region binder for the receiver
         let mut generics = trait_impl.generics.clone();
 
-        // Ensure we have at least one region for the receiver parameter
-        if generics.regions.is_empty() {
-            let _ = generics.regions.push_with(|id| RegionVar {
-                index: id,
-                name: None,
-            });
-        }
+        // Insert the region for the drop shim receiver
+        generics.regions.iter_mut().for_each(|reg| reg.index += 1);
+        generics.regions.insert_and_shift_ids(RegionId::ZERO, RegionVar { index: RegionId::ZERO, name: None });
 
         Ok(generics)
     }
@@ -987,7 +985,7 @@ impl<'a> DropShimCtx<'a> {
         // Create a new variable with var := &mut drop_place
         // This is the argument to the drop function
         let drop_place_ref = self.new_var(None, Ty::new(TyKind::Ref(
-            Region::Erased,
+            Region::Var(DeBruijnVar::new_at_zero(RegionId::ZERO)),
             drop_place.ty().clone(),
             RefKind::Mut,
         )));
@@ -1255,7 +1253,7 @@ impl<'a> DropShimCtx<'a> {
             }
             _ => {
                 let concrete_place = locals.new_var(Some("concrete".into()), Ty::new(TyKind::Ref(
-                    Region::Erased,
+                    Region::Var(DeBruijnVar::new_at_zero(RegionId::ZERO)),
                     concrete_ty.clone(),
                     RefKind::Mut,
                 )));
@@ -1267,12 +1265,7 @@ impl<'a> DropShimCtx<'a> {
                         Rvalue::UnaryOp(
                             UnOp::Cast(CastKind::Concretize(
                                 dyn_trait_param_ty.clone(),
-                                TyKind::Ref(
-                                    Region::Erased,
-                                    concrete_ty.clone(),
-                                    RefKind::Mut,
-                                )
-                                .into_ty(),
+                                concrete_place.ty.clone(),
                             )),
                             Operand::Move(locals.place_for_var(LocalId::new(1))),
                         ),
diff --git a/charon/tests/ui/monomorphization/dyn-trait.out b/charon/tests/ui/monomorphization/dyn-trait.out
@@ -124,7 +124,7 @@ note: the error occurred when translating `core::marker::MetaSized::<type_error(
 7 |     x.to_string()
   |     -------------
 
-thread 'rustc' panicked at /home/ssyram/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/index_vec-0.1.4/src/indexing.rs:128:10:
+thread 'rustc' panicked at /Users/ssyram/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/index_vec-0.1.4/src/indexing.rs:128:10:
 index out of bounds: the len is 0 but the index is 0
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
 error: Thread panicked when extracting item `alloc::string::{impl#23}`.
diff --git a/charon/tests/ui/monomorphization/unsatisfied-method-bounds.out b/charon/tests/ui/monomorphization/unsatisfied-method-bounds.out
@@ -57,7 +57,7 @@ error: Error during trait resolution: Could not find a clause for `Binder { valu
 
 disabled backtrace
 warning[E9999]: Could not find a clause for `Binder { value: <std::string::String as std::marker::Copy>, bound_vars: [] }` in the current context: `Unimplemented`
-   --> /home/ssyram/.rustup/toolchains/nightly-2025-07-08-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/drop.rs:208:1
+   --> /Users/ssyram/.rustup/toolchains/nightly-2025-07-08-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/ops/drop.rs:208:1
     |
 208 | pub trait Drop {
     | ^^^^^^^^^^^^^^
@@ -67,7 +67,7 @@ warning[E9999]: Could not find a clause for `Binder { value: <std::string::Strin
 
 disabled backtrace
 warning[E9999]: Could not find a clause for `Binder { value: <std::string::String as std::marker::Copy>, bound_vars: [] }` in the current context: `Unimplemented`
-   --> /home/ssyram/.rustup/toolchains/nightly-2025-07-08-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/drop.rs:241:5
+   --> /Users/ssyram/.rustup/toolchains/nightly-2025-07-08-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/ops/drop.rs:241:5
     |
 241 |     fn drop(&mut self);
     |     ^^^^^^^^^^^^^^^^^^^
@@ -77,7 +77,7 @@ warning[E9999]: Could not find a clause for `Binder { value: <std::string::Strin
 
 disabled backtrace
 warning[E9999]: Could not find a clause for `Binder { value: <std::string::String as std::marker::Copy>, bound_vars: [] }` in the current context: `Unimplemented`
-   --> /home/ssyram/.rustup/toolchains/nightly-2025-07-08-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/marker.rs:179:1
+   --> /Users/ssyram/.rustup/toolchains/nightly-2025-07-08-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/marker.rs:179:1
     |
 179 | pub trait MetaSized: PointeeSized {
     | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out
@@ -196,16 +196,16 @@ impl Clone for String {
 // Full name: alloc::string::{impl Display for String}::fmt
 pub fn {impl Display for String}::fmt<'_0, '_1, '_2>(@1: &'_0 (String), @2: &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized<Error>]
 
-fn {{impl Display for String}}::{vtable}::{drop_method}<'_0>(@1: &'_ mut ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)))
+fn {{impl Display for String}}::{vtable}::{drop_method}<'_0>(@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)))
 {
     let ret@0: (); // return
-    let self@1: &'_ mut ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)); // arg #1
-    let concrete@2: &'_ mut (String); // local
-    let @3: &'_ mut (String); // anonymous local
+    let self@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)); // arg #1
+    let concrete@2: &'_0 mut (String); // local
+    let @3: &'_0 mut (String); // anonymous local
 
     storage_live(concrete@2)
     storage_live(@3)
-    concrete@2 := concretize<&'_ mut ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)), &'_ mut (String)>(move (self@1))
+    concrete@2 := concretize<&'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)), &'_0 mut (String)>(move (self@1))
     @3 := &mut *(concrete@2)
     ret@0 := {impl Drop for String}::drop<'_0>(move (@3))
     ret@0 := ()
diff --git a/charon/tests/ui/vtable-simple.out b/charon/tests/ui/vtable-simple.out
@@ -87,13 +87,13 @@ where
     return
 }
 
-fn {{impl Modifiable<T> for i32}}::{vtable}::{drop_method}<'_0, T>(@1: &'_ mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)))
+fn {{impl Modifiable<T> for i32}}::{vtable}::{drop_method}<'_0, T>(@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)))
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Clone<T>,
 {
     let ret@0: (); // return
-    let self@1: &'_ mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)); // arg #1
+    let self@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)); // arg #1
 
     ret@0 := ()
     return
diff --git a/charon/tests/ui/vtables.out b/charon/tests/ui/vtables.out

Original file line number	Diff line number	Diff line change
`@@ -87,13 +87,13 @@ where`
`87`	`87`	`return`
`88`	`88`	`}`
`89`	`89`
`90`		`-fn {{impl Modifiable<T> for i32}}::{vtable}::{drop_method}<'_0, T>(@1: &'_ mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)))`
	`90`	`+fn {{impl Modifiable<T> for i32}}::{vtable}::{drop_method}<'_0, T>(@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)))`
`91`	`91`	`where`
`92`	`92`	`[@TraitClause0]: Sized<T>,`
`93`	`93`	`[@TraitClause1]: Clone<T>,`
`94`	`94`	`{`
`95`	`95`	`let ret@0: (); // return`
`96`		`- let self@1: &'_ mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)); // arg #1`
	`96`	`+ let self@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)); // arg #1`
`97`	`97`
`98`	`98`	`ret@0 := ()`
`99`	`99`	`return`