From e181cc32820f06a67c1fa6e6dfcb68d27468dc38 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 30 Nov 2021 18:53:58 +0100 Subject: Remove the vector type for the Id module --- src/CfimAst.ml | 8 +-- src/CfimOfJson.ml | 30 +++----- src/Contexts.ml | 6 +- src/Identifiers.ml | 65 ++--------------- src/Interpreter.ml | 208 ++++++++++++++++++----------------------------------- src/Modules.ml | 4 +- src/Print.ml | 66 +++++++---------- src/Substitute.ml | 17 ++--- src/Types.ml | 13 ++-- src/Values.ml | 8 +-- 10 files changed, 136 insertions(+), 289 deletions(-) (limited to 'src') diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 7be1a4bc..36977aad 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -14,10 +14,10 @@ type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id type assertion = { cond : operand; expected : bool } [@@deriving show] type fun_sig = { - region_params : region_var RegionVarId.vector; + region_params : region_var list; num_early_bound_regions : int; - type_params : type_var TypeVarId.vector; - inputs : rty VarId.vector; + type_params : type_var list; + inputs : rty list; output : rty; } [@@deriving show] @@ -75,7 +75,7 @@ type fun_def = { signature : fun_sig; divergent : bool; arg_count : int; - locals : var VarId.vector; + locals : var list; body : expression; } [@@deriving show] diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index bb0e9b69..4f6c2e73 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -138,7 +138,7 @@ let variant_of_json (js : json) : (T.variant, string) result = (match js with | `Assoc [ ("name", name); ("fields", fields) ] -> let* name = string_of_json name in - let* fields = T.FieldId.vector_of_json field_of_json fields in + let* fields = list_of_json field_of_json fields in Ok { T.variant_name = name; fields } | _ -> Error "") @@ -146,10 +146,10 @@ let type_def_kind_of_json (js : json) : (T.type_def_kind, string) result = combine_error_msgs js "type_def_kind_of_json" (match js with | `Assoc [ ("Struct", fields) ] -> - let* fields = T.FieldId.vector_of_json field_of_json fields in + let* fields = list_of_json field_of_json fields in Ok (T.Struct fields) | `Assoc [ ("Enum", variants) ] -> - let* variants = T.VariantId.vector_of_json variant_of_json variants in + let* variants = list_of_json variant_of_json variants in Ok (T.Enum variants) | _ -> Error "") @@ -166,12 +166,8 @@ let type_def_of_json (js : json) : (T.type_def, string) result = ] -> let* def_id = T.TypeDefId.id_of_json def_id in let* name = name_of_json name in - let* region_params = - T.RegionVarId.vector_of_json region_var_of_json region_params - in - let* type_params = - T.TypeVarId.vector_of_json type_var_of_json type_params - in + let* region_params = list_of_json region_var_of_json region_params in + let* type_params = list_of_json type_var_of_json type_params in let* kind = type_def_kind_of_json kind in Ok { T.def_id; name; region_params; type_params; kind } | _ -> Error "") @@ -445,14 +441,10 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result = ("inputs", inputs); ("output", output); ] -> - let* region_params = - T.RegionVarId.vector_of_json region_var_of_json region_params - in + let* region_params = list_of_json region_var_of_json region_params in let* num_early_bound_regions = int_of_json num_early_bound_regions in - let* type_params = - T.TypeVarId.vector_of_json type_var_of_json type_params - in - let* inputs = V.VarId.vector_of_json rty_of_json inputs in + let* type_params = list_of_json type_var_of_json type_params in + let* inputs = list_of_json rty_of_json inputs in let* output = rty_of_json output in Ok { @@ -572,7 +564,7 @@ let fun_def_of_json (js : json) : (A.fun_def, string) result = let* signature = fun_sig_of_json signature in let* divergent = bool_of_json divergent in let* arg_count = int_of_json arg_count in - let* locals = V.VarId.vector_of_json var_of_json locals in + let* locals = list_of_json var_of_json locals in let* body = expression_of_json body in Ok { A.def_id; name; signature; divergent; arg_count; locals; body } | _ -> Error "") @@ -604,7 +596,7 @@ let cfim_module_of_json (js : json) : (M.cfim_module, string) result = ("functions", functions); ] -> let* declarations = list_of_json declaration_of_json declarations in - let* types = T.TypeDefId.vector_of_json type_def_of_json types in - let* functions = A.FunDefId.vector_of_json fun_def_of_json functions in + let* types = list_of_json type_def_of_json types in + let* functions = list_of_json fun_def_of_json functions in Ok { M.declarations; types; functions } | _ -> Error "") diff --git a/src/Contexts.ml b/src/Contexts.ml index 8a498e2e..84c88e1c 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -18,9 +18,9 @@ type config = { mode : interpreter_mode; check_invariants : bool } [@@deriving show] type eval_ctx = { - type_context : type_def TypeDefId.vector; - fun_context : fun_def FunDefId.vector; - type_vars : type_var TypeVarId.vector; + type_context : type_def list; + fun_context : fun_def list; + type_vars : type_var list; env : env; symbolic_counter : SymbolicValueId.generator; borrow_counter : BorrowId.generator; diff --git a/src/Identifiers.ml b/src/Identifiers.ml index ebe0d898..3c07b511 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -10,16 +10,13 @@ module type Id = sig type generator (** Id generator - simply a counter *) - (* TODO: use list instead *) - type 'a vector - type set_t val zero : id val generator_zero : generator - (* TODO: this is stateful! *) + (* TODO: this is stateful! - but we may want to be able to duplicated contexts... *) val fresh : generator -> id * generator val to_string : id -> string @@ -36,42 +33,21 @@ module type Id = sig val of_int : id -> int - val pp_vector : - (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a vector -> unit - - val show_vector : (Format.formatter -> 'a -> unit) -> 'a vector -> string - - val empty_vector : 'a vector - - val vector_to_list : 'a vector -> 'a list - - val vector_of_list : 'a list -> 'a vector - - val length : 'a vector -> int + val nth : 'a list -> id -> 'a - val nth : 'a vector -> id -> 'a + val nth_opt : 'a list -> id -> 'a option - val nth_opt : 'a vector -> id -> 'a option - - val update_nth : 'a vector -> id -> 'a -> 'a vector - (** Update the nth element of the vector. + val update_nth : 'a list -> id -> 'a -> 'a list + (** Update the nth element of the list. Raises [Invalid_argument] if the identifier is out of range. *) - val iter : ('a -> unit) -> 'a vector -> unit - - val map : ('a -> 'b) -> 'a vector -> 'b vector - - val mapi : (id -> 'a -> 'b) -> 'a vector -> 'b vector + val mapi : (id -> 'a -> 'b) -> 'a list -> 'b list - val mapi_from1 : (id -> 'a -> 'b) -> 'a vector -> 'b vector + val mapi_from1 : (id -> 'a -> 'b) -> 'a list -> 'b list (** Same as [mapi], but where the indices start with 1 *) - val for_all : ('a -> bool) -> 'a vector -> bool - - val exists : ('a -> bool) -> 'a vector -> bool - val pp_set_t : Format.formatter -> set_t -> unit val show_set_t : set_t -> string @@ -85,11 +61,6 @@ module type Id = sig module Map : Map.S with type key = id val id_of_json : Yojson.Basic.t -> (id, string) result - - val vector_of_json : - (Yojson.Basic.t -> ('a, string) result) -> - Yojson.Basic.t -> - ('a vector, string) result end (** Generative functor for identifiers. @@ -102,8 +73,6 @@ module IdGen () : Id = struct type generator = id [@@deriving show] - type 'a vector = 'a list [@@deriving show] - let zero = 0 let generator_zero = 0 @@ -122,14 +91,6 @@ module IdGen () : Id = struct let of_int x = x - let empty_vector = [] - - let vector_to_list v = v - - let vector_of_list v = v - - let length v = List.length v - let nth v id = List.nth v id let nth_opt v id = List.nth_opt v id @@ -140,10 +101,6 @@ module IdGen () : Id = struct | _ :: vec', 0 -> v :: vec' | x :: vec', _ -> x :: update_nth vec' (id - 1) v - let iter = List.iter - - let map = List.map - let mapi = List.mapi let mapi_from1 f ls = @@ -152,10 +109,6 @@ module IdGen () : Id = struct in aux 1 ls - let for_all = List.for_all - - let exists = List.exists - module Ord = struct type t = id @@ -183,10 +136,6 @@ module IdGen () : Id = struct match js with | `Int i -> Ok i | _ -> Error ("id_of_json: failed on " ^ Yojson.Basic.show js) - - let vector_of_json a_of_json js = - OfJsonBasic.combine_error_msgs js "vector_of_json" - (OfJsonBasic.list_of_json a_of_json js) end type name = string list [@@deriving show] diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 05dc3f5a..003f5411 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -47,8 +47,7 @@ let expression_to_string ctx = let mk_unit_ty : T.ety = T.Tuple [] (* TODO: move *) -let mk_unit_value : V.typed_value = - { V.value = V.Tuple (T.FieldId.vector_of_list []); V.ty = mk_unit_ty } +let mk_unit_value : V.typed_value = { V.value = V.Tuple []; V.ty = mk_unit_ty } let mk_typed_value (ty : T.ety) (value : V.value) : V.typed_value = { V.value; ty } @@ -81,8 +80,8 @@ let rec check_borrows_in_value (check : V.borrow_content -> bool) (v : V.typed_value) : bool = match v.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> true - | V.Adt av -> T.FieldId.for_all (check_borrows_in_value check) av.field_values - | V.Tuple values -> T.FieldId.for_all (check_borrows_in_value check) values + | V.Adt av -> List.for_all (check_borrows_in_value check) av.field_values + | V.Tuple values -> List.for_all (check_borrows_in_value check) values | V.Assumed (Box bv) -> check_borrows_in_value check bv | V.Borrow bc -> ( check bc @@ -100,8 +99,8 @@ let rec check_loans_in_value (check : V.loan_content -> bool) (v : V.typed_value) : bool = match v.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> true - | V.Adt av -> T.FieldId.for_all (check_loans_in_value check) av.field_values - | V.Tuple values -> T.FieldId.for_all (check_loans_in_value check) values + | V.Adt av -> List.for_all (check_loans_in_value check) av.field_values + | V.Tuple values -> List.for_all (check_loans_in_value check) values | V.Assumed (Box bv) -> check_loans_in_value check bv | V.Borrow bc -> ( match bc with @@ -119,12 +118,8 @@ let rec lookup_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id) (v : V.typed_value) : V.loan_content option = match v.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> None - | V.Adt av -> - let values = T.FieldId.vector_to_list av.field_values in - List.find_map (lookup_loan_in_value ek l) values - | V.Tuple values -> - let values = T.FieldId.vector_to_list values in - List.find_map (lookup_loan_in_value ek l) values + | V.Adt av -> List.find_map (lookup_loan_in_value ek l) av.field_values + | V.Tuple values -> List.find_map (lookup_loan_in_value ek l) values | V.Assumed (Box bv) -> lookup_loan_in_value ek l bv | V.Borrow bc -> ( match bc with @@ -175,13 +170,11 @@ let rec update_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id) match v.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> v | V.Adt av -> - let values = - T.FieldId.map (update_loan_in_value ek l nlc) av.field_values - in + let values = List.map (update_loan_in_value ek l nlc) av.field_values in let av = { av with field_values = values } in { v with value = Adt av } | V.Tuple values -> - let values = T.FieldId.map (update_loan_in_value ek l nlc) values in + let values = List.map (update_loan_in_value ek l nlc) values in { v with value = Tuple values } | V.Assumed (Box bv) -> { v with value = Assumed (Box (update_loan_in_value ek l nlc bv)) } @@ -228,12 +221,8 @@ let rec lookup_borrow_in_value (ek : exploration_kind) (l : V.BorrowId.id) (v : V.typed_value) : V.borrow_content option = match v.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> None - | V.Adt av -> - let values = T.FieldId.vector_to_list av.field_values in - List.find_map (lookup_borrow_in_value ek l) values - | V.Tuple values -> - let values = T.FieldId.vector_to_list values in - List.find_map (lookup_borrow_in_value ek l) values + | V.Adt av -> List.find_map (lookup_borrow_in_value ek l) av.field_values + | V.Tuple values -> List.find_map (lookup_borrow_in_value ek l) values | V.Assumed (Box bv) -> lookup_borrow_in_value ek l bv | V.Borrow bc -> ( match bc with @@ -281,13 +270,11 @@ let rec update_borrow_in_value (ek : exploration_kind) (l : V.BorrowId.id) match v.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> v | V.Adt av -> - let values = - T.FieldId.map (update_borrow_in_value ek l nbc) av.field_values - in + let values = List.map (update_borrow_in_value ek l nbc) av.field_values in let av = { av with field_values = values } in { v with value = Adt av } | V.Tuple values -> - let values = T.FieldId.map (update_borrow_in_value ek l nbc) values in + let values = List.map (update_borrow_in_value ek l nbc) values in { v with value = Tuple values } | V.Assumed (Box bv) -> { v with value = Assumed (Box (update_borrow_in_value ek l nbc bv)) } @@ -369,12 +356,8 @@ let borrows_in_value (v : V.typed_value) : bool = let rec loans_in_value (v : V.typed_value) : bool = match v.V.value with | V.Concrete _ -> false - | V.Adt av -> - let fields = T.FieldId.vector_to_list av.field_values in - List.exists loans_in_value fields - | V.Tuple fields -> - let fields = T.FieldId.vector_to_list fields in - List.exists loans_in_value fields + | V.Adt av -> List.exists loans_in_value av.field_values + | V.Tuple fields -> List.exists loans_in_value fields | V.Assumed (Box bv) -> loans_in_value bv | V.Borrow bc -> ( match bc with @@ -387,12 +370,8 @@ let rec loans_in_value (v : V.typed_value) : bool = let rec get_first_loan_in_value (v : V.typed_value) : V.loan_content option = match v.V.value with | V.Concrete _ -> None - | V.Adt av -> - let fields = T.FieldId.vector_to_list av.field_values in - get_first_loan_in_values fields - | V.Tuple fields -> - let fields = T.FieldId.vector_to_list fields in - get_first_loan_in_values fields + | V.Adt av -> get_first_loan_in_values av.field_values + | V.Tuple fields -> get_first_loan_in_values fields | V.Assumed (Box bv) -> get_first_loan_in_value bv | V.Borrow bc -> ( match bc with @@ -413,12 +392,8 @@ and get_first_loan_in_values (vl : V.typed_value list) : V.loan_content option = let rec bottom_in_value (v : V.typed_value) : bool = match v.V.value with | V.Concrete _ -> false - | V.Adt av -> - let fields = T.FieldId.vector_to_list av.field_values in - List.exists bottom_in_value fields - | V.Tuple fields -> - let fields = T.FieldId.vector_to_list fields in - List.exists bottom_in_value fields + | V.Adt av -> List.exists bottom_in_value av.field_values + | V.Tuple fields -> List.exists bottom_in_value fields | V.Assumed (Box bv) -> bottom_in_value bv | V.Borrow bc -> ( match bc with @@ -450,19 +425,16 @@ let rec end_borrow_get_borrow_in_value (config : C.config) (io : inner_outer) * boxes upon ending inner borrows *) ({ v0 with value = Assumed (Box bv') }, res) | V.Adt adt -> - let values = T.FieldId.vector_to_list adt.field_values in - let values', res = - end_borrow_get_borrow_in_values config io l outer_borrows values + let values, res = + end_borrow_get_borrow_in_values config io l outer_borrows + adt.field_values in - let values' = T.FieldId.vector_of_list values' in - ({ v0 with value = Adt { adt with field_values = values' } }, res) + ({ v0 with value = Adt { adt with field_values = values } }, res) | V.Tuple values -> - let values = T.FieldId.vector_to_list values in - let values', res = + let values, res = end_borrow_get_borrow_in_values config io l outer_borrows values in - let values' = T.FieldId.vector_of_list values' in - ({ v0 with value = Tuple values' }, res) + ({ v0 with value = Tuple values }, res) | V.Loan (V.MutLoan _) -> (v0, NotFound) | V.Loan (V.SharedLoan (borrows, v)) -> (* Update the outer borrows, if necessary *) @@ -543,19 +515,11 @@ let rec give_back_value_to_value config bid (v : V.typed_value) | V.Concrete _ | V.Bottom | V.Symbolic _ -> destv | V.Adt av -> let field_values = - List.map - (give_back_value_to_value config bid v) - (T.FieldId.vector_to_list av.field_values) + List.map (give_back_value_to_value config bid v) av.field_values in - let field_values = T.FieldId.vector_of_list field_values in { destv with value = Adt { av with field_values } } | V.Tuple values -> - let values = - List.map - (give_back_value_to_value config bid v) - (T.FieldId.vector_to_list values) - in - let values = T.FieldId.vector_of_list values in + let values = List.map (give_back_value_to_value config bid v) values in { destv with value = Tuple values } | V.Assumed (Box destv') -> { @@ -590,19 +554,11 @@ let rec give_back_shared_to_value (config : C.config) bid | V.Concrete _ | V.Bottom | V.Symbolic _ -> destv | V.Adt av -> let field_values = - List.map - (give_back_shared_to_value config bid) - (T.FieldId.vector_to_list av.field_values) + List.map (give_back_shared_to_value config bid) av.field_values in - let field_values = T.FieldId.vector_of_list field_values in { destv with value = Adt { av with field_values } } | V.Tuple values -> - let values = - List.map - (give_back_shared_to_value config bid) - (T.FieldId.vector_to_list values) - in - let values = T.FieldId.vector_of_list values in + let values = List.map (give_back_shared_to_value config bid) values in { destv with value = Tuple values } | V.Assumed (Box destv') -> { @@ -699,14 +655,10 @@ let reborrow_shared (config : C.config) (original_bid : V.BorrowId.id) match v.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> v | V.Adt av -> - let fields = T.FieldId.vector_to_list av.field_values in - let fields = List.map reborrow_in_value fields in - let fields = T.FieldId.vector_of_list fields in + let fields = List.map reborrow_in_value av.field_values in { v with value = Adt { av with field_values = fields } } | V.Tuple fields -> - let fields = T.FieldId.vector_to_list fields in let fields = List.map reborrow_in_value fields in - let fields = T.FieldId.vector_of_list fields in { v with value = Tuple fields } | V.Assumed (Box bv) -> { v with value = Assumed (Box (reborrow_in_value bv)) } @@ -1045,7 +997,7 @@ let rec access_projection (access : projection_access) (env : C.env) Ok (env1, { res with updated })) (* Tuples *) | Field (ProjTuple arity, field_id), V.Tuple values -> ( - assert (arity = T.FieldId.length values); + assert (arity = List.length values); let fv = T.FieldId.nth values field_id in (* Project *) match access_projection access env update p' fv with @@ -1238,7 +1190,7 @@ let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place) | Ok ctx -> ctx (** Compute an expanded ADT bottom value *) -let compute_expanded_bottom_adt_value (tyctx : T.type_def T.TypeDefId.vector) +let compute_expanded_bottom_adt_value (tyctx : T.type_def list) (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option) (regions : T.erased_region list) (types : T.ety list) : V.typed_value = (* Lookup the definition and check if it is an enumeration - it @@ -1246,15 +1198,13 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_def T.TypeDefId.vector) is a field projection with *some* variant id. Retrieve the list of fields at the same time. *) let def = T.TypeDefId.nth tyctx def_id in - assert (List.length regions = T.RegionVarId.length def.T.region_params); + assert (List.length regions = List.length def.T.region_params); (* Compute the field types *) let field_types = Subst.type_def_get_instantiated_field_type def opt_variant_id types in (* Initialize the expanded value *) - let field_types = T.FieldId.vector_to_list field_types in let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in - let fields = T.FieldId.vector_of_list fields in let av = V.Adt { @@ -1273,7 +1223,6 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) : V.typed_value = (* Generate the field values *) let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in - let fields = T.FieldId.vector_of_list fields in let v = V.Tuple fields in let ty = T.Tuple field_types in { V.value = v; V.ty } @@ -1434,8 +1383,8 @@ let rec collect_borrows_at_place (config : C.config) (access : access_kind) (* Nothing to do for symbolic values - note that if the value needs to be copied, etc. we perform additional checks later *) () - | V.Adt adt -> T.FieldId.iter inspect_update adt.field_values - | V.Tuple values -> T.FieldId.iter inspect_update values + | V.Adt adt -> List.iter inspect_update adt.field_values + | V.Tuple values -> List.iter inspect_update values | V.Assumed (Box v) -> inspect_update v | V.Borrow bc -> ( match bc with @@ -1534,9 +1483,8 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place) | V.Symbolic _ -> (* Nothing to do for symbolic values - TODO: not sure *) raise Unimplemented - | V.Adt adt -> - T.FieldId.iter (inspect_update end_loans) adt.field_values - | V.Tuple values -> T.FieldId.iter (inspect_update end_loans) values + | V.Adt adt -> List.iter (inspect_update end_loans) adt.field_values + | V.Tuple values -> List.iter (inspect_update end_loans) values | V.Assumed (Box v) -> inspect_update end_loans v | V.Borrow bc -> ( assert (not end_loans); @@ -1609,15 +1557,13 @@ let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) : match v.V.value with | V.Concrete _ -> (ctx, v) | V.Adt av -> - let fields = T.FieldId.vector_to_list av.field_values in - let ctx', fields = List.fold_left_map (copy_value config) ctx fields in - let fields = T.FieldId.vector_of_list fields in - (ctx', { v with V.value = V.Adt { av with field_values = fields } }) + let ctx, fields = + List.fold_left_map (copy_value config) ctx av.field_values + in + (ctx, { v with V.value = V.Adt { av with field_values = fields } }) | V.Tuple fields -> - let fields = T.FieldId.vector_to_list fields in - let ctx', fields = List.fold_left_map (copy_value config) ctx fields in - let fields = T.FieldId.vector_of_list fields in - (ctx', { v with V.value = V.Tuple fields }) + let ctx, fields = List.fold_left_map (copy_value config) ctx fields in + (ctx, { v with V.value = V.Tuple fields }) | V.Bottom -> failwith "Can't copy ⊥" | V.Assumed _ -> failwith "Can't copy an assumed value" | V.Borrow bc -> ( @@ -1625,6 +1571,7 @@ let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) : match bc with | SharedBorrow bid -> let ctx', bid' = C.fresh_borrow_id ctx in + (* TODO: clean indices *) let env'' = reborrow_shared config bid bid' ctx'.env in let ctx'' = { ctx' with env = env'' } in (ctx'', { v with V.value = V.Borrow (SharedBorrow bid') }) @@ -1646,36 +1593,30 @@ let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) (* Check the type while converting *) match (ty, cv) with (* Unit *) - | T.Tuple [], Unit -> { V.value = V.Tuple (T.FieldId.vector_of_list []); ty } + | T.Tuple [], Unit -> { V.value = V.Tuple []; ty } (* Adt with one variant and no fields *) | T.Adt (def_id, [], []), ConstantAdt def_id' -> assert (def_id = def_id'); (* Check that the adt definition only has one variant with no fields, compute the variant id at the same time. *) let def = T.TypeDefId.nth ctx.type_context def_id in - assert (T.RegionVarId.length def.region_params = 0); - assert (T.TypeVarId.length def.type_params = 0); + assert (List.length def.region_params = 0); + assert (List.length def.type_params = 0); let variant_id = match def.kind with | Struct fields -> - assert (T.FieldId.length fields = 0); + assert (List.length fields = 0); None | Enum variants -> - assert (T.VariantId.length variants = 1); + assert (List.length variants = 1); let variant_id = T.VariantId.zero in let variant = T.VariantId.nth variants variant_id in - assert (T.FieldId.length variant.fields = 0); + assert (List.length variant.fields = 0); Some variant_id in let value = V.Adt - { - def_id; - variant_id; - regions = []; - types = []; - field_values = T.FieldId.vector_of_list []; - } + { def_id; variant_id; regions = []; types = []; field_values = [] } in { value; ty } (* Scalar, boolean... *) @@ -1918,24 +1859,20 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : | E.Aggregate (aggregate_kind, ops) -> ( (* Evaluate the operands *) let ctx, values = eval_operands config ctx ops in - let values = T.FieldId.vector_of_list values in (* Match on the aggregate kind *) match aggregate_kind with | E.AggregatedTuple -> - let tys = - List.map (fun v -> v.V.ty) (T.FieldId.vector_to_list values) - in + let tys = List.map (fun v -> v.V.ty) values in Ok (ctx, { V.value = Tuple values; ty = T.Tuple tys }) | E.AggregatedAdt (def_id, opt_variant_id, regions, types) -> (* Sanity checks *) let type_def = C.ctx_lookup_type_def ctx def_id in - assert ( - T.RegionVarId.length type_def.region_params = List.length regions); + assert (List.length type_def.region_params = List.length regions); let expected_field_types = Subst.ctx_adt_get_instantiated_field_types ctx def_id opt_variant_id types in - assert (expected_field_types = T.FieldId.map (fun v -> v.V.ty) values); + assert (expected_field_types = List.map (fun v -> v.V.ty) values); (* Construct the value *) let av = { @@ -2312,10 +2249,7 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx) (* Create and push the input variables *) let input_vars = - V.VarId.vector_to_list - (V.VarId.mapi_from1 - (fun id v -> (mk_var id None v.V.ty, v)) - (V.VarId.vector_of_list args_vl)) + V.VarId.mapi_from1 (fun id v -> (mk_var id None v.V.ty, v)) args_vl in let ctx = C.ctx_push_vars ctx input_vars in @@ -2413,13 +2347,10 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx) | ConcreteMode -> ( let tsubst = Subst.make_type_subst - (List.map - (fun v -> v.T.tv_index) - (T.TypeVarId.vector_to_list def.A.signature.type_params)) + (List.map (fun v -> v.T.tv_index) def.A.signature.type_params) type_params in let locals, body = Subst.fun_def_substitute_in_body tsubst def in - let locals = V.VarId.vector_to_list locals in (* Evaluate the input operands *) let ctx1, args = eval_operands config ctx args in @@ -2554,9 +2485,8 @@ and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) : (** Test a unit function (taking no arguments) by evaluating it in an empty environment *) -let test_unit_function (type_defs : T.type_def T.TypeDefId.vector) - (fun_defs : A.fun_def A.FunDefId.vector) (fid : A.FunDefId.id) : - unit eval_result = +let test_unit_function (type_defs : T.type_def list) (fun_defs : A.fun_def list) + (fid : A.FunDefId.id) : unit eval_result = (* Retrieve the function declaration *) let fdef = A.FunDefId.nth fun_defs fid in @@ -2565,8 +2495,8 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector) (lazy ("test_unit_function: " ^ Print.Types.name_to_string fdef.A.name)); (* Sanity check - *) - assert (T.RegionVarId.length fdef.A.signature.region_params = 0); - assert (T.TypeVarId.length fdef.A.signature.type_params = 0); + assert (List.length fdef.A.signature.region_params = 0); + assert (List.length fdef.A.signature.type_params = 0); assert (fdef.A.arg_count = 0); (* Create the evaluation context *) @@ -2574,7 +2504,7 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector) { C.type_context = type_defs; C.fun_context = fun_defs; - C.type_vars = T.TypeVarId.empty_vector; + C.type_vars = []; C.env = []; C.symbolic_counter = V.SymbolicValueId.generator_zero; C.borrow_counter = V.BorrowId.generator_zero; @@ -2582,9 +2512,7 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector) in (* Put the (uninitialized) local variables *) - let ctx = - C.ctx_push_uninitialized_vars ctx (V.VarId.vector_to_list fdef.A.locals) - in + let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in (* Evaluate the function *) let config = { C.mode = C.ConcreteMode; C.check_invariants = true } in @@ -2596,13 +2524,13 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector) no arguments) - TODO: move *) let fun_def_is_unit (def : A.fun_def) : bool = def.A.arg_count = 0 - && T.RegionVarId.length def.A.signature.region_params = 0 - && T.TypeVarId.length def.A.signature.type_params = 0 - && V.VarId.length def.A.signature.inputs = 0 + && List.length def.A.signature.region_params = 0 + && List.length def.A.signature.type_params = 0 + && List.length def.A.signature.inputs = 0 (** Test all the unit functions in a list of function definitions *) -let test_all_unit_functions (type_defs : T.type_def T.TypeDefId.vector) - (fun_defs : A.fun_def A.FunDefId.vector) : unit = +let test_all_unit_functions (type_defs : T.type_def list) + (fun_defs : A.fun_def list) : unit = let test_fun (def : A.fun_def) : unit = if fun_def_is_unit def then match test_unit_function type_defs fun_defs def.A.def_id with @@ -2610,4 +2538,4 @@ let test_all_unit_functions (type_defs : T.type_def T.TypeDefId.vector) | Ok _ -> () else () in - A.FunDefId.iter test_fun fun_defs + List.iter test_fun fun_defs diff --git a/src/Modules.ml b/src/Modules.ml index a2b1d3bf..3be1c742 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -15,7 +15,7 @@ type declaration = type cfim_module = { declarations : declaration list; - types : type_def TypeDefId.vector; - functions : fun_def FunDefId.vector; + types : type_def list; + functions : fun_def list; } (** CFIM module *) diff --git a/src/Print.ml b/src/Print.ml index 8547d5cb..bb172d5f 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -98,18 +98,15 @@ module Types = struct let variant_to_string fmt (v : T.variant) : string = v.variant_name ^ "(" - ^ String.concat ", " - (List.map (field_to_string fmt) (T.FieldId.vector_to_list v.fields)) + ^ String.concat ", " (List.map (field_to_string fmt) v.fields) ^ ")" let name_to_string (name : name) : string = String.concat "::" name let type_def_to_string (type_def_id_to_string : T.TypeDefId.id -> string) (def : T.type_def) : string = - let regions : T.region_var list = - T.RegionVarId.vector_to_list def.region_params - in - let types : T.type_var list = T.TypeVarId.vector_to_list def.type_params in + let regions = def.region_params in + let types = def.type_params in let rid_to_string rid = match List.find_opt (fun rv -> rv.T.rv_index = rid) regions with | Some rv -> region_var_to_string rv @@ -133,7 +130,6 @@ module Types = struct in match def.kind with | T.Struct fields -> - let fields = T.FieldId.vector_to_list fields in if List.length fields > 0 then let fields = String.concat "," @@ -142,7 +138,6 @@ module Types = struct "struct " ^ name ^ params ^ "{" ^ fields ^ "}" else "struct " ^ name ^ params ^ "{}" | T.Enum variants -> - let variants = T.VariantId.vector_to_list variants in let variants = List.map (fun v -> "| " ^ variant_to_string fmt v) variants in @@ -222,8 +217,9 @@ module Values = struct | Some vid -> fmt.adt_variant_to_string av.def_id vid | None -> fmt.type_def_id_to_string av.def_id in - let field_values = T.FieldId.vector_to_list av.field_values in - let field_values = List.map (typed_value_to_string fmt) field_values in + let field_values = + List.map (typed_value_to_string fmt) av.field_values + in if List.length field_values > 0 then match fmt.adt_field_names av.V.def_id av.V.variant_id with | None -> @@ -240,7 +236,6 @@ module Values = struct adt_ident ^ " { " ^ field_values ^ " }" else adt_ident | Tuple values -> - let values = T.FieldId.vector_to_list values in let values = String.concat ", " (List.map (typed_value_to_string fmt) values) in @@ -302,7 +297,7 @@ module Values = struct | Some vid -> fmt.adt_variant_to_string av.adef_id vid | None -> fmt.type_def_id_to_string av.adef_id in - let field_values = T.FieldId.vector_to_list av.afield_values in + let field_values = av.afield_values in if List.length field_values > 0 then let field_values = String.concat " " @@ -311,7 +306,6 @@ module Values = struct adt_ident ^ " " ^ field_values else adt_ident | ATuple values -> - let values = T.FieldId.vector_to_list values in let values = String.concat ", " (List.map (typed_avalue_to_string fmt) values) in @@ -428,8 +422,7 @@ module Contexts = struct let ctx_to_rtype_formatter (fmt : ctx_formatter) : PT.rtype_formatter = PV.value_to_rtype_formatter fmt - let type_ctx_to_adt_variant_to_string_fun - (ctx : T.type_def T.TypeDefId.vector) : + let type_ctx_to_adt_variant_to_string_fun (ctx : T.type_def list) : T.TypeDefId.id -> T.VariantId.id -> string = fun def_id variant_id -> let def = T.TypeDefId.nth ctx def_id in @@ -439,14 +432,14 @@ module Contexts = struct let variant = T.VariantId.nth variants variant_id in PT.name_to_string def.name ^ "::" ^ variant.variant_name - let type_ctx_to_adt_field_names_fun (ctx : T.type_def T.TypeDefId.vector) : + let type_ctx_to_adt_field_names_fun (ctx : T.type_def list) : T.TypeDefId.id -> T.VariantId.id option -> string list option = fun def_id opt_variant_id -> let def = T.TypeDefId.nth ctx def_id in let fields = T.type_def_get_fields def opt_variant_id in (* TODO: the field name should be optional?? *) - let fields = T.FieldId.map (fun f -> f.T.field_name) fields in - Some (T.FieldId.vector_to_list fields) + let fields = List.map (fun f -> f.T.field_name) fields in + Some fields let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter = (* We shouldn't use r_to_string *) @@ -547,8 +540,8 @@ module CfimAst = struct PT.type_def_id_to_string = fmt.type_def_id_to_string; } - let type_ctx_to_adt_field_to_string_fun (ctx : T.type_def T.TypeDefId.vector) - : T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string = + let type_ctx_to_adt_field_to_string_fun (ctx : T.type_def list) : + T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string = fun def_id opt_variant_id field_id -> let def = T.TypeDefId.nth ctx def_id in let fields = T.type_def_get_fields def opt_variant_id in @@ -783,8 +776,8 @@ module CfimAst = struct let name = PT.name_to_string def.A.name in (* Region/type parameters *) - let regions = T.RegionVarId.vector_to_list sg.region_params in - let types = T.TypeVarId.vector_to_list sg.type_params in + let regions = sg.region_params in + let types = sg.type_params in let params = if List.length regions + List.length types = 0 then "" else @@ -794,14 +787,14 @@ module CfimAst = struct in (* Arguments *) - let inputs = V.VarId.vector_to_list def.locals in + let inputs = def.locals in let ret_var, inputs = match inputs with | [] -> failwith "Inconsistent signature" | ret_var :: inputs -> (ret_var, inputs) in let inputs, _aux_locals = Utilities.list_split_at inputs def.arg_count in - let args = List.combine inputs (V.VarId.vector_to_list sg.inputs) in + let args = List.combine inputs sg.inputs in let args = List.map (fun (var, rty) -> PV.var_to_string var ^ " : " ^ rty_to_string rty) @@ -821,7 +814,7 @@ module CfimAst = struct (fun var -> indent ^ indent_incr ^ PV.var_to_string var ^ " : " ^ ety_to_string var.var_ty ^ ";") - (V.VarId.vector_to_list def.locals) + def.locals in let locals = String.concat "\n" locals in @@ -841,8 +834,8 @@ module PA = CfimAst (* local module *) module Module = struct (** This function pretty-prints a type definition by using a definition context *) - let type_def_to_string (type_context : T.type_def T.TypeDefId.vector) - (def : T.type_def) : string = + let type_def_to_string (type_context : T.type_def list) (def : T.type_def) : + string = let type_def_id_to_string (id : T.TypeDefId.id) : string = let def = T.TypeDefId.nth type_context id in PT.name_to_string def.name @@ -851,9 +844,8 @@ module Module = struct (** Generate an [ast_formatter] by using a definition context in combination with the variables local to a function's definition *) - let def_ctx_to_ast_formatter (type_context : T.type_def T.TypeDefId.vector) - (fun_context : A.fun_def A.FunDefId.vector) (def : A.fun_def) : - PA.ast_formatter = + let def_ctx_to_ast_formatter (type_context : T.type_def list) + (fun_context : A.fun_def list) (def : A.fun_def) : PA.ast_formatter = let r_to_string vid = let var = T.RegionVarId.nth def.signature.region_params vid in PT.region_var_to_string var @@ -894,24 +886,18 @@ module Module = struct (** This function pretty-prints a function definition by using a definition context *) - let fun_def_to_string (type_context : T.type_def T.TypeDefId.vector) - (fun_context : A.fun_def A.FunDefId.vector) (def : A.fun_def) : string = + let fun_def_to_string (type_context : T.type_def list) + (fun_context : A.fun_def list) (def : A.fun_def) : string = let fmt = def_ctx_to_ast_formatter type_context fun_context def in PA.fun_def_to_string fmt "" " " def let module_to_string (m : M.cfim_module) : string = (* The types *) - let type_defs = - List.map - (type_def_to_string m.M.types) - (T.TypeDefId.vector_to_list m.M.types) - in + let type_defs = List.map (type_def_to_string m.M.types) m.M.types in (* The functions *) let fun_defs = - List.map - (fun_def_to_string m.M.types m.M.functions) - (A.FunDefId.vector_to_list m.M.functions) + List.map (fun_def_to_string m.M.types m.M.functions) m.M.functions in (* Put everything together *) diff --git a/src/Substitute.ml b/src/Substitute.ml index 452b125f..b8c3edd9 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -54,17 +54,12 @@ let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) : (** Instantiate the type variables in an ADT definition, and return the list of types of the fields for the chosen variant *) let type_def_get_instantiated_field_type (def : T.type_def) - (opt_variant_id : T.VariantId.id option) (types : T.ety list) : - T.ety T.FieldId.vector = + (opt_variant_id : T.VariantId.id option) (types : T.ety list) : T.ety list = let ty_subst = - make_type_subst - (List.map - (fun x -> x.T.tv_index) - (T.TypeVarId.vector_to_list def.T.type_params)) - types + make_type_subst (List.map (fun x -> x.T.tv_index) def.T.type_params) types in let fields = T.type_def_get_fields def opt_variant_id in - T.FieldId.map + List.map (fun f -> erase_regions_substitute_types ty_subst f.T.field_ty) fields @@ -72,7 +67,7 @@ let type_def_get_instantiated_field_type (def : T.type_def) context *) let ctx_adt_get_instantiated_field_types (ctx : C.eval_ctx) (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option) - (types : T.ety list) : T.ety T.FieldId.vector = + (types : T.ety list) : T.ety list = let def = C.ctx_lookup_type_def ctx def_id in type_def_get_instantiated_field_type def opt_variant_id types @@ -204,10 +199,10 @@ and switch_targets_substitute (tsubst : T.TypeVarId.id -> T.ety) (** Apply a type substitution to a function body. Return the local variables and the body. *) let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety) - (def : A.fun_def) : V.var V.VarId.vector * A.expression = + (def : A.fun_def) : V.var list * A.expression = let rsubst r = r in let locals = - V.VarId.map + List.map (fun v -> { v with V.var_ty = ty_substitute rsubst tsubst v.V.var_ty }) def.A.locals in diff --git a/src/Types.ml b/src/Types.ml index 77296ac1..2b57e3f7 100644 --- a/src/Types.ml +++ b/src/Types.ml @@ -90,19 +90,16 @@ type ety = erased_region ty [@@deriving show] type field = { field_name : string; field_ty : rty } [@@deriving show] -type variant = { variant_name : string; fields : field FieldId.vector } -[@@deriving show] +type variant = { variant_name : string; fields : field list } [@@deriving show] -type type_def_kind = - | Struct of field FieldId.vector - | Enum of variant VariantId.vector +type type_def_kind = Struct of field list | Enum of variant list [@@deriving show] type type_def = { def_id : TypeDefId.id; name : name; - region_params : region_var RegionVarId.vector; - type_params : type_var TypeVarId.vector; + region_params : region_var list; + type_params : type_var list; kind : type_def_kind; } [@@deriving show] @@ -137,7 +134,7 @@ let rec erase_regions (ty : rty) : ety = Raises [Invalid_argument] if the arguments are incorrect. *) let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option) - : field FieldId.vector = + : field list = match (def.kind, opt_variant_id) with | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields | Struct fields, None -> fields diff --git a/src/Values.ml b/src/Values.ml index 9d1cb819..330f22d3 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -79,7 +79,7 @@ type symbolic_proj_comp = { type value = | Concrete of constant_value (** Concrete (non-symbolic) value *) | Adt of adt_value (** Enumerations and structures *) - | Tuple of typed_value FieldId.vector + | Tuple of typed_value list (** Tuple - note that units are encoded as 0-tuples *) | Bottom (** No value (uninitialized or moved value) *) | Assumed of assumed_value (** Assumed types (Box, Vec, Cell...) *) @@ -93,7 +93,7 @@ and adt_value = { variant_id : VariantId.id option; regions : erased_region list; types : ety list; - field_values : typed_value FieldId.vector; + field_values : typed_value list; } [@@deriving show] @@ -138,7 +138,7 @@ type abstract_shared_borrows = type avalue = | AConcrete of constant_value | AAdt of aadt_value - | ATuple of typed_avalue FieldId.vector + | ATuple of typed_avalue list | ABottom | ALoan of aloan_content | ABorrow of aborrow_content @@ -151,7 +151,7 @@ and aadt_value = { avariant_id : VariantId.id option; aregions : erased_region list; atypes : rty list; - afield_values : typed_avalue FieldId.vector; + afield_values : typed_avalue list; } [@@deriving show] -- cgit v1.2.3