diff options
| -rw-r--r-- | src/TypesAnalysis.ml | 224 | ||||
| -rw-r--r-- | src/main.ml | 1 |
2 files changed, 225 insertions, 0 deletions
diff --git a/src/TypesAnalysis.ml b/src/TypesAnalysis.ml new file mode 100644 index 00000000..c8f16449 --- /dev/null +++ b/src/TypesAnalysis.ml @@ -0,0 +1,224 @@ +open Types +open Utils +open TypesUtils +open Modules + +type subtype_info = { + under_borrow : bool; (** Are we inside a borrow? *) + under_nested_borrows : bool; (** Are we inside nested borrows? *) +} + +type type_param_info = subtype_info +(** See [type_def_info] *) + +type expl_info = subtype_info + +type 'p g_type_info = { + contains_static : bool; + (** Does the type (transitively) contains a static borrow? *) + contains_borrow : bool; + (** Does the type (transitively) contains a borrow? *) + contains_nested_borrows : bool; + (** Does the type (transitively) contains nested borrows? *) + param_infos : 'p; (** Gives information about the type parameters *) +} +(** Generic definition *) + +type type_def_info = type_param_info list g_type_info +(** Information about a type definition. *) + +type ty_info = unit g_type_info +(** Information about a type. *) + +type partial_type_info = type_param_info list option g_type_info +(** Helper definition. + + Allows us to factorize code: [analyze_full_ty] is used both to analyze + type definitions and types. *) + +let initialize_type_def_info (def : type_def) : type_def_info = + let param_info = { under_borrow = false; under_nested_borrows = false } in + let param_infos = List.map (fun _ -> param_info) def.type_params in + { + contains_static = false; + contains_borrow = false; + contains_nested_borrows = false; + param_infos; + } + +let type_def_info_to_partial_type_info (info : type_def_info) : + partial_type_info = + { + contains_static = info.contains_static; + contains_borrow = info.contains_borrow; + contains_nested_borrows = info.contains_nested_borrows; + param_infos = Some info.param_infos; + } + +let partial_type_info_to_type_def_info (info : partial_type_info) : + type_def_info = + { + contains_static = info.contains_static; + contains_borrow = info.contains_borrow; + contains_nested_borrows = info.contains_nested_borrows; + param_infos = Option.get info.param_infos; + } + +type type_infos = type_def_info TypeDefId.Map.t + +let expl_info_init = { under_borrow = false; under_nested_borrows = false } + +let analyze_full_ty (updated : bool ref) (infos : type_infos) + (ty_info : partial_type_info) (ty : 'r gr_ty) : partial_type_info = + (* Small utility *) + let check_update_bool (original : bool) (nv : bool) : bool = + if nv && not original then ( + updated := true; + nv) + else original + in + (* The recursive function which explores the type *) + let rec analyze (expl_info : expl_info) (ty_info : partial_type_info) + (ty : 'r gr_ty) : partial_type_info = + match ty with + | Bool | Char | Never | Integer _ | Str -> ty_info + | TypeVar var_id -> ( + (* Update the information for the proper parameter, if necessary *) + match ty_info.param_infos with + | None -> ty_info + | Some param_infos -> + let param_info = TypeVarId.nth param_infos var_id in + (* Set `under_borrow` *) + let param_info = + { + param_info with + under_borrow = + check_update_bool param_info.under_borrow + expl_info.under_borrow; + } + in + (* Set `under_nested_borrows` *) + let param_info = + { + param_info with + under_nested_borrows = + check_update_bool param_info.under_nested_borrows + expl_info.under_nested_borrows; + } + in + let param_infos = + TypeVarId.update_nth param_infos var_id param_info + in + let param_infos = Some param_infos in + { ty_info with param_infos }) + | Array ty | Slice ty -> + (* Just dive in *) + analyze expl_info ty_info ty + | Ref (r, rty, _) -> + (* Update the exploration info *) + let expl_info = + { under_borrow = true; under_nested_borrows = expl_info.under_borrow } + in + (* Update the type info *) + (* Set `contains_static` *) + let ty_info = + { + ty_info with + contains_static = + check_update_bool ty_info.contains_static (r = Static); + } + in + (* Set `contains_borrow` *) + let ty_info = + { + ty_info with + contains_borrow = check_update_bool ty_info.contains_borrow true; + } + in + (* Set `contains_nested_borrows` *) + let ty_info = + { + ty_info with + contains_nested_borrows = + check_update_bool ty_info.contains_nested_borrows + expl_info.under_nested_borrows; + } + in + (* Continue exploring *) + analyze expl_info ty_info rty + | Adt ((Tuple | Assumed Box), _, tys) -> + (* Nothing to update: just explore the type parameters *) + List.fold_left + (fun ty_info ty -> analyze expl_info ty_info ty) + ty_info tys + | Adt (AdtId adt_id, _, tys) -> + (* Lookup the information for this type definition *) + let adt_info = TypeDefId.Map.find adt_id infos in + (* Update the *) + failwith "" + in + (* Explore *) + analyze expl_info_init ty_info ty + +let analyze_type_def (updated : bool ref) (infos : type_infos) (def : type_def) + : type_infos = + (* Retrieve all the types of all the fields of all the variants *) + let fields_tys : sty list = + match def.kind with + | Struct fields -> List.map (fun f -> f.field_ty) fields + | Enum variants -> + List.concat + (List.map (fun v -> List.map (fun f -> f.field_ty) v.fields) variants) + in + (* Explore the types and accumulate information *) + let type_def_info = TypeDefId.Map.find def.def_id infos in + let type_def_info = type_def_info_to_partial_type_info type_def_info in + let type_def_info = + List.fold_left + (fun type_def_info ty -> analyze_full_ty updated infos type_def_info ty) + type_def_info fields_tys + in + let type_def_info = partial_type_info_to_type_def_info type_def_info in + (* Update the information for the type definition we explored *) + let infos = TypeDefId.Map.add def.def_id type_def_info infos in + (* Return *) + infos + +let analyze_type_declaration_group (type_defs : type_def TypeDefId.Map.t) + (infos : type_infos) (decl : type_declaration_group) : type_infos = + (* Collect the identifiers used in the declaration group *) + let ids = match decl with NonRec id -> [ id ] | Rec ids -> ids in + let ids_set : TypeDefId.Set.t = + List.fold_left + (fun set id -> TypeDefId.Set.add id set) + TypeDefId.Set.empty ids + in + (* Retrieve the type definitions *) + let decl_defs = List.map (fun id -> TypeDefId.Map.find id type_defs) ids in + (* Initialize the type information for the current definitions *) + let infos = + List.fold_left + (fun infos def -> + TypeDefId.Map.add def.def_id (initialize_type_def_info def) infos) + infos decl_defs + in + (* Analyze the types - this function simply computes a fixed-point *) + let updated : bool ref = ref false in + let rec analyze (infos : type_infos) : type_infos = + let infos = + List.fold_left + (fun infos def -> analyze_type_def updated infos def) + infos decl_defs + in + if !updated then ( + updated := false; + analyze infos) + else infos + in + analyze infos + +let analyze_type_declarations (type_defs : type_def TypeDefId.Map.t) + (decls : type_declaration_group list) : type_infos = + List.fold_left + (fun infos decl -> analyze_type_declaration_group type_defs infos decl) + TypeDefId.Map.empty decls diff --git a/src/main.ml b/src/main.ml index fee51421..df9134e0 100644 --- a/src/main.ml +++ b/src/main.ml @@ -5,6 +5,7 @@ module T = Types module A = CfimAst module I = Interpreter module EL = Easy_logging.Logging +module TA = TypesAnalysis (* This is necessary to have a backtrace when raising exceptions - for some * reason, the -g option doesn't work. |