Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Let charon manage Self clauses #413

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
+213 −319
Open

Let charon manage Self clauses #413

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion charon-pin
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
df3b7fd4c1277827c92b4a2cb84347f1f54d92a6
c7243f2ffb89f16f07cb0eda67478b33640ee3c7
12 changes: 6 additions & 6 deletions flake.lock
View file
Open in desktop

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

1 change: 0 additions & 1 deletion src/Translate.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1126,7 +1126,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
use_dep_ite =
Config.backend () = Lean && !Config.extract_decreases_clauses;
trait_decl_id = None (* None by default *);
is_provided_method = false (* false by default *);
trans_trait_decls;
trans_trait_impls;
trans_types;
Expand Down
112 changes: 55 additions & 57 deletions src/extract/Extract.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -505,51 +505,63 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx)
true
]}
*)
(match fun_id with
| FromLlbc (TraitMethod (trait_ref, method_name, _fun_decl_id), lp_id) ->
(* We have to check whether the trait method is required or provided *)
let trait_decl_id = trait_ref.trait_decl_ref.trait_decl_id in
let trait_decl =
TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls
in
let method_id =
PureUtils.trait_decl_get_method trait_decl method_name
in

if not method_id.is_provided then (
(* Required method *)
sanity_check __FILE__ __LINE__ (lp_id = None)
trait_decl.item_meta.span;
extract_trait_ref trait_decl.item_meta.span ctx fmt
TypeDeclId.Set.empty true trait_ref;
let fun_name =
ctx_get_trait_method span trait_ref.trait_decl_ref.trait_decl_id
method_name ctx
in
let add_brackets (s : string) =
if backend () = Coq then "(" ^ s ^ ")" else s
let generics =
match fun_id with
| FromLlbc (TraitMethod (trait_ref, method_name, _fun_decl_id), lp_id)
->
(* We have to check whether the trait method is required or provided *)
let trait_decl_id = trait_ref.trait_decl_ref.trait_decl_id in
let trait_decl =
TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls
in
F.pp_print_string fmt ("." ^ add_brackets fun_name))
else
(* Provided method: we see it as a regular function call, and use
the function name *)
let fun_id = FromLlbc (FunId (FRegular method_id.id), lp_id) in
let fun_name =
ctx_get_function trait_decl.item_meta.span fun_id ctx
let bound_method =
PureUtils.trait_decl_get_method trait_decl method_name
in
F.pp_print_string fmt fun_name;

(* Note that we do not need to print the generics for the trait
declaration: they are always implicit as they can be deduced
from the trait self clause.
if not bound_method.is_provided then begin
(* Required method *)
sanity_check __FILE__ __LINE__ (lp_id = None)
trait_decl.item_meta.span;
extract_trait_ref trait_decl.item_meta.span ctx fmt
TypeDeclId.Set.empty true trait_ref;
let fun_name =
ctx_get_trait_method span trait_ref.trait_decl_ref.trait_decl_id
method_name ctx
in
let add_brackets (s : string) =
if backend () = Coq then "(" ^ s ^ ")" else s
in
F.pp_print_string fmt ("." ^ add_brackets fun_name);
generics
end
else begin
(* Provided method: we see it as a regular function call, and use
the function name. `generics` is generics for the method only;
we must substitute the bound method to get the correct
generics for the function item. *)
let subst =
make_subst_from_generics_including_methods trait_decl.generics
bound_method.bound_method.binder_generics trait_ref.trait_id
trait_ref.trait_decl_ref.decl_generics generics
in
let fn_ref =
subst_visitor#visit_fun_decl_ref subst
bound_method.bound_method.binder_value
in
let fun_id = FromLlbc (FunId (FRegular fn_ref.fun_id), lp_id) in
let fun_name =
ctx_get_function trait_decl.item_meta.span fun_id ctx
in
F.pp_print_string fmt fun_name;

Print the trait ref (to instantate the self clause) *)
F.pp_print_space fmt ();
extract_trait_ref trait_decl.item_meta.span ctx fmt
TypeDeclId.Set.empty true trait_ref
| _ ->
let fun_name = ctx_get_function span fun_id ctx in
F.pp_print_string fmt fun_name);
(* Return the newly-computed function item generics. *)
fn_ref.fun_generics
end
| _ ->
let fun_name = ctx_get_function span fun_id ctx in
F.pp_print_string fmt fun_name;
generics
in

(* Sanity check: HOL4 doesn't support const generics *)
sanity_check __FILE__ __LINE__
Expand Down Expand Up @@ -1296,21 +1308,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
About the order: we want to make sure the names are reserved for
those (variable names might collide with them but it is ok, we will add
suffixes to the variables).

TODO: micro-pass to update what happens when calling trait provided
functions.
*)
let ctx, trait_decl =
match def.kind with
| TraitDeclItem (trait_ref, _, true) ->
let trait_decl =
T.TraitDeclId.Map.find trait_ref.trait_decl_id ctx.trans_trait_decls
in
let ctx, _ = ctx_add_trait_self_clause def.item_meta.span ctx in
let ctx = { ctx with is_provided_method = true } in
(ctx, Some trait_decl)
| _ -> (ctx, None)
in
(* Add the type parameters - note that we need those bindings only for the
* body translation (they are not top-level) *)
let ctx, type_params, cg_params, trait_clauses =
Expand All @@ -1323,8 +1321,8 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
let explicit = def.signature.explicit_info in
(let space = Some space in
extract_generic_params def.item_meta.span ctx fmt TypeDeclId.Set.empty ~space
~trait_decl Item def.signature.generics (Some explicit) type_params
cg_params trait_clauses);
Item def.signature.generics (Some explicit) type_params cg_params
trait_clauses);
(* Close the box for the generics *)
F.pp_close_box fmt ();
(* The input parameters - note that doing this adds bindings to the context *)
Expand Down
74 changes: 1 addition & 73 deletions src/extract/ExtractBase.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,15 +113,7 @@ let decl_is_not_last_from_group (kind : decl_kind) : bool =

type type_decl_kind = Enum | Struct | Tuple [@@deriving show]

(** Generics can be bound in two places: each item has its generics, and
additionally within a trait decl or impl each method has its own generics.
We distinguish these two cases here. In charon, the distinction is made
thanks to `de_bruijn_var`.
Note that for the generics of a top-level `fun_decl` we always use `Item`;
`Method` only refers to the inner binder found in the list of methods in a
trait_decl/trait_impl.
*)
type generic_origin = Item | Method
type generic_origin = PureUtils.generic_origin

(** We use identifiers to look for name clashes *)
and id =
Expand Down Expand Up @@ -183,41 +175,6 @@ and id =
| TraitItemId of TraitDeclId.id * string
(** A trait associated item which is not a method *)
| TraitParentClauseId of TraitDeclId.id * TraitClauseId.id
| TraitSelfClauseId
(** Specifically for the clause: [Self : Trait].

For now, we forbid provided methods (methods in trait declarations
with a default implementation) from being overriden in trait implementations.
We extract trait provided methods such that they take an instance of
the trait as input: this instance is given by the trait self clause.

For instance:
{[
//
// Rust
//
trait ToU64 {
fn to_u64(&self) -> u64;

// Provided method
fn is_pos(&self) -> bool {
self.to_u64() > 0
}
}

//
// Generated code
//
struct ToU64 (T : Type) {
to_u64 : T -> u64;
}

// The trait self clause
// vvvvvvvvvvvvvvvvvvvvvv
let is_pos (T : Type) (trait_self : ToU64 T) (self : T) : bool =
trait_self.to_u64 self > 0
]}
*)
| UnknownId
(** Used for stored various strings like keywords, definitions which
should always be in context, etc. and which can't be linked to one
Expand Down Expand Up @@ -592,7 +549,6 @@ type extraction_ctx = {
*)
trait_decl_id : trait_decl_id option;
(** If we are extracting a trait declaration, identifies it *)
is_provided_method : bool;
trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
trans_funs : pure_fun_translation A.FunDeclId.Map.t;
trans_globals : Pure.global_decl Pure.GlobalDeclId.Map.t;
Expand Down Expand Up @@ -706,7 +662,6 @@ let id_to_string (span : Meta.span option) (id : id) (ctx : extraction_ctx) :
"trait_item_id: " ^ trait_decl_id_to_string id ^ ", type name: " ^ name
| TraitMethodId (trait_decl_id, fun_name) ->
trait_decl_id_to_string trait_decl_id ^ ", method name: " ^ fun_name
| TraitSelfClauseId -> "trait_self_clause"

let ctx_add (span : Meta.span) (id : id) (name : string) (ctx : extraction_ctx)
: extraction_ctx =
Expand Down Expand Up @@ -750,10 +705,6 @@ let ctx_get_trait_constructor (span : Meta.span) (id : trait_decl_id)
(ctx : extraction_ctx) : string =
ctx_get (Some span) (TraitDeclConstructorId id) ctx

let ctx_get_trait_self_clause (span : Meta.span) (ctx : extraction_ctx) : string
=
ctx_get (Some span) TraitSelfClauseId ctx

let ctx_get_trait_decl (span : Meta.span) (id : trait_decl_id)
(ctx : extraction_ctx) : string =
ctx_get (Some span) (TraitDeclId id) ctx
Expand Down Expand Up @@ -786,21 +737,6 @@ let ctx_get_var (span : Meta.span) (id : VarId.id) (ctx : extraction_ctx) :
string =
ctx_get (Some span) (VarId id) ctx

(** This warrants explanations. Charon supports several levels of nested
binders; however there are currently only two cases where we bind
non-lifetime variables: at the top-level of each item, and for each method
inside a trait_decl/trait_impl. Moreover, we use `Free` vars to identify
item-bound vars. This means that we can identify which binder a variable
comes from without rigorously tracking binder levels, which is what this
function does.
Note that the `de_bruijn_id`s are wrong anyway because we kept charon's
binding levels but forgot all the region binders.
*)
let origin_from_de_bruijn_var (var : 'a de_bruijn_var) : generic_origin * 'a =
match var with
| Bound (_, id) -> (Method, id)
| Free id -> (Item, id)

let ctx_get_type_var (span : Meta.span) (origin : generic_origin)
(id : TypeVarId.id) (ctx : extraction_ctx) : string =
ctx_get (Some span) (TypeVarId (origin, id)) ctx
Expand Down Expand Up @@ -2018,14 +1954,6 @@ let ctx_add_var (span : Meta.span) (basename : string) (id : VarId.id)
let ctx = ctx_add span (VarId id) name ctx in
(ctx, name)

(** Generate a unique variable name for the trait self clause and add it to the context *)
let ctx_add_trait_self_clause (span : Meta.span) (ctx : extraction_ctx) :
extraction_ctx * string =
let basename = trait_self_clause_basename in
let name = basename_to_unique ctx basename in
let ctx = ctx_add span TraitSelfClauseId name ctx in
(ctx, name)

(** Generate a unique trait clause name and add it to the context *)
let ctx_add_local_trait_clause (span : Meta.span) (origin : generic_origin)
(basename : string) (id : TraitClauseId.id) (ctx : extraction_ctx) :
Expand Down
Loading
Loading