Skip to content

Commit

Permalink
Clarify uses of Vector::len
Browse files Browse the repository at this point in the history 
The fact that the vector need not be contiguous is a footgun, we should
fix that.
  • Loading branch information
@Nadrieril
Nadrieril committed Feb 14, 2025
1 parent d51d241 commit f08de39
Show file tree
Hide file tree
Showing 16 changed files with 162 additions and 81 deletions.
10 changes: 5 additions & 5 deletions charon/src/ast/expressions_utils.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
45 changes: 24 additions & 21 deletions charon/src/ast/types_utils.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -151,28 +151,28 @@ impl<T: AstVisitable> Binder<Binder<T>> {
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();
}
}
}
Expand All @@ -199,19 +199,19 @@ impl<T: AstVisitable> Binder<Binder<T>> {
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,
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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
}
Expand All @@ -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])
}
Expand All @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion charon/src/bin/charon-driver/translate/translate_ctx.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down
12 changes: 7 additions & 5 deletions charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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());
}
_ => {
Expand All @@ -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 {
Expand All @@ -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)
}
Expand All @@ -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);
Expand Down Expand Up @@ -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);
Expand Down
2 changes: 1 addition & 1 deletion charon/src/bin/charon-driver/translate/translate_types.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
14 changes: 8 additions & 6 deletions charon/src/bin/generate-ml/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"),
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
Loading

0 comments on commit f08de39

Please sign in to comment.