Resolve polymorphic drops

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.109"
+let supported_charon_version = "0.1.110"

charon-ml/src/OfJsonBasic.ml

@@ -56,6 +56,18 @@ let pair_of_json (a_of_json : 'ctx -> json -> ('a, string) result)
       Ok (a, b)
   | _ -> Error ("pair_of_json failed on: " ^ show js)
 
+let triple_of_json (a_of_json : 'ctx -> json -> ('a, string) result)
+    (b_of_json : 'ctx -> json -> ('b, string) result)
+    (c_of_json : 'ctx -> json -> ('c, string) result) (ctx : 'ctx) (js : json) :
+    ('a * 'b * 'c, string) result =
+  match js with
+  | `List [ a; b; c ] ->
+      let* a = a_of_json ctx a in
+      let* b = b_of_json ctx b in
+      let* c = c_of_json ctx c in
+      Ok (a, b, c)
+  | _ -> Error ("triple_of_json failed on: " ^ show js)
+
 let list_of_json (a_of_json : 'ctx -> json -> ('a, string) result) (ctx : 'ctx)
     (js : json) : ('a list, string) result =
   combine_error_msgs js "list_of_json"

charon-ml/src/PrintLlbcAst.ml

@@ -36,7 +36,7 @@ module Ast = struct
     | StorageDead var_id ->
         indent ^ "storage_dead " ^ local_id_to_string env var_id
     | Deinit p -> indent ^ "deinit " ^ place_to_string env p
-    | Drop p -> indent ^ "drop " ^ place_to_string env p
+    | Drop (p, _) -> indent ^ "drop " ^ place_to_string env p
     | Assert a -> assertion_to_string env indent a
     | Call call -> call_to_string env indent call
     | Abort (Panic _) -> indent ^ "panic"

charon-ml/src/PrintUllbcAst.ml

@@ -33,7 +33,7 @@ module Ast = struct
     | StorageDead var_id ->
         indent ^ "storage_dead " ^ local_id_to_string env var_id
     | Deinit p -> indent ^ "deinit " ^ place_to_string env p
-    | Drop p -> indent ^ "drop " ^ place_to_string env p
+    | Drop (p, _) -> indent ^ "drop " ^ place_to_string env p
     | CopyNonOverlapping { src; dst; count } ->
         indent ^ "copy_non_overlapping(" ^ operand_to_string env src ^ ", "
         ^ operand_to_string env dst ^ ", "

charon-ml/src/generated/Generated_GAst.ml

@@ -337,6 +337,9 @@ type cli_options = {
           trait definitions to be mutually recursive with their method
           declarations. This flag removes [Self] clauses that aren't used to
           break this mutual recursion. *)
+  add_drop_bounds : bool;
+      (** Whether to add [Drop] bounds everywhere to enable proper tracking of
+          what code runs on a given [drop] 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-ml/src/generated/Generated_GAstOfJson.ml

@@ -316,6 +316,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
           ("remove_associated_types", remove_associated_types);
           ("hide_marker_traits", hide_marker_traits);
           ("remove_unused_self_clauses", remove_unused_self_clauses);
+          ("add_drop_bounds", add_drop_bounds);
           ("start_from", start_from);
           ("no_cargo", no_cargo);
           ("rustc_args", rustc_args);
@@ -357,6 +358,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
         let* remove_unused_self_clauses =
           bool_of_json ctx remove_unused_self_clauses
         in
+        let* add_drop_bounds = bool_of_json ctx add_drop_bounds in
         let* start_from = list_of_json string_of_json ctx start_from in
         let* no_cargo = bool_of_json ctx no_cargo in
         let* rustc_args = list_of_json string_of_json ctx rustc_args in
@@ -397,6 +399,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
              remove_associated_types;
              hide_marker_traits;
              remove_unused_self_clauses;
+             add_drop_bounds;
              start_from;
              no_cargo;
              rustc_args;
@@ -1708,7 +1711,8 @@ and trait_instance_id_of_json (ctx : of_json_ctx) (js : json) :
         in
         let* types =
           list_of_json
-            (pair_of_json trait_item_name_of_json ty_of_json)
+            (triple_of_json trait_item_name_of_json ty_of_json
+               (vector_of_json trait_clause_id_of_json trait_ref_of_json))
             ctx types
         in
         Ok (BuiltinOrAuto (trait_decl_ref, parent_trait_refs, types))

charon-ml/src/generated/Generated_LlbcAst.ml

@@ -29,7 +29,7 @@ and raw_statement =
           the function's body, in which case it is implicitly deallocated at the
           end of the function. *)
   | Deinit of place
-  | Drop of place
+  | Drop of place * trait_ref
       (** Drop the value at the given place.
 
           For MIR built and promoted, this is a conditional drop: the value will

charon-ml/src/generated/Generated_LlbcOfJson.ml

@@ -40,9 +40,10 @@ and raw_statement_of_json (ctx : of_json_ctx) (js : json) :
     | `Assoc [ ("Deinit", deinit) ] ->
         let* deinit = place_of_json ctx deinit in
         Ok (Deinit deinit)
-    | `Assoc [ ("Drop", drop) ] ->
-        let* drop = place_of_json ctx drop in
-        Ok (Drop drop)
+    | `Assoc [ ("Drop", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = place_of_json ctx x_0 in
+        let* x_1 = trait_ref_of_json ctx x_1 in
+        Ok (Drop (x_0, x_1))
     | `Assoc [ ("Assert", assert_) ] ->
         let* assert_ = assertion_of_json ctx assert_ in
         Ok (Assert assert_)

charon-ml/src/generated/Generated_Types.ml

@@ -327,7 +327,7 @@ and trait_instance_id =
   | BuiltinOrAuto of
       trait_decl_ref region_binder
       * trait_ref list
-      * (trait_item_name * ty) list
+      * (trait_item_name * ty * trait_ref list) list
       (** A trait implementation that is computed by the compiler, such as for
           built-in trait [Sized]. This morally points to an invisible [impl]
           block; as such it contains the information we may need from one.

charon-ml/src/generated/Generated_UllbcAst.ml

@@ -29,7 +29,7 @@ and raw_statement =
           the function's body, in which case it is implicitly deallocated at the
           end of the function. *)
   | Deinit of place
-  | Drop of place
+  | Drop of place * trait_ref
   | Assert of assertion
       (** A built-in assert, which corresponds to runtime checks that we remove,
           namely: bounds checks, over/underflow checks, div/rem by zero checks,

charon-ml/src/generated/Generated_UllbcOfJson.ml

@@ -54,9 +54,10 @@ and raw_statement_of_json (ctx : of_json_ctx) (js : json) :
     | `Assoc [ ("Deinit", deinit) ] ->
         let* deinit = place_of_json ctx deinit in
         Ok (Deinit deinit)
-    | `Assoc [ ("Drop", drop) ] ->
-        let* drop = place_of_json ctx drop in
-        Ok (Drop drop)
+    | `Assoc [ ("Drop", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = place_of_json ctx x_0 in
+        let* x_1 = trait_ref_of_json ctx x_1 in
+        Ok (Drop (x_0, x_1))
     | `Assoc [ ("Assert", assert_) ] ->
         let* assert_ = assertion_of_json ctx assert_ in
         Ok (Assert assert_)

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.109"
+version = "0.1.110"
 authors = [
     "Son Ho <hosonmarc@gmail.com>",
     "Guillaume Boisseau <nadrieril+git@gmail.com>",

charon/src/ast/llbc_ast.rs

@@ -41,7 +41,7 @@ pub enum RawStatement {
     /// it has not already been moved out. For MIR elaborated and optimized, this is a real drop.
     ///
     /// This drop is then equivalent to a call to `std::ptr::drop_in_place(&raw mut place)`.
-    Drop(Place),
+    Drop(Place, TraitRef),
     Assert(Assert),
     Call(Call),
     /// Panic also handles "unreachable". We keep the name of the panicking function that was

charon/src/ast/meta.rs

@@ -136,7 +136,7 @@ pub struct RawAttribute {
 }
 
 /// Information about the attributes and visibility of an item, field or variant..
-#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
+#[derive(Debug, Default, Clone, Serialize, Deserialize, Drive, DriveMut)]
 pub struct AttrInfo {
     /// Attributes (`#[...]`).
     pub attributes: Vec<Attribute>,

charon/src/ast/types.rs

@@ -130,7 +130,7 @@ pub enum TraitRefKind {
         /// FnOnce`.
         parent_trait_refs: Vector<TraitClauseId, TraitRef>,
         /// The values of the associated types for this trait.
-        types: Vec<(TraitItemName, Ty)>,
+        types: Vec<(TraitItemName, Ty, Vector<TraitClauseId, TraitRef>)>,
     },
 
     /// The automatically-generated implementation for `dyn Trait`.

charon/src/ast/types_utils.rs

@@ -656,6 +656,27 @@ impl TypeDeclRef {
     }
 }
 
+impl TraitRef {
+    pub fn new_builtin(
+        trait_id: TraitDeclId,
+        ty: Ty,
+        parents: Vector<TraitClauseId, TraitRef>,
+    ) -> Self {
+        let trait_decl_ref = RegionBinder::empty(TraitDeclRef {
+            id: trait_id,
+            generics: Box::new(GenericArgs::new_types([ty].into())),
+        });
+        TraitRef {
+            kind: TraitRefKind::BuiltinOrAuto {
+                trait_decl_ref: trait_decl_ref.clone(),
+                parent_trait_refs: parents,
+                types: Default::default(),
+            },
+            trait_decl_ref,
+        }
+    }
+}
+
 impl Field {
     /// The new name for this field, as suggested by the `#[charon::rename]` attribute.
     pub fn renamed_name(&self) -> Option<&str> {

charon/src/ast/ullbc_ast.rs

@@ -36,7 +36,7 @@ pub enum RawStatement {
     /// is implicitly deallocated at the end of the function.
     StorageDead(LocalId),
     Deinit(Place),
-    Drop(Place),
+    Drop(Place, TraitRef),
     /// A built-in assert, which corresponds to runtime checks that we remove, namely: bounds
     /// checks, over/underflow checks, div/rem by zero checks, pointer alignement check.
     Assert(Assert),

charon/src/ast/visitor.rs

@@ -55,6 +55,7 @@ use indexmap::IndexMap;
         for<T: AstVisitable> Box<T>,
         for<T: AstVisitable> Option<T>,
         for<A: AstVisitable, B: AstVisitable> (A, B),
+        for<A: AstVisitable, B: AstVisitable, C: AstVisitable> (A, B, C),
         for<A: AstVisitable, B: AstVisitable> Result<A, B>,
         for<A: AstVisitable, B: AstVisitable> OutlivesPred<A, B>,
         for<T: AstVisitable> Vec<T>,
@@ -143,6 +144,7 @@ impl<K: Any, T: AstVisitable> AstVisitable for IndexMap<K, T> {
         AbortKind, BinOp, BorrowKind, ConstantExpr, ConstGeneric, FieldId, FieldProjKind,
         TypeDeclRef, FunDeclId, FunIdOrTraitMethodRef, GenericArgs, GlobalDeclRef, IntegerTy,
         NullOp, RefKind, ScalarValue, Span, Ty, TypeDeclId, TypeId, UnOp, VariantId, LocalId,
+        TraitRef,
     ),
     // Types that we unconditionally explore.
     drive(
@@ -155,6 +157,7 @@ impl<K: Any, T: AstVisitable> AstVisitable for IndexMap<K, T> {
         for<T: BodyVisitable> Option<T>,
         for<T: BodyVisitable, E: BodyVisitable> Result<T, E>,
         for<A: BodyVisitable, B: BodyVisitable> (A, B),
+        for<A: BodyVisitable, B: BodyVisitable, C: BodyVisitable> (A, B, C),
         for<T: BodyVisitable> Vec<T>,
         for<I: Idx, T: BodyVisitable> Vector<I, T>,
     ),

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

@@ -5,6 +5,7 @@ pub mod translate_closures;
 pub mod translate_constants;
 pub mod translate_crate;
 pub mod translate_ctx;
+pub mod translate_drops;
 pub mod translate_functions;
 pub mod translate_generics;
 pub mod translate_items;

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

@@ -814,12 +814,14 @@ impl BodyTransCtx<'_, '_, '_> {
             TerminatorKind::Unreachable => RawTerminator::Abort(AbortKind::UndefinedBehavior),
             TerminatorKind::Drop {
                 place,
+                impl_expr,
                 target,
                 unwind: _, // We consider that panic is an error, and don't model unwinding
                 ..
             } => {
                 let place = self.translate_place(span, place)?;
-                statements.push(Statement::new(span, RawStatement::Drop(place)));
+                let tref = self.translate_trait_impl_expr(span, impl_expr)?;
+                statements.push(Statement::new(span, RawStatement::Drop(place, tref)));
                 let target = self.translate_basic_block_id(*target);
                 RawTerminator::Goto { target }
             }

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

@@ -632,32 +632,35 @@ impl ItemTransCtx<'_, '_> {
         let input = Ty::mk_tuple(inputs);
 
         let parent_trait_refs = {
-            // Makes a built-in trait ref for `ty: trait`.
-            let builtin_tref = |trait_id, ty| {
-                let generics = Box::new(GenericArgs::new_types([ty].into()));
-                let trait_decl_ref = TraitDeclRef {
-                    id: trait_id,
-                    generics,
-                };
-                let trait_decl_ref = RegionBinder::empty(trait_decl_ref);
-                TraitRef {
-                    kind: TraitRefKind::BuiltinOrAuto {
-                        trait_decl_ref: trait_decl_ref.clone(),
-                        parent_trait_refs: Vector::new(),
-                        types: vec![],
-                    },
-                    trait_decl_ref,
-                }
-            };
-
+            let input_is_meta_sized =
+                TraitRef::new_builtin(meta_sized_trait, input.clone(), Default::default());
+            let input_is_sized = TraitRef::new_builtin(
+                sized_trait,
+                input.clone(),
+                [input_is_meta_sized.clone()].into(),
+            );
+            let input_is_tuple = TraitRef::new_builtin(
+                tuple_trait,
+                input.clone(),
+                [input_is_meta_sized.clone()].into(),
+            );
             match target_kind {
-                ClosureKind::FnOnce => [
-                    builtin_tref(meta_sized_trait, input.clone()),
-                    builtin_tref(sized_trait, input.clone()),
-                    builtin_tref(tuple_trait, input.clone()),
-                    builtin_tref(sized_trait, output.clone()),
-                ]
-                .into(),
+                ClosureKind::FnOnce => {
+                    let output_is_meta_sized =
+                        TraitRef::new_builtin(meta_sized_trait, output.clone(), Default::default());
+                    let output_is_sized = TraitRef::new_builtin(
+                        sized_trait,
+                        output.clone(),
+                        [output_is_meta_sized].into(),
+                    );
+                    [
+                        input_is_meta_sized,
+                        input_is_sized,
+                        input_is_tuple,
+                        output_is_sized,
+                    ]
+                    .into()
+                }
                 ClosureKind::FnMut | ClosureKind::Fn => {
                     let parent_kind = match target_kind {
                         ClosureKind::FnOnce => unreachable!(),
@@ -673,10 +676,10 @@ impl ItemTransCtx<'_, '_> {
                         trait_decl_ref: RegionBinder::empty(parent_predicate),
                     };
                     [
-                        builtin_tref(meta_sized_trait, input.clone()),
+                        input_is_meta_sized,
                         parent_trait_ref,
-                        builtin_tref(sized_trait, input.clone()),
-                        builtin_tref(tuple_trait, input.clone()),
+                        input_is_sized,
+                        input_is_tuple,
                     ]
                     .into()
                 }