Resolve Drop calls

cli/driver/src/exporter.rs

@@ -194,6 +194,7 @@ impl From<ExtractionCallbacks> for hax_frontend_exporter_options::Options {
     fn from(opts: ExtractionCallbacks) -> hax_frontend_exporter_options::Options {
         hax_frontend_exporter_options::Options {
             inline_anon_consts: true,
+            resolve_drop_bounds: false,
         }
     }
 }

engine/lib/concrete_ident/concrete_ident.ml

@@ -483,7 +483,7 @@ module MakeRenderAPI (NP : NAME_POLICY) : RENDER_API = struct
       let*? _no_generics = List.is_empty impl_infos.generics.params in
       match impl_infos.trait_ref with
       | None -> Some ty
-      | Some { def_id = trait; generic_args = [ _self ] } ->
+      | Some { def_id = trait; generic_args = [ _self ]; _ } ->
           let* trait = Explicit_def_id.of_def_id trait in
           let trait = View.of_def_id trait in
           let*? _same_ns = [%eq: View.ModPath.t] namespace trait.mod_path in

engine/lib/import_thir.ml

@@ -1147,6 +1147,7 @@ end) : EXPR = struct
     | Dyn -> Dyn
     | SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path
     | Builtin { trait; _ } -> Builtin (c_trait_ref span trait.value)
+    | Drop _ -> failwith @@ "impl_expr_atom: Drop"
     | Error str -> failwith @@ "impl_expr_atom: Error " ^ str
 
   and c_generic_value (span : Thir.span) (ty : Thir.generic_arg) : generic_value

frontend/exporter/options/src/lib.rs

@@ -101,4 +101,7 @@ pub struct Options {
     /// blocks or advanced constant expressions as in `[T; N+1]`), or refer to them as
     /// `GlobalName`s.
     pub inline_anon_consts: bool,
+    /// Add `T: Drop` bounds to every type generic, so that we can build `ImplExpr`s to know what
+    /// code is run on drop.
+    pub resolve_drop_bounds: bool,
 }

frontend/exporter/src/traits.rs

@@ -93,6 +93,11 @@ pub enum ImplExprAtom {
     /// `dyn Trait` implements `Trait` using a built-in implementation; this refers to that
     /// built-in implementation.
     Dyn,
+    /// A virtual `Drop` implementation.
+    /// `Drop` doesn't work like a real trait but we want to pretend it does. If a type has a
+    /// user-defined `impl Drop for X` we just use the `Concrete` variant, but if it doesn't we use
+    /// this variant to supply the data needed to know what code will run on drop.
+    Drop(DropData),
     /// A built-in trait whose implementation is computed by the compiler, such as `FnMut`. This
     /// morally points to an invisible `impl` block; as such it contains the information we may
     /// need from one.
@@ -109,6 +114,30 @@ pub enum ImplExprAtom {
     Error(String),
 }
 
+#[derive(AdtInto)]
+#[args(<'tcx, S: UnderOwnerState<'tcx> >, from: resolution::DropData<'tcx>, state: S as s)]
+#[derive_group(Serializers)]
+#[derive(Clone, Debug, Hash, PartialEq, Eq, PartialOrd, Ord, JsonSchema)]
+pub enum DropData {
+    /// A drop that does nothing, e.g. for scalars and pointers.
+    Noop,
+    /// An implicit `Drop` local clause, if the `resolve_drop_bounds` option is `false`. If that
+    /// option is `true`, we'll add `Drop` bounds to every type param, and use that to resolve
+    /// `Drop` impls of generics. If it's `false`, we use this variant to indicate that the drop
+    /// clause comes from a generic or associated type.
+    Implicit,
+    /// The implicit `Drop` impl that exists for every type without an explicit `Drop` impl. The
+    /// virtual impl is considered to have one `T: Drop` bound for each generic argument of the
+    /// target type; it then simply drops each field in order.
+    Glue {
+        /// The type we're generating glue for.
+        ty: Ty,
+        /// The `ImplExpr`s for the `T: Drop` bounds of the virtual impl. There is one for each
+        /// generic argument, in order.
+        impl_exprs: Vec<ImplExpr>,
+    },
+}
+
 /// An `ImplExpr` describes the full data of a trait implementation. Because of generics, this may
 /// need to combine several concrete trait implementation items. For example, `((1u8, 2u8),
 /// "hello").clone()` combines the generic implementation of `Clone` for `(A, B)` with the
@@ -173,7 +202,13 @@ pub fn solve_trait<'tcx, S: BaseState<'tcx> + HasOwnerId>(
     let resolved = s.with_cache(|cache| {
         cache
             .predicate_searcher
-            .get_or_insert_with(|| PredicateSearcher::new_for_owner(s.base().tcx, s.owner_id()))
+            .get_or_insert_with(|| {
+                PredicateSearcher::new_for_owner(
+                    s.base().tcx,
+                    s.owner_id(),
+                    s.base().options.resolve_drop_bounds,
+                )
+            })
             .resolve(&trait_ref, &warn)
     });
     let impl_expr = match resolved {
@@ -209,7 +244,7 @@ pub fn solve_item_required_traits<'tcx, S: UnderOwnerState<'tcx>>(
             }
             _ => {}
         }
-        let predicates = required_predicates(tcx, def_id);
+        let predicates = required_predicates(tcx, def_id, s.base().options.resolve_drop_bounds);
         impl_exprs.extend(solve_item_traits_inner(s, generics, predicates));
     }
     let mut impl_exprs = vec![];
@@ -226,7 +261,7 @@ pub fn solve_item_implied_traits<'tcx, S: UnderOwnerState<'tcx>>(
     def_id: RDefId,
     generics: ty::GenericArgsRef<'tcx>,
 ) -> Vec<ImplExpr> {
-    let predicates = implied_predicates(s.base().tcx, def_id);
+    let predicates = implied_predicates(s.base().tcx, def_id, s.base().options.resolve_drop_bounds);
     solve_item_traits_inner(s, generics, predicates)
 }