diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 3 | ||||
| -rw-r--r-- | src/InterpreterProjectors.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 2 | ||||
| -rw-r--r-- | src/Invariants.ml | 36 | ||||
| -rw-r--r-- | src/Print.ml | 4 | ||||
| -rw-r--r-- | src/TypesUtils.ml | 2 | ||||
| -rw-r--r-- | src/Values.ml | 6 |
7 files changed, 42 insertions, 15 deletions
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index ccc259f5..6e09c90c 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -128,7 +128,8 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) assert (Option.is_none !abs_or_var); if ek.enter_abs then ( abs_or_var := Some (AbsId abs.V.abs_id); - super#visit_Abs env abs) + super#visit_Abs env abs; + abs_or_var := None) else () end in diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index 105adb5a..dfc821de 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -275,6 +275,8 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t) in (V.AAdt { V.variant_id; field_values }, original_sv_ty) | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) -> + (* Sanity check *) + assert (spc.V.svalue.V.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) let child_av = mk_aproj_loans_from_proj_comp spc in (* Check if the region is in the set of projected regions (note that @@ -286,6 +288,8 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t) (* Not in the set: ignore *) (V.ALoan (V.AIgnoredMutLoan (bid, child_av)), ref_ty) | SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) -> + (* Sanity check *) + assert (spc.V.svalue.V.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) let child_av = mk_aproj_loans_from_proj_comp spc in (* Check if the region is in the set of projected regions (note that diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index f0e3d420..458c11b4 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -21,6 +21,8 @@ let rty_to_string = Print.EvalCtxCfimAst.rty_to_string let typed_value_to_string = Print.EvalCtxCfimAst.typed_value_to_string +let typed_avalue_to_string = Print.EvalCtxCfimAst.typed_avalue_to_string + let place_to_string = Print.EvalCtxCfimAst.place_to_string let operand_to_string = Print.EvalCtxCfimAst.operand_to_string diff --git a/src/Invariants.ml b/src/Invariants.ml index be3260be..b723d861 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -8,6 +8,7 @@ module C = Contexts module Subst = Substitute module A = CfimAst module L = Logging +open TypesUtils open InterpreterUtils open InterpreterBorrowsCore @@ -341,6 +342,18 @@ let check_constant_value_type (cv : V.constant_value) (ty : T.ety) : unit = | _ -> failwith "Erroneous typing" let check_typing_invariant (ctx : C.eval_ctx) : unit = + (* TODO: the type of aloans doens't make sense: they have a type + * of the shape `& (mut) T` where they should have type `T`... + * This messes a bit the type invariant checks when checking the + * children. In order to isolate the problem (for future modifications) + * we introduce function, so that we can easily spot all the involved + * places. + * *) + let aloan_get_expected_child_type (ty : 'r T.ty) : 'r T.ty = + let _, ty, _ = ty_get_ref ty in + ty + in + let visitor = object inherit [_] C.iter_eval_ctx as super @@ -496,31 +509,30 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = match lc with | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (bid, child_av) -> ( - L.log#ldebug - (lazy - ("- child_av.ty: " - ^ rty_to_string ctx child_av.V.ty - ^ "\n- aty: " ^ rty_to_string ctx aty)); - assert (child_av.V.ty = aty); + let borrowed_aty = aloan_get_expected_child_type aty in + assert (child_av.V.ty = borrowed_aty); (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow ek_all bid ctx in match glc with | Concrete (V.MutBorrow (_, bv)) -> - assert (bv.V.ty = Subst.erase_regions aty) + assert (bv.V.ty = Subst.erase_regions borrowed_aty) | Abstract (V.AMutBorrow (_, sv)) -> assert ( - Subst.erase_regions sv.V.ty = Subst.erase_regions aty) + Subst.erase_regions sv.V.ty + = Subst.erase_regions borrowed_aty) | _ -> failwith "Inconsistent context") | V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av) -> let ty = Subst.erase_regions aty in assert (sv.V.ty = ty); - assert (child_av.V.ty = aty) + (* TODO: the type of aloans doesn't make sense, see above *) + assert (child_av.V.ty = aloan_get_expected_child_type aty) | V.AEndedMutLoan { given_back; child } | V.AEndedIgnoredMutLoan { given_back; child } -> - assert (given_back.V.ty = aty); - assert (child.V.ty = aty) - | V.AIgnoredSharedLoan child_av -> assert (child_av.V.ty = aty)) + assert (given_back.V.ty = aloan_get_expected_child_type aty); + assert (child.V.ty = aloan_get_expected_child_type aty) + | V.AIgnoredSharedLoan child_av -> + assert (child_av.V.ty = aloan_get_expected_child_type aty)) | V.ASymbolic aproj, ty -> let ty1 = Subst.erase_regions ty in let ty2 = diff --git a/src/Print.ml b/src/Print.ml index e751d0a3..0b436f1a 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -981,6 +981,10 @@ module EvalCtxCfimAst = struct let fmt = PC.eval_ctx_to_ctx_formatter ctx in PV.typed_value_to_string fmt v + let typed_avalue_to_string (ctx : C.eval_ctx) (v : V.typed_avalue) : string = + let fmt = PC.eval_ctx_to_ctx_formatter ctx in + PV.typed_avalue_to_string fmt v + let place_to_string (ctx : C.eval_ctx) (op : E.place) : string = let fmt = PA.eval_ctx_to_ast_formatter ctx in PA.place_to_string fmt op diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml index a658adce..04a579bf 100644 --- a/src/TypesUtils.ml +++ b/src/TypesUtils.ml @@ -32,7 +32,7 @@ let ty_get_box (box_ty : ety) : ety = (** Deconstruct a type of the form `&T` or `&mut T` to retrieve the `T` (and the borrow kind, etc.) *) -let ty_get_ref (ty : ety) : erased_region * ety * ref_kind = +let ty_get_ref (ty : 'r ty) : 'r * 'r ty * ref_kind = match ty with | Ref (r, ty, ref_kind) -> (r, ty, ref_kind) | _ -> failwith "Not a ref type" diff --git a/src/Values.ml b/src/Values.ml index ac4145eb..47bdda23 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -518,7 +518,11 @@ and aborrow_content = *) (* TODO: we may want to merge this with typed_value - would prevent some issues - when accessing fields... *) + when accessing fields.... + + TODO: the type of avalues doesn't make sense for loan avalues: they currently + are typed as `& (mut) T` instead of `T`... +*) and typed_avalue = { value : avalue; ty : rty } [@@deriving show, |