Skip to content

Commit bf43b79

Browse files
committed
Transform associated types into type parameters
1 parent 686f779 commit bf43b79

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

56 files changed

+1965
-395
lines changed

charon-ml/src/CharonVersion.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
(* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
22
(* To re-generate this file, rune `make` in the root directory *)
3-
let supported_charon_version = "0.1.63"
3+
let supported_charon_version = "0.1.64"

charon-ml/src/generated/Generated_GAst.ml

+2
Original file line numberDiff line numberDiff line change
@@ -417,6 +417,8 @@ and cli_options = {
417417
(** Blacklist of items to keep opaque. These use the name-matcher syntax. *)
418418
exclude : string list;
419419
(** Blacklist of items to not translate at all. These use the name-matcher syntax. *)
420+
remove_associated_types : string list;
421+
(** List of traits for which we transform associated types to type parameters. *)
420422
hide_marker_traits : bool;
421423
(** Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show
422424
up.

charon-ml/src/generated/Generated_GAstOfJson.ml

+13-1
Original file line numberDiff line numberDiff line change
@@ -907,6 +907,13 @@ and trait_clause_id_of_json (ctx : of_json_ctx) (js : json) :
907907
| x -> TraitClauseId.id_of_json ctx x
908908
| _ -> Error "")
909909

910+
and trait_type_constraint_id_of_json (ctx : of_json_ctx) (js : json) :
911+
(trait_type_constraint_id, string) result =
912+
combine_error_msgs js __FUNCTION__
913+
(match js with
914+
| x -> TraitTypeConstraintId.id_of_json ctx x
915+
| _ -> Error "")
916+
910917
and type_var_of_json (ctx : of_json_ctx) (js : json) : (type_var, string) result
911918
=
912919
combine_error_msgs js __FUNCTION__
@@ -1202,7 +1209,7 @@ and generic_params_of_json (ctx : of_json_ctx) (js : json) :
12021209
ctx types_outlive
12031210
in
12041211
let* trait_type_constraints =
1205-
list_of_json
1212+
vector_of_json trait_type_constraint_id_of_json
12061213
(region_binder_of_json trait_type_constraint_of_json)
12071214
ctx trait_type_constraints
12081215
in
@@ -1619,6 +1626,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
16191626
("include", include_);
16201627
("opaque", opaque);
16211628
("exclude", exclude);
1629+
("remove_associated_types", remove_associated_types);
16221630
("hide_marker_traits", hide_marker_traits);
16231631
("no_cargo", no_cargo);
16241632
("rustc_args", rustc_args);
@@ -1647,6 +1655,9 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
16471655
let* included = list_of_json string_of_json ctx include_ in
16481656
let* opaque = list_of_json string_of_json ctx opaque in
16491657
let* exclude = list_of_json string_of_json ctx exclude in
1658+
let* remove_associated_types =
1659+
list_of_json string_of_json ctx remove_associated_types
1660+
in
16501661
let* hide_marker_traits = bool_of_json ctx hide_marker_traits in
16511662
let* no_cargo = bool_of_json ctx no_cargo in
16521663
let* rustc_args = list_of_json string_of_json ctx rustc_args in
@@ -1676,6 +1687,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
16761687
included;
16771688
opaque;
16781689
exclude;
1690+
remove_associated_types;
16791691
hide_marker_traits;
16801692
no_cargo;
16811693
rustc_args;

charon-ml/src/generated/Generated_Types.ml

+8-6
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ module ConstGenericVarId = IdGen ()
2020
module TraitDeclId = IdGen ()
2121
module TraitImplId = IdGen ()
2222
module TraitClauseId = IdGen ()
23+
module TraitTypeConstraintId = IdGen ()
2324
module UnsolvedTraitId = IdGen ()
2425
module RegionId = IdGen ()
2526
module Disambiguator = IdGen ()
@@ -31,6 +32,11 @@ type integer_type = Values.integer_type [@@deriving show, ord]
3132
type float_type = Values.float_type [@@deriving show, ord]
3233
type literal_type = Values.literal_type [@@deriving show, ord]
3334

35+
(* Manually implemented because no type uses it (we use plain lists instead of
36+
vectors in generic_params), which causes visitor inference problems if we
37+
declare it within a visitor group. *)
38+
type trait_type_constraint_id = TraitTypeConstraintId.id [@@deriving show, ord]
39+
3440
(** We define these types to control the name of the visitor functions *)
3541
type ('id, 'name) indexed_var = {
3642
index : 'id; (** Unique index identifying the variable *)
@@ -256,12 +262,8 @@ and trait_instance_id =
256262
```
257263
*)
258264
| Self
259-
(** Self, in case of trait declarations/implementations.
260-
261-
Putting [Self] at the end on purpose, so that when ordering the clauses
262-
we start with the other clauses (in particular, the local clauses). It
263-
is useful to give priority to the local clauses when solving the trait
264-
obligations which are fullfilled by the trait parameters.
265+
(** The implicit `Self: Trait` clause. Present inside trait declarations, including trait
266+
method declarations. Not present in trait implementations as we can use `TraitImpl` intead.
265267
*)
266268
| BuiltinOrAuto of
267269
trait_decl_ref region_binder

charon/Cargo.lock

+1-1
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

charon/Cargo.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "charon"
3-
version = "0.1.63"
3+
version = "0.1.64"
44
authors = ["Son Ho <hosonmarc@gmail.com>"]
55
edition = "2021"
66
license = "Apache-2.0"

charon/src/ast/mod.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,6 @@ pub use krate::*;
2828
pub use meta::*;
2929
pub use names::*;
3030
pub use types::*;
31-
pub use types_utils::TyVisitable;
31+
pub use types_utils::*;
3232
pub use values::*;
3333
pub use visitor::*;

charon/src/ast/types.rs

+4-8
Original file line numberDiff line numberDiff line change
@@ -115,12 +115,8 @@ pub enum TraitRefKind {
115115
#[charon::opaque]
116116
ItemClause(Box<TraitRefKind>, TraitDeclId, TraitItemName, TraitClauseId),
117117

118-
/// Self, in case of trait declarations/implementations.
119-
///
120-
/// Putting [Self] at the end on purpose, so that when ordering the clauses
121-
/// we start with the other clauses (in particular, the local clauses). It
122-
/// is useful to give priority to the local clauses when solving the trait
123-
/// obligations which are fullfilled by the trait parameters.
118+
/// The implicit `Self: Trait` clause. Present inside trait declarations, including trait
119+
/// method declarations. Not present in trait implementations as we can use `TraitImpl` intead.
124120
#[charon::rename("Self")]
125121
SelfId,
126122

@@ -291,7 +287,7 @@ pub struct GenericParams {
291287
/// The type outlives the region
292288
pub types_outlive: Vec<RegionBinder<TypeOutlives>>,
293289
/// Constraints over trait associated types
294-
pub trait_type_constraints: Vec<RegionBinder<TraitTypeConstraint>>,
290+
pub trait_type_constraints: Vector<TraitTypeConstraintId, RegionBinder<TraitTypeConstraint>>,
295291
}
296292

297293
/// A predicate of the form `exists<T> where T: Trait`.
@@ -329,7 +325,7 @@ pub enum PredicateOrigin {
329325
// trait Trait {}
330326
// ```
331327
TraitSelf,
332-
// Note: this also includes supertrait constraings.
328+
// Note: this also includes supertrait constraints.
333329
// ```
334330
// trait Trait<T: Clone> {}
335331
// trait Trait<T> where T: Clone {}

charon/src/ast/types/vars.rs

+1
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,7 @@ generate_index_type!(RegionId, "Region");
9494
generate_index_type!(TypeVarId, "T");
9595
generate_index_type!(ConstGenericVarId, "Const");
9696
generate_index_type!(TraitClauseId, "TraitClause");
97+
generate_index_type!(TraitTypeConstraintId, "TraitTypeConstraint");
9798

9899
/// A type variable in a signature or binder.
99100
#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]

charon/src/ast/types_utils.rs

+106
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ use crate::ids::Vector;
44
use derive_generic_visitor::*;
55
use std::collections::HashSet;
66
use std::convert::Infallible;
7+
use std::fmt::Debug;
78
use std::iter::Iterator;
89
use std::mem;
910
use std::ops::Index;
@@ -130,6 +131,27 @@ impl<T> RegionBinder<T> {
130131
skip_binder: x.move_under_binder(),
131132
}
132133
}
134+
135+
pub fn map_ref<U>(&self, f: impl FnOnce(&T) -> U) -> RegionBinder<U> {
136+
RegionBinder {
137+
regions: self.regions.clone(),
138+
skip_binder: f(&self.skip_binder),
139+
}
140+
}
141+
142+
/// Substitute the bound variables with erased lifetimes.
143+
pub fn erase(self) -> T
144+
where
145+
T: AstVisitable,
146+
{
147+
let mut val = self.skip_binder;
148+
let args = GenericArgs {
149+
regions: self.regions.map_ref_indexed(|_, _| Region::Erased),
150+
..GenericArgs::empty(GenericsSource::Builtin)
151+
};
152+
val.drive_mut(&mut SubstVisitor::new(&args));
153+
val
154+
}
133155
}
134156

135157
impl GenericArgs {
@@ -270,6 +292,90 @@ impl IntegerTy {
270292
}
271293
}
272294

295+
/// A value of type `T` bound by the generic parameters of item
296+
/// `item`. Used when dealing with multiple items at a time, to
297+
/// ensure we don't mix up generics.
298+
///
299+
/// To get the value, use `under_binder_of` or `subst_for`.
300+
#[derive(Debug, Clone, Copy)]
301+
pub struct ItemBinder<ItemId, T> {
302+
pub item_id: ItemId,
303+
val: T,
304+
}
305+
306+
impl<ItemId, T> ItemBinder<ItemId, T>
307+
where
308+
ItemId: Debug + Copy + PartialEq,
309+
{
310+
pub fn new(item_id: ItemId, val: T) -> Self {
311+
Self { item_id, val }
312+
}
313+
314+
pub fn as_ref(&self) -> ItemBinder<ItemId, &T> {
315+
ItemBinder {
316+
item_id: self.item_id,
317+
val: &self.val,
318+
}
319+
}
320+
321+
pub fn map_bound<U>(self, f: impl FnOnce(T) -> U) -> ItemBinder<ItemId, U> {
322+
ItemBinder {
323+
item_id: self.item_id,
324+
val: f(self.val),
325+
}
326+
}
327+
328+
fn assert_item_id(&self, item_id: ItemId) {
329+
assert_eq!(
330+
self.item_id, item_id,
331+
"Trying to use item bound for {:?} as if it belonged to {:?}",
332+
self.item_id, item_id
333+
);
334+
}
335+
336+
/// Assert that the value is bound for item `item_id`, and returns it. This is used when we
337+
/// plan to store the returned value inside that item.
338+
pub fn under_binder_of(self, item_id: ItemId) -> T {
339+
self.assert_item_id(item_id);
340+
self.val
341+
}
342+
343+
/// Given generic args for `item_id`, assert that the value is bound for `item_id` and
344+
/// substitute it with the provided generic arguments. Because the arguments are bound in the
345+
/// context of another item, so it the resulting substituted value.
346+
pub fn substitute<OtherItem: Debug + Copy + PartialEq>(
347+
self,
348+
args: ItemBinder<OtherItem, &GenericArgs>,
349+
) -> ItemBinder<OtherItem, T>
350+
where
351+
ItemId: Into<AnyTransId>,
352+
T: TyVisitable,
353+
{
354+
args.map_bound(|args| {
355+
assert_eq!(
356+
args.target,
357+
GenericsSource::item(self.item_id),
358+
"These `GenericArgs` are meant for {:?} but were used on {:?}",
359+
args.target,
360+
self.item_id
361+
);
362+
let mut val = self.val;
363+
val.substitute(args);
364+
val
365+
})
366+
}
367+
}
368+
369+
/// Dummy item identifier that represents the current item when not ambiguous.
370+
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
371+
pub struct CurrentItem;
372+
373+
impl<T> ItemBinder<CurrentItem, T> {
374+
pub fn under_current_binder(self) -> T {
375+
self.val
376+
}
377+
}
378+
273379
impl Ty {
274380
/// Return true if it is actually unit (i.e.: 0-tuple)
275381
pub fn is_unit(&self) -> bool {

charon/src/ast/visitor.rs

+4-4
Original file line numberDiff line numberDiff line change
@@ -46,8 +46,8 @@ use index_vec::Idx;
4646
FnOperand, FunId, FunIdOrTraitMethodRef, FunSig, ImplElem, IntegerTy, Literal, LiteralTy,
4747
llbc_ast::Block, llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Switch,
4848
Locals, Name, NullOp, Opaque, Operand, PathElem, Place, PlaceKind, ProjectionElem, RawConstantExpr,
49-
RefKind, RegionId, RegionVar, Rvalue, ScalarValue, TraitClause, TraitClauseId, TraitItemName,
50-
TraitRefKind, TraitTypeConstraint, TranslatedCrate, TyKind, TypeDeclKind, TypeId, TypeVar, TypeVarId,
49+
RefKind, RegionId, RegionVar, Rvalue, ScalarValue, TraitClauseId, TraitItemName,
50+
TranslatedCrate, TypeDeclKind, TypeId, TypeVar, TypeVarId,
5151
ullbc_ast::BlockData, ullbc_ast::BlockId, ullbc_ast::ExprBody, ullbc_ast::RawStatement,
5252
ullbc_ast::RawTerminator, ullbc_ast::SwitchTargets, ullbc_ast::Terminator,
5353
UnOp, Var, Variant, VariantId, VarId,
@@ -62,9 +62,9 @@ use index_vec::Idx;
6262
// Types for which we call the corresponding `visit_$ty` method, which by default explores the
6363
// type but can be overridden.
6464
override(
65-
DeBruijnId, Ty, Region, ConstGeneric, TraitRef,
65+
DeBruijnId, Ty, TyKind, Region, ConstGeneric, TraitRef, TraitRefKind,
6666
FunDeclRef, GlobalDeclRef, TraitDeclRef, TraitImplRef,
67-
GenericArgs, GenericParams,
67+
GenericArgs, GenericParams, TraitClause, TraitTypeConstraint,
6868
for<T: AstVisitable + Idx> DeBruijnVar<T>,
6969
for<T: AstVisitable> RegionBinder<T>,
7070
for<T: AstVisitable> Binder<T>,

charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs

+3-8
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
use super::translate_ctx::*;
22
use charon_lib::ast::*;
33
use charon_lib::options::CliOpts;
4-
use charon_lib::transform::ctx::TransformOptions;
54
use charon_lib::transform::TransformCtx;
65
use hax_frontend_exporter as hax;
76
use rustc_hir::def_id::DefId;
@@ -297,13 +296,9 @@ pub fn translate<'tcx, 'ctx>(
297296
}
298297

299298
// Return the context, dropping the hax state and rustc `tcx`.
300-
let transform_options = TransformOptions {
301-
no_code_duplication: options.no_code_duplication,
302-
hide_marker_traits: options.hide_marker_traits,
303-
no_merge_goto_chains: options.no_merge_goto_chains,
304-
print_built_llbc: options.print_built_llbc,
305-
item_opacities: ctx.options.item_opacities,
306-
};
299+
let transform_options = ctx
300+
.options
301+
.into_transform_options(&mut *ctx.errors.borrow_mut(), options);
307302

308303
TransformCtx {
309304
options: transform_options,

charon/src/bin/charon-driver/translate/translate_ctx.rs

+25
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ use charon_lib::formatter::{FmtCtx, IntoFormatter};
66
use charon_lib::ids::{MapGenerator, Vector};
77
use charon_lib::name_matcher::NamePattern;
88
use charon_lib::options::CliOpts;
9+
use charon_lib::transform::ctx::TransformOptions;
910
use charon_lib::ullbc_ast as ast;
1011
use hax_frontend_exporter::SInto;
1112
use hax_frontend_exporter::{self as hax, DefPathItem};
@@ -49,6 +50,8 @@ pub struct TranslateOptions {
4950
/// matches determines the opacity of the item. When no options are provided this is initialized
5051
/// to treat items in the crate as transparent and items in other crates as foreign.
5152
pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
53+
/// List of traits for which we transform associated types to type parameters.
54+
pub remove_associated_types: Vec<NamePattern>,
5255
}
5356

5457
impl TranslateOptions {
@@ -110,9 +113,31 @@ impl TranslateOptions {
110113
.collect()
111114
};
112115

116+
let remove_associated_types = options
117+
.remove_associated_types
118+
.iter()
119+
.filter_map(|s| parse_pattern(&s).ok())
120+
.collect();
121+
113122
TranslateOptions {
114123
mir_level,
115124
item_opacities,
125+
remove_associated_types,
126+
}
127+
}
128+
129+
pub(crate) fn into_transform_options(
130+
self,
131+
_error_ctx: &mut ErrorCtx,
132+
options: &CliOpts,
133+
) -> TransformOptions {
134+
TransformOptions {
135+
no_code_duplication: options.no_code_duplication,
136+
hide_marker_traits: options.hide_marker_traits,
137+
no_merge_goto_chains: options.no_merge_goto_chains,
138+
print_built_llbc: options.print_built_llbc,
139+
item_opacities: self.item_opacities,
140+
remove_associated_types: self.remove_associated_types,
116141
}
117142
}
118143
}

0 commit comments

Comments
 (0)