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/Interpreter.ml | 208 ++++++++++++++++++----------------------------------- 1 file changed, 68 insertions(+), 140 deletions(-) (limited to 'src/Interpreter.ml') 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 -- cgit v1.2.3