diff --git a/charon-ml/Makefile b/charon-ml/Makefile index 3b24a1d80..9a731b87e 100644 --- a/charon-ml/Makefile +++ b/charon-ml/Makefile @@ -11,7 +11,7 @@ build-dev: # You can use the environment variable "CHARON_LOG" to activate the log. # For instance: `CHARON_LOG=1 make tests`. .PHONY: tests -tests: build copy-tests +tests: copy-tests dune test # Reformat the code diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index a4b95e419..7244d81f4 100644 --- a/charon-ml/src/CharonVersion.ml +++ b/charon-ml/src/CharonVersion.ml @@ -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.10" +let supported_charon_version = "0.1.15" diff --git a/charon-ml/src/GAst.ml b/charon-ml/src/GAst.ml index 4fa20e308..7083b3587 100644 --- a/charon-ml/src/GAst.ml +++ b/charon-ml/src/GAst.ml @@ -9,6 +9,14 @@ module TraitDeclId = Types.TraitDeclId module TraitImplId = Types.TraitImplId module TraitClauseId = Types.TraitClauseId +type any_decl_id = + | IdFun of FunDeclId.id + | IdGlobal of GlobalDeclId.id + | IdType of TypeDeclId.id + | IdTraitDecl of TraitDeclId.id + | IdTraitImpl of TraitImplId.id +[@@deriving show, ord] + type fun_decl_id = FunDeclId.id [@@deriving show, ord] type assumed_fun_id = Expressions.assumed_fun_id [@@deriving show, ord] type fun_id = Expressions.fun_id [@@deriving show, ord] @@ -31,14 +39,14 @@ type var = { class ['self] iter_ast_base = object (_self : 'self) inherit [_] iter_rvalue - inherit! [_] iter_predicates + inherit! [_] iter_generic_params end (** Ancestor the AST map visitors *) class ['self] map_ast_base = object (_self : 'self) inherit [_] map_rvalue - inherit! [_] map_predicates + inherit! [_] map_generic_params end (* Below: the types need not be mutually recursive, but it makes it easier @@ -98,7 +106,6 @@ type fun_sig = { is_closure : bool; closure_info : closure_info option; generics : generic_params; - preds : predicates; parent_params_info : params_info option; inputs : ty list; output : ty; @@ -154,7 +161,6 @@ type trait_decl = { is_local : bool; name : name; generics : generic_params; - preds : predicates; parent_clauses : trait_clause list; consts : (trait_item_name * (ty * global_decl_id option)) list; types : (trait_item_name * (trait_clause list * ty option)) list; @@ -170,7 +176,6 @@ type trait_impl = { name : name; impl_trait : trait_decl_ref; generics : generic_params; - preds : predicates; parent_trait_refs : trait_ref list; consts : (trait_item_name * (ty * global_decl_id)) list; types : (trait_item_name * (trait_ref list * ty)) list; @@ -190,6 +195,8 @@ type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show] type trait_declaration_group = TraitDeclId.id g_declaration_group [@@deriving show] +type mixed_declaration_group = any_decl_id g_declaration_group [@@deriving show] + (** Module declaration. Globals cannot be mutually recursive. *) type declaration_group = | TypeGroup of type_declaration_group @@ -197,6 +204,7 @@ type declaration_group = | GlobalGroup of GlobalDeclId.id | TraitDeclGroup of trait_declaration_group | TraitImplGroup of TraitImplId.id + | MixedGroup of mixed_declaration_group [@@deriving show] type 'body gglobal_decl = { @@ -205,7 +213,6 @@ type 'body gglobal_decl = { is_local : bool; name : name; generics : generic_params; - preds : predicates; ty : ty; kind : item_kind; body : 'body; diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index 4978dfcee..0f68c1c97 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/charon-ml/src/GAstOfJson.ml @@ -135,12 +135,14 @@ let item_meta_of_json (id_to_file : id_to_file_map) (js : json) : ("attributes", attributes); ("inline", inline); ("public", public); + ("rename", rename); ] -> let* span = span_of_json id_to_file span in let* attributes = list_of_json string_of_json attributes in let* inline = option_of_json inline_attr_of_json inline in let* public = bool_of_json public in - Ok { span; attributes; inline; public } + let* rename = string_option_of_json rename in + Ok { span; attributes; inline; public; rename } | _ -> Error "") let type_var_of_json (js : json) : (type_var, string) result = @@ -452,11 +454,11 @@ let field_of_json (id_to_file : id_to_file_map) (js : json) : (field, string) result = combine_error_msgs js __FUNCTION__ (match js with - | `Assoc [ ("span", span); ("name", name); ("ty", ty) ] -> - let* span = span_of_json id_to_file span in + | `Assoc [ ("item_meta", item_meta); ("name", name); ("ty", ty) ] -> + let* item_meta = item_meta_of_json id_to_file item_meta in let* name = option_of_json string_of_json name in let* ty = ty_of_json ty in - Ok { span; field_name = name; field_ty = ty } + Ok { item_meta; field_name = name; field_ty = ty } | _ -> Error "") let variant_of_json (id_to_file : id_to_file_map) (js : json) : @@ -465,16 +467,16 @@ let variant_of_json (id_to_file : id_to_file_map) (js : json) : (match js with | `Assoc [ - ("span", span); + ("item_meta", item_meta); ("name", name); ("fields", fields); ("discriminant", discriminant); ] -> - let* span = span_of_json id_to_file span in + let* item_meta = item_meta_of_json id_to_file item_meta in let* name = string_of_json name in let* fields = list_of_json (field_of_json id_to_file) fields in let* discriminant = scalar_value_of_json discriminant in - Ok { span; variant_name = name; fields; discriminant } + Ok { item_meta; variant_name = name; fields; discriminant } | _ -> Error "") let type_decl_kind_of_json (id_to_file : id_to_file_map) (js : json) : @@ -514,6 +516,7 @@ let trait_clause_of_json (id_to_file : id_to_file_map) (js : json) : [ ("clause_id", clause_id); ("span", span); + ("origin", _); ("trait_id", trait_id); ("generics", generics); ] -> @@ -524,28 +527,6 @@ let trait_clause_of_json (id_to_file : id_to_file_map) (js : json) : Ok ({ clause_id; span; trait_id; clause_generics } : trait_clause) | _ -> Error "") -let generic_params_of_json (id_to_file : id_to_file_map) (js : json) : - (generic_params, string) result = - combine_error_msgs js __FUNCTION__ - (match js with - | `Assoc - [ - ("regions", regions); - ("types", types); - ("const_generics", const_generics); - ("trait_clauses", trait_clauses); - ] -> - let* regions = list_of_json region_var_of_json regions in - let* types = list_of_json type_var_of_json types in - let* const_generics = - list_of_json const_generic_var_of_json const_generics - in - let* trait_clauses = - list_of_json (trait_clause_of_json id_to_file) trait_clauses - in - Ok { regions; types; const_generics; trait_clauses } - | _ -> Error "") - let region_outlives_of_json (js : json) : (region_outlives, string) result = combine_error_msgs js __FUNCTION__ (match js with @@ -576,15 +557,28 @@ let trait_type_constraint_of_json (js : json) : Ok ({ trait_ref; type_name; ty } : trait_type_constraint) | _ -> Error "") -let predicates_of_json (js : json) : (predicates, string) result = +let generic_params_of_json (id_to_file : id_to_file_map) (js : json) : + (generic_params, string) result = combine_error_msgs js __FUNCTION__ (match js with | `Assoc [ + ("regions", regions); + ("types", types); + ("const_generics", const_generics); + ("trait_clauses", trait_clauses); ("regions_outlive", regions_outlive); ("types_outlive", types_outlive); ("trait_type_constraints", trait_type_constraints); ] -> + let* regions = list_of_json region_var_of_json regions in + let* types = list_of_json type_var_of_json types in + let* const_generics = + list_of_json const_generic_var_of_json const_generics + in + let* trait_clauses = + list_of_json (trait_clause_of_json id_to_file) trait_clauses + in let* regions_outlive = list_of_json region_outlives_of_json regions_outlive in @@ -592,7 +586,16 @@ let predicates_of_json (js : json) : (predicates, string) result = let* trait_type_constraints = list_of_json trait_type_constraint_of_json trait_type_constraints in - Ok { regions_outlive; types_outlive; trait_type_constraints } + Ok + { + regions; + types; + const_generics; + trait_clauses; + regions_outlive; + types_outlive; + trait_type_constraints; + } | _ -> Error "") let impl_elem_kind_of_json (js : json) : (impl_elem_kind, string) result = @@ -614,14 +617,12 @@ let impl_elem_of_json (id_to_file : id_to_file_map) (js : json) : [ ("disambiguator", disambiguator); ("generics", generics); - ("preds", preds); ("kind", kind); ] -> let* disambiguator = Disambiguator.id_of_json disambiguator in let* generics = generic_params_of_json id_to_file generics in - let* preds = predicates_of_json preds in let* kind = impl_elem_kind_of_json kind in - Ok { disambiguator; generics; preds; kind } + Ok { disambiguator; generics; kind } | _ -> Error "") let path_elem_of_json (id_to_file : id_to_file_map) (js : json) : @@ -653,7 +654,6 @@ let type_decl_of_json (id_to_file : id_to_file_map) (js : json) : ("is_local", is_local); ("name", name); ("generics", generics); - ("preds", preds); ("kind", kind); ] -> let* def_id = TypeDeclId.id_of_json def_id in @@ -661,9 +661,8 @@ let type_decl_of_json (id_to_file : id_to_file_map) (js : json) : let* is_local = bool_of_json is_local in let* name = name_of_json id_to_file name in let* generics = generic_params_of_json id_to_file generics in - let* preds = predicates_of_json preds in let* kind = type_decl_kind_of_json id_to_file kind in - Ok { def_id; item_meta; is_local; name; generics; preds; kind } + Ok { def_id; item_meta; is_local; name; generics; kind } | _ -> Error "") let var_of_json (js : json) : (var, string) result = @@ -1007,7 +1006,6 @@ let fun_sig_of_json (id_to_file : id_to_file_map) (js : json) : ("is_closure", is_closure); ("closure_info", closure_info); ("generics", generics); - ("preds", preds); ("parent_params_info", parent_params_info); ("inputs", inputs); ("output", output); @@ -1017,7 +1015,6 @@ let fun_sig_of_json (id_to_file : id_to_file_map) (js : json) : let* closure_info = option_of_json closure_info_of_json closure_info in let* generics = generic_params_of_json id_to_file generics in - let* preds = predicates_of_json preds in let* parent_params_info = option_of_json params_info_of_json parent_params_info in @@ -1029,7 +1026,6 @@ let fun_sig_of_json (id_to_file : id_to_file_map) (js : json) : is_closure; closure_info; generics; - preds; parent_params_info; inputs; output; @@ -1153,7 +1149,6 @@ let gglobal_decl_of_json (bodies : 'body gexpr_body option list) ("is_local", is_local); ("name", name); ("generics", generics); - ("preds", preds); ("ty", ty); ("kind", kind); ("body", body); @@ -1163,7 +1158,6 @@ let gglobal_decl_of_json (bodies : 'body gexpr_body option list) let* is_local = bool_of_json is_local in let* name = name_of_json id_to_file name in let* generics = generic_params_of_json id_to_file generics in - let* preds = predicates_of_json preds in let* ty = ty_of_json ty in let* kind = item_kind_of_json kind in let* body = maybe_opaque_body_of_json bodies body in @@ -1175,7 +1169,6 @@ let gglobal_decl_of_json (bodies : 'body gexpr_body option list) name; body; generics; - preds; ty; kind; } @@ -1194,7 +1187,6 @@ let trait_decl_of_json (id_to_file : id_to_file_map) (js : json) : ("item_meta", item_meta); ("name", name); ("generics", generics); - ("preds", preds); ("parent_clauses", parent_clauses); ("consts", consts); ("types", types); @@ -1206,7 +1198,6 @@ let trait_decl_of_json (id_to_file : id_to_file_map) (js : json) : let* name = name_of_json id_to_file name in let* item_meta = item_meta_of_json id_to_file item_meta in let* generics = generic_params_of_json id_to_file generics in - let* preds = predicates_of_json preds in let* parent_clauses = list_of_json (trait_clause_of_json id_to_file) parent_clauses in @@ -1242,7 +1233,6 @@ let trait_decl_of_json (id_to_file : id_to_file_map) (js : json) : is_local; name; generics; - preds; parent_clauses; consts; types; @@ -1263,7 +1253,6 @@ let trait_impl_of_json (id_to_file : id_to_file_map) (js : json) : ("item_meta", item_meta); ("impl_trait", impl_trait); ("generics", generics); - ("preds", preds); ("parent_trait_refs", parent_trait_refs); ("consts", consts); ("types", types); @@ -1276,7 +1265,6 @@ let trait_impl_of_json (id_to_file : id_to_file_map) (js : json) : let* name = name_of_json id_to_file name in let* impl_trait = trait_decl_ref_of_json impl_trait in let* generics = generic_params_of_json id_to_file generics in - let* preds = predicates_of_json preds in let* parent_trait_refs = list_of_json trait_ref_of_json parent_trait_refs in @@ -1305,7 +1293,6 @@ let trait_impl_of_json (id_to_file : id_to_file_map) (js : json) : name; impl_trait; generics; - preds; parent_trait_refs; consts; types; @@ -1358,6 +1345,31 @@ let trait_implementation_group_of_json (js : json) : | NonRecGroup id -> Ok id | RecGroup _ -> Error "got mutually dependent trait impls") +let any_decl_id_of_json (js : json) : (any_decl_id, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | `Assoc [ ("Fun", id) ] -> + let* id = FunDeclId.id_of_json id in + Ok (IdFun id) + | `Assoc [ ("Global", id) ] -> + let* id = GlobalDeclId.id_of_json id in + Ok (IdGlobal id) + | `Assoc [ ("Type", id) ] -> + let* id = TypeDeclId.id_of_json id in + Ok (IdType id) + | `Assoc [ ("TraitDecl", id) ] -> + let* id = TraitDeclId.id_of_json id in + Ok (IdTraitDecl id) + | `Assoc [ ("TraitImpl", id) ] -> + let* id = TraitImplId.id_of_json id in + Ok (IdTraitImpl id) + | _ -> Error "") + +let mixed_group_of_json (js : json) : + (any_decl_id g_declaration_group, string) result = + combine_error_msgs js __FUNCTION__ + (g_declaration_group_of_json any_decl_id_of_json js) + let declaration_group_of_json (js : json) : (declaration_group, string) result = combine_error_msgs js __FUNCTION__ (match js with @@ -1376,6 +1388,9 @@ let declaration_group_of_json (js : json) : (declaration_group, string) result = | `Assoc [ ("TraitImpl", decl) ] -> let* id = trait_implementation_group_of_json decl in Ok (TraitImplGroup id) + | `Assoc [ ("Mixed", decl) ] -> + let* id = mixed_group_of_json decl in + Ok (MixedGroup id) | _ -> Error "") let length_of_json_list (js : json) : (int, string) result = diff --git a/charon-ml/src/GAstUtils.ml b/charon-ml/src/GAstUtils.ml index ea21af9b9..db231c21d 100644 --- a/charon-ml/src/GAstUtils.ml +++ b/charon-ml/src/GAstUtils.ml @@ -41,29 +41,37 @@ let gexpr_body_get_input_vars (fbody : 'body gexpr_body) : var list = let fun_body_get_input_vars (fbody : 'body gexpr_body) : var list = gexpr_body_get_input_vars fbody +let g_declaration_group_to_list (g : 'a g_declaration_group) : 'a list = + match g with RecGroup ids -> ids | NonRecGroup id -> [ id ] + (** Split a module's declarations between types, functions and globals *) let split_declarations (decls : declaration_group list) : type_declaration_group list * fun_declaration_group list * GlobalDeclId.id list * trait_declaration_group list - * TraitImplId.id list = + * TraitImplId.id list + * mixed_declaration_group list = let rec split decls = match decls with - | [] -> ([], [], [], [], []) + | [] -> ([], [], [], [], [], []) | d :: decls' -> ( - let types, funs, globals, trait_decls, trait_impls = split decls' in + let types, funs, globals, trait_decls, trait_impls, mixeds = + split decls' + in match d with | TypeGroup decl -> - (decl :: types, funs, globals, trait_decls, trait_impls) + (decl :: types, funs, globals, trait_decls, trait_impls, mixeds) | FunGroup decl -> - (types, decl :: funs, globals, trait_decls, trait_impls) + (types, decl :: funs, globals, trait_decls, trait_impls, mixeds) | GlobalGroup decl -> - (types, funs, decl :: globals, trait_decls, trait_impls) + (types, funs, decl :: globals, trait_decls, trait_impls, mixeds) | TraitDeclGroup decl -> - (types, funs, globals, decl :: trait_decls, trait_impls) + (types, funs, globals, decl :: trait_decls, trait_impls, mixeds) | TraitImplGroup decl -> - (types, funs, globals, trait_decls, decl :: trait_impls)) + (types, funs, globals, trait_decls, decl :: trait_impls, mixeds) + | MixedGroup decls -> + (types, funs, globals, trait_decls, trait_impls, decls :: mixeds)) in split decls @@ -88,9 +96,11 @@ let split_declarations_to_group_maps (decls : declaration_group list) : M.key g_declaration_group M.t = List.fold_left add_group M.empty groups end in - let types, funs, globals, trait_decls, trait_impls = + let types, funs, globals, trait_decls, trait_impls, mixed_groups = split_declarations decls in + if List.length mixed_groups <> 0 then + raise (Failure "Mixed declaration groups cannot be indexed by declaration"); let module TG = G (TypeDeclId.Map) in let types = TG.create_map types in let module FG = G (FunDeclId.Map) in diff --git a/charon-ml/src/LlbcAstUtils.ml b/charon-ml/src/LlbcAstUtils.ml index 967605fc4..c93d89c17 100644 --- a/charon-ml/src/LlbcAstUtils.ml +++ b/charon-ml/src/LlbcAstUtils.ml @@ -82,5 +82,9 @@ let compute_fun_decl_groups_map (c : crate) : FunDeclId.Set.t FunDeclId.Map.t = Some (List.map (fun id -> (id, idset)) ids) | TypeGroup _ | GlobalGroup _ | TraitDeclGroup _ | TraitImplGroup _ -> - None) + None + | MixedGroup _ -> + raise + (Failure + "Mixed declaration groups cannot be indexed by declaration")) c.declarations)) diff --git a/charon-ml/src/LlbcOfJson.ml b/charon-ml/src/LlbcOfJson.ml index c46a83335..872f1f802 100644 --- a/charon-ml/src/LlbcOfJson.ml +++ b/charon-ml/src/LlbcOfJson.ml @@ -60,10 +60,21 @@ and raw_statement_of_json (id_to_file : id_to_file_map) (js : json) : let* i = int_of_json i in Ok (Continue i) | `String "Nop" -> Ok Nop - | `Assoc [ ("Sequence", `List [ st1; st2 ]) ] -> - let* st1 = statement_of_json id_to_file st1 in - let* st2 = statement_of_json id_to_file st2 in - Ok (Sequence (st1, st2)) + (* We get a list from the rust side, which we fold into our recursive `Sequence` representation. *) + | `Assoc [ ("Sequence", `List seq) ] -> ( + let seq = List.map (statement_of_json id_to_file) seq in + match List.rev seq with + | [] -> Ok Nop + | last :: rest -> + let* seq = + List.fold_left + (fun acc st -> + let* st = st in + let* acc = acc in + Ok { span = st.span; content = Sequence (st, acc) }) + last rest + in + Ok seq.content) | `Assoc [ ("Switch", tgt) ] -> let* switch = switch_of_json id_to_file tgt in Ok (Switch switch) @@ -149,7 +160,6 @@ let global_decl_of_json (bodies : expr_body option list) is_local; name; generics; - preds; ty; kind; } = @@ -164,7 +174,6 @@ let global_decl_of_json (bodies : expr_body option list) is_closure = false; closure_info = None; generics; - preds; parent_params_info = None; inputs = []; output = ty; @@ -178,7 +187,6 @@ let global_decl_of_json (bodies : expr_body option list) is_local; name; generics; - preds; ty; kind; } diff --git a/charon-ml/src/Meta.ml b/charon-ml/src/Meta.ml index 5e325c62b..d1ed0c01d 100644 --- a/charon-ml/src/Meta.ml +++ b/charon-ml/src/Meta.ml @@ -55,5 +55,6 @@ type item_meta = { attributes : string list; (** Attributes (`#[...]`). **) inline : inline_attr option; public : bool; + rename : string option; } [@@deriving show, ord] diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml index ac2d8d57a..1f223d634 100644 --- a/charon-ml/src/NameMatcher.ml +++ b/charon-ml/src/NameMatcher.ml @@ -210,11 +210,8 @@ let ctx_to_fmt_env (ctx : ctx) : PrintLlbcAst.fmt_env = global_decls = ctx.global_decls; trait_decls = ctx.trait_decls; trait_impls = ctx.trait_impls; - types = []; regions = []; - const_generics = []; - trait_clauses = []; - preds = TypesUtils.empty_predicates; + generics = TypesUtils.empty_generic_params; locals = []; } diff --git a/charon-ml/src/PrintGAst.ml b/charon-ml/src/PrintGAst.ml index ef8e537f5..804febb45 100644 --- a/charon-ml/src/PrintGAst.ml +++ b/charon-ml/src/PrintGAst.ml @@ -7,6 +7,14 @@ open PrintUtils open PrintTypes open PrintExpressions +let any_decl_id_to_string (id : any_decl_id) : string = + match id with + | IdFun id -> FunDeclId.to_string id + | IdGlobal id -> GlobalDeclId.to_string id + | IdType id -> TypeDeclId.to_string id + | IdTraitDecl id -> TraitDeclId.to_string id + | IdTraitImpl id -> TraitImplId.to_string id + let fn_operand_to_string (env : ('a, 'b) fmt_env) (op : fn_operand) : string = match op with | FnOpRegular func -> fn_ptr_to_string env func @@ -36,10 +44,9 @@ let fun_sig_with_name_to_string (env : ('a, 'b) fmt_env) (indent : string) let unsafe = if sg.is_unsafe then "unsafe " else "" in (* Generics and predicates *) - let params, trait_clauses = generic_params_to_strings env sg.generics in - let clauses = + let params, clauses = predicates_and_trait_clauses_to_string env indent indent_incr - sg.parent_params_info trait_clauses sg.preds + sg.parent_params_info sg.generics in let params = if params = [] then "" else "<" ^ String.concat ", " params ^ ">" @@ -80,10 +87,7 @@ let gfun_decl_to_string (env : ('a, 'b) fmt_env) (indent : string) (body_to_string : ('a, 'b) fmt_env -> string -> string -> 'body -> string) (def : 'body gfun_decl) : string = (* Locally update the environment *) - let env = - fmt_env_update_generics_and_preds env def.signature.generics - def.signature.preds - in + let env = fmt_env_update_generics_and_preds env def.signature.generics in let sg = def.signature in @@ -131,7 +135,7 @@ let gfun_decl_to_string (env : ('a, 'b) fmt_env) (indent : string) let trait_decl_to_string (env : ('a, 'b) fmt_env) (indent : string) (indent_incr : string) (def : trait_decl) : string = (* Locally update the environment *) - let env = fmt_env_update_generics_and_preds env def.generics def.preds in + let env = fmt_env_update_generics_and_preds env def.generics in let ty_to_string = ty_to_string env in @@ -139,10 +143,9 @@ let trait_decl_to_string (env : ('a, 'b) fmt_env) (indent : string) let name = name_to_string env def.name in (* Generics and predicates *) - let params, trait_clauses = generic_params_to_strings env def.generics in - let clauses = + let params, clauses = predicates_and_trait_clauses_to_string env indent indent_incr None - trait_clauses def.preds + def.generics in let params = if params = [] then "" else "<" ^ String.concat ", " params ^ ">" @@ -220,7 +223,7 @@ let trait_decl_to_string (env : ('a, 'b) fmt_env) (indent : string) let trait_impl_to_string (env : ('a, 'b) fmt_env) (indent : string) (indent_incr : string) (def : trait_impl) : string = (* Locally update the environment *) - let env = fmt_env_update_generics_and_preds env def.generics def.preds in + let env = fmt_env_update_generics_and_preds env def.generics in let ty_to_string = ty_to_string env in @@ -228,10 +231,9 @@ let trait_impl_to_string (env : ('a, 'b) fmt_env) (indent : string) let name = name_to_string env def.name in (* Generics and predicates *) - let params, trait_clauses = generic_params_to_strings env def.generics in - let clauses = + let params, clauses = predicates_and_trait_clauses_to_string env indent indent_incr None - trait_clauses def.preds + def.generics in let params = if params = [] then "" else "<" ^ String.concat ", " params ^ ">" diff --git a/charon-ml/src/PrintLlbcAst.ml b/charon-ml/src/PrintLlbcAst.ml index 1f2b6f2b4..f4fb44820 100644 --- a/charon-ml/src/PrintLlbcAst.ml +++ b/charon-ml/src/PrintLlbcAst.ml @@ -120,11 +120,9 @@ module Ast = struct let global_decl_to_string (env : fmt_env) (indent : string) (_indent_incr : string) (def : global_decl) : string = (* Locally update the generics and the predicates *) - let env = fmt_env_update_generics_and_preds env def.generics def.preds in - let params, trait_clauses = generic_params_to_strings env def.generics in - let clauses = - predicates_and_trait_clauses_to_string env "" " " None trait_clauses - def.preds + let env = fmt_env_update_generics_and_preds env def.generics in + let params, clauses = + predicates_and_trait_clauses_to_string env "" " " None def.generics in let params = if params <> [] then "<" ^ String.concat ", " params ^ ">" else "" @@ -152,10 +150,7 @@ module Crate = struct trait_decls = m.trait_decls; trait_impls = m.trait_impls; regions = []; - types = []; - const_generics = []; - trait_clauses = []; - preds = empty_predicates; + generics = empty_generic_params; locals = []; } diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 4ec6f4857..341577f3e 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -68,7 +68,9 @@ let region_var_id_to_string (env : ('a, 'b) fmt_env) (db_id : region_db_id) let type_var_id_to_string (env : ('a, 'b) fmt_env) (id : type_var_id) : string = (* Note that the types are not necessarily ordered following their indices *) - match List.find_opt (fun (x : type_var) -> x.index = id) env.types with + match + List.find_opt (fun (x : type_var) -> x.index = id) env.generics.types + with | None -> type_var_id_to_pretty_string id | Some x -> type_var_to_string x @@ -78,7 +80,7 @@ let const_generic_var_id_to_string (env : ('a, 'b) fmt_env) match List.find_opt (fun (x : const_generic_var) -> x.index = id) - env.const_generics + env.generics.const_generics with | None -> const_generic_var_id_to_pretty_string id | Some x -> const_generic_var_to_string x @@ -261,7 +263,7 @@ and impl_elem_kind_to_string (env : ('a, 'b) fmt_env) (k : impl_elem_kind) : and impl_elem_to_string (env : ('a, 'b) fmt_env) (e : impl_elem) : string = (* Locally replace the generics and the predicates *) - let env = fmt_env_update_generics_and_preds env e.generics e.preds in + let env = fmt_env_update_generics_and_preds env e.generics in let d = if e.disambiguator = Disambiguator.zero then "" else "#" ^ Disambiguator.to_string e.disambiguator @@ -291,7 +293,7 @@ let trait_clause_to_string (env : ('a, 'b) fmt_env) (clause : trait_clause) : let generic_params_to_strings (env : ('a, 'b) fmt_env) (generics : generic_params) : string list * string list = - let { regions; types; const_generics; trait_clauses } : generic_params = + let { regions; types; const_generics; trait_clauses; _ } : generic_params = generics in let regions = List.map region_var_to_string regions in @@ -343,52 +345,58 @@ let clauses_to_string (indent : string) (indent_incr : string) (** Helper to format "where" clauses *) let predicates_and_trait_clauses_to_string (env : ('a, 'b) fmt_env) (indent : string) (indent_incr : string) (params_info : params_info option) - (trait_clauses : string list) (preds : predicates) : string = - let { regions_outlive; types_outlive; trait_type_constraints } = preds in + (generics : generic_params) : string list * string = + let params, trait_clauses = generic_params_to_strings env generics in let region_to_string = region_to_string env in let regions_outlive = List.map (fun (x, y) -> region_to_string x ^ " : " ^ region_to_string y) - regions_outlive + generics.regions_outlive in let types_outlive = List.map (fun (x, y) -> ty_to_string env x ^ " : " ^ region_to_string y) - types_outlive + generics.types_outlive in let trait_type_constraints = - List.map (trait_type_constraint_to_string env) trait_type_constraints + List.map + (trait_type_constraint_to_string env) + generics.trait_type_constraints in (* Split between the inherited clauses and the local clauses *) - match params_info with - | None -> - let clauses = - List.concat [ regions_outlive; types_outlive; trait_type_constraints ] - in - clauses_to_string indent indent_incr 0 clauses - | Some pi -> - let split_at = Collections.List.split_at in - let trait_clauses = split_at trait_clauses pi.num_trait_clauses in - let regions_outlive = split_at regions_outlive pi.num_regions_outlive in - let types_outlive = split_at types_outlive pi.num_types_outlive in - let ttc = split_at trait_type_constraints pi.num_trait_type_constraints in - let inherited, local = - List.split [ trait_clauses; regions_outlive; types_outlive; ttc ] - in - let inherited = List.concat inherited in - let local = List.concat local in - let num_inherited = List.length inherited in - let clauses = List.append inherited local in - clauses_to_string indent indent_incr num_inherited clauses + let clauses = + match params_info with + | None -> + let clauses = + List.concat [ regions_outlive; types_outlive; trait_type_constraints ] + in + clauses_to_string indent indent_incr 0 clauses + | Some pi -> + let split_at = Collections.List.split_at in + let trait_clauses = split_at trait_clauses pi.num_trait_clauses in + let regions_outlive = split_at regions_outlive pi.num_regions_outlive in + let types_outlive = split_at types_outlive pi.num_types_outlive in + let ttc = + split_at trait_type_constraints pi.num_trait_type_constraints + in + let inherited, local = + List.split [ trait_clauses; regions_outlive; types_outlive; ttc ] + in + let inherited = List.concat inherited in + let local = List.concat local in + let num_inherited = List.length inherited in + let clauses = List.append inherited local in + clauses_to_string indent indent_incr num_inherited clauses + in + (params, clauses) let type_decl_to_string (env : ('a, 'b) fmt_env) (def : type_decl) : string = (* Locally update the generics and the predicates *) - let env = fmt_env_update_generics_and_preds env def.generics def.preds in - let params, trait_clauses = generic_params_to_strings env def.generics in - let clauses = - predicates_and_trait_clauses_to_string env "" " " None trait_clauses - def.preds + let env = fmt_env_update_generics_and_preds env def.generics in + let params, clauses = + predicates_and_trait_clauses_to_string env "" " " None def.generics in + let name = name_to_string env def.name in let params = if params <> [] then "<" ^ String.concat ", " params ^ ">" else "" diff --git a/charon-ml/src/PrintUllbcAst.ml b/charon-ml/src/PrintUllbcAst.ml index 17783d61f..e92260e29 100644 --- a/charon-ml/src/PrintUllbcAst.ml +++ b/charon-ml/src/PrintUllbcAst.ml @@ -98,11 +98,9 @@ module Ast = struct let global_decl_to_string (env : fmt_env) (indent : string) (indent_incr : string) (def : global_decl) : string = (* Locally update the generics and the predicates *) - let env = fmt_env_update_generics_and_preds env def.generics def.preds in - let params, trait_clauses = generic_params_to_strings env def.generics in - let clauses = - predicates_and_trait_clauses_to_string env "" " " None trait_clauses - def.preds + let env = fmt_env_update_generics_and_preds env def.generics in + let params, clauses = + predicates_and_trait_clauses_to_string env "" " " None def.generics in let params = if params <> [] then "<" ^ String.concat ", " params ^ ">" else "" @@ -136,10 +134,7 @@ module Crate = struct trait_decls = m.trait_decls; trait_impls = m.trait_impls; regions = []; - types = []; - const_generics = []; - trait_clauses = []; - preds = empty_predicates; + generics = empty_generic_params; locals = []; } in diff --git a/charon-ml/src/PrintUtils.ml b/charon-ml/src/PrintUtils.ml index 558576b6f..931f5e84a 100644 --- a/charon-ml/src/PrintUtils.ml +++ b/charon-ml/src/PrintUtils.ml @@ -26,27 +26,16 @@ type ('fun_body, 'global_body) fmt_env = { indices, i.e., the region var of index 0 doesn't have to be at index 0, etc. We lookup the variables by checking their id, not their position. *) - types : type_var list; - const_generics : const_generic_var list; - trait_clauses : trait_clause list; - preds : predicates; + generics : generic_params; + (* We ignore `generics.regions` as they are tracked in `regions` already *) locals : (VarId.id * string option) list; (** The local variables don't need to be ordered (same as the generics) *) } let fmt_env_update_generics_and_preds (env : ('a, 'b) fmt_env) - (generics : generic_params) (preds : predicates) : ('a, 'b) fmt_env = - let { regions; types; const_generics; trait_clauses } : generic_params = - generics - in - { - env with - regions = regions :: env.regions; - types; - const_generics; - trait_clauses; - preds; - } + (generics : generic_params) : ('a, 'b) fmt_env = + let { regions; _ } : generic_params = generics in + { env with regions = regions :: env.regions; generics } let fmt_env_push_regions (env : ('a, 'b) fmt_env) (regions : region_var list) : ('a, 'b) fmt_env = diff --git a/charon-ml/src/Substitute.ml b/charon-ml/src/Substitute.ml index 8184b32a9..66e6a3785 100644 --- a/charon-ml/src/Substitute.ml +++ b/charon-ml/src/Substitute.ml @@ -49,17 +49,7 @@ let st_substitute_visitor (subst : subst) = TArrow (regions, inputs, output) method! visit_TVar (subst : subst) id = subst.ty_subst id - - method! visit_type_var_id _ _ = - (* We should never get here because we reimplemented [visit_TypeVar] *) - raise (Failure "Unexpected") - method! visit_CgVar _ id = subst.cg_subst id - - method! visit_const_generic_var_id _ _ = - (* We should never get here because we reimplemented [visit_Var] *) - raise (Failure "Unexpected") - method! visit_Clause (subst : subst) id = subst.tr_subst id method! visit_Self (subst : subst) = subst.tr_self end @@ -88,9 +78,10 @@ let generic_args_substitute (subst : subst) (g : generic_args) : generic_args = let visitor = st_substitute_visitor subst in visitor#visit_generic_args subst g -let predicates_substitute (subst : subst) (p : predicates) : predicates = +let generic_params_substitute (subst : subst) (p : generic_params) : + generic_params = let visitor = st_substitute_visitor subst in - visitor#visit_predicates subst p + visitor#visit_generic_params subst p let erase_regions_subst : subst = { diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index c8bccb073..b2a2ab687 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -374,8 +374,8 @@ and region = polymorphic = false; }] -(** Ancestor for iter visitor for {!type: Types.predicates} *) -class ['self] iter_predicates_base = +(** Ancestor for iter visitor for {!type: Types.generic_params} *) +class ['self] iter_generic_params_base = object (self : 'self) inherit [_] iter_ty method visit_span : 'env -> span -> unit = fun _ _ -> () @@ -394,8 +394,8 @@ class ['self] iter_predicates_base = self#visit_literal_type env ty end -(** Ancestor for map visitor for {!type: Types.ty} *) -class virtual ['self] map_predicates_base = +(** Ancestor for map visitor for {!type: Types.generic_params} *) +class virtual ['self] map_generic_params_base = object (self : 'self) inherit [_] map_ty method visit_span : 'env -> span -> span = fun _ x -> x @@ -449,6 +449,9 @@ and generic_params = { because of the way the clauses are resolved in hax (see the comments in Charon). *) + regions_outlive : region_outlives list; + types_outlive : type_outlives list; + trait_type_constraints : trait_type_constraint list; } (** ('long, 'short) means that 'long outlives 'short *) @@ -462,29 +465,23 @@ and trait_type_constraint = { type_name : trait_item_name; ty : ty; } - -and predicates = { - regions_outlive : region_outlives list; - types_outlive : type_outlives list; - trait_type_constraints : trait_type_constraint list; -} [@@deriving show, ord, visitors { - name = "iter_predicates"; + name = "iter_generic_params"; variety = "iter"; - ancestors = [ "iter_predicates_base" ]; + ancestors = [ "iter_generic_params_base" ]; nude = true (* Don't inherit {!VisitorsRuntime.iter} *); concrete = true; polymorphic = false; }, visitors { - name = "map_predicates"; + name = "map_generic_params"; variety = "map"; - ancestors = [ "map_predicates_base" ]; + ancestors = [ "map_generic_params_base" ]; nude = true (* Don't inherit {!VisitorsRuntime.map} *); concrete = false; polymorphic = false; @@ -499,7 +496,6 @@ type impl_elem_kind = ImplElemTy of ty | ImplElemTrait of trait_decl_ref type impl_elem = { disambiguator : Disambiguator.id; generics : generic_params; - preds : predicates; kind : impl_elem_kind; } [@@deriving show, ord] @@ -530,11 +526,15 @@ type region_var_group = (RegionVarId.id, RegionGroupId.id) g_region_group type region_var_groups = region_var_group list [@@deriving show] -type field = { span : span; field_name : string option; field_ty : ty } +type field = { + item_meta : item_meta; + field_name : string option; + field_ty : ty; +} [@@deriving show] type variant = { - span : span; + item_meta : item_meta; variant_name : string; fields : field list; (** The fields can be indexed with {!FieldId.id}. @@ -568,7 +568,6 @@ type type_decl = { is_local : bool; name : name; generics : generic_params; - preds : predicates; kind : type_decl_kind; } [@@deriving show] diff --git a/charon-ml/src/TypesUtils.ml b/charon-ml/src/TypesUtils.ml index 92405d776..40e51d35b 100644 --- a/charon-ml/src/TypesUtils.ml +++ b/charon-ml/src/TypesUtils.ml @@ -97,10 +97,15 @@ let mk_generic_args_from_types (types : ty list) : generic_args = { regions = []; types; const_generics = []; trait_refs = [] } let empty_generic_params : generic_params = - { regions = []; types = []; const_generics = []; trait_clauses = [] } - -let empty_predicates : predicates = - { regions_outlive = []; types_outlive = []; trait_type_constraints = [] } + { + regions = []; + types = []; + const_generics = []; + trait_clauses = []; + regions_outlive = []; + types_outlive = []; + trait_type_constraints = []; + } let merge_generic_args (g1 : generic_args) (g2 : generic_args) : generic_args = let { regions = r1; types = tys1; const_generics = cgs1; trait_refs = tr1 } = diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 834cf3675..1dc1167d1 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -160,7 +160,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.10" +version = "0.1.15" dependencies = [ "anyhow", "assert_cmd", @@ -169,6 +169,7 @@ dependencies = [ "clap", "colored", "derivative", + "derive-visitor", "env_logger", "hashlink", "hax-frontend-exporter", @@ -270,6 +271,12 @@ version = "0.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d6417fe6fc03a8b533fd2177742eeb39a90c7233eedec7bac96d4d6b69a09449" +[[package]] +name = "convert_case" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6245d59a3e82a7fc217c5828a6692dbc6dfb63a0c8c90495621f7b9d79704a0e" + [[package]] name = "crossbeam-channel" version = "0.5.12" @@ -315,6 +322,28 @@ dependencies = [ "syn 1.0.109", ] +[[package]] +name = "derive-visitor" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d47165df83b9707cbada3216607a5d66125b6a66906de0bc1216c0669767ca9e" +dependencies = [ + "derive-visitor-macros", +] + +[[package]] +name = "derive-visitor-macros" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "427b39a85fecafea16b1a5f3f50437151022e35eb4fe038107f08adbf7f8def6" +dependencies = [ + "convert_case", + "itertools 0.10.5", + "proc-macro2", + "quote", + "syn 1.0.109", +] + [[package]] name = "difflib" version = "0.4.0" @@ -472,7 +501,7 @@ dependencies = [ [[package]] name = "hax-adt-into" version = "0.1.0-pre.1" -source = "git+https://github.com/Nadrieril/hax?branch=update-rustc#53247ba53ea8d0912305dba39f4bc2de2dd180d5" +source = "git+https://github.com/hacspec/hax?branch=main#f4fd720fb039ffbab44f6d08784f019869d31dac" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -483,7 +512,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.1.0-pre.1" -source = "git+https://github.com/Nadrieril/hax?branch=update-rustc#53247ba53ea8d0912305dba39f4bc2de2dd180d5" +source = "git+https://github.com/hacspec/hax?branch=main#f4fd720fb039ffbab44f6d08784f019869d31dac" dependencies = [ "extension-traits", "hax-adt-into", @@ -500,7 +529,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.1.0-pre.1" -source = "git+https://github.com/Nadrieril/hax?branch=update-rustc#53247ba53ea8d0912305dba39f4bc2de2dd180d5" +source = "git+https://github.com/hacspec/hax?branch=main#f4fd720fb039ffbab44f6d08784f019869d31dac" dependencies = [ "schemars", "serde", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index dbd353bc7..7d49e7e86 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.10" +version = "0.1.15" authors = ["Son Ho "] edition = "2021" @@ -28,6 +28,7 @@ bumpalo = "3.11.1" # We constrain the version of [bumpalo] because of a vulnerab clap = { version = "3.0", features = ["derive", "env"] } colored = "2.0.4" derivative = "2.2.0" +derive-visitor = { version = "0.4.0", features = ["std-types-drive"] } env_logger = "0.8.4" hashlink = "0.7.0" heck = "0.3.3" @@ -54,7 +55,7 @@ tracing = { version = "0.1", features = [ "max_level_trace", "release_max_level_ walkdir = "2.3.2" which = "6.0.1" -hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "update-rustc" } +hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main" } # hax-frontend-exporter = { path = "../../hax/frontend/exporter" } macros = { path = "./macros" } diff --git a/charon/macros/src/lib.rs b/charon/macros/src/lib.rs index f9aa3fe5d..8e77a080c 100644 --- a/charon/macros/src/lib.rs +++ b/charon/macros/src/lib.rs @@ -9,7 +9,6 @@ use proc_macro::TokenStream; use quote::quote; mod enum_helpers; -mod make_generic_in_borrows; use enum_helpers::EnumMethodKind; @@ -68,8 +67,3 @@ pub fn derive_enum_as_getters(item: TokenStream) -> TokenStream { pub fn derive_enum_to_getters(item: TokenStream) -> TokenStream { enum_helpers::derive_enum_variant_method(item.into(), EnumMethodKind::EnumToGetters).into() } - -#[proc_macro] -pub fn make_generic_in_borrows(tokens: TokenStream) -> TokenStream { - make_generic_in_borrows::make_generic_in_borrows(tokens) -} diff --git a/charon/macros/src/make_generic_in_borrows.rs b/charon/macros/src/make_generic_in_borrows.rs deleted file mode 100644 index 77f26c94a..000000000 --- a/charon/macros/src/make_generic_in_borrows.rs +++ /dev/null @@ -1,344 +0,0 @@ -use proc_macro::{Span, TokenStream}; -use quote::ToTokens; -use std::vec::Vec; -use syn::{ - parse_macro_input, Block, Expr, FnArg, Ident, Item, ItemTrait, Pat, ReturnType, Stmt, - TraitItem, Type, TypeParamBound, -}; - -fn generic_type_to_mut(ty: &mut Type) { - match ty { - Type::Reference(r) => match &mut r.mutability { - Option::None => { - r.mutability = Option::Some(syn::token::Mut([Span::call_site().into()])) - } - Option::Some(_) => (), - }, - _ => (), - } -} - -fn generic_stmt_to_mut(s: &mut Stmt) { - match s { - Stmt::Local(s) => s - .init - .iter_mut() - .for_each(|e| generic_expr_to_mut(&mut e.1)), - Stmt::Item(item) => generic_item_to_mut(item), - Stmt::Expr(e) => generic_expr_to_mut(e), - Stmt::Semi(e, _) => generic_expr_to_mut(e), - } -} - -fn generic_stmts_to_mut(stmts: &mut Vec) { - for stmt in stmts { - generic_stmt_to_mut(stmt) - } -} - -fn generic_item_to_mut(item: &mut Item) { - use Item::*; - match item { - Const(_) => unimplemented!("Item::Const"), - Enum(_) => unimplemented!("Item::Enum"), - ExternCrate(_) => unimplemented!("Item::ExternCrate"), - Fn(_) => unimplemented!("Item::Fn"), - ForeignMod(_) => unimplemented!("Item::ForeignMod"), - Impl(_) => unimplemented!("Item::Impl"), - Macro(_) => unimplemented!("Item::Macro"), - Macro2(_) => unimplemented!("Item::Macro2"), - Mod(_) => unimplemented!("Item::Mod"), - Static(_) => unimplemented!("Item::Static"), - Struct(_) => unimplemented!("Item::Struct"), - Trait(_) => unimplemented!("Item::Trait"), - TraitAlias(_) => unimplemented!("Item::TraitAlias"), - Type(_) => unimplemented!("Item::Type"), - Union(_) => unimplemented!("Item::Union"), - Use(_) => (), // Nothing to do - Verbatim(_) => unimplemented!("Item::Verbatim"), - #[cfg_attr(test, deny(non_exhaustive_omitted_patterns))] - _ => { - unimplemented!(); - } - } -} - -fn generic_block_to_mut(e: &mut Block) { - generic_stmts_to_mut(&mut (e.stmts)); -} - -fn generic_expr_to_mut(e: &mut Expr) { - // There are really a lot of cases: we try to filter the ones in which - // we are not interested. - match e { - Expr::Assign(e) => { - generic_expr_to_mut(&mut (*e.left)); - generic_expr_to_mut(&mut (*e.right)); - } - Expr::AssignOp(e) => { - generic_expr_to_mut(&mut (*e.left)); - generic_expr_to_mut(&mut (*e.right)); - } - Expr::Binary(e) => { - generic_expr_to_mut(&mut (*e.left)); - generic_expr_to_mut(&mut (*e.right)); - } - Expr::Block(e) => { - generic_block_to_mut(&mut (e.block)); - } - Expr::Box(e) => { - generic_expr_to_mut(&mut (*e.expr)); - } - Expr::Call(e) => { - generic_expr_to_mut(&mut (*e.func)); - for arg in e.args.iter_mut() { - generic_expr_to_mut(arg); - } - } - Expr::Closure(e) => { - // Keeping things simple - e.inputs.iter_mut().for_each(|i| generic_pat_to_mut(i)); - generic_expr_to_mut(&mut (*e.body)); - } - Expr::Field(e) => { - generic_expr_to_mut(&mut (*e.base)); - } - Expr::ForLoop(e) => { - // We ignore the pattern for now - generic_expr_to_mut(&mut (*e.expr)); - generic_block_to_mut(&mut (e.body)); - } - Expr::Group(e) => { - generic_expr_to_mut(&mut (*e.expr)); - } - Expr::If(e) => { - generic_expr_to_mut(&mut (*e.cond)); - generic_block_to_mut(&mut (e.then_branch)); - e.else_branch - .iter_mut() - .for_each(|(_, b)| generic_expr_to_mut(b)); - } - Expr::Index(e) => { - generic_expr_to_mut(&mut (*e.expr)); - generic_expr_to_mut(&mut (*e.index)); - } - Expr::Let(e) => { - // Ignoring the pattern - generic_expr_to_mut(&mut (*e.expr)); - } - Expr::Loop(e) => { - generic_block_to_mut(&mut (e.body)); - } - Expr::Macro(_) => { - // Doing nothing - } - Expr::Match(e) => { - generic_expr_to_mut(&mut (*e.expr)); - e.arms.iter_mut().for_each(|a| { - a.guard.iter_mut().for_each(|(_, g)| generic_expr_to_mut(g)); - generic_expr_to_mut(&mut a.body) - }); - } - Expr::MethodCall(e) => { - generic_expr_to_mut(&mut (*e.receiver)); - e.args.iter_mut().for_each(|a| generic_expr_to_mut(a)); - - // IMPORTANT: check the name of the method: if it is `iter` change - // to `iter_mut` - let id = e.method.to_string(); - if id == "iter" { - e.method = Ident::new("iter_mut", Span::call_site().into()); - } - } - Expr::Paren(e) => { - generic_expr_to_mut(&mut (*e.expr)); - } - Expr::Path(_) => { - // Doing nothing - } - Expr::Reference(e) => { - // IMPORTANT: change the mutability - // Remark: closures are handled elsewhere - e.mutability = Option::Some(syn::token::Mut([Span::call_site().into()])); - generic_expr_to_mut(&mut (*e.expr)); - } - Expr::Return(e) => { - e.expr.iter_mut().for_each(|e| generic_expr_to_mut(e)); - } - Expr::Type(e) => { - generic_expr_to_mut(&mut (*e.expr)); - generic_type_to_mut(&mut (*e.ty)); - } - Expr::While(e) => { - generic_expr_to_mut(&mut (*e.cond)); - generic_block_to_mut(&mut (e.body)); - } - _ => (), - } -} - -/// We use this method to update the names of the supertraits -/// when defining an implementation generic over the borrow type. -/// -/// For instance, if we write: -/// ```ignore -/// make_generic_in_borrows! { -/// trait AstVisitor : ExprVisitor { ... } -/// } -/// ``` -/// -/// We want to generate two definitions: -/// ```ignore -/// make_generic_in_borrows! { -/// trait SharedAstVisitor : SharedExprVisitor { ... } -/// } -/// ``` -/// -/// and: -/// ```ignore -/// make_generic_in_borrows! { -/// trait MutAstVisitor : MutExprVisitor { ... } -/// } -/// ``` -fn generic_supertraits_to_mut_shared(tr: &mut ItemTrait, to_mut: bool) { - for p in tr.supertraits.iter_mut() { - match p { - TypeParamBound::Trait(t) => { - // Update the path: update the last segment - let mut it = t.path.segments.iter_mut(); - let mut last_s = it.next().unwrap(); - while let Some(s) = it.next() { - last_s = s; - } - last_s.ident = generic_mk_ident(&last_s.ident, to_mut); - } - TypeParamBound::Lifetime(_) => (), - } - } -} - -fn generic_mk_ident(id: &syn::Ident, to_mut: bool) -> syn::Ident { - // TODO: not sure about the spans - // Not very clean, but does the job - let id = id.to_string(); - let name = if to_mut { - format!("Mut{}", id) - } else { - format!("Shared{}", id) - }; - syn::Ident::new(&name, Span::call_site().into()) -} - -fn generic_pat_to_mut(p: &mut Pat) { - match p { - Pat::Type(p) => generic_type_to_mut(&mut p.ty), - _ => (), - } -} - -fn generic_mk_item(id: &Ident, to_mut: bool, item: &mut TraitItem) { - match item { - TraitItem::Const(_) | TraitItem::Macro(_) => { - unimplemented!("Trait item") - } - TraitItem::Type(ty) => { - // Update the references to self (we need to change the name). - // For now, we only update the bounds - for bound in &mut ty.bounds { - if let TypeParamBound::Trait(tr) = bound { - if tr.path.segments.len() == 1 { - if let Some(last) = tr.path.segments.last_mut() { - if &last.ident == id { - last.ident = generic_mk_ident(&mut last.ident, to_mut) - } - } - } - } - } - } - TraitItem::Verbatim(_) => (), - TraitItem::Method(s) => { - // Update the borrows - if to_mut { - // Update the signature - for input in &mut s.sig.inputs { - match input { - FnArg::Receiver(_) => { - /* We don't touch the self parameter for now */ - () - } - FnArg::Typed(arg) => { - // Change the reference types - generic_type_to_mut(&mut (*arg.ty)); - } - } - } - - match &mut s.sig.output { - ReturnType::Default => (), - ReturnType::Type(_, ty) => { - generic_type_to_mut(ty); - } - } - - // Update the body - // - we replace all the references - // - we replace the occurrences of `iter` - match &mut s.default { - Option::None => (), - Option::Some(body) => { - generic_stmts_to_mut(&mut body.stmts); - } - } - } - } - #[cfg_attr(test, deny(non_exhaustive_omitted_patterns))] - _ => { - /* See the fox of [TraitItem] */ - unimplemented!() - } - } -} - -/// We use this macro to write implementation which are generic in borrow -/// kinds (i.e., from one implementation, we derive two implementations which -/// use shared borrows or mut borrows). -/// -/// Note that this macro is meant to work on a limited set of cases: it is not -/// very general. -/// For instance, for now it only works on traits. -/// -/// Applied on a trait definition named "Trait", it will generate two traits: -/// "MutTrait" and "SharedTrait". -pub fn make_generic_in_borrows(tokens: TokenStream) -> TokenStream { - let input_item = parse_macro_input!(tokens as ItemTrait); - // We should have received the shared version - let mut shared_item = input_item.clone(); - let mut mut_item = input_item; - - let id = shared_item.ident.clone(); - mut_item.ident = generic_mk_ident(&id, true); - shared_item.ident = generic_mk_ident(&id, false); - - generic_supertraits_to_mut_shared(&mut shared_item, false); - generic_supertraits_to_mut_shared(&mut mut_item, true); - - // Update the shared version - for item in &mut shared_item.items { - generic_mk_item(&id, false, item) - } - - // Update the mutable version - for item in &mut mut_item.items { - generic_mk_item(&id, true, item) - } - - // TODO: This is not very clean, but I don't know how to concatenate stream tokens - format!( - "{}\n{}", - shared_item.to_token_stream(), - mut_item.to_token_stream() - ) - .parse() - .unwrap() -} diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs index de11aa7c1..5c9997c17 100644 --- a/charon/src/ast/expressions.rs +++ b/charon/src/ast/expressions.rs @@ -1,15 +1,15 @@ //! Implements expressions: paths, operands, rvalues, lvalues -pub use crate::expressions_utils::*; use crate::gast::{FunDeclId, TraitItemName}; use crate::types::*; pub use crate::values::VarId; use crate::values::*; +use derive_visitor::{Drive, DriveMut}; use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName}; use serde::{Deserialize, Serialize}; use std::vec::Vec; -#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize)] +#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Place { // TODO: update to transform to a recursive type pub var_id: VarId, @@ -37,6 +37,8 @@ pub type Projection = Vec; VariantName, Serialize, Deserialize, + Drive, + DriveMut, )] pub enum ProjectionElem { /// Dereference a shared/mutable reference. @@ -70,7 +72,19 @@ pub enum ProjectionElem { Index(Operand, Ty), } -#[derive(Debug, PartialEq, Eq, Copy, Clone, EnumIsA, EnumAsGetters, Serialize, Deserialize)] +#[derive( + Debug, + PartialEq, + Eq, + Copy, + Clone, + EnumIsA, + EnumAsGetters, + Serialize, + Deserialize, + Drive, + DriveMut, +)] pub enum FieldProjKind { #[serde(rename = "ProjAdt")] Adt(TypeDeclId, Option), @@ -83,7 +97,19 @@ pub enum FieldProjKind { ClosureState, } -#[derive(Debug, PartialEq, Eq, Copy, Clone, EnumIsA, EnumAsGetters, Serialize, Deserialize)] +#[derive( + Debug, + PartialEq, + Eq, + Copy, + Clone, + EnumIsA, + EnumAsGetters, + Serialize, + Deserialize, + Drive, + DriveMut, +)] pub enum BorrowKind { Shared, Mut, @@ -99,7 +125,9 @@ pub enum BorrowKind { } /// Unary operation -#[derive(Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize)] +#[derive( + Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut, +)] pub enum UnOp { Not, /// This can overflow. In practice, rust introduces an assert before @@ -120,7 +148,9 @@ pub enum UnOp { /// For all the variants: the first type gives the source type, the second one gives /// the destination type. -#[derive(Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize)] +#[derive( + Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut, +)] pub enum CastKind { /// Conversion between types in {Integer, Bool} /// Remark: for now we don't support conversions with Char. @@ -129,7 +159,9 @@ pub enum CastKind { } /// Binary operations. -#[derive(Debug, PartialEq, Eq, Copy, Clone, EnumIsA, VariantName, Serialize, Deserialize)] +#[derive( + Debug, PartialEq, Eq, Copy, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut, +)] pub enum BinOp { BitXor, BitAnd, @@ -176,6 +208,8 @@ pub enum BinOp { VariantName, Serialize, Deserialize, + Drive, + DriveMut, )] pub enum Operand { Copy(Place), @@ -186,7 +220,17 @@ pub enum Operand { /// A function identifier. See [crate::ullbc_ast::Terminator] #[derive( - Debug, Clone, PartialEq, Eq, EnumIsA, EnumAsGetters, VariantName, Serialize, Deserialize, + Debug, + Clone, + PartialEq, + Eq, + EnumIsA, + EnumAsGetters, + VariantName, + Serialize, + Deserialize, + Drive, + DriveMut, )] pub enum FunId { /// A "regular" function (function local to the crate, external function @@ -201,7 +245,18 @@ pub enum FunId { /// An assumed function identifier, identifying a function coming from a /// standard library. #[derive( - Debug, Clone, Copy, PartialEq, Eq, EnumIsA, EnumAsGetters, VariantName, Serialize, Deserialize, + Debug, + Clone, + Copy, + PartialEq, + Eq, + EnumIsA, + EnumAsGetters, + VariantName, + Serialize, + Deserialize, + Drive, + DriveMut, )] pub enum AssumedFunId { /// `alloc::boxed::Box::new` @@ -254,7 +309,7 @@ pub enum AssumedFunId { SliceIndexMut, } -#[derive(Debug, Clone, PartialEq, Eq, EnumAsGetters, Serialize, Deserialize)] +#[derive(Debug, Clone, PartialEq, Eq, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut)] pub enum FunIdOrTraitMethodRef { Fun(FunId), /// If a trait: the reference to the trait and the id of the trait method. @@ -263,7 +318,7 @@ pub enum FunIdOrTraitMethodRef { Trait(TraitRef, TraitItemName, FunDeclId), } -#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize)] +#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct FnPtr { pub func: FunIdOrTraitMethodRef, pub generics: GenericArgs, @@ -296,7 +351,17 @@ pub struct FnPtr { /// MIR seems to forbid more complex expressions like paths. For instance, /// reading the constant `a.b` is translated to `{ _1 = const a; _2 = (_1.0) }`. #[derive( - Debug, PartialEq, Eq, Clone, VariantName, EnumIsA, EnumAsGetters, Serialize, Deserialize, + Debug, + PartialEq, + Eq, + Clone, + VariantName, + EnumIsA, + EnumAsGetters, + Serialize, + Deserialize, + Drive, + DriveMut, )] pub enum RawConstantExpr { Literal(Literal), @@ -353,7 +418,7 @@ pub enum RawConstantExpr { FnPtr(FnPtr), } -#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize)] +#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct ConstantExpr { pub value: RawConstantExpr, pub ty: Ty, @@ -361,7 +426,9 @@ pub struct ConstantExpr { /// TODO: we could factor out [Rvalue] and function calls (for LLBC, not ULLBC). /// We can also factor out the unops, binops with the function calls. -#[derive(Debug, Clone, EnumToGetters, EnumAsGetters, EnumIsA, Serialize, Deserialize)] +#[derive( + Debug, Clone, EnumToGetters, EnumAsGetters, EnumIsA, Serialize, Deserialize, Drive, DriveMut, +)] pub enum Rvalue { Use(Operand), Ref(Place, BorrowKind), @@ -428,7 +495,7 @@ pub enum Rvalue { Repeat(Operand, Ty, ConstGeneric), } -#[derive(Debug, Clone, VariantIndexArity, Serialize, Deserialize)] +#[derive(Debug, Clone, VariantIndexArity, Serialize, Deserialize, Drive, DriveMut)] pub enum AggregateKind { Adt(TypeId, Option, GenericArgs), /// We don't put this with the ADT cas because this is the only assumed type diff --git a/charon/src/ast/expressions_utils.rs b/charon/src/ast/expressions_utils.rs index 2dceb7a85..6690ec1e7 100644 --- a/charon/src/ast/expressions_utils.rs +++ b/charon/src/ast/expressions_utils.rs @@ -1,10 +1,6 @@ //! This file groups everything which is linked to implementations about [crate::expressions] use crate::expressions::*; -use crate::gast::{AssumedFunId, Call, FnOperand, FunId, FunIdOrTraitMethodRef, TraitItemName}; -use crate::types::*; -use crate::ullbc_ast::GlobalDeclId; use crate::values::*; -use macros::make_generic_in_borrows; use std::vec::Vec; impl Place { @@ -15,252 +11,3 @@ impl Place { } } } - -// Derive two implementations at once: one which uses shared borrows, and one -// which uses mutable borrows. -// Generates the traits: `SharedExprVisitor` and `MutExprVisitor`. -make_generic_in_borrows! { - -/// A visitor for expressions. -/// -/// TODO: implement macros to automatically derive visitors. -pub trait ExprVisitor: crate::types::TypeVisitor { - fn visit_place(&mut self, p: &Place) { - self.visit_var_id(&p.var_id); - self.visit_projection(&p.projection); - } - - fn visit_var_id(&mut self, _: &VarId) {} - - fn visit_projection(&mut self, p: &Projection) { - for pe in p.iter() { - self.visit_projection_elem(pe) - } - } - - fn default_visit_projection_elem(&mut self, pe: &ProjectionElem) { - match pe { - ProjectionElem::Deref => self.visit_deref(), - ProjectionElem::DerefBox => self.visit_deref_box(), - ProjectionElem::DerefRawPtr => self.visit_deref_raw_ptr(), - ProjectionElem::Field(proj_kind, fid) => self.visit_projection_field(proj_kind, fid), - ProjectionElem::Index(operand, _) => self.visit_operand(operand), - } - } - - fn visit_projection_elem(&mut self, pe: &ProjectionElem) { - self.default_visit_projection_elem(pe) - } - - fn visit_deref(&mut self) {} - fn visit_deref_box(&mut self) {} - fn visit_deref_raw_ptr(&mut self) {} - fn visit_projection_field(&mut self, _: &FieldProjKind, _: &FieldId) {} - - fn default_visit_operand(&mut self, o: &Operand) { - match o { - Operand::Copy(p) => self.visit_copy(p), - Operand::Move(p) => self.visit_move(p), - Operand::Const(cv) => self.visit_operand_const(cv), - } - } - - fn visit_operand(&mut self, o: &Operand) { - self.default_visit_operand(o) - } - - fn visit_copy(&mut self, p: &Place) { - self.visit_place(p) - } - - fn visit_move(&mut self, p: &Place) { - self.visit_place(p) - } - - fn visit_operand_const(&mut self, op: &ConstantExpr) { - self.visit_constant_expr(op); - } - - fn visit_constant_expr(&mut self, expr: &ConstantExpr) { - self.visit_ty(&expr.ty); - self.visit_raw_constant_expr(&expr.value); - } - - fn visit_raw_constant_expr(&mut self, expr: &RawConstantExpr) { - self.default_visit_raw_constant_expr(expr) - } - - fn default_visit_raw_constant_expr(&mut self, expr: &RawConstantExpr) { - use RawConstantExpr::*; - match expr { - Literal(lit) => self.visit_literal(lit), - Adt(oid, ops) => self.visit_constant_expr_adt(oid, ops), - Global(id, generics) => { - self.visit_global_decl_id(id); - self.visit_generic_args(generics); - } - TraitConst(trait_ref, _name) => { - self.visit_trait_ref(trait_ref); - } - Ref(cv) => self.visit_constant_expr(cv), - Var(id) => self.visit_const_generic_var_id(id), - FnPtr(f) => { - self.visit_fn_ptr(f); - } - } - } - - fn visit_constant_expr_adt(&mut self, _oid: &Option, ops: &Vec) { - for op in ops { - self.visit_constant_expr(op) - } - } - - fn default_visit_rvalue(&mut self, rv: &Rvalue) { - match rv { - Rvalue::Use(o) => self.visit_use(o), - Rvalue::Ref(p, bkind) => self.visit_ref(p, bkind), - Rvalue::UnaryOp(op, o1) => self.visit_unary_op(op, o1), - Rvalue::BinaryOp(op, o1, o2) => self.visit_binary_op(op, o1, o2), - Rvalue::Discriminant(p, adt_id) => self.visit_discriminant(p, adt_id), - Rvalue::Aggregate(kind, ops) => self.visit_aggregate(kind, ops), - Rvalue::Global(gid, generics) => { - self.visit_global(gid); - self.visit_generic_args(generics); - } - Rvalue::Len(p, ty, cg) => self.visit_len(p, ty, cg), - Rvalue::Repeat(op, ty, cg) => self.visit_repeat(op, ty, cg), - } - } - - fn visit_rvalue(&mut self, o: &Rvalue) { - self.default_visit_rvalue(o) - } - - fn visit_use(&mut self, o: &Operand) { - self.visit_operand(o) - } - - fn visit_ref(&mut self, p: &Place, _: &BorrowKind) { - self.visit_place(p) - } - - fn visit_unary_op(&mut self, unop: &UnOp, o1: &Operand) { - match unop { - UnOp::Not | UnOp::Neg | UnOp::Cast(CastKind::Scalar(_, _)) => (), - UnOp::Cast(CastKind::FnPtr(src, tgt)) => { - self.visit_ty(src); - self.visit_ty(tgt); - } - UnOp::ArrayToSlice(_, ty, cg) => { - self.visit_ty(ty); - self.visit_const_generic(cg); - } - } - self.visit_operand(o1) - } - - fn visit_binary_op(&mut self, _: &BinOp, o1: &Operand, o2: &Operand) { - self.visit_operand(o1); - self.visit_operand(o2); - } - - fn visit_discriminant(&mut self, p: &Place, adt_id: &TypeDeclId) { - self.visit_place(p); - self.visit_type_decl_id(adt_id); - } - - fn visit_aggregate(&mut self, ak: &AggregateKind, ops: &Vec) { - self.visit_aggregate_kind(ak); - for o in ops { - self.visit_operand(o) - } - } - - fn visit_aggregate_kind(&mut self, ak: &AggregateKind) { - use AggregateKind::*; - // We could generalize and introduce auxiliary functions for - // the various cases - this is not necessary for now - match ak { - Adt(adt_id, _, generics) => { - self.visit_type_id(adt_id); - self.visit_generic_args(generics); - } - Array(ty, cg) => { - self.visit_ty(ty); - self.visit_const_generic(cg); - } - Closure(fn_id, generics) => { - self.visit_fun_decl_id(fn_id); - self.visit_generic_args(generics); - } - } - } - - fn visit_global(&mut self, _: &GlobalDeclId) {} - - fn visit_len(&mut self, p: &Place, ty: &Ty, cg: &Option) { - self.visit_place(p); - self.visit_ty(ty); - match cg { - Some(cg) => self.visit_const_generic(cg), - None => (), - } - } - - fn visit_repeat(&mut self, op: &Operand, ty: &Ty, cg: &ConstGeneric) { - self.visit_operand(op); - self.visit_ty(ty); - self.visit_const_generic(cg); - } - - fn visit_call(&mut self, c: &Call) { - let Call { - func, - args, - dest, - } = c; - self.visit_fn_operand(func); - for o in args { - self.visit_operand(o); - } - self.visit_place(dest); - } - - fn visit_fn_ptr(&mut self, fn_ptr: &FnPtr) { - let FnPtr { func, generics } = fn_ptr; - self.visit_fun_id_or_trait_ref(func); - self.visit_generic_args(generics); - } - - fn visit_fn_operand(&mut self, fn_op: &FnOperand) { - match fn_op { - FnOperand::Regular(func) => self.visit_fn_ptr(func), - FnOperand::Move(p) => self.visit_place(p), - } - } - - fn visit_fun_id(&mut self, fun_id: &FunId) { - match fun_id { - FunId::Regular(fid) => self.visit_fun_decl_id(fid), - FunId::Assumed(aid) => self.visit_assumed_fun_id(aid), - } - } - - fn visit_fun_id_or_trait_ref(&mut self, fun_id: &FunIdOrTraitMethodRef) { - use FunIdOrTraitMethodRef::*; - match fun_id { - Fun(fun_id) => self.visit_fun_id(fun_id), - Trait(trait_ref, method_id, fun_decl_id) => { - self.visit_trait_ref(trait_ref); - self.visit_trait_method_name(method_id); - self.visit_fun_decl_id(fun_decl_id); - } - } - } - - fn visit_trait_method_name(&mut self, _: &TraitItemName) {} - fn visit_assumed_fun_id(&mut self, _: &AssumedFunId) {} -} - -} // make_generic_in_borrows diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs index cb879df03..d6a48e0d8 100644 --- a/charon/src/ast/gast.rs +++ b/charon/src/ast/gast.rs @@ -13,6 +13,7 @@ pub use crate::types::{ GenericArgs, GenericParams, TraitDeclId, TraitImplId, TraitInstanceId, TraitRef, }; use crate::ullbc_ast; +use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut}; use macros::EnumIsA; use macros::EnumToGetters; use serde::{Deserialize, Serialize}; @@ -30,7 +31,7 @@ fn dummy_def_id() -> rustc_hir::def_id::DefId { } /// A variable -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Var { /// Unique index identifying the variable pub index: VarId, @@ -42,7 +43,7 @@ pub struct Var { } /// Marker to indicate that a declaration is opaque (i.e. we don't inspect its body). -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Copy, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Opaque; /// An expression body. @@ -62,8 +63,30 @@ pub struct GExprBody { pub body: T, } +// The derive macro doesn't handle generics well. +impl Drive for GExprBody { + fn drive(&self, visitor: &mut V) { + visitor.visit(self, Event::Enter); + self.span.drive(visitor); + self.arg_count.drive(visitor); + self.locals.drive(visitor); + self.body.drive(visitor); + visitor.visit(self, Event::Exit); + } +} +impl DriveMut for GExprBody { + fn drive_mut(&mut self, visitor: &mut V) { + visitor.visit(self, Event::Enter); + self.span.drive_mut(visitor); + self.arg_count.drive_mut(visitor); + self.locals.drive_mut(visitor); + self.body.drive_mut(visitor); + visitor.visit(self, Event::Exit); + } +} + /// The body of a function or a constant. -#[derive(Debug, Clone, Serialize, Deserialize, EnumIsA, EnumToGetters)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut, EnumIsA, EnumToGetters)] pub enum Body { /// Body represented as a CFG. This is what ullbc is made of, and what we get after translating MIR. Unstructured(ullbc_ast::ExprBody), @@ -93,7 +116,7 @@ pub enum Body { /// fn test(...) { ... } // regular /// } /// ``` -#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut, PartialEq, Eq)] pub enum ItemKind { /// A "normal" function Regular, @@ -116,10 +139,12 @@ pub enum ItemKind { } /// A function definition -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct FunDecl { + #[drive(skip)] pub def_id: FunDeclId, #[serde(skip)] + #[drive(skip)] #[serde(default = "dummy_def_id")] pub rust_id: rustc_hir::def_id::DefId, /// The meta data associated with the declaration. @@ -140,10 +165,12 @@ pub struct FunDecl { } /// A global variable definition -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct GlobalDecl { + #[drive(skip)] pub def_id: GlobalDeclId, #[serde(skip)] + #[drive(skip)] #[serde(default = "dummy_def_id")] pub rust_id: rustc_hir::def_id::DefId, /// The meta data associated with the declaration. @@ -153,14 +180,15 @@ pub struct GlobalDecl { pub is_local: bool, pub name: Name, pub generics: GenericParams, - pub preds: Predicates, pub ty: Ty, /// The global kind: "regular" function, trait const declaration, etc. pub kind: ItemKind, pub body: Result, } -#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, PartialOrd, Ord)] +#[derive( + Debug, Clone, Serialize, Deserialize, Drive, DriveMut, PartialEq, Eq, Hash, PartialOrd, Ord, +)] pub struct TraitItemName(pub String); /// A trait **declaration**. @@ -196,8 +224,9 @@ pub struct TraitItemName(pub String); /// Of course, this forbids other useful use cases such as visitors implemented /// by means of traits. #[allow(clippy::type_complexity)] -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct TraitDecl { + #[drive(skip)] pub def_id: TraitDeclId, /// [true] if the decl is a local decl, [false] if it comes from /// an external crate. @@ -205,7 +234,6 @@ pub struct TraitDecl { pub item_meta: ItemMeta, pub name: Name, pub generics: GenericParams, - pub preds: Predicates, /// The "parent" clauses: the supertraits. /// /// Supertraits are actually regular where clauses, but we decided to have @@ -258,8 +286,9 @@ pub struct TraitDecl { /// fn baz(...) { ... } /// } /// ``` -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct TraitImpl { + #[drive(skip)] pub def_id: TraitImplId, /// [true] if the decl is a local decl, [false] if it comes from /// an external crate. @@ -271,7 +300,6 @@ pub struct TraitImpl { /// clauses. pub impl_trait: TraitDeclRef, pub generics: GenericParams, - pub preds: Predicates, /// The trait references for the parent clauses (see [TraitDecl]). pub parent_trait_refs: Vector, /// The associated constants declared in the trait. @@ -287,7 +315,7 @@ pub struct TraitImpl { /// A function operand is used in function calls. /// It either designates a top-level function, or a place in case /// we are using function pointers stored in local variables. -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub enum FnOperand { /// Regular case: call to a top-level function, trait method, etc. Regular(FnPtr), @@ -295,14 +323,14 @@ pub enum FnOperand { Move(Place), } -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Call { pub func: FnOperand, pub args: Vec, pub dest: Place, } -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub enum AbortKind { /// A built-in panicking function. Panic(Name), diff --git a/charon/src/ast/llbc_ast.rs b/charon/src/ast/llbc_ast.rs index 979d91a0f..b89c61035 100644 --- a/charon/src/ast/llbc_ast.rs +++ b/charon/src/ast/llbc_ast.rs @@ -12,6 +12,7 @@ use crate::meta::Span; use crate::types::*; pub use crate::ullbc_ast::{Call, FunDeclId, GlobalDeclId, Var}; use crate::values::*; +use derive_visitor::{Drive, DriveMut}; use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName}; use serde::{Deserialize, Serialize}; @@ -19,14 +20,16 @@ use serde::{Deserialize, Serialize}; /// checks, to detect out-of-bounds accesses or divisions by zero for /// instance. We eliminate the assertions in [crate::remove_dynamic_checks], /// then introduce other dynamic checks in [crate::reconstruct_asserts]. -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Assert { pub cond: Operand, pub expected: bool, } /// A raw statement: a statement without meta data. -#[derive(Debug, Clone, EnumIsA, EnumToGetters, EnumAsGetters, Serialize, Deserialize)] +#[derive( + Debug, Clone, EnumIsA, EnumToGetters, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut, +)] pub enum RawStatement { Assign(Place, Rvalue), FakeRead(Place), @@ -52,17 +55,15 @@ pub enum RawStatement { Continue(usize), /// No-op. Nop, - /// The left statement must NOT be a sequence. - /// For instance, `(s0; s1); s2` is forbidden and should be rewritten - /// to the semantically equivalent statement `s0; (s1; s2)` - /// To ensure that, use [crate::llbc_ast_utils::new_sequence] to build sequences. - Sequence(Box, Box), + /// The contained statements must NOT be sequences. To ensure that, use [Sequence::then] to + /// build sequences. + Sequence(Vec), Switch(Switch), Loop(Box), Error(String), } -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Statement { pub span: Span, pub content: RawStatement, @@ -76,6 +77,8 @@ pub struct Statement { EnumAsGetters, Serialize, Deserialize, + Drive, + DriveMut, VariantName, VariantIndexArity, )] diff --git a/charon/src/ast/llbc_ast_utils.rs b/charon/src/ast/llbc_ast_utils.rs index 45ee493ed..05155462c 100644 --- a/charon/src/ast/llbc_ast_utils.rs +++ b/charon/src/ast/llbc_ast_utils.rs @@ -1,61 +1,21 @@ //! Implementations for [crate::llbc_ast] -use crate::common::ensure_sufficient_stack; -use crate::expressions::{MutExprVisitor, Operand, Place, Rvalue}; -use crate::llbc_ast::{Assert, RawStatement, Statement, Switch}; +use crate::llbc_ast::{RawStatement, Statement, Switch}; use crate::meta; use crate::meta::Span; -use crate::types::*; -use crate::values::*; -use macros::make_generic_in_borrows; -use std::ops::DerefMut; +use derive_visitor::{visitor_fn_mut, DriveMut, Event}; use take_mut::take; -/// Goes from e.g. `(A; B; C) ; D` to `(A; (B; (C; D)))`. +/// Goes from e.g. `(A; B; C) ; D` to `(A; (B; (C; D)))`. Statements in `firsts` must not be +/// sequences. pub fn chain_statements(firsts: Vec, last: Statement) -> Statement { - firsts.into_iter().rev().fold(last, |cont, bind| { - assert!(!bind.content.is_sequence()); - let span = meta::combine_span(&bind.span, &cont.span); - Statement::new(span, RawStatement::Sequence(Box::new(bind), Box::new(cont))) - }) -} - -/// Utility function for [new_sequence]. -/// Efficiently appends a new statement at the rightmost place of a well-formed sequence. -fn append_rightmost(seq: &mut Statement, r: Box) { - let (_l1, l2) = match &mut seq.content { - RawStatement::Sequence(l1, l2) => (l1, l2), - _ => unreachable!(), - }; - if l2.content.is_sequence() { - append_rightmost(l2, r); + if let Some(firsts) = Statement::from_seq(firsts) { + firsts.then(last) } else { - take(l2.deref_mut(), move |l2| { - let span = meta::combine_span(&l2.span, &r.span); - Statement::new(span, RawStatement::Sequence(Box::new(l2), r)) - }); + last } } -/// Builds a sequence from well-formed statements. -/// Ensures that the left statement will not be a sequence in the new sequence: -/// Must be used instead of the raw [RawStatement::Sequence] constructor, -/// unless you're sure that the left statement is not a sequence. -pub fn new_sequence(mut l: Statement, r: Statement) -> Statement { - let span = meta::combine_span(&l.span, &r.span); - - let r = Box::new(r); - let nst = match l.content { - RawStatement::Sequence(_, _) => { - append_rightmost(&mut l, r); - l.content - } - lc => RawStatement::Sequence(Box::new(Statement::new(l.span, lc)), r), - }; - - Statement::new(span, nst) -} - /// Combine the span information from a [Switch] pub fn combine_switch_targets_span(targets: &Switch) -> Span { match targets { @@ -109,248 +69,137 @@ impl Statement { pub fn new(span: Span, content: RawStatement) -> Self { Statement { span, content } } -} - -// Derive two implementations at once: one which uses shared borrows, and one -// which uses mutable borrows. -// Generates the traits: `SharedAstVisitor` and `MutAstVisitor`. -make_generic_in_borrows! { - -/// A visitor for the LLBC AST -/// -/// Remark: we can't call the "super" method when reimplementing a method -/// (unlike what can be done in, say, OCaml). This makes imlementing visitors -/// slightly awkward, and is the reason why we split some visit functions in two: -/// a "standard" version to be overriden, and a "default" version which should -/// not be overriden and gives access to the "super" method. -/// -/// TODO: implement macros to automatically derive visitors. -/// TODO: explore all the types -pub trait AstVisitor: crate::expressions::ExprVisitor { - /// We call this function right after we explored all the branches - /// in a branching. - fn merge(&mut self) {} - fn default_visit_statement(&mut self, st: &Statement) { - self.visit_span(&st.span); - ensure_sufficient_stack(|| { - self.visit_raw_statement(&st.content) - }) - } - - fn visit_statement(&mut self, st: &Statement) { - self.default_visit_statement(st) - } - - fn visit_span(&mut self, st: &Span) {} - - fn default_visit_raw_statement(&mut self, st: &RawStatement) { - match st { - RawStatement::Assign(p, rv) => { - self.visit_assign(p, rv); - } - RawStatement::FakeRead(p) => { - self.visit_fake_read(p); - } - RawStatement::SetDiscriminant(p, vid) => { - self.visit_set_discriminant(p, vid); - } - RawStatement::Drop(p) => { - self.visit_drop(p); - } - RawStatement::Assert(a) => { - self.visit_assert(a); - } - RawStatement::Call(c) => { - self.visit_call(c); - } - RawStatement::Abort(..) => { - self.visit_abort(); - } - RawStatement::Return => self.visit_return(), - RawStatement::Break(i) => { - self.visit_break(i); - } - RawStatement::Continue(i) => { - self.visit_continue(i); - } - RawStatement::Nop => self.visit_nop(), - RawStatement::Sequence(st1, st2) => self.visit_sequence(st1, st2), - RawStatement::Switch(s) => self.visit_switch(s), - RawStatement::Loop(lp) => self.visit_loop(lp), - RawStatement::Error(s) => self.visit_error(s), + pub fn from_seq(seq: Vec) -> Option { + if seq.is_empty() { + None + } else { + let span = seq + .iter() + .map(|st| st.span) + .reduce(|a, b| meta::combine_span(&a, &b)) + .unwrap(); + Some(Statement { + span, + content: RawStatement::Sequence(seq), + }) } } - fn visit_raw_statement(&mut self, st: &RawStatement) { - self.default_visit_raw_statement(st); - } - - fn visit_assign(&mut self, p: &Place, rv: &Rvalue) { - self.visit_place(p); - self.visit_rvalue(rv) - } - - fn visit_fake_read(&mut self, p: &Place) { - self.visit_place(p); + pub fn into_box(self) -> Box { + Box::new(self) } - fn visit_set_discriminant(&mut self, p: &Place, _: &VariantId) { - self.visit_place(p); - } + /// Builds a sequence from well-formed statements. Ensures that we don't incorrectly nest + /// sequences. Must be used instead of the raw [RawStatement::Sequence] constructor. + pub fn then(self, r: Statement) -> Statement { + let span = meta::combine_span(&self.span, &r.span); - fn visit_drop(&mut self, p: &Place) { - self.visit_place(p); - } + let vec = if !self.content.is_sequence() && !r.content.is_sequence() { + vec![self, r] + } else { + let mut l = self.into_sequence(); + let mut r = r.into_sequence(); + l.append(&mut r); + l + }; - fn visit_assert(&mut self, a: &Assert) { - self.visit_operand(&a.cond); + Statement::new(span, RawStatement::Sequence(vec)) } - fn visit_abort(&mut self) {} - fn visit_return(&mut self) {} - fn visit_break(&mut self, _: &usize) {} - fn visit_continue(&mut self, _: &usize) {} - fn visit_nop(&mut self) {} - fn visit_error(&mut self, _: &String) {} - - - fn visit_sequence(&mut self, st1: &Statement, st2: &Statement) { - self.visit_statement(st1); - self.visit_statement(st2); - } - - fn default_visit_switch(&mut self, s: &Switch) { - match s { - Switch::If(scrut, then_branch, else_branch) => { - self.visit_if(scrut, then_branch, else_branch) - } - Switch::SwitchInt(scrut, int_ty, branches, otherwise) => { - self.visit_switch_int(scrut, int_ty, branches, otherwise) - } - Switch::Match(scrut, branches, otherwise) => { - self.visit_match(scrut, branches, otherwise) - } + pub fn then_opt(self, other: Option) -> Statement { + if let Some(other) = other { + self.then(other) + } else { + self } } - fn visit_switch(&mut self, s: &Switch) { - self.default_visit_switch(s) - } - - /// Generic visitor for branches. - fn visit_branch(&mut self, branch: &Statement) { - self.visit_statement(branch); - } - - fn visit_if(&mut self, scrut: &Operand, then_branch: &Statement, else_branch: &Statement) { - self.visit_operand(scrut); - self.visit_branch(then_branch); - self.visit_branch(else_branch); - self.merge(); - } - - fn visit_switch_int( - &mut self, - scrut: &Operand, - _: &IntegerTy, - branches: &Vec<(Vec, Statement)>, - otherwise: &Statement, - ) { - self.visit_operand(scrut); - for (_, st) in branches { - self.visit_branch(st); + /// If `self` is a sequence, return that sequence. Otherwise return `vec![self]`. + pub fn into_sequence(self) -> Vec { + match self.content { + RawStatement::Sequence(vec) => vec, + _ => vec![self], } - self.visit_branch(otherwise); - self.merge(); } - fn visit_match( - &mut self, - scrut: &Place, - branches: &Vec<(Vec, Statement)>, - otherwise: &Option>, - ) { - self.visit_place(scrut); - for (_, st) in branches { - self.visit_branch(st); - } - if let Some(otherwise) = otherwise { - self.visit_branch(otherwise); + pub fn as_sequence_slice_mut(&mut self) -> &mut [Self] { + match self.content { + RawStatement::Sequence(ref mut vec) => vec.as_mut_slice(), + _ => std::slice::from_mut(self), } - self.merge(); } - fn visit_loop(&mut self, lp: &Statement) { - self.visit_statement(lp) + /// If `self` is a sequence that contains sequences, flatten the nesting. Use this when + /// mutating a statement in a visitor if needed. + pub fn flatten(&mut self) { + if let RawStatement::Sequence(vec) = &self.content { + if vec.iter().any(|st| st.content.is_sequence()) { + take(&mut self.content, |rawst| { + RawStatement::Sequence( + rawst + .to_sequence() + .into_iter() + .flat_map(|st| st.into_sequence()) + .collect(), + ) + }) + } + } } -} -} // make_generic_in_borrows - -/// Helper for [transform_statements] -struct TransformStatements<'a, F: FnMut(&mut Statement) -> Option>> { - tr: &'a mut F, -} - -impl<'a, F: FnMut(&mut Statement) -> Option>> MutTypeVisitor - for TransformStatements<'a, F> -{ -} -impl<'a, F: FnMut(&mut Statement) -> Option>> MutExprVisitor - for TransformStatements<'a, F> -{ -} - -impl<'a, F: FnMut(&mut Statement) -> Option>> MutAstVisitor - for TransformStatements<'a, F> -{ - fn visit_statement(&mut self, st: &mut Statement) { - match &mut st.content { - RawStatement::Sequence(st1, st2) => { - // Bottom-up - self.visit_statement(st2); - self.default_visit_raw_statement(&mut st1.content); - - // Transform the current statement - let st_seq = (self.tr)(st1); - if let Some(seq) = st_seq - && !seq.is_empty() - { - take(st, |st| chain_statements(seq, st)) - } - // TODO: we might want to apply tr to the whole resulting sequence - } - _ => { - // Bottom-up - self.default_visit_raw_statement(&mut st.content); + /// Apply a transformer to all the statements, in a bottom-up manner. + /// + /// The transformer should: + /// - mutate the current statement in place + /// - return the sequence of statements to introduce before the current statement + pub fn transform Option>>(&mut self, f: &mut F) { + self.drive_mut(&mut visitor_fn_mut(|st: &mut Statement, e: Event| { + if matches!(e, Event::Exit) { + // Flatten any nested sequences created while traversing this statement.. + st.flatten(); // Transform the current statement - let st_seq = (self.tr)(st); - if let Some(seq) = st_seq - && !seq.is_empty() + let prefix_seq = f(st); + if let Some(prefix_seq) = prefix_seq + && !prefix_seq.is_empty() { - take(st, |st| chain_statements(seq, st)) + take_mut::take(st, |st| chain_statements(prefix_seq, st)) } } - } + })); } -} -impl Statement { - /// Apply a transformer to all the statements, in a bottom-up manner. + /// Apply a transformer to all the statements, in a bottom-up manner. Compared to `transform`, + /// this also gives access to the following statements if any. Statements that are not part of + /// a sequence will be traversed as `[st]`. Statements that are will be traversed twice: once + /// as `[st]`, and then as `[st, ..]` with the following statements if any. /// /// The transformer should: - /// - mutate the current statement in place - /// - return the sequence of statements to introduce before the current statement - /// - /// We do the transformation in such a way that the - /// sequences of statements are properly chained. In particuliar, - /// if in `s1; s2` we transform `s1` to the sequence `s1_1; s1_2`, - /// then the resulting statement is `s1_1; s1_2; s2` and **not** - /// `{ s1_1; s1_2 }; s2`. - pub fn transform Option>>(&mut self, f: &mut F) { - let mut visitor = TransformStatements { tr: f }; - visitor.visit_statement(self); + /// - mutate the current statements in place + /// - return the sequence of statements to introduce before the current statements + pub fn transform_sequences Vec>(&mut self, f: &mut F) { + self.drive_mut(&mut visitor_fn_mut(|st: &mut Statement, e: Event| { + if matches!(e, Event::Exit) { + // Flatten any nested sequences created while traversing this statement.. + st.flatten(); + + if let RawStatement::Sequence(seq) = &mut st.content { + for i in (0..seq.len()).rev() { + let prefix_to_insert = f(&mut seq[i..]); + if !prefix_to_insert.is_empty() { + // Insert the new elements at index `i`. This only modifies `vec[i..]` + // so we can keep iterating `i` down as if nothing happened. + seq.splice(i..i, prefix_to_insert); + } + } + } else { + let prefix_to_insert = f(std::slice::from_mut(st)); + if !prefix_to_insert.is_empty() { + take_mut::take(st, |st| chain_statements(prefix_to_insert, st)) + } + } + } + })); } } diff --git a/charon/src/ast/meta.rs b/charon/src/ast/meta.rs index 0d4c237a3..b84479a6f 100644 --- a/charon/src/ast/meta.rs +++ b/charon/src/ast/meta.rs @@ -1,6 +1,8 @@ //! Meta-information about programs (spans, etc.). pub use crate::meta_utils::*; +use derive_visitor::{Drive, DriveMut}; +use hax_frontend_exporter::PathBuf; use macros::{EnumAsGetters, EnumIsA}; use serde::{Deserialize, Serialize}; @@ -20,13 +22,15 @@ generate_index_type!(VirtualFileId); EnumAsGetters, Serialize, Deserialize, + Drive, + DriveMut, )] pub enum FileId { LocalId(LocalFileId), VirtualId(VirtualFileId), } -#[derive(Debug, Copy, Clone, Serialize, Deserialize)] +#[derive(Debug, Copy, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Loc { /// The (1-based) line number. pub line: usize, @@ -40,7 +44,7 @@ fn dummy_span_data() -> rustc_span::SpanData { } /// Span information -#[derive(Debug, Copy, Clone, Serialize, Deserialize)] +#[derive(Debug, Copy, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct RawSpan { pub file_id: FileId, pub beg: Loc, @@ -51,6 +55,7 @@ pub struct RawSpan { /// single-threaded (default on older versions). We need this to be `Send` because we pass this /// data out of the rustc callbacks in charon-driver. #[serde(skip)] + #[drive(skip)] #[serde(default = "dummy_span_data")] pub rust_span_data: rustc_span::SpanData, } @@ -62,7 +67,7 @@ impl From for rustc_error_messages::MultiSpan { } /// Meta information about a piece of code (block, statement, etc.) -#[derive(Debug, Copy, Clone, Serialize, Deserialize)] +#[derive(Debug, Copy, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Span { /// The source code span. /// @@ -98,7 +103,7 @@ impl From for rustc_error_messages::MultiSpan { pub type Attribute = String; /// `#[inline]` built-in attribute. -#[derive(Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[derive(Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] pub enum InlineAttr { /// `#[inline]` Hint, @@ -109,7 +114,7 @@ pub enum InlineAttr { } /// Meta information about an item (function, trait decl, trait impl, type decl, global). -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct ItemMeta { pub span: Span, /// Attributes (`#[...]`). @@ -135,21 +140,28 @@ pub struct ItemMeta { /// API (this is called "pub-in-priv" items). With or without the `pub use`, we set `public = /// true`; computing item reachability is harder. pub public: bool, + /// Attribute `charon::rename("...")` (and `aeneas::rename("...")`) to provide a custom + /// name that can be used for instance when extracting the code via Aeneas. + pub rename: Option, #[serde(skip_serializing)] #[serde(default)] pub opaque: bool, } -#[derive(Debug, PartialEq, Eq, Clone, Copy, Serialize, Deserialize)] +#[derive(Debug, PartialEq, Eq, Clone, Copy, Serialize, Deserialize, Drive, DriveMut)] pub struct FileInfo {} /// A filename. -#[derive(Debug, PartialEq, Eq, Clone, Hash, PartialOrd, Ord, Serialize, Deserialize)] +#[derive( + Debug, PartialEq, Eq, Clone, Hash, PartialOrd, Ord, Serialize, Deserialize, Drive, DriveMut, +)] pub enum FileName { /// A remapped path (namely paths into stdlib) - Virtual(String), + #[drive(skip)] // drive is not implemented for `PathBuf` + Virtual(PathBuf), /// A local path (a file coming from the current crate for instance) - Local(String), + #[drive(skip)] // drive is not implemented for `PathBuf` + Local(PathBuf), /// A "not real" file name (macro, query, etc.) NotReal(String), } diff --git a/charon/src/ast/meta_utils.rs b/charon/src/ast/meta_utils.rs index 4c6eab86b..b486ec939 100644 --- a/charon/src/ast/meta_utils.rs +++ b/charon/src/ast/meta_utils.rs @@ -6,6 +6,7 @@ use rustc_middle::ty::TyCtxt; use rustc_session::Session; use std::cmp::Ordering; use std::iter::Iterator; +use std::path::Component; /// Retrieve the Rust span from a def id. /// @@ -87,13 +88,23 @@ pub fn convert_filename(name: &hax::FileName) -> FileName { use hax::RealFileName; match name { RealFileName::LocalPath(path) => FileName::Local(path.clone()), - RealFileName::Remapped { - local_path: _, - virtual_name, - } => - // We use the virtual name because it is always available - { - FileName::Virtual(virtual_name.clone()) + RealFileName::Remapped { virtual_name, .. } => { + // We use the virtual name because it is always available. + // That name normally starts with `/rustc//`. For our purposes we hide + // the hash. + let mut components_iter = virtual_name.components(); + if let Some( + [Component::RootDir, Component::Normal(rustc), Component::Normal(hash)], + ) = components_iter.by_ref().array_chunks().next() + && rustc.to_str() == Some("rustc") + && hash.len() == 40 + { + let path_without_hash = + [Component::RootDir, Component::Normal(rustc)].into_iter().chain(components_iter).collect(); + FileName::Virtual(path_without_hash) + } else { + FileName::Virtual(virtual_name.clone()) + } } } } diff --git a/charon/src/ast/names.rs b/charon/src/ast/names.rs index fd4802aa3..386316f49 100644 --- a/charon/src/ast/names.rs +++ b/charon/src/ast/names.rs @@ -1,22 +1,24 @@ //! Defines some utilities for the variables use crate::types::*; +use derive_visitor::{Drive, DriveMut}; use macros::{EnumAsGetters, EnumIsA}; use serde::{Deserialize, Serialize}; generate_index_type!(Disambiguator); /// See the comments for [Name] -#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, EnumIsA, EnumAsGetters)] +#[derive( + Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut, EnumIsA, EnumAsGetters, +)] pub enum PathElem { Ident(String, Disambiguator), Impl(ImplElem), } -#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] pub struct ImplElem { pub disambiguator: Disambiguator, pub generics: GenericParams, - pub preds: Predicates, pub kind: ImplElemKind, } @@ -30,7 +32,7 @@ pub struct ImplElem { /// impl PartialEq for List { ...} /// ``` /// We distinguish the two. -#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] pub enum ImplElemKind { Ty(Ty), /// Remark: the first type argument in the trait ref gives the type for @@ -75,7 +77,7 @@ pub enum ImplElemKind { /// name clashes anyway. Still, we might want to be more precise in the future. /// /// Also note that the first path element in the name is always the crate name. -#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] #[serde(transparent)] pub struct Name { pub name: Vec, diff --git a/charon/src/ast/names_utils.rs b/charon/src/ast/names_utils.rs index c0690aea2..bb97a7aff 100644 --- a/charon/src/ast/names_utils.rs +++ b/charon/src/ast/names_utils.rs @@ -5,6 +5,7 @@ use crate::common::*; use crate::names::*; use crate::translate_ctx::*; +use crate::types::PredicateOrigin; use hax_frontend_exporter as hax; use hax_frontend_exporter::SInto; use rustc_hir::{Item, ItemKind}; @@ -205,26 +206,28 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // a body translation context. let id = cur_id; + // Translate from hax to LLBC + let mut bt_ctx = BodyTransCtx::new(id, self); + // Translate to hax types - let s1 = &hax::State::new_from_state_and_id(&self.hax_state, id); - let substs = - rustc_middle::ty::GenericArgs::identity_for_item(tcx, id).sinto(s1); // TODO: use the bounds - let _bounds: Vec = tcx + let _bounds: Vec = bt_ctx + .t_ctx + .tcx .predicates_of(id) .predicates .iter() - .map(|(x, _)| x.sinto(s1)) + .map(|(x, _)| x.sinto(&bt_ctx.hax_state)) .collect(); - let ty = tcx.type_of(id).instantiate_identity().sinto(s1); - - // Translate from hax to LLBC - let mut bt_ctx = BodyTransCtx::new(id, self); + let ty = tcx + .type_of(id) + .instantiate_identity() + .sinto(&bt_ctx.hax_state); + bt_ctx.translate_generic_params(id).unwrap(); bt_ctx - .translate_generic_params_from_hax(span, &substs) + .translate_predicates_of(None, id, PredicateOrigin::WhereClauseOnImpl) .unwrap(); - bt_ctx.translate_predicates_of(None, id).unwrap(); let erase_regions = false; // Two cases, depending on whether the impl block is // a "regular" impl block (`impl Foo { ... }`) or a trait @@ -253,7 +256,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { name.push(PathElem::Impl(ImplElem { disambiguator, generics: bt_ctx.get_generics(), - preds: bt_ctx.get_predicates(), kind, })); } @@ -296,23 +298,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { Ok(Name { name }) } - pub(crate) fn make_hax_state_with_id( - &mut self, - def_id: DefId, - ) -> hax::State, (), (), DefId> { - hax::state::State { - thir: (), - mir: (), - owner_id: def_id, - base: hax::Base::new( - self.tcx, - hax::options::Options { - inline_macro_calls: Vec::new(), - }, - ), - } - } - /// Returns an optional name for an HIR item. /// /// If the option is `None`, it means the item is to be ignored (example: it diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 8c3a46c7c..c9c5c2d5d 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -5,6 +5,7 @@ use crate::names::Name; pub use crate::types_utils::*; use crate::values::{Literal, ScalarValue}; use derivative::Derivative; +use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut}; use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName}; use serde::{Deserialize, Serialize}; @@ -26,7 +27,7 @@ generate_index_type!(GlobalDeclId, "Global"); /// Type variable. /// We make sure not to mix variables and type variables by having two distinct /// definitions. -#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] pub struct TypeVar { /// Unique index identifying the variable pub index: TypeVarId, @@ -35,7 +36,9 @@ pub struct TypeVar { } /// Region variable. -#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Hash, PartialOrd, Ord)] +#[derive( + Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Hash, PartialOrd, Ord, Drive, DriveMut, +)] pub struct RegionVar { /// Unique index identifying the variable pub index: RegionId, @@ -44,7 +47,7 @@ pub struct RegionVar { } /// Const Generic Variable -#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] pub struct ConstGenericVar { /// Unique index identifying the variable pub index: ConstGenericVarId, @@ -54,7 +57,20 @@ pub struct ConstGenericVar { pub ty: LiteralTy, } -#[derive(Debug, PartialEq, Eq, Copy, Clone, Hash, PartialOrd, Ord, Serialize, Deserialize)] +#[derive( + Debug, + PartialEq, + Eq, + Copy, + Clone, + Hash, + PartialOrd, + Ord, + Serialize, + Deserialize, + Drive, + DriveMut, +)] #[serde(transparent)] pub struct DeBruijnId { pub index: usize, @@ -73,6 +89,8 @@ pub struct DeBruijnId { EnumAsGetters, Serialize, Deserialize, + Drive, + DriveMut, )] pub enum Region { /// Static region @@ -113,7 +131,9 @@ pub enum Region { /// definition. Note that every path designated by [TraitInstanceId] refers /// to a *trait instance*, which is why the [Clause] variant may seem redundant /// with some of the other variants. -#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Ord, PartialOrd)] +#[derive( + Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Ord, PartialOrd, Drive, DriveMut, +)] pub enum TraitInstanceId { /// /// A specific implementation @@ -202,24 +222,19 @@ pub enum TraitInstanceId { /// is useful to give priority to the local clauses when solving the trait /// obligations which are fullfilled by the trait parameters. SelfId, - /// Clause which hasn't been solved yet. - /// This happens when we register clauses in the context: solving some - /// trait obligations/references might require to refer to clauses which - /// haven't been registered yet. This variant is purely internal: after we - /// finished solving the trait obligations, all the remaining unsolved - /// clauses (in case we don't fail hard on error) are converted to [Unknown]. - Unsolved(TraitDeclId, GenericArgs), /// For error reporting. - /// Can appear only if the option [CliOpts::continue_on_failure] is used. Unknown(String), } /// A reference to a trait -#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Ord, PartialOrd)] +#[derive( + Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Ord, PartialOrd, Drive, DriveMut, +)] pub struct TraitRef { pub trait_id: TraitInstanceId, pub generics: GenericArgs, /// Not necessary, but useful + #[drive(skip)] pub trait_decl_ref: TraitDeclRef, } @@ -231,7 +246,9 @@ pub struct TraitRef { /// ``` /// /// The substitution is: `[String, bool]`. -#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Ord, PartialOrd)] +#[derive( + Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Ord, PartialOrd, Drive, DriveMut, +)] pub struct TraitDeclRef { pub trait_id: TraitDeclId, pub generics: GenericArgs, @@ -241,6 +258,24 @@ pub struct TraitDeclRef { #[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)] pub struct OutlivesPred(pub T, pub U); +// The derive macro doesn't handle generics well. +impl Drive for OutlivesPred { + fn drive(&self, visitor: &mut V) { + visitor.visit(self, Event::Enter); + self.0.drive(visitor); + self.1.drive(visitor); + visitor.visit(self, Event::Exit); + } +} +impl DriveMut for OutlivesPred { + fn drive_mut(&mut self, visitor: &mut V) { + visitor.visit(self, Event::Enter); + self.0.drive_mut(visitor); + self.1.drive_mut(visitor); + visitor.visit(self, Event::Exit); + } +} + pub type RegionOutlives = OutlivesPred; pub type TypeOutlives = OutlivesPred; @@ -251,25 +286,16 @@ pub type TypeOutlives = OutlivesPred; /// T : Foo /// ^^^^^^^^^^ /// ``` -#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)] +#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Drive, DriveMut)] pub struct TraitTypeConstraint { pub trait_ref: TraitRef, pub type_name: TraitItemName, pub ty: Ty, } -/// The predicates which apply to a definition -#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)] -pub struct Predicates { - /// The first region in the pair outlives the second region - pub regions_outlive: Vec, - /// The type outlives the region - pub types_outlive: Vec, - /// Constraints over trait associated types - pub trait_type_constraints: Vec, -} - -#[derive(Debug, Clone, Eq, PartialEq, Serialize, Deserialize, Hash, Ord, PartialOrd)] +#[derive( + Debug, Clone, Eq, PartialEq, Serialize, Deserialize, Hash, Ord, PartialOrd, Drive, DriveMut, +)] pub struct GenericArgs { pub regions: Vec, pub types: Vec, @@ -285,20 +311,27 @@ pub struct GenericArgs { /// be filled. We group in a different place the predicates which are not /// trait clauses, because those enforce constraints but do not need to /// be filled with witnesses/instances. -#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[derive(Debug, Default, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] pub struct GenericParams { pub regions: Vector, pub types: Vector, pub const_generics: Vector, // TODO: rename to match [GenericArgs]? pub trait_clauses: Vector, + /// The first region in the pair outlives the second region + pub regions_outlive: Vec, + /// The type outlives the region + pub types_outlive: Vec, + /// Constraints over trait associated types + pub trait_type_constraints: Vec, } generate_index_type!(TraitClauseId, "TraitClause"); generate_index_type!(TraitDeclId, "TraitDecl"); generate_index_type!(TraitImplId, "TraitImpl"); -#[derive(Debug, Clone, Serialize, Deserialize, Derivative)] +/// A predicate of the form `Type: Trait`. +#[derive(Debug, Clone, Serialize, Deserialize, Derivative, Drive, DriveMut)] #[derivative(PartialEq)] pub struct TraitClause { /// We use this id when solving trait constraints, to be able to refer @@ -307,13 +340,62 @@ pub struct TraitClause { pub clause_id: TraitClauseId, #[derivative(PartialEq = "ignore")] pub span: Option, + /// Where the predicate was written, relative to the item that requires it. + #[derivative(PartialEq = "ignore")] + pub origin: PredicateOrigin, + /// The trait that is implemented. pub trait_id: TraitDeclId, + /// The generics applied to the trait. Note: this includes the `Self` type. /// Remark: the trait refs list in the [generics] field should be empty. pub generics: GenericArgs, } impl Eq for TraitClause {} +/// Where a given predicate came from. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Derivative, Drive, DriveMut)] +pub enum PredicateOrigin { + // Note: we use this for globals too, but that's only available with an unstable feature. + // ``` + // fn function() {} + // fn function() where T: Clone {} + // const NONE: Option = None; + // ``` + WhereClauseOnFn, + // ``` + // struct Struct {} + // struct Struct where T: Clone {} + // type TypeAlias = ...; + // ``` + WhereClauseOnType, + // Note: this is both trait impls and inherent impl blocks. + // ``` + // impl Type {} + // impl Type where T: Clone {} + // impl Trait for Type where T: Clone {} + // ``` + WhereClauseOnImpl, + // The special `Self: Trait` clause which is in scope inside the definition of `Foo` or an + // implementation of it. + // ``` + // trait Trait {} + // ``` + TraitSelf, + // Note: this also includes supertrait constraings. + // ``` + // trait Trait {} + // trait Trait where T: Clone {} + // trait Trait: Clone {} + // ``` + WhereClauseOnTrait, + // ``` + // trait Trait { + // type AssocType: Clone; + // } + // ``` + TraitItem(TraitItemName), +} + /// A type declaration. /// /// Types can be opaque or transparent. @@ -327,8 +409,9 @@ impl Eq for TraitClause {} /// /// A type can only be an ADT (structure or enumeration), as type aliases are /// inlined in MIR. -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct TypeDecl { + #[drive(skip)] pub def_id: TypeDeclId, /// Meta information associated with the type. pub item_meta: ItemMeta, @@ -337,12 +420,11 @@ pub struct TypeDecl { pub is_local: bool, pub name: Name, pub generics: GenericParams, - pub preds: Predicates, /// The type kind: enum, struct, or opaque. pub kind: TypeDeclKind, } -#[derive(Debug, Clone, EnumIsA, EnumAsGetters, Serialize, Deserialize)] +#[derive(Debug, Clone, EnumIsA, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut)] pub enum TypeDeclKind { Struct(Vector), Enum(Vector), @@ -358,9 +440,9 @@ pub enum TypeDeclKind { Error(String), } -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Variant { - pub span: Span, + pub item_meta: ItemMeta, pub name: String, pub fields: Vector, /// The discriminant used at runtime. This is used in `remove_read_discriminant` to match up @@ -368,9 +450,10 @@ pub struct Variant { pub discriminant: ScalarValue, } -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Field { - pub span: Span, + /// FIXME: define a more appropriate container for attribute and visibility information. + pub item_meta: ItemMeta, pub name: Option, pub ty: Ty, } @@ -385,6 +468,8 @@ pub struct Field { VariantName, Serialize, Deserialize, + Drive, + DriveMut, Hash, Ord, PartialOrd, @@ -415,6 +500,8 @@ pub enum IntegerTy { EnumIsA, Serialize, Deserialize, + Drive, + DriveMut, Ord, PartialOrd, )] @@ -437,6 +524,8 @@ pub enum RefKind { EnumIsA, Serialize, Deserialize, + Drive, + DriveMut, Hash, Ord, PartialOrd, @@ -471,6 +560,8 @@ pub enum TypeId { VariantIndexArity, Serialize, Deserialize, + Drive, + DriveMut, Hash, Ord, PartialOrd, @@ -493,6 +584,8 @@ pub enum LiteralTy { VariantIndexArity, Serialize, Deserialize, + Drive, + DriveMut, Hash, Ord, PartialOrd, @@ -520,6 +613,8 @@ pub enum ConstGeneric { VariantIndexArity, Serialize, Deserialize, + Drive, + DriveMut, Ord, PartialOrd, )] @@ -592,6 +687,8 @@ pub enum Ty { VariantName, Serialize, Deserialize, + Drive, + DriveMut, Hash, Ord, PartialOrd, @@ -654,7 +751,7 @@ pub enum AssumedTy { /// outer block. For this reason, when we need to store the information about /// the generics of the outer block(s), we need to do it only for one level /// (this definitely makes things simpler). -#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] pub struct ParamsInfo { pub num_region_params: usize, pub num_type_params: usize, @@ -665,7 +762,7 @@ pub struct ParamsInfo { pub num_trait_type_constraints: usize, } -#[derive(Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[derive(Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] pub enum ClosureKind { Fn, FnMut, @@ -674,7 +771,7 @@ pub enum ClosureKind { /// Additional information for closures. /// We mostly use it in micro-passes like [crate::update_closure_signature]. -#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] pub struct ClosureInfo { pub kind: ClosureKind, /// Contains the types of the fields in the closure state. @@ -692,7 +789,7 @@ pub struct ClosureInfo { } /// A function signature. -#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] pub struct FunSig { /// Is the function unsafe or not pub is_unsafe: bool, @@ -706,7 +803,6 @@ pub struct FunSig { /// Additional information if this is the signature of a closure. pub closure_info: Option, pub generics: GenericParams, - pub preds: Predicates, /// Optional fields, for trait methods only (see the comments in [ParamsInfo]). pub parent_params_info: Option, pub inputs: Vec, diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index d806b8da9..27c16ff8e 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -1,10 +1,8 @@ //! This file groups everything which is linked to implementations about [crate::types] use crate::ids::Vector; use crate::types::*; -use crate::values::*; use hax_frontend_exporter as hax; use im::HashMap; -use macros::make_generic_in_borrows; use std::iter::Iterator; impl DeBruijnId { @@ -36,8 +34,17 @@ impl GenericParams { types, const_generics, trait_clauses, + regions_outlive, + types_outlive, + trait_type_constraints, } = self; - regions.len() + types.len() + const_generics.len() + trait_clauses.len() + regions.len() + + types.len() + + const_generics.len() + + trait_clauses.len() + + regions_outlive.len() + + types_outlive.len() + + trait_type_constraints.len() } pub fn is_empty(&self) -> bool { @@ -45,23 +52,7 @@ impl GenericParams { } pub fn empty() -> Self { - GenericParams { - regions: Vector::new(), - types: Vector::new(), - const_generics: Vector::new(), - trait_clauses: Vector::new(), - } - } -} - -impl Predicates { - pub fn is_empty(&self) -> bool { - let Predicates { - regions_outlive, - types_outlive, - trait_type_constraints, - } = self; - regions_outlive.is_empty() && types_outlive.is_empty() && trait_type_constraints.is_empty() + Self::default() } } @@ -473,312 +464,3 @@ impl TySubst { Ok(s) } } - -/// Visitor to replace the [TraitInstanceId::SelfId] inside a type -struct TraitInstanceIdSelfReplacer { - new_id: TraitInstanceId, -} - -impl MutTypeVisitor for TraitInstanceIdSelfReplacer { - fn visit_trait_instance_id(&mut self, id: &mut TraitInstanceId) { - match id { - TraitInstanceId::SelfId => *id = self.new_id.clone(), - TraitInstanceId::ParentClause(box id, _, _) - | TraitInstanceId::ItemClause(box id, _, _, _) => self.visit_trait_instance_id(id), - TraitInstanceId::TraitImpl(_) - | TraitInstanceId::Clause(_) - | TraitInstanceId::BuiltinOrAuto(_) - | TraitInstanceId::Unsolved(..) - | TraitInstanceId::Unknown(_) => (), - } - } -} - -// Derive two implementations at once: one which uses shared borrows, and one -// which uses mutable borrows. -// Generates the traits: `SharedTypeVisitor` and `MutTypeVisitor`. -make_generic_in_borrows! { - -// TODO: we should use traits with default implementations to allow overriding -// the default behavior (that would also prevent problems with naming collisions) -pub trait TypeVisitor { - fn default_enter_region_group(&mut self, regions: &Vector, visitor: &mut dyn FnMut(&mut Self)) { - visitor(self) - } - - fn enter_region_group(&mut self, regions: &Vector, visitor: &mut dyn FnMut(&mut Self)) { - self.default_enter_region_group(regions, visitor) - } - - fn visit_ty(&mut self, ty: &Ty) { - self.default_visit_ty(ty) - } - - fn default_visit_ty(&mut self, ty: &Ty) { - use Ty::*; - match ty { - Adt(id, args) => self.visit_ty_adt(id, args), - TypeVar(vid) => self.visit_ty_type_var(vid), - Literal(lit) => self.visit_ty_literal(lit), - Never => self.visit_ty_never(), - Ref(r, ty, rk) => self.visit_ty_ref(r, ty, rk), - RawPtr(ty, rk) => self.visit_ty_raw_ptr(ty, rk), - TraitType(trait_ref, _name) => { - self.visit_trait_ref(trait_ref); - } - Arrow(regions, inputs, box output) => self.visit_arrow(regions, inputs, output), - } - } - - fn visit_region(&mut self, r: &Region) { - match r { - Region::Erased | Region::Static | Region::Unknown => (), - Region::BVar(grid, id) => { - self.visit_region_bvar(grid, id) - }, - } - } - - fn visit_region_bvar(&mut self, _grid: &DeBruijnId, _rid: &RegionId) {} - - fn visit_arrow(&mut self, regions: &Vector, inputs: &Vec, output: &Ty) { - for r in regions.iter() { - self.visit_region_var(r); - } - - let regions = &(*regions); - let inputs = &(*inputs); - let output = &(*output); - self.enter_region_group(regions, &mut |ctx| { - for ty in inputs.iter() { - ctx.visit_ty(ty); - } - ctx.visit_ty(output); - }); - } - - fn visit_ty_adt( - &mut self, - id: &TypeId, - args: &GenericArgs, - ) { - self.visit_type_id(id); - self.visit_generic_args(args); - } - - fn visit_region_var(&mut self, r: &RegionVar) {} - - fn visit_ty_type_var(&mut self, vid: &TypeVarId) { - self.visit_type_var_id(vid); - } - - fn visit_ty_literal(&mut self, ty: &LiteralTy) {} - - fn visit_ty_never(&mut self) {} - - fn visit_ty_ref(&mut self, r: &Region, ty: &Box, _rk: &RefKind) { - self.visit_region(r); - self.visit_ty(ty); - } - - fn visit_ty_raw_ptr(&mut self, ty: &Box, _rk: &RefKind) { - self.visit_ty(ty); - } - - fn visit_type_id(&mut self, id: &TypeId) { - use TypeId::*; - match id { - Adt(id) => self.visit_type_decl_id(id), - Tuple => (), - Assumed(aty) => self.visit_assumed_ty(aty), - } - } - - fn visit_type_decl_id(&mut self, _: &TypeDeclId) {} - - fn visit_assumed_ty(&mut self, _: &AssumedTy) {} - - fn visit_const_generic(&mut self, cg: &ConstGeneric) { - use ConstGeneric::*; - match cg { - Global(id) => self.visit_global_decl_id(id), - Var(id) => self.visit_const_generic_var_id(id), - Value(lit) => self.visit_literal(lit), - } - } - - fn visit_type_var(&mut self, ty: &TypeVar) { - self.visit_type_var_id(&ty.index); - // Ignoring the name - } - - fn visit_const_generic_var(&mut self, cg: &ConstGenericVar) { - self.visit_const_generic_var_id(&cg.index); - // Ignoring the name and type - } - - fn visit_global_decl_id(&mut self, _: &GlobalDeclId) {} - fn visit_type_var_id(&mut self, _: &TypeVarId) {} - fn visit_const_generic_var_id(&mut self, _: &ConstGenericVarId) {} - - fn visit_literal(&mut self, _: &Literal) {} - - fn visit_trait_ref(&mut self, tr: &TraitRef) { - let TraitRef { - trait_id, - generics, - trait_decl_ref, - } = tr; - self.visit_trait_instance_id(trait_id); - self.visit_generic_args(generics); - self.visit_trait_decl_ref(trait_decl_ref); - } - - fn visit_trait_decl_ref(&mut self, tr: &TraitDeclRef) { - let TraitDeclRef { - trait_id, - generics, - } = tr; - self.visit_trait_decl_id(trait_id); - self.visit_generic_args(generics); - } - - fn visit_trait_decl_id(&mut self, _: &TraitDeclId) {} - fn visit_trait_impl_id(&mut self, _: &TraitImplId) {} - fn visit_trait_clause_id(&mut self, _: &TraitClauseId) {} - - fn default_visit_trait_instance_id(&mut self, id: &TraitInstanceId) { - match id { - TraitInstanceId::SelfId => (), - TraitInstanceId::TraitImpl(id) => self.visit_trait_impl_id(id), - TraitInstanceId::BuiltinOrAuto(id) => self.visit_trait_decl_id(id), - TraitInstanceId::Clause(id) => self.visit_trait_clause_id(id), - TraitInstanceId::ParentClause(box id, decl_id, clause_id) => { - self.visit_trait_instance_id(id); - self.visit_trait_decl_id(decl_id); - self.visit_trait_clause_id(clause_id) - }, - TraitInstanceId::ItemClause(box id, decl_id, _name, clause_id) => { - self.visit_trait_instance_id(id); - self.visit_trait_decl_id(decl_id); - self.visit_trait_clause_id(clause_id) - }, - TraitInstanceId::Unsolved(trait_id, generics) => { - self.visit_trait_decl_id(trait_id); - self.visit_generic_args(generics); - }, - TraitInstanceId::Unknown(_) => (), - } - } - - fn visit_trait_instance_id(&mut self, id: &TraitInstanceId) { - self.default_visit_trait_instance_id(id) - } - - fn visit_generic_args(&mut self, g: &GenericArgs) { - for r in &g.regions { - self.visit_region(r) - } - for t in &g.types { - self.visit_ty(t); - } - for cg in &g.const_generics { - self.visit_const_generic(cg); - } - for t in &g.trait_refs { - self.visit_trait_ref(t); - } - } - - fn visit_generic_params(&mut self, g: &GenericParams) { - for r in g.regions.iter() { - self.visit_region_var(r) - } - for t in g.types.iter() { - self.visit_type_var(t); - } - for cg in g.const_generics.iter() { - self.visit_const_generic_var(cg); - } - for t in g.trait_clauses.iter() { - self.visit_trait_clause(t); - } - } - - fn visit_trait_clause(&mut self, c: &TraitClause) { - let TraitClause { clause_id, span: _, trait_id, generics } = c; - self.visit_trait_clause_id(clause_id); - self.visit_trait_decl_id(trait_id); - self.visit_generic_args(generics); - } - - fn visit_predicates(&mut self, preds: &Predicates) { - let Predicates { - regions_outlive, - types_outlive, - trait_type_constraints, - } = preds; - for p in regions_outlive { - self.visit_region(&p.0); - self.visit_region(&p.1); - } - for p in types_outlive { - self.visit_ty(&p.0); - self.visit_region(&p.1); - } - for TraitTypeConstraint { - trait_ref, - type_name: _, - ty, - } in trait_type_constraints - { - self.visit_trait_ref(trait_ref); - self.visit_ty(ty); - } - } - - fn visit_fun_sig(&mut self, sig: &FunSig) { - let FunSig { - is_unsafe : _, - is_closure: _, - closure_info, - generics, - preds, - parent_params_info: _, - inputs, - output, - } = sig; - - if let Some(info) = closure_info { - self.visit_closure_info(info); - } - - self.visit_generic_params(generics); - self.visit_predicates(preds); - for ty in inputs { self.visit_ty(ty); } - self.visit_ty(output); - } - - fn visit_closure_info(&mut self, info: &ClosureInfo) { - let ClosureInfo { - kind: _, - state, - } = info; - - for ty in state { self.visit_ty(ty); } - } - - fn visit_type_outlives(&mut self, x: &TypeOutlives) { - self.visit_ty(&x.0); - } - - fn visit_trait_type_constraint(&mut self, x : &TraitTypeConstraint) { - let TraitTypeConstraint { trait_ref, type_name: _, ty } = x; - self.visit_trait_ref(trait_ref); - self.visit_ty(ty); - } - - fn visit_fun_decl_id(&mut self, _: &FunDeclId) {} -} - -} // make_generic_in_borrows diff --git a/charon/src/ast/ullbc_ast.rs b/charon/src/ast/ullbc_ast.rs index 4370e7e76..1fc63312c 100644 --- a/charon/src/ast/ullbc_ast.rs +++ b/charon/src/ast/ullbc_ast.rs @@ -7,6 +7,7 @@ pub use crate::types::GlobalDeclId; use crate::types::*; pub use crate::ullbc_ast_utils::*; use crate::values::*; +use derive_visitor::{Drive, DriveMut}; use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName}; use serde::{Deserialize, Serialize}; @@ -20,7 +21,9 @@ pub type BodyContents = Vector; pub type ExprBody = GExprBody; /// A raw statement: a statement without meta data. -#[derive(Debug, Clone, EnumIsA, EnumAsGetters, VariantName, Serialize, Deserialize)] +#[derive( + Debug, Clone, EnumIsA, EnumAsGetters, VariantName, Serialize, Deserialize, Drive, DriveMut, +)] pub enum RawStatement { Assign(Place, Rvalue), FakeRead(Place), @@ -32,14 +35,23 @@ pub enum RawStatement { Error(String), } -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Statement { pub span: Span, pub content: RawStatement, } #[derive( - Debug, Clone, EnumIsA, EnumAsGetters, VariantName, VariantIndexArity, Serialize, Deserialize, + Debug, + Clone, + EnumIsA, + EnumAsGetters, + VariantName, + VariantIndexArity, + Serialize, + Deserialize, + Drive, + DriveMut, )] pub enum SwitchTargets { /// Gives the `if` block and the `else` block @@ -51,7 +63,7 @@ pub enum SwitchTargets { } /// A raw terminator: a terminator without meta data. -#[derive(Debug, Clone, EnumIsA, EnumAsGetters, Serialize, Deserialize)] +#[derive(Debug, Clone, EnumIsA, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut)] pub enum RawTerminator { Goto { target: BlockId, @@ -82,13 +94,13 @@ pub enum RawTerminator { }, } -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Terminator { pub span: Span, pub content: RawTerminator, } -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct BlockData { pub statements: Vec, pub terminator: Terminator, diff --git a/charon/src/ast/ullbc_ast_utils.rs b/charon/src/ast/ullbc_ast_utils.rs index 0893961be..f1e47f747 100644 --- a/charon/src/ast/ullbc_ast_utils.rs +++ b/charon/src/ast/ullbc_ast_utils.rs @@ -1,10 +1,7 @@ //! Implementations for [crate::ullbc_ast] use crate::ids::Vector; use crate::meta::Span; -use crate::types::*; use crate::ullbc_ast::*; -use crate::values::*; -use macros::make_generic_in_borrows; use take_mut::take; impl SwitchTargets { @@ -144,167 +141,3 @@ pub fn body_transform_operands, &mut Operand take(block, |b| b.transform_operands(f)); } } - -// Derive two implementations at once: one which uses shared borrows, and one -// which uses mutable borrows. -// Generates the traits: `SharedAstVisitor` and `MutAstVisitor`. -make_generic_in_borrows! { - -/// A visitor for the ULLBC AST -/// -/// Remark: we can't call the "super" method when reimplementing a method -/// (unlike what can be done in, say, OCaml). This makes imlementing visitors -/// slightly awkward, and is the reason why we split some visit functions in two: -/// a "standard" version to be overriden, and a "default" version which should -/// not be overriden and gives access to the "super" method. -/// -/// TODO: implement macros to automatically derive visitors. -pub trait AstVisitor: crate::expressions::ExprVisitor { - fn visit_block_data(&mut self, block: &BlockData) { - for st in &block.statements { - self.visit_statement(st); - } - self.visit_terminator(&block.terminator); - } - - fn visit_statement(&mut self, st: &Statement) { - self.visit_span(&st.span); - self.visit_raw_statement(&st.content); - } - - fn visit_raw_statement(&mut self, st: &RawStatement) { - self.default_visit_raw_statement(st); - } - - fn default_visit_raw_statement(&mut self, st: &RawStatement) { - use RawStatement::*; - match st { - Assign(p, rv) => self.visit_assign(p, rv), - FakeRead(p) => self.visit_fake_read(p), - SetDiscriminant(p, vid) => self.visit_set_discriminant(p, vid), - StorageDead(vid) => self.visit_storage_dead(vid), - Deinit(p) => self.visit_deinit(p), - Error(s) => self.visit_error(s), - } - } - - fn visit_assign(&mut self, p: &Place, rv: &Rvalue) { - self.visit_place(p); - self.visit_rvalue(rv); - } - - fn visit_fake_read(&mut self, p: &Place) { - self.visit_place(p); - } - - fn visit_set_discriminant(&mut self, p: &Place, _vid: &VariantId) { - self.visit_place(p); - } - - fn visit_storage_dead(&mut self, vid: &VarId) { - self.visit_var_id(vid); - } - - fn visit_deinit(&mut self, p: &Place) { - self.visit_place(p); - } - - fn visit_error(&mut self, s: &String) {} - - fn visit_terminator(&mut self, st: &Terminator) { - self.visit_span(&st.span); - self.visit_raw_terminator(&st.content); - } - - fn visit_span(&mut self, st: &Span) {} - - fn default_visit_raw_terminator(&mut self, st: &RawTerminator) { - use RawTerminator::*; - match st { - Goto { target } => self.visit_goto(target), - Switch { discr, targets } => { - self.visit_switch(discr, targets); - } - Abort(..) => self.visit_abort(), - Return => self.visit_return(), - Drop { place, target } => { - self.visit_drop(place, target); - } - Call { call, target } => { - self.visit_call_statement(call, target); - } - Assert { - cond, - expected, - target, - } => { - self.visit_assert(cond, expected, target); - } - } - } - - fn visit_raw_terminator(&mut self, st: &RawTerminator) { - self.default_visit_raw_terminator(st); - } - - fn visit_goto(&mut self, target: &BlockId) { - self.visit_block_id(target) - } - - fn visit_switch(&mut self, discr: &Operand, targets: &SwitchTargets) { - self.visit_operand(discr); - self.visit_switch_targets(targets); - } - - fn visit_abort(&mut self) {} - - fn visit_return(&mut self) {} - - fn visit_drop(&mut self, place: &Place, target: &BlockId) { - self.visit_place(place); - self.visit_block_id(target); - } - - fn visit_call_statement(&mut self, call: &Call, target: &Option) { - self.visit_call(call); - if let Some(target) = target { - self.visit_block_id(target); - } - } - - fn visit_assert(&mut self, cond: &Operand, expected: &bool, target: &BlockId) { - self.visit_operand(cond); - self.visit_block_id(target); - } - - fn visit_block_id(&mut self, id: &BlockId) {} - - fn visit_switch_targets(&mut self, targets: &SwitchTargets) { - use SwitchTargets::*; - match targets { - If(then_id, else_id) => self.visit_if(then_id, else_id), - SwitchInt(int_ty, branches, otherwise) => { - self.visit_switch_int(int_ty, branches, otherwise) - } - } - } - - fn visit_if(&mut self, then_id: &BlockId, else_id: &BlockId) { - self.visit_block_id(then_id); - self.visit_block_id(else_id); - } - - fn visit_switch_int( - &mut self, - int_ty: &IntegerTy, - branches: &Vec<(ScalarValue, BlockId)>, - otherwise: &BlockId, - ) { - for (_, br) in branches { - self.visit_block_id(br); - } - self.visit_block_id(otherwise); - } -} - -} // make_generic_in_borrows diff --git a/charon/src/ast/values.rs b/charon/src/ast/values.rs index 99ae0d629..4d91d2e59 100644 --- a/charon/src/ast/values.rs +++ b/charon/src/ast/values.rs @@ -2,6 +2,7 @@ pub use crate::values_utils::*; use core::hash::Hash; +use derive_visitor::{Drive, DriveMut}; use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName}; use serde::{Deserialize, Serialize}; @@ -26,6 +27,8 @@ generate_index_type!(VarId, ""); EnumAsGetters, Serialize, Deserialize, + Drive, + DriveMut, Hash, PartialOrd, Ord, @@ -59,6 +62,8 @@ pub enum Literal { Hash, PartialOrd, Ord, + Drive, + DriveMut, )] pub enum ScalarValue { /// Using i64 to be safe diff --git a/charon/src/bin/charon-driver/main.rs b/charon/src/bin/charon-driver/main.rs index 020aabc41..14add4a86 100644 --- a/charon/src/bin/charon-driver/main.rs +++ b/charon/src/bin/charon-driver/main.rs @@ -174,7 +174,7 @@ fn main() { } } - for extra_flag in options.rustc_flags.iter().cloned() { + for extra_flag in options.rustc_args.iter().cloned() { compiler_args.push(extra_flag); } diff --git a/charon/src/bin/charon/main.rs b/charon/src/bin/charon/main.rs index cc7a87493..77a48bb6b 100644 --- a/charon/src/bin/charon/main.rs +++ b/charon/src/bin/charon/main.rs @@ -176,6 +176,10 @@ pub fn main() -> anyhow::Result<()> { let host = &rustc_version.host; let exit_status = if options.no_cargo { + if !options.cargo_args.is_empty() { + bail!("Option `--cargo-arg` is not compatible with `--no-cargo`") + } + // Run just the driver. let mut cmd = driver_cmd()?; @@ -231,6 +235,10 @@ pub fn main() -> anyhow::Result<()> { cmd.arg(options.bin.as_ref().unwrap().clone()); } + for arg in &options.cargo_args { + cmd.arg(arg); + } + cmd.spawn() .expect("could not run cargo") .wait() diff --git a/charon/src/bin/charon/toml_config.rs b/charon/src/bin/charon/toml_config.rs index c063e715e..8c0ef03ef 100644 --- a/charon/src/bin/charon/toml_config.rs +++ b/charon/src/bin/charon/toml_config.rs @@ -53,7 +53,7 @@ impl TomlConfig { config.no_code_duplication |= self.charon.no_code_duplication; config.opaque_modules.extend(self.charon.opaque_modules); config.extract_opaque_bodies |= self.charon.extract_opaque_bodies; - config.rustc_flags.extend(self.rustc.flags); + config.rustc_args.extend(self.rustc.flags); config } } diff --git a/charon/src/cli_options.rs b/charon/src/cli_options.rs index 741ec8ba9..2055367ff 100644 --- a/charon/src/cli_options.rs +++ b/charon/src/cli_options.rs @@ -125,9 +125,13 @@ performs: `y := (x as E2).1`). Producing a better reconstruction is non-trivial. #[serde(default)] pub no_cargo: bool, /// Extra flags to pass to rustc. - #[clap(long = "rustc-flag")] + #[clap(long = "rustc-flag", alias = "rustc-arg")] #[serde(default)] - pub rustc_flags: Vec, + pub rustc_args: Vec, + /// Extra flags to pass to cargo. Incompatible with `--no-cargo`. + #[clap(long = "cargo-arg")] + #[serde(default)] + pub cargo_args: Vec, /// Panic on the first error. This is useful for debugging. #[clap(long = "abort-on-error")] #[serde(default)] diff --git a/charon/src/ids/mod.rs b/charon/src/ids/mod.rs index 631b3e81f..a1e893a70 100644 --- a/charon/src/ids/mod.rs +++ b/charon/src/ids/mod.rs @@ -18,6 +18,7 @@ macro_rules! generate_index_type { }; ($name:ident, $pretty_name:expr) => { index_vec::define_index_type! { + #[derive(derive_visitor::Drive, derive_visitor::DriveMut)] pub struct $name = usize; // Must fit in an u32 for serialization. MAX_INDEX = std::u32::MAX as usize; diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs index 252ccd2f1..b4e5606ad 100644 --- a/charon/src/ids/vector.rs +++ b/charon/src/ids/vector.rs @@ -7,6 +7,7 @@ //! Note that this data structure is implemented by using persistent vectors. //! This makes the clone operation almost a no-op. +use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut}; use index_vec::{Idx, IdxSliceIndex, IndexVec}; use serde::{Deserialize, Serialize, Serializer}; use std::{ @@ -240,3 +241,22 @@ impl<'de, I: Idx, T: Deserialize<'de>> Deserialize<'de> for Vector { }) } } + +impl Drive for Vector { + fn drive(&self, visitor: &mut V) { + visitor.visit(self, Event::Enter); + for x in self { + x.drive(visitor); + } + visitor.visit(self, Event::Exit); + } +} +impl DriveMut for Vector { + fn drive_mut(&mut self, visitor: &mut V) { + visitor.visit(self, Event::Enter); + for x in &mut *self { + x.drive_mut(visitor); + } + visitor.visit(self, Event::Exit); + } +} diff --git a/charon/src/lib.rs b/charon/src/lib.rs index 988cb9d01..35a862b97 100644 --- a/charon/src/lib.rs +++ b/charon/src/lib.rs @@ -18,6 +18,7 @@ #![feature(trait_alias)] #![feature(let_chains)] #![feature(if_let_guard)] +#![feature(iter_array_chunks)] #![feature(impl_trait_in_assoc_type)] #![feature(iterator_try_collect)] diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index e47d5f806..2ffa17f36 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -6,6 +6,7 @@ use crate::{ gast, ids::Vector, llbc_ast::{self as llbc, *}, + meta::*, names::*, reorder_decls::*, translate_predicates::NonLocalTraitClause, @@ -14,6 +15,7 @@ use crate::{ values::*, }; use hax_frontend_exporter as hax; +use itertools::Itertools; /// Format the AST type as a string. pub trait FmtWithCtx { @@ -128,6 +130,7 @@ impl FmtWithCtx for DeclarationGroup { Global(g) => format!("Global decls group: {}", g.fmt_with_ctx(ctx)), TraitDecl(g) => format!("Trait decls group: {}", g.fmt_with_ctx(ctx)), TraitImpl(g) => format!("Trait impls group: {}", g.fmt_with_ctx(ctx)), + Mixed(g) => format!("Mixed group: {}", g.fmt_with_ctx(ctx)), } } } @@ -180,7 +183,9 @@ impl FmtWithCtx for FunSig { }; // Generic parameters - let (params, trait_clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx); + let (params, clauses, _) = + self.generics + .fmt_with_ctx_with_trait_clauses(ctx, "", &self.parent_params_info); // Arguments let mut args: Vec = Vec::new(); @@ -197,15 +202,6 @@ impl FmtWithCtx for FunSig { format!(" -> {}", ret_ty.fmt_with_ctx(ctx)) }; - // Clauses - let clauses = fmt_where_clauses_with_ctx( - ctx, - "", - &self.parent_params_info, - trait_clauses, - &self.preds, - ); - // Put everything together format!("{unsafe_kw}fn{params}({args}){ret_ty}{clauses}",) } @@ -305,24 +301,24 @@ impl FmtWithCtx for GenericArgs { } impl GenericParams { - pub fn fmt_with_ctx_with_trait_clauses(&self, ctx: &C) -> (String, Vec) + pub fn fmt_with_ctx_with_trait_clauses( + &self, + ctx: &C, + tab: &str, + info: &Option, + ) -> (String, String, bool) where C: AstFormatter, { + let generics = self; let mut params = Vec::new(); - let GenericParams { - regions, - types, - const_generics, - trait_clauses, - } = self; - for x in regions { + for x in &generics.regions { params.push(x.to_string()); } - for x in types { + for x in &generics.types { params.push(x.to_string()); } - for x in const_generics { + for x in &generics.const_generics { params.push(x.to_string()); } let params = if params.is_empty() { @@ -331,11 +327,63 @@ impl GenericParams { format!("<{}>", params.join(", ")) }; - let mut clauses = Vec::new(); - for x in trait_clauses { - clauses.push(x.fmt_with_ctx(ctx)); - } - (params, clauses) + let mut trait_clauses = generics + .trait_clauses + .iter() + .map(|x| x.fmt_with_ctx(ctx)) + .collect_vec(); + let mut types_outlive: Vec<_> = generics + .types_outlive + .iter() + .map(|OutlivesPred(x, y)| format!("{} : {}", x.fmt_with_ctx(ctx), y.fmt_with_ctx(ctx))) + .collect(); + let mut regions_outlive: Vec<_> = generics + .regions_outlive + .iter() + .map(|OutlivesPred(x, y)| format!("{} : {}", x.fmt_with_ctx(ctx), y.fmt_with_ctx(ctx))) + .collect(); + let mut type_constraints: Vec<_> = generics + .trait_type_constraints + .iter() + .map(|x| x.fmt_with_ctx(ctx)) + .collect(); + let any_where = !(trait_clauses.is_empty() + && types_outlive.is_empty() + && regions_outlive.is_empty() + && type_constraints.is_empty()); + let preds = match info { + None => { + let clauses: Vec<_> = trait_clauses + .into_iter() + .chain(types_outlive.into_iter()) + .chain(regions_outlive.into_iter()) + .chain(type_constraints.into_iter()) + .collect(); + fmt_where_clauses(tab, 0, clauses) + } + Some(info) => { + // Below: definitely not efficient nor convenient, but it is not really + // important + let local_clauses: Vec<_> = trait_clauses + .split_off(info.num_trait_clauses) + .into_iter() + .chain(regions_outlive.split_off(info.num_regions_outlive)) + .chain(types_outlive.split_off(info.num_types_outlive)) + .chain(type_constraints.split_off(info.num_trait_type_constraints)) + .collect(); + let inherited_clauses: Vec<_> = trait_clauses + .into_iter() + .chain(regions_outlive) + .chain(types_outlive) + .chain(type_constraints) + .collect(); + let num_inherited = inherited_clauses.len(); + let all_clauses: Vec<_> = + inherited_clauses.into_iter().chain(local_clauses).collect(); + fmt_where_clauses(tab, num_inherited, all_clauses) + } + }; + (params, preds, any_where) } } @@ -350,6 +398,9 @@ impl FmtWithCtx for GenericParams { types, const_generics, trait_clauses, + regions_outlive: _, + types_outlive: _, + trait_type_constraints: _, } = self; for x in regions { params.push(x.to_string()); @@ -451,7 +502,11 @@ where let name = self.name.fmt_with_ctx(ctx); // Generic parameters - let (params, trait_clauses) = self.signature.generics.fmt_with_ctx_with_trait_clauses(ctx); + let (params, preds, _) = self.signature.generics.fmt_with_ctx_with_trait_clauses( + ctx, + tab, + &self.signature.parent_params_info, + ); // Arguments let mut args: Vec = Vec::new(); @@ -473,15 +528,6 @@ where format!(" -> {}", ret_ty.fmt_with_ctx(ctx)) }; - // Predicates - let preds = fmt_where_clauses_with_ctx( - ctx, - tab, - &self.signature.parent_params_info, - trait_clauses, - &self.signature.preds, - ); - // Body let body = match self.body { Ok(body_id) => { @@ -514,14 +560,15 @@ where let ctx = &ctx.set_generics(&self.generics); // Translate the parameters and the trait clauses - let (params, trait_clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx); + let (params, preds, any_where) = self + .generics + .fmt_with_ctx_with_trait_clauses(ctx, " ", &None); // Predicates - let eq_space = if trait_clauses.is_empty() && self.preds.is_empty() { + let eq_space = if !any_where { " ".to_string() } else { "\n ".to_string() }; - let preds = fmt_where_clauses_with_ctx(ctx, " ", &None, trait_clauses, &self.preds); // Decl name let name = self.name.fmt_with_ctx(ctx); @@ -861,11 +908,10 @@ impl FmtWithCtx for llbc::Statement { RawStatement::Break(index) => format!("{tab}break {index}"), RawStatement::Continue(index) => format!("{tab}continue {index}"), RawStatement::Nop => format!("{tab}nop"), - RawStatement::Sequence(st1, st2) => format!( - "{}\n{}", - st1.fmt_with_ctx_and_indent(tab, ctx), - st2.fmt_with_ctx_and_indent(tab, ctx) - ), + RawStatement::Sequence(vec) => vec + .iter() + .map(|st| st.fmt_with_ctx_and_indent(tab, ctx)) + .join("\n"), RawStatement::Switch(switch) => match switch { Switch::If(discr, true_st, false_st) => { let inner_tab = format!("{tab}{TAB_INCR}"); @@ -1028,8 +1074,9 @@ impl FmtWithCtx for TraitDecl { let ctx = &ctx.set_generics(&self.generics); let name = self.name.fmt_with_ctx(ctx); - let (generics, trait_clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx); - let clauses = fmt_where_clauses_with_ctx(ctx, "", &None, trait_clauses, &self.preds); + let (generics, clauses, _) = self + .generics + .fmt_with_ctx_with_trait_clauses(ctx, "", &None); let items = { let items = self @@ -1109,8 +1156,9 @@ impl FmtWithCtx for TraitImpl { let ctx = &ctx.set_generics(&self.generics); let name = self.name.fmt_with_ctx(ctx); - let (generics, trait_clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx); - let clauses = fmt_where_clauses_with_ctx(ctx, "", &None, trait_clauses, &self.preds); + let (generics, clauses, _) = self + .generics + .fmt_with_ctx_with_trait_clauses(ctx, "", &None); let items = { let items = self @@ -1187,13 +1235,6 @@ impl FmtWithCtx for TraitInstanceId { TraitInstanceId::TraitImpl(id) => ctx.format_object(*id), TraitInstanceId::Clause(id) => ctx.format_object(*id), TraitInstanceId::BuiltinOrAuto(id) => ctx.format_object(*id), - TraitInstanceId::Unsolved(trait_id, generics) => { - format!( - "Unsolved({}{})", - ctx.format_object(*trait_id), - generics.fmt_with_ctx(ctx), - ) - } TraitInstanceId::Unknown(msg) => format!("UNKNOWN({msg})"), } } @@ -1284,14 +1325,15 @@ impl FmtWithCtx for TypeDecl { fn fmt_with_ctx(&self, ctx: &C) -> String { let ctx = &ctx.set_generics(&self.generics); - let (params, trait_clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx); + let (params, preds, any_where) = self + .generics + .fmt_with_ctx_with_trait_clauses(ctx, " ", &None); // Predicates - let eq_space = if trait_clauses.is_empty() && self.preds.is_empty() { + let eq_space = if !any_where { " ".to_string() } else { "\n ".to_string() }; - let preds = fmt_where_clauses_with_ctx(ctx, " ", &None, trait_clauses, &self.preds); match &self.kind { TypeDeclKind::Struct(fields) => { @@ -1456,6 +1498,12 @@ impl std::fmt::Display for LiteralTy { } } +impl std::fmt::Display for Loc { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { + write!(f, "{}:{}", self.line, self.col) + } +} + impl std::fmt::Display for Operand { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { write!(f, "{}", self.fmt_with_ctx(&FmtCtx::new())) @@ -1627,71 +1675,6 @@ pub fn fmt_where_clauses(tab: &str, num_parent_clauses: usize, clauses: Vec( - ctx: &C, - tab: &str, - info: &Option, - mut trait_clauses: Vec, - preds: &Predicates, -) -> String -where - C: AstFormatter, -{ - let mut types_outlive: Vec<_> = preds - .types_outlive - .iter() - .map(|OutlivesPred(x, y)| format!("{} : {}", x.fmt_with_ctx(ctx), y.fmt_with_ctx(ctx))) - .collect(); - let mut regions_outlive: Vec<_> = preds - .regions_outlive - .iter() - .map(|OutlivesPred(x, y)| format!("{} : {}", x.fmt_with_ctx(ctx), y.fmt_with_ctx(ctx))) - .collect(); - let mut type_constraints: Vec<_> = preds - .trait_type_constraints - .iter() - .map(|x| x.fmt_with_ctx(ctx)) - .collect(); - match info { - None => { - let clauses: Vec<_> = trait_clauses - .into_iter() - .chain(types_outlive.into_iter()) - .chain(regions_outlive.into_iter()) - .chain(type_constraints.into_iter()) - .collect(); - fmt_where_clauses(tab, 0, clauses) - } - Some(info) => { - // Below: definitely not efficient nor convenient, but it is not really - // important - let local_clauses: Vec<_> = trait_clauses - .split_off(info.num_trait_clauses) - .into_iter() - .chain(regions_outlive.split_off(info.num_regions_outlive)) - .chain(types_outlive.split_off(info.num_types_outlive).into_iter()) - .chain( - type_constraints - .split_off(info.num_trait_type_constraints) - .into_iter(), - ) - .collect(); - let inherited_clauses: Vec<_> = trait_clauses - .into_iter() - .chain(regions_outlive.into_iter()) - .chain(types_outlive.into_iter()) - .chain(type_constraints.into_iter()) - .collect(); - let num_inherited = inherited_clauses.len(); - let all_clauses: Vec<_> = inherited_clauses - .into_iter() - .chain(local_clauses.into_iter()) - .collect(); - fmt_where_clauses(tab, num_inherited, all_clauses) - } - } -} - // IntTy is not defined in the current crate pub fn intty_to_string(ty: hax::IntTy) -> String { use hax::IntTy::*; diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs index 6d3c86a19..ba7092e42 100644 --- a/charon/src/pretty/formatter.rs +++ b/charon/src/pretty/formatter.rs @@ -4,7 +4,7 @@ use crate::ids::Vector; use crate::llbc_ast; use crate::llbc_ast::*; use crate::pretty::{fmt_with_ctx, FmtWithCtx}; -use crate::translate_ctx::TranslatedCrate; +use crate::translate_ctx::{AnyTransId, TranslatedCrate}; use crate::types::*; use crate::ullbc_ast; use crate::ullbc_ast as ast; @@ -174,6 +174,7 @@ pub trait AstFormatter = Formatter + Formatter + Formatter + Formatter + + Formatter + Formatter + Formatter<(DeBruijnId, RegionId)> + Formatter @@ -214,6 +215,16 @@ impl<'a> FmtCtx<'a> { locals: None, } } + + pub fn format_decl_id(&self, id: AnyTransId) -> String { + match id { + AnyTransId::Type(id) => self.format_decl(id), + AnyTransId::Fun(id) => self.format_decl(id), + AnyTransId::Global(id) => self.format_decl(id), + AnyTransId::TraitDecl(id) => self.format_decl(id), + AnyTransId::TraitImpl(id) => self.format_decl(id), + } + } } impl<'a> Default for FmtCtx<'a> { @@ -294,6 +305,18 @@ impl<'a> Formatter for FmtCtx<'a> { } } +impl<'a> Formatter for FmtCtx<'a> { + fn format_object(&self, id: AnyTransId) -> String { + match id { + AnyTransId::Type(x) => self.format_object(x), + AnyTransId::Fun(x) => self.format_object(x), + AnyTransId::Global(x) => self.format_object(x), + AnyTransId::TraitDecl(x) => self.format_object(x), + AnyTransId::TraitImpl(x) => self.format_object(x), + } + } +} + impl<'a> Formatter<(DeBruijnId, RegionId)> for FmtCtx<'a> { fn format_object(&self, (grid, id): (DeBruijnId, RegionId)) -> String { match self.region_vars.get(grid.index) { diff --git a/charon/src/transform/index_to_function_calls.rs b/charon/src/transform/index_to_function_calls.rs index 172e72bdb..5364b9c36 100644 --- a/charon/src/transform/index_to_function_calls.rs +++ b/charon/src/transform/index_to_function_calls.rs @@ -1,6 +1,8 @@ //! Desugar array/slice index operations to function calls. -use crate::expressions::{BorrowKind, MutExprVisitor, Operand, Place, ProjectionElem, Rvalue}; +use derive_visitor::{DriveMut, VisitorMut}; + +use crate::expressions::{BorrowKind, Operand, Place, ProjectionElem, Rvalue}; use crate::gast::{Call, GenericArgs, Var}; use crate::ids::Vector; use crate::llbc_ast::*; @@ -8,7 +10,6 @@ use crate::meta::Span; use crate::transform::TransformCtx; use crate::types::*; use crate::values::VarId; -use std::mem::replace; use super::ctx::LlbcPass; @@ -20,10 +21,25 @@ use super::ctx::LlbcPass; /// While we explore the places/operands present in a statement, We temporarily /// store the new statements inside the visitor. Once we've finished exploring /// the statement, we insert those before the statement. +#[derive(VisitorMut)] +#[visitor( + Statement(enter, exit), + Place(enter), + Operand(enter), + Call(enter), + FnOperand(enter), + Rvalue(enter), + RawStatement(enter), + Switch(enter) +)] struct Visitor<'a> { locals: &'a mut Vector, statements: Vec, - /// Span information of the outer statement + // When we encounter a place, we remember when a given place is accessed mutably in this + // stack. Unfortunately this requires us to be very careful to catch all the cases where we + // see places. + place_mutability_stack: Vec, + // Span information of the outer statement span: Option, } @@ -32,7 +48,7 @@ impl<'a> Visitor<'a> { self.locals.push_with(|index| Var { index, name, ty }) } - fn visit_transform_place(&mut self, mut_access: bool, p: &mut Place) { + fn transform_place(&mut self, mut_access: bool, p: &mut Place) { // Explore the place from the **end** to the beginning let mut var_id = p.var_id; let mut proj = Vec::new(); @@ -126,112 +142,105 @@ impl<'a> Visitor<'a> { projection: proj, } } -} -impl<'a> MutTypeVisitor for Visitor<'a> {} - -impl<'a> MutExprVisitor for Visitor<'a> { - fn visit_place(&mut self, p: &mut Place) { - // By default, places are used to access elements to mutate them. - // We intercept the places where it is not the case. - let mut_access = true; - self.visit_transform_place(mut_access, p); + fn enter_place(&mut self, p: &mut Place) { + // We intercept every traversal that would reach a place and push the correct mutability on + // the stack. If we missed one this will panic. + let mut_access = *self.place_mutability_stack.last().unwrap(); + self.transform_place(mut_access, p); + self.place_mutability_stack.pop(); } - fn visit_operand(&mut self, op: &mut Operand) { + fn enter_operand(&mut self, op: &mut Operand) { match op { - Operand::Move(p) => self.visit_transform_place(true, p), - Operand::Copy(p) => self.visit_transform_place(false, p), - Operand::Const(..) => (), + Operand::Move(_) => { + self.place_mutability_stack.push(true); + } + Operand::Copy(_) => { + self.place_mutability_stack.push(false); + } + Operand::Const(..) => {} + } + } + + fn enter_call(&mut self, _c: &mut Call) { + self.place_mutability_stack.push(true); + } + + fn enter_fn_operand(&mut self, fn_op: &mut FnOperand) { + match fn_op { + FnOperand::Regular(_) => {} + FnOperand::Move(_) => { + self.place_mutability_stack.push(true); + } } } - fn visit_rvalue(&mut self, rv: &mut Rvalue) { + fn enter_rvalue(&mut self, rv: &mut Rvalue) { use Rvalue::*; match rv { - Use(_) | UnaryOp(..) | BinaryOp(..) | Aggregate(..) | Global(..) | Repeat(..) => { - // We don't access places here, only operands - self.default_visit_rvalue(rv) - } - Ref(p, bkind) => { - // Ref is special - match *bkind { - BorrowKind::Mut | BorrowKind::TwoPhaseMut => { - self.visit_transform_place(true, p) - } - BorrowKind::Shared | BorrowKind::Shallow => { - self.visit_transform_place(false, p) - } + Use(_) | UnaryOp(..) | BinaryOp(..) | Aggregate(..) | Global(..) | Repeat(..) => {} + Ref(_, bkind) => match *bkind { + BorrowKind::Mut | BorrowKind::TwoPhaseMut => { + self.place_mutability_stack.push(true); } - } - Discriminant(p, _) | Len(p, _, _) => { + BorrowKind::Shared | BorrowKind::Shallow => { + self.place_mutability_stack.push(false); + } + }, + Discriminant(..) | Len(..) => { // We access places, but those places are used to access // elements without mutating them - self.visit_transform_place(false, p); + self.place_mutability_stack.push(false); } } } -} -impl<'a> MutAstVisitor for Visitor<'a> { - fn visit_branch(&mut self, branch: &mut Statement) { - #[allow(clippy::mem_replace_with_default)] - let statements = replace(&mut self.statements, Vec::new()); - self.visit_statement(branch); - // Make sure we didn't update the vector of statements + fn enter_statement(&mut self, st: &mut Statement) { + // Retrieve the span information + self.span = Some(st.span); + // As we explore this statement, we may collect extra statements to prepend to it. assert!(self.statements.is_empty()); - let _ = replace(&mut self.statements, statements); } - fn visit_statement(&mut self, st: &mut Statement) { - // Retrieve the span information - self.span = Some(st.span); - self.visit_raw_statement(&mut st.content); + fn exit_statement(&mut self, st: &mut Statement) { self.span = None; + + // Reparenthesize sequences we messed up while traversing. + st.flatten(); + + // We potentially collected statements to prepend to this one. + let seq = std::mem::take(&mut self.statements); + if !seq.is_empty() { + take_mut::take(st, |st| chain_statements(seq, st)) + } } - fn visit_raw_statement(&mut self, st: &mut RawStatement) { + fn enter_raw_statement(&mut self, st: &mut RawStatement) { use RawStatement::*; // The match is explicit on purpose: we want to make sure we intercept changes match st { - Sequence(..) => { - // Do nothing: we don't want to dive - } - FakeRead(p) => { - self.visit_transform_place(false, p); + Sequence(..) | Abort(..) | Return | Break(..) | Continue(..) | Nop | Switch(..) + | Loop(..) | Error(..) | Assert(..) | Call(..) => {} + FakeRead(_) => { + self.place_mutability_stack.push(false); } - Assign(..) | SetDiscriminant(..) | Drop(..) | Assert(..) | Call(..) | Abort(..) - | Return | Break(..) | Continue(..) | Nop | Switch(..) | Loop(..) | Error(..) => { - // Explore - self.default_visit_raw_statement(st) + Assign(..) | SetDiscriminant(..) | Drop(..) => { + self.place_mutability_stack.push(true); } } } - fn visit_switch(&mut self, s: &mut Switch) { + fn enter_switch(&mut self, s: &mut Switch) { match s { - Switch::If(op, ..) | Switch::SwitchInt(op, ..) => self.visit_operand(op), - Switch::Match(p, _, _) => { - let mut_access = false; - self.visit_transform_place(mut_access, p); + Switch::If(..) | Switch::SwitchInt(..) => {} + Switch::Match(..) => { + self.place_mutability_stack.push(false); } } } } -fn transform_st(locals: &mut Vector, s: &mut Statement) -> Option> { - // Explore the places/operands - let mut visitor = Visitor { - locals, - statements: Vec::new(), - span: None, - }; - visitor.visit_statement(s); - - // Return the statements to insert before the current one - Some(visitor.statements) -} - pub struct Transform; /// We do the following. @@ -294,7 +303,12 @@ pub struct Transform; /// ``` impl LlbcPass for Transform { fn transform_body(&self, _ctx: &mut TransformCtx<'_>, b: &mut ExprBody) { - b.body - .transform(&mut (|s: &mut Statement| transform_st(&mut b.locals, s))); + let mut visitor = Visitor { + locals: &mut b.locals, + statements: Vec::new(), + place_mutability_stack: Vec::new(), + span: None, + }; + b.body.drive_mut(&mut visitor); } } diff --git a/charon/src/transform/inline_local_panic_functions.rs b/charon/src/transform/inline_local_panic_functions.rs index 2fe33b019..7dd21fec6 100644 --- a/charon/src/transform/inline_local_panic_functions.rs +++ b/charon/src/transform/inline_local_panic_functions.rs @@ -8,47 +8,18 @@ //! Which defines a new function each time. This pass recognizes these functions and replaces calls //! to them by a `Panic` terminator. +use derive_visitor::{visitor_enter_fn_mut, DriveMut}; use std::collections::HashSet; use super::{ctx::LlbcPass, TransformCtx}; use crate::{ assumed, llbc_ast::{ - AbortKind, Call, FnOperand, FnPtr, FunDeclId, FunId, FunIdOrTraitMethodRef, MutExprVisitor, - RawStatement, Statement, + AbortKind, Call, FnOperand, FnPtr, FunId, FunIdOrTraitMethodRef, RawStatement, Statement, }, - llbc_ast_utils::MutAstVisitor, names::Name, - types_utils::MutTypeVisitor, }; -struct ReplacePanics<'a> { - fns_to_replace: &'a HashSet, - replace_with_statement: &'a RawStatement, -} - -impl MutTypeVisitor for ReplacePanics<'_> {} -impl MutAstVisitor for ReplacePanics<'_> { - fn visit_statement(&mut self, st: &mut Statement) { - match &mut st.content { - RawStatement::Call(Call { - func: - FnOperand::Regular(FnPtr { - func: FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)), - .. - }), - .. - }) if self.fns_to_replace.contains(fun_id) => { - st.content = self.replace_with_statement.clone(); - } - _ => { - self.default_visit_raw_statement(&mut st.content); - } - } - } -} -impl MutExprVisitor for ReplacePanics<'_> {} - pub struct Transform; impl LlbcPass for Transform { fn transform_ctx(&self, ctx: &mut TransformCtx<'_>) { @@ -73,11 +44,21 @@ impl LlbcPass for Transform { // Replace each call to one such function with a `Panic`. ctx.for_each_structured_body(|_ctx, body| { - let mut visitor = ReplacePanics { - fns_to_replace: &panic_fns, - replace_with_statement: &panic_statement, - }; - visitor.visit_statement(&mut body.body); + body.body.drive_mut(&mut visitor_enter_fn_mut( + |st: &mut Statement| match &mut st.content { + RawStatement::Call(Call { + func: + FnOperand::Regular(FnPtr { + func: FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)), + .. + }), + .. + }) if panic_fns.contains(fun_id) => { + st.content = panic_statement.clone(); + } + _ => {} + }, + )); }); // Remove these functions from the context. diff --git a/charon/src/transform/insert_assign_return_unit.rs b/charon/src/transform/insert_assign_return_unit.rs index a0e253777..687452016 100644 --- a/charon/src/transform/insert_assign_return_unit.rs +++ b/charon/src/transform/insert_assign_return_unit.rs @@ -24,7 +24,7 @@ fn transform_st(st: &mut Statement) -> Option> { ); let assign_st = Statement::new(st.span, RawStatement::Assign(ret_place, unit_value)); let ret_st = Statement::new(st.span, RawStatement::Return); - st.content = RawStatement::Sequence(Box::new(assign_st), Box::new(ret_st)); + st.content = assign_st.then(ret_st).content; }; None } diff --git a/charon/src/transform/reconstruct_asserts.rs b/charon/src/transform/reconstruct_asserts.rs index fc19396b9..77f685dfb 100644 --- a/charon/src/transform/reconstruct_asserts.rs +++ b/charon/src/transform/reconstruct_asserts.rs @@ -25,8 +25,7 @@ fn transform_st(st: &mut Statement) -> Option> { expected: false, }), ); - let st1 = Box::new(st1); - RawStatement::Sequence(st1, st2) + st1.then(*st2).content }); } } diff --git a/charon/src/transform/remove_arithmetic_overflow_checks.rs b/charon/src/transform/remove_arithmetic_overflow_checks.rs index 37e68ad97..7d74b6b41 100644 --- a/charon/src/transform/remove_arithmetic_overflow_checks.rs +++ b/charon/src/transform/remove_arithmetic_overflow_checks.rs @@ -2,14 +2,12 @@ //! [`remove_dynamic_checks`]. See comments there for more details. use crate::llbc_ast::*; use crate::transform::TransformCtx; -use crate::types::*; -use take_mut::take; use super::ctx::LlbcPass; -struct RemoveDynChecks; +pub struct Transform; -impl RemoveDynChecks { +impl Transform { /// After `remove_dynamic_checks`, the only remaining dynamic checks are overflow checks. We /// couldn't remove them in ullbc because the generated code spans two basic blocks. They are /// inserted only in constants since we otherwise compile in release mode. These assertions @@ -23,85 +21,68 @@ impl RemoveDynChecks { /// ```text /// z := x + y; /// ``` - fn simplify(&mut self, s: &mut Statement) { - if let RawStatement::Sequence(s0, s1) = &mut s.content { - if let RawStatement::Sequence(s1, s2) = &mut s1.content { - // TODO: the last statement is not necessarily a sequence - if let RawStatement::Sequence(s2, _) = &mut s2.content { - if let ( - RawStatement::Assign( - binop, - Rvalue::BinaryOp( - op @ (BinOp::CheckedAdd | BinOp::CheckedSub | BinOp::CheckedMul), - _, - _, - ), - ), - RawStatement::Assert(Assert { - cond: Operand::Move(assert_cond), - expected: false, - }), - RawStatement::Assign(final_value, Rvalue::Use(Operand::Move(assigned))), - ) = (&mut s0.content, &s1.content, &mut s2.content) - { - // assigned should be: binop.0 - // assert_cond should be: binop.1 - if let ( - [ProjectionElem::Field(FieldProjKind::Tuple(..), fid0)], - [ProjectionElem::Field(FieldProjKind::Tuple(..), fid1)], - ) = ( - assigned.projection.as_slice(), - assert_cond.projection.as_slice(), - ) { - if assert_cond.var_id == binop.var_id - && assigned.var_id == binop.var_id - && binop.projection.len() == 0 - && fid0.index() == 0 - && fid1.index() == 1 - { - // Switch to the unchecked operation. - *op = match op { - BinOp::CheckedAdd => BinOp::Add, - BinOp::CheckedSub => BinOp::Sub, - BinOp::CheckedMul => BinOp::Mul, - _ => unreachable!(), - }; - // Assign to the correct value in `s0`. - std::mem::swap(binop, final_value); - // Remove `s1` and `s2`. - take(s, |s| { - let (s0, s1) = s.content.to_sequence(); - let (_s1, s2) = s1.content.to_sequence(); - let (_s2, s3) = s2.content.to_sequence(); - Statement { - span: s0.span, - content: RawStatement::Sequence(s0, s3), - } - }); - } - } - } + fn update_statements(seq: &mut [Statement]) { + if let [Statement { + content: + RawStatement::Assign( + binop, + Rvalue::BinaryOp( + op @ (BinOp::CheckedAdd | BinOp::CheckedSub | BinOp::CheckedMul), + _, + _, + ), + ), + .. + }, Statement { + content: + RawStatement::Assert(Assert { + cond: Operand::Move(assert_cond), + expected: false, + }), + .. + }, Statement { + content: RawStatement::Assign(final_value, Rvalue::Use(Operand::Move(assigned))), + .. + }, ..] = seq + { + // assigned should be: binop.0 + // assert_cond should be: binop.1 + if let ( + [ProjectionElem::Field(FieldProjKind::Tuple(..), fid0)], + [ProjectionElem::Field(FieldProjKind::Tuple(..), fid1)], + ) = ( + assigned.projection.as_slice(), + assert_cond.projection.as_slice(), + ) { + if assert_cond.var_id == binop.var_id + && assigned.var_id == binop.var_id + && binop.projection.len() == 0 + && fid0.index() == 0 + && fid1.index() == 1 + { + // Switch to the unchecked operation. + *op = match op { + BinOp::CheckedAdd => BinOp::Add, + BinOp::CheckedSub => BinOp::Sub, + BinOp::CheckedMul => BinOp::Mul, + _ => unreachable!(), + }; + // Assign to the correct value in the first statement. + std::mem::swap(binop, final_value); + // Remove the other two statements. + seq[1].content = RawStatement::Nop; + seq[2].content = RawStatement::Nop; } } } } } -impl MutTypeVisitor for RemoveDynChecks {} -impl MutExprVisitor for RemoveDynChecks {} - -impl MutAstVisitor for RemoveDynChecks { - fn visit_statement(&mut self, s: &mut Statement) { - // Simplify this statement. - self.simplify(s); - // Recurse into subsequent statements. - self.default_visit_raw_statement(&mut s.content); - } -} - -pub struct Transform; impl LlbcPass for Transform { fn transform_body(&self, _ctx: &mut TransformCtx<'_>, b: &mut ExprBody) { - RemoveDynChecks.visit_statement(&mut b.body); + b.body.transform_sequences(&mut |seq| { + Transform::update_statements(seq); + Vec::new() + }) } } diff --git a/charon/src/transform/remove_drop_never.rs b/charon/src/transform/remove_drop_never.rs index 7711ed7cf..52b49d7a1 100644 --- a/charon/src/transform/remove_drop_never.rs +++ b/charon/src/transform/remove_drop_never.rs @@ -13,22 +13,13 @@ use super::ctx::LlbcPass; /// Filter the statement by replacing it with `Nop` if it is a `Drop(x)` where /// `x` has type `Never`. Otherwise leave it unchanged. fn transform_st(locals: &Vector, st: &mut Statement) { - // Shall we filter the statement? - let filter = match &mut st.content { - RawStatement::Drop(p) => { - if p.projection.is_empty() { - let var = locals.get(p.var_id).unwrap(); - var.ty.is_never() - } else { - false + if let RawStatement::Drop(p) = &st.content { + if p.projection.is_empty() { + let var = locals.get(p.var_id).unwrap(); + if var.ty.is_never() { + st.content = RawStatement::Nop; } } - _ => false, - }; - - // If we filter the statement, we simply replace it with `nop` - if filter { - *st = Statement::new(st.span, RawStatement::Nop); } } diff --git a/charon/src/transform/remove_nops.rs b/charon/src/transform/remove_nops.rs index 465d0fdc5..ea4a565e6 100644 --- a/charon/src/transform/remove_nops.rs +++ b/charon/src/transform/remove_nops.rs @@ -1,22 +1,20 @@ //! Remove the useless no-ops. use crate::llbc_ast::{ExprBody, RawStatement, Statement}; -use crate::meta::combine_span; use crate::transform::TransformCtx; use take_mut::take; use super::ctx::LlbcPass; fn transform_st(s: &mut Statement) { - if let RawStatement::Sequence(s1, _) = &s.content { - if s1.content.is_nop() { - take(s, |s| { - let (s1, s2) = s.content.to_sequence(); - Statement { - content: s2.content, - span: combine_span(&s1.span, &s2.span), - } - }) + if let RawStatement::Sequence(seq) = &mut s.content { + // Remove all the `Nop`s from this sequence. + if seq.iter().any(|st| st.content.is_nop()) { + seq.retain(|st| !st.content.is_nop()) + } + // Replace an empty sequence with a `Nop`. + if seq.is_empty() { + take(&mut s.content, |_| RawStatement::Nop) } } } diff --git a/charon/src/transform/remove_read_discriminant.rs b/charon/src/transform/remove_read_discriminant.rs index 935a3f5b2..e85b9eec1 100644 --- a/charon/src/transform/remove_read_discriminant.rs +++ b/charon/src/transform/remove_read_discriminant.rs @@ -4,44 +4,36 @@ //! filtering). Then, we filter the unused variables ([crate::remove_unused_locals]). use crate::llbc_ast::*; -use crate::meta::combine_span; use crate::transform::TransformCtx; use crate::translate_ctx::*; use crate::types::*; use crate::values::{Literal, ScalarValue}; +use derive_visitor::visitor_enter_fn_mut; +use derive_visitor::DriveMut; use itertools::Itertools; use std::collections::{HashMap, HashSet}; use super::ctx::LlbcPass; -struct Visitor<'a, 'ctx> { - ctx: &'a mut TransformCtx<'ctx>, -} - -impl<'a, 'ctx> Visitor<'a, 'ctx> { - fn update_statement(&mut self, st: &mut Statement) { - match &mut st.content { - RawStatement::Sequence( - box Statement { - content: RawStatement::Assign(dest, Rvalue::Discriminant(p, adt_id)), - span: span1, - }, - box st2, - ) => { +pub struct Transform; +impl Transform { + fn update_statement(ctx: &mut TransformCtx<'_>, st: &mut Statement) { + let RawStatement::Sequence(seq) = &mut st.content else { + return; + }; + // Iterate through the statements. + for i in 0..seq.len() { + let suffix = &mut seq[i..]; + if let [Statement { + content: RawStatement::Assign(dest, Rvalue::Discriminant(p, adt_id)), + span: span1, + }, rest @ ..] = suffix + { // The destination should be a variable assert!(dest.projection.is_empty()); - // Take st2 - let st2 = std::mem::replace( - st2, - Statement { - content: RawStatement::Nop, - span: st2.span, - }, - ); - // Lookup the type of the scrutinee - let variants = match self.ctx.translated.type_decls.get(*adt_id) { + let variants = match ctx.translated.type_decls.get(*adt_id) { // This can happen if there was an error while extracting the definitions None => None, Some(d) => { @@ -51,7 +43,7 @@ impl<'a, 'ctx> Visitor<'a, 'ctx> { | TypeDeclKind::Alias(..) => { // We shouldn't get there register_error_or_panic!( - self.ctx, + ctx, st.span.span.rust_span_data.span(), "Unreachable case" ); @@ -64,89 +56,69 @@ impl<'a, 'ctx> Visitor<'a, 'ctx> { }; let Some(variants) = variants else { // An error occurred. We can't keep the `Rvalue::Discriminant` around so we - // `Nop` the whole statement sequence. - assert!(self.ctx.has_errors()); - *st = Statement { - content: RawStatement::Nop, - span: st.span, - }; + // `Nop` the discriminant read. + assert!(ctx.has_errors()); + seq[i].content = RawStatement::Nop; return; }; // We look for a `SwitchInt` just after the discriminant read. - // Note that it may be contained in a sequence, of course. - let maybe_switch = match st2.content { - RawStatement::Sequence( - box Statement { - content: RawStatement::Switch(switch @ Switch::SwitchInt(..)), - span: span2, - }, - box st3, - ) => Ok((span2, switch, Some(st3))), - RawStatement::Switch(switch @ Switch::SwitchInt(..)) => { - Ok((st2.span, switch, None)) - } - _ => Err(st2), - }; - - match maybe_switch { - Ok((span2, switch, st3_opt)) => { - let Switch::SwitchInt(Operand::Move(op_p), _int_ty, targets, otherwise) = - switch - else { - unreachable!() - }; - assert!(op_p.projection.is_empty() && op_p.var_id == dest.var_id); - + match rest { + [Statement { + content: + RawStatement::Switch(switch @ Switch::SwitchInt(Operand::Move(_), ..)), + .. + }, ..] => { // Convert between discriminants and variant indices. Remark: the discriminant can // be of any *signed* integer type (`isize`, `i8`, etc.). let discr_to_id: HashMap = variants .iter_indexed_values() .map(|(id, variant)| (variant.discriminant, id)) .collect(); - let mut covered_discriminants: HashSet = HashSet::default(); - let targets = targets - .into_iter() - .map(|(v, e)| { - ( - v.into_iter() - .filter_map(|discr| { - covered_discriminants.insert(discr); - discr_to_id.get(&discr).or_else(|| { - register_error_or_panic!( - self.ctx, - st.span.span.rust_span_data.span(), - "Found incorrect discriminant {discr} for enum {adt_id}" - ); - None - }) - }) - .copied() - .collect_vec(), - e, - ) - }) - .collect_vec(); - // Filter the otherwise branch if it is not necessary. - let covers_all = covered_discriminants.len() == discr_to_id.len(); - let otherwise = if covers_all { None } else { Some(otherwise) }; - let switch = - RawStatement::Switch(Switch::Match(p.clone(), targets, otherwise)); - - // Add the next statement if there is one - st.content = if let Some(st3) = st3_opt { - let span = combine_span(span1, &span2); - let switch = Statement { - span, - content: switch, + take_mut::take(switch, |switch| { + let (Operand::Move(op_p), _, targets, otherwise) = + switch.to_switch_int() + else { + unreachable!() }; - new_sequence(switch, st3).content - } else { - switch - }; + assert!(op_p.projection.is_empty() && op_p.var_id == dest.var_id); + + let mut covered_discriminants: HashSet = + HashSet::default(); + let targets = targets + .into_iter() + .map(|(v, e)| { + ( + v.into_iter() + .filter_map(|discr| { + covered_discriminants.insert(discr); + discr_to_id.get(&discr).or_else(|| { + register_error_or_panic!( + ctx, + st.span.span.rust_span_data.span(), + "Found incorrect discriminant {discr} for enum {adt_id}" + ); + None + }) + }) + .copied() + .collect_vec(), + e, + ) + }) + .collect_vec(); + // Filter the otherwise branch if it is not necessary. + let covers_all = covered_discriminants.len() == discr_to_id.len(); + let otherwise = if covers_all { None } else { Some(otherwise) }; + + // Replace the old switch with a match. + Switch::Match(p.clone(), targets, otherwise) + }); + // `Nop` the discriminant read. + seq[i].content = RawStatement::Nop; } - Err(st2) => { + _ => { // The discriminant read is not followed by a `SwitchInt`. This can happen // in optimized MIR. We replace `_x = Discr(_y)` with `match _y { 0 => { _x // = 0 }, 1 => { _x = 1; }, .. }`. @@ -169,41 +141,20 @@ impl<'a, 'ctx> Visitor<'a, 'ctx> { (vec![id], statement) }) .collect(); - let switch = RawStatement::Switch(Switch::Match(p.clone(), targets, None)); - let switch = Statement { - span: *span1, - content: switch, - }; - st.content = new_sequence(switch, st2).content + seq[i].content = + RawStatement::Switch(Switch::Match(p.clone(), targets, None)) } } } - RawStatement::Assign(_, Rvalue::Discriminant(_, _)) => { - // We failed to remove a [Discriminant] - unreachable!(); - } - _ => (), } } } -impl<'a, 'ctx> MutTypeVisitor for Visitor<'a, 'ctx> {} -impl<'a, 'ctx> MutExprVisitor for Visitor<'a, 'ctx> {} -impl<'a, 'ctx> MutAstVisitor for Visitor<'a, 'ctx> { - fn visit_statement(&mut self, st: &mut Statement) { - self.update_statement(st); - - // Visit again, to make sure we transform the branches and - // the next statement, in case we updated, or to update the - // sub-statements, in case we didn't perform any updates. - self.default_visit_statement(st); - } -} - -pub struct Transform; impl LlbcPass for Transform { fn transform_body(&self, ctx: &mut TransformCtx<'_>, b: &mut ExprBody) { - let mut visitor = Visitor { ctx }; - visitor.visit_statement(&mut b.body); + b.body + .drive_mut(&mut visitor_enter_fn_mut(|st: &mut Statement| { + Transform::update_statement(ctx, st); + })); } } diff --git a/charon/src/transform/remove_unused_locals.rs b/charon/src/transform/remove_unused_locals.rs index 46f7be629..59944a229 100644 --- a/charon/src/transform/remove_unused_locals.rs +++ b/charon/src/transform/remove_unused_locals.rs @@ -2,72 +2,17 @@ //! never used in the function bodies. This is useful to remove the locals with //! type `Never`. We actually check that there are no such local variables //! remaining afterwards. -use crate::expressions::{MutExprVisitor, SharedExprVisitor}; use crate::ids::Vector; -use crate::llbc_ast::{ExprBody, MutAstVisitor, SharedAstVisitor, Statement}; +use crate::llbc_ast::{ExprBody, Statement}; use crate::transform::TransformCtx; -use crate::types::{MutTypeVisitor, SharedTypeVisitor}; use crate::ullbc_ast::Var; use crate::values::*; +use derive_visitor::{visitor_enter_fn, visitor_enter_fn_mut, Drive, DriveMut}; use std::collections::{HashMap, HashSet}; use take_mut::take; use super::ctx::LlbcPass; -#[derive(Debug, Clone)] -pub(crate) struct ComputeUsedLocals { - vars: im::HashMap, -} - -impl ComputeUsedLocals { - fn new() -> Self { - ComputeUsedLocals { - vars: im::HashMap::new(), - } - } - - pub(crate) fn compute_in_statement(st: &Statement) -> im::HashMap { - let mut visitor = Self::new(); - visitor.visit_statement(st); - visitor.vars - } -} - -impl SharedTypeVisitor for ComputeUsedLocals {} -impl SharedExprVisitor for ComputeUsedLocals { - fn visit_var_id(&mut self, vid: &VarId) { - match self.vars.get_mut(vid) { - None => { - let _ = self.vars.insert(*vid, 1); - } - Some(cnt) => *cnt += 1, - } - } -} - -impl SharedAstVisitor for ComputeUsedLocals {} - -#[derive(Debug, Clone)] -struct UpdateUsedLocals { - vids_map: HashMap, -} - -impl UpdateUsedLocals { - fn update_statement(vids_map: HashMap, st: &mut Statement) { - let mut v = UpdateUsedLocals { vids_map }; - v.visit_statement(st); - } -} - -impl MutTypeVisitor for UpdateUsedLocals {} -impl MutExprVisitor for UpdateUsedLocals { - fn visit_var_id(&mut self, vid: &mut VarId) { - *vid = *self.vids_map.get(vid).unwrap(); - } -} - -impl MutAstVisitor for UpdateUsedLocals {} - /// Compute the set of used locals, filter the unused locals and compute a new /// mapping from variable index to variable index. fn update_locals( @@ -82,7 +27,15 @@ fn update_locals( used_locals.insert(VarId::new(i)); } // Explore the body - let used_locals_cnt = ComputeUsedLocals::compute_in_statement(st); + let mut used_locals_cnt: im::HashMap = im::HashMap::default(); + st.drive(&mut visitor_enter_fn(|vid: &VarId| { + match used_locals_cnt.get_mut(vid) { + None => { + let _ = used_locals_cnt.insert(*vid, 1); + } + Some(cnt) => *cnt += 1, + } + })); for (vid, cnt) in used_locals_cnt.iter() { if *cnt > 0 { used_locals.insert(*vid); @@ -112,7 +65,12 @@ impl LlbcPass for Transform { let (locals, vids_map) = update_locals(b.arg_count, b.locals, &b.body); b.locals = locals; trace!("vids_maps: {:?}", vids_map); - UpdateUsedLocals::update_statement(vids_map, &mut b.body); + + // Update all `VarId`s. + b.body + .drive_mut(&mut visitor_enter_fn_mut(|vid: &mut VarId| { + *vid = *vids_map.get(vid).unwrap(); + })); b }); } diff --git a/charon/src/transform/reorder_decls.rs b/charon/src/transform/reorder_decls.rs index eeef7f76f..af0306668 100644 --- a/charon/src/transform/reorder_decls.rs +++ b/charon/src/transform/reorder_decls.rs @@ -5,6 +5,7 @@ use crate::transform::TransformCtx; pub use crate::translate_ctx::AnyTransId; use crate::types::*; use crate::ullbc_ast::*; +use derive_visitor::{Drive, Visitor}; use hashlink::linked_hash_map::LinkedHashMap; use linked_hash_set::LinkedHashSet; use macros::{VariantIndexArity, VariantName}; @@ -37,85 +38,51 @@ pub enum DeclarationGroup { TraitDecl(GDeclarationGroup), /// TraitImpl(GDeclarationGroup), + /// Anything that doesn't fit into these categories. + Mixed(GDeclarationGroup), } impl GDeclarationGroup { - pub fn get_ids(&self) -> Vec { + pub fn get_ids(&self) -> &[Id] { use GDeclarationGroup::*; match self { - NonRec(id) => vec![*id], - Rec(ids) => ids.clone(), + NonRec(id) => std::slice::from_ref(id), + Rec(ids) => ids.as_slice(), } } -} - -impl DeclarationGroup { - fn make_type_group(is_rec: bool, gr: impl Iterator) -> Self { - let gr: Vec<_> = gr.collect(); - if is_rec { - DeclarationGroup::Type(GDeclarationGroup::Rec(gr)) - } else { - assert!(gr.len() == 1); - DeclarationGroup::Type(GDeclarationGroup::NonRec(gr[0])) - } + pub fn get_any_trans_ids(&self) -> Vec + where + Id: Into, + { + self.get_ids().iter().copied().map(|id| id.into()).collect() } - - fn make_fun_group(is_rec: bool, gr: impl Iterator) -> Self { - let gr: Vec<_> = gr.collect(); + fn make_group(is_rec: bool, gr: impl Iterator) -> Self + where + Id: TryFrom, + Id::Error: Debug, + { + let gr: Vec<_> = gr.map(|x| x.try_into().unwrap()).collect(); if is_rec { - DeclarationGroup::Fun(GDeclarationGroup::Rec(gr)) + GDeclarationGroup::Rec(gr) } else { assert!(gr.len() == 1); - DeclarationGroup::Fun(GDeclarationGroup::NonRec(gr[0])) - } - } - - fn make_global_group(is_rec: bool, gr: impl Iterator) -> Self { - let gr: Vec<_> = gr.collect(); - if is_rec { - DeclarationGroup::Global(GDeclarationGroup::Rec(gr)) - } else { - assert!(gr.len() == 1); - DeclarationGroup::Global(GDeclarationGroup::NonRec(gr[0])) + GDeclarationGroup::NonRec(gr[0]) } } +} - fn make_trait_decl_group( - _ctx: &TransformCtx, - _is_rec: bool, - gr: impl Iterator, - ) -> Self { - let gr: Vec<_> = gr.collect(); - // Trait declarations often refer to `Self`, like below, - // which means they are often considered as recursive by our - // analysis. TODO: do something more precise. What is important - // is that we never use the "whole" self clause as argument, - // but rather projections over the self clause (like `::u`, - // in the declaration for `Foo`). - if gr.len() == 1 { - DeclarationGroup::TraitDecl(GDeclarationGroup::NonRec(gr[0])) - } else { - DeclarationGroup::TraitDecl(GDeclarationGroup::Rec(gr)) +impl DeclarationGroup { + pub fn get_ids(&self) -> Vec { + use DeclarationGroup::*; + match self { + Type(gr) => gr.get_any_trans_ids(), + Fun(gr) => gr.get_any_trans_ids(), + Global(gr) => gr.get_any_trans_ids(), + TraitDecl(gr) => gr.get_any_trans_ids(), + TraitImpl(gr) => gr.get_any_trans_ids(), + Mixed(gr) => gr.get_any_trans_ids(), } } - - fn make_trait_impl_group( - ctx: &TransformCtx, - is_rec: bool, - gr: impl Iterator, - ) -> Self { - let gr: Vec<_> = gr.collect(); - let ctx = ctx.into_fmt(); - assert!( - !is_rec && gr.len() == 1, - "Invalid trait impl group:\n{}", - gr.iter() - .map(|id| ctx.format_object(*id)) - .collect::>() - .join("\n") - ); - DeclarationGroup::TraitImpl(GDeclarationGroup::NonRec(gr[0])) - } } #[derive(Clone, Copy)] @@ -150,63 +117,75 @@ impl Display for DeclarationGroup { DeclarationGroup::Global(decl) => write!(f, "{{ Global(s): {decl} }}"), DeclarationGroup::TraitDecl(decl) => write!(f, "{{ Trait decls(s): {decl} }}"), DeclarationGroup::TraitImpl(decl) => write!(f, "{{ Trait impl(s): {decl} }}"), + DeclarationGroup::Mixed(decl) => write!(f, "{{ Mixed items: {decl} }}"), } } } -pub struct Deps { +#[derive(Visitor)] +#[visitor( + TypeDeclId(enter), + FunDeclId(enter), + GlobalDeclId(enter), + TraitImplId(enter), + TraitDeclId(enter), + BodyId(enter) +)] +pub struct Deps<'tcx, 'ctx> { + ctx: &'tcx TransformCtx<'ctx>, dgraph: DiGraphMap, - /// Want to make sure we remember the order of insertion + // Want to make sure we remember the order of insertion graph: LinkedHashMap>, - /// We use this when computing the graph + // We use this when computing the graph current_id: Option, - /// We use this to track the trait impl block the current item belongs to - /// (if relevant). - /// - /// We use this to ignore the references to the parent impl block. - /// - /// If we don't do so, when computing our dependency graph we end up with - /// mutually recursive trait impl blocks/trait method impls in the presence - /// of associated types (the deepest reason is that we don't normalize the - /// types we query from rustc when translating the types from function - /// signatures - we avoid doing so because as of now it makes resolving - /// the trait params harder: if we get normalized types, we have to - /// implement a normalizer on our side to make sure we correctly match - /// types...). - /// - /// - /// For instance, the problem happens if in Rust we have: - /// ```text - /// pub trait WithConstTy { - /// type W; - /// fn f(x: &mut Self::W); - /// } - /// - /// impl WithConstTy for bool { - /// type W = u64; - /// fn f(_: &mut Self::W) {} - /// } - /// ``` - /// - /// In LLBC we get: - /// - /// ```text - /// impl traits::Bool::0 : traits::WithConstTy - /// { - /// type W = u64 with [] - /// fn f = traits::Bool::0::f - /// } - /// - /// fn traits::Bool::0::f<@R0>(@1: &@R0 mut (traits::Bool::0::W)) { .. } - /// // ^^^^^^^^^^^^^^^ - /// // refers to the trait impl - /// ``` + // We use this to track the trait impl block the current item belongs to + // (if relevant). + // + // We use this to ignore the references to the parent impl block. + // + // If we don't do so, when computing our dependency graph we end up with + // mutually recursive trait impl blocks/trait method impls in the presence + // of associated types (the deepest reason is that we don't normalize the + // types we query from rustc when translating the types from function + // signatures - we avoid doing so because as of now it makes resolving + // the trait params harder: if we get normalized types, we have to + // implement a normalizer on our side to make sure we correctly match + // types...). + // + // + // For instance, the problem happens if in Rust we have: + // ```text + // pub trait WithConstTy { + // type W; + // fn f(x: &mut Self::W); + // } + // + // impl WithConstTy for bool { + // type W = u64; + // fn f(_: &mut Self::W) {} + // } + // ``` + // + // In LLBC we get: + // + // ```text + // impl traits::Bool::0 : traits::WithConstTy + // { + // type W = u64 with [] + // fn f = traits::Bool::0::f + // } + // + // fn traits::Bool::0::f<@R0>(@1: &@R0 mut (traits::Bool::0::W)) { .. } + // // ^^^^^^^^^^^^^^^ + // // refers to the trait impl + // ``` impl_trait_id: Option, } -impl Deps { - fn new() -> Self { +impl<'tcx, 'ctx> Deps<'tcx, 'ctx> { + fn new(ctx: &'tcx TransformCtx<'ctx>) -> Self { Deps { + ctx, dgraph: DiGraphMap::new(), graph: LinkedHashMap::new(), current_id: None, @@ -272,18 +251,18 @@ impl Deps { } } -impl SharedTypeVisitor for Deps { - fn visit_type_decl_id(&mut self, id: &TypeDeclId) { +impl Deps<'_, '_> { + fn enter_type_decl_id(&mut self, id: &TypeDeclId) { let id = AnyTransId::Type(*id); self.insert_edge(id); } - fn visit_global_decl_id(&mut self, id: &GlobalDeclId) { + fn enter_global_decl_id(&mut self, id: &GlobalDeclId) { let id = AnyTransId::Global(*id); self.insert_edge(id); } - fn visit_trait_impl_id(&mut self, id: &TraitImplId) { + fn enter_trait_impl_id(&mut self, id: &TraitImplId) { // If the impl is the impl this item belongs to, we ignore it // TODO: this is not very satisfying but this is the only way // we have of preventing mutually recursive groups between @@ -298,60 +277,20 @@ impl SharedTypeVisitor for Deps { } } - fn visit_trait_decl_id(&mut self, id: &TraitDeclId) { + fn enter_trait_decl_id(&mut self, id: &TraitDeclId) { let id = AnyTransId::TraitDecl(*id); self.insert_edge(id); } - /// We override this method to not visit the trait decl. - /// - /// This is sound because the trait ref itself will either have a dependency - /// on the trait decl it implements, or it will refer to a clause which - /// will imply a dependency on the trait decl. - /// - /// The reason why we do this is that otherwise if a trait decl declares - /// a method which uses one of its associated types we will conclude that - /// the trait decl is recursive, while it isn't. - fn visit_trait_ref(&mut self, tr: &TraitRef) { - self.visit_trait_instance_id(&tr.trait_id); - self.visit_generic_args(&tr.generics); - } - - fn visit_fun_decl_id(&mut self, id: &FunDeclId) { + fn enter_fun_decl_id(&mut self, id: &FunDeclId) { let id = AnyTransId::Fun(*id); self.insert_edge(id); } -} - -impl SharedExprVisitor for Deps {} -impl SharedAstVisitor for Deps {} - -impl Deps { - fn visit_body(&mut self, body: Option<&Body>) { - if let Some(Body::Unstructured(body)) = body { - for v in &body.locals { - self.visit_ty(&v.ty); - } - for block in &body.body { - self.visit_block_data(block); - } - } - } - fn visit_generics_and_preds(&mut self, generics: &GenericParams, preds: &Predicates) { - // Visit the traits referenced in the generics - for clause in &generics.trait_clauses { - self.visit_trait_clause(clause); + fn enter_body_id(&mut self, id: &BodyId) { + if let Some(body) = self.ctx.translated.bodies.get(*id) { + body.drive(self); } - - // Visit the predicates - self.visit_predicates(preds); - } - - /// Lookup a function and visit its signature - fn visit_fun_signature_from_trait(&mut self, ctx: &TransformCtx, fid: FunDeclId) { - let decl = ctx.translated.fun_decls.get(fid).unwrap(); - self.visit_fun_sig(&decl.signature); } } @@ -369,7 +308,7 @@ impl AnyTransId { } } -impl Deps { +impl Deps<'_, '_> { fn fmt_with_ctx(&self, ctx: &TransformCtx) -> String { self.dgraph .nodes() @@ -388,35 +327,14 @@ impl Deps { } } -fn compute_declarations_graph(ctx: &TransformCtx) -> Deps { - let mut graph = Deps::new(); +fn compute_declarations_graph<'tcx, 'ctx>(ctx: &'tcx TransformCtx<'ctx>) -> Deps<'tcx, 'ctx> { + let mut graph = Deps::new(ctx); for id in &ctx.translated.all_ids { graph.set_current_id(ctx, *id); match id { AnyTransId::Type(id) => { if let Some(d) = ctx.translated.type_decls.get(*id) { - use TypeDeclKind::*; - - // Visit the generics and the predicates - graph.visit_generics_and_preds(&d.generics, &d.preds); - - // Visit the body - match &d.kind { - Struct(fields) => { - for f in fields { - graph.visit_ty(&f.ty) - } - } - Enum(vl) => { - for v in vl { - for f in &v.fields { - graph.visit_ty(&f.ty); - } - } - } - Alias(ty) => graph.visit_ty(ty), - Opaque | Error(_) => (), - } + d.drive(&mut graph); } else { // There may have been errors assert!(ctx.has_errors()); @@ -425,18 +343,10 @@ fn compute_declarations_graph(ctx: &TransformCtx) -> Deps { AnyTransId::Fun(id) => { if let Some(d) = ctx.translated.fun_decls.get(*id) { // Explore the signature - let sig = &d.signature; - graph.visit_generics_and_preds(&sig.generics, &sig.preds); - for ty in &sig.inputs { - graph.visit_ty(ty); - } - graph.visit_ty(&sig.output); - - if let Ok(id) = d.body { - // Explore the body - let body = ctx.translated.bodies.get(id); - graph.visit_body(body); - } + d.signature.drive(&mut graph); + // Skip `d.kind`: we don't want to record a dependency to the impl block this + // belongs to. + d.body.drive(&mut graph); } else { // There may have been errors assert!(ctx.has_errors()); @@ -444,11 +354,8 @@ fn compute_declarations_graph(ctx: &TransformCtx) -> Deps { } AnyTransId::Global(id) => { if let Some(d) = ctx.translated.global_decls.get(*id) { - if let Ok(id) = d.body { - // Explore the body - let body = ctx.translated.bodies.get(id); - graph.visit_body(body); - } + // FIXME: shouldn't we visit the generics etc? + d.body.drive(&mut graph); } else { // There may have been errors assert!(ctx.has_errors()); @@ -456,36 +363,22 @@ fn compute_declarations_graph(ctx: &TransformCtx) -> Deps { } AnyTransId::TraitDecl(id) => { if let Some(d) = ctx.translated.trait_decls.get(*id) { - // Visit the generics and the predicates - graph.visit_generics_and_preds(&d.generics, &d.preds); + // Visit the traits referenced in the generics + d.generics.drive(&mut graph); // Visit the parent clauses - for clause in &d.parent_clauses { - graph.visit_trait_clause(clause); - } + d.parent_clauses.drive(&mut graph); // Visit the items - for (_, (ty, c)) in &d.consts { - graph.visit_ty(ty); - if let Some(id) = c { - graph.visit_global_decl_id(id); - } - } - - for (_, (clauses, ty)) in &d.types { - for c in clauses { - graph.visit_trait_clause(c); - } - if let Some(ty) = ty { - graph.visit_ty(ty); - } - } - - let method_ids = d.required_methods.iter().map(|(_, id)| *id).chain( - d.provided_methods - .iter() - .filter_map(|(_, id)| id.as_ref().copied()), - ); + d.consts.drive(&mut graph); + d.types.drive(&mut graph); + + let method_ids = d + .required_methods + .iter() + .map(|(_, id)| id) + .chain(d.provided_methods.iter().filter_map(|(_, id)| id.as_ref())) + .copied(); for id in method_ids { // Important: we must ignore the function id, because // otherwise in the presence of associated types we may @@ -498,7 +391,8 @@ fn compute_declarations_graph(ctx: &TransformCtx) -> Deps { // fn f(x : Trait::X); // } // ``` - graph.visit_fun_signature_from_trait(ctx, id) + let decl = ctx.translated.fun_decls.get(id).unwrap(); + decl.signature.drive(&mut graph); } } else { // There may have been errors @@ -507,34 +401,7 @@ fn compute_declarations_graph(ctx: &TransformCtx) -> Deps { } AnyTransId::TraitImpl(id) => { if let Some(d) = ctx.translated.trait_impls.get(*id) { - // Visit the generics and the predicates - graph.visit_generics_and_preds(&d.generics, &d.preds); - - // Visit the implemented trait - graph.visit_trait_decl_id(&d.impl_trait.trait_id); - graph.visit_generic_args(&d.impl_trait.generics); - - // Visit the parent trait refs - for tr in &d.parent_trait_refs { - graph.visit_trait_ref(tr) - } - - // Visit the items - for (_, (ty, id)) in &d.consts { - graph.visit_ty(ty); - graph.visit_global_decl_id(id); - } - - for (_, (trait_refs, ty)) in &d.types { - graph.visit_ty(ty); - for trait_ref in trait_refs { - graph.visit_trait_ref(trait_ref); - } - } - - for (_, id) in d.required_methods.iter().chain(d.provided_methods.iter()) { - graph.visit_fun_decl_id(id) - } + d.drive(&mut graph); } else { // There may have been errors assert!(ctx.has_errors()); @@ -547,8 +414,8 @@ fn compute_declarations_graph(ctx: &TransformCtx) -> Deps { } fn group_declarations_from_scc( - ctx: &TransformCtx, - graph: Deps, + _ctx: &TransformCtx, + graph: Deps<'_, '_>, reordered_sccs: SCCs, ) -> DeclarationsGroups { let reordered_sccs = &reordered_sccs.sccs; @@ -563,54 +430,52 @@ fn group_declarations_from_scc( let id0 = *it.next().unwrap(); let decl = graph.graph.get(&id0).unwrap(); - // The group should consist of only functions, only types or only one global. - for id in scc { + if let AnyTransId::Global(_) = id0 { assert!( - id0.variant_index_arity() == id.variant_index_arity(), - "Invalid scc:\n{}", - scc.iter() - .map(|x| x.fmt_with_ctx(ctx)) - .collect::>() - .join("\n") + scc.len() == 1, + "Error: this constant recursively depends on itself, what is happening" ); } - if let AnyTransId::Global(_) = id0 { - assert!(scc.len() == 1); - } // If an SCC has length one, the declaration may be simply recursive: // we determine whether it is the case by checking if the def id is in // its own set of dependencies. let is_mutually_recursive = scc.len() > 1; let is_simply_recursive = !is_mutually_recursive && decl.contains(&id0); - - // Add the declaration. - // Note that we clone the vectors: it is not optimal, but they should - // be pretty small. let is_rec = is_mutually_recursive || is_simply_recursive; + + let all_same_kind = scc + .iter() + .all(|id| id0.variant_index_arity() == id.variant_index_arity()); + let ids = scc.iter().copied(); let group: DeclarationGroup = match id0 { - AnyTransId::Type(_) => DeclarationGroup::make_type_group( - is_rec, - scc.iter().map(AnyTransId::as_type).copied(), - ), - AnyTransId::Fun(_) => DeclarationGroup::make_fun_group( - is_rec, - scc.iter().map(AnyTransId::as_fun).copied(), - ), - AnyTransId::Global(_) => DeclarationGroup::make_global_group( - is_rec, - scc.iter().map(AnyTransId::as_global).copied(), - ), - AnyTransId::TraitDecl(_) => DeclarationGroup::make_trait_decl_group( - ctx, - is_rec, - scc.iter().map(AnyTransId::as_trait_decl).copied(), - ), - AnyTransId::TraitImpl(_) => DeclarationGroup::make_trait_impl_group( - ctx, - is_rec, - scc.iter().map(AnyTransId::as_trait_impl).copied(), - ), + _ if !all_same_kind => { + DeclarationGroup::Mixed(GDeclarationGroup::make_group(is_rec, ids)) + } + AnyTransId::Type(_) => { + DeclarationGroup::Type(GDeclarationGroup::make_group(is_rec, ids)) + } + AnyTransId::Fun(_) => DeclarationGroup::Fun(GDeclarationGroup::make_group(is_rec, ids)), + AnyTransId::Global(_) => { + DeclarationGroup::Global(GDeclarationGroup::make_group(is_rec, ids)) + } + AnyTransId::TraitDecl(_) => { + let gr: Vec<_> = ids.map(|x| x.try_into().unwrap()).collect(); + // Trait declarations often refer to `Self`, like below, + // which means they are often considered as recursive by our + // analysis. TODO: do something more precise. What is important + // is that we never use the "whole" self clause as argument, + // but rather projections over the self clause (like `::u`, + // in the declaration for `Foo`). + if gr.len() == 1 { + DeclarationGroup::TraitDecl(GDeclarationGroup::NonRec(gr[0])) + } else { + DeclarationGroup::TraitDecl(GDeclarationGroup::Rec(gr)) + } + } + AnyTransId::TraitImpl(_) => { + DeclarationGroup::TraitImpl(GDeclarationGroup::make_group(is_rec, ids)) + } }; reordered_decls.push(group); diff --git a/charon/src/transform/ullbc_to_llbc.rs b/charon/src/transform/ullbc_to_llbc.rs index c8bbb4359..4156984ea 100644 --- a/charon/src/transform/ullbc_to_llbc.rs +++ b/charon/src/transform/ullbc_to_llbc.rs @@ -31,6 +31,7 @@ use crate::ullbc_ast::{self as src}; use crate::values as v; use hashlink::linked_hash_map::LinkedHashMap; use im::Vector; +use itertools::Itertools; use petgraph::algo::floyd_warshall::floyd_warshall; use petgraph::algo::toposort; use petgraph::graphmap::DiGraphMap; @@ -1410,31 +1411,15 @@ fn compute_loop_switch_exits(cfg_info: &CfgInfo) -> ExitInfo { exit_info } -fn combine_statement_and_statement( - statement: Box, - next_st: Option>, -) -> Box { - match next_st { - Some(next_st) => { - let span = combine_span(&statement.span, &next_st.span); - let st = tgt::RawStatement::Sequence(statement, next_st); - Box::new(tgt::Statement::new(span, st)) - } - None => statement, - } -} - fn combine_statements_and_statement( statements: Vec, - next: Option>, -) -> Option> { - statements - .into_iter() - .map(Box::new) - .rev() - .fold(next, |seq, st| { - Some(combine_statement_and_statement(st, seq)) - }) + next: Option, +) -> Option { + if let Some(st) = tgt::Statement::from_seq(statements) { + Some(st.then_opt(next)) + } else { + next + } } fn get_goto_kind( @@ -1482,16 +1467,16 @@ fn translate_child_block( switch_exit_blocks: &im::HashSet, parent_span: Span, child_id: src::BlockId, -) -> Option> { +) -> Option { // Check if this is a backward call match get_goto_kind(info.exits_info, parent_loops, switch_exit_blocks, child_id) { GotoKind::Break(index) => { let st = tgt::RawStatement::Break(index); - Some(Box::new(tgt::Statement::new(parent_span, st))) + Some(tgt::Statement::new(parent_span, st)) } GotoKind::Continue(index) => { let st = tgt::RawStatement::Continue(index); - Some(Box::new(tgt::Statement::new(parent_span, st))) + Some(tgt::Statement::new(parent_span, st)) } // If we are going to an exit block we simply ignore the goto GotoKind::ExitBlock => None, @@ -1504,14 +1489,8 @@ fn translate_child_block( } } -fn opt_statement_to_nop_if_none( - span: Span, - opt_st: Option>, -) -> Box { - match opt_st { - Some(st) => st, - None => Box::new(tgt::Statement::new(span, tgt::RawStatement::Nop)), - } +fn opt_statement_to_nop_if_none(span: Span, opt_st: Option) -> tgt::Statement { + opt_st.unwrap_or_else(|| tgt::Statement::new(span, tgt::RawStatement::Nop)) } fn translate_statement(st: &src::Statement) -> Option { @@ -1543,18 +1522,17 @@ fn translate_terminator( parent_loops: &Vector, switch_exit_blocks: &im::HashSet, terminator: &src::Terminator, -) -> Option> { +) -> Option { let src_span = terminator.span; match &terminator.content { - src::RawTerminator::Abort(kind) => Some(Box::new(tgt::Statement::new( + src::RawTerminator::Abort(kind) => Some(tgt::Statement::new( src_span, tgt::RawStatement::Abort(kind.clone()), - ))), - src::RawTerminator::Return => Some(Box::new(tgt::Statement::new( - src_span, - tgt::RawStatement::Return, - ))), + )), + src::RawTerminator::Return => { + Some(tgt::Statement::new(src_span, tgt::RawStatement::Return)) + } src::RawTerminator::Goto { target } => translate_child_block( info, parent_loops, @@ -1570,11 +1548,8 @@ fn translate_terminator( terminator.span, *target, ); - let st = Box::new(tgt::Statement::new( - src_span, - tgt::RawStatement::Drop(place.clone()), - )); - Some(combine_statement_and_statement(st, opt_child)) + let st = tgt::Statement::new(src_span, tgt::RawStatement::Drop(place.clone())); + Some(st.then_opt(opt_child)) } src::RawTerminator::Call { call, target } => { let opt_child = if let Some(target) = target { @@ -1589,8 +1564,8 @@ fn translate_terminator( None }; let st = tgt::RawStatement::Call(call.clone()); - let st = Box::new(tgt::Statement::new(src_span, st)); - Some(combine_statement_and_statement(st, opt_child)) + let st = tgt::Statement::new(src_span, st); + Some(st.then_opt(opt_child)) } src::RawTerminator::Assert { cond, @@ -1608,8 +1583,8 @@ fn translate_terminator( cond: cond.clone(), expected: *expected, }); - let st = Box::new(tgt::Statement::new(src_span, st)); - Some(combine_statement_and_statement(st, opt_child)) + let st = tgt::Statement::new(src_span, st); + Some(st.then_opt(opt_child)) } src::RawTerminator::Switch { discr, targets } => { // Translate the target expressions @@ -1636,7 +1611,7 @@ fn translate_terminator( let else_exp = opt_statement_to_nop_if_none(terminator.span, else_exp); // Translate - tgt::Switch::If(discr.clone(), then_exp, else_exp) + tgt::Switch::If(discr.clone(), then_exp.into_box(), else_exp.into_box()) } src::SwitchTargets::SwitchInt(int_ty, targets, otherwise) => { // Note that some branches can be grouped together, like @@ -1684,7 +1659,7 @@ fn translate_terminator( // We use the terminator span information in case then // then statement is `None` let exp = opt_statement_to_nop_if_none(terminator.span, exp); - branches.insert(*bid, (vec![*v], *exp)); + branches.insert(*bid, (vec![*v], exp)); } } let targets_exps: Vec<(Vec, tgt::Statement)> = @@ -1703,7 +1678,12 @@ fn translate_terminator( opt_statement_to_nop_if_none(terminator.span, otherwise_exp); // Translate - tgt::Switch::SwitchInt(discr.clone(), *int_ty, targets_exps, otherwise_exp) + tgt::Switch::SwitchInt( + discr.clone(), + *int_ty, + targets_exps, + otherwise_exp.into_box(), + ) } }; @@ -1711,29 +1691,11 @@ fn translate_terminator( let span = tgt::combine_switch_targets_span(&switch); let span = combine_span(&src_span, &span); let st = tgt::RawStatement::Switch(switch); - let st = Box::new(tgt::Statement::new(span, st)); - Some(st) + Some(tgt::Statement::new(span, st)) } } } -fn combine_expressions( - exp1: Option>, - exp2: Option>, -) -> Option> { - match exp1 { - None => exp2, - Some(exp1) => match exp2 { - None => Some(exp1), - Some(exp2) => { - let span = combine_span(&exp1.span, &exp2.span); - let st = tgt::RawStatement::Sequence(exp1, exp2); - Some(Box::new(tgt::Statement::new(span, st))) - } - }, - } -} - fn is_terminal(exp: &tgt::Statement) -> bool { is_terminal_explore(0, exp) } @@ -1756,13 +1718,7 @@ fn is_terminal_explore(num_loops: usize, st: &tgt::Statement) -> bool { tgt::RawStatement::Abort(..) | tgt::RawStatement::Return => true, tgt::RawStatement::Break(index) => *index >= num_loops, tgt::RawStatement::Continue(_index) => true, - tgt::RawStatement::Sequence(st1, st2) => { - if is_terminal_explore(num_loops, st1) { - true - } else { - is_terminal_explore(num_loops, st2) - } - } + tgt::RawStatement::Sequence(seq) => seq.iter().any(|st| is_terminal_explore(num_loops, st)), tgt::RawStatement::Switch(switch) => switch .get_targets() .iter() @@ -1780,7 +1736,7 @@ fn translate_block( parent_loops: &Vector, switch_exit_blocks: &im::HashSet, block_id: src::BlockId, -) -> Option> { +) -> Option { // If the user activated this check: check that we didn't already translate // this block, and insert the block id in the set of already translated blocks. trace!( @@ -1842,60 +1798,44 @@ fn translate_block( translate_terminator(info, nparent_loops, &nswitch_exit_blocks, &block.terminator); // Translate the statements inside the block - let statements = Vec::from_iter(block.statements.iter().filter_map(translate_statement)); - - // We do different things if this is a loop, a switch (which is not - // a loop) or something else. - // Note that we need to do different treatments, because we don't - // concatenate the exit block the same way for loops and switches. - // In particular, for switches, we have to make sure we concatenate - // the exit block *before* concatenating the statements preceding - // the terminator, in order to avoid generating code of the form: - // ``` - // e_prev; (s1; ...: sn; switch ...); e_switch_exit - // ``` - if is_loop { - // Put the statements and the terminator together - let exp = combine_statements_and_statement(statements, terminator); + let statements = block + .statements + .iter() + .filter_map(translate_statement) + .collect_vec(); - // Put the whole loop body inside a `Loop` wrapper - let exp = exp.unwrap(); - let exp = Box::new(tgt::Statement::new(exp.span, tgt::RawStatement::Loop(exp))); + // Prepend the statements to the terminator. + let mut exp = combine_statements_and_statement(statements, terminator); - // Add the exit block - if let Some(exit_block_id) = next_block { - let next_exp = ensure_sufficient_stack(|| { - translate_block(info, parent_loops, switch_exit_blocks, exit_block_id) - }); - combine_expressions(Some(exp), next_exp) - } else { - Some(exp) + if is_loop { + // Put the whole loop body inside a `Loop` wrapper + exp = { + let exp = exp.unwrap(); + Some(tgt::Statement::new( + exp.span, + tgt::RawStatement::Loop(exp.into_box()), + )) } } else if is_switch { - // Use the terminator - let exp = terminator.unwrap(); - - // Concatenate the exit expression, if needs be - let exp = if let Some(exit_block_id) = next_block { + if next_block.is_some() { // Sanity check: if there is an exit block, this block must be // reachable (i.e, there must exist a path in the switch which // doesn't end with `panic`, `return`, etc.). - assert!(!is_terminal(&exp)); - - let next_exp = ensure_sufficient_stack(|| { - translate_block(info, parent_loops, switch_exit_blocks, exit_block_id) - }); - combine_expressions(Some(exp), next_exp) - } else { - Some(exp) - }; - - // Concatenate the statements - combine_statements_and_statement(statements, exp) + assert!(!is_terminal(exp.as_ref().unwrap())); + } } else { - // Simply concatenate the statements and the terminator - combine_statements_and_statement(statements, terminator) + assert!(next_block.is_none()); + } + + // Concatenate the exit expression, if needs be + if let Some(exit_block_id) = next_block { + let next_exp = ensure_sufficient_stack(|| { + translate_block(info, parent_loops, switch_exit_blocks, exit_block_id) + }); + exp = Some(exp.unwrap().then_opt(next_exp)); } + + exp } fn translate_body_aux(no_code_duplication: bool, src_body: &src::ExprBody) -> tgt::ExprBody { @@ -1923,7 +1863,7 @@ fn translate_body_aux(no_code_duplication: bool, src_body: &src::ExprBody) -> tg exits_info: &exits_info, explored: &mut explored, }; - let stmt = translate_block( + let tgt_body = translate_block( &mut info, &Vector::new(), &im::HashSet::new(), @@ -1940,7 +1880,7 @@ fn translate_body_aux(no_code_duplication: bool, src_body: &src::ExprBody) -> tg span: src_body.span, arg_count: src_body.arg_count, locals: src_body.locals.clone(), - body: *stmt, + body: tgt_body, } } diff --git a/charon/src/transform/update_closure_signatures.rs b/charon/src/transform/update_closure_signatures.rs index 51c0e2eed..3c7294739 100644 --- a/charon/src/transform/update_closure_signatures.rs +++ b/charon/src/transform/update_closure_signatures.rs @@ -1,6 +1,8 @@ //! # Micro-pass: the first local variable of closures is (a borrow to) the //! closure itself. This is not consistent with the closure signature, //! which ignores this first variable. This micro-pass updates this. +use derive_visitor::{visitor_enter_fn_mut, DriveMut, VisitorMut}; + use crate::common::*; use crate::ids::Vector; use crate::llbc_ast::*; @@ -9,15 +11,17 @@ use crate::types::*; use super::ctx::LlbcPass; +#[derive(VisitorMut)] +#[visitor(Region(exit), Ty(enter, exit))] struct InsertRegions<'a> { regions: &'a mut Vector, - /// The number of region groups we dived into (we don't count the regions - /// at the declaration level). We use this for the DeBruijn indices. + // The number of region groups we dived into (we don't count the regions + // at the declaration level). We use this for the DeBruijn indices. depth: usize, } -impl<'a> MutTypeVisitor for InsertRegions<'a> { - fn visit_region(&mut self, r: &mut Region) { +impl<'a> InsertRegions<'a> { + fn exit_region(&mut self, r: &mut Region) { if r == &Region::Erased { // Insert a fresh region let index = self @@ -27,35 +31,19 @@ impl<'a> MutTypeVisitor for InsertRegions<'a> { } } - fn enter_region_group( - &mut self, - _regions: &mut Vector, - visitor: &mut dyn FnMut(&mut Self), - ) { - self.depth += 1; - visitor(self); - self.depth -= 1; + fn enter_ty(&mut self, ty: &mut Ty) { + if let Ty::Arrow(..) = ty { + self.depth += 1; + } } -} -struct ClosureStateAccess { - num_fields: usize, -} - -impl MutTypeVisitor for ClosureStateAccess {} - -impl MutExprVisitor for ClosureStateAccess { - fn visit_projection_elem(&mut self, pe: &mut ProjectionElem) { - if let ProjectionElem::Field(pk @ FieldProjKind::ClosureState, _) = pe { - *pk = FieldProjKind::Tuple(self.num_fields); - } else { - self.default_visit_projection_elem(pe) + fn exit_ty(&mut self, ty: &mut Ty) { + if let Ty::Arrow(..) = ty { + self.depth -= 1; } } } -impl MutAstVisitor for ClosureStateAccess {} - fn transform_function( _ctx: &TransformCtx, def: &mut FunDecl, @@ -107,7 +95,7 @@ fn transform_function( regions: &mut generics.regions, depth: 0, }; - visitor.visit_ty(&mut state); + state.drive_mut(&mut visitor); // Update the inputs (slightly annoying to push to the front of // a vector...). @@ -148,8 +136,12 @@ fn transform_function( state_var.name = Some("state".to_string()); // Update the body, and in particular the accesses to the states - let mut visitor = ClosureStateAccess { num_fields }; - visitor.visit_statement(&mut body.body); + body.body + .drive_mut(&mut visitor_enter_fn_mut(|pe: &mut ProjectionElem| { + if let ProjectionElem::Field(pk @ FieldProjKind::ClosureState, _) = pe { + *pk = FieldProjKind::Tuple(num_fields); + } + })); } Ok(()) diff --git a/charon/src/translate/translate_crate_to_ullbc.rs b/charon/src/translate/translate_crate_to_ullbc.rs index 54d38a607..5762bfc98 100644 --- a/charon/src/translate/translate_crate_to_ullbc.rs +++ b/charon/src/translate/translate_crate_to_ullbc.rs @@ -3,62 +3,16 @@ use crate::common::*; use crate::get_mir::{extract_constants_at_top_level, MirLevel}; use crate::transform::TransformCtx; use crate::translate_ctx::*; -use crate::translate_functions_to_ullbc; use hax_frontend_exporter as hax; use hax_frontend_exporter::SInto; use rustc_hir::def_id::DefId; -use rustc_hir::{Defaultness, ForeignItemKind, ImplItem, ImplItemKind, Item, ItemKind}; +use rustc_hir::{ForeignItemKind, ImplItemKind, Item, ItemKind}; use rustc_middle::ty::TyCtxt; use rustc_session::Session; use std::collections::{HashMap, HashSet}; impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { - fn register_local_hir_impl_item(&mut self, _top_item: bool, impl_item: &ImplItem) { - // TODO: make a proper error message - assert!(impl_item.defaultness == Defaultness::Final); - - let def_id = impl_item.owner_id.to_def_id(); - - // Match on the impl item kind - match &impl_item.kind { - ImplItemKind::Const(_, _) => { - // Can happen in traits: - // ``` - // trait Foo { - // const C : usize; - // } - // - // impl Foo for Bar { - // const C = 32; // HERE - // } - // ``` - let _ = self.register_global_decl_id(&None, def_id); - } - ImplItemKind::Type(_) => { - // Trait type: - // ``` - // trait Foo { - // type T; - // } - // - // impl Foo for Bar { - // type T = bool; // HERE - // } - // ``` - // - // Do nothing for now: we won't generate a top-level definition - // for this, and handle it when translating the trait implementation - // this item belongs to. - let tcx = self.tcx; - assert!(tcx.associated_item(def_id).trait_item_def_id.is_some()); - } - ImplItemKind::Fn(_, _) => { - let _ = self.register_fun_decl_id(&None, def_id); - } - } - } - /// General function to register a MIR item. It is called on all the top-level /// items. This includes: crate inclusions and `use` instructions (which are /// ignored), but also type and functions declarations. @@ -146,8 +100,18 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { ItemKind::Impl(impl_block) => { trace!("impl"); - // Sanity checks - TODO: remove? - translate_functions_to_ullbc::check_impl_item(impl_block); + // Sanity checks + // TODO: make proper error messages + use rustc_hir::{Defaultness, ImplPolarity, Unsafety}; + assert!(impl_block.unsafety == Unsafety::Normal); + // About polarity: + // [https://doc.rust-lang.org/beta/unstable-book/language-features/negative-impls.html] + // Not sure about what I should do about it. Should I do anything, actually? + // This seems useful to enforce some discipline on the user-side, but not + // necessary for analysis purposes. + assert!(impl_block.polarity == ImplPolarity::Positive); + // Not sure what this is about + assert!(impl_block.defaultness == Defaultness::Final); // If this is a trait implementation, register it if self.tcx.trait_id_of_impl(def_id).is_some() { @@ -161,7 +125,48 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // we need to look it up let impl_item = hir_map.impl_item(impl_item_ref.id); - self.register_local_hir_impl_item(false, impl_item); + // TODO: make a proper error message + assert!(impl_item.defaultness == Defaultness::Final); + + let def_id = impl_item.owner_id.to_def_id(); + + // Match on the impl item kind + match &impl_item.kind { + ImplItemKind::Const(_, _) => { + // Can happen in traits: + // ``` + // trait Foo { + // const C : usize; + // } + // + // impl Foo for Bar { + // const C = 32; // HERE + // } + // ``` + let _ = self.register_global_decl_id(&None, def_id); + } + ImplItemKind::Type(_) => { + // Trait type: + // ``` + // trait Foo { + // type T; + // } + // + // impl Foo for Bar { + // type T = bool; // HERE + // } + // ``` + // + // Do nothing for now: we won't generate a top-level definition + // for this, and handle it when translating the trait implementation + // this item belongs to. + let tcx = self.tcx; + assert!(tcx.associated_item(def_id).trait_item_def_id.is_some()); + } + ImplItemKind::Fn(_, _) => { + let _ = self.register_fun_decl_id(&None, def_id); + } + } } Ok(()) } diff --git a/charon/src/translate/translate_ctx.rs b/charon/src/translate/translate_ctx.rs index dcb2a6eee..f40bd7ded 100644 --- a/charon/src/translate/translate_ctx.rs +++ b/charon/src/translate/translate_ctx.rs @@ -1,18 +1,19 @@ //! The translation contexts. use crate::common::*; -use crate::formatter::{DeclFormatter, FmtCtx, Formatter, IntoFormatter}; +use crate::formatter::{FmtCtx, Formatter, IntoFormatter}; use crate::gast::*; use crate::get_mir::MirLevel; use crate::ids::{Generator, MapGenerator, Vector}; use crate::meta::{self, Attribute, ItemMeta, RawSpan}; use crate::meta::{FileId, FileName, InlineAttr, LocalFileId, Span, VirtualFileId}; use crate::names::Name; -use crate::reorder_decls::{DeclarationGroup, DeclarationsGroups, GDeclarationGroup}; +use crate::reorder_decls::DeclarationsGroups; use crate::translate_predicates::NonLocalTraitClause; use crate::translate_traits::ClauseTransCtx; use crate::types::*; use crate::ullbc_ast as ast; use crate::values::*; +use derive_visitor::{Drive, DriveMut}; use hax_frontend_exporter as hax; use hax_frontend_exporter::SInto; use linked_hash_set::LinkedHashSet; @@ -22,6 +23,7 @@ use rustc_hir::def_id::DefId; use rustc_hir::Node as HirNode; use rustc_middle::ty::TyCtxt; use rustc_session::Session; +use serde::{Deserialize, Serialize}; use std::cmp::{Ord, Ordering, PartialOrd}; use std::collections::{BTreeMap, HashMap, HashSet, VecDeque}; use std::fmt; @@ -83,6 +85,11 @@ impl DepSource { /// The id of a translated item. #[derive( + Copy, + Clone, + Debug, + PartialOrd, + Ord, PartialEq, Eq, Hash, @@ -90,11 +97,10 @@ impl DepSource { EnumAsGetters, VariantName, VariantIndexArity, - Copy, - Clone, - Debug, - PartialOrd, - Ord, + Serialize, + Deserialize, + Drive, + DriveMut, )] pub enum AnyTransId { Type(TypeDeclId), @@ -104,6 +110,33 @@ pub enum AnyTransId { TraitImpl(TraitImplId), } +/// Implement `TryFrom` and `From` to convert between an enum and its variants. +macro_rules! wrap_unwrap_enum { + ($enum:ident::$variant:ident($variant_ty:ident)) => { + impl TryFrom<$enum> for $variant_ty { + type Error = (); + fn try_from(x: $enum) -> Result { + match x { + $enum::$variant(x) => Ok(x), + _ => Err(()), + } + } + } + + impl From<$variant_ty> for $enum { + fn from(x: $variant_ty) -> Self { + $enum::$variant(x) + } + } + }; +} + +wrap_unwrap_enum!(AnyTransId::Fun(FunDeclId)); +wrap_unwrap_enum!(AnyTransId::Global(GlobalDeclId)); +wrap_unwrap_enum!(AnyTransId::Type(TypeDeclId)); +wrap_unwrap_enum!(AnyTransId::TraitDecl(TraitDeclId)); +wrap_unwrap_enum!(AnyTransId::TraitImpl(TraitImplId)); + /// We use a special type to store the Rust identifiers in the stack, to /// make sure we translate them in a specific order (top-level constants /// before constant functions before functions...). This allows us to @@ -136,7 +169,7 @@ impl PartialOrd for OrdRustId { let (vid0, _) = self.variant_index_arity(); let (vid1, _) = other.variant_index_arity(); if vid0 != vid1 { - Some(vid0.cmp(&vid1)) + Option::Some(vid0.cmp(&vid1)) } else { let id0 = self.get_id(); let id1 = other.get_id(); @@ -310,13 +343,7 @@ pub(crate) struct BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// `ImplExprAtom::LocalBound`, we use this to recover the specific trait reference it /// corresponds to. /// FIXME: hax should take care of this matching up. - pub trait_clauses: HashMap>, - /// If [true] it means we are currently registering trait clauses in the - /// local context. As a consequence, we allow not solving all the trait - /// obligations, because the obligations for some clauses may be solved - /// by other clauses which have not been registered yet. - /// For this reason, we do the resolution in several passes. - pub registering_trait_clauses: bool, + pub trait_clauses: BTreeMap>, /// pub types_outlive: Vec, /// @@ -426,6 +453,71 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { self.translate_span_from_rspan(rspan) } + fn parse_rename_attribute(&mut self, span: Span, attributes: Vec) -> Option { + // Search for rename attributes + let attributes: Vec<(&String, &str)> = attributes + .iter() + .filter_map(|raw_attr| { + raw_attr + .strip_prefix("charon::rename(") + .or(raw_attr.strip_prefix("aeneas::rename(")) + .and_then(|str| str.strip_suffix(")").and_then(|str| Some((raw_attr, str)))) + }) + .collect(); + + // Check if there is a rename attribute + if attributes.len() == 0 { + return None; + } + + // We don't allow giving several rename attributes + if attributes.len() > 1 { + self.span_err( + span, + "There shouldn't be more than one `charon::rename(\"...\")` or `aeneas::rename(\"...\")` attribute per declaration", + ); + return None; + } + + // There is exactly one attribute: retrieve it + let (raw_attr, str) = attributes.get(0).unwrap(); + let str = str + .strip_prefix("\"") + .and_then(|str| str.strip_suffix("\"")); + + // The name should be between quotation marks + if str.is_none() { + self.span_err( + span, + &format!("Attribute `{{charon,aeneas}}::rename` should be of the shape `{{charon,aeneas}}::rename(\"...\")`: `{raw_attr}` is not valid"), + ); + return None; + } + let str = str.unwrap(); + + // The name shouldn't be empty + if str.is_empty() { + self.span_err( + span, + "Attribute `{charon,aeneas}::rename` should not contain an empty string", + ); + return None; + } + + // Check that the name starts with a letter, and only contains alphanumeric + // characters or '_' + let first_char = str.chars().nth(0).unwrap(); + let first_char_ok = first_char.is_alphabetic() || first_char == '_'; + let is_identifier = first_char_ok && str.chars().all(|c| c.is_alphanumeric() || c == '_'); + if !is_identifier { + self.span_err(span, &format!("Attribute `rename` should only contain alphanumeric characters and `_`, and should start with a letter or '_': \"{str}\" is not a valid name")); + return None; + } + + // Ok: we can return the attribute + return Some(str.to_string()); + } + /// Compute the meta information for a Rust item identified by its id. pub(crate) fn translate_item_meta_from_rid(&mut self, def_id: DefId) -> ItemMeta { let span = self.translate_span_from_rid(def_id); @@ -437,12 +529,14 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { let opaque = attributes .iter() .any(|attr| attr == "charon::opaque" || attr == "aeneas::opaque"); + let rename = self.parse_rename_attribute(span, attributes.clone()); ItemMeta { span, - attributes: attributes, + attributes, inline: self.translate_inline_from_rid(def_id), public, opaque, + rename, } } @@ -580,7 +674,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { | TraitAlias | TyAlias { .. } | Union - | Use => Some(self.tcx.visibility(id).is_public()), + | Use + | Variant => Some(self.tcx.visibility(id).is_public()), // These kinds don't have visibility modifiers (which would cause `visibility` to panic). Closure | Impl { .. } => None, // Kinds we shouldn't be calling this function on. @@ -595,8 +690,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { | InlineConst | LifetimeParam | OpaqueTy - | TyParam - | Variant => { + | TyParam => { register_error_or_panic!( self, span, @@ -750,7 +844,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// Create a new `ExecContext`. pub(crate) fn new(def_id: DefId, t_ctx: &'ctx mut TranslateCtx<'tcx, 'ctx1>) -> Self { - let hax_state = t_ctx.make_hax_state_with_id(def_id); + let hax_state = hax::State::new_from_state_and_id(&t_ctx.hax_state, def_id); BodyTransCtx { def_id, t_ctx, @@ -766,7 +860,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { const_generic_vars_map: MapGenerator::new(), clause_translation_context: Default::default(), trait_clauses: Default::default(), - registering_trait_clauses: false, regions_outlive: Vec::new(), types_outlive: Vec::new(), trait_type_constraints: Vec::new(), @@ -948,6 +1041,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { types: self.type_vars.clone(), const_generics: self.const_generic_vars.clone(), trait_clauses: self.get_local_trait_clauses(), + regions_outlive: self.regions_outlive.clone(), + types_outlive: self.types_outlive.clone(), + trait_type_constraints: self.trait_type_constraints.clone(), } } @@ -966,14 +1062,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { clauses.clone() } - pub(crate) fn get_predicates(&self) -> Predicates { - Predicates { - regions_outlive: self.regions_outlive.clone(), - types_outlive: self.types_outlive.clone(), - trait_type_constraints: self.trait_type_constraints.clone(), - } - } - /// We use this when exploring the clauses of a predicate, to introduce /// its parent clauses, etc. in the context. We temporarily replace the /// trait instance id generator so that the continuation registers the @@ -1001,19 +1089,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { (out, new_ctx) } - /// Set [registering_trait_clauses] to [true], call the continuation, and - /// reset it to [false] - pub(crate) fn while_registering_trait_clauses(&mut self, f: F) -> T - where - F: FnOnce(&mut Self) -> T, - { - assert!(!self.registering_trait_clauses); - self.registering_trait_clauses = true; - let out = f(self); - self.registering_trait_clauses = false; - out - } - pub(crate) fn make_dep_source(&self, span: rustc_span::Span) -> Option { DepSource::make(self.def_id, span) } @@ -1055,22 +1130,6 @@ impl<'tcx, 'ctx, 'ctx1, 'a> IntoFormatter for &'a BodyTransCtx<'tcx, 'ctx, 'ctx1 } } -impl<'a> FmtCtx<'a> { - fn fmt_decl_group( - &self, - f: &mut fmt::Formatter, - gr: &GDeclarationGroup, - ) -> fmt::Result - where - Self: DeclFormatter, - { - for id in gr.get_ids() { - writeln!(f, "{}\n", self.format_decl(id))? - } - fmt::Result::Ok(()) - } -} - impl<'tcx, 'ctx> fmt::Display for TranslateCtx<'tcx, 'ctx> { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { self.translated.fmt(f) @@ -1101,13 +1160,8 @@ impl fmt::Display for TranslatedCrate { } Some(ordered_decls) => { for gr in ordered_decls { - use DeclarationGroup::*; - match gr { - Type(gr) => fmt.fmt_decl_group(f, gr)?, - Fun(gr) => fmt.fmt_decl_group(f, gr)?, - Global(gr) => fmt.fmt_decl_group(f, gr)?, - TraitDecl(gr) => fmt.fmt_decl_group(f, gr)?, - TraitImpl(gr) => fmt.fmt_decl_group(f, gr)?, + for id in gr.get_ids() { + writeln!(f, "{}\n", fmt.format_decl_id(id))? } } } diff --git a/charon/src/translate/translate_functions_to_ullbc.rs b/charon/src/translate/translate_functions_to_ullbc.rs index 0ea44aed6..3e3fb1132 100644 --- a/charon/src/translate/translate_functions_to_ullbc.rs +++ b/charon/src/translate/translate_functions_to_ullbc.rs @@ -66,21 +66,6 @@ fn translate_unaryop_kind(binop: hax::UnOp) -> UnOp { } } -/// Small utility -pub(crate) fn check_impl_item(impl_item: &rustc_hir::Impl<'_>) { - // TODO: make proper error messages - use rustc_hir::{Defaultness, ImplPolarity, Unsafety}; - assert!(impl_item.unsafety == Unsafety::Normal); - // About polarity: - // [https://doc.rust-lang.org/beta/unstable-book/language-features/negative-impls.html] - // Not sure about what I should do about it. Should I do anything, actually? - // This seems useful to enforce some discipline on the user-side, but not - // necessary for analysis purposes. - assert!(impl_item.polarity == ImplPolarity::Positive); - // Not sure what this is about - assert!(impl_item.defaultness == Defaultness::Final); -} - impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { fn translate_binaryop_kind( &mut self, @@ -1669,34 +1654,33 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { self.set_first_bound_regions_group(bvar_names); let fun_kind = &self.t_ctx.get_item_kind(&dep_src, def_id)?; - // Add the trait clauses - self.while_registering_trait_clauses(move |ctx| { - // Add the ctx trait clause if it is a trait decl item - match fun_kind { - ItemKind::Regular => {} - ItemKind::TraitItemImpl { impl_id, .. } => { - ctx.translate_trait_impl_self_trait_clause(*impl_id)? - } - ItemKind::TraitItemProvided(..) | ItemKind::TraitItemDecl(..) => { - // This is a trait decl item - let trait_id = tcx.trait_of_item(def_id).unwrap(); - ctx.translate_trait_decl_self_trait_clause(trait_id)?; - } + // Add the ctx trait clause if it is a trait decl item + match fun_kind { + ItemKind::Regular => {} + ItemKind::TraitItemImpl { impl_id, .. } => { + self.translate_trait_impl_self_trait_clause(*impl_id)? } - - // Translate the predicates (in particular, the trait clauses) - match &fun_kind { - ItemKind::Regular | ItemKind::TraitItemImpl { .. } => { - ctx.translate_predicates_of(None, def_id)?; - } - ItemKind::TraitItemProvided(trait_decl_id, ..) - | ItemKind::TraitItemDecl(trait_decl_id, ..) => { - ctx.translate_predicates_of(Some(*trait_decl_id), def_id)?; - } + ItemKind::TraitItemProvided(..) | ItemKind::TraitItemDecl(..) => { + // This is a trait decl item + let trait_id = tcx.trait_of_item(def_id).unwrap(); + self.translate_trait_decl_self_trait_clause(trait_id)?; } + } - Ok(()) - })?; + // Translate the predicates (in particular, the trait clauses) + match &fun_kind { + ItemKind::Regular | ItemKind::TraitItemImpl { .. } => { + self.translate_predicates_of(None, def_id, PredicateOrigin::WhereClauseOnFn)?; + } + ItemKind::TraitItemProvided(trait_decl_id, ..) + | ItemKind::TraitItemDecl(trait_decl_id, ..) => { + self.translate_predicates_of( + Some(*trait_decl_id), + def_id, + PredicateOrigin::WhereClauseOnFn, + )?; + } + } // Translate the signature trace!("signature of {def_id:?}:\n{:?}", signature); @@ -1745,7 +1729,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { Ok(FunSig { generics: self.get_generics(), - preds: self.get_predicates(), is_unsafe, is_closure, closure_info, @@ -1858,7 +1841,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // } // ``` bt_ctx.translate_generic_params(rust_id)?; - bt_ctx.translate_predicates_solve_trait_obligations_of(None, rust_id)?; + bt_ctx.translate_predicates_of(None, rust_id, PredicateOrigin::WhereClauseOnFn)?; let hax_state = &bt_ctx.hax_state; @@ -1876,7 +1859,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { .get_item_kind(&DepSource::make(rust_id, span), rust_id)?; let generics = bt_ctx.get_generics(); - let preds = bt_ctx.get_predicates(); // Translate its body like the body of a function. This returns `Opaque if we can't/decide // not to translate this body. @@ -1896,7 +1878,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { is_local: rust_id.is_local(), name, generics, - preds, ty, kind, body: body_id, diff --git a/charon/src/translate/translate_predicates.rs b/charon/src/translate/translate_predicates.rs index 7faa8e518..007d93250 100644 --- a/charon/src/translate/translate_predicates.rs +++ b/charon/src/translate/translate_predicates.rs @@ -39,6 +39,7 @@ pub(crate) struct NonLocalTraitClause { /// [Some] if this is the top clause, [None] if this is about a parent/ /// associated type clause. pub span: Option, + pub origin: PredicateOrigin, pub trait_id: TraitDeclId, pub generics: GenericArgs, } @@ -47,6 +48,7 @@ impl NonLocalTraitClause { pub(crate) fn to_trait_clause_with_id(&self, clause_id: TraitClauseId) -> TraitClause { TraitClause { clause_id, + origin: self.origin.clone(), span: self.span, trait_id: self.trait_id, generics: self.generics.clone(), @@ -124,6 +126,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // a definition: // - [TyCtxt::predicates_defined_on]: returns exactly the list of predicates // that the user has written on the definition: + // FIXME: today's docs say that these includes `outlives` predicates as well // - [TyCtxt::predicates_of]: returns the user defined predicates and also: // - if called on a trait `Foo`, we get an additional trait clause // `Self : Foo` (i.e., the trait requires itself), which is not what we want. @@ -131,25 +134,32 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // information, which the user doesn't have to write by hand (but it doesn't // add those for functions). For instance, below: // ``` - // type MutMut<'a, 'b> { - // x : &'a mut &'b mut u32, + // struct MutMut<'a, 'b, T> { + // x: &'a mut &'b mut T, // } // ``` - // The rust compiler adds the predicate: `'b : 'a` ('b outlives 'a). + // The rust compiler adds the predicates: `'b: 'a` ('b outlives 'a) and `T: 'b`. // For this reason we: // - retrieve the trait predicates with [TyCtxt::predicates_defined_on] // - retrieve the other predicates with [TyCtxt::predicates_of] // // Also, we reorder the predicates to make sure that the trait clauses come - // *before* the other clauses. This way we are sure that, when translating, - // all the trait clauses are in the context if we need them. + // *before* the other clauses. This helps, when translating, with having the trait clauses + // in the context if we need them. // // Example: // ``` - // f, U : Foo>(...) - // ^^^^ - // must make sure we have U : Foo in the context - // before translating this + // fn f, U: Foo>(...) + // ^^^^ must make sure we have U: Foo in the context + // before translating this + // ``` + // There's no perfect ordering though, as this shows: + // ``` + // fn f, U: Foo>(...) + // ^^^^ we'd need to have T: Foo in the context + // before translating this + // ^^^^ we'd need to have U: Foo in the context + // before translating this // ``` let tcx = self.t_ctx.tcx; let param_env = tcx.param_env(def_id); @@ -244,6 +254,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { &mut self, parent_trait_id: Option, def_id: DefId, + origin: PredicateOrigin, ) -> Result<(), Error> { trace!("def_id: {:?}", def_id); let tcx = self.t_ctx.tcx; @@ -260,11 +271,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { trace!("Predicates of parent ({:?}): {:?}", parent_id, preds); if let Some(trait_id) = parent_trait_id { - self.with_parent_trait_clauses(trait_id, &mut |ctx: &mut Self| { - ctx.translate_predicates(&preds) + self.with_parent_trait_clauses(trait_id, |ctx: &mut Self| { + // TODO: distinguish where clauses from supertraits. + ctx.translate_predicates(&preds, PredicateOrigin::WhereClauseOnTrait) })?; } else { - self.translate_predicates(&preds)?; + self.translate_predicates(&preds, PredicateOrigin::WhereClauseOnImpl)?; } } } @@ -286,7 +298,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // The predicates of the current definition let preds = self.get_predicates_of(def_id)?; trace!("Local predicates of {:?}:\n{:?}", def_id, preds); - self.translate_predicates(&preds)?; + self.translate_predicates(&preds, origin)?; let fmt_ctx = self.into_fmt(); let clauses = self @@ -304,33 +316,22 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { Ok(()) } - /// Translate the predicates then solve the unsolved trait obligations - /// in the registered trait clauses. - pub(crate) fn translate_predicates_solve_trait_obligations_of( - &mut self, - parent_trait_id: Option, - def_id: DefId, - ) -> Result<(), Error> { - self.while_registering_trait_clauses(move |ctx| { - ctx.translate_predicates_of(parent_trait_id, def_id)?; - Ok(()) - }) - } - pub(crate) fn translate_predicates( &mut self, preds: &hax::GenericPredicates, + origin: PredicateOrigin, ) -> Result<(), Error> { - self.translate_predicates_vec(&preds.predicates) + self.translate_predicates_vec(&preds.predicates, origin) } pub(crate) fn translate_predicates_vec( &mut self, preds: &Vec<(hax::Predicate, hax::Span)>, + origin: PredicateOrigin, ) -> Result<(), Error> { trace!("Predicates:\n{:?}", preds); for (pred, span) in preds { - match self.translate_predicate(pred, span)? { + match self.translate_predicate(pred, span, origin.clone())? { None => (), Some(pred) => match pred { Predicate::Trait(_) => { @@ -375,15 +376,18 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// Returns an [Option] because we may filter clauses about builtin or /// auto traits like [core::marker::Sized] and [core::marker::Sync]. + /// + /// `origin` is where this clause comes from. pub(crate) fn translate_trait_clause( &mut self, hspan: &hax::Span, trait_pred: &hax::TraitPredicate, + origin: PredicateOrigin, ) -> Result, Error> { // FIXME: once `clause` can't be `None`, use |Vector::reserve_slot` to be sure we don't use // the same id twice. let (clause_id, instance_id) = self.clause_translation_context.generate_instance_id(); - let clause = self.translate_trait_clause_aux(hspan, trait_pred, instance_id)?; + let clause = self.translate_trait_clause_aux(hspan, trait_pred, instance_id, origin)?; if let Some(clause) = clause { let local_clause = clause.to_trait_clause_with_id(clause_id); self.clause_translation_context @@ -407,7 +411,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { trait_pred: &hax::TraitPredicate, ) -> Result<(), Error> { // Save the self clause (and its parent/item clauses) - let clause = self.translate_trait_clause_aux(span, &trait_pred, TraitInstanceId::SelfId)?; + let clause = self.translate_trait_clause_aux( + span, + &trait_pred, + TraitInstanceId::SelfId, + PredicateOrigin::TraitSelf, + )?; if let Some(clause) = clause { self.trait_clauses .entry(clause.trait_id) @@ -422,6 +431,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { hspan: &hax::Span, trait_pred: &hax::TraitPredicate, clause_id: TraitInstanceId, + origin: PredicateOrigin, ) -> Result, Error> { // Note sure what this is about assert!(trait_pred.is_positive); @@ -449,6 +459,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { Ok(Some(NonLocalTraitClause { clause_id, span: Some(span), + origin, trait_id, generics, })) @@ -458,6 +469,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { &mut self, pred: &hax::Predicate, hspan: &hax::Span, + origin: PredicateOrigin, ) -> Result, Error> { trace!("{:?}", pred); // Predicates are always used in signatures/type definitions, etc. @@ -474,7 +486,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { PredicateKind::Clause(kind) => { match kind { ClauseKind::Trait(trait_pred) => Ok(self - .translate_trait_clause(hspan, trait_pred)? + .translate_trait_clause(hspan, trait_pred, origin)? .map(Predicate::Trait)), ClauseKind::RegionOutlives(p) => { let r0 = self.translate_region(span, erase_regions, &p.lhs)?; @@ -818,41 +830,37 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // Could not find a clause. // Check if we are in the registration process, otherwise report an error. // TODO: we might be registering a where clause. - if self.registering_trait_clauses { - TraitInstanceId::Unsolved(trait_id, generics.clone()) + let fmt_ctx = self.into_fmt(); + let trait_ref = format!( + "{}{}", + fmt_ctx.format_object(trait_id), + generics.fmt_with_ctx(&fmt_ctx) + ); + let clauses: Vec = self + .trait_clauses + .values() + .flat_map(|x| x) + .map(|x| x.fmt_with_ctx(&fmt_ctx)) + .collect(); + + if !self.t_ctx.continue_on_failure() { + let clauses = clauses.join("\n"); + unreachable!( + "Could not find a clause for parameter:\n- target param: {}\n- available clauses:\n{}\n- context: {:?}", + trait_ref, clauses, self.def_id + ); } else { - let fmt_ctx = self.into_fmt(); - let trait_ref = format!( - "{}{}", - fmt_ctx.format_object(trait_id), - generics.fmt_with_ctx(&fmt_ctx) + // Return the UNKNOWN clause + log::warn!( + "Could not find a clause for parameter:\n- target param: {}\n- available clauses:\n{}\n- context: {:?}", + trait_ref, clauses.join("\n"), self.def_id ); - let clauses: Vec = self - .trait_clauses - .values() - .flat_map(|x| x) - .map(|x| x.fmt_with_ctx(&fmt_ctx)) - .collect(); - - if !self.t_ctx.continue_on_failure() { - let clauses = clauses.join("\n"); - unreachable!( - "Could not find a clause for parameter:\n- target param: {}\n- available clauses:\n{}\n- context: {:?}", - trait_ref, clauses, self.def_id - ); - } else { - // Return the UNKNOWN clause - log::warn!( - "Could not find a clause for parameter:\n- target param: {}\n- available clauses:\n{}\n- context: {:?}", - trait_ref, clauses.join("\n"), self.def_id - ); - TraitInstanceId::Unknown(format!( - "Could not find a clause for parameter: {} (available clauses: {}) (context: {:?})", - trait_ref, - clauses.join("; "), - self.def_id - )) - } + TraitInstanceId::Unknown(format!( + "Could not find a clause for parameter: {} (available clauses: {}) (context: {:?})", + trait_ref, + clauses.join("; "), + self.def_id + )) } } } diff --git a/charon/src/translate/translate_traits.rs b/charon/src/translate/translate_traits.rs index 2b0fb4272..3e77bc821 100644 --- a/charon/src/translate/translate_traits.rs +++ b/charon/src/translate/translate_traits.rs @@ -221,7 +221,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { pub(crate) fn with_parent_trait_clauses( &mut self, trait_decl_id: TraitDeclId, - f: &mut dyn FnMut(&mut Self) -> Result<(), Error>, + f: impl FnOnce(&mut Self) -> Result<(), Error>, ) -> Result, Error> { let (out, ctx) = self.with_clause_translation_context( ClauseTransCtx::Parent(Default::default(), trait_decl_id), @@ -235,7 +235,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { &mut self, trait_decl_id: TraitDeclId, item_name: TraitItemName, - f: &mut dyn FnMut(&mut Self) -> Result<(), Error>, + f: impl FnOnce(&mut Self) -> Result<(), Error>, ) -> Result, Error> { let (out, ctx) = self.with_clause_translation_context( ClauseTransCtx::Item(Default::default(), trait_decl_id, item_name), @@ -274,18 +274,13 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { bt_ctx.translate_generic_params(rust_id)?; // Add the trait clauses - let parent_clauses = bt_ctx.while_registering_trait_clauses(move |bt_ctx| { - // Add the self trait clause - bt_ctx.translate_trait_decl_self_trait_clause(rust_id)?; - - // Translate the predicates. - bt_ctx.with_parent_trait_clauses(def_id, &mut |s| { - s.translate_predicates_of(None, rust_id) - }) - })?; + // Add the self trait clause + bt_ctx.translate_trait_decl_self_trait_clause(rust_id)?; - // TODO: move this below (we don't need to perform this function call exactly here) - let preds = bt_ctx.get_predicates(); + // Translate the predicates. + let parent_clauses = bt_ctx.with_parent_trait_clauses(def_id, |s| { + s.translate_predicates_of(None, rust_id, PredicateOrigin::WhereClauseOnTrait) + })?; // Explore the associated items // We do something subtle here: TODO: explain @@ -347,10 +342,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { .map(|x| (x.as_predicate(), span)) .collect(); let bounds = bounds.sinto(&bt_ctx.hax_state); + let origin = PredicateOrigin::TraitItem(item_name.clone()); // Register the trait clauses as item trait clauses - bt_ctx.with_item_trait_clauses(def_id, item_name.clone(), &mut |s| { - s.translate_predicates_vec(&bounds) + bt_ctx.with_item_trait_clauses(def_id, item_name.clone(), |s| { + s.translate_predicates_vec(&bounds, origin) })? }; @@ -415,7 +411,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { name, item_meta, generics, - preds, parent_clauses, consts, types, @@ -442,16 +437,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // Translate the generics bt_ctx.translate_generic_params(rust_id)?; - // Add the trait self clauses - bt_ctx.while_registering_trait_clauses(move |bt_ctx| { - // Translate the predicates - bt_ctx.translate_predicates_of(None, rust_id)?; + // Translate the predicates + bt_ctx.translate_predicates_of(None, rust_id, PredicateOrigin::WhereClauseOnImpl)?; - // Add the self trait clause - bt_ctx.translate_trait_impl_self_trait_clause(def_id)?; - - Ok(()) - })?; + // Add the self trait clause + bt_ctx.translate_trait_impl_self_trait_clause(def_id)?; // Retrieve the information about the implemented trait. let ( @@ -630,7 +620,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { item_meta, impl_trait: implemented_trait, generics: bt_ctx.get_generics(), - preds: bt_ctx.get_predicates(), parent_trait_refs, consts, types, diff --git a/charon/src/translate/translate_types.rs b/charon/src/translate/translate_types.rs index 28715312c..b464c09ac 100644 --- a/charon/src/translate/translate_types.rs +++ b/charon/src/translate/translate_types.rs @@ -582,7 +582,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { for (j, field_def) in var_def.fields.into_iter().enumerate() { trace!("variant {i}: field {j}: {field_def:?}"); let field_span = field_def.span.rust_span_data.unwrap().span(); - + let field_meta = self + .t_ctx + .translate_item_meta_from_rid(DefId::from(&field_def.did)); // Translate the field type let ty = self.translate_ty(field_span, erase_regions, &field_def.ty)?; @@ -601,22 +603,21 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } }; - // Translate the span information - let span = self.translate_span_from_rspan(field_def.span); - // Store the field let field = Field { - span, + item_meta: field_meta, name: field_name.clone(), ty, }; fields.push(field); } - let span = self.translate_span_from_rspan(var_def.span); + let variant_meta = self + .t_ctx + .translate_item_meta_from_rid(DefId::from(&var_def.def_id)); let variant_name = var_def.name; variants.push(Variant { - span, + item_meta: variant_meta, name: variant_name, fields, discriminant, @@ -738,7 +739,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { bt_ctx.translate_generic_params(rust_id)?; // Translate the predicates - bt_ctx.translate_predicates_solve_trait_obligations_of(None, rust_id)?; + bt_ctx.translate_predicates_of(None, rust_id, PredicateOrigin::WhereClauseOnType)?; // Translate the meta information let item_meta = bt_ctx.t_ctx.translate_item_meta_from_rid(rust_id); @@ -769,12 +770,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { is_local: rust_id.is_local(), name, generics, - preds: bt_ctx.get_predicates(), kind, }; - trace!("translate_type: preds: {:?}", &type_def.preds); - trace!( "{} -> {}", trans_id.to_string(), diff --git a/charon/tests/cargo.rs b/charon/tests/cargo.rs index 1b2719350..5f5087b5f 100644 --- a/charon/tests/cargo.rs +++ b/charon/tests/cargo.rs @@ -70,7 +70,11 @@ fn cargo() -> Result<(), Box> { }; let tests = vec![ mktest("build-script", root.join("build-script"), &[]), - mktest("dependencies", root.join("dependencies"), &[]), + mktest( + "dependencies", + root.join("dependencies"), + &["--cargo-arg=--features=test_feature".to_owned()], + ), mktest("toml", root.join("toml"), &[]), mktest( "workspace", diff --git a/charon/tests/cargo/dependencies/Cargo.toml b/charon/tests/cargo/dependencies/Cargo.toml index 2abf34833..024f7f992 100644 --- a/charon/tests/cargo/dependencies/Cargo.toml +++ b/charon/tests/cargo/dependencies/Cargo.toml @@ -8,4 +8,9 @@ edition = "2021" # Important: because of how we use Nix, only the dependencies of charon itself # will be available when running tests. So the only dependencies we can list # here must be in `charon/Cargo.toml`. -take_mut = "0.2.2" +take_mut = { version = "0.2.2", optional = true } + +[features] +default = [] +# We activate this feature by calling charon with `--cargo-arg=--features=test_feature`. +test_feature = [ "dep:take_mut" ] diff --git a/charon/tests/crate_data.rs b/charon/tests/crate_data.rs index 48ad4d5c5..6768a7f79 100644 --- a/charon/tests/crate_data.rs +++ b/charon/tests/crate_data.rs @@ -1,16 +1,14 @@ #![feature(rustc_private)] +#![feature(lint_reasons)] use assert_cmd::prelude::{CommandCargoExt, OutputAssertExt}; use itertools::Itertools; +use macros::EnumAsGetters; +use std::collections::HashMap; use std::{error::Error, fs::File, io::BufReader, process::Command}; use charon_lib::{ - export::CrateData, - logger, - meta::InlineAttr, - names::{Name, PathElem}, - types::TypeDecl, - values::ScalarValue, + export::CrateData, gast::*, logger, meta::*, names::*, types::*, values::ScalarValue, }; fn translate(code: impl std::fmt::Display) -> Result> { @@ -49,16 +47,105 @@ fn translate(code: impl std::fmt::Display) -> Result> } /// `Name` is a complex datastructure; to inspect it we serialize it a little bit. -fn repr_name(n: &Name) -> String { +fn repr_name(crate_data: &CrateData, n: &Name) -> String { n.name .iter() .map(|path_elem| match path_elem { - PathElem::Ident(i, _) => i, - PathElem::Impl(_) => "", + PathElem::Ident(i, _) => i.clone(), + PathElem::Impl(elem) => match &elem.kind { + ImplElemKind::Trait(trait_ref) => { + let trait_name = trait_name(crate_data, trait_ref.trait_id); + format!("") + } + ImplElemKind::Ty(..) => "".to_string(), + }, }) .join("::") } +fn repr_span(span: Span) -> String { + let raw_span = span.span; + format!("{}-{}", raw_span.beg, raw_span.end) +} + +fn trait_name(crate_data: &CrateData, trait_id: TraitDeclId) -> &str { + let tr = &crate_data.trait_decls[trait_id.index()]; + let PathElem::Ident(trait_name, _) = tr.name.name.last().unwrap() else { + panic!() + }; + trait_name +} + +#[derive(EnumAsGetters)] +enum ItemKind<'c> { + Fun(&'c FunDecl), + Global(&'c GlobalDecl), + Type(&'c TypeDecl), + TraitDecl(&'c TraitDecl), + TraitImpl(&'c TraitImpl), +} + +/// A general item, with information shared by all items. +#[expect(dead_code)] +struct Item<'c> { + name: &'c Name, + name_str: String, + item_meta: &'c ItemMeta, + // Not a ref because we do a little hack. + generics: GenericParams, + kind: ItemKind<'c>, +} + +/// Get all the items for this crate. +fn items_by_name<'c>(crate_data: &'c CrateData) -> HashMap> { + crate_data + .functions + .iter() + .map(|x| Item { + name: &x.name, + name_str: repr_name(crate_data, &x.name), + item_meta: &x.item_meta, + generics: x.signature.generics.clone(), + kind: ItemKind::Fun(x), + }) + .chain(crate_data.globals.iter().map(|x| Item { + name: &x.name, + name_str: repr_name(crate_data, &x.name), + item_meta: &x.item_meta, + generics: x.generics.clone(), + kind: ItemKind::Global(x), + })) + .chain(crate_data.types.iter().map(|x| Item { + name: &x.name, + name_str: repr_name(crate_data, &x.name), + item_meta: &x.item_meta, + generics: x.generics.clone(), + kind: ItemKind::Type(x), + })) + .chain(crate_data.trait_impls.iter().map(|x| Item { + name: &x.name, + name_str: repr_name(crate_data, &x.name), + item_meta: &x.item_meta, + generics: x.generics.clone(), + kind: ItemKind::TraitImpl(x), + })) + .chain(crate_data.trait_decls.iter().map(|x| { + let mut generics = x.generics.clone(); + // We do a little hack. + assert!(generics.trait_clauses.is_empty()); + generics.trait_clauses = x.parent_clauses.clone(); + Item { + name: &x.name, + name_str: repr_name(crate_data, &x.name), + item_meta: &x.item_meta, + generics, + kind: ItemKind::TraitDecl(x), + } + })) + .map(|item| (item.name_str.clone(), item)) + .collect() +} + #[test] fn type_decl() -> Result<(), Box> { let crate_data = translate( @@ -67,7 +154,175 @@ fn type_decl() -> Result<(), Box> { fn main() {} ", )?; - assert_eq!(repr_name(&crate_data.types[0].name), "test_crate::Struct"); + assert_eq!( + repr_name(&crate_data, &crate_data.types[0].name), + "test_crate::Struct" + ); + Ok(()) +} + +#[test] +fn file_name() -> Result<(), Box> { + let crate_data = translate( + " + type Foo = Option<()>; + ", + )?; + assert_eq!( + repr_name(&crate_data, &crate_data.types[0].name), + "test_crate::Foo" + ); + assert_eq!( + repr_name(&crate_data, &crate_data.types[1].name), + "core::option::Option" + ); + let file_id = crate_data.types[1].item_meta.span.span.file_id; + let (_, file) = crate_data + .id_to_file + .iter() + .find(|(i, _)| *i == file_id) + .unwrap(); + let FileName::Virtual(file) = file else { + panic!() + }; + assert_eq!(file.to_str().unwrap(), "/rustc/library/core/src/option.rs"); + Ok(()) +} + +#[test] +fn spans() -> Result<(), Box> { + let crate_data = translate( + " + pub fn sum(s: &[u32]) -> u32 { + let mut sum = 0; + let mut i = 0; + while i < s.len() { + sum += s[i]; + i += 1; + } + sum + } + ", + )?; + let function = &crate_data.functions[0]; + // Span of the function signature. + assert_eq!(repr_span(function.item_meta.span), "2:8-2:36"); + let body_id = function.body.unwrap(); + let body = &crate_data.bodies[body_id].as_structured().unwrap().body; + // The whole function declaration. + assert_eq!(repr_span(body.span), "2:8-10:9"); + let seq = body.clone().into_sequence(); + let the_loop = seq.iter().find(|st| st.content.is_loop()).unwrap(); + // That's not a very precise span :/ + assert_eq!(repr_span(the_loop.span), "4:12-10:9"); + Ok(()) +} + +#[test] +fn predicate_origins() -> Result<(), Box> { + use PredicateOrigin::*; + let crate_data = translate( + " + fn top_level_function() where T: Default {} + + #[derive(Clone)] + struct Struct where T: Default { x: T } + + type TypeAlias where T: Default = Struct; + + impl Struct where T: Default { + fn inherent_method>() where T: From {} + } + + trait Trait: Clone where T: Default { + type AssocType: Default; + fn trait_method>() where T: From; + } + + impl Trait for Struct where T: Default { + type AssocType = (); + fn trait_method>() where T: From {} + } + ", + )?; + let expected_function_clause_origins: Vec<(&str, &[_])> = vec![ + ( + "test_crate::top_level_function", + &[(WhereClauseOnFn, "Clone"), (WhereClauseOnFn, "Default")], + ), + ( + "test_crate::Struct", + &[(WhereClauseOnType, "Clone"), (WhereClauseOnType, "Default")], + ), + ( + "test_crate::TypeAlias", + &[(WhereClauseOnType, "Clone"), (WhereClauseOnType, "Default")], + ), + ( + "test_crate::::inherent_method", + &[ + (WhereClauseOnImpl, "Clone"), + (WhereClauseOnImpl, "Default"), + (WhereClauseOnFn, "From"), + (WhereClauseOnFn, "From"), + ], + ), + ( + "test_crate::Trait", + &[ + (WhereClauseOnTrait, "Clone"), + (WhereClauseOnTrait, "Copy"), + (WhereClauseOnTrait, "Default"), + ], + ), + // Interesting note: the method definition does not mention the clauses on the trait. + ( + "test_crate::Trait::trait_method", + &[(WhereClauseOnFn, "From"), (WhereClauseOnFn, "From")], + ), + ( + "test_crate::", + &[(WhereClauseOnImpl, "Copy"), (WhereClauseOnImpl, "Default")], + ), + ( + "test_crate::::trait_method", + &[ + (WhereClauseOnImpl, "Copy"), + (WhereClauseOnImpl, "Default"), + (WhereClauseOnFn, "From"), + (WhereClauseOnFn, "From"), + ], + ), + ]; + let items_by_name = items_by_name(&crate_data); + for (item_name, origins) in expected_function_clause_origins { + let Some(item) = items_by_name.get(item_name) else { + let keys = items_by_name + .keys() + .sorted() + .map(|k| format!("- `{k}`")) + .join("\n"); + panic!("Item `{item_name}` not found. Available items: \n{keys}") + }; + let clauses = &item.generics.trait_clauses; + assert_eq!(origins.len(), clauses.len(), "failed for {item_name}"); + for (clause, (expected_origin, expected_trait_name)) in clauses.iter().zip(origins) { + let trait_name = trait_name(&crate_data, clause.trait_id); + assert_eq!(trait_name, *expected_trait_name, "failed for {item_name}"); + assert_eq!(&clause.origin, expected_origin, "failed for {item_name}"); + } + } + + let my_trait = items_by_name + .get("test_crate::Trait") + .unwrap() + .kind + .as_trait_decl(); + let item_clauses = &(my_trait.types[0].1).0; + assert_eq!( + item_clauses[0].origin, + TraitItem(TraitItemName("AssocType".into())) + ); Ok(()) } @@ -147,14 +402,20 @@ fn visibility() -> Result<(), Box> { } "#, )?; - assert_eq!(repr_name(&crate_data.types[0].name), "test_crate::Pub"); + assert_eq!( + repr_name(&crate_data, &crate_data.types[0].name), + "test_crate::Pub" + ); assert!(crate_data.types[0].item_meta.public); - assert_eq!(repr_name(&crate_data.types[1].name), "test_crate::Priv"); + assert_eq!( + repr_name(&crate_data, &crate_data.types[1].name), + "test_crate::Priv" + ); assert!(!crate_data.types[1].item_meta.public); // Note how we think `PubInPriv` is public. It kind of is but there is no path to it. This is // probably fine. assert_eq!( - repr_name(&crate_data.types[2].name), + repr_name(&crate_data, &crate_data.types[2].name), "test_crate::private::PubInPriv" ); assert!(crate_data.types[2].item_meta.public); @@ -189,3 +450,129 @@ fn discriminants() -> Result<(), Box> { ); Ok(()) } + +#[test] +fn rename_attribute() -> Result<(), Box> { + let crate_data = translate( + r#" + #![feature(register_tool)] + #![register_tool(charon)] + #![register_tool(aeneas)] + + #[charon::rename("BoolTest")] + pub trait BoolTrait { + // Required method + #[charon::rename("getTest")] + fn get_bool(&self) -> bool; + + // Provided method + #[charon::rename("retTest")] + fn ret_true(&self) -> bool { + true + } + } + + #[charon::rename("BoolImpl")] + impl BoolTrait for bool { + fn get_bool(&self) -> bool { + *self + } + } + + #[charon::rename("BoolFn")] + fn test_bool_trait(x: bool) -> bool { + x.get_bool() && x.ret_true() + } + + #[charon::rename("TypeTest")] + type Test = i32; + + #[charon::rename("VariantsTest")] + enum SimpleEnum { + #[charon::rename("Variant1")] + FirstVariant, + SecondVariant, + ThirdVariant, + } + + #[charon::rename("StructTest")] + struct Foo { + #[charon::rename("FieldTest")] + field1: u32, + } + + #[charon::rename("Const_Test")] + const C: u32 = 100 + 10 + 1; + + #[aeneas::rename("_TypeAeneas36")] + type Test2 = u32; + "#, + )?; + + assert_eq!( + crate_data.trait_decls[0].item_meta.rename.as_deref(), + Some("BoolTest") + ); + + assert_eq!( + crate_data.functions[2].item_meta.rename.as_deref(), + Some("getTest") + ); + + assert_eq!( + crate_data.functions[3].item_meta.rename.as_deref(), + Some("retTest") + ); + + assert_eq!( + crate_data.trait_impls[0].item_meta.rename.as_deref(), + Some("BoolImpl") + ); + + assert_eq!( + crate_data.functions[1].item_meta.rename.as_deref(), + Some("BoolFn") + ); + + assert_eq!( + crate_data.types[0].item_meta.rename.as_deref(), + Some("TypeTest") + ); + + assert_eq!( + crate_data.types[1].item_meta.rename.as_deref(), + Some("VariantsTest") + ); + + assert_eq!( + crate_data.types[1].kind.as_enum()[0] + .item_meta + .rename + .as_deref(), + Some("Variant1") + ); + + assert_eq!( + crate_data.types[2].item_meta.rename.as_deref(), + Some("StructTest") + ); + + assert_eq!( + crate_data.globals[0].item_meta.rename.as_deref(), + Some("Const_Test") + ); + + assert_eq!( + crate_data.types[3].item_meta.rename.as_deref(), + Some("_TypeAeneas36") + ); + + assert_eq!( + crate_data.types[2].kind.as_struct()[0] + .item_meta + .rename + .as_deref(), + Some("FieldTest") + ); + Ok(()) +} diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out index c9a5b73f0..94d422aa1 100644 --- a/charon/tests/ui/arrays.out +++ b/charon/tests/ui/arrays.out @@ -1235,13 +1235,13 @@ fn test_crate::sum2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 (Slice)) -> u drop @15 drop @14 @19 := copy (i@10) - @28 := &*(s@1) - @29 := @SliceIndexShared<'_, u32>(move (@28), copy (@19)) - @18 := copy (*(@29)) + @26 := &*(s@1) + @27 := @SliceIndexShared<'_, u32>(move (@26), copy (@19)) + @18 := copy (*(@27)) @21 := copy (i@10) - @26 := &*(s2@2) - @27 := @SliceIndexShared<'_, u32>(move (@26), copy (@21)) - @20 := copy (*(@27)) + @28 := &*(s2@2) + @29 := @SliceIndexShared<'_, u32>(move (@28), copy (@21)) + @20 := copy (*(@29)) @17 := move (@18) + move (@20) drop @20 drop @18 @@ -1700,15 +1700,15 @@ fn test_crate::slice_pattern_2<'_0, T>(@1: Array<&'_0 mut (T), 3 : usize>) let @11: &'_ mut (&'_ mut (T)); // anonymous local @fake_read(x@1) - @10 := &mut x@1 - @11 := @ArrayIndexMut<'_, &'_ mut (T), 3 : usize>(move (@10), const (0 : usize)) - _a@2 := move (*(@11)) + @6 := &mut x@1 + @7 := @ArrayIndexMut<'_, &'_ mut (T), 3 : usize>(move (@6), const (0 : usize)) + _a@2 := move (*(@7)) @8 := &mut x@1 @9 := @ArrayIndexMut<'_, &'_ mut (T), 3 : usize>(move (@8), const (1 : usize)) _b@3 := move (*(@9)) - @6 := &mut x@1 - @7 := @ArrayIndexMut<'_, &'_ mut (T), 3 : usize>(move (@6), const (2 : usize)) - _c@4 := move (*(@7)) + @10 := &mut x@1 + @11 := @ArrayIndexMut<'_, &'_ mut (T), 3 : usize>(move (@10), const (2 : usize)) + _c@4 := move (*(@11)) @5 := () @0 := move (@5) drop _c@4 diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 429aa1249..6801961fe 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -144,6 +144,8 @@ trait core::iter::traits::iterator::Iterator } trait core::iter::traits::collect::IntoIterator +where + (Self::IntoIter::[@TraitClause0])::Item = Self::Item, { type Item type IntoIter diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out index f8feb03e3..a15833fdc 100644 --- a/charon/tests/ui/loops.out +++ b/charon/tests/ui/loops.out @@ -873,6 +873,8 @@ trait core::iter::traits::iterator::Iterator } trait core::iter::traits::collect::IntoIterator +where + (Self::IntoIter::[@TraitClause0])::Item = Self::Item, { type Item type IntoIter @@ -1782,7 +1784,6 @@ fn test_crate::get_elem_mut<'_0>(@1: &'_0 mut (test_crate::List), @2: usi drop @6 drop tl@5 drop y@4 - nop return } panic(core::panicking::panic_explicit) diff --git a/charon/tests/ui/matches.out b/charon/tests/ui/matches.out index 374514a48..a3df35dac 100644 --- a/charon/tests/ui/matches.out +++ b/charon/tests/ui/matches.out @@ -71,38 +71,42 @@ fn test_crate::test3(@1: test_crate::E2) -> u32 { let @0: u32; // return let x@1: test_crate::E2; // arg #1 - let y@2: u32; // local - let n@3: u32; // local - let z@4: u32; // local - let @5: u32; // anonymous local + let @2: (); // anonymous local + let y@3: u32; // local + let n@4: u32; // local + let z@5: u32; // local let @6: u32; // anonymous local + let @7: u32; // anonymous local + @2 := () + @fake_read(@2) + drop @2 @fake_read(x@1) match x@1 { 0 => { - n@3 := copy ((x@1 as variant @0).0) - y@2 := copy (n@3) - drop n@3 + n@4 := copy ((x@1 as variant @0).0) + y@3 := copy (n@4) + drop n@4 }, 1 => { - n@3 := copy ((x@1 as variant @1).0) - y@2 := copy (n@3) - drop n@3 + n@4 := copy ((x@1 as variant @1).0) + y@3 := copy (n@4) + drop n@4 }, 2 => { - y@2 := const (0 : u32) + y@3 := const (0 : u32) } } - @fake_read(y@2) - z@4 := test_crate::id(const (3 : u32)) - @fake_read(z@4) - @5 := copy (y@2) - @6 := copy (z@4) - @0 := move (@5) + move (@6) + @fake_read(y@3) + z@5 := test_crate::id(const (3 : u32)) + @fake_read(z@5) + @6 := copy (y@3) + @7 := copy (z@5) + @0 := move (@6) + move (@7) + drop @7 drop @6 - drop @5 - drop z@4 - drop y@2 + drop z@5 + drop y@3 return } diff --git a/charon/tests/ui/matches.rs b/charon/tests/ui/matches.rs index a021cedd3..15dcd85eb 100644 --- a/charon/tests/ui/matches.rs +++ b/charon/tests/ui/matches.rs @@ -31,7 +31,7 @@ pub enum E1 { /// especially because it makes the control-flow reconstruction more ad-hoc. The /// main problem is that it would be difficult to make the distinction between /// a goto we need to ignore, and a "real" goto. -/// Consequently, whenever branhces are fused, don't use `--no-code-duplication`. +/// Consequently, whenever branches are fused, don't use `--no-code-duplication`. pub fn test1(x: E1) -> bool { match x { E1::V1 | E1::V2 => true, @@ -61,6 +61,7 @@ pub fn test2(x: E2) -> u32 { /// Similar to test2 pub fn test3(x: E2) -> u32 { + let () = (); // Test that we don't assume the match is the first statement. let y = match x { E2::V1(n) | E2::V2(n) => n, E2::V3 => 0, diff --git a/charon/tests/ui/rename_attribute.out b/charon/tests/ui/rename_attribute.out new file mode 100644 index 000000000..19abd0778 --- /dev/null +++ b/charon/tests/ui/rename_attribute.out @@ -0,0 +1,84 @@ +# Final LLBC before serialization: + +trait test_crate::BoolTrait +{ + fn get_bool : test_crate::BoolTrait::get_bool + fn ret_true : test_crate::BoolTrait::ret_true +} + +fn test_crate::{impl test_crate::BoolTrait for bool}::get_bool<'_0>(@1: &'_0 (bool)) -> bool +{ + let @0: bool; // return + let self@1: &'_ (bool); // arg #1 + + @0 := copy (*(self@1)) + return +} + +impl test_crate::{impl test_crate::BoolTrait for bool} : test_crate::BoolTrait +{ + fn get_bool = test_crate::{impl test_crate::BoolTrait for bool}::get_bool +} + +fn test_crate::BoolTrait::get_bool<'_0, Self>(@1: &'_0 (Self)) -> bool + +fn test_crate::BoolTrait::ret_true<'_0, Self>(@1: &'_0 (Self)) -> bool +{ + let @0: bool; // return + let self@1: &'_ (Self); // arg #1 + + @0 := const (true) + return +} + +fn test_crate::test_bool_trait(@1: bool) -> bool +{ + let @0: bool; // return + let x@1: bool; // arg #1 + let @2: bool; // anonymous local + let @3: &'_ (bool); // anonymous local + let @4: &'_ (bool); // anonymous local + + @3 := &x@1 + @2 := test_crate::{impl test_crate::BoolTrait for bool}::get_bool(move (@3)) + if move (@2) { + drop @3 + @4 := &x@1 + @0 := test_crate::{impl test_crate::BoolTrait for bool}::ret_true(move (@4)) + drop @4 + } + else { + drop @3 + @0 := const (false) + } + drop @2 + return +} + +type test_crate::Test = i32 + +enum test_crate::SimpleEnum = +| FirstVariant() +| SecondVariant() +| ThirdVariant() + + +struct test_crate::Foo = +{ + field1: u32 +} + +global test_crate::C { + let @0: u32; // return + let @1: u32; // anonymous local + + @1 := const (100 : u32) + const (10 : u32) + @0 := copy (@1) + const (1 : u32) + drop @1 + return +} + +type test_crate::Test2 = u32 + + + diff --git a/charon/tests/ui/rename_attribute.rs b/charon/tests/ui/rename_attribute.rs new file mode 100644 index 000000000..06e32ecf0 --- /dev/null +++ b/charon/tests/ui/rename_attribute.rs @@ -0,0 +1,51 @@ +#![feature(register_tool)] +#![register_tool(charon)] +#![register_tool(aeneas)] + +#[charon::rename("BoolTest")] +pub trait BoolTrait { + // Required method + #[charon::rename("getTest")] + fn get_bool(&self) -> bool; + + // Provided method + #[charon::rename("retTest")] + fn ret_true(&self) -> bool { + true + } +} + +#[charon::rename("BoolImpl")] +impl BoolTrait for bool { + fn get_bool(&self) -> bool { + *self + } +} + +#[charon::rename("BoolFn")] +pub fn test_bool_trait(x: bool) -> bool { + x.get_bool() && x.ret_true() +} + +#[charon::rename("TypeTest")] +type Test = i32; + +#[charon::rename("VariantsTest")] +enum SimpleEnum { + #[charon::rename("Variant1")] + FirstVariant, + SecondVariant, + ThirdVariant, +} + +#[charon::rename("StructTest")] +struct Foo { + #[charon::rename("FieldTest")] + field1: u32, +} + +#[charon::rename("Const_Test")] +const C: u32 = 100 + 10 + 1; + +#[aeneas::rename("_TypeAeneas36")] +type Test2 = u32; diff --git a/charon/tests/ui/rename_attribute_failure.out b/charon/tests/ui/rename_attribute_failure.out new file mode 100644 index 000000000..d1fe0c281 --- /dev/null +++ b/charon/tests/ui/rename_attribute_failure.out @@ -0,0 +1,28 @@ +error: Attribute `{charon,aeneas}::rename` should not contain an empty string + --> tests/ui/rename_attribute_failure.rs:8:1 + | +8 | type TestEmpty = i32; + | ^^^^^^^^^^^^^^ + +error: Attribute `rename` should only contain alphanumeric characters and `_`, and should start with a letter or '_': "Test!976?" is not a valid name + --> tests/ui/rename_attribute_failure.rs:12:1 + | +12 | type TestNonAlphanumeric = i32; + | ^^^^^^^^^^^^^^^^^^^^^^^^ + +error: Attribute `rename` should only contain alphanumeric characters and `_`, and should start with a letter or '_': "75Test" is not a valid name + --> tests/ui/rename_attribute_failure.rs:16:1 + | +16 | type TestNotStartingWithLetter = i32; + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error: Attribute `{charon,aeneas}::rename` should be of the shape `{charon,aeneas}::rename("...")`: `charon::rename()` is not valid + --> tests/ui/rename_attribute_failure.rs:20:1 + | +20 | type TestNotProperShape = i32; + | ^^^^^^^^^^^^^^^^^^^^^^^ + +error: aborting due to 4 previous errors + +[ ERROR charon_driver:231] The extraction encountered 4 errors +Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/rename_attribute_failure.rs b/charon/tests/ui/rename_attribute_failure.rs new file mode 100644 index 000000000..404e04fdc --- /dev/null +++ b/charon/tests/ui/rename_attribute_failure.rs @@ -0,0 +1,20 @@ +//@ known-failure +#![feature(register_tool)] +#![register_tool(charon)] +#![register_tool(aeneas)] + +// Errors because rename attribute should not be empty +#[charon::rename("")] +type TestEmpty = i32; + +// Errors because rename attribute should only contain alphanumeric or '_' characters +#[charon::rename("Test!976?")] +type TestNonAlphanumeric = i32; + +// Errors because rename attribute should begin with a letter +#[charon::rename("75Test")] +type TestNotStartingWithLetter = i32; + +// Errors because rename attribute is not of the proper shape (lacks "") +#[charon::rename()] +type TestNotProperShape = i32; diff --git a/charon/tests/ui/trait-instance-id.out b/charon/tests/ui/trait-instance-id.out index e33c473e3..54920e908 100644 --- a/charon/tests/ui/trait-instance-id.out +++ b/charon/tests/ui/trait-instance-id.out @@ -115,6 +115,8 @@ trait core::iter::traits::iterator::Iterator } trait core::iter::traits::collect::IntoIterator +where + (Self::IntoIter::[@TraitClause0])::Item = Self::Item, { type Item type IntoIter @@ -142,7 +144,7 @@ trait core::ops::function::FnMut fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}::fold(@1: core::array::iter::IntoIter, @2: Acc, @3: Fold) -> Acc where [@TraitClause0]: core::ops::function::FnMut, - (parents(Unsolved(core::ops::function::FnMut#2}::Item)>))::[@TraitClause0])::Output = Acc, + (parents(UNKNOWN(Could not find a clause for parameter: @TraitDecl3#2}::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt0>; [@TraitClause0]: @TraitDecl3) (context: core::array::iter::{impl#2}::fold)))::[@TraitClause0])::Output = Acc, fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}::count(@1: core::array::iter::IntoIter) -> usize @@ -215,34 +217,34 @@ fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::sli fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::fold<'a, T, B, F>(@1: core::slice::iter::Iter<'a, T>, @2: B, @3: F) -> B where [@TraitClause0]: core::ops::function::FnMut, - (parents(Unsolved(core::ops::function::FnMut#181}<'_, T>::Item)>))::[@TraitClause0])::Output = B, + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#181}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#181}::fold)))::[@TraitClause0])::Output = B, fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::for_each<'a, T, F>(@1: core::slice::iter::Iter<'a, T>, @2: F) where [@TraitClause0]: core::ops::function::FnMut, - (parents(Unsolved(core::ops::function::FnMut#181}<'_, T>::Item)>))::[@TraitClause0])::Output = (), + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#181}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#181}::for_each)))::[@TraitClause0])::Output = (), fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::all<'a, '_1, T, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: F) -> bool where [@TraitClause0]: core::ops::function::FnMut, - (parents(Unsolved(core::ops::function::FnMut#181}<'_, T>::Item)>))::[@TraitClause0])::Output = bool, + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#181}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#181}::all)))::[@TraitClause0])::Output = bool, fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::any<'a, '_1, T, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: F) -> bool where [@TraitClause0]: core::ops::function::FnMut, - (parents(Unsolved(core::ops::function::FnMut#181}<'_, T>::Item)>))::[@TraitClause0])::Output = bool, + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#181}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#181}::any)))::[@TraitClause0])::Output = bool, Unknown decl: 39 fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::find_map<'a, '_1, T, B, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: F) -> core::option::Option where [@TraitClause0]: core::ops::function::FnMut, - (parents(Unsolved(core::ops::function::FnMut#181}<'_, T>::Item)>))::[@TraitClause0])::Output = core::option::Option, + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#181}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#181}::find_map)))::[@TraitClause0])::Output = core::option::Option, fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::position<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: P) -> core::option::Option where [@TraitClause0]: core::ops::function::FnMut, - (parents(Unsolved(core::ops::function::FnMut#181}<'_, T>::Item)>))::[@TraitClause0])::Output = bool, + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#181}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#181}::position)))::[@TraitClause0])::Output = bool, trait core::iter::traits::exact_size::ExactSizeIterator { @@ -264,10 +266,10 @@ trait core::iter::traits::double_ended::DoubleEndedIterator fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::rposition<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: P) -> core::option::Option where - [@TraitClause0]: core::ops::function::FnMut>))::[@TraitClause0])::Item)>, + [@TraitClause0]: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>) (context: core::slice::iter::{impl#181}::rposition)))::[@TraitClause0])::Item)>, [@TraitClause1]: core::iter::traits::exact_size::ExactSizeIterator>, [@TraitClause2]: core::iter::traits::double_ended::DoubleEndedIterator>, - (parents(Unsolved(core::ops::function::FnMut>))::[@TraitClause0])::Item)>))::[@TraitClause0])::Output = bool, + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>) (context: core::slice::iter::{impl#181}::rposition)))::[@TraitClause0])::Item)>; [@TraitClause1]: @TraitDecl5<@Adt2<'_, T>>; [@TraitClause2]: @TraitDecl6<@Adt2<'_, T>>) (context: core::slice::iter::{impl#181}::rposition)))::[@TraitClause0])::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>) (context: core::slice::iter::{impl#181}::rposition)))::[@TraitClause0])::Item)>; [@TraitClause1]: @TraitDecl5<@Adt2<'_, T>>; [@TraitClause2]: @TraitDecl6<@Adt2<'_, T>>) (context: core::slice::iter::{impl#181}::rposition)))::[@TraitClause0])::Output = bool, unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}<'_, T>::Item diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index b47e873d4..4d30b7b16 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -643,6 +643,8 @@ trait test_crate::Iterator } trait test_crate::IntoIterator +where + (Self::IntoIter::[@TraitClause0])::Item = Self::Item, { type Item type IntoIter diff --git a/charon/tests/ui/type_alias.out b/charon/tests/ui/type_alias.out index 51a78c984..e35caf4f7 100644 --- a/charon/tests/ui/type_alias.out +++ b/charon/tests/ui/type_alias.out @@ -36,8 +36,6 @@ enum alloc::borrow::Cow<'a, B> opaque type alloc::vec::Vec -struct alloc::alloc::Global = {} - fn alloc::slice::{impl core::borrow::Borrow> for alloc::vec::Vec#5}::borrow<'_0, T, A>(@1: &'_0 (alloc::vec::Vec)) -> &'_0 (Slice) impl alloc::slice::{impl core::borrow::Borrow> for alloc::vec::Vec#5} : core::borrow::Borrow, Slice> @@ -45,6 +43,8 @@ impl alloc::slice::{impl core::borrow::Borrow> for alloc::vec::Ve fn borrow = alloc::slice::{impl core::borrow::Borrow> for alloc::vec::Vec#5}::borrow } +struct alloc::alloc::Global = {} + fn alloc::slice::{impl alloc::borrow::ToOwned for Slice#9}::to_owned<'_0, T>(@1: &'_0 (Slice)) -> alloc::vec::Vec where // Inherited clauses: