Skip to content

Commit ea6cacb

Browse files
N1arkN1ark
committed
Add fn_[once_,mut_]impl to ClosureInfo (fails)
1 parent 35fa711 commit ea6cacb

File tree

10 files changed

+318
-225
lines changed

10 files changed

+318
-225
lines changed

‎charon/src/ast/types.rs

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -821,10 +821,12 @@ impl ClosureKind {
821821
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
822822
pub struct ClosureInfo {
823823
pub kind: ClosureKind,
824-
/// The function id of the closure's original kind. For instance, a `Fn` closure will have a
825-
/// function for its `FnOnce`, `FnMut` and `Fn` traits, but here we would only specify the
826-
/// id of the `Fn` function.
827-
pub fun_id: FunDeclId,
824+
/// The `FnOnce` implementation of this closure -- always exists.
825+
pub fn_once_impl: TraitImplRef,
826+
/// The `FnMut` implementation of this closure, if any.
827+
pub fn_mut_impl: Option<TraitImplRef>,
828+
/// The `Fn` implementation of this closure, if any.
829+
pub fn_impl: Option<TraitImplRef>,
828830
/// The signature of the function that this closure represents.
829831
pub signature: RegionBinder<(Vec<Ty>, Ty)>,
830832
}

‎charon/src/bin/charon-driver/translate/translate_closures.rs

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -67,8 +67,19 @@ impl ItemTransCtx<'_, '_> {
6767
id: &hax::DefId,
6868
args: &hax::ClosureArgs,
6969
) -> Result<ClosureInfo, Error> {
70+
use ClosureKind::*;
7071
let kind = translate_closure_kind(&args.kind);
71-
let fun_id = self.register_closure_method_decl_id(span, id, kind);
72+
let fn_once_impl = self.translate_closure_impl_ref(span, id, args, FnOnce)?;
73+
let fn_mut_impl = if matches!(kind, FnMut | Fn) {
74+
Some(self.translate_closure_impl_ref(span, id, args, FnMut)?)
75+
} else {
76+
None
77+
};
78+
let fn_impl = if matches!(kind, Fn) {
79+
Some(self.translate_closure_impl_ref(span, id, args, Fn)?)
80+
} else {
81+
None
82+
};
7283
let signature = self.translate_region_binder(span, &args.untupled_sig, |ctx, sig| {
7384
let inputs = sig
7485
.inputs
@@ -80,7 +91,9 @@ impl ItemTransCtx<'_, '_> {
8091
})?;
8192
Ok(ClosureInfo {
8293
kind,
83-
fun_id,
94+
fn_once_impl,
95+
fn_mut_impl,
96+
fn_impl,
8497
signature,
8598
})
8699
}

‎charon/tests/ui/closure-as-fn.out

Lines changed: 32 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -29,22 +29,6 @@ fn main()
2929
return
3030
}
3131

32-
// Full name: test_crate::main::{impl Fn<()> for closure}::call
33-
fn {impl Fn<()> for closure}::call<'_0>(@1: &'_0 (closure), @2: ())
34-
{
35-
let @0: (); // return
36-
let @1: &'_ (closure); // arg #1
37-
let tupled_args@2: (); // arg #2
38-
let @3: i32; // anonymous local
39-
40-
storage_live(@3)
41-
@3 := const (1 : i32) / const (0 : i32)
42-
storage_dead(@3)
43-
@0 := ()
44-
@0 := ()
45-
return
46-
}
47-
4832
// Full name: core::marker::Sized
4933
#[lang_item("sized")]
5034
pub trait Sized<Self>
@@ -64,24 +48,20 @@ pub trait FnOnce<Self, Args>
6448
fn call_once = core::ops::function::FnOnce::call_once<Self, Args>[Self]
6549
}
6650

67-
// Full name: core::ops::function::FnMut
68-
#[lang_item("fn_mut")]
69-
pub trait FnMut<Self, Args>
51+
// Full name: test_crate::main::{impl Fn<()> for closure}::call
52+
fn {impl Fn<()> for closure}::call<'_0>(@1: &'_0 (closure), @2: ())
7053
{
71-
parent_clause0 : [@TraitClause0]: FnOnce<Self, Args>
72-
parent_clause1 : [@TraitClause1]: Sized<Args>
73-
parent_clause2 : [@TraitClause2]: Tuple<Args>
74-
fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self]
75-
}
54+
let @0: (); // return
55+
let @1: &'_ (closure); // arg #1
56+
let tupled_args@2: (); // arg #2
57+
let @3: i32; // anonymous local
7658

77-
// Full name: core::ops::function::Fn
78-
#[lang_item("r#fn")]
79-
pub trait Fn<Self, Args>
80-
{
81-
parent_clause0 : [@TraitClause0]: FnMut<Self, Args>
82-
parent_clause1 : [@TraitClause1]: Sized<Args>
83-
parent_clause2 : [@TraitClause2]: Tuple<Args>
84-
fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self]
59+
storage_live(@3)
60+
@3 := const (1 : i32) / const (0 : i32)
61+
storage_dead(@3)
62+
@0 := ()
63+
@0 := ()
64+
return
8565
}
8666

8767
// Full name: test_crate::main::{impl FnMut<()> for closure}::call_mut
@@ -124,6 +104,16 @@ impl FnOnce<()> for closure {
124104
fn call_once = {impl FnOnce<()> for closure}::call_once
125105
}
126106

107+
// Full name: core::ops::function::FnMut
108+
#[lang_item("fn_mut")]
109+
pub trait FnMut<Self, Args>
110+
{
111+
parent_clause0 : [@TraitClause0]: FnOnce<Self, Args>
112+
parent_clause1 : [@TraitClause1]: Sized<Args>
113+
parent_clause2 : [@TraitClause2]: Tuple<Args>
114+
fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self]
115+
}
116+
127117
// Full name: test_crate::main::{impl FnMut<()> for closure}
128118
impl FnMut<()> for closure {
129119
parent_clause0 = {impl FnOnce<()> for closure}
@@ -132,6 +122,16 @@ impl FnMut<()> for closure {
132122
fn call_mut<'_0> = {impl FnMut<()> for closure}::call_mut<'_0_0>
133123
}
134124

125+
// Full name: core::ops::function::Fn
126+
#[lang_item("r#fn")]
127+
pub trait Fn<Self, Args>
128+
{
129+
parent_clause0 : [@TraitClause0]: FnMut<Self, Args>
130+
parent_clause1 : [@TraitClause1]: Sized<Args>
131+
parent_clause2 : [@TraitClause2]: Tuple<Args>
132+
fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self]
133+
}
134+
135135
// Full name: test_crate::main::{impl Fn<()> for closure}
136136
impl Fn<()> for closure {
137137
parent_clause0 = {impl FnMut<()> for closure}

‎charon/tests/ui/generic-associated-types.out

Lines changed: 79 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -58,4 +58,82 @@ error: Error during trait resolution: Found unsupported GAT `Type` when resolvin
5858
55 | x.foo()
5959
| ^^^^^^^
6060

61-
ERROR Charon failed to translate this code (10 errors)
61+
error: Found inconsistent generics after translation:
62+
Mismatched regions:
63+
target: {impl FnOnce<(&'_ (i32))> for closure<'_0>}
64+
expected: ['_0, '_1]
65+
got: ['_0]
66+
Visitor stack:
67+
charon_lib::ast::types::GenericArgs
68+
alloc::boxed::Box<charon_lib::ast::types::GenericArgs>
69+
charon_lib::ast::types::TraitImplRef
70+
charon_lib::ast::types::ClosureInfo
71+
charon_lib::ast::gast::ItemKind
72+
charon_lib::ast::types::TypeDecl
73+
Binding stack (depth 1):
74+
0: <'_0>
75+
--> tests/ui/generic-associated-types.rs:38:20
76+
|
77+
38 | for_each(iter, |item| sum += *item);
78+
| ^^^^^^^^^^^^^^^^^^^
79+
80+
error: Found inconsistent generics after translation:
81+
Mismatched regions:
82+
target: {impl FnMut<(&'_ (i32))> for closure<'_0>}
83+
expected: ['_0, '_1]
84+
got: ['_0]
85+
Visitor stack:
86+
charon_lib::ast::types::GenericArgs
87+
alloc::boxed::Box<charon_lib::ast::types::GenericArgs>
88+
charon_lib::ast::types::TraitImplRef
89+
core::option::Option<charon_lib::ast::types::TraitImplRef>
90+
charon_lib::ast::types::ClosureInfo
91+
charon_lib::ast::gast::ItemKind
92+
charon_lib::ast::types::TypeDecl
93+
Binding stack (depth 1):
94+
0: <'_0>
95+
--> tests/ui/generic-associated-types.rs:38:20
96+
|
97+
38 | for_each(iter, |item| sum += *item);
98+
| ^^^^^^^^^^^^^^^^^^^
99+
100+
error: Found inconsistent generics after transformations:
101+
Mismatched regions:
102+
target: {impl FnOnce<(&'_ (i32))> for closure<'_0>}
103+
expected: ['_0, '_1]
104+
got: ['_0]
105+
Visitor stack:
106+
charon_lib::ast::types::GenericArgs
107+
alloc::boxed::Box<charon_lib::ast::types::GenericArgs>
108+
charon_lib::ast::types::TraitImplRef
109+
charon_lib::ast::types::ClosureInfo
110+
charon_lib::ast::gast::ItemKind
111+
charon_lib::ast::types::TypeDecl
112+
Binding stack (depth 1):
113+
0: <'_0>
114+
--> tests/ui/generic-associated-types.rs:38:20
115+
|
116+
38 | for_each(iter, |item| sum += *item);
117+
| ^^^^^^^^^^^^^^^^^^^
118+
119+
error: Found inconsistent generics after transformations:
120+
Mismatched regions:
121+
target: {impl FnMut<(&'_ (i32))> for closure<'_0>}
122+
expected: ['_0, '_1]
123+
got: ['_0]
124+
Visitor stack:
125+
charon_lib::ast::types::GenericArgs
126+
alloc::boxed::Box<charon_lib::ast::types::GenericArgs>
127+
charon_lib::ast::types::TraitImplRef
128+
core::option::Option<charon_lib::ast::types::TraitImplRef>
129+
charon_lib::ast::types::ClosureInfo
130+
charon_lib::ast::gast::ItemKind
131+
charon_lib::ast::types::TypeDecl
132+
Binding stack (depth 1):
133+
0: <'_0>
134+
--> tests/ui/generic-associated-types.rs:38:20
135+
|
136+
38 | for_each(iter, |item| sum += *item);
137+
| ^^^^^^^^^^^^^^^^^^^
138+
139+
ERROR Charon failed to translate this code (14 errors)

‎charon/tests/ui/issue-323-closure-borrow.out

Lines changed: 27 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -38,26 +38,6 @@ fn new<'_0>(@1: &'_0 mut (Rng))
3838
return
3939
}
4040

41-
// Full name: test_crate::new::{impl FnMut<()> for closure<'_0>}::call_mut
42-
fn {impl FnMut<()> for closure<'_0>}::call_mut<'_0, '_1>(@1: &'_1 mut (closure<'_0>), @2: ())
43-
{
44-
let @0: (); // return
45-
let @1: &'_ mut (closure<'_0>); // arg #1
46-
let tupled_args@2: (); // arg #2
47-
let @3: (); // anonymous local
48-
let @4: &'_ mut (Rng); // anonymous local
49-
50-
storage_live(@3)
51-
storage_live(@4)
52-
@4 := &two-phase-mut *((*(@1)).0)
53-
@3 := next_u64<'_>(move (@4))
54-
storage_dead(@4)
55-
storage_dead(@3)
56-
@0 := ()
57-
@0 := ()
58-
return
59-
}
60-
6141
// Full name: core::marker::Sized
6242
#[lang_item("sized")]
6343
pub trait Sized<Self>
@@ -77,14 +57,24 @@ pub trait FnOnce<Self, Args>
7757
fn call_once = core::ops::function::FnOnce::call_once<Self, Args>[Self]
7858
}
7959

80-
// Full name: core::ops::function::FnMut
81-
#[lang_item("fn_mut")]
82-
pub trait FnMut<Self, Args>
60+
// Full name: test_crate::new::{impl FnMut<()> for closure<'_0>}::call_mut
61+
fn {impl FnMut<()> for closure<'_0>}::call_mut<'_0, '_1>(@1: &'_1 mut (closure<'_0>), @2: ())
8362
{
84-
parent_clause0 : [@TraitClause0]: FnOnce<Self, Args>
85-
parent_clause1 : [@TraitClause1]: Sized<Args>
86-
parent_clause2 : [@TraitClause2]: Tuple<Args>
87-
fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self]
63+
let @0: (); // return
64+
let @1: &'_ mut (closure<'_0>); // arg #1
65+
let tupled_args@2: (); // arg #2
66+
let @3: (); // anonymous local
67+
let @4: &'_ mut (Rng); // anonymous local
68+
69+
storage_live(@3)
70+
storage_live(@4)
71+
@4 := &two-phase-mut *((*(@1)).0)
72+
@3 := next_u64<'_>(move (@4))
73+
storage_dead(@4)
74+
storage_dead(@3)
75+
@0 := ()
76+
@0 := ()
77+
return
8878
}
8979

9080
// Full name: test_crate::new::{impl FnOnce<()> for closure<'_0>}::call_once
@@ -112,6 +102,16 @@ impl<'_0> FnOnce<()> for closure<'_0> {
112102
fn call_once = {impl FnOnce<()> for closure<'_0>}::call_once<'_0>
113103
}
114104

105+
// Full name: core::ops::function::FnMut
106+
#[lang_item("fn_mut")]
107+
pub trait FnMut<Self, Args>
108+
{
109+
parent_clause0 : [@TraitClause0]: FnOnce<Self, Args>
110+
parent_clause1 : [@TraitClause1]: Sized<Args>
111+
parent_clause2 : [@TraitClause2]: Tuple<Args>
112+
fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self]
113+
}
114+
115115
// Full name: test_crate::new::{impl FnMut<()> for closure<'_0>}
116116
impl<'_0> FnMut<()> for closure<'_0> {
117117
parent_clause0 = {impl FnOnce<()> for closure<'_0>}<'_0>

0 commit comments

Comments
 (0)