Skip to content

Commit

Permalink
Don't list hidden methods in the trait declaration
Browse files Browse the repository at this point in the history 
This is a bugfix while there are method signatures we can't translate
  • Loading branch information
@Nadrieril
Nadrieril committed Aug 26, 2024
1 parent 9857532 commit b8e5313
Show file tree
Hide file tree
Showing 5 changed files with 14 additions and 58 deletions.
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 @@ -107,10 +107,10 @@ impl TranslateOptions {
"max_by",
"max_by_key",
"min_by",
"rposition",
"min_by_key",
"partition",
"partition_in_place",
"rposition",
"scan",
"skip_while",
"take_while",
Expand Down
11 changes: 9 additions & 2 deletions charon/src/bin/charon-driver/translate/translate_traits.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -165,12 +165,19 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
let item_span = bt_ctx.t_ctx.tcx.def_span(rust_item_id);
match &hax_item.kind {
AssocKind::Fn => {
let fun_id = bt_ctx.register_fun_decl_id(item_span, rust_item_id);
if hax_item.has_value {
// This is a *provided* method,
provided_methods.push((item_name.clone(), fun_id));
// Hack: To avoid having a trait that lists methods that aren't translated,
// we filter out invisible methods early. FIXME: remove this once we can
// translate all `Iterator` method signatures.
let fun_name = bt_ctx.t_ctx.def_id_to_name(rust_item_id)?;
if !bt_ctx.t_ctx.opacity_for_name(&fun_name).is_invisible() {
let fun_id = bt_ctx.register_fun_decl_id(item_span, rust_item_id);
provided_methods.push((item_name.clone(), fun_id));
}
} else {
// This is a required method (no default implementation)
let fun_id = bt_ctx.register_fun_decl_id(item_span, rust_item_id);
required_methods.push((item_name.clone(), fun_id));
}
}
Expand Down
17 changes: 0 additions & 17 deletions charon/tests/ui/issue-45-misc.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -248,27 +248,19 @@ trait core::iter::traits::iterator::Iterator<Self>
fn intersperse_with : core::iter::traits::iterator::Iterator::intersperse_with
fn map : core::iter::traits::iterator::Iterator::map
fn for_each : core::iter::traits::iterator::Iterator::for_each
fn filter : @Fun39
fn filter_map : core::iter::traits::iterator::Iterator::filter_map
fn enumerate : core::iter::traits::iterator::Iterator::enumerate
fn peekable : core::iter::traits::iterator::Iterator::peekable
fn skip_while : @Fun43
fn take_while : @Fun44
fn map_while : core::iter::traits::iterator::Iterator::map_while
fn skip : core::iter::traits::iterator::Iterator::skip
fn take : core::iter::traits::iterator::Iterator::take
fn scan : @Fun48
fn flat_map : core::iter::traits::iterator::Iterator::flat_map
fn flatten : core::iter::traits::iterator::Iterator::flatten
fn map_windows : @Fun51
fn fuse : core::iter::traits::iterator::Iterator::fuse
fn inspect : @Fun53
fn by_ref : core::iter::traits::iterator::Iterator::by_ref
fn collect : core::iter::traits::iterator::Iterator::collect
fn try_collect : core::iter::traits::iterator::Iterator::try_collect
fn collect_into : core::iter::traits::iterator::Iterator::collect_into
fn partition : @Fun58
fn partition_in_place : @Fun59
fn is_partitioned : core::iter::traits::iterator::Iterator::is_partitioned
fn try_fold : core::iter::traits::iterator::Iterator::try_fold
fn try_for_each : core::iter::traits::iterator::Iterator::try_for_each
Expand All @@ -277,17 +269,10 @@ trait core::iter::traits::iterator::Iterator<Self>
fn try_reduce : core::iter::traits::iterator::Iterator::try_reduce
fn all : core::iter::traits::iterator::Iterator::all
fn any : core::iter::traits::iterator::Iterator::any
fn find : @Fun68
fn find_map : core::iter::traits::iterator::Iterator::find_map
fn try_find : @Fun70
fn position : core::iter::traits::iterator::Iterator::position
fn rposition : @Fun72
fn max : core::iter::traits::iterator::Iterator::max
fn min : core::iter::traits::iterator::Iterator::min
fn max_by_key : @Fun75
fn max_by : @Fun76
fn min_by_key : @Fun77
fn min_by : @Fun78
fn rev : core::iter::traits::iterator::Iterator::rev
fn unzip : core::iter::traits::iterator::Iterator::unzip
fn copied : core::iter::traits::iterator::Iterator::copied
Expand All @@ -308,7 +293,6 @@ trait core::iter::traits::iterator::Iterator<Self>
fn gt : core::iter::traits::iterator::Iterator::gt
fn ge : core::iter::traits::iterator::Iterator::ge
fn is_sorted : core::iter::traits::iterator::Iterator::is_sorted
fn is_sorted_by : @Fun99
fn is_sorted_by_key : core::iter::traits::iterator::Iterator::is_sorted_by_key
fn __iterator_get_unchecked : core::iter::traits::iterator::Iterator::__iterator_get_unchecked
}
Expand Down Expand Up @@ -366,7 +350,6 @@ trait core::iter::traits::double_ended::DoubleEndedIterator<Self>
fn nth_back : core::iter::traits::double_ended::DoubleEndedIterator::nth_back
fn try_rfold : core::iter::traits::double_ended::DoubleEndedIterator::try_rfold
fn rfold : core::iter::traits::double_ended::DoubleEndedIterator::rfold
fn rfind : @Fun150
}

opaque type core::iter::adapters::array_chunks::ArrayChunks<I, const N : usize>
Expand Down
17 changes: 0 additions & 17 deletions charon/tests/ui/loops.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -989,27 +989,19 @@ trait core::iter::traits::iterator::Iterator<Self>
fn intersperse_with : core::iter::traits::iterator::Iterator::intersperse_with
fn map : core::iter::traits::iterator::Iterator::map
fn for_each : core::iter::traits::iterator::Iterator::for_each
fn filter : @Fun46
fn filter_map : core::iter::traits::iterator::Iterator::filter_map
fn enumerate : core::iter::traits::iterator::Iterator::enumerate
fn peekable : core::iter::traits::iterator::Iterator::peekable
fn skip_while : @Fun50
fn take_while : @Fun51
fn map_while : core::iter::traits::iterator::Iterator::map_while
fn skip : core::iter::traits::iterator::Iterator::skip
fn take : core::iter::traits::iterator::Iterator::take
fn scan : @Fun55
fn flat_map : core::iter::traits::iterator::Iterator::flat_map
fn flatten : core::iter::traits::iterator::Iterator::flatten
fn map_windows : @Fun58
fn fuse : core::iter::traits::iterator::Iterator::fuse
fn inspect : @Fun60
fn by_ref : core::iter::traits::iterator::Iterator::by_ref
fn collect : core::iter::traits::iterator::Iterator::collect
fn try_collect : core::iter::traits::iterator::Iterator::try_collect
fn collect_into : core::iter::traits::iterator::Iterator::collect_into
fn partition : @Fun65
fn partition_in_place : @Fun66
fn is_partitioned : core::iter::traits::iterator::Iterator::is_partitioned
fn try_fold : core::iter::traits::iterator::Iterator::try_fold
fn try_for_each : core::iter::traits::iterator::Iterator::try_for_each
Expand All @@ -1018,17 +1010,10 @@ trait core::iter::traits::iterator::Iterator<Self>
fn try_reduce : core::iter::traits::iterator::Iterator::try_reduce
fn all : core::iter::traits::iterator::Iterator::all
fn any : core::iter::traits::iterator::Iterator::any
fn find : @Fun75
fn find_map : core::iter::traits::iterator::Iterator::find_map
fn try_find : @Fun77
fn position : core::iter::traits::iterator::Iterator::position
fn rposition : @Fun79
fn max : core::iter::traits::iterator::Iterator::max
fn min : core::iter::traits::iterator::Iterator::min
fn max_by_key : @Fun82
fn max_by : @Fun83
fn min_by_key : @Fun84
fn min_by : @Fun85
fn rev : core::iter::traits::iterator::Iterator::rev
fn unzip : core::iter::traits::iterator::Iterator::unzip
fn copied : core::iter::traits::iterator::Iterator::copied
Expand All @@ -1049,7 +1034,6 @@ trait core::iter::traits::iterator::Iterator<Self>
fn gt : core::iter::traits::iterator::Iterator::gt
fn ge : core::iter::traits::iterator::Iterator::ge
fn is_sorted : core::iter::traits::iterator::Iterator::is_sorted
fn is_sorted_by : @Fun106
fn is_sorted_by_key : core::iter::traits::iterator::Iterator::is_sorted_by_key
fn __iterator_get_unchecked : core::iter::traits::iterator::Iterator::__iterator_get_unchecked
}
Expand Down Expand Up @@ -1107,7 +1091,6 @@ trait core::iter::traits::double_ended::DoubleEndedIterator<Self>
fn nth_back : core::iter::traits::double_ended::DoubleEndedIterator::nth_back
fn try_rfold : core::iter::traits::double_ended::DoubleEndedIterator::try_rfold
fn rfold : core::iter::traits::double_ended::DoubleEndedIterator::rfold
fn rfind : @Fun206
}

opaque type core::iter::adapters::array_chunks::ArrayChunks<I, const N : usize>
Expand Down
25 changes: 4 additions & 21 deletions charon/tests/ui/trait-instance-id.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -239,27 +239,19 @@ trait core::iter::traits::iterator::Iterator<Self>
fn intersperse_with : core::iter::traits::iterator::Iterator::intersperse_with
fn map : core::iter::traits::iterator::Iterator::map
fn for_each : core::iter::traits::iterator::Iterator::for_each
fn filter : @Fun20
fn filter_map : core::iter::traits::iterator::Iterator::filter_map
fn enumerate : core::iter::traits::iterator::Iterator::enumerate
fn peekable : core::iter::traits::iterator::Iterator::peekable
fn skip_while : @Fun24
fn take_while : @Fun25
fn map_while : core::iter::traits::iterator::Iterator::map_while
fn skip : core::iter::traits::iterator::Iterator::skip
fn take : core::iter::traits::iterator::Iterator::take
fn scan : @Fun29
fn flat_map : core::iter::traits::iterator::Iterator::flat_map
fn flatten : core::iter::traits::iterator::Iterator::flatten
fn map_windows : @Fun32
fn fuse : core::iter::traits::iterator::Iterator::fuse
fn inspect : @Fun34
fn by_ref : core::iter::traits::iterator::Iterator::by_ref
fn collect : core::iter::traits::iterator::Iterator::collect
fn try_collect : core::iter::traits::iterator::Iterator::try_collect
fn collect_into : core::iter::traits::iterator::Iterator::collect_into
fn partition : @Fun39
fn partition_in_place : @Fun40
fn is_partitioned : core::iter::traits::iterator::Iterator::is_partitioned
fn try_fold : core::iter::traits::iterator::Iterator::try_fold
fn try_for_each : core::iter::traits::iterator::Iterator::try_for_each
Expand All @@ -268,17 +260,10 @@ trait core::iter::traits::iterator::Iterator<Self>
fn try_reduce : core::iter::traits::iterator::Iterator::try_reduce
fn all : core::iter::traits::iterator::Iterator::all
fn any : core::iter::traits::iterator::Iterator::any
fn find : @Fun49
fn find_map : core::iter::traits::iterator::Iterator::find_map
fn try_find : @Fun51
fn position : core::iter::traits::iterator::Iterator::position
fn rposition : @Fun53
fn max : core::iter::traits::iterator::Iterator::max
fn min : core::iter::traits::iterator::Iterator::min
fn max_by_key : @Fun56
fn max_by : @Fun57
fn min_by_key : @Fun58
fn min_by : @Fun59
fn rev : core::iter::traits::iterator::Iterator::rev
fn unzip : core::iter::traits::iterator::Iterator::unzip
fn copied : core::iter::traits::iterator::Iterator::copied
Expand All @@ -299,7 +284,6 @@ trait core::iter::traits::iterator::Iterator<Self>
fn gt : core::iter::traits::iterator::Iterator::gt
fn ge : core::iter::traits::iterator::Iterator::ge
fn is_sorted : core::iter::traits::iterator::Iterator::is_sorted
fn is_sorted_by : @Fun80
fn is_sorted_by_key : core::iter::traits::iterator::Iterator::is_sorted_by_key
fn __iterator_get_unchecked : core::iter::traits::iterator::Iterator::__iterator_get_unchecked
}
Expand Down Expand Up @@ -347,7 +331,6 @@ trait core::iter::traits::double_ended::DoubleEndedIterator<Self>
fn nth_back : core::iter::traits::double_ended::DoubleEndedIterator::nth_back
fn try_rfold : core::iter::traits::double_ended::DoubleEndedIterator::try_rfold
fn rfold : core::iter::traits::double_ended::DoubleEndedIterator::rfold
fn rfind : @Fun152
}

opaque type core::iter::adapters::array_chunks::ArrayChunks<I, const N : usize>
Expand Down Expand Up @@ -462,7 +445,7 @@ where
[@TraitClause0]: core::ops::function::FnMut<F, (&'_ (T))>,
(parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut<F, (core::slice::iter::{impl core::iter::traits::iterator::Iterator for @Adt2<'a, T>}#182<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut<F, (&'_ (T))>) (context: core::slice::iter::{impl#182}::any)))::[@TraitClause0])::Output = bool,

Missing decl: Fun(115) (core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::find)
Missing decl: Fun(99) (core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::find)

fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::find_map<'a, '_1, T, B, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: F) -> core::option::Option<B>
where
Expand All @@ -488,7 +471,7 @@ where
[@TraitClause2]: core::iter::traits::double_ended::DoubleEndedIterator<core::slice::iter::Iter<'_, T>>,
(parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut<P, ((parents(UNKNOWN(Could not find a clause for parameter: @TraitDecl23<@Adt2<'a, T>> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut<P, ((parents(UNKNOWN(Could not find a clause for parameter: @TraitDecl23<@Adt2<'a, T>> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>) (context: core::slice::iter::{impl#182}::rposition)))::[@TraitClause0])::Item)>; [@TraitClause2]: core::iter::traits::double_ended::DoubleEndedIterator<@Adt2<'_, T>>; [@TraitClause1]: @TraitDecl23<@Adt2<'_, T>>) (context: core::slice::iter::{impl#182}::rposition)))::[@TraitClause0])::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut<P, ((parents(UNKNOWN(Could not find a clause for parameter: @TraitDecl23<@Adt2<'a, T>> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>) (context: core::slice::iter::{impl#182}::rposition)))::[@TraitClause0])::Item)>; [@TraitClause2]: core::iter::traits::double_ended::DoubleEndedIterator<@Adt2<'_, T>>; [@TraitClause1]: @TraitDecl23<@Adt2<'_, T>>) (context: core::slice::iter::{impl#182}::rposition)))::[@TraitClause0])::Output = bool,

Missing decl: Fun(120) (core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::is_sorted_by)
Missing decl: Fun(104) (core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::is_sorted_by)

unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182<'_, T>::Item

Expand All @@ -505,11 +488,11 @@ impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for
fn fold = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::fold
fn all = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::all
fn any = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::any
fn find = @Fun115
fn find = @Fun99
fn find_map = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::find_map
fn position = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::position
fn rposition = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::rposition
fn is_sorted_by = @Fun120
fn is_sorted_by = @Fun104
fn __iterator_get_unchecked = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::__iterator_get_unchecked
}

Expand Down

0 comments on commit b8e5313

Please sign in to comment.