Skip to content

Commit

Permalink
Remove the newly-added clauses if not used
Browse files Browse the repository at this point in the history
  • Loading branch information
Nadrieril committed Jan 8, 2025
1 parent ef456a7 commit d773757
Show file tree
Hide file tree
Showing 8 changed files with 154 additions and 23 deletions.
33 changes: 33 additions & 0 deletions charon/src/ast/krate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -218,6 +218,17 @@ impl<'ctx> AnyTransItem<'ctx> {
}
}

/// Get information about the parent of this item, if any.
pub fn parent_info(&self) -> &'ctx ItemKind {
match self {
AnyTransItem::Fun(d) => &d.kind,
AnyTransItem::Global(d) => &d.kind,
AnyTransItem::Type(_) | AnyTransItem::TraitDecl(_) | AnyTransItem::TraitImpl(_) => {
&ItemKind::Regular
}
}
}

/// See [`GenericParams::identity_args`].
pub fn identity_args(&self) -> GenericArgs {
self.generic_params()
Expand All @@ -235,6 +246,17 @@ impl<'ctx> AnyTransItem<'ctx> {
AnyTransItem::TraitImpl(d) => visitor.visit(d),
}
}

/// Visit all occurrences of that type inside `self`, in pre-order traversal.
pub fn dyn_visit<T: AstVisitable>(&self, f: impl FnMut(&T)) {
match *self {
AnyTransItem::Type(d) => d.dyn_visit(f),
AnyTransItem::Fun(d) => d.dyn_visit(f),
AnyTransItem::Global(d) => d.dyn_visit(f),
AnyTransItem::TraitDecl(d) => d.dyn_visit(f),
AnyTransItem::TraitImpl(d) => d.dyn_visit(f),
}
}
}

impl<'ctx> AnyTransItemMut<'ctx> {
Expand Down Expand Up @@ -270,6 +292,17 @@ impl<'ctx> AnyTransItemMut<'ctx> {
AnyTransItemMut::TraitImpl(d) => visitor.visit(*d),
}
}

/// Visit all occurrences of that type inside `self`, in pre-order traversal.
pub fn dyn_visit_mut<T: AstVisitable>(&mut self, f: impl FnMut(&mut T)) {
match self {
AnyTransItemMut::Type(d) => d.dyn_visit_mut(f),
AnyTransItemMut::Fun(d) => d.dyn_visit_mut(f),
AnyTransItemMut::Global(d) => d.dyn_visit_mut(f),
AnyTransItemMut::TraitDecl(d) => d.dyn_visit_mut(f),
AnyTransItemMut::TraitImpl(d) => d.dyn_visit_mut(f),
}
}
}

impl fmt::Display for TranslatedCrate {
Expand Down
4 changes: 2 additions & 2 deletions charon/src/ast/visitor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ use index_vec::Idx;
FnOperand, FunId, FunIdOrTraitMethodRef, FunSig, ImplElem, IntegerTy, Literal, LiteralTy,
llbc_ast::Block, llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Switch,
Locals, Name, NullOp, Opaque, Operand, PathElem, Place, PlaceKind, ProjectionElem, RawConstantExpr,
RefKind, RegionId, RegionVar, Rvalue, ScalarValue, TraitClause, TraitClauseId, TraitItemName,
RefKind, RegionId, RegionVar, Rvalue, ScalarValue, TraitItemName,
TraitRefKind, TraitTypeConstraint, TranslatedCrate, TyKind, TypeDeclKind, TypeId, TypeVar, TypeVarId,
ullbc_ast::BlockData, ullbc_ast::BlockId, ullbc_ast::ExprBody, ullbc_ast::RawStatement,
ullbc_ast::RawTerminator, ullbc_ast::SwitchTargets, ullbc_ast::Terminator,
Expand All @@ -64,7 +64,7 @@ use index_vec::Idx;
override(
DeBruijnId, Ty, Region, ConstGeneric, TraitRef,
FunDeclRef, GlobalDeclRef, TraitDeclRef, TraitImplRef,
GenericArgs, GenericParams,
GenericArgs, GenericParams, TraitClause, TraitClauseId,
for<T: AstVisitable + Idx> DeBruijnVar<T>,
for<T: AstVisitable> RegionBinder<T>,
for<T: AstVisitable> Binder<T>,
Expand Down
10 changes: 9 additions & 1 deletion charon/src/ids/vector.rs
Original file line number Diff line number Diff line change
Expand Up @@ -84,14 +84,22 @@ where
self.real_len += 1;
}

/// Remove the value from this slot.
/// Remove the value from this slot, leaving other ids unchanged.
pub fn remove(&mut self, id: I) -> Option<T> {
if self.vector[id].is_some() {
self.real_len -= 1;
}
self.vector[id].take()
}

/// Remove the value from this slot, shifting other ids as needed.
pub fn remove_and_shift_ids(&mut self, id: I) -> Option<T> {
if self.vector[id].is_some() {
self.real_len -= 1;
}
self.vector.remove(id)
}

pub fn push(&mut self, x: T) -> I {
self.real_len += 1;
self.vector.push(Some(x))
Expand Down
4 changes: 4 additions & 0 deletions charon/src/transform/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ pub mod remove_dynamic_checks;
pub mod remove_nops;
pub mod remove_read_discriminant;
pub mod remove_unused_locals;
pub mod remove_unused_self_clause;
pub mod reorder_decls;
pub mod simplify_constants;
pub mod skip_trait_refs_when_known;
Expand All @@ -45,6 +46,9 @@ pub static INITIAL_CLEANUP_PASSES: &[Pass] = &[
// # Micro-pass: filter the trait impls that were marked invisible since we couldn't filter
// them out earlier.
NonBody(&filter_invisible_trait_impls::Transform),
// # Micro-pass: remove the explicit `Self: Trait` clause of methods/assco const declaration
// items if they're not used. This simplifies the graph of dependencies between definitions.
NonBody(&remove_unused_self_clause::Transform),
// # Micro-pass: whenever we call a trait method on a known type, refer to the method `FunDecl`
// directly instead of going via a `TraitRef`. This is done before `reorder_decls` to remove
// some sources of mutual recursion.
Expand Down
100 changes: 100 additions & 0 deletions charon/src/transform/remove_unused_self_clause.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
//! We have added an explicit `Self: Trait` clause to the function and global items that correspond
//! to a trait method/associated const declaration. This pass removes the clause in question if it
//! is not used by the item.
use derive_generic_visitor::*;
use std::collections::HashSet;

use crate::ast::*;

use super::{ctx::TransformPass, TransformCtx};

struct FoundClause;

struct UsesClauseVisitor(TraitClauseId);
impl Visitor for UsesClauseVisitor {
type Break = FoundClause;
}

/// Visit an item looking for uses of the given clause.
impl VisitAst for UsesClauseVisitor {
fn visit_trait_clause_id(&mut self, x: &TraitClauseId) -> ControlFlow<Self::Break> {
if *x == self.0 {
Break(FoundClause)
} else {
Continue(())
}
}
fn visit_trait_clause(&mut self, _: &TraitClause) -> ControlFlow<Self::Break> {
// Don't look inside the clause declaration as this will always contain the
// `TraitClauseId`.
Continue(())
}
fn visit_fun_decl(&mut self, x: &FunDecl) -> ControlFlow<Self::Break> {
if let Err(Opaque) = x.body {
// For function without bodies we can't know whether the clause is used so we err on
// the side of it being used.
return Break(FoundClause);
}
self.visit_inner(x)
}
}

pub struct Transform;
impl TransformPass for Transform {
fn transform_ctx(&self, ctx: &mut TransformCtx) {
let self_clause_id = TraitClauseId::from_raw(0);
let mut doesnt_use_self: HashSet<AnyTransId> = Default::default();

// We explore only items with an explicit `Self` clause, namely method and associated const
// declarations.
for tdecl in &ctx.translated.trait_decls {
let methods = tdecl
.required_methods
.iter()
.chain(tdecl.provided_methods.iter())
.map(|(_, bound_fn)| bound_fn.skip_binder.id);
// For consts, we need to explore the corresponding initializer body.
let consts = tdecl
.const_defaults
.iter()
.filter_map(|(_, x)| ctx.translated.global_decls.get(x.id))
.map(|gdecl| gdecl.init);
let funs = methods
.chain(consts)
.filter_map(|id: FunDeclId| ctx.translated.fun_decls.get(id));
for fun in funs {
match fun.drive(&mut UsesClauseVisitor(self_clause_id)) {
Continue(()) => {
doesnt_use_self.insert(fun.def_id.into());
if let Some(gid) = fun.is_global_initializer {
doesnt_use_self.insert(gid.into());
}
}
Break(FoundClause) => {}
}
}
}

// In each item, remove the first clause and renumber the others.
for &id in &doesnt_use_self {
let Some(mut item) = ctx.translated.get_item_mut(id) else {
continue;
};
item.generic_params()
.trait_clauses
.remove_and_shift_ids(self_clause_id);
item.dyn_visit_mut(|clause_id: &mut TraitClauseId| {
*clause_id = TraitClauseId::from_usize(clause_id.index() - 1);
});
}

// Update any `GenericArgs` destined for the items we just changed.
ctx.translated.dyn_visit_mut(|args: &mut GenericArgs| {
if let GenericsSource::Item(target_id) = args.target
&& doesnt_use_self.contains(&target_id)
{
args.trait_refs.remove_and_shift_ids(self_clause_id);
}
});
}
}
9 changes: 2 additions & 7 deletions charon/tests/ui/assoc-const-with-generics.out
Original file line number Diff line number Diff line change
Expand Up @@ -94,19 +94,14 @@ where
}

fn test_crate::HasDefaultLen::LEN<Self, const M : usize>() -> usize
where
[@TraitClause0]: test_crate::HasDefaultLen<Self, const M : usize>,
{
let @0: usize; // return

@0 := const (const M : usize)
return
}

global test_crate::HasDefaultLen::LEN<Self, const M : usize>: usize
where
[@TraitClause0]: test_crate::HasDefaultLen<Self, const M : usize>,
= test_crate::HasDefaultLen::LEN()
global test_crate::HasDefaultLen::LEN<Self, const M : usize>: usize = test_crate::HasDefaultLen::LEN()

trait test_crate::HasDefaultLen<Self, const M : usize>
{
Expand All @@ -115,7 +110,7 @@ trait test_crate::HasDefaultLen<Self, const M : usize>

impl<const N : usize> test_crate::{impl test_crate::HasDefaultLen<const N : usize> for Array<(), const N : usize>}#4<const N : usize> : test_crate::HasDefaultLen<Array<(), const N : usize>, const N : usize>
{
const LEN = test_crate::HasDefaultLen::LEN<Array<(), const N : usize>, const N : usize>[test_crate::{impl test_crate::HasDefaultLen<const N : usize> for Array<(), const N : usize>}#4<const N : usize>]
const LEN = test_crate::HasDefaultLen::LEN<Array<(), const N : usize>, const N : usize>
}

fn test_crate::{impl test_crate::HasDefaultLen<const N : usize> for Array<bool, const N : usize>}#5::LEN<const N : usize>() -> usize
Expand Down
4 changes: 1 addition & 3 deletions charon/tests/ui/rename_attribute.out
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
trait test_crate::BoolTrait<Self>
{
fn get_bool<'_0> = test_crate::BoolTrait::get_bool<'_0_0, Self>[Self]
fn ret_true<'_0> = test_crate::BoolTrait::ret_true<'_0_0, Self>[Self]
fn ret_true<'_0> = test_crate::BoolTrait::ret_true<'_0_0, Self>
}

fn test_crate::{impl test_crate::BoolTrait for bool}::get_bool<'_0>(@1: &'_0 (bool)) -> bool
Expand All @@ -23,8 +23,6 @@ impl test_crate::{impl test_crate::BoolTrait for bool} : test_crate::BoolTrait<b
trait core::marker::Sized<Self>

fn test_crate::BoolTrait::ret_true<'_0, Self>(@1: &'_0 (Self)) -> bool
where
[@TraitClause0]: test_crate::BoolTrait<Self>,
{
let @0: bool; // return
let self@1: &'_ (Self); // arg #1
Expand Down
13 changes: 3 additions & 10 deletions charon/tests/ui/traits.out
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
trait test_crate::BoolTrait<Self>
{
fn get_bool<'_0> = test_crate::BoolTrait::get_bool<'_0_0, Self>[Self]
fn ret_true<'_0> = test_crate::BoolTrait::ret_true<'_0_0, Self>[Self]
fn ret_true<'_0> = test_crate::BoolTrait::ret_true<'_0_0, Self>
}

fn test_crate::{impl test_crate::BoolTrait for bool}::get_bool<'_0>(@1: &'_0 (bool)) -> bool
Expand All @@ -21,8 +21,6 @@ impl test_crate::{impl test_crate::BoolTrait for bool} : test_crate::BoolTrait<b
}

fn test_crate::BoolTrait::ret_true<'_0, Self>(@1: &'_0 (Self)) -> bool
where
[@TraitClause0]: test_crate::BoolTrait<Self>,
{
let @0: bool; // return
let self@1: &'_ (Self); // arg #1
Expand Down Expand Up @@ -488,19 +486,14 @@ where
}

fn test_crate::WithConstTy::LEN2<Self, const LEN : usize>() -> usize
where
[@TraitClause0]: test_crate::WithConstTy<Self, const LEN : usize>,
{
let @0: usize; // return

@0 := const (32 : usize)
return
}

global test_crate::WithConstTy::LEN2<Self, const LEN : usize>: usize
where
[@TraitClause0]: test_crate::WithConstTy<Self, const LEN : usize>,
= test_crate::WithConstTy::LEN2()
global test_crate::WithConstTy::LEN2<Self, const LEN : usize>: usize = test_crate::WithConstTy::LEN2()

trait test_crate::WithConstTy<Self, const LEN : usize>
{
Expand Down Expand Up @@ -543,7 +536,7 @@ impl test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8 : test_cr
parent_clause1 = test_crate::{impl test_crate::ToU64 for u64}#2
parent_clause2 = core::marker::Sized<u64>
const LEN1 = test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::LEN1
const LEN2 = test_crate::WithConstTy::LEN2<bool, 32 : usize>[test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8]
const LEN2 = test_crate::WithConstTy::LEN2<bool, 32 : usize>
type V = u8
type W = u64
fn f<'_0, '_1> = test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::f<'_0_0, '_0_1>
Expand Down

0 comments on commit d773757

Please sign in to comment.