summaryrefslogtreecommitdiff
path: root/src/Interpreter.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/Interpreter.ml')
-rw-r--r--src/Interpreter.ml208
1 files changed, 68 insertions, 140 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 13:52:54 +0000