From c8a2793a87e6a7f6a4ebdfc0e52140048bfd97f6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 8 Dec 2021 12:47:17 +0100 Subject: Remove g_value, g_typed_value, etc. to make values and abstract values distinct --- src/Interpreter.ml | 47 +++++++++++++++++++++++++++++++---------------- 1 file changed, 31 insertions(+), 16 deletions(-) (limited to 'src/Interpreter.ml') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index d6367702..ad7bdba1 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -251,11 +251,11 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) else () (** Check the borrow id and control the diving *) - method! visit_SharedBorrow env bid = + method! visit_SharedBorrow _env bid = if bid = l then raise (FoundBorrowContent (V.SharedBorrow bid)) else () (** Check the borrow id *) - method! visit_InactivatedMutBorrow env bid = + method! visit_InactivatedMutBorrow _env bid = if bid = l then raise (FoundBorrowContent (V.InactivatedMutBorrow bid)) else () (** Check the borrow id *) @@ -372,7 +372,7 @@ let unwrap_res_to_outer_or opt default = match opt with Some x -> Outer x | None -> default (** Return the first loan we find in a value *) -let rec get_first_loan_in_value (v : V.typed_value) : V.loan_content option = +let get_first_loan_in_value (v : V.typed_value) : V.loan_content option = let obj = object inherit [_] V.iter_typed_value @@ -387,7 +387,7 @@ let rec get_first_loan_in_value (v : V.typed_value) : V.loan_content option = with FoundLoanContent lc -> Some lc (** Check if a value contains ⊥ *) -let rec bottom_in_value (v : V.typed_value) : bool = +let bottom_in_value (v : V.typed_value) : bool = let obj = object inherit [_] V.iter_typed_value @@ -1202,7 +1202,11 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_def list) Subst.type_def_get_instantiated_field_type def opt_variant_id types in (* Initialize the expanded value *) - let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in + let fields = + List.map + (fun ty : V.typed_value -> ({ V.value = V.Bottom; ty } : V.typed_value)) + field_types + in let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in let ty = T.Adt (T.AdtId def_id, regions, types) in { V.value = av; V.ty } @@ -1211,7 +1215,9 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_def list) 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 = + List.map (fun ty : V.typed_value -> { V.value = Bottom; ty }) field_types + in let v = V.Adt { variant_id = None; field_values = fields } in let ty = T.Adt (T.Tuple, [], field_types) in { V.value = v; V.ty } @@ -1366,7 +1372,7 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) We use exceptions to make it handy: whenever we update the context, we raise an exception wrapping the updated context. *) - let rec inspect_update v : unit = + let rec inspect_update (v : V.typed_value) : unit = match v.V.value with | V.Concrete _ -> () | V.Bottom -> () @@ -1463,7 +1469,7 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place) We use exceptions to make it handy. *) - let rec inspect_update (end_loans : bool) v : unit = + let rec inspect_update (end_loans : bool) (v : V.typed_value) : unit = match v.V.value with | V.Concrete _ -> () | V.Bottom -> @@ -1654,7 +1660,7 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : (* Move the value *) L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx v)); assert (not (bottom_in_value v)); - let bottom = { V.value = Bottom; ty = v.ty } in + let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in match write_place config access p bottom ctx with | Error _ -> failwith "Unreachable" | Ok ctx -> (ctx, v)) @@ -1723,7 +1729,8 @@ let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop) | E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq -> failwith "Unreachable" in - Ok { V.value = V.Concrete (Bool b); ty = T.Bool } + Ok + ({ V.value = V.Concrete (Bool b); ty = T.Bool } : V.typed_value) | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd | E.BitOr -> ( (* The two operands must have the same type and the result is an integer *) @@ -1783,7 +1790,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : if bkind = E.Shared then V.SharedBorrow bid else V.InactivatedMutBorrow bid in - let rv = { V.value = V.Borrow bc; ty = rv_ty } in + let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in (* Compute the value with which to replace the value at place p *) let nv = match v.V.value with @@ -1809,7 +1816,9 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) let ctx, bid = C.fresh_borrow_id ctx in let rv_ty = T.Ref (T.Erased, v.ty, Mut) in - let rv = { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty } in + let rv : V.typed_value = + { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty } + in (* Compute the value with which to replace the value at place p *) let nv = { v with V.value = V.Loan (V.MutLoan bid) } in (* Update the value in the context *) @@ -1847,7 +1856,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : (* Match on the aggregate kind *) match aggregate_kind with | E.AggregatedTuple -> - let tys = List.map (fun v -> v.V.ty) values in + let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in let v = V.Adt { variant_id = None; field_values = values } in let ty = T.Adt (T.Tuple, [], tys) in Ok (ctx, { V.value = v; ty }) @@ -1859,9 +1868,13 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : Subst.ctx_adt_get_instantiated_field_types ctx def_id opt_variant_id types in - assert (expected_field_types = List.map (fun v -> v.V.ty) values); + assert ( + expected_field_types + = List.map (fun (v : V.typed_value) -> v.V.ty) values); (* Construct the value *) - let av = { V.variant_id = opt_variant_id; V.field_values = values } in + let av : V.adt_value = + { V.variant_id = opt_variant_id; V.field_values = values } + in let aty = T.Adt (T.AdtId def_id, regions, types) in Ok (ctx, { V.value = Adt av; ty = aty })) @@ -2242,7 +2255,9 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx) (* Create and push the input variables *) let input_vars = - V.VarId.mapi_from1 (fun id v -> (mk_var id None v.V.ty, v)) args_vl + V.VarId.mapi_from1 + (fun id (v : V.typed_value) -> (mk_var id None v.V.ty, v)) + args_vl in let ctx = C.ctx_push_vars ctx input_vars in -- cgit v1.2.3