summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-18 19:49:24 +0100
committerSon Ho2022-01-18 19:49:24 +0100
commit2a8fbe0c19b11799f0d1854bc269fc788787bd0e (patch)
tree1fba872941b34a9c33144679b2dae4da8c4340a7 /src
parente21464bd6fbfd26bc8453995d180a519a10ba867 (diff)
Start working on TypesAnalysis
Diffstat (limited to 'src')
-rw-r--r--src/TypesAnalysis.ml224
-rw-r--r--src/main.ml1
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.