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 Feb 12, 2025
1 parent f8b4d8b commit da0bb13
Show file tree
Hide file tree
Showing 11 changed files with 156 additions and 36 deletions.
33 changes: 33 additions & 0 deletions charon/src/ast/krate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -221,6 +221,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 @@ -238,6 +249,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 @@ -273,6 +295,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 @@ -47,7 +47,7 @@ use indexmap::IndexMap;
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, TraitClauseId, TraitItemName,
RefKind, RegionId, RegionVar, Rvalue, ScalarValue, TraitItemName,
TranslatedCrate, 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 @@ -65,7 +65,7 @@ use indexmap::IndexMap;
override(
DeBruijnId, Ty, TyKind, Region, ConstGeneric, TraitRef, TraitRefKind,
FunDeclRef, GlobalDeclRef, TraitDeclRef, TraitImplRef,
GenericArgs, GenericParams, TraitClause, TraitTypeConstraint,
GenericArgs, GenericParams, TraitClause, TraitClauseId, TraitTypeConstraint,
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 @@ -25,6 +25,7 @@ pub mod remove_nops;
pub mod remove_read_discriminant;
pub mod remove_unused_locals;
pub mod remove_unused_methods;
pub mod remove_unused_self_clause;
pub mod reorder_decls;
pub mod simplify_constants;
pub mod skip_trait_refs_when_known;
Expand All @@ -51,6 +52,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/assoc const declaration
// items if they're not used. This simplifies the graph of dependencies between definitions.
NonBody(&remove_unused_self_clause::Transform),
// Add missing methods to trait impls by duplicating the default method.
NonBody(&duplicate_defaulted_methods::Transform),
// # Micro-pass: whenever we call a trait method on a known type, refer to the method `FunDecl`
Expand Down
96 changes: 96 additions & 0 deletions charon/src/transform/remove_unused_self_clause.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,96 @@
//! 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.methods().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
8 changes: 2 additions & 6 deletions charon/tests/ui/opaque-trait.out
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,8 @@ trait test_crate::Trait<Self>
const CONST1 : usize
const CONST2 : usize
const CONST3 : usize
fn method1 = test_crate::Trait::method1<Self>[Self]
fn method2 = test_crate::Trait::method2<Self>[Self]
fn method1 = test_crate::Trait::method1<Self>
fn method2 = test_crate::Trait::method2<Self>
}

fn test_crate::{impl test_crate::Trait for ()}#1::CONST1() -> usize
Expand Down Expand Up @@ -144,8 +144,6 @@ impl test_crate::{impl test_crate::Trait for u8} : test_crate::Trait<u8>
trait core::marker::Sized<Self>

fn test_crate::Trait::method1<Self>()
where
[@TraitClause0]: test_crate::Trait<Self>,
{
let @0: (); // return
let @1: (); // anonymous local
Expand Down Expand Up @@ -177,8 +175,6 @@ where
}

fn test_crate::Trait::method2<Self>()
where
[@TraitClause0]: test_crate::Trait<Self>,
{
let @0: (); // return
let @1: (); // anonymous local
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 Down Expand Up @@ -91,8 +91,6 @@ where
[@TraitClause0]: test_crate::BoolTrait<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
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ trait test_crate::HasType<Self, Self_Type>

trait test_crate::HasMethod<Self>
{
fn method<Clause0_Type, [@TraitClause0]: test_crate::HasType<Self, Clause0_Type>> = test_crate::HasMethod::method<Self, Clause0_Type>[Self, @TraitClause0_0]
fn method<Clause0_Type, [@TraitClause0]: test_crate::HasType<Self, Clause0_Type>> = test_crate::HasMethod::method<Self, Clause0_Type>[@TraitClause0_0]
}

enum core::option::Option<T>
Expand Down Expand Up @@ -41,10 +41,9 @@ where
fn method<Clause0_Type, [@TraitClause0]: test_crate::HasType<core::option::Option<T>[@TraitClause0], Clause0_Type>> = test_crate::{impl test_crate::HasMethod for core::option::Option<T>[@TraitClause0]}::method<T, Clause0_Type>[@TraitClause0, @TraitClause0_0]
}

fn test_crate::HasMethod::method<Self, Clause1_Type>()
fn test_crate::HasMethod::method<Self, Clause0_Type>()
where
[@TraitClause0]: test_crate::HasMethod<Self>,
[@TraitClause1]: test_crate::HasType<Self, Clause1_Type>,
[@TraitClause0]: test_crate::HasType<Self, Clause0_Type>,
{
let @0: (); // return
let @1: (); // anonymous local
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

trait test_crate::BoolTrait<Self>
{
fn foo<'_0> = test_crate::BoolTrait::foo<'_0_0, Self>[Self]
fn foo<'_0> = test_crate::BoolTrait::foo<'_0_0, Self>
}

trait core::marker::Sized<Self>
Expand Down Expand Up @@ -37,8 +37,6 @@ where
}

fn test_crate::BoolTrait::foo<'_0, Self>(@1: &'_0 (Self))
where
[@TraitClause0]: test_crate::BoolTrait<Self>,
{
let @0: (); // 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 Down Expand Up @@ -499,19 +499,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 @@ -554,7 +549,7 @@ impl test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8 : test_cr
parent_clause1 = core::marker::Sized<u64>
parent_clause2 = test_crate::{impl test_crate::ToU64 for u64}#2
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 Expand Up @@ -1070,8 +1065,6 @@ where
}

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

0 comments on commit da0bb13

Please sign in to comment.