diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 2760d6b2..7a725545 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -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", diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index cfb3280d..98cc73e0 100644 --- a/charon/src/bin/charon-driver/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -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)); } } diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 3c56d673..c1be178f 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -248,27 +248,19 @@ trait core::iter::traits::iterator::Iterator 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 @@ -277,17 +269,10 @@ trait core::iter::traits::iterator::Iterator 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 @@ -308,7 +293,6 @@ trait core::iter::traits::iterator::Iterator 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 } @@ -366,7 +350,6 @@ trait core::iter::traits::double_ended::DoubleEndedIterator 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 diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out index 5704c3fb..9e553119 100644 --- a/charon/tests/ui/loops.out +++ b/charon/tests/ui/loops.out @@ -989,27 +989,19 @@ trait core::iter::traits::iterator::Iterator 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 @@ -1018,17 +1010,10 @@ trait core::iter::traits::iterator::Iterator 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 @@ -1049,7 +1034,6 @@ trait core::iter::traits::iterator::Iterator 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 } @@ -1107,7 +1091,6 @@ trait core::iter::traits::double_ended::DoubleEndedIterator 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 diff --git a/charon/tests/ui/trait-instance-id.out b/charon/tests/ui/trait-instance-id.out index 47bad236..ff2655ad 100644 --- a/charon/tests/ui/trait-instance-id.out +++ b/charon/tests/ui/trait-instance-id.out @@ -239,27 +239,19 @@ trait core::iter::traits::iterator::Iterator 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 @@ -268,17 +260,10 @@ trait core::iter::traits::iterator::Iterator 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 @@ -299,7 +284,6 @@ trait core::iter::traits::iterator::Iterator 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 } @@ -347,7 +331,6 @@ trait core::iter::traits::double_ended::DoubleEndedIterator 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 @@ -462,7 +445,7 @@ where [@TraitClause0]: core::ops::function::FnMut, (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut}#182<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (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 where @@ -488,7 +471,7 @@ where [@TraitClause2]: core::iter::traits::double_ended::DoubleEndedIterator>, (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut> (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> (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 @@ -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 }