Skip to content

Commit

Permalink
Collect implemented methods in trait declaration order
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril committed Aug 21, 2024
1 parent f3c6656 commit 9e782be
Show file tree
Hide file tree
Showing 6 changed files with 96 additions and 95 deletions.
41 changes: 21 additions & 20 deletions charon/src/bin/charon-driver/translate/translate_traits.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ use charon_lib::pretty::FmtWithCtx;
use charon_lib::types::*;
use charon_lib::ullbc_ast as ast;
use hax_frontend_exporter as hax;
use hax_frontend_exporter::AssocItemContainer;
use hax_frontend_exporter::SInto;
use itertools::Itertools;
use rustc_hir::def_id::DefId;
Expand Down Expand Up @@ -362,8 +361,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
let tcx = bt_ctx.t_ctx.tcx;
let mut consts = HashMap::new();
let mut types: HashMap<TraitItemName, Ty> = HashMap::new();
let mut required_methods = Vec::new();
let mut provided_methods = Vec::new();
let mut methods = HashMap::new();

for item in impl_items {
let name = TraitItemName(item.name.clone());
Expand All @@ -372,17 +370,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
match &item.kind {
hax::AssocKind::Fn => {
let fun_id = bt_ctx.register_fun_decl_id(item_span, rust_item_id);
let AssocItemContainer::TraitImplContainer {
overrides_default, ..
} = item.container
else {
unreachable!()
};
if overrides_default {
provided_methods.push((name, fun_id));
} else {
required_methods.push((name, fun_id));
}
methods.insert(name, fun_id);
}
hax::AssocKind::Const => {
// The parameters of the constant are the same as those of the item that
Expand Down Expand Up @@ -418,13 +406,27 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
let mut consts = Vec::new();
let mut type_clauses = Vec::new();
let mut types: Vec<(TraitItemName, Ty)> = Vec::new();
for item in decl_items {
let item_def_id = (&item.def_id).into();
let mut required_methods = Vec::new();
let mut provided_methods = Vec::new();

for decl_item in decl_items {
let item_def_id = (&decl_item.def_id).into();
let item_span = tcx.def_span(item_def_id);
match &item.kind {
hax::AssocKind::Fn => (),
let name = TraitItemName(decl_item.name.to_string());
match &decl_item.kind {
hax::AssocKind::Fn => {
if let Some(&fun_id) = methods.get(&name) {
// Check if we implement a required method or reimplement a provided
// method.
if decl_item.has_value {
provided_methods.push((name, fun_id));
} else {
required_methods.push((name, fun_id));
}
}
}

hax::AssocKind::Const => {
let name = TraitItemName(item.name.to_string());
// Does the trait impl provide an implementation for this const?
let c = match partial_consts.get(&name) {
Some(c) => c.clone(),
Expand All @@ -442,7 +444,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
consts.push((name, c));
}
hax::AssocKind::Type => {
let name = TraitItemName(item.name.to_string());
// Does the trait impl provide an implementation for this type?
let ty = match partial_types.get(&name) {
Some(ty) => ty.clone(),
Expand Down
32 changes: 16 additions & 16 deletions charon/tests/ui/issue-45-misc.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -432,22 +432,20 @@ where
// Inherited clauses:
[@TraitClause0]: core::iter::range::Step<A>,

fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::nth<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>), @2: usize) -> core::option::Option<A>
fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::last<A>(@1: core::ops::range::Range<A>) -> core::option::Option<A>
where
// Inherited clauses:
[@TraitClause0]: core::iter::range::Step<A>,

fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::last<A>(@1: core::ops::range::Range<A>) -> core::option::Option<A>
fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::advance_by<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26>>
where
// Inherited clauses:
[@TraitClause0]: core::iter::range::Step<A>,

fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::min<A>(@1: core::ops::range::Range<A>) -> core::option::Option<A>
fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::nth<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>), @2: usize) -> core::option::Option<A>
where
// Inherited clauses:
[@TraitClause0]: core::iter::range::Step<A>,
// Local clauses:
[@TraitClause1]: core::cmp::Ord<A>,

fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::max<A>(@1: core::ops::range::Range<A>) -> core::option::Option<A>
where
Expand All @@ -456,12 +454,14 @@ where
// Local clauses:
[@TraitClause1]: core::cmp::Ord<A>,

fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::is_sorted<A>(@1: core::ops::range::Range<A>) -> bool
fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::min<A>(@1: core::ops::range::Range<A>) -> core::option::Option<A>
where
// Inherited clauses:
[@TraitClause0]: core::iter::range::Step<A>,
// Local clauses:
[@TraitClause1]: core::cmp::Ord<A>,

fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::advance_by<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26>>
fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::is_sorted<A>(@1: core::ops::range::Range<A>) -> bool
where
// Inherited clauses:
[@TraitClause0]: core::iter::range::Step<A>,
Expand All @@ -481,12 +481,12 @@ where
fn next = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::next
fn size_hint = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::size_hint
fn count = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::count
fn nth = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::nth
fn last = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::last
fn min = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::min
fn advance_by = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::advance_by
fn nth = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::nth
fn max = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::max
fn min = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::min
fn is_sorted = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::is_sorted
fn advance_by = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::advance_by
fn __iterator_get_unchecked = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>}#6::__iterator_get_unchecked
}

Expand All @@ -513,18 +513,18 @@ fn core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::lt<'_0, '_1>(@1

fn core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::le<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool

fn core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::ge<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool

fn core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::gt<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool

fn core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::ge<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool

impl core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60 : core::cmp::PartialOrd<u8, u8>
{
parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq<u8> for u8}#22
fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::partial_cmp
fn lt = core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::lt
fn le = core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::le
fn ge = core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::ge
fn gt = core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::gt
fn ge = core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::ge
}

fn core::iter::range::{impl core::iter::range::Step for u8}#35::steps_between<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> core::option::Option<usize>
Expand All @@ -535,10 +535,10 @@ fn core::iter::range::{impl core::iter::range::Step for u8}#35::backward_checked

fn core::iter::range::{impl core::iter::range::Step for u8}#35::forward(@1: u8, @2: usize) -> u8

fn core::iter::range::{impl core::iter::range::Step for u8}#35::backward(@1: u8, @2: usize) -> u8

unsafe fn core::iter::range::{impl core::iter::range::Step for u8}#35::forward_unchecked(@1: u8, @2: usize) -> u8

fn core::iter::range::{impl core::iter::range::Step for u8}#35::backward(@1: u8, @2: usize) -> u8

unsafe fn core::iter::range::{impl core::iter::range::Step for u8}#35::backward_unchecked(@1: u8, @2: usize) -> u8

impl core::iter::range::{impl core::iter::range::Step for u8}#35 : core::iter::range::Step<u8>
Expand All @@ -549,8 +549,8 @@ impl core::iter::range::{impl core::iter::range::Step for u8}#35 : core::iter::r
fn forward_checked = core::iter::range::{impl core::iter::range::Step for u8}#35::forward_checked
fn backward_checked = core::iter::range::{impl core::iter::range::Step for u8}#35::backward_checked
fn forward = core::iter::range::{impl core::iter::range::Step for u8}#35::forward
fn backward = core::iter::range::{impl core::iter::range::Step for u8}#35::backward
fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for u8}#35::forward_unchecked
fn backward = core::iter::range::{impl core::iter::range::Step for u8}#35::backward
fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for u8}#35::backward_unchecked
}

Expand Down
6 changes: 3 additions & 3 deletions charon/tests/ui/issue-70-override-provided-method.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,18 +124,18 @@ fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::lt<'_0, '_1>(

fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::le<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool

fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::ge<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool

fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::gt<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool

fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::ge<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool

impl core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64 : core::cmp::PartialOrd<u32, u32>
{
parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24
fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::partial_cmp
fn lt = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::lt
fn le = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::le
fn ge = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::ge
fn gt = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::gt
fn ge = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::ge
}

fn core::cmp::PartialOrd::partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> core::option::Option<core::cmp::Ordering>
Expand Down
Loading

0 comments on commit 9e782be

Please sign in to comment.