Skip to content

Commit ad99af7

Browse files
NadrierilNadrieril
authored
Merge pull request #580 from Nadrieril/discriminant-ty
Don't expand builtin associated types
2 parents 31f7c3c + 50a2062 commit ad99af7

File tree

5 files changed

+452
-6
lines changed

5 files changed

+452
-6
lines changed

‎charon/src/transform/expand_associated_types.rs

Lines changed: 15 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -715,12 +715,19 @@ impl<'a> ComputeItemModifications<'a> {
715715
Processing::Processing => false,
716716
Processing::Cyclic => true,
717717
};
718-
let remove_assoc_type = self
719-
.ctx
720-
.options
721-
.remove_associated_types
722-
.iter()
723-
.any(|pat| pat.matches(&self.ctx.translated, &tr.item_meta.name));
718+
// These traits carry a built-in associated type that we can't replace with
719+
// anything else than itself, so we keep it as an associated type.
720+
let has_builtin_assoc_ty = matches!(
721+
tr.item_meta.lang_item.as_deref(),
722+
Some("discriminant_kind" | "pointee_trait")
723+
);
724+
let remove_assoc_type = !has_builtin_assoc_ty
725+
&& self
726+
.ctx
727+
.options
728+
.remove_associated_types
729+
.iter()
730+
.any(|pat| pat.matches(&self.ctx.translated, &tr.item_meta.name));
724731
let remove_assoc_types = !is_self_referential && remove_assoc_type;
725732
let mut modifications =
726733
ItemModifications::new(&tr.generics.trait_type_constraints, remove_assoc_types);
@@ -871,6 +878,8 @@ impl<'a> ComputeItemModifications<'a> {
871878
/// `visit_generic_args` will skip `GenericArgs` meant for traits, and we must manually catch
872879
#[derive(Visitor)]
873880
struct UpdateItemBody<'a> {
881+
/// Warning: we keep the ctx around but we can't meaningfully use it for inspecting items as we
882+
/// remporarily remove them for in-place modification.
874883
ctx: &'a TransformCtx,
875884
span: Span,
876885
item_modifications: &'a HashMap<GenericsSource, ItemModifications>,

‎charon/tests/ui/simple/mem-discriminant-from-derive.out

Lines changed: 222 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,222 @@
1+
# Final LLBC before serialization:
2+
3+
enum test_crate::Enum =
4+
| Some(u8)
5+
| None()
6+
7+
8+
#[lang_item("structural_peq")]
9+
pub trait core::marker::StructuralPartialEq<Self>
10+
11+
impl test_crate::{impl core::marker::StructuralPartialEq for test_crate::Enum} : core::marker::StructuralPartialEq<test_crate::Enum>
12+
13+
#[lang_item("eq")]
14+
pub trait core::cmp::PartialEq<Self, Rhs>
15+
{
16+
fn eq<'_0, '_1> = core::cmp::PartialEq::eq<'_0_0, '_0_1, Self, Rhs>
17+
}
18+
19+
#[lang_item("sized")]
20+
pub trait core::marker::Sized<Self>
21+
22+
#[lang_item("clone")]
23+
pub trait core::clone::Clone<Self>
24+
{
25+
parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
26+
fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
27+
}
28+
29+
#[lang_item("copy")]
30+
pub trait core::marker::Copy<Self>
31+
{
32+
parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
33+
}
34+
35+
#[lang_item("Formatter")]
36+
pub opaque type core::fmt::Formatter<'a>
37+
where
38+
'a : 'a,
39+
40+
#[lang_item("Result")]
41+
pub enum core::result::Result<T, E>
42+
where
43+
[@TraitClause0]: core::marker::Sized<T>,
44+
[@TraitClause1]: core::marker::Sized<E>,
45+
=
46+
| Ok(T)
47+
| Err(E)
48+
49+
50+
pub struct core::fmt::Error = {}
51+
52+
#[lang_item("Debug")]
53+
pub trait core::fmt::Debug<Self>
54+
{
55+
fn fmt<'_0, '_1, '_2> = core::fmt::Debug::fmt<'_0_0, '_0_1, '_0_2, Self>
56+
}
57+
58+
#[lang_item("Eq")]
59+
pub trait core::cmp::Eq<Self>
60+
{
61+
parent_clause0 : [@TraitClause0]: core::cmp::PartialEq<Self, Self>
62+
}
63+
64+
pub trait core::hash::Hasher<Self>
65+
{
66+
fn finish<'_0> = core::hash::Hasher::finish<'_0_0, Self>
67+
fn write<'_0, '_1> = core::hash::Hasher::write<'_0_0, '_0_1, Self>
68+
}
69+
70+
#[lang_item("Hash")]
71+
pub trait core::hash::Hash<Self>
72+
{
73+
fn hash<'_0, '_1, H, [@TraitClause0]: core::marker::Sized<H>, [@TraitClause1]: core::hash::Hasher<H>> = core::hash::Hash::hash<'_0_0, '_0_1, Self, H>[@TraitClause0_0, @TraitClause0_1]
74+
}
75+
76+
#[lang_item("Send")]
77+
pub trait core::marker::Send<Self>
78+
79+
#[lang_item("sync")]
80+
pub trait core::marker::Sync<Self>
81+
82+
#[lang_item("unpin")]
83+
pub trait core::marker::Unpin<Self>
84+
85+
#[lang_item("discriminant_kind")]
86+
pub trait core::marker::DiscriminantKind<Self>
87+
{
88+
parent_clause0 : [@TraitClause0]: core::marker::Sized<core::marker::DiscriminantKind<Self>::Discriminant>
89+
parent_clause1 : [@TraitClause1]: core::clone::Clone<core::marker::DiscriminantKind<Self>::Discriminant>
90+
parent_clause2 : [@TraitClause2]: core::marker::Copy<core::marker::DiscriminantKind<Self>::Discriminant>
91+
parent_clause3 : [@TraitClause3]: core::fmt::Debug<core::marker::DiscriminantKind<Self>::Discriminant>
92+
parent_clause4 : [@TraitClause4]: core::cmp::Eq<core::marker::DiscriminantKind<Self>::Discriminant>
93+
parent_clause5 : [@TraitClause5]: core::cmp::PartialEq<core::marker::DiscriminantKind<Self>::Discriminant, core::marker::DiscriminantKind<Self>::Discriminant>
94+
parent_clause6 : [@TraitClause6]: core::hash::Hash<core::marker::DiscriminantKind<Self>::Discriminant>
95+
parent_clause7 : [@TraitClause7]: core::marker::Send<core::marker::DiscriminantKind<Self>::Discriminant>
96+
parent_clause8 : [@TraitClause8]: core::marker::Sync<core::marker::DiscriminantKind<Self>::Discriminant>
97+
parent_clause9 : [@TraitClause9]: core::marker::Unpin<core::marker::DiscriminantKind<Self>::Discriminant>
98+
type Discriminant
99+
}
100+
101+
pub fn core::intrinsics::discriminant_value<'_0, T>(@1: &'_0 (T)) -> core::marker::DiscriminantKind<T>::Discriminant
102+
where
103+
[@TraitClause0]: core::marker::Sized<T>,
104+
105+
pub fn core::cmp::impls::{impl core::cmp::PartialEq<&'_0 (B)> for &'_1 (A)}#9::eq<'_0, '_1, '_2, '_3, A, B>(@1: &'_2 (&'_1 (A)), @2: &'_3 (&'_0 (B))) -> bool
106+
where
107+
[@TraitClause0]: core::cmp::PartialEq<A, B>,
108+
109+
pub fn core::cmp::impls::{impl core::cmp::PartialEq<u8> for u8}#22::eq<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool
110+
111+
impl core::cmp::impls::{impl core::cmp::PartialEq<u8> for u8}#22 : core::cmp::PartialEq<u8, u8>
112+
{
113+
fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<u8> for u8}#22::eq<'_0_0, '_0_1>
114+
}
115+
116+
pub fn test_crate::{impl core::cmp::PartialEq<test_crate::Enum> for test_crate::Enum}#1::eq<'_0, '_1>(@1: &'_0 (test_crate::Enum), @2: &'_1 (test_crate::Enum)) -> bool
117+
{
118+
let @0: bool; // return
119+
let self@1: &'_ (test_crate::Enum); // arg #1
120+
let other@2: &'_ (test_crate::Enum); // arg #2
121+
let __self_discr@3: isize; // local
122+
let @4: &'_ (test_crate::Enum); // anonymous local
123+
let __arg1_discr@5: isize; // local
124+
let @6: &'_ (test_crate::Enum); // anonymous local
125+
let @7: bool; // anonymous local
126+
let @8: isize; // anonymous local
127+
let @9: isize; // anonymous local
128+
let @10: (&'_ (test_crate::Enum), &'_ (test_crate::Enum)); // anonymous local
129+
let @11: &'_ (test_crate::Enum); // anonymous local
130+
let @12: &'_ (test_crate::Enum); // anonymous local
131+
let __self_0@13: &'_ (u8); // local
132+
let __arg1_0@14: &'_ (u8); // local
133+
let @15: &'_ (&'_ (u8)); // anonymous local
134+
let @16: &'_ (&'_ (u8)); // anonymous local
135+
136+
@4 := &*(self@1)
137+
__self_discr@3 := core::intrinsics::discriminant_value<'_, test_crate::Enum>[core::marker::Sized<test_crate::Enum>](move (@4))
138+
drop @4
139+
@fake_read(__self_discr@3)
140+
@6 := &*(other@2)
141+
__arg1_discr@5 := core::intrinsics::discriminant_value<'_, test_crate::Enum>[core::marker::Sized<test_crate::Enum>](move (@6))
142+
drop @6
143+
@fake_read(__arg1_discr@5)
144+
@8 := copy (__self_discr@3)
145+
@9 := copy (__arg1_discr@5)
146+
@7 := move (@8) == move (@9)
147+
if move (@7) {
148+
drop @9
149+
drop @8
150+
@11 := copy (self@1)
151+
@12 := copy (other@2)
152+
@10 := (move (@11), move (@12))
153+
drop @12
154+
drop @11
155+
@fake_read(@10)
156+
match *((@10).0) {
157+
0 => {
158+
match *((@10).1) {
159+
0 => {
160+
__self_0@13 := &(*((@10).0) as variant @0).0
161+
__arg1_0@14 := &(*((@10).1) as variant @0).0
162+
@15 := &__self_0@13
163+
@16 := &__arg1_0@14
164+
@0 := core::cmp::impls::{impl core::cmp::PartialEq<&'_0 (B)> for &'_1 (A)}#9::eq<'_, '_, '_, '_, u8, u8>[core::cmp::impls::{impl core::cmp::PartialEq<u8> for u8}#22](move (@15), move (@16))
165+
drop @16
166+
drop @15
167+
drop __arg1_0@14
168+
drop __self_0@13
169+
},
170+
_ => {
171+
@0 := const (true)
172+
},
173+
}
174+
},
175+
_ => {
176+
@0 := const (true)
177+
},
178+
}
179+
drop @10
180+
}
181+
else {
182+
drop @9
183+
drop @8
184+
@0 := const (false)
185+
}
186+
drop @7
187+
drop __arg1_discr@5
188+
drop __self_discr@3
189+
return
190+
}
191+
192+
impl test_crate::{impl core::cmp::PartialEq<test_crate::Enum> for test_crate::Enum}#1 : core::cmp::PartialEq<test_crate::Enum, test_crate::Enum>
193+
{
194+
fn eq<'_0, '_1> = test_crate::{impl core::cmp::PartialEq<test_crate::Enum> for test_crate::Enum}#1::eq<'_0_0, '_0_1>
195+
}
196+
197+
#[lang_item("cmp_partialeq_eq")]
198+
pub fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
199+
200+
impl core::cmp::impls::{impl core::cmp::PartialEq<&'_0 (B)> for &'_1 (A)}#9<'_0, '_1, A, B> : core::cmp::PartialEq<&'_1 (A), &'_0 (B)>
201+
where
202+
[@TraitClause0]: core::cmp::PartialEq<A, B>,
203+
{
204+
fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<&'_0 (B)> for &'_1 (A)}#9::eq<'_0, '_1, '_0_0, '_0_1, A, B>[@TraitClause0]
205+
}
206+
207+
#[lang_item("clone_fn")]
208+
pub fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
209+
210+
pub fn core::fmt::Debug::fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (core::fmt::Formatter<'_2>)) -> core::result::Result<(), core::fmt::Error>[core::marker::Sized<()>, core::marker::Sized<core::fmt::Error>]
211+
212+
pub fn core::hash::Hash::hash<'_0, '_1, Self, H>(@1: &'_0 (Self), @2: &'_1 mut (H))
213+
where
214+
[@TraitClause0]: core::marker::Sized<H>,
215+
[@TraitClause1]: core::hash::Hasher<H>,
216+
217+
pub fn core::hash::Hasher::finish<'_0, Self>(@1: &'_0 (Self)) -> u64
218+
219+
pub fn core::hash::Hasher::write<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Slice<u8>))
220+
221+
222+

‎charon/tests/ui/simple/mem-discriminant-from-derive.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
//@ charon-args=--remove-associated-types=*
2+
// This derive generates code that uses `mem::discriminant`, which involves the builtin associated
3+
// type `<T as DiscriminantKind>::Discriminant`.
4+
#[derive(PartialEq)]
5+
enum Enum {
6+
Some(u8),
7+
None,
8+
}

0 commit comments

Comments
 (0)