Skip to content

Commit

Permalink
Transform associated types into type parameters
Browse files Browse the repository at this point in the history
  • Loading branch information
Nadrieril committed Jan 22, 2025
1 parent 686f779 commit 27678ed
Show file tree
Hide file tree
Showing 56 changed files with 1,958 additions and 395 deletions.
2 changes: 1 addition & 1 deletion charon-ml/src/CharonVersion.ml
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
(* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
(* To re-generate this file, rune `make` in the root directory *)
let supported_charon_version = "0.1.63"
let supported_charon_version = "0.1.64"
2 changes: 2 additions & 0 deletions charon-ml/src/generated/Generated_GAst.ml
Original file line number Diff line number Diff line change
Expand Up @@ -417,6 +417,8 @@ and cli_options = {
(** Blacklist of items to keep opaque. These use the name-matcher syntax. *)
exclude : string list;
(** Blacklist of items to not translate at all. These use the name-matcher syntax. *)
remove_associated_types : string list;
(** List of traits for which we transform associated types to type parameters. *)
hide_marker_traits : bool;
(** Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show
up.
Expand Down
14 changes: 13 additions & 1 deletion charon-ml/src/generated/Generated_GAstOfJson.ml
Original file line number Diff line number Diff line change
Expand Up @@ -907,6 +907,13 @@ and trait_clause_id_of_json (ctx : of_json_ctx) (js : json) :
| x -> TraitClauseId.id_of_json ctx x
| _ -> Error "")

and trait_type_constraint_id_of_json (ctx : of_json_ctx) (js : json) :
(trait_type_constraint_id, string) result =
combine_error_msgs js __FUNCTION__
(match js with
| x -> TraitTypeConstraintId.id_of_json ctx x
| _ -> Error "")

and type_var_of_json (ctx : of_json_ctx) (js : json) : (type_var, string) result
=
combine_error_msgs js __FUNCTION__
Expand Down Expand Up @@ -1202,7 +1209,7 @@ and generic_params_of_json (ctx : of_json_ctx) (js : json) :
ctx types_outlive
in
let* trait_type_constraints =
list_of_json
vector_of_json trait_type_constraint_id_of_json
(region_binder_of_json trait_type_constraint_of_json)
ctx trait_type_constraints
in
Expand Down Expand Up @@ -1619,6 +1626,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
("include", include_);
("opaque", opaque);
("exclude", exclude);
("remove_associated_types", remove_associated_types);
("hide_marker_traits", hide_marker_traits);
("no_cargo", no_cargo);
("rustc_args", rustc_args);
Expand Down Expand Up @@ -1647,6 +1655,9 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
let* included = list_of_json string_of_json ctx include_ in
let* opaque = list_of_json string_of_json ctx opaque in
let* exclude = list_of_json string_of_json ctx exclude in
let* remove_associated_types =
list_of_json string_of_json ctx remove_associated_types
in
let* hide_marker_traits = bool_of_json ctx hide_marker_traits in
let* no_cargo = bool_of_json ctx no_cargo in
let* rustc_args = list_of_json string_of_json ctx rustc_args in
Expand Down Expand Up @@ -1676,6 +1687,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
included;
opaque;
exclude;
remove_associated_types;
hide_marker_traits;
no_cargo;
rustc_args;
Expand Down
14 changes: 8 additions & 6 deletions charon-ml/src/generated/Generated_Types.ml
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ module ConstGenericVarId = IdGen ()
module TraitDeclId = IdGen ()
module TraitImplId = IdGen ()
module TraitClauseId = IdGen ()
module TraitTypeConstraintId = IdGen ()
module UnsolvedTraitId = IdGen ()
module RegionId = IdGen ()
module Disambiguator = IdGen ()
Expand All @@ -31,6 +32,11 @@ type integer_type = Values.integer_type [@@deriving show, ord]
type float_type = Values.float_type [@@deriving show, ord]
type literal_type = Values.literal_type [@@deriving show, ord]

(* Manually implemented because no type uses it (we use plain lists instead of
vectors in generic_params), which causes visitor inference problems if we
declare it within a visitor group. *)
type trait_type_constraint_id = TraitTypeConstraintId.id [@@deriving show, ord]

(** We define these types to control the name of the visitor functions *)
type ('id, 'name) indexed_var = {
index : 'id; (** Unique index identifying the variable *)
Expand Down Expand Up @@ -256,12 +262,8 @@ and trait_instance_id =
```
*)
| Self
(** Self, in case of trait declarations/implementations.
Putting [Self] at the end on purpose, so that when ordering the clauses
we start with the other clauses (in particular, the local clauses). It
is useful to give priority to the local clauses when solving the trait
obligations which are fullfilled by the trait parameters.
(** The implicit `Self: Trait` clause. Present inside trait declarations, including trait
method declarations. Not present in trait implementations as we can use `TraitImpl` intead.
*)
| BuiltinOrAuto of
trait_decl_ref region_binder
Expand Down
2 changes: 1 addition & 1 deletion charon/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion charon/Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[package]
name = "charon"
version = "0.1.63"
version = "0.1.64"
authors = ["Son Ho <hosonmarc@gmail.com>"]
edition = "2021"
license = "Apache-2.0"
Expand Down
2 changes: 1 addition & 1 deletion charon/src/ast/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,6 @@ pub use krate::*;
pub use meta::*;
pub use names::*;
pub use types::*;
pub use types_utils::TyVisitable;
pub use types_utils::*;
pub use values::*;
pub use visitor::*;
12 changes: 4 additions & 8 deletions charon/src/ast/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -115,12 +115,8 @@ pub enum TraitRefKind {
#[charon::opaque]
ItemClause(Box<TraitRefKind>, TraitDeclId, TraitItemName, TraitClauseId),

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

Expand Down Expand Up @@ -291,7 +287,7 @@ pub struct GenericParams {
/// The type outlives the region
pub types_outlive: Vec<RegionBinder<TypeOutlives>>,
/// Constraints over trait associated types
pub trait_type_constraints: Vec<RegionBinder<TraitTypeConstraint>>,
pub trait_type_constraints: Vector<TraitTypeConstraintId, RegionBinder<TraitTypeConstraint>>,
}

/// A predicate of the form `exists<T> where T: Trait`.
Expand Down Expand Up @@ -329,7 +325,7 @@ pub enum PredicateOrigin {
// trait Trait {}
// ```
TraitSelf,
// Note: this also includes supertrait constraings.
// Note: this also includes supertrait constraints.
// ```
// trait Trait<T: Clone> {}
// trait Trait<T> where T: Clone {}
Expand Down
1 change: 1 addition & 0 deletions charon/src/ast/types/vars.rs
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,7 @@ generate_index_type!(RegionId, "Region");
generate_index_type!(TypeVarId, "T");
generate_index_type!(ConstGenericVarId, "Const");
generate_index_type!(TraitClauseId, "TraitClause");
generate_index_type!(TraitTypeConstraintId, "TraitTypeConstraint");

/// A type variable in a signature or binder.
#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
Expand Down
92 changes: 92 additions & 0 deletions charon/src/ast/types_utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ use crate::ids::Vector;
use derive_generic_visitor::*;
use std::collections::HashSet;
use std::convert::Infallible;
use std::fmt::Debug;
use std::iter::Iterator;
use std::mem;
use std::ops::Index;
Expand Down Expand Up @@ -130,6 +131,13 @@ impl<T> RegionBinder<T> {
skip_binder: x.move_under_binder(),
}
}

pub fn map_ref<U>(&self, f: impl FnOnce(&T) -> U) -> RegionBinder<U> {
RegionBinder {
regions: self.regions.clone(),
skip_binder: f(&self.skip_binder),
}
}
}

impl GenericArgs {
Expand Down Expand Up @@ -270,6 +278,90 @@ impl IntegerTy {
}
}

/// A value of type `T` bound by the generic parameters of item
/// `item`. Used when dealing with multiple items at a time, to
/// ensure we don't mix up generics.
///
/// To get the value, use `under_binder_of` or `subst_for`.
#[derive(Debug, Clone, Copy)]
pub struct ItemBinder<ItemId, T> {
pub item_id: ItemId,
val: T,
}

impl<ItemId, T> ItemBinder<ItemId, T>
where
ItemId: Debug + Copy + PartialEq,
{
pub fn new(item_id: ItemId, val: T) -> Self {
Self { item_id, val }
}

pub fn as_ref(&self) -> ItemBinder<ItemId, &T> {
ItemBinder {
item_id: self.item_id,
val: &self.val,
}
}

pub fn map_bound<U>(self, f: impl FnOnce(T) -> U) -> ItemBinder<ItemId, U> {
ItemBinder {
item_id: self.item_id,
val: f(self.val),
}
}

fn assert_item_id(&self, item_id: ItemId) {
assert_eq!(
self.item_id, item_id,
"Trying to use item bound for {:?} as if it belonged to {:?}",
self.item_id, item_id
);
}

/// Assert that the value is bound for item `item_id`, and returns it. This is used when we
/// plan to store the returned value inside that item.
pub fn under_binder_of(self, item_id: ItemId) -> T {
self.assert_item_id(item_id);
self.val
}

/// Given generic args for `item_id`, assert that the value is bound for `item_id` and
/// substitute it with the provided generic arguments. Because the arguments are bound in the
/// context of another item, so it the resulting substituted value.
pub fn substitute<OtherItem: Debug + Copy + PartialEq>(
self,
args: ItemBinder<OtherItem, &GenericArgs>,
) -> ItemBinder<OtherItem, T>
where
ItemId: Into<AnyTransId>,
T: TyVisitable,
{
args.map_bound(|args| {
assert_eq!(
args.target,
GenericsSource::item(self.item_id),
"These `GenericArgs` are meant for {:?} but were used on {:?}",
args.target,
self.item_id
);
let mut val = self.val;
val.substitute(args);
val
})
}
}

/// Dummy item identifier that represents the current item when not ambiguous.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct CurrentItem;

impl<T> ItemBinder<CurrentItem, T> {
pub fn under_current_binder(self) -> T {
self.val
}
}

impl Ty {
/// Return true if it is actually unit (i.e.: 0-tuple)
pub fn is_unit(&self) -> bool {
Expand Down
8 changes: 4 additions & 4 deletions charon/src/ast/visitor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,8 +46,8 @@ use index_vec::Idx;
FnOperand, FunId, FunIdOrTraitMethodRef, FunSig, ImplElem, IntegerTy, Literal, LiteralTy,
llbc_ast::Block, llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Switch,
Locals, Name, NullOp, Opaque, Operand, PathElem, Place, PlaceKind, ProjectionElem, RawConstantExpr,
RefKind, RegionId, RegionVar, Rvalue, ScalarValue, TraitClause, TraitClauseId, TraitItemName,
TraitRefKind, TraitTypeConstraint, TranslatedCrate, TyKind, TypeDeclKind, TypeId, TypeVar, TypeVarId,
RefKind, RegionId, RegionVar, Rvalue, ScalarValue, TraitClauseId, TraitItemName,
TranslatedCrate, TypeDeclKind, TypeId, TypeVar, TypeVarId,
ullbc_ast::BlockData, ullbc_ast::BlockId, ullbc_ast::ExprBody, ullbc_ast::RawStatement,
ullbc_ast::RawTerminator, ullbc_ast::SwitchTargets, ullbc_ast::Terminator,
UnOp, Var, Variant, VariantId, VarId,
Expand All @@ -62,9 +62,9 @@ use index_vec::Idx;
// Types for which we call the corresponding `visit_$ty` method, which by default explores the
// type but can be overridden.
override(
DeBruijnId, Ty, Region, ConstGeneric, TraitRef,
DeBruijnId, Ty, TyKind, Region, ConstGeneric, TraitRef, TraitRefKind,
FunDeclRef, GlobalDeclRef, TraitDeclRef, TraitImplRef,
GenericArgs, GenericParams,
GenericArgs, GenericParams, TraitClause, TraitTypeConstraint,
for<T: AstVisitable + Idx> DeBruijnVar<T>,
for<T: AstVisitable> RegionBinder<T>,
for<T: AstVisitable> Binder<T>,
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
use super::translate_ctx::*;
use charon_lib::ast::*;
use charon_lib::options::CliOpts;
use charon_lib::transform::ctx::TransformOptions;
use charon_lib::transform::TransformCtx;
use hax_frontend_exporter as hax;
use rustc_hir::def_id::DefId;
Expand Down Expand Up @@ -297,13 +296,9 @@ pub fn translate<'tcx, 'ctx>(
}

// Return the context, dropping the hax state and rustc `tcx`.
let transform_options = TransformOptions {
no_code_duplication: options.no_code_duplication,
hide_marker_traits: options.hide_marker_traits,
no_merge_goto_chains: options.no_merge_goto_chains,
print_built_llbc: options.print_built_llbc,
item_opacities: ctx.options.item_opacities,
};
let transform_options = ctx
.options
.into_transform_options(&mut *ctx.errors.borrow_mut(), options);

TransformCtx {
options: transform_options,
Expand Down
25 changes: 25 additions & 0 deletions charon/src/bin/charon-driver/translate/translate_ctx.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ use charon_lib::formatter::{FmtCtx, IntoFormatter};
use charon_lib::ids::{MapGenerator, Vector};
use charon_lib::name_matcher::NamePattern;
use charon_lib::options::CliOpts;
use charon_lib::transform::ctx::TransformOptions;
use charon_lib::ullbc_ast as ast;
use hax_frontend_exporter::SInto;
use hax_frontend_exporter::{self as hax, DefPathItem};
Expand Down Expand Up @@ -49,6 +50,8 @@ pub struct TranslateOptions {
/// matches determines the opacity of the item. When no options are provided this is initialized
/// to treat items in the crate as transparent and items in other crates as foreign.
pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
/// List of traits for which we transform associated types to type parameters.
pub remove_associated_types: Vec<NamePattern>,
}

impl TranslateOptions {
Expand Down Expand Up @@ -110,9 +113,31 @@ impl TranslateOptions {
.collect()
};

let remove_associated_types = options
.remove_associated_types
.iter()
.filter_map(|s| parse_pattern(&s).ok())
.collect();

TranslateOptions {
mir_level,
item_opacities,
remove_associated_types,
}
}

pub(crate) fn into_transform_options(
self,
_error_ctx: &mut ErrorCtx,
options: &CliOpts,
) -> TransformOptions {
TransformOptions {
no_code_duplication: options.no_code_duplication,
hide_marker_traits: options.hide_marker_traits,
no_merge_goto_chains: options.no_merge_goto_chains,
print_built_llbc: options.print_built_llbc,
item_opacities: self.item_opacities,
remove_associated_types: self.remove_associated_types,
}
}
}
Expand Down
8 changes: 7 additions & 1 deletion charon/src/bin/generate-ml/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1078,7 +1078,13 @@ fn generate_ml(
),
];
// Types for which we don't want to generate a type at all.
let dont_generate_ty = &["ItemOpacity", "PredicateOrigin", "Ty", "Vector"];
let dont_generate_ty = &[
"ItemOpacity",
"PredicateOrigin",
"TraitTypeConstraintId",
"Ty",
"Vector",
];
// Types that we don't want visitors to go into.
let opaque_for_visitor = &["Name"];
let ctx = GenerateCtx::new(
Expand Down
Loading

0 comments on commit 27678ed

Please sign in to comment.