Skip to content

Commit

Permalink
Let charon manage Self clauses
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril committed Jan 9, 2025
1 parent 62a5530 commit b0b8df7
Show file tree
Hide file tree
Showing 19 changed files with 213 additions and 319 deletions.
2 changes: 1 addition & 1 deletion charon-pin
View file
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

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
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
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
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

0 comments on commit b0b8df7

Please sign in to comment.