summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/InterpreterLoops.ml163
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
(*