Skip to content

Commit d97f20d

Browse files
committed
Transform associated types into type parameters
1 parent b6bcda1 commit d97f20d

Some content is hidden

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

58 files changed

+1996
-394
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
@@ -91,6 +91,7 @@ generate_index_type!(RegionId, "Region");
9191
generate_index_type!(TypeVarId, "T");
9292
generate_index_type!(ConstGenericVarId, "Const");
9393
generate_index_type!(TraitClauseId, "TraitClause");
94+
generate_index_type!(TraitTypeConstraintId, "TraitTypeConstraint");
9495

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

charon/src/ast/types_utils.rs

+104
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;
@@ -128,6 +129,27 @@ impl<T> RegionBinder<T> {
128129
skip_binder: x.move_under_binder(),
129130
}
130131
}
132+
133+
pub fn map_ref<U>(&self, f: impl FnOnce(&T) -> U) -> RegionBinder<U> {
134+
RegionBinder {
135+
regions: self.regions.clone(),
136+
skip_binder: f(&self.skip_binder),
137+
}
138+
}
139+
140+
/// Substitute the bound variables with erased lifetimes.
141+
pub fn erase(self) -> T
142+
where
143+
T: AstVisitable,
144+
{
145+
let mut val = self.skip_binder;
146+
let args = GenericArgs {
147+
regions: self.regions.map_ref_indexed(|_, _| Region::Erased),
148+
..GenericArgs::empty(GenericsSource::Builtin)
149+
};
150+
val.drive_mut(&mut SubstVisitor::new(&args));
151+
val
152+
}
131153
}
132154

133155
impl GenericArgs {
@@ -268,6 +290,88 @@ impl IntegerTy {
268290
}
269291
}
270292

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