diff options
| -rw-r--r-- | compiler/InterpreterLoops.ml | 163 |
1 files changed, 102 insertions, 61 deletions
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 002abfb5..b159ab58 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -349,40 +349,41 @@ let collapse_ctx (loop_id : V.LoopId.id) (* Return the new context *) !ctx -let rec match_types (check_regions : 'r -> 'r -> unit) (ctx : C.eval_ctx) - (ty0 : 'r T.ty) (ty1 : 'r T.ty) : unit = - let match_rec = match_types check_regions ctx in - match (ty0, ty1) with - | Adt (id0, regions0, tys0), Adt (id1, regions1, tys1) -> - assert (id0 = id1); - List.iter - (fun (id0, id1) -> check_regions id0 id1) - (List.combine regions0 regions1); - List.iter (fun (ty0, ty1) -> match_rec ty0 ty1) (List.combine tys0 tys1) - | TypeVar vid0, TypeVar vid1 -> assert (vid0 = vid1) - | Bool, Bool | Char, Char | Never, Never | Str, Str -> () - | Integer int_ty0, Integer int_ty1 -> assert (int_ty0 = int_ty1) - | Array ty0, Array ty1 | Slice ty0, Slice ty1 -> match_rec ty0 ty1 - | Ref (r0, ty0, k0), Ref (r1, ty1, k1) -> - check_regions r0 r1; - match_rec ty0 ty1; - assert (k0 = k1) - | _ -> raise (Failure "Unreachable") +(*(** Match two types during a join. This simply performs a sanity check. *) + let rec match_types (check_regions : 'r -> 'r -> unit) (ctx : C.eval_ctx) + (ty0 : 'r T.ty) (ty1 : 'r T.ty) : unit = + let match_rec = match_types check_regions ctx in + match (ty0, ty1) with + | Adt (id0, regions0, tys0), Adt (id1, regions1, tys1) -> + assert (id0 = id1); + List.iter + (fun (id0, id1) -> check_regions id0 id1) + (List.combine regions0 regions1); + List.iter (fun (ty0, ty1) -> match_rec ty0 ty1) (List.combine tys0 tys1) + | TypeVar vid0, TypeVar vid1 -> assert (vid0 = vid1) + | Bool, Bool | Char, Char | Never, Never | Str, Str -> () + | Integer int_ty0, Integer int_ty1 -> assert (int_ty0 = int_ty1) + | Array ty0, Array ty1 | Slice ty0, Slice ty1 -> match_rec ty0 ty1 + | Ref (r0, ty0, k0), Ref (r1, ty1, k1) -> + check_regions r0 r1; + match_rec ty0 ty1; + assert (k0 = k1) + | _ -> raise (Failure "Unreachable") -let match_rtypes (rid_map : T.RegionId.InjSubst.t ref) (ctx : C.eval_ctx) - (ty0 : T.rty) (ty1 : T.rty) : unit = - let lookup_rid (id : T.RegionId.id) : T.RegionId.id = - T.RegionId.InjSubst.find_with_default id id !rid_map - in - let check_regions r0 r1 = - match (r0, r1) with - | T.Static, T.Static -> () - | T.Var id0, T.Var id1 -> - let id0 = lookup_rid id0 in - assert (id0 = id1) - | _ -> raise (Failure "Unexpected") - in - match_types check_regions ctx ty0 ty1 + let match_rtypes (rid_map : T.RegionId.InjSubst.t ref) (ctx : C.eval_ctx) + (ty0 : T.rty) (ty1 : T.rty) : unit = + let lookup_rid (id : T.RegionId.id) : T.RegionId.id = + T.RegionId.InjSubst.find_with_default id id !rid_map + in + let check_regions r0 r1 = + match (r0, r1) with + | T.Static, T.Static -> () + | T.Var id0, T.Var id1 -> + let id0 = lookup_rid id0 in + assert (id0 = id1) + | _ -> raise (Failure "Unexpected") + in + match_types check_regions ctx ty0 ty1 *) (** See {!Match} *) module type Matcher = sig @@ -427,6 +428,16 @@ module type Matcher = sig (** There are no constraints on the input symbolic values *) val match_symbolic_values : V.symbolic_value -> V.symbolic_value -> V.symbolic_value + + (** Match a symbolic value with a value which is not symbolic. + + If the boolean is [true], it means the symbolic value comes from the + left environment. Otherwise it comes from the right environment (it + is important when throwing exceptions, for instance when we need to + end loans in one of the two environments). + *) + val match_symbolic_with_other : + bool -> V.symbolic_value -> V.typed_value -> V.typed_value end (** Generic functor to implement matching functions between values, environments, @@ -514,24 +525,13 @@ module Match (M : Matcher) = struct in { V.value = Loan lc; ty = v1.V.ty } | Symbolic sv0, Symbolic sv1 -> + (* For now, we force all the symbolic values containing borrows to + be eagerly expanded, and we don't support nested borrows *) + assert (not (value_has_borrows ctx v0.V.value)); + assert (not (value_has_borrows ctx v1.V.value)); + (* Match *) let sv = M.match_symbolic_values sv0 sv1 in { v1 with V.value = V.Symbolic sv } - (* (* TODO: id check mapping *) - let id0 = lookup_sid sv0.sv_id in - let id1 = sv1.sv_id in - if id0 = id1 then ( - assert (sv0.sv_kind = sv1.sv_kind); - (* Sanity check: the types should be the same *) - match_rtypes rid_map ctx sv0.sv_ty sv1.sv_ty; - (* Return *) - v1) - else ( - (* For now, we force all the symbolic values containing borrows to - be eagerly expanded, and we don't support nested borrows *) - assert (not (value_has_borrows ctx v0.V.value)); - assert (not (value_has_borrows ctx v1.V.value)); - raise (Failure "Unimplemented") - *) | Loan lc, _ -> ( match lc with | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids)) @@ -540,9 +540,13 @@ module Match (M : Matcher) = struct match lc with | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids)) | MutLoan id -> raise (ValueMatchFailure (LoanInRight id))) - | Symbolic _, _ -> raise (Failure "Unimplemented") - | _, Symbolic _ -> raise (Failure "Unimplemented") + | Symbolic sv, _ -> M.match_symbolic_with_other true sv v1 + | _, Symbolic sv -> M.match_symbolic_with_other false sv v0 | _ -> raise (Failure "Unreachable") + + and match_typed_avalues (ctx : C.eval_ctx) (v0 : V.typed_avalue) + (v1 : V.typed_avalue) : V.typed_avalue = + raise (Failure "Unreachable") end (* Very annoying: functors only take modules as inputs... *) @@ -708,9 +712,11 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct let match_shared_loans (ty : T.ety) (ids0 : V.loan_id_set) (ids1 : V.loan_id_set) (sv : V.typed_value) : V.loan_id_set * V.typed_value = - (* Check if the ids are the same - Rem.: we forbid the loans to a value - to vary. However, we allow to dive inside a data-structure: in this - case, + (* Check if the ids are the same - Rem.: we forbid the sets of loans + to be different. However, if we dive inside data-structures (by + using a shared borrow) the shared values might themselves contain + shared loans, which need to be matched. For this reason, we destructure + the shared values (see {!destructure_abs}). *) let extra_ids_left = V.BorrowId.Set.diff ids0 ids1 in let extra_ids_right = V.BorrowId.Set.diff ids1 ids0 in @@ -719,17 +725,52 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct if not (V.BorrowId.Set.is_empty extra_ids_right) then raise (ValueMatchFailure (LoansInRight extra_ids_right)); - (* *) - raise (Failure "Unimplemented") + (* This should always be true if we get here *) + assert (ids0 = ids1); + let ids = ids0 in - let match_mut_loans (ty : T.ety) (id0 : V.loan_id) (id1 : V.loan_id) : - V.loan_id = - raise (Failure "Unimplemented") + (* Return *) + (ids, sv) + + let match_mut_loans (_ : T.ety) (id0 : V.loan_id) (_ : V.loan_id) : V.loan_id + = + id0 - (** There are no constraints on the input symbolic values *) let match_symbolic_values (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : V.symbolic_value = - raise (Failure "Unimplemented") + let id0 = sv0.sv_id in + let id1 = sv1.sv_id in + if id0 = id1 then ( + (* Sanity check *) + assert (sv0 = sv1); + (* Return *) + sv0) + else ( + (* The caller should have checked that the symbolic values don't contain + borrows *) + assert (not (ty_has_borrows S.ctx.type_context.type_infos sv0.sv_ty)); + (* We simply introduce a fresh symbolic value *) + mk_fresh_symbolic_value V.LoopJoin sv0.sv_ty) + + let match_symbolic_with_other (left : bool) (sv : V.symbolic_value) + (v : V.typed_value) : V.typed_value = + (* Check that: + - there are no borrows in the symbolic value + - there are no borrows in the "regular" value + If there are loans in the regular value, raise an exception. + *) + assert (not (ty_has_borrows S.ctx.type_context.type_infos sv.sv_ty)); + assert (not (value_has_borrows S.ctx v.V.value)); + (match InterpreterBorrowsCore.get_first_loan_in_value v with + | None -> () + | Some (SharedLoan (ids, _)) -> + if left then raise (ValueMatchFailure (LoansInLeft ids)) + else raise (ValueMatchFailure (LoansInRight ids)) + | Some (MutLoan id) -> + if left then raise (ValueMatchFailure (LoanInLeft id)) + else raise (ValueMatchFailure (LoanInRight id))); + (* Return a fresh symbolic value *) + mk_fresh_symbolic_typed_value V.LoopJoin sv.sv_ty end (* |