From f08de391772cb03ec0e19c5a4ba7ffe3f0e04882 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 14 Feb 2025 18:07:06 +0100 Subject: [PATCH] Clarify uses of `Vector::len` The fact that the vector need not be contiguous is a footgun, we should fix that. --- charon/src/ast/expressions_utils.rs | 10 ++-- charon/src/ast/types_utils.rs | 45 ++++++++-------- .../charon-driver/translate/translate_ctx.rs | 2 +- .../translate/translate_functions_to_ullbc.rs | 12 +++-- .../translate/translate_types.rs | 2 +- charon/src/bin/generate-ml/main.rs | 14 ++--- charon/src/ids/vector.rs | 54 ++++++++++--------- charon/src/name_matcher/mod.rs | 4 +- charon/src/transform/check_generics.rs | 2 +- charon/src/transform/duplicate_return.rs | 3 +- charon/src/transform/hide_marker_traits.rs | 18 +++---- .../transform/inline_local_panic_functions.rs | 2 +- .../transform/update_closure_signatures.rs | 4 +- charon/tests/crate_data.rs | 6 ++- ...lt-method-with-clause-and-marker-trait.out | 48 +++++++++++++++++ ...ult-method-with-clause-and-marker-trait.rs | 17 ++++++ 16 files changed, 162 insertions(+), 81 deletions(-) create mode 100644 charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out create mode 100644 charon/tests/ui/simple/default-method-with-clause-and-marker-trait.rs diff --git a/charon/src/ast/expressions_utils.rs b/charon/src/ast/expressions_utils.rs index 52f90789..60bf5ef4 100644 --- a/charon/src/ast/expressions_utils.rs +++ b/charon/src/ast/expressions_utils.rs @@ -85,14 +85,14 @@ impl ProjectionElem { let type_decl = type_decls.get(*type_decl_id).ok_or(())?; let (type_id, generics) = ty.as_adt().ok_or(())?; assert!(TypeId::Adt(*type_decl_id) == type_id); - assert!(generics.regions.len() == type_decl.generics.regions.len()); - assert!(generics.types.len() == type_decl.generics.types.len()); + assert!(generics.regions.elem_count() == type_decl.generics.regions.elem_count()); + assert!(generics.types.elem_count() == type_decl.generics.types.elem_count()); assert!( - generics.const_generics.len() - == type_decl.generics.const_generics.len() + generics.const_generics.elem_count() + == type_decl.generics.const_generics.elem_count() ); assert!( - generics.trait_refs.len() == type_decl.generics.trait_clauses.len() + generics.trait_refs.elem_count() == type_decl.generics.trait_clauses.elem_count() ); use TypeDeclKind::*; match &type_decl.kind { diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index fa46898e..6ebc5a78 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -61,13 +61,13 @@ impl GenericParams { types_outlive, trait_type_constraints, } = self; - regions.len() - + types.len() - + const_generics.len() - + trait_clauses.len() + regions.elem_count() + + types.elem_count() + + const_generics.elem_count() + + trait_clauses.elem_count() + regions_outlive.len() + types_outlive.len() - + trait_type_constraints.len() + + trait_type_constraints.elem_count() } /// Construct a set of generic arguments in the scope of `self` that matches `self` and feeds @@ -151,28 +151,28 @@ impl Binder> { if let Region::Var(var) = x && let Some(id) = var.bound_at_depth_mut(self.binder_depth) { - *id += self.shift_by.regions.len(); + *id += self.shift_by.regions.slot_count(); } } fn enter_ty_kind(&mut self, x: &mut TyKind) { if let TyKind::TypeVar(var) = x && let Some(id) = var.bound_at_depth_mut(self.binder_depth) { - *id += self.shift_by.types.len(); + *id += self.shift_by.types.slot_count(); } } fn enter_const_generic(&mut self, x: &mut ConstGeneric) { if let ConstGeneric::Var(var) = x && let Some(id) = var.bound_at_depth_mut(self.binder_depth) { - *id += self.shift_by.const_generics.len(); + *id += self.shift_by.const_generics.slot_count(); } } fn enter_trait_ref_kind(&mut self, x: &mut TraitRefKind) { if let TraitRefKind::Clause(var) = x && let Some(id) = var.bound_at_depth_mut(self.binder_depth) { - *id += self.shift_by.trait_clauses.len(); + *id += self.shift_by.trait_clauses.slot_count(); } } } @@ -199,19 +199,19 @@ impl Binder> { inner_params .regions .iter_mut() - .for_each(|v| v.index += outer_params.regions.len()); + .for_each(|v| v.index += outer_params.regions.slot_count()); inner_params .types .iter_mut() - .for_each(|v| v.index += outer_params.types.len()); + .for_each(|v| v.index += outer_params.types.slot_count()); inner_params .const_generics .iter_mut() - .for_each(|v| v.index += outer_params.const_generics.len()); + .for_each(|v| v.index += outer_params.const_generics.slot_count()); inner_params .trait_clauses .iter_mut() - .for_each(|v| v.clause_id += outer_params.trait_clauses.len()); + .for_each(|v| v.clause_id += outer_params.trait_clauses.slot_count()); let GenericParams { regions, @@ -285,7 +285,10 @@ impl GenericArgs { trait_refs, target: _, } = self; - regions.len() + types.len() + const_generics.len() + trait_refs.len() + regions.elem_count() + + types.elem_count() + + const_generics.elem_count() + + trait_refs.elem_count() } pub fn is_empty(&self) -> bool { @@ -334,10 +337,10 @@ impl GenericArgs { /// Check whether this matches the given `GenericParams`. /// TODO: check more things, e.g. that the trait refs use the correct trait and generics. pub fn matches(&self, params: &GenericParams) -> bool { - params.regions.len() == self.regions.len() - && params.types.len() == self.types.len() - && params.const_generics.len() == self.const_generics.len() - && params.trait_clauses.len() == self.trait_refs.len() + params.regions.elem_count() == self.regions.elem_count() + && params.types.elem_count() == self.types.elem_count() + && params.const_generics.elem_count() == self.const_generics.elem_count() + && params.trait_clauses.elem_count() == self.trait_refs.elem_count() } /// Return the same generics, but where we pop the first type arguments. @@ -541,7 +544,7 @@ impl Ty { match self.kind() { TyKind::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => { assert!(generics.regions.is_empty()); - assert!(generics.types.len() == 1); + assert!(generics.types.elem_count() == 1); assert!(generics.const_generics.is_empty()); true } @@ -553,7 +556,7 @@ impl Ty { match self.kind() { TyKind::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => { assert!(generics.regions.is_empty()); - assert!(generics.types.len() == 1); + assert!(generics.types.elem_count() == 1); assert!(generics.const_generics.is_empty()); Some(&generics.types[0]) } @@ -565,7 +568,7 @@ impl Ty { match self.kind() { TyKind::Adt(TypeId::Builtin(BuiltinTy::Array | BuiltinTy::Slice), generics) => { assert!(generics.regions.is_empty()); - assert!(generics.types.len() == 1); + assert!(generics.types.elem_count() == 1); Some(&generics.types[0]) } _ => None, diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 927e34f7..91e3a871 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -1107,7 +1107,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { .0; // Iterate over the binders, starting from the outermost. for (dbid, bl) in self.binding_levels.iter_enumerated().rev() { - let num_clauses_bound_at_this_level = bl.params.trait_clauses.len(); + let num_clauses_bound_at_this_level = bl.params.trait_clauses.elem_count(); if id < num_clauses_bound_at_this_level || dbid == innermost_item_binder_id { let id = TraitClauseId::from_usize(id); return Ok(DeBruijnVar::bound(dbid, id)); diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs index c791d650..e0ea6d80 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs @@ -289,7 +289,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { // This case only happens in some MIR levels assert!(!boxes_are_desugared(self.t_ctx.options.mir_level)); assert!(generics.regions.is_empty()); - assert!(generics.types.len() == 1); + assert!(generics.types.elem_count() == 1); assert!(generics.const_generics.is_empty()); } _ => { @@ -308,7 +308,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { Tuple(id) => { let (_, generics) = subplace.ty().kind().as_adt().unwrap(); let field_id = translate_field_id(*id); - let proj_kind = FieldProjKind::Tuple(generics.types.len()); + let proj_kind = FieldProjKind::Tuple(generics.types.elem_count()); ProjectionElem::Field(proj_kind, field_id) } Adt { @@ -327,7 +327,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { assert!(generics.regions.is_empty()); assert!(variant.is_none()); assert!(generics.const_generics.is_empty()); - let proj_kind = FieldProjKind::Tuple(generics.types.len()); + let proj_kind = + FieldProjKind::Tuple(generics.types.elem_count()); ProjectionElem::Field(proj_kind, field_id) } @@ -336,7 +337,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { // Some more sanity checks assert!(generics.regions.is_empty()); - assert!(generics.types.len() == 1); + assert!(generics.types.elem_count() == 1); assert!(generics.const_generics.is_empty()); assert!(variant_id.is_none()); assert!(field_id == FieldId::ZERO); @@ -556,7 +557,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { // destination type. At runtime, the converse happens: the length // materializes into the fat pointer. assert!( - generics.types.len() == 1 && generics.const_generics.len() == 1 + generics.types.elem_count() == 1 + && generics.const_generics.elem_count() == 1 ); assert!(generics.types[0] == generics1.types[0]); assert!(kind1 == kind2); diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 781353d4..0605e8d4 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -158,7 +158,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { // TODO: do this in a micro-pass if let TypeId::Builtin(builtin_ty) = type_id { let used_args = builtins::type_to_used_params(builtin_ty); - error_assert!(self, span, generics.types.len() == used_args.len()); + error_assert!(self, span, generics.types.elem_count() == used_args.len()); let types = std::mem::take(&mut generics.types) .into_iter() .zip(used_args) diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index 93ace7e5..b4052629 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -195,7 +195,7 @@ fn type_to_ocaml_call(ctx: &GenerateCtx, ty: &Ty) -> String { } TypeId::Builtin(BuiltinTy::Box) => expr.insert(0, "box_of_json".to_owned()), TypeId::Tuple => { - let name = match generics.types.len() { + let name = match generics.types.elem_count() { 2 => "pair_of_json".to_string(), 3 => "triple_of_json".to_string(), len => format!("tuple_{len}_of_json"), @@ -356,7 +356,8 @@ fn type_decl_to_json_deserializer(ctx: &GenerateCtx, decl: &TypeDecl) -> String build_branch(ctx, "`Null", fields, "()") } TypeDeclKind::Struct(fields) - if fields.len() == 1 && fields[0].name.as_ref().is_some_and(|name| name == "_raw") => + if fields.elem_count() == 1 + && fields[0].name.as_ref().is_some_and(|name| name == "_raw") => { // These are the special strongly-typed integers. let short_name = decl @@ -372,7 +373,7 @@ fn type_decl_to_json_deserializer(ctx: &GenerateCtx, decl: &TypeDecl) -> String format!("| x -> {short_name}.id_of_json ctx x") } TypeDeclKind::Struct(fields) - if fields.len() == 1 + if fields.elem_count() == 1 && (fields[0].name.is_none() || decl .item_meta @@ -458,7 +459,7 @@ fn type_decl_to_json_deserializer(ctx: &GenerateCtx, decl: &TypeDecl) -> String let mut fields = variant.fields.clone(); let inner_pat = if fields.iter().all(|f| f.name.is_none()) { // Tuple variant - if variant.fields.len() == 1 { + if variant.fields.elem_count() == 1 { let var = make_ocaml_ident(&variant.name); fields[0].name = Some(var.clone()); var @@ -581,7 +582,8 @@ fn type_decl_to_ocaml_decl(ctx: &GenerateCtx, decl: &TypeDecl, co_rec: bool) -> } TypeDeclKind::Struct(fields) if fields.is_empty() => "unit".to_string(), TypeDeclKind::Struct(fields) - if fields.len() == 1 && fields[0].name.as_ref().is_some_and(|name| name == "_raw") => + if fields.elem_count() == 1 + && fields[0].name.as_ref().is_some_and(|name| name == "_raw") => { // These are the special strongly-typed integers. let short_name = decl @@ -597,7 +599,7 @@ fn type_decl_to_ocaml_decl(ctx: &GenerateCtx, decl: &TypeDecl, co_rec: bool) -> format!("{short_name}.id [@visitors.opaque]") } TypeDeclKind::Struct(fields) - if fields.len() == 1 + if fields.elem_count() == 1 && (fields[0].name.is_none() || decl .item_meta diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs index 141cabe3..24dd1083 100644 --- a/charon/src/ids/vector.rs +++ b/charon/src/ids/vector.rs @@ -25,7 +25,7 @@ where { vector: IndexVec>, /// The number of non-`None` elements. - real_len: usize, + elem_count: usize, } impl std::fmt::Debug for Vector @@ -46,7 +46,7 @@ where pub fn new() -> Self { Vector { vector: IndexVec::new(), - real_len: 0, + elem_count: 0, } } @@ -59,11 +59,17 @@ where } pub fn is_empty(&self) -> bool { - self.real_len == 0 + self.elem_count == 0 } - pub fn len(&self) -> usize { - self.real_len + /// The number of elements stored in the vector. + pub fn elem_count(&self) -> usize { + self.elem_count + } + + /// The number of slots allocated in the vector (empty or not). + pub fn slot_count(&self) -> usize { + self.vector.len() } /// Gets the value of the next available id. Avoid if possible; use `reserve_slot` instead. @@ -81,19 +87,19 @@ where pub fn set_slot(&mut self, id: I, x: T) { assert!(self.vector[id].is_none()); self.vector[id] = Some(x); - self.real_len += 1; + self.elem_count += 1; } /// Remove the value from this slot. pub fn remove(&mut self, id: I) -> Option { if self.vector[id].is_some() { - self.real_len -= 1; + self.elem_count -= 1; } self.vector[id].take() } pub fn push(&mut self, x: T) -> I { - self.real_len += 1; + self.elem_count += 1; self.vector.push(Some(x)) } @@ -123,7 +129,7 @@ where T: Clone, { self.vector.extend_from_slice(&other.vector); - self.real_len += other.real_len; + self.elem_count += other.elem_count; } /// Get a mutable reference into the ith element. If the vector is too short, extend it until @@ -144,7 +150,7 @@ where .into_iter() .map(|x_opt| x_opt.map(&mut f)) .collect(), - real_len: self.real_len, + elem_count: self.elem_count, } } @@ -156,7 +162,7 @@ where .iter() .map(|x_opt| x_opt.as_ref().map(&mut f)) .collect(), - real_len: self.real_len, + elem_count: self.elem_count, } } @@ -168,7 +174,7 @@ where .iter_mut() .map(|x_opt| x_opt.as_mut().map(&mut f)) .collect(), - real_len: self.real_len, + elem_count: self.elem_count, } } @@ -180,7 +186,7 @@ where .iter_enumerated() .map(|(i, x_opt)| x_opt.as_ref().map(|x| f(i, x))) .collect(), - real_len: self.real_len, + elem_count: self.elem_count, } } @@ -188,7 +194,7 @@ where pub fn map_opt(self, f: impl FnMut(Option) -> Option) -> Vector { Vector { vector: self.vector.into_iter().map(f).collect(), - real_len: self.real_len, + elem_count: self.elem_count, } } @@ -199,9 +205,9 @@ where ) -> Vector { let mut ret = Vector { vector: self.vector.iter().map(|x_opt| f(x_opt.as_ref())).collect(), - real_len: self.real_len, + elem_count: self.elem_count, }; - ret.real_len = ret.iter().count(); + ret.elem_count = ret.iter().count(); ret } @@ -262,10 +268,10 @@ where pub fn split_off(&mut self, at: usize) -> Self { let mut ret = Self { vector: self.vector.split_off(I::from_usize(at)), - real_len: 0, + elem_count: 0, }; - self.real_len = self.iter().count(); - ret.real_len = ret.iter().count(); + self.elem_count = self.iter().count(); + ret.elem_count = ret.iter().count(); ret } } @@ -347,9 +353,9 @@ where { #[inline] fn from_iter>(iter: It) -> Vector { - let mut real_len = 0; - let vector = IndexVec::from_iter(iter.into_iter().inspect(|_| real_len += 1).map(Some)); - Vector { vector, real_len } + let mut elem_count = 0; + let vector = IndexVec::from_iter(iter.into_iter().inspect(|_| elem_count += 1).map(Some)); + Vector { vector, elem_count } } } @@ -379,9 +385,9 @@ impl<'de, I: Idx, T: Deserialize<'de>> Deserialize<'de> for Vector { { let mut ret = Self { vector: Deserialize::deserialize(deserializer)?, - real_len: 0, + elem_count: 0, }; - ret.real_len = ret.iter().count(); + ret.elem_count = ret.iter().count(); Ok(ret) } } diff --git a/charon/src/name_matcher/mod.rs b/charon/src/name_matcher/mod.rs index d521c9e8..3e7d7078 100644 --- a/charon/src/name_matcher/mod.rs +++ b/charon/src/name_matcher/mod.rs @@ -209,10 +209,10 @@ impl PatTy { return true; } // We don't include regions in patterns. - if pats.len() != generics.types.len() + generics.const_generics.len() { + if pats.len() != generics.types.elem_count() + generics.const_generics.elem_count() { return false; } - let (type_pats, const_pats) = pats.split_at(generics.types.len()); + let (type_pats, const_pats) = pats.split_at(generics.types.elem_count()); let types_match = generics .types .iter() diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index 1d6840ca..9acb0d60 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -67,7 +67,7 @@ impl CheckGenericsVisitor<'_> { A: for<'a> FmtWithCtx, B: for<'a> FmtWithCtx, { - if a.len() == b.len() { + if a.elem_count() == b.elem_count() { a.iter().zip(b.iter()).for_each(|(x, y)| check_inner(x, y)); } else { let a = a.iter().map(|x| x.fmt_with_ctx(a_fmt)).join(", "); diff --git a/charon/src/transform/duplicate_return.rs b/charon/src/transform/duplicate_return.rs index a3a99a68..74ab6a95 100644 --- a/charon/src/transform/duplicate_return.rs +++ b/charon/src/transform/duplicate_return.rs @@ -53,8 +53,7 @@ impl UllbcPass for Transform { // for this (remark: in the end, it makes the return block dangling). // We do this in two steps. // First, introduce fresh ids. - assert!(usize::from(b.body.next_id()) == b.body.len()); - let mut generator = Generator::new_with_init_value(b.body.len()); + let mut generator = Generator::new_with_init_value(b.body.next_id().index()); let mut new_spans = Vec::new(); b.body.dyn_visit_in_body_mut(|bid: &mut BlockId| { if let Some(span) = returns.get(bid) { diff --git a/charon/src/transform/hide_marker_traits.rs b/charon/src/transform/hide_marker_traits.rs index 0cf5fe8c..1ddf774e 100644 --- a/charon/src/transform/hide_marker_traits.rs +++ b/charon/src/transform/hide_marker_traits.rs @@ -1,5 +1,4 @@ use derive_generic_visitor::*; -use index_vec::Idx; use itertools::Itertools; use std::collections::HashSet; @@ -14,46 +13,47 @@ struct RemoveMarkersVisitor { // Remove clauses and trait refs that mention the offending traits. This relies on the fact that // `Vector::remove` does not shift indices: it simply leaves an empty slot. +// FIXME: this is a footgun, it caused at least https://github.com/AeneasVerif/charon/issues/561. impl VisitAstMut for RemoveMarkersVisitor { fn enter_generic_params(&mut self, args: &mut GenericParams) { let trait_clauses = &mut args.trait_clauses; - for i in 0..trait_clauses.len() { + for i in trait_clauses.all_indices() { let clause = &trait_clauses[i]; if self.exclude.contains(&clause.trait_.skip_binder.trait_id) { - trait_clauses.remove(<_ as Idx>::from_usize(i)); + trait_clauses.remove(i); } } } fn enter_generic_args(&mut self, args: &mut GenericArgs) { let trait_refs = &mut args.trait_refs; - for i in 0..trait_refs.len() { + for i in trait_refs.all_indices() { let tref = &trait_refs[i]; if self .exclude .contains(&tref.trait_decl_ref.skip_binder.trait_id) { - trait_refs.remove(<_ as Idx>::from_usize(i)); + trait_refs.remove(i); } } } fn enter_trait_decl(&mut self, tdecl: &mut TraitDecl) { let trait_clauses = &mut tdecl.parent_clauses; - for i in 0..trait_clauses.len() { + for i in trait_clauses.all_indices() { let clause = &trait_clauses[i]; if self.exclude.contains(&clause.trait_.skip_binder.trait_id) { - trait_clauses.remove(<_ as Idx>::from_usize(i)); + trait_clauses.remove(i); } } } fn enter_trait_impl(&mut self, timpl: &mut TraitImpl) { let trait_refs = &mut timpl.parent_trait_refs; - for i in 0..trait_refs.len() { + for i in trait_refs.all_indices() { let tref = &trait_refs[i]; if self .exclude .contains(&tref.trait_decl_ref.skip_binder.trait_id) { - trait_refs.remove(<_ as Idx>::from_usize(i)); + trait_refs.remove(i); } } } diff --git a/charon/src/transform/inline_local_panic_functions.rs b/charon/src/transform/inline_local_panic_functions.rs index 5dc4b9e5..8fe3ffbe 100644 --- a/charon/src/transform/inline_local_panic_functions.rs +++ b/charon/src/transform/inline_local_panic_functions.rs @@ -21,7 +21,7 @@ impl UllbcPass for Transform { if let Ok(body) = &mut decl.body { let body = body.as_unstructured().unwrap(); // If the whole body is only a call to this specific panic function. - if body.body.len() == 1 + if body.body.elem_count() == 1 && let Some(block) = body.body.iter().next() && block.statements.is_empty() && let RawTerminator::Abort(AbortKind::Panic(name)) = &block.terminator.content diff --git a/charon/src/transform/update_closure_signatures.rs b/charon/src/transform/update_closure_signatures.rs index 6d93b966..cab1a1c0 100644 --- a/charon/src/transform/update_closure_signatures.rs +++ b/charon/src/transform/update_closure_signatures.rs @@ -78,7 +78,7 @@ fn transform_function(_ctx: &TransformCtx, def: &mut FunDecl) -> Result<(), Erro let body = body.as_unstructured_mut().unwrap(); // Update the type of the local 1 (which is the closure) - assert!(body.locals.vars.len() > 1); + assert!(body.locals.vars.elem_count() > 1); let state_var = &mut body.locals.vars[1]; state_var.ty = inputs[0].clone(); state_var.name = Some("state".to_string()); @@ -86,7 +86,7 @@ fn transform_function(_ctx: &TransformCtx, def: &mut FunDecl) -> Result<(), Erro // Update the body, and in particular the accesses to the states // TODO: translate to ADT field access // TODO: handle directly during translation - let num_fields = info.state.len(); + let num_fields = info.state.elem_count(); body.body.dyn_visit_in_body_mut(|pe: &mut ProjectionElem| { if let ProjectionElem::Field(pk @ FieldProjKind::ClosureState, _) = pe { *pk = FieldProjKind::Tuple(num_fields); diff --git a/charon/tests/crate_data.rs b/charon/tests/crate_data.rs index 4147dde5..cef73246 100644 --- a/charon/tests/crate_data.rs +++ b/charon/tests/crate_data.rs @@ -258,7 +258,11 @@ fn predicate_origins() -> anyhow::Result<()> { panic!("Item `{item_name}` not found. Available items: \n{keys}") }; let clauses = &item.generics.trait_clauses; - assert_eq!(origins.len(), clauses.len(), "failed for {item_name}"); + assert_eq!( + origins.len(), + clauses.elem_count(), + "failed for {item_name}" + ); for (clause, (expected_origin, expected_trait_name)) in clauses.iter().zip(origins) { let trait_name = trait_name(&crate_data, clause.trait_.skip_binder.trait_id); assert_eq!(trait_name, expected_trait_name, "failed for {item_name}"); diff --git a/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out b/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out new file mode 100644 index 00000000..e32a62a3 --- /dev/null +++ b/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out @@ -0,0 +1,48 @@ +# Final LLBC before serialization: + +trait test_crate::HasAssoc +{ + type Assoc +} + +trait test_crate::Trait +{ + fn default_method> = test_crate::Trait::default_method[@TraitClause0_1] +} + +fn test_crate::{impl test_crate::Trait for T}::default_method() -> @TraitClause2::Assoc +where + [@TraitClause2]: test_crate::HasAssoc, +{ + let @0: @TraitClause2::Assoc; // return + + panic(core::panicking::panic) +} + +impl test_crate::{impl test_crate::Trait for T} : test_crate::Trait +{ + fn default_method> = test_crate::{impl test_crate::Trait for T}::default_method[@TraitClause0_1] +} + +fn test_crate::main() +{ + let @0: (); // return + let @1: (); // anonymous local + + @1 := () + @0 := move (@1) + @0 := () + return +} + +fn test_crate::Trait::default_method() -> @TraitClause1::Assoc +where + [@TraitClause1]: test_crate::HasAssoc, +{ + let @0: @TraitClause1::Assoc; // return + + panic(core::panicking::panic) +} + + + diff --git a/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.rs b/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.rs new file mode 100644 index 00000000..4b503486 --- /dev/null +++ b/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.rs @@ -0,0 +1,17 @@ +//@ charon-args=--hide-marker-traits +// https://github.com/AeneasVerif/charon/issues/561 +use std::marker::PhantomData; + +trait HasAssoc { + type Assoc; +} +trait Trait { + fn default_method() -> T::Assoc { + todo!() + } +} + +// The `Sized` trait is the culprit. +impl Trait for T {} + +fn main() {}