diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index 5e74d255..2a64cb88 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.45" +let supported_charon_version = "0.1.47" diff --git a/charon-ml/src/GAst.ml b/charon-ml/src/GAst.ml index 262269af..1604712f 100644 --- a/charon-ml/src/GAst.ml +++ b/charon-ml/src/GAst.ml @@ -26,10 +26,8 @@ type fun_id = Expressions.fun_id [@@deriving show, ord] type fun_id_or_trait_method_ref = Expressions.fun_id_or_trait_method_ref [@@deriving show, ord] -type fun_decl_id = FunDeclId.id - (** A variable *) -and var = { +type var = { index : var_id; (** Unique index identifying the variable *) name : string option; (** Variable name - may be `None` if the variable was introduced by Rust @@ -38,6 +36,8 @@ and var = { var_ty : ty; (** The variable type *) } +and fun_decl_id = FunDeclId.id + (** The id of a translated item. *) and any_decl_id = | IdType of type_decl_id @@ -159,6 +159,18 @@ and item_kind = item is a copy of the default item. *) +(** A global variable definition (constant or static). *) +and global_decl = { + def_id : global_decl_id; + item_meta : item_meta; (** The meta data associated with the declaration. *) + generics : generic_params; + ty : ty; + kind : item_kind; + (** The global kind: "regular" function, trait const declaration, etc. *) + body : fun_decl_id; + (** The initializer function used to compute the initial value for this constant/static. *) +} + (** A trait **declaration**. For instance: @@ -346,6 +358,10 @@ and fun_sig = { (the function in which the closure is defined) - the region variables are local to the closure *) + is_global_initializer : bool; + (** Whether this function is in fact the body of a constant/static that we turned into an + initializer function. + *) closure_info : closure_info option; (** Additional information if this is the signature of a closure. *) generics : generic_params; @@ -398,30 +414,18 @@ type 'body gfun_decl = { signature : fun_sig; kind : item_kind; body : 'body gexpr_body option; - is_global_decl_body : bool; -} -[@@deriving show] - -(* Hand-written because the rust equivalent isn't generic *) -type 'body gglobal_decl = { - def_id : GlobalDeclId.id; - item_meta : item_meta; - generics : generic_params; - ty : ty; - kind : item_kind; - body : 'body; } [@@deriving show] (* Hand-written because the rust equivalent isn't generic *) (** A crate *) -type ('fun_body, 'global_body) gcrate = { +type 'fun_body gcrate = { name : string; declarations : declaration_group list; type_decls : type_decl TypeDeclId.Map.t; fun_decls : 'fun_body gfun_decl FunDeclId.Map.t; - global_decls : 'global_body gglobal_decl GlobalDeclId.Map.t; + global_decls : global_decl GlobalDeclId.Map.t; trait_decls : trait_decl TraitDeclId.Map.t; trait_impls : trait_impl TraitImplId.Map.t; source_files : string FileNameMap.t; diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index 2f3a7857..86af5db6 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/charon-ml/src/GAstOfJson.ml @@ -324,10 +324,6 @@ and aggregate_kind_of_json (js : json) : (aggregate_kind, string) result = Ok (AggregatedClosure (x_0, x_1)) | _ -> Error "") -and fun_decl_id_of_json (js : json) : (fun_decl_id, string) result = - combine_error_msgs js __FUNCTION__ - (match js with x -> FunDeclId.id_of_json x | _ -> Error "") - and var_of_json (js : json) : (var, string) result = combine_error_msgs js __FUNCTION__ (match js with @@ -398,6 +394,28 @@ and item_kind_of_json (js : json) : (item_kind, string) result = Ok (TraitImplItem (impl_id, trait_id, item_name, reuses_default)) | _ -> Error "") +and global_decl_of_json (id_to_file : id_to_file_map) (js : json) : + (global_decl, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | `Assoc + [ + ("def_id", def_id); + ("item_meta", item_meta); + ("generics", generics); + ("ty", ty); + ("kind", kind); + ("init", init); + ] -> + let* def_id = global_decl_id_of_json def_id 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* ty = ty_of_json ty in + let* kind = item_kind_of_json kind in + let* body = fun_decl_id_of_json init in + Ok ({ def_id; item_meta; generics; ty; kind; body } : global_decl) + | _ -> Error "") + and global_decl_ref_of_json (js : json) : (global_decl_ref, string) result = combine_error_msgs js __FUNCTION__ (match js with @@ -563,6 +581,26 @@ and assertion_of_json (js : json) : (assertion, string) result = Ok ({ cond; expected } : assertion) | _ -> Error "") +and fun_decl_id_of_json (js : json) : (fun_decl_id, string) result = + combine_error_msgs js __FUNCTION__ + (match js with x -> FunDeclId.id_of_json x | _ -> Error "") + +and type_decl_id_of_json (js : json) : (type_decl_id, string) result = + combine_error_msgs js __FUNCTION__ + (match js with x -> TypeDeclId.id_of_json x | _ -> Error "") + +and global_decl_id_of_json (js : json) : (global_decl_id, string) result = + combine_error_msgs js __FUNCTION__ + (match js with x -> GlobalDeclId.id_of_json x | _ -> Error "") + +and trait_decl_id_of_json (js : json) : (trait_decl_id, string) result = + combine_error_msgs js __FUNCTION__ + (match js with x -> TraitDeclId.id_of_json x | _ -> Error "") + +and trait_impl_id_of_json (js : json) : (trait_impl_id, string) result = + combine_error_msgs js __FUNCTION__ + (match js with x -> TraitImplId.id_of_json x | _ -> Error "") + and any_decl_id_of_json (js : json) : (any_decl_id, string) result = combine_error_msgs js __FUNCTION__ (match js with @@ -749,10 +787,6 @@ and type_var_id_of_json (js : json) : (type_var_id, string) result = combine_error_msgs js __FUNCTION__ (match js with x -> TypeVarId.id_of_json x | _ -> Error "") -and type_decl_id_of_json (js : json) : (type_decl_id, string) result = - combine_error_msgs js __FUNCTION__ - (match js with x -> TypeDeclId.id_of_json x | _ -> Error "") - and variant_id_of_json (js : json) : (variant_id, string) result = combine_error_msgs js __FUNCTION__ (match js with x -> VariantId.id_of_json x | _ -> Error "") @@ -766,10 +800,6 @@ and const_generic_var_id_of_json (js : json) : combine_error_msgs js __FUNCTION__ (match js with x -> ConstGenericVarId.id_of_json x | _ -> Error "") -and global_decl_id_of_json (js : json) : (global_decl_id, string) result = - combine_error_msgs js __FUNCTION__ - (match js with x -> GlobalDeclId.id_of_json x | _ -> Error "") - and type_var_of_json (js : json) : (type_var, string) result = combine_error_msgs js __FUNCTION__ (match js with @@ -993,14 +1023,6 @@ and trait_clause_id_of_json (js : json) : (trait_clause_id, string) result = combine_error_msgs js __FUNCTION__ (match js with x -> TraitClauseId.id_of_json x | _ -> Error "") -and trait_decl_id_of_json (js : json) : (trait_decl_id, string) result = - combine_error_msgs js __FUNCTION__ - (match js with x -> TraitDeclId.id_of_json x | _ -> Error "") - -and trait_impl_id_of_json (js : json) : (trait_impl_id, string) result = - combine_error_msgs js __FUNCTION__ - (match js with x -> TraitImplId.id_of_json x | _ -> Error "") - and trait_clause_of_json (id_to_file : id_to_file_map) (js : json) : (trait_clause, string) result = combine_error_msgs js __FUNCTION__ @@ -1278,6 +1300,7 @@ and fun_sig_of_json (id_to_file : id_to_file_map) (js : json) : [ ("is_unsafe", is_unsafe); ("is_closure", is_closure); + ("is_global_initializer", is_global_initializer); ("closure_info", closure_info); ("generics", generics); ("parent_params_info", parent_params_info); @@ -1286,6 +1309,7 @@ and fun_sig_of_json (id_to_file : id_to_file_map) (js : json) : ] -> let* is_unsafe = bool_of_json is_unsafe in let* is_closure = bool_of_json is_closure in + let* is_global_initializer = bool_of_json is_global_initializer in 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* parent_params_info = @@ -1297,6 +1321,7 @@ and fun_sig_of_json (id_to_file : id_to_file_map) (js : json) : ({ is_unsafe; is_closure; + is_global_initializer; closure_info; generics; parent_params_info; @@ -1450,42 +1475,7 @@ and gfun_decl_of_json (bodies : 'body gexpr_body option list) let* signature = fun_sig_of_json id_to_file signature in let* kind = item_kind_of_json kind in let* body = maybe_opaque_body_of_json bodies body in - Ok - { - def_id; - item_meta; - signature; - kind; - body; - is_global_decl_body = false; - } - | _ -> Error "") - -(* This is written by hand because the corresponding rust type is not type-generic. *) -and gglobal_decl_of_json (bodies : 'body gexpr_body option list) - (id_to_file : id_to_file_map) (js : json) : - ('body gexpr_body option gglobal_decl, string) result = - combine_error_msgs js __FUNCTION__ - (match js with - | `Assoc - [ - ("def_id", def_id); - ("item_meta", item_meta); - ("generics", generics); - ("ty", ty); - ("kind", kind); - ("body", body); - ] -> - let* global_id = GlobalDeclId.id_of_json def_id 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* ty = ty_of_json ty in - let* kind = item_kind_of_json kind in - let* body = maybe_opaque_body_of_json bodies body in - let global = - { def_id = global_id; item_meta; body; generics; ty; kind } - in - Ok global + Ok { def_id; item_meta; signature; kind; body } | _ -> Error "") (** Deserialize a map from file id to file name. @@ -1512,17 +1502,17 @@ and id_to_file_of_json (js : json) : (id_to_file_map, string) result = (* This is written by hand because the corresponding rust type is not type-generic. *) and gtranslated_crate_of_json (body_of_json : id_to_file_map -> json -> ('body gexpr_body, string) result) - (js : json) : (('body, 'body gexpr_body option) gcrate, string) result = + (js : json) : ('body gcrate, string) result = combine_error_msgs js __FUNCTION__ (match js with | `Assoc [ ("crate_name", name); ("real_crate_name", _); - ("id_to_file", id_to_file); ("file_id_to_content", file_id_to_content); ("all_ids", _); ("item_names", _); + ("id_to_file", id_to_file); ("type_decls", types); ("fun_decls", functions); ("global_decls", globals); @@ -1551,7 +1541,7 @@ and gtranslated_crate_of_json in let* globals = vector_of_json global_decl_id_of_json - (gglobal_decl_of_json bodies id_to_file) + (global_decl_of_json id_to_file) globals in let* trait_decls = @@ -1580,9 +1570,7 @@ and gtranslated_crate_of_json in let global_decls = GlobalDeclId.Map.of_list - (List.map - (fun (d : 'body gexpr_body option gglobal_decl) -> (d.def_id, d)) - globals) + (List.map (fun (d : global_decl) -> (d.def_id, d)) globals) in let trait_decls = TraitDeclId.Map.of_list @@ -1617,7 +1605,7 @@ and gtranslated_crate_of_json and gcrate_of_json (body_of_json : id_to_file_map -> json -> ('body gexpr_body, string) result) - (js : json) : (('body, 'body gexpr_body option) gcrate, string) result = + (js : json) : ('body gcrate, string) result = match js with | `Assoc [ ("charon_version", charon_version); ("translated", translated) ] -> (* Ensure the version is the one we support. *) diff --git a/charon-ml/src/GAstUtils.ml b/charon-ml/src/GAstUtils.ml index 2da8caee..8761d722 100644 --- a/charon-ml/src/GAstUtils.ml +++ b/charon-ml/src/GAstUtils.ml @@ -101,10 +101,10 @@ let split_declarations_to_group_maps (decls : declaration_group list) : let module G (M : Map.S) = struct let add_group (map : M.key g_declaration_group M.t) (group : M.key g_declaration_group) : M.key g_declaration_group M.t = - match group with - | NonRecGroup id -> M.add id group map - | RecGroup ids -> - List.fold_left (fun map id -> M.add id group map) map ids + List.fold_left + (fun map id -> M.add id group map) + map + (g_declaration_group_to_list group) let create_map (groups : M.key g_declaration_group list) : M.key g_declaration_group M.t = diff --git a/charon-ml/src/LlbcAst.ml b/charon-ml/src/LlbcAst.ml index 6c061306..cf78c996 100644 --- a/charon-ml/src/LlbcAst.ml +++ b/charon-ml/src/LlbcAst.ml @@ -93,8 +93,5 @@ type expr_body = statement gexpr_body [@@deriving show] type fun_body = expr_body [@@deriving show] type fun_decl = statement gfun_decl [@@deriving show] -(* TODO: the function id should be an option *) -type global_decl = FunDeclId.id gglobal_decl [@@deriving show] - (** LLBC crate *) -type crate = (statement, FunDeclId.id) gcrate +type crate = statement gcrate diff --git a/charon-ml/src/LlbcOfJson.ml b/charon-ml/src/LlbcOfJson.ml index 23c5fbe0..236ebd5d 100644 --- a/charon-ml/src/LlbcOfJson.ml +++ b/charon-ml/src/LlbcOfJson.ml @@ -141,97 +141,5 @@ let expr_body_of_json (id_to_file : id_to_file_map) (js : json) : Ok body | _ -> Error "") -(** Strict type for the number of function declarations (see {!global_to_fun_id} below) *) -type global_id_converter = { max_fun_id : int } [@@deriving show] - -(** Converts a global id to its corresponding function id. - To do so, it adds the global id to the number of function declarations : - We have the bijection [global_fun_id <=> global_id + fun_id_count]. -*) -let global_to_fun_id (conv : global_id_converter) (gid : GlobalDeclId.id) : - FunDeclId.id = - FunDeclId.of_int (GlobalDeclId.to_int gid + conv.max_fun_id) - -(** Deserialize a global declaration, and decompose it into a global declaration - and a function declaration. - *) -let split_global (gid_conv : global_id_converter) global : - global_decl * fun_decl = - (* Deserialize the global declaration *) - let { def_id = global_id; item_meta; body; generics; ty; kind } = global in - (* Decompose into a global and a function *) - let fun_id = global_to_fun_id gid_conv global.def_id in - let signature : fun_sig = - { - (* Not sure about `is_unsafe` actually *) - is_unsafe = false; - is_closure = false; - closure_info = None; - generics; - parent_params_info = None; - inputs = []; - output = ty; - } - in - let global_decl : global_decl = - { def_id = global_id; item_meta; body = fun_id; generics; ty; kind } - in - let fun_decl : fun_decl = - { - def_id = fun_id; - item_meta; - signature; - kind = RegularItem; - body; - is_global_decl_body = true; - } - in - (global_decl, fun_decl) - let crate_of_json (js : json) : (crate, string) result = - begin - let* crate = gcrate_of_json expr_body_of_json js in - (* When deserializing the globals, we split the global declarations - * between the globals themselves and their bodies, which are simply - * functions with no arguments. We add the global bodies to the list - * of function declarations; we give fresh ids to these new bodies - * by incrementing from the last function id recorded *) - let gid_conv = - { - max_fun_id = - List.fold_left - (fun acc (id, _) -> max acc (1 + FunDeclId.to_int id)) - 0 - (FunDeclId.Map.bindings crate.fun_decls); - } - in - let globals, global_bodies = - List.split - (List.map - (fun (_, g) -> split_global gid_conv g) - (GlobalDeclId.Map.bindings crate.global_decls)) - in - - (* Add the global bodies to the list of functions *) - let fun_decls = - List.fold_left - (fun m (d : fun_decl) -> FunDeclId.Map.add d.def_id d m) - crate.fun_decls global_bodies - in - let global_decls = - GlobalDeclId.Map.of_list - (List.map (fun (d : global_decl) -> (d.def_id, d)) globals) - in - - Ok - { - name = crate.name; - declarations = crate.declarations; - type_decls = crate.type_decls; - fun_decls; - global_decls; - trait_decls = crate.trait_decls; - trait_impls = crate.trait_impls; - source_files = crate.source_files; - } - end + gcrate_of_json expr_body_of_json js diff --git a/charon-ml/src/PrintExpressions.ml b/charon-ml/src/PrintExpressions.ml index 81389f6d..da16c3cf 100644 --- a/charon-ml/src/PrintExpressions.ml +++ b/charon-ml/src/PrintExpressions.ml @@ -14,7 +14,7 @@ let var_to_string (v : var) : string = | None -> var_id_to_pretty_string v.index | Some name -> name ^ "^" ^ VarId.to_string v.index -let var_id_to_string (env : ('a, 'b) fmt_env) (id : VarId.id) : string = +let var_id_to_string (env : 'a fmt_env) (id : VarId.id) : string = match List.find_opt (fun (i, _) -> i = id) env.locals with | None -> var_id_to_pretty_string id | Some (_, name) -> ( @@ -22,8 +22,8 @@ let var_id_to_string (env : ('a, 'b) fmt_env) (id : VarId.id) : string = | None -> var_id_to_pretty_string id | Some name -> name ^ "^" ^ VarId.to_string id) -let rec projection_to_string (env : ('a, 'b) fmt_env) (s : string) - (p : projection) : string = +let rec projection_to_string (env : 'a fmt_env) (s : string) (p : projection) : + string = match p with | [] -> s | pe :: p' -> @@ -47,11 +47,11 @@ let rec projection_to_string (env : ('a, 'b) fmt_env) (s : string) in projection_to_string env s p' -let place_to_string (env : ('a, 'b) fmt_env) (p : place) : string = +let place_to_string (env : 'a fmt_env) (p : place) : string = let var = var_id_to_string env p.var_id in projection_to_string env var p.projection -let cast_kind_to_string (env : ('a, 'b) fmt_env) (cast : cast_kind) : string = +let cast_kind_to_string (env : 'a fmt_env) (cast : cast_kind) : string = match cast with | CastScalar (src, tgt) -> "cast<" ^ literal_type_to_string src ^ "," ^ literal_type_to_string tgt @@ -61,14 +61,14 @@ let cast_kind_to_string (env : ('a, 'b) fmt_env) (cast : cast_kind) : string = | CastUnsize (src, tgt) -> "unsize<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">" -let nullop_to_string (env : ('a, 'b) fmt_env) (op : nullop) : string = +let nullop_to_string (env : 'a fmt_env) (op : nullop) : string = match op with | SizeOf -> "size_of" | AlignOf -> "align_of" | OffsetOf _ -> "offset_of(?)" | UbChecks -> "ub_checks" -let unop_to_string (env : ('a, 'b) fmt_env) (unop : unop) : string = +let unop_to_string (env : 'a fmt_env) (unop : unop) : string = match unop with | Not -> "¬" | Neg -> "-" @@ -108,24 +108,23 @@ let assumed_fun_id_to_string (aid : assumed_fun_id) : string = let mutability = ref_kind_to_string mutability in "@" ^ ty ^ op ^ mutability -let fun_id_to_string (env : ('a, 'b) fmt_env) (fid : fun_id) : string = +let fun_id_to_string (env : 'a fmt_env) (fid : fun_id) : string = match fid with | FRegular fid -> fun_decl_id_to_string env fid | FAssumed aid -> assumed_fun_id_to_string aid -let fun_id_or_trait_method_ref_to_string (env : ('a, 'b) fmt_env) +let fun_id_or_trait_method_ref_to_string (env : 'a fmt_env) (r : fun_id_or_trait_method_ref) : string = match r with | TraitMethod (trait_ref, method_name, _) -> trait_ref_to_string env trait_ref ^ "::" ^ method_name | FunId fid -> fun_id_to_string env fid -let fn_ptr_to_string (env : ('a, 'b) fmt_env) (ptr : fn_ptr) : string = +let fn_ptr_to_string (env : 'a fmt_env) (ptr : fn_ptr) : string = let generics = generic_args_to_string env ptr.generics in fun_id_or_trait_method_ref_to_string env ptr.func ^ generics -let constant_expr_to_string (env : ('a, 'b) fmt_env) (cv : constant_expr) : - string = +let constant_expr_to_string (env : 'a fmt_env) (cv : constant_expr) : string = match cv.value with | CLiteral lit -> "(" ^ literal_to_string lit ^ " : " ^ ty_to_string env cv.ty ^ ")" @@ -135,13 +134,13 @@ let constant_expr_to_string (env : ('a, 'b) fmt_env) (cv : constant_expr) : trait_ref ^ const_name | CFnPtr fn_ptr -> fn_ptr_to_string env fn_ptr -let operand_to_string (env : ('a, 'b) fmt_env) (op : operand) : string = +let operand_to_string (env : 'a fmt_env) (op : operand) : string = match op with | Copy p -> "copy " ^ place_to_string env p | Move p -> "move " ^ place_to_string env p | Constant cv -> constant_expr_to_string env cv -let rvalue_to_string (env : ('a, 'b) fmt_env) (rv : rvalue) : string = +let rvalue_to_string (env : 'a fmt_env) (rv : rvalue) : string = match rv with | Use op -> operand_to_string env op | RvRef (p, bk) -> begin diff --git a/charon-ml/src/PrintGAst.ml b/charon-ml/src/PrintGAst.ml index 5b26b8c9..614f66aa 100644 --- a/charon-ml/src/PrintGAst.ml +++ b/charon-ml/src/PrintGAst.ml @@ -15,27 +15,26 @@ let any_decl_id_to_string (id : any_decl_id) : string = | 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 = +let fn_operand_to_string (env : 'a fmt_env) (op : fn_operand) : string = match op with | FnOpRegular func -> fn_ptr_to_string env func | FnOpMove p -> "move " ^ place_to_string env p -let call_to_string (env : ('a, 'b) fmt_env) (indent : string) (call : call) : - string = +let call_to_string (env : 'a fmt_env) (indent : string) (call : call) : string = let func = fn_operand_to_string env call.func in let args = List.map (operand_to_string env) call.args in let args = "(" ^ String.concat ", " args ^ ")" in let dest = place_to_string env call.dest in indent ^ dest ^ " := move " ^ func ^ args -let assertion_to_string (env : ('a, 'b) fmt_env) (indent : string) - (a : assertion) : string = +let assertion_to_string (env : 'a fmt_env) (indent : string) (a : assertion) : + string = let cond = operand_to_string env a.cond in if a.expected then indent ^ "assert(" ^ cond ^ ")" else indent ^ "assert(¬" ^ cond ^ ")" (** Small helper *) -let fun_sig_with_name_to_string (env : ('a, 'b) fmt_env) (indent : string) +let fun_sig_with_name_to_string (env : 'a fmt_env) (indent : string) (indent_incr : string) (attribute : string option) (name : string option) (args : var list option) (sg : fun_sig) : string = let ty_to_string = ty_to_string env in @@ -78,13 +77,13 @@ let fun_sig_with_name_to_string (env : ('a, 'b) fmt_env) (indent : string) indent ^ attribute ^ unsafe ^ "fn" ^ name ^ params ^ "(" ^ args ^ ")" ^ ret_ty ^ clauses -let fun_sig_to_string (env : ('a, 'b) fmt_env) (indent : string) +let fun_sig_to_string (env : 'a fmt_env) (indent : string) (indent_incr : string) (sg : fun_sig) : string = fun_sig_with_name_to_string env indent indent_incr None None None sg -let gfun_decl_to_string (env : ('a, 'b) fmt_env) (indent : string) +let gfun_decl_to_string (env : 'a fmt_env) (indent : string) (indent_incr : string) - (body_to_string : ('a, 'b) fmt_env -> string -> string -> 'body -> string) + (body_to_string : 'a 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 in @@ -132,7 +131,7 @@ let gfun_decl_to_string (env : ('a, 'b) fmt_env) (indent : string) (Some inputs) sg ^ indent ^ "\n{\n" ^ locals ^ "\n\n" ^ body ^ "\n" ^ indent ^ "}" -let trait_decl_to_string (env : ('a, 'b) fmt_env) (indent : string) +let trait_decl_to_string (env : 'a 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 in @@ -203,7 +202,7 @@ let trait_decl_to_string (env : ('a, 'b) fmt_env) (indent : string) "trait " ^ name ^ params ^ clauses ^ items -let trait_impl_to_string (env : ('a, 'b) fmt_env) (indent : string) +let trait_impl_to_string (env : 'a 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 in diff --git a/charon-ml/src/PrintLlbcAst.ml b/charon-ml/src/PrintLlbcAst.ml index 2207b439..66b626fe 100644 --- a/charon-ml/src/PrintLlbcAst.ml +++ b/charon-ml/src/PrintLlbcAst.ml @@ -6,7 +6,7 @@ open PrintTypes open PrintValues open PrintExpressions -type fmt_env = (statement, FunDeclId.id) PrintUtils.fmt_env +type fmt_env = statement PrintUtils.fmt_env (** Pretty-printing for LLBC AST (generic functions) *) module Ast = struct diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index f05f66b0..47f277bf 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -57,7 +57,7 @@ let variant_id_to_pretty_string (id : variant_id) : string = let field_id_to_pretty_string (id : field_id) : string = "Field@" ^ FieldId.to_string id -let region_var_id_to_string (env : ('a, 'b) fmt_env) (db_id : region_db_id) +let region_var_id_to_string (env : 'a fmt_env) (db_id : region_db_id) (id : region_var_id) : string = match List.nth_opt env.regions db_id with | None -> region_var_id_to_pretty_string db_id id @@ -67,7 +67,7 @@ let region_var_id_to_string (env : ('a, 'b) fmt_env) (db_id : region_db_id) | None -> region_var_id_to_pretty_string db_id id | Some r -> region_var_to_string r) -let type_var_id_to_string (env : ('a, 'b) fmt_env) (id : type_var_id) : string = +let type_var_id_to_string (env : 'a 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.generics.types @@ -75,7 +75,7 @@ let type_var_id_to_string (env : ('a, 'b) fmt_env) (id : type_var_id) : string = | None -> type_var_id_to_pretty_string id | Some x -> type_var_to_string x -let const_generic_var_id_to_string (env : ('a, 'b) fmt_env) +let const_generic_var_id_to_string (env : 'a fmt_env) (id : const_generic_var_id) : string = (* Note that the const generics are not necessarily ordered following their indices *) match @@ -86,7 +86,7 @@ let const_generic_var_id_to_string (env : ('a, 'b) fmt_env) | None -> const_generic_var_id_to_pretty_string id | Some x -> const_generic_var_to_string x -let region_to_string (env : ('a, 'b) fmt_env) (r : region) : string = +let region_to_string (env : 'a fmt_env) (r : region) : string = match r with | RStatic -> "'static" | RErased -> "'_" @@ -95,8 +95,8 @@ let region_to_string (env : ('a, 'b) fmt_env) (r : region) : string = let trait_clause_id_to_string _ id = trait_clause_id_to_pretty_string id -let region_binder_to_string (value_to_string : ('a, 'b) fmt_env -> 'c -> string) - (env : ('a, 'b) fmt_env) (rb : 'c region_binder) : string = +let region_binder_to_string (value_to_string : 'a fmt_env -> 'c -> string) + (env : 'a fmt_env) (rb : 'c region_binder) : string = let env = fmt_env_push_regions env rb.binder_regions in let value = value_to_string env rb.binder_value in match rb.binder_regions with @@ -106,7 +106,7 @@ let region_binder_to_string (value_to_string : ('a, 'b) fmt_env -> 'c -> string) ^ String.concat "," (List.map region_var_to_string rb.binder_regions) ^ "> " ^ value -let rec type_id_to_string (env : ('a, 'b) fmt_env) (id : type_id) : string = +let rec type_id_to_string (env : 'a fmt_env) (id : type_id) : string = match id with | TAdtId id -> type_decl_id_to_string env id | TTuple -> "" @@ -123,8 +123,7 @@ and type_decl_id_to_string env def_id = | None -> type_decl_id_to_pretty_string def_id | Some def -> name_to_string env def.item_meta.name -and fun_decl_id_to_string (env : ('a, 'b) fmt_env) (id : FunDeclId.id) : string - = +and fun_decl_id_to_string (env : 'a fmt_env) (id : FunDeclId.id) : string = match FunDeclId.Map.find_opt id env.fun_decls with | None -> fun_decl_id_to_pretty_string id | Some def -> name_to_string env def.item_meta.name @@ -134,8 +133,8 @@ and global_decl_id_to_string env def_id = | None -> global_decl_id_to_pretty_string def_id | Some def -> name_to_string env def.item_meta.name -and global_decl_ref_to_string (env : ('a, 'b) fmt_env) (gr : global_decl_ref) : - string = +and global_decl_ref_to_string (env : 'a fmt_env) (gr : global_decl_ref) : string + = let global_id = global_decl_id_to_string env gr.global_id in let generics = generic_args_to_string env gr.global_generics in global_id ^ generics @@ -150,14 +149,13 @@ and trait_impl_id_to_string env id = | None -> trait_impl_id_to_pretty_string id | Some def -> name_to_string env def.item_meta.name -and const_generic_to_string (env : ('a, 'b) fmt_env) (cg : const_generic) : - string = +and const_generic_to_string (env : 'a fmt_env) (cg : const_generic) : string = match cg with | CgGlobal id -> global_decl_id_to_string env id | CgVar id -> const_generic_var_id_to_string env id | CgValue lit -> literal_to_string lit -and ty_to_string (env : ('a, 'b) fmt_env) (ty : ty) : string = +and ty_to_string (env : 'a fmt_env) (ty : ty) : string = match ty with | TAdt (id, generics) -> let is_tuple = match id with TTuple -> true | _ -> false in @@ -187,7 +185,7 @@ and ty_to_string (env : ('a, 'b) fmt_env) (ty : ty) : string = inputs ^ ty_to_string env output | TDynTrait _ -> "dyn (TODO)" -and params_to_string (env : ('a, 'b) fmt_env) (is_tuple : bool) +and params_to_string (env : 'a fmt_env) (is_tuple : bool) (generics : generic_args) : string = if is_tuple then (* Remark: there shouldn't be any trait ref, but we still print them @@ -204,7 +202,7 @@ and params_to_string (env : ('a, 'b) fmt_env) (is_tuple : bool) - one for the regions, types, const generics - one for the trait refs *) -and generic_args_to_strings (env : ('a, 'b) fmt_env) (generics : generic_args) : +and generic_args_to_strings (env : 'a fmt_env) (generics : generic_args) : string list * string list = let { regions; types; const_generics; trait_refs } = generics in let regions = List.map (region_to_string env) regions in @@ -214,8 +212,8 @@ and generic_args_to_strings (env : ('a, 'b) fmt_env) (generics : generic_args) : let trait_refs = List.map (trait_ref_to_string env) trait_refs in (params, trait_refs) -and generic_args_to_string (env : ('a, 'b) fmt_env) (generics : generic_args) : - string = +and generic_args_to_string (env : 'a fmt_env) (generics : generic_args) : string + = let params, trait_refs = generic_args_to_strings env generics in let params = if params = [] then "" else "<" ^ String.concat ", " params ^ ">" @@ -225,17 +223,16 @@ and generic_args_to_string (env : ('a, 'b) fmt_env) (generics : generic_args) : in params ^ trait_refs -and trait_ref_to_string (env : ('a, 'b) fmt_env) (tr : trait_ref) : string = +and trait_ref_to_string (env : 'a fmt_env) (tr : trait_ref) : string = trait_instance_id_to_string env tr.trait_id -and trait_decl_ref_to_string (env : ('a, 'b) fmt_env) (tr : trait_decl_ref) : - string = +and trait_decl_ref_to_string (env : 'a fmt_env) (tr : trait_decl_ref) : string = let trait_id = trait_decl_id_to_string env tr.trait_decl_id in let generics = generic_args_to_string env tr.decl_generics in trait_id ^ generics -and trait_instance_id_to_string (env : ('a, 'b) fmt_env) - (id : trait_instance_id) : string = +and trait_instance_id_to_string (env : 'a fmt_env) (id : trait_instance_id) : + string = match id with | Self -> "Self" | TraitImpl (id, generics) -> @@ -265,7 +262,7 @@ and trait_instance_id_to_string (env : ('a, 'b) fmt_env) ^ ")" | UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")" -and impl_elem_to_string (env : ('a, 'b) fmt_env) (elem : impl_elem) : string = +and impl_elem_to_string (env : 'a fmt_env) (elem : impl_elem) : string = match elem with | ImplElemTy (generics, ty) -> (* Locally replace the generics and the predicates *) @@ -288,7 +285,7 @@ and impl_elem_to_string (env : ('a, 'b) fmt_env) (elem : impl_elem) : string = tr ^ " for " ^ ty end -and path_elem_to_string (env : ('a, 'b) fmt_env) (e : path_elem) : string = +and path_elem_to_string (env : 'a fmt_env) (e : path_elem) : string = match e with | PeIdent (s, d) -> let d = @@ -301,7 +298,7 @@ and path_elem_to_string (env : ('a, 'b) fmt_env) (e : path_elem) : string = in "{" ^ impl_elem_to_string env impl ^ "}" ^ d -and name_to_string (env : ('a, 'b) fmt_env) (n : name) : string = +and name_to_string (env : 'a fmt_env) (n : name) : string = let name = List.map (path_elem_to_string env) n in String.concat "::" name @@ -311,16 +308,15 @@ and raw_attribute_to_string (attr : raw_attribute) : string = in attr.path ^ args -let trait_clause_to_string (env : ('a, 'b) fmt_env) (clause : trait_clause) : - string = +let trait_clause_to_string (env : 'a fmt_env) (clause : trait_clause) : string = let clause_id = trait_clause_id_to_string env clause.clause_id in let trait = region_binder_to_string trait_decl_ref_to_string env clause.trait in "[" ^ clause_id ^ "]: " ^ trait -let generic_params_to_strings (env : ('a, 'b) fmt_env) - (generics : generic_params) : string list * string list = +let generic_params_to_strings (env : 'a fmt_env) (generics : generic_params) : + string list * string list = let { regions; types; const_generics; trait_clauses; _ } : generic_params = generics in @@ -341,7 +337,7 @@ let variant_to_string env (v : variant) : string = ^ String.concat ", " (List.map (field_to_string env) v.fields) ^ ")" -let trait_type_constraint_to_string (env : ('a, 'b) fmt_env) +let trait_type_constraint_to_string (env : 'a fmt_env) (ttc : trait_type_constraint) : string = let { trait_ref; type_name; ty } = ttc in let trait_ref = trait_ref_to_string env trait_ref in @@ -371,8 +367,8 @@ let clauses_to_string (indent : string) (indent_incr : string) "\n" ^ String.concat "\n" clauses (** 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) +let predicates_and_trait_clauses_to_string (env : 'a fmt_env) (indent : string) + (indent_incr : string) (params_info : params_info option) (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 @@ -424,7 +420,7 @@ let predicates_and_trait_clauses_to_string (env : ('a, 'b) fmt_env) in (params, clauses) -let type_decl_to_string (env : ('a, 'b) fmt_env) (def : type_decl) : string = +let type_decl_to_string (env : 'a fmt_env) (def : type_decl) : string = (* Locally update the generics and the predicates *) let env = fmt_env_update_generics_and_preds env def.generics in let params, clauses = @@ -462,7 +458,7 @@ let type_decl_to_string (env : ('a, 'b) fmt_env) (def : type_decl) : string = | Opaque -> "opaque type " ^ name ^ params ^ clauses | Error err -> "error(\"" ^ err ^ "\")" -let adt_variant_to_string (env : ('a, 'b) fmt_env) (def_id : TypeDeclId.id) +let adt_variant_to_string (env : 'a fmt_env) (def_id : TypeDeclId.id) (variant_id : VariantId.id) : string = match TypeDeclId.Map.find_opt def_id env.type_decls with | None -> @@ -477,7 +473,7 @@ let adt_variant_to_string (env : ('a, 'b) fmt_env) (def_id : TypeDeclId.id) | _ -> raise (Failure "Unreachable") end -let adt_field_names (env : ('a, 'b) fmt_env) (def_id : TypeDeclId.id) +let adt_field_names (env : 'a fmt_env) (def_id : TypeDeclId.id) (opt_variant_id : VariantId.id option) : string list option = match TypeDeclId.Map.find_opt def_id env.type_decls with | None -> None @@ -493,7 +489,7 @@ let adt_field_names (env : ('a, 'b) fmt_env) (def_id : TypeDeclId.id) Some fields else None -let adt_field_to_string (env : ('a, 'b) fmt_env) (def_id : TypeDeclId.id) +let adt_field_to_string (env : 'a fmt_env) (def_id : TypeDeclId.id) (opt_variant_id : VariantId.id option) (field_id : FieldId.id) : string option = match TypeDeclId.Map.find_opt def_id env.type_decls with diff --git a/charon-ml/src/PrintUllbcAst.ml b/charon-ml/src/PrintUllbcAst.ml index d750e913..e5861444 100644 --- a/charon-ml/src/PrintUllbcAst.ml +++ b/charon-ml/src/PrintUllbcAst.ml @@ -6,7 +6,7 @@ open PrintTypes open PrintValues open PrintExpressions -type fmt_env = (blocks, global_body option) PrintUtils.fmt_env +type fmt_env = blocks PrintUtils.fmt_env (** Pretty-printing for ULLBC AST (generic functions) *) module Ast = struct @@ -103,16 +103,8 @@ module Ast = struct let name = name_to_string env def.item_meta.name in let ty = ty_to_string env def.ty in - (* We print the declaration differently if it is opaque (no body) or transparent - * (we have access to a body) *) - match def.body with - | None -> - (* Put everything together *) - indent ^ "opaque global " ^ name ^ params ^ clauses ^ " : " ^ ty - | Some body -> - let body = blocks_to_string env indent indent_incr body.body in - indent ^ "global " ^ name ^ params ^ clauses ^ " : " ^ ty ^ " =\n" - ^ body + let body_id = fun_decl_id_to_string env def.body in + indent ^ "global " ^ name ^ params ^ clauses ^ " : " ^ ty ^ " = " ^ body_id end (** Pretty-printing for ASTs (functions based on a declaration context) *) diff --git a/charon-ml/src/PrintUtils.ml b/charon-ml/src/PrintUtils.ml index 931f5e84..424bafef 100644 --- a/charon-ml/src/PrintUtils.ml +++ b/charon-ml/src/PrintUtils.ml @@ -11,10 +11,10 @@ let block_id_to_string (id : UllbcAst.BlockId.id) : string = (** The formatting environment can be incomplete: if some information is missing (for instance we can't find the type variable for a given index) we print the id in raw format. *) -type ('fun_body, 'global_body) fmt_env = { +type 'fun_body fmt_env = { type_decls : type_decl TypeDeclId.Map.t; fun_decls : 'fun_body gfun_decl FunDeclId.Map.t; - global_decls : 'global_body gglobal_decl GlobalDeclId.Map.t; + global_decls : global_decl GlobalDeclId.Map.t; trait_decls : trait_decl TraitDeclId.Map.t; trait_impls : trait_impl TraitImplId.Map.t; regions : region_var list list; @@ -32,11 +32,11 @@ type ('fun_body, 'global_body) fmt_env = { (** 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) : ('a, 'b) fmt_env = +let fmt_env_update_generics_and_preds (env : 'a fmt_env) + (generics : generic_params) : 'a 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 = +let fmt_env_push_regions (env : 'a fmt_env) (regions : region_var list) : + 'a fmt_env = { env with regions = regions :: env.regions } diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index 53195a6f..9f62146a 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -49,17 +49,17 @@ type ('id, 'name) indexed_var = { [@@deriving show, ord] type fun_decl_id = FunDeclId.id +and type_decl_id = TypeDeclId.id +and global_decl_id = GlobalDeclId.id +and trait_decl_id = TraitDeclId.id +and trait_impl_id = TraitImplId.id and disambiguator = Disambiguator.id and type_var_id = TypeVarId.id -and type_decl_id = TypeDeclId.id and variant_id = VariantId.id and field_id = FieldId.id and region_id = RegionId.id and const_generic_var_id = ConstGenericVarId.id -and global_decl_id = GlobalDeclId.id -and trait_clause_id = TraitClauseId.id -and trait_decl_id = TraitDeclId.id -and trait_impl_id = TraitImplId.id [@@deriving show, ord] +and trait_clause_id = TraitClauseId.id [@@deriving show, ord] let all_signed_int_types = [ Isize; I8; I16; I32; I64; I128 ] let all_unsigned_int_types = [ Usize; U8; U16; U32; U64; U128 ] diff --git a/charon-ml/src/UllbcAst.ml b/charon-ml/src/UllbcAst.ml index 84d16c5e..944af7f6 100644 --- a/charon-ml/src/UllbcAst.ml +++ b/charon-ml/src/UllbcAst.ml @@ -110,8 +110,6 @@ and block = { statements : statement list; terminator : terminator } type expr_body = blocks gexpr_body [@@deriving show] type fun_body = expr_body [@@deriving show] type fun_decl = blocks gfun_decl [@@deriving show] -type global_body = expr_body [@@deriving show] -type global_decl = global_body option gglobal_decl [@@deriving show] (** ULLBC crate *) -type crate = (blocks, global_body option) gcrate +type crate = blocks gcrate diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 3b198a8f..3f47ff2f 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -217,7 +217,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.45" +version = "0.1.47" dependencies = [ "anyhow", "assert_cmd", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 2d91f10d..489b5574 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.45" +version = "0.1.47" authors = ["Son Ho "] edition = "2021" license = "Apache-2.0" diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs index 3000104a..16fef627 100644 --- a/charon/src/ast/expressions.rs +++ b/charon/src/ast/expressions.rs @@ -1,8 +1,6 @@ //! Implements expressions: paths, operands, rvalues, lvalues -use crate::gast::*; -use crate::types::*; -use crate::values::*; +use crate::ast::*; use derive_visitor::{Drive, DriveMut}; use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName}; use serde::{Deserialize, Serialize}; diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs index 5e8fcb39..4c592087 100644 --- a/charon/src/ast/gast.rs +++ b/charon/src/ast/gast.rs @@ -1,23 +1,15 @@ //! Definitions common to [crate::ullbc_ast] and [crate::llbc_ast] pub use super::gast_utils::*; -use crate::expressions::*; -use crate::generate_index_type; +use crate::ast::*; use crate::ids::Vector; use crate::llbc_ast; -use crate::meta::{ItemMeta, Span}; -use crate::names::Name; -use crate::types::*; use crate::ullbc_ast; -use crate::values::*; use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut}; use macros::EnumIsA; use macros::EnumToGetters; use serde::{Deserialize, Serialize}; use std::collections::HashMap; -generate_index_type!(FunDeclId, "Fun"); -generate_index_type!(BodyId, "Body"); - /// A variable #[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Var { @@ -157,7 +149,7 @@ pub struct FunDecl { pub body: Result, } -/// A global variable definition +/// A global variable definition (constant or static). #[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct GlobalDecl { #[drive(skip)] @@ -168,7 +160,9 @@ pub struct GlobalDecl { pub ty: Ty, /// The global kind: "regular" function, trait const declaration, etc. pub kind: ItemKind, - pub body: Result, + /// The initializer function used to compute the initial value for this constant/static. + #[charon::rename("body")] + pub init: FunDeclId, } /// Reference to a global declaration. diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs index f20e2136..d9394e13 100644 --- a/charon/src/ast/krate.rs +++ b/charon/src/ast/krate.rs @@ -12,6 +12,13 @@ use std::collections::HashMap; use std::fmt; use std::ops::{Index, IndexMut}; +generate_index_type!(FunDeclId, "Fun"); +generate_index_type!(TypeDeclId, "Adt"); +generate_index_type!(GlobalDeclId, "Global"); +generate_index_type!(TraitDeclId, "TraitDecl"); +generate_index_type!(TraitImplId, "TraitImpl"); +generate_index_type!(BodyId, "Body"); + /// The id of a translated item. #[derive( Copy, @@ -87,14 +94,6 @@ pub struct TranslatedCrate { /// The name of the crate according to rustc. pub real_crate_name: String, - /// File names to ids and vice-versa - #[drive(skip)] - pub id_to_file: Vector, - #[drive(skip)] - #[serde(skip)] - #[charon::opaque] - pub file_to_id: HashMap, - /// File id to content. /// /// Note that some files may be missing, if they are not "real" files. @@ -102,7 +101,7 @@ pub struct TranslatedCrate { #[serde(with = "HashMapToArray::")] pub file_id_to_content: HashMap, - /// All the ids, in the order in which we encountered them + /// All the item ids, in the order in which we encountered them #[drive(skip)] pub all_ids: LinkedHashSet, /// The names of all registered items. Available so we can know the names even of items that @@ -110,13 +109,16 @@ pub struct TranslatedCrate { #[serde(with = "HashMapToArray::")] pub item_names: HashMap, + /// The translated files. + #[drive(skip)] + pub id_to_file: Vector, /// The translated type definitions pub type_decls: Vector, /// The translated function definitions pub fun_decls: Vector, /// The translated global definitions pub global_decls: Vector, - /// The bodies of functions and constants + /// The bodies of functions pub bodies: Vector, /// The translated trait declarations pub trait_decls: Vector, diff --git a/charon/src/ast/names.rs b/charon/src/ast/names.rs index 47136f2f..ab7e9f09 100644 --- a/charon/src/ast/names.rs +++ b/charon/src/ast/names.rs @@ -1,5 +1,5 @@ //! Defines some utilities for the variables -use crate::types::*; +use crate::ast::*; use derive_visitor::{Drive, DriveMut}; use macros::{EnumAsGetters, EnumIsA}; use serde::{Deserialize, Serialize}; diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index ea50a21b..0e3ab3df 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -12,12 +12,10 @@ pub type FieldName = String; // utilities like a fresh index generator. Those structures and utilities are // generated by using macros. generate_index_type!(TypeVarId, "T"); -generate_index_type!(TypeDeclId, "Adt"); generate_index_type!(VariantId, "Variant"); generate_index_type!(FieldId, "Field"); generate_index_type!(RegionId, "Region"); generate_index_type!(ConstGenericVarId, "Const"); -generate_index_type!(GlobalDeclId, "Global"); /// Type variable. /// We make sure not to mix variables and type variables by having two distinct @@ -342,8 +340,6 @@ pub struct GenericParams { pub struct ExistentialPredicate; generate_index_type!(TraitClauseId, "TraitClause"); -generate_index_type!(TraitDeclId, "TraitDecl"); -generate_index_type!(TraitImplId, "TraitImpl"); /// A predicate of the form `Type: Trait`. #[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] @@ -883,6 +879,9 @@ pub struct FunSig { /// (the function in which the closure is defined) /// - the region variables are local to the closure pub is_closure: bool, + /// Whether this function is in fact the body of a constant/static that we turned into an + /// initializer function. + pub is_global_initializer: bool, /// Additional information if this is the signature of a closure. pub closure_info: Option, pub generics: GenericParams, diff --git a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs index bd7091f6..928ac0a1 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs @@ -109,12 +109,13 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } } - pub(crate) fn translate_item(&mut self, rust_id: DefId, trans_id: AnyTransId) { + pub(crate) fn translate_item(&mut self, item_src: TransItemSource, trans_id: AnyTransId) { if self.errors.ignored_failed_decls.contains(&trans_id) || self.translated.get_item(trans_id).is_some() { return; } + let rust_id = item_src.to_def_id(); self.with_def_id(rust_id, trans_id, |mut ctx| { let span = ctx.def_span(rust_id); // Catch cycles @@ -211,12 +212,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { /// translated version of this item. #[allow(dead_code)] pub(crate) fn get_or_translate(&mut self, id: AnyTransId) -> Result, Error> { - let rust_id = *self.reverse_id_map.get(&id).unwrap(); + let item_source = *self.reverse_id_map.get(&id).unwrap(); // Translate if not already translated. - self.translate_item(rust_id, id); + self.translate_item(item_source, id); if self.errors.ignored_failed_decls.contains(&id) { - let span = self.def_span(rust_id); + let span = self.def_span(item_source.to_def_id()); error_or_panic!(self, span, format!("Failed to translate item {id:?}.")) } Ok(self.translated.get_item(id).unwrap()) @@ -273,6 +274,7 @@ pub fn translate<'tcx, 'ctx>( }, id_map: Default::default(), reverse_id_map: Default::default(), + file_to_id: Default::default(), items_to_translate: Default::default(), translate_stack: Default::default(), cached_names: Default::default(), @@ -298,9 +300,9 @@ pub fn translate<'tcx, 'ctx>( // Note that the order in which we translate the definitions doesn't matter: // we never need to lookup a translated definition, and only use the map // from Rust ids to translated ids. - while let Some((ord_id, trans_id)) = ctx.items_to_translate.pop_first() { - trace!("About to translate id: {:?}", ord_id); - ctx.translate_item(ord_id.get_id(), trans_id); + while let Some((item_src, trans_id)) = ctx.items_to_translate.pop_first() { + trace!("About to translate item: {:?}", item_src); + ctx.translate_item(item_src, trans_id); } // Return the context, dropping the hax state and rustc `tcx`. diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 92ade0c9..a6832167 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -113,8 +113,10 @@ impl TranslateOptions { } } -/// The id of an untranslated item. -#[derive(Clone, Copy, Debug, PartialEq, Eq, VariantIndexArity)] +/// The id of an untranslated item. Note that a given `DefId` may show up as multiple different +/// item sources, e.g. a constant will have both a `Global` version (for the constant itself) and a +/// `FunDecl` one (for its initializer function). +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, VariantIndexArity)] pub enum TransItemSource { Global(DefId), TraitDecl(DefId), @@ -124,7 +126,7 @@ pub enum TransItemSource { } impl TransItemSource { - pub(crate) fn get_id(&self) -> DefId { + pub(crate) fn to_def_id(&self) -> DefId { match self { TransItemSource::Global(id) | TransItemSource::TraitDecl(id) @@ -139,7 +141,7 @@ impl TransItemSource { /// Value with which we order values. fn sort_key(&self) -> impl Ord { let (variant_index, _) = self.variant_index_arity(); - let def_id = self.get_id(); + let def_id = self.to_def_id(); (variant_index, def_id.index, def_id.krate) } } @@ -171,9 +173,11 @@ pub struct TranslateCtx<'tcx, 'ctx> { pub translated: TranslatedCrate, /// The map from rustc id to translated id. - pub id_map: HashMap, + pub id_map: HashMap, /// The reverse map of ids. - pub reverse_id_map: HashMap, + pub reverse_id_map: HashMap, + /// The reverse filename map. + pub file_to_id: HashMap, /// Context for tracking and reporting errors. pub errors: ErrorCtx<'ctx>, @@ -299,11 +303,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { /// `span` must be a span from which we obtained that filename. fn register_file(&mut self, filename: FileName, span: rustc_span::Span) -> FileId { // Lookup the file if it was already registered - match self.translated.file_to_id.get(&filename) { + match self.file_to_id.get(&filename) { Some(id) => *id, None => { let id = self.translated.id_to_file.push(filename.clone()); - self.translated.file_to_id.insert(filename.clone(), id); + self.file_to_id.insert(filename.clone(), id); let source_file = self.tcx.sess.source_map().lookup_source_file(span.lo()); if let Some(src) = source_file.src.as_deref() { self.translated.file_id_to_content.insert(id, src.clone()); @@ -766,8 +770,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { src: &Option, id: TransItemSource, ) -> AnyTransId { - let rust_id = id.get_id(); - let item_id = match self.id_map.get(&rust_id) { + let item_id = match self.id_map.get(&id) { Some(tid) => *tid, None => { let trans_id = match id { @@ -789,20 +792,20 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { }; // Add the id to the queue of declarations to translate self.items_to_translate.insert(id, trans_id); - self.id_map.insert(id.get_id(), trans_id); - self.reverse_id_map.insert(trans_id, id.get_id()); + self.id_map.insert(id, trans_id); + self.reverse_id_map.insert(trans_id, id); self.translated.all_ids.insert(trans_id); // Store the name early so the name matcher can identify paths. We can't to it for // trait impls because they register themselves when computing their name. if !matches!(id, TransItemSource::TraitImpl(_)) { - if let Ok(name) = self.def_id_to_name(rust_id) { + if let Ok(name) = self.def_id_to_name(id.to_def_id()) { self.translated.item_names.insert(trans_id, name); } } trans_id } }; - self.register_dep_source(src, rust_id, item_id); + self.register_dep_source(src, id.to_def_id(), item_id); item_id } diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs index 5165329e..1360ae5e 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs @@ -1351,6 +1351,23 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { "Casting constructors to function pointers is not supported" ) } + hax::FullDefKind::Const { ty, .. } + | hax::FullDefKind::AssocConst { ty, .. } + | hax::FullDefKind::Static { ty, .. } => { + let sig = hax::TyFnSig { + inputs: vec![], + output: ty.clone(), + c_variadic: false, + safety: hax::Safety::Safe, + abi: hax::Abi::Abi { + todo: String::new(), + }, + }; + &hax::Binder { + value: sig, + bound_vars: Default::default(), + } + } _ => panic!("Unexpected definition for function: {def:?}"), }; @@ -1393,9 +1410,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { .try_collect()?; Some(ClosureInfo { kind, state }) } - hax::FullDefKind::Fn { .. } => None, - hax::FullDefKind::AssocFn { .. } => None, - _ => panic!("Unexpected definition for function: {def:?}"), + _ => None, }; let parent_params_info = match &def.kind { @@ -1425,6 +1440,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { generics, is_unsafe, is_closure: matches!(&def.kind, hax::FullDefKind::Closure { .. }), + is_global_initializer: matches!( + &def.kind, + hax::FullDefKind::Const { .. } + | hax::FullDefKind::AssocConst { .. } + | hax::FullDefKind::Static { .. } + ), closure_info, parent_params_info, inputs, @@ -1517,16 +1538,7 @@ impl BodyTransCtx<'_, '_, '_> { }; let ty = self.translate_ty(span, ty)?; - // Translate its body like the body of a function. This returns `Opaque if we can't/decide - // not to translate this body. - let body_id = match self.translate_body(def, 0, &item_meta) { - Ok(Ok(body)) => Ok(self.t_ctx.translated.bodies.push(body)), - // Opaque declaration - Ok(Err(Opaque)) => Err(Opaque), - // Translation error. We reserve a slot and leave it empty. - // FIXME: handle error cases more explicitly. - Err(_) => Ok(self.t_ctx.translated.bodies.reserve_slot()), - }; + let initializer = self.register_fun_decl_id(span, rust_id); Ok(GlobalDecl { def_id, @@ -1534,7 +1546,7 @@ impl BodyTransCtx<'_, '_, '_> { generics, ty, kind: global_kind, - body: body_id, + init: initializer, }) } } diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index b1c8c45a..ef634b43 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -1214,7 +1214,6 @@ fn generate_ml( "Body", "BodyId", "FunDecl", - "GlobalDecl", "TranslatedCrate", ] .iter() @@ -1275,6 +1274,7 @@ fn generate_ml( "FunSig", "ItemKind", "GExprBody", + "GlobalDecl", "TraitDecl", "TraitImpl", "GDeclarationGroup", diff --git a/charon/src/bin/generate-ml/templates/GAst.ml b/charon/src/bin/generate-ml/templates/GAst.ml index 3eb275cb..18410520 100644 --- a/charon/src/bin/generate-ml/templates/GAst.ml +++ b/charon/src/bin/generate-ml/templates/GAst.ml @@ -54,30 +54,18 @@ type 'body gfun_decl = { signature : fun_sig; kind : item_kind; body : 'body gexpr_body option; - is_global_decl_body : bool; -} -[@@deriving show] - -(* Hand-written because the rust equivalent isn't generic *) -type 'body gglobal_decl = { - def_id : GlobalDeclId.id; - item_meta : item_meta; - generics : generic_params; - ty : ty; - kind : item_kind; - body : 'body; } [@@deriving show] (* Hand-written because the rust equivalent isn't generic *) (** A crate *) -type ('fun_body, 'global_body) gcrate = { +type 'fun_body gcrate = { name : string; declarations : declaration_group list; type_decls : type_decl TypeDeclId.Map.t; fun_decls : 'fun_body gfun_decl FunDeclId.Map.t; - global_decls : 'global_body gglobal_decl GlobalDeclId.Map.t; + global_decls : global_decl GlobalDeclId.Map.t; trait_decls : trait_decl TraitDeclId.Map.t; trait_impls : trait_impl TraitImplId.Map.t; source_files : string FileNameMap.t; diff --git a/charon/src/bin/generate-ml/templates/GAstOfJson.ml b/charon/src/bin/generate-ml/templates/GAstOfJson.ml index dd6d5192..281f3f01 100644 --- a/charon/src/bin/generate-ml/templates/GAstOfJson.ml +++ b/charon/src/bin/generate-ml/templates/GAstOfJson.ml @@ -79,37 +79,9 @@ and gfun_decl_of_json (bodies : 'body gexpr_body option list) signature; kind; body; - is_global_decl_body = false; } | _ -> Error "") -(* This is written by hand because the corresponding rust type is not type-generic. *) -and gglobal_decl_of_json (bodies : 'body gexpr_body option list) - (id_to_file : id_to_file_map) (js : json) : - ('body gexpr_body option gglobal_decl, string) result = - combine_error_msgs js __FUNCTION__ - (match js with - | `Assoc - [ - ("def_id", def_id); - ("item_meta", item_meta); - ("generics", generics); - ("ty", ty); - ("kind", kind); - ("body", body); - ] -> - let* global_id = GlobalDeclId.id_of_json def_id 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* ty = ty_of_json ty in - let* kind = item_kind_of_json kind in - let* body = maybe_opaque_body_of_json bodies body in - let global = - { def_id = global_id; item_meta; body; generics; ty; kind } - in - Ok global - | _ -> Error "") - (** Deserialize a map from file id to file name. In the serialized LLBC, the files in the loc spans are refered to by their @@ -134,17 +106,17 @@ and id_to_file_of_json (js : json) : (id_to_file_map, string) result = (* This is written by hand because the corresponding rust type is not type-generic. *) and gtranslated_crate_of_json (body_of_json : id_to_file_map -> json -> ('body gexpr_body, string) result) - (js : json) : (('body, 'body gexpr_body option) gcrate, string) result = + (js : json) : ('body gcrate, string) result = combine_error_msgs js __FUNCTION__ (match js with | `Assoc [ ("crate_name", name); ("real_crate_name", _); - ("id_to_file", id_to_file); ("file_id_to_content", file_id_to_content); ("all_ids", _); ("item_names", _); + ("id_to_file", id_to_file); ("type_decls", types); ("fun_decls", functions); ("global_decls", globals); @@ -173,7 +145,7 @@ and gtranslated_crate_of_json in let* globals = vector_of_json global_decl_id_of_json - (gglobal_decl_of_json bodies id_to_file) + (global_decl_of_json id_to_file) globals in let* trait_decls = @@ -202,9 +174,7 @@ and gtranslated_crate_of_json in let global_decls = GlobalDeclId.Map.of_list - (List.map - (fun (d : 'body gexpr_body option gglobal_decl) -> (d.def_id, d)) - globals) + (List.map (fun (d : global_decl) -> (d.def_id, d)) globals) in let trait_decls = TraitDeclId.Map.of_list @@ -239,7 +209,7 @@ and gtranslated_crate_of_json and gcrate_of_json (body_of_json : id_to_file_map -> json -> ('body gexpr_body, string) result) - (js : json) : (('body, 'body gexpr_body option) gcrate, string) result = + (js : json) : ('body gcrate, string) result = match js with | `Assoc [ ("charon_version", charon_version); ("translated", translated) ] -> (* Ensure the version is the one we support. *) diff --git a/charon/src/bin/generate-ml/templates/LlbcAst.ml b/charon/src/bin/generate-ml/templates/LlbcAst.ml index f4736db9..e5abb8c9 100644 --- a/charon/src/bin/generate-ml/templates/LlbcAst.ml +++ b/charon/src/bin/generate-ml/templates/LlbcAst.ml @@ -10,8 +10,5 @@ type expr_body = statement gexpr_body [@@deriving show] type fun_body = expr_body [@@deriving show] type fun_decl = statement gfun_decl [@@deriving show] -(* TODO: the function id should be an option *) -type global_decl = FunDeclId.id gglobal_decl [@@deriving show] - (** LLBC crate *) -type crate = (statement, FunDeclId.id) gcrate +type crate = statement gcrate diff --git a/charon/src/bin/generate-ml/templates/LlbcOfJson.ml b/charon/src/bin/generate-ml/templates/LlbcOfJson.ml index 15df0fce..4c832d46 100644 --- a/charon/src/bin/generate-ml/templates/LlbcOfJson.ml +++ b/charon/src/bin/generate-ml/templates/LlbcOfJson.ml @@ -21,97 +21,5 @@ let expr_body_of_json (id_to_file : id_to_file_map) (js : json) : Ok body | _ -> Error "") -(** Strict type for the number of function declarations (see {!global_to_fun_id} below) *) -type global_id_converter = { max_fun_id : int } [@@deriving show] - -(** Converts a global id to its corresponding function id. - To do so, it adds the global id to the number of function declarations : - We have the bijection [global_fun_id <=> global_id + fun_id_count]. -*) -let global_to_fun_id (conv : global_id_converter) (gid : GlobalDeclId.id) : - FunDeclId.id = - FunDeclId.of_int (GlobalDeclId.to_int gid + conv.max_fun_id) - -(** Deserialize a global declaration, and decompose it into a global declaration - and a function declaration. - *) -let split_global (gid_conv : global_id_converter) global : - global_decl * fun_decl = - (* Deserialize the global declaration *) - let { def_id = global_id; item_meta; body; generics; ty; kind } = global in - (* Decompose into a global and a function *) - let fun_id = global_to_fun_id gid_conv global.def_id in - let signature : fun_sig = - { - (* Not sure about `is_unsafe` actually *) - is_unsafe = false; - is_closure = false; - closure_info = None; - generics; - parent_params_info = None; - inputs = []; - output = ty; - } - in - let global_decl : global_decl = - { def_id = global_id; item_meta; body = fun_id; generics; ty; kind } - in - let fun_decl : fun_decl = - { - def_id = fun_id; - item_meta; - signature; - kind = RegularItem; - body; - is_global_decl_body = true; - } - in - (global_decl, fun_decl) - let crate_of_json (js : json) : (crate, string) result = - begin - let* crate = gcrate_of_json expr_body_of_json js in - (* When deserializing the globals, we split the global declarations - * between the globals themselves and their bodies, which are simply - * functions with no arguments. We add the global bodies to the list - * of function declarations; we give fresh ids to these new bodies - * by incrementing from the last function id recorded *) - let gid_conv = - { - max_fun_id = - List.fold_left - (fun acc (id, _) -> max acc (1 + FunDeclId.to_int id)) - 0 - (FunDeclId.Map.bindings crate.fun_decls); - } - in - let globals, global_bodies = - List.split - (List.map - (fun (_, g) -> split_global gid_conv g) - (GlobalDeclId.Map.bindings crate.global_decls)) - in - - (* Add the global bodies to the list of functions *) - let fun_decls = - List.fold_left - (fun m (d : fun_decl) -> FunDeclId.Map.add d.def_id d m) - crate.fun_decls global_bodies - in - let global_decls = - GlobalDeclId.Map.of_list - (List.map (fun (d : global_decl) -> (d.def_id, d)) globals) - in - - Ok - { - name = crate.name; - declarations = crate.declarations; - type_decls = crate.type_decls; - fun_decls; - global_decls; - trait_decls = crate.trait_decls; - trait_impls = crate.trait_impls; - source_files = crate.source_files; - } - end + gcrate_of_json expr_body_of_json js diff --git a/charon/src/bin/generate-ml/templates/UllbcAst.ml b/charon/src/bin/generate-ml/templates/UllbcAst.ml index 22bff3a8..27d7916d 100644 --- a/charon/src/bin/generate-ml/templates/UllbcAst.ml +++ b/charon/src/bin/generate-ml/templates/UllbcAst.ml @@ -18,8 +18,6 @@ type block_id = BlockId.id [@@deriving show, ord] type expr_body = blocks gexpr_body [@@deriving show] type fun_body = expr_body [@@deriving show] type fun_decl = blocks gfun_decl [@@deriving show] -type global_body = expr_body [@@deriving show] -type global_decl = global_body option gglobal_decl [@@deriving show] (** ULLBC crate *) -type crate = (blocks, global_body option) gcrate +type crate = blocks gcrate diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index ecdfea53..c058e81b 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -633,6 +633,8 @@ where let (params, preds, any_where) = self .generics .fmt_with_ctx_with_trait_clauses(ctx, " ", &None); + // Type + let ty = self.ty.fmt_with_ctx(ctx); // Predicates let eq_space = if !any_where { " ".to_string() @@ -642,23 +644,10 @@ where // Decl name let name = self.item_meta.name.fmt_with_ctx(ctx); - - // Body - let body = match self.body { - Ok(body_id) => { - // FIXME: pass the indent here somehow - let body = ctx.format_object(body_id); - if body == "" { - String::new() - } else { - format!(" {{\n{body}{tab}}}") - } - } - Err(Opaque) => String::new(), - }; + let initializer = ctx.format_object(self.init); // Put everything together - format!("{tab}global {name}{params}{preds}{eq_space}{body}") + format!("{tab}global {name}{params}: {ty}{preds}{eq_space}= {initializer}()") } } diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs index cb12cf06..ddf54215 100644 --- a/charon/src/transform/ctx.rs +++ b/charon/src/transform/ctx.rs @@ -52,18 +52,6 @@ pub trait UllbcPass: Sync { } } - /// Transform a global declaration. This forwards to `transform_body` by default. - fn transform_global( - &self, - ctx: &mut TransformCtx<'_>, - _decl: &mut GlobalDecl, - body: Result<&mut ullbc_ast::ExprBody, Opaque>, - ) { - if let Ok(body) = body { - self.transform_body(ctx, body) - } - } - /// Transform the given context. This forwards to the other methods by default. fn transform_ctx(&self, ctx: &mut TransformCtx<'_>) { ctx.for_each_fun_decl(|ctx, decl, body| { @@ -71,11 +59,6 @@ pub trait UllbcPass: Sync { self.log_before_body(ctx, &decl.item_meta.name, body.as_deref()); self.transform_function(ctx, decl, body); }); - ctx.for_each_global_decl(|ctx, decl, body| { - let body = body.map(|body| body.as_unstructured_mut().unwrap()); - self.log_before_body(ctx, &decl.item_meta.name, body.as_deref()); - self.transform_global(ctx, decl, body); - }); } /// The name of the pass, used for debug logging. The default implementation uses the type @@ -123,18 +106,6 @@ pub trait LlbcPass: Sync { } } - /// Transform a global declaration. This forwards to `transform_body` by default. - fn transform_global( - &self, - ctx: &mut TransformCtx<'_>, - _decl: &mut GlobalDecl, - body: Result<&mut llbc_ast::ExprBody, Opaque>, - ) { - if let Ok(body) = body { - self.transform_body(ctx, body) - } - } - /// Transform the given context. This forwards to the other methods by default. fn transform_ctx(&self, ctx: &mut TransformCtx<'_>) { ctx.for_each_fun_decl(|ctx, decl, body| { @@ -142,11 +113,6 @@ pub trait LlbcPass: Sync { self.log_before_body(ctx, &decl.item_meta.name, body.as_deref()); self.transform_function(ctx, decl, body); }); - ctx.for_each_global_decl(|ctx, decl, body| { - let body = body.map(|body| body.as_structured_mut().unwrap()); - self.log_before_body(ctx, &decl.item_meta.name, body.as_deref()); - self.transform_global(ctx, decl, body); - }); } /// The name of the pass, used for debug logging. The default implementation uses the type @@ -240,16 +206,6 @@ impl<'ctx> TransformCtx<'ctx> { self.translated.fun_decls = fun_decls; ret } - /// Get mutable access to both the ctx and the global declarations. - pub(crate) fn with_mut_global_decls( - &mut self, - f: impl FnOnce(&mut Self, &mut Vector) -> R, - ) -> R { - let mut global_decls = std::mem::take(&mut self.translated.global_decls); - let ret = f(self, &mut global_decls); - self.translated.global_decls = global_decls; - ret - } /// Mutably iterate over the bodies. // FIXME: this does not set `with_def_id` to track error sources. That would require having a @@ -293,32 +249,6 @@ impl<'ctx> TransformCtx<'ctx> { }) }) } - - /// Mutably iterate over the global declarations without errors. - pub(crate) fn for_each_global_decl( - &mut self, - mut f: impl FnMut(&mut Self, &mut GlobalDecl, Result<&mut Body, Opaque>), - ) { - self.with_mut_bodies(|ctx, bodies| { - ctx.with_mut_global_decls(|ctx, decls| { - for decl in decls.iter_mut() { - let body = match decl.body { - Ok(id) => { - match bodies.get_mut(id) { - Some(body) => Ok(body), - // This body has errored, we skip the item. - None => continue, - } - } - Err(Opaque) => Err(Opaque), - }; - ctx.with_def_id(decl.def_id, decl.item_meta.is_local, |ctx| { - f(ctx, decl, body); - }) - } - }) - }) - } } impl<'a> IntoFormatter for &'a TransformCtx<'_> { diff --git a/charon/src/transform/insert_assign_return_unit.rs b/charon/src/transform/insert_assign_return_unit.rs index 1173dbec..3cd69f41 100644 --- a/charon/src/transform/insert_assign_return_unit.rs +++ b/charon/src/transform/insert_assign_return_unit.rs @@ -40,18 +40,6 @@ impl LlbcPass for Transform { } } } - fn transform_global( - &self, - ctx: &mut TransformCtx, - decl: &mut GlobalDecl, - body: Result<&mut ExprBody, Opaque>, - ) { - if decl.ty.is_unit() { - if let Ok(body) = body { - self.transform_body(ctx, body) - } - } - } fn transform_body(&self, _ctx: &mut TransformCtx<'_>, body: &mut ExprBody) { body.body.transform(&mut transform_st); } diff --git a/charon/src/transform/reorder_decls.rs b/charon/src/transform/reorder_decls.rs index b930a5b7..5212df6a 100644 --- a/charon/src/transform/reorder_decls.rs +++ b/charon/src/transform/reorder_decls.rs @@ -53,12 +53,14 @@ impl GDeclarationGroup { Rec(ids) => ids.as_slice(), } } + pub fn get_any_trans_ids(&self) -> Vec where Id: Into, { self.get_ids().iter().copied().map(|id| id.into()).collect() } + fn make_group(is_rec: bool, gr: impl Iterator) -> Self where Id: TryFrom, @@ -72,9 +74,31 @@ impl GDeclarationGroup { GDeclarationGroup::NonRec(gr[0]) } } + + fn to_mixed(&self) -> GDeclarationGroup + where + Id: Into, + { + match self { + GDeclarationGroup::NonRec(x) => GDeclarationGroup::NonRec((*x).into()), + GDeclarationGroup::Rec(_) => GDeclarationGroup::Rec(self.get_any_trans_ids()), + } + } } impl DeclarationGroup { + pub fn to_mixed_group(&self) -> GDeclarationGroup { + use DeclarationGroup::*; + match self { + Type(gr) => gr.to_mixed(), + Fun(gr) => gr.to_mixed(), + Global(gr) => gr.to_mixed(), + TraitDecl(gr) => gr.to_mixed(), + TraitImpl(gr) => gr.to_mixed(), + Mixed(gr) => gr.clone(), + } + } + pub fn get_ids(&self) -> Vec { use DeclarationGroup::*; match self { @@ -177,7 +201,8 @@ pub struct Deps<'tcx, 'ctx> { // // ^^^^^^^^^^^^^^^ // // refers to the trait impl // ``` - impl_trait_id: Option, + parent_trait_impl: Option, + parent_trait_decl: Option, } impl<'tcx, 'ctx> Deps<'tcx, 'ctx> { @@ -187,30 +212,34 @@ impl<'tcx, 'ctx> Deps<'tcx, 'ctx> { dgraph: DiGraphMap::new(), graph: LinkedHashMap::new(), current_id: None, - impl_trait_id: None, + parent_trait_impl: None, + parent_trait_decl: None, } } + fn set_impl_or_trait_id(&mut self, kind: &ItemKind) { + match kind { + ItemKind::Regular => {} + ItemKind::TraitDecl { trait_id, .. } => self.parent_trait_decl = Some(*trait_id), + ItemKind::TraitImpl { impl_id, .. } => self.parent_trait_impl = Some(*impl_id), + } + } fn set_current_id(&mut self, ctx: &TransformCtx, id: AnyTransId) { self.insert_node(id); self.current_id = Some(id); - // Add the id of the trait impl trait this item belongs to, if necessary + // Add the id of the impl/trait this item belongs to, if necessary use AnyTransId::*; match id { - TraitDecl(_) | TraitImpl(_) => (), - Type(_) | Global(_) => { - // TODO + TraitDecl(_) | TraitImpl(_) | Type(_) => (), + Global(id) => { + if let Some(decl) = ctx.translated.global_decls.get(id) { + self.set_impl_or_trait_id(&decl.kind); + } } Fun(id) => { - // Lookup the function declaration. - // - // The declaration may not be present if we encountered errors. if let Some(decl) = ctx.translated.fun_decls.get(id) { - if let ItemKind::TraitImpl { impl_id, .. } = &decl.kind { - // Register the trait decl id - self.impl_trait_id = Some(*impl_id) - } + self.set_impl_or_trait_id(&decl.kind); } } } @@ -218,7 +247,8 @@ impl<'tcx, 'ctx> Deps<'tcx, 'ctx> { fn unset_current_id(&mut self) { self.current_id = None; - self.impl_trait_id = None; + self.parent_trait_impl = None; + self.parent_trait_decl = None; } fn insert_node(&mut self, id: AnyTransId) { @@ -242,38 +272,41 @@ impl<'tcx, 'ctx> Deps<'tcx, 'ctx> { impl Deps<'_, '_> { fn enter_type_decl_id(&mut self, id: &TypeDeclId) { - let id = AnyTransId::Type(*id); - self.insert_edge(id); + self.insert_edge((*id).into()); } fn enter_global_decl_id(&mut self, id: &GlobalDeclId) { - let id = AnyTransId::Global(*id); - self.insert_edge(id); + self.insert_edge((*id).into()); } 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 - // method impls and trait impls in the presence of associated types... - if let Some(impl_id) = &self.impl_trait_id + // TODO: this is not very satisfying but this is the only way we have of preventing + // mutually recursive groups between method impls and trait impls in the presence of + // associated types... + if let Some(impl_id) = &self.parent_trait_impl && impl_id == id { - // Ignore - } else { - let id = AnyTransId::TraitImpl(*id); - self.insert_edge(id); + return; } + self.insert_edge((*id).into()); } fn enter_trait_decl_id(&mut self, id: &TraitDeclId) { - let id = AnyTransId::TraitDecl(*id); - self.insert_edge(id); + // If the trait is the trait 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 methods and trait decls in the presence of associated + // types... + if let Some(trait_id) = &self.parent_trait_decl + && trait_id == id + { + return; + } + self.insert_edge((*id).into()); } fn enter_fun_decl_id(&mut self, id: &FunDeclId) { - let id = AnyTransId::Fun(*id); - self.insert_edge(id); + self.insert_edge((*id).into()); } fn enter_body_id(&mut self, id: &BodyId) { @@ -337,8 +370,7 @@ fn compute_declarations_graph<'tcx, 'ctx>(ctx: &'tcx TransformCtx<'ctx>) -> Deps d.body.drive(&mut graph); } AnyTransItem::Global(d) => { - // FIXME: shouldn't we visit the generics etc? - d.body.drive(&mut graph); + d.drive(&mut graph); } AnyTransItem::TraitDecl(d) => { let TraitDecl { diff --git a/charon/tests/cargo/build-script.out b/charon/tests/cargo/build-script.out index dfeee2d1..a5c1bcad 100644 --- a/charon/tests/cargo/build-script.out +++ b/charon/tests/cargo/build-script.out @@ -1,12 +1,15 @@ # Final LLBC before serialization: -global test_cargo_build_script::FOO { +fn test_cargo_build_script::FOO() -> u8 +{ let @0: u8; // return @0 := const (42 : u8) return } +global test_cargo_build_script::FOO: u8 = test_cargo_build_script::FOO() + fn test_cargo_build_script::main() { let @0: (); // return diff --git a/charon/tests/crate_data.rs b/charon/tests/crate_data.rs index 1ece998d..b1b6b8be 100644 --- a/charon/tests/crate_data.rs +++ b/charon/tests/crate_data.rs @@ -497,7 +497,7 @@ fn rename_attribute() -> anyhow::Result<()> { .attr_info .rename .as_deref(), - Some("getTest") + Some("Const_Test") ); assert_eq!( @@ -506,6 +506,15 @@ fn rename_attribute() -> anyhow::Result<()> { .attr_info .rename .as_deref(), + Some("getTest") + ); + + assert_eq!( + crate_data.fun_decls[3] + .item_meta + .attr_info + .rename + .as_deref(), Some("retTest") ); @@ -598,7 +607,9 @@ fn declaration_groups() -> anyhow::Result<()> { fn foo() { panic!() } - trait Foo {} + trait Foo { + const FOO: usize = 42; + } impl Foo for () {} "#, )?; @@ -606,11 +617,11 @@ fn declaration_groups() -> anyhow::Result<()> { // There are two function ids registered, but only one is nonempty. `functions.len() == 2` as // `len()` counts the empty slots too. let decl_groups = crate_data.ordered_decls.unwrap(); - assert_eq!(crate_data.fun_decls.iter().count(), 1); - assert_eq!(decl_groups.len(), 3); - assert!(decl_groups[0].as_fun().unwrap().is_non_rec()); - assert!(decl_groups[1].as_trait_decl().unwrap().is_non_rec()); - assert!(decl_groups[2].as_trait_impl().unwrap().is_non_rec()); + assert_eq!(crate_data.fun_decls.iter().count(), 2); + assert_eq!(decl_groups.len(), 5); + assert!(decl_groups + .iter() + .all(|group| group.to_mixed_group().is_non_rec())); Ok(()) } diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out index c113347a..effba6c5 100644 --- a/charon/tests/ui/arrays.out +++ b/charon/tests/ui/arrays.out @@ -1542,13 +1542,16 @@ fn test_crate::f3() -> u32 return } -global test_crate::SZ { +fn test_crate::SZ() -> usize +{ let @0: usize; // return @0 := const (32 : usize) return } +global test_crate::SZ: usize = test_crate::SZ() + fn test_crate::f5<'_0>(@1: &'_0 (Array)) -> u32 { let @0: u32; // return diff --git a/charon/tests/ui/assoc-const-with-generics.out b/charon/tests/ui/assoc-const-with-generics.out index 39b7ff29..2ac607db 100644 --- a/charon/tests/ui/assoc-const-with-generics.out +++ b/charon/tests/ui/assoc-const-with-generics.out @@ -10,52 +10,66 @@ struct test_crate::V x: Array, } -global test_crate::{test_crate::V[@TraitClause0]}::LEN - where - [@TraitClause0]: core::marker::Sized, - { +fn test_crate::{test_crate::V[@TraitClause0]}::LEN() -> usize +where + [@TraitClause0]: core::marker::Sized, +{ let @0: usize; // return @0 := const (const N : usize) return } +global test_crate::{test_crate::V[@TraitClause0]}::LEN: usize + where + [@TraitClause0]: core::marker::Sized, + = test_crate::{test_crate::V[@TraitClause0]}::LEN() + trait test_crate::HasLen { const LEN : usize } -global test_crate::{impl test_crate::HasLen for Array<(), const N : usize>}#1::LEN { +fn test_crate::{impl test_crate::HasLen for Array<(), const N : usize>}#1::LEN() -> usize +{ let @0: usize; // return @0 := const (const N : usize) return } +global test_crate::{impl test_crate::HasLen for Array<(), const N : usize>}#1::LEN: usize = test_crate::{impl test_crate::HasLen for Array<(), const N : usize>}#1::LEN() + impl test_crate::{impl test_crate::HasLen for Array<(), const N : usize>}#1 : test_crate::HasLen> { const LEN = test_crate::{impl test_crate::HasLen for Array<(), const N : usize>}#1::LEN } -global test_crate::{impl test_crate::HasLen for Array}#2::LEN { +fn test_crate::{impl test_crate::HasLen for Array}#2::LEN() -> usize +{ let @0: usize; // return @0 := const (const N : usize) + const (1 : usize) return } +global test_crate::{impl test_crate::HasLen for Array}#2::LEN: usize = test_crate::{impl test_crate::HasLen for Array}#2::LEN() + impl test_crate::{impl test_crate::HasLen for Array}#2 : test_crate::HasLen> { const LEN = test_crate::{impl test_crate::HasLen for Array}#2::LEN } -global test_crate::HasDefaultLen::LEN { +fn test_crate::HasDefaultLen::LEN() -> usize +{ let @0: usize; // return @0 := const (const M : usize) return } +global test_crate::HasDefaultLen::LEN: usize = test_crate::HasDefaultLen::LEN() + trait test_crate::HasDefaultLen { const LEN : usize @@ -66,12 +80,8 @@ impl test_crate::{impl test_crate::HasDefaultLen, const N : usize> } -impl test_crate::{impl test_crate::HasDefaultLen for Array}#4 : test_crate::HasDefaultLen, const N : usize> +fn test_crate::{impl test_crate::HasDefaultLen for Array}#4::LEN() -> usize { - const LEN = test_crate::{impl test_crate::HasDefaultLen for Array}#4::LEN -} - -global test_crate::{impl test_crate::HasDefaultLen for Array}#4::LEN { let @0: usize; // return let @1: bool; // anonymous local @@ -86,5 +96,12 @@ global test_crate::{impl test_crate::HasDefaultLen for Array for Array}#4::LEN: usize = test_crate::{impl test_crate::HasDefaultLen for Array}#4::LEN() + +impl test_crate::{impl test_crate::HasDefaultLen for Array}#4 : test_crate::HasDefaultLen, const N : usize> +{ + const LEN = test_crate::{impl test_crate::HasDefaultLen for Array}#4::LEN +} + diff --git a/charon/tests/ui/closures.out b/charon/tests/ui/closures.out index 22200a7b..8227c7b1 100644 --- a/charon/tests/ui/closures.out +++ b/charon/tests/ui/closures.out @@ -757,7 +757,8 @@ fn test_crate::BLAH::closure<'_0>(@1: &'_0 (()), @2: ()) -> u32 return } -global test_crate::BLAH { +fn test_crate::BLAH() -> u32 +{ let @0: u32; // return let clo@1: fn() -> u32; // local let @2: &'_ (fn() -> u32); // anonymous local @@ -774,6 +775,8 @@ global test_crate::BLAH { return } +global test_crate::BLAH: u32 = test_crate::BLAH() + fn core::clone::Clone::clone_from<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Self)) fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> Self::parent_clause0::Output diff --git a/charon/tests/ui/comments.out b/charon/tests/ui/comments.out index bd992977..2b71af13 100644 --- a/charon/tests/ui/comments.out +++ b/charon/tests/ui/comments.out @@ -363,13 +363,16 @@ fn test_crate::foo() return } -global test_crate::CONSTANT { +fn test_crate::CONSTANT() -> u32 +{ let @0: u32; // return @0 := const (42 : u32) return } +global test_crate::CONSTANT: u32 = test_crate::CONSTANT() + fn test_crate::thing() { let @0: (); // return diff --git a/charon/tests/ui/constants.out b/charon/tests/ui/constants.out index 2c744730..9c265ada 100644 --- a/charon/tests/ui/constants.out +++ b/charon/tests/ui/constants.out @@ -1,15 +1,21 @@ # Final LLBC before serialization: -global test_crate::X0 { +fn test_crate::X0() -> u32 +{ let @0: u32; // return @0 := const (0 : u32) return } -global core::num::{u32}#8::MAX +global test_crate::X0: u32 = test_crate::X0() + +fn core::num::{u32}#8::MAX() -> u32 -global test_crate::X1 { +global core::num::{u32}#8::MAX: u32 = core::num::{u32}#8::MAX() + +fn test_crate::X1() -> u32 +{ let @0: u32; // return let @1: u32; // anonymous local @@ -18,7 +24,10 @@ global test_crate::X1 { return } -global test_crate::X2 { +global test_crate::X1: u32 = test_crate::X1() + +fn test_crate::X2() -> u32 +{ let @0: u32; // return let x@1: u32; // local @@ -29,6 +38,8 @@ global test_crate::X2 { return } +global test_crate::X2: u32 = test_crate::X2() + fn test_crate::incr(@1: u32) -> u32 { let @0: u32; // return @@ -41,13 +52,16 @@ fn test_crate::incr(@1: u32) -> u32 return } -global test_crate::X3 { +fn test_crate::X3() -> u32 +{ let @0: u32; // return @0 := test_crate::incr(const (32 : u32)) return } +global test_crate::X3: u32 = test_crate::X3() + fn test_crate::mk_pair0(@1: u32, @2: u32) -> (u32, u32) { let @0: (u32, u32); // return @@ -92,34 +106,46 @@ fn test_crate::mk_pair1(@1: u32, @2: u32) -> test_crate::Pair[core::ma return } -global test_crate::P0 { +fn test_crate::P0() -> (u32, u32) +{ let @0: (u32, u32); // return @0 := test_crate::mk_pair0(const (0 : u32), const (1 : u32)) return } -global test_crate::P1 { +global test_crate::P0: (u32, u32) = test_crate::P0() + +fn test_crate::P1() -> test_crate::Pair[core::marker::Sized, core::marker::Sized] +{ let @0: test_crate::Pair[core::marker::Sized, core::marker::Sized]; // return @0 := test_crate::mk_pair1(const (0 : u32), const (1 : u32)) return } -global test_crate::P2 { +global test_crate::P1: test_crate::Pair[core::marker::Sized, core::marker::Sized] = test_crate::P1() + +fn test_crate::P2() -> (u32, u32) +{ let @0: (u32, u32); // return @0 := (const (0 : u32), const (1 : u32)) return } -global test_crate::P3 { +global test_crate::P2: (u32, u32) = test_crate::P2() + +fn test_crate::P3() -> test_crate::Pair[core::marker::Sized, core::marker::Sized] +{ let @0: test_crate::Pair[core::marker::Sized, core::marker::Sized]; // return @0 := test_crate::Pair { x: const (0 : u32), y: const (1 : u32) } return } +global test_crate::P3: test_crate::Pair[core::marker::Sized, core::marker::Sized] = test_crate::P3() + struct test_crate::Wrap where [@TraitClause0]: core::marker::Sized, @@ -145,13 +171,16 @@ where return } -global test_crate::Y { +fn test_crate::Y() -> test_crate::Wrap[core::marker::Sized] +{ let @0: test_crate::Wrap[core::marker::Sized]; // return @0 := test_crate::{test_crate::Wrap[@TraitClause0]}::new[core::marker::Sized](const (2 : i32)) return } +global test_crate::Y: test_crate::Wrap[core::marker::Sized] = test_crate::Y() + fn test_crate::unwrap_y() -> i32 { let @0: i32; // return @@ -165,20 +194,26 @@ fn test_crate::unwrap_y() -> i32 return } -global test_crate::YVAL { +fn test_crate::YVAL() -> i32 +{ let @0: i32; // return @0 := test_crate::unwrap_y() return } -global test_crate::get_z1::Z1 { +global test_crate::YVAL: i32 = test_crate::YVAL() + +fn test_crate::get_z1::Z1() -> i32 +{ let @0: i32; // return @0 := const (3 : i32) return } +global test_crate::get_z1::Z1: i32 = test_crate::get_z1::Z1() + fn test_crate::get_z1() -> i32 { let @0: i32; // return @@ -205,14 +240,18 @@ fn test_crate::add(@1: i32, @2: i32) -> i32 return } -global test_crate::Q1 { +fn test_crate::Q1() -> i32 +{ let @0: i32; // return @0 := const (5 : i32) return } -global test_crate::Q2 { +global test_crate::Q1: i32 = test_crate::Q1() + +fn test_crate::Q2() -> i32 +{ let @0: i32; // return let @1: i32; // anonymous local @@ -221,7 +260,10 @@ global test_crate::Q2 { return } -global test_crate::Q3 { +global test_crate::Q2: i32 = test_crate::Q2() + +fn test_crate::Q3() -> i32 +{ let @0: i32; // return let @1: i32; // anonymous local @@ -230,6 +272,8 @@ global test_crate::Q3 { return } +global test_crate::Q3: i32 = test_crate::Q3() + fn test_crate::get_z2() -> i32 { let @0: i32; // return @@ -248,14 +292,18 @@ fn test_crate::get_z2() -> i32 return } -global test_crate::S1 { +fn test_crate::S1() -> u32 +{ let @0: u32; // return @0 := const (6 : u32) return } -global test_crate::S2 { +global test_crate::S1: u32 = test_crate::S1() + +fn test_crate::S2() -> u32 +{ let @0: u32; // return let @1: u32; // anonymous local let @2: &'_ (u32); // anonymous local @@ -270,7 +318,10 @@ global test_crate::S2 { return } -global test_crate::S3 { +global test_crate::S2: u32 = test_crate::S2() + +fn test_crate::S3() -> test_crate::Pair[core::marker::Sized, core::marker::Sized] +{ let @0: test_crate::Pair[core::marker::Sized, core::marker::Sized]; // return let @1: test_crate::Pair[core::marker::Sized, core::marker::Sized]; // anonymous local @@ -279,13 +330,18 @@ global test_crate::S3 { return } -global test_crate::S4 { +global test_crate::S3: test_crate::Pair[core::marker::Sized, core::marker::Sized] = test_crate::S3() + +fn test_crate::S4() -> test_crate::Pair[core::marker::Sized, core::marker::Sized] +{ let @0: test_crate::Pair[core::marker::Sized, core::marker::Sized]; // return @0 := test_crate::mk_pair1(const (7 : u32), const (8 : u32)) return } +global test_crate::S4: test_crate::Pair[core::marker::Sized, core::marker::Sized] = test_crate::S4() + struct test_crate::V where [@TraitClause0]: core::marker::Sized, @@ -294,16 +350,21 @@ struct test_crate::V x: Array, } -global test_crate::{test_crate::V[@TraitClause0]}#1::LEN - where - [@TraitClause0]: core::marker::Sized, - { +fn test_crate::{test_crate::V[@TraitClause0]}#1::LEN() -> usize +where + [@TraitClause0]: core::marker::Sized, +{ let @0: usize; // return @0 := const (const N : usize) return } +global test_crate::{test_crate::V[@TraitClause0]}#1::LEN: usize + where + [@TraitClause0]: core::marker::Sized, + = test_crate::{test_crate::V[@TraitClause0]}#1::LEN() + fn test_crate::use_v() -> usize where [@TraitClause0]: core::marker::Sized, @@ -316,7 +377,10 @@ where return } -global test_crate::REC1 { +global test_crate::REC1: usize = test_crate::REC1() + +fn test_crate::REC1() -> usize +{ let @0: usize; // return let @1: bool; // anonymous local let @2: usize; // anonymous local @@ -333,7 +397,10 @@ global test_crate::REC1 { return } -global test_crate::REC2 { +global test_crate::REC2: usize = test_crate::REC2() + +fn test_crate::REC2() -> usize +{ let @0: usize; // return let @1: bool; // anonymous local let @2: usize; // anonymous local diff --git a/charon/tests/ui/foreign-constant.out b/charon/tests/ui/foreign-constant.out index 2c592323..598984c3 100644 --- a/charon/tests/ui/foreign-constant.out +++ b/charon/tests/ui/foreign-constant.out @@ -1,6 +1,8 @@ # Final LLBC before serialization: -global foreign_constant_aux::CONSTANT +fn foreign_constant_aux::CONSTANT() -> u8 + +global foreign_constant_aux::CONSTANT: u8 = foreign_constant_aux::CONSTANT() fn test_crate::foo() -> u8 { diff --git a/charon/tests/ui/issue-114-opaque-bodies.out b/charon/tests/ui/issue-114-opaque-bodies.out index a7e325fa..a47d3356 100644 --- a/charon/tests/ui/issue-114-opaque-bodies.out +++ b/charon/tests/ui/issue-114-opaque-bodies.out @@ -200,13 +200,16 @@ fn test_crate::vec(@1: alloc::vec::Vec[core::marker:: return } -global core::num::{usize}#11::MAX { +fn core::num::{usize}#11::MAX() -> usize +{ let @0: usize; // return @0 := ~(const (0 : usize)) return } +global core::num::{usize}#11::MAX: usize = core::num::{usize}#11::MAX() + fn test_crate::max() -> usize { let @0: usize; // return diff --git a/charon/tests/ui/issue-73-extern.out b/charon/tests/ui/issue-73-extern.out index e92407ea..8be29fbf 100644 --- a/charon/tests/ui/issue-73-extern.out +++ b/charon/tests/ui/issue-73-extern.out @@ -2,7 +2,9 @@ unsafe fn test_crate::foo(@1: i32) -global test_crate::CONST +fn test_crate::CONST() -> u8 + +global test_crate::CONST: u8 = test_crate::CONST() opaque type test_crate::Type diff --git a/charon/tests/ui/opaque_attribute.out b/charon/tests/ui/opaque_attribute.out index 488949af..796140fe 100644 --- a/charon/tests/ui/opaque_attribute.out +++ b/charon/tests/ui/opaque_attribute.out @@ -36,7 +36,9 @@ where opaque type test_crate::Test -global test_crate::SIX_SIX_SIX +fn test_crate::SIX_SIX_SIX() -> u32 + +global test_crate::SIX_SIX_SIX: u32 = test_crate::SIX_SIX_SIX() opaque type test_crate::Test2 diff --git a/charon/tests/ui/remove-dynamic-checks.out b/charon/tests/ui/remove-dynamic-checks.out index 799887f1..4688ff6e 100644 --- a/charon/tests/ui/remove-dynamic-checks.out +++ b/charon/tests/ui/remove-dynamic-checks.out @@ -371,70 +371,98 @@ fn test_crate::shr(@1: u32, @2: u32) -> u32 return } -global test_crate::_ { +fn test_crate::_() -> isize +{ let @0: isize; // return @0 := const (1 : isize) + const (1 : isize) return } -global test_crate::_#1 { +global test_crate::_: isize = test_crate::_() + +fn test_crate::_#1() -> isize +{ let @0: isize; // return @0 := const (1 : isize) - const (1 : isize) return } -global test_crate::_#2 { +global test_crate::_#1: isize = test_crate::_#1() + +fn test_crate::_#2() -> isize +{ let @0: isize; // return @0 := const (-1 : isize) return } -global test_crate::_#3 { +global test_crate::_#2: isize = test_crate::_#2() + +fn test_crate::_#3() -> isize +{ let @0: isize; // return @0 := const (2 : isize) * const (2 : isize) return } -global test_crate::_#4 { +global test_crate::_#3: isize = test_crate::_#3() + +fn test_crate::_#4() -> isize +{ let @0: isize; // return @0 := const (2 : isize) >> const (2 : i32) return } -global test_crate::_#5 { +global test_crate::_#4: isize = test_crate::_#4() + +fn test_crate::_#5() -> isize +{ let @0: isize; // return @0 := const (2 : isize) << const (2 : i32) return } -global test_crate::_#6 { +global test_crate::_#5: isize = test_crate::_#5() + +fn test_crate::_#6() -> isize +{ let @0: isize; // return @0 := const (2 : isize) % const (2 : isize) return } -global test_crate::_#7 { +global test_crate::_#6: isize = test_crate::_#6() + +fn test_crate::_#7() -> isize +{ let @0: isize; // return @0 := const (2 : isize) / const (2 : isize) return } -global test_crate::FOO { +global test_crate::_#7: isize = test_crate::_#7() + +fn test_crate::FOO() -> u32 +{ let @0: u32; // return @0 := const (10 : u32) return } -global test_crate::_#8 { +global test_crate::FOO: u32 = test_crate::FOO() + +fn test_crate::_#8() -> u32 +{ let @0: u32; // return let @1: u32; // anonymous local @@ -443,7 +471,10 @@ global test_crate::_#8 { return } -global test_crate::_#9 { +global test_crate::_#8: u32 = test_crate::_#8() + +fn test_crate::_#9() -> u32 +{ let @0: u32; // return let @1: u32; // anonymous local @@ -452,7 +483,10 @@ global test_crate::_#9 { return } -global test_crate::_#10 { +global test_crate::_#9: u32 = test_crate::_#9() + +fn test_crate::_#10() -> u32 +{ let @0: u32; // return let @1: u32; // anonymous local @@ -461,7 +495,10 @@ global test_crate::_#10 { return } -global test_crate::_#11 { +global test_crate::_#10: u32 = test_crate::_#10() + +fn test_crate::_#11() -> u32 +{ let @0: u32; // return let @1: u32; // anonymous local @@ -470,7 +507,10 @@ global test_crate::_#11 { return } -global test_crate::_#12 { +global test_crate::_#11: u32 = test_crate::_#11() + +fn test_crate::_#12() -> u32 +{ let @0: u32; // return let @1: u32; // anonymous local @@ -479,7 +519,10 @@ global test_crate::_#12 { return } -global test_crate::_#13 { +global test_crate::_#12: u32 = test_crate::_#12() + +fn test_crate::_#13() -> u32 +{ let @0: u32; // return let @1: u32; // anonymous local @@ -488,7 +531,10 @@ global test_crate::_#13 { return } -global test_crate::_#14 { +global test_crate::_#13: u32 = test_crate::_#13() + +fn test_crate::_#14() -> u32 +{ let @0: u32; // return let @1: u32; // anonymous local @@ -497,13 +543,18 @@ global test_crate::_#14 { return } -global test_crate::div_signed_with_constant::FOO { +global test_crate::_#14: u32 = test_crate::_#14() + +fn test_crate::div_signed_with_constant::FOO() -> i32 +{ let @0: i32; // return @0 := const (42 : i32) return } +global test_crate::div_signed_with_constant::FOO: i32 = test_crate::div_signed_with_constant::FOO() + fn test_crate::div_signed_with_constant() -> i32 { let @0: i32; // return diff --git a/charon/tests/ui/rename_attribute.out b/charon/tests/ui/rename_attribute.out index eedbd54b..5842f070 100644 --- a/charon/tests/ui/rename_attribute.out +++ b/charon/tests/ui/rename_attribute.out @@ -72,7 +72,8 @@ struct test_crate::Foo = field1: u32, } -global test_crate::C { +fn test_crate::C() -> u32 +{ let @0: u32; // return let @1: u32; // anonymous local @@ -82,6 +83,8 @@ global test_crate::C { return } +global test_crate::C: u32 = test_crate::C() + type test_crate::Test2 = u32 diff --git a/charon/tests/ui/rvalues.out b/charon/tests/ui/rvalues.out index a32ace39..955aff1f 100644 --- a/charon/tests/ui/rvalues.out +++ b/charon/tests/ui/rvalues.out @@ -30,9 +30,13 @@ fn test_crate::addr_of() return } -global core::f64::{f64}::MIN +fn core::f64::{f64}::MIN() -> f64 -global core::f32::{f32}::MAX +global core::f64::{f64}::MIN: f64 = core::f64::{f64}::MIN() + +fn core::f32::{f32}::MAX() -> f32 + +global core::f32::{f32}::MAX: f32 = core::f32::{f32}::MAX() fn test_crate::literal_casts() { @@ -244,7 +248,8 @@ fn test_crate::boxes() return } -global test_crate::STEAL { +fn test_crate::STEAL() -> Array<(), 1 : usize> +{ let @0: Array<(), 1 : usize>; // return let @1: (); // anonymous local @@ -254,6 +259,8 @@ global test_crate::STEAL { return } +global test_crate::STEAL: Array<(), 1 : usize> = test_crate::STEAL() + fn test_crate::transmute(@1: Array) -> u64 { let @0: u64; // return @@ -267,7 +274,8 @@ fn test_crate::transmute(@1: Array) -> u64 return } -global test_crate::STEAL2 { +fn test_crate::STEAL2() -> Array<(), 13 : usize> +{ let @0: Array<(), 13 : usize>; // return let @1: (); // anonymous local @@ -277,6 +285,8 @@ global test_crate::STEAL2 { return } +global test_crate::STEAL2: Array<(), 13 : usize> = test_crate::STEAL2() + fn core::mem::size_of() -> usize where [@TraitClause0]: core::marker::Sized, diff --git a/charon/tests/ui/statics.out b/charon/tests/ui/statics.out index 04a33631..69b368de 100644 --- a/charon/tests/ui/statics.out +++ b/charon/tests/ui/statics.out @@ -1,12 +1,15 @@ # Final LLBC before serialization: -global test_crate::constant::CONST { +fn test_crate::constant::CONST() -> usize +{ let @0: usize; // return @0 := const (0 : usize) return } +global test_crate::constant::CONST: usize = test_crate::constant::CONST() + fn test_crate::constant() { let @0: (); // return @@ -42,13 +45,16 @@ fn test_crate::constant() return } -global test_crate::shared_static::SHARED_STATIC { +fn test_crate::shared_static::SHARED_STATIC() -> usize +{ let @0: usize; // return @0 := const (0 : usize) return } +global test_crate::shared_static::SHARED_STATIC: usize = test_crate::shared_static::SHARED_STATIC() + fn test_crate::shared_static() { let @0: (); // return @@ -87,13 +93,16 @@ fn test_crate::shared_static() return } -global test_crate::mut_static::MUT_STATIC { +fn test_crate::mut_static::MUT_STATIC() -> usize +{ let @0: usize; // return @0 := const (0 : usize) return } +global test_crate::mut_static::MUT_STATIC: usize = test_crate::mut_static::MUT_STATIC() + fn test_crate::mut_static() { let @0: (); // return @@ -152,13 +161,16 @@ fn test_crate::mut_static() struct test_crate::non_copy_static::Foo = {} -global test_crate::non_copy_static::FOO { +fn test_crate::non_copy_static::FOO() -> test_crate::non_copy_static::Foo +{ let @0: test_crate::non_copy_static::Foo; // return @0 := test_crate::non_copy_static::Foo { } return } +global test_crate::non_copy_static::FOO: test_crate::non_copy_static::Foo = test_crate::non_copy_static::FOO() + fn test_crate::non_copy_static::{test_crate::non_copy_static::Foo}::method<'_0>(@1: &'_0 (test_crate::non_copy_static::Foo)) { let @0: (); // return diff --git a/charon/tests/ui/stealing.out b/charon/tests/ui/stealing.out index d6c4f170..1a0ac118 100644 --- a/charon/tests/ui/stealing.out +++ b/charon/tests/ui/stealing.out @@ -1,6 +1,7 @@ # Final LLBC before serialization: -global test_crate::SLICE { +fn test_crate::SLICE() -> Array<(), 4 : usize> +{ let @0: Array<(), 4 : usize>; // return let @1: (); // anonymous local @@ -10,6 +11,8 @@ global test_crate::SLICE { return } +global test_crate::SLICE: Array<(), 4 : usize> = test_crate::SLICE() + fn test_crate::four() -> usize { let @0: usize; // return @@ -18,7 +21,8 @@ fn test_crate::four() -> usize return } -global test_crate::BAR { +fn test_crate::BAR() -> Array<(), 42 : usize> +{ let @0: Array<(), 42 : usize>; // return let @1: (); // anonymous local @@ -28,12 +32,17 @@ global test_crate::BAR { return } -global test_crate::FOO { +global test_crate::BAR: Array<(), 42 : usize> = test_crate::BAR() + +fn test_crate::FOO() -> usize +{ let @0: usize; // return @0 := const (42 : usize) return } +global test_crate::FOO: usize = test_crate::FOO() + diff --git a/charon/tests/ui/string-literal.out b/charon/tests/ui/string-literal.out index befc10a3..4d473177 100644 --- a/charon/tests/ui/string-literal.out +++ b/charon/tests/ui/string-literal.out @@ -1,13 +1,17 @@ # Final LLBC before serialization: -global test_crate::FOO { +fn test_crate::FOO() -> &'static (Str) +{ let @0: &'_ (Str); // return @0 := const ("hello") return } -global test_crate::BAR { +global test_crate::FOO: &'static (Str) = test_crate::FOO() + +fn test_crate::BAR() -> &'static (Slice) +{ let @0: &'_ (Slice); // return let @1: &'_ (Array); // anonymous local let @2: &'_ (Array); // anonymous local @@ -24,6 +28,8 @@ global test_crate::BAR { return } +global test_crate::BAR: &'static (Slice) = test_crate::BAR() + opaque type alloc::string::String trait alloc::string::ToString diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index c2e5ae85..08546ac8 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -493,13 +493,16 @@ where fn to_type = test_crate::{impl test_crate::ToType for test_crate::BoolWrapper}#7::to_type } -global test_crate::WithConstTy::LEN2 { +fn test_crate::WithConstTy::LEN2() -> usize +{ let @0: usize; // return @0 := const (32 : usize) return } +global test_crate::WithConstTy::LEN2: usize = test_crate::WithConstTy::LEN2() + trait test_crate::WithConstTy { parent_clause0 : [@TraitClause0]: core::marker::Sized @@ -512,13 +515,16 @@ trait test_crate::WithConstTy fn f : test_crate::WithConstTy::f } -global test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::LEN1 { +fn test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::LEN1() -> usize +{ let @0: usize; // return @0 := const (12 : usize) return } +global test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::LEN1: usize = test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::LEN1() + fn test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::f<'_0, '_1>(@1: &'_0 mut (test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::W), @2: &'_1 (Array)) { let @0: (); // return @@ -827,16 +833,21 @@ trait test_crate::Trait const LEN : usize } -global test_crate::{impl test_crate::Trait for Array}#14::LEN - where - [@TraitClause0]: core::marker::Sized, - { +fn test_crate::{impl test_crate::Trait for Array}#14::LEN() -> usize +where + [@TraitClause0]: core::marker::Sized, +{ let @0: usize; // return @0 := const (const N : usize) return } +global test_crate::{impl test_crate::Trait for Array}#14::LEN: usize + where + [@TraitClause0]: core::marker::Sized, + = test_crate::{impl test_crate::Trait for Array}#14::LEN() + impl test_crate::{impl test_crate::Trait for Array}#14 : test_crate::Trait> where [@TraitClause0]: core::marker::Sized, @@ -844,17 +855,23 @@ where const LEN = test_crate::{impl test_crate::Trait for Array}#14::LEN[@TraitClause0] } -global test_crate::{impl test_crate::Trait for test_crate::Wrapper[@TraitClause0]}#15::LEN - where - [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: test_crate::Trait, - { +fn test_crate::{impl test_crate::Trait for test_crate::Wrapper[@TraitClause0]}#15::LEN() -> usize +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: test_crate::Trait, +{ let @0: usize; // return @0 := const (0 : usize) return } +global test_crate::{impl test_crate::Trait for test_crate::Wrapper[@TraitClause0]}#15::LEN: usize + where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: test_crate::Trait, + = test_crate::{impl test_crate::Trait for test_crate::Wrapper[@TraitClause0]}#15::LEN() + impl test_crate::{impl test_crate::Trait for test_crate::Wrapper[@TraitClause0]}#15 : test_crate::Trait[@TraitClause0]> where [@TraitClause0]: core::marker::Sized, @@ -893,18 +910,25 @@ enum core::result::Result | Err(E) -global test_crate::{test_crate::Foo[@TraitClause0, @TraitClause1]}#16::FOO - where - [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: test_crate::Trait, - { +fn test_crate::{test_crate::Foo[@TraitClause0, @TraitClause1]}#16::FOO() -> core::result::Result[@TraitClause0, core::marker::Sized] +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Sized, + [@TraitClause2]: test_crate::Trait, +{ let @0: core::result::Result[@TraitClause0, core::marker::Sized]; // return @0 := core::result::Result::Err { 0: const (0 : i32) } return } +global test_crate::{test_crate::Foo[@TraitClause0, @TraitClause1]}#16::FOO: core::result::Result[@TraitClause0, core::marker::Sized] + where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Sized, + [@TraitClause2]: test_crate::Trait, + = test_crate::{test_crate::Foo[@TraitClause0, @TraitClause1]}#16::FOO() + fn test_crate::use_foo1() -> core::result::Result[@TraitClause0, core::marker::Sized] where [@TraitClause0]: core::marker::Sized, diff --git a/charon/tests/ui/unsafe.out b/charon/tests/ui/unsafe.out index 6edaa16d..a4b22e85 100644 --- a/charon/tests/ui/unsafe.out +++ b/charon/tests/ui/unsafe.out @@ -55,13 +55,16 @@ trait test_crate::Trait impl test_crate::{impl test_crate::Trait for ()} : test_crate::Trait<()> -global test_crate::COUNTER { +fn test_crate::COUNTER() -> usize +{ let @0: usize; // return @0 := const (0 : usize) return } +global test_crate::COUNTER: usize = test_crate::COUNTER() + fn test_crate::access_mutable_static() { let @0: (); // return