summaryrefslogtreecommitdiff
path: root/compiler/InterpreterLoops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterLoops.ml')
-rw-r--r--compiler/InterpreterLoops.ml193
1 files changed, 186 insertions, 7 deletions
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index b159ab58..00e6eb01 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -415,7 +415,12 @@ module type Matcher = sig
V.typed_value ->
V.borrow_id * V.typed_value
- (** The shared value is the result of a match *)
+ (** Parameters:
+ [ty]
+ [ids0]
+ [ids1]
+ [v]: the result of matching the shared values coming from the two loans
+ *)
val match_shared_loans :
T.ety ->
V.loan_id_set ->
@@ -438,6 +443,93 @@ module type Matcher = sig
*)
val match_symbolic_with_other :
bool -> V.symbolic_value -> V.typed_value -> V.typed_value
+
+ (** The input ADTs don't have the same variant *)
+ val match_distinct_aadts :
+ T.rty -> V.adt_avalue -> T.rty -> V.adt_avalue -> V.typed_avalue
+
+ (** Parameters:
+ [ty0]
+ [bid0]
+ [ty1]
+ [bid1]
+ *)
+ val match_ashared_borrows :
+ T.rty -> V.borrow_id -> T.rty -> V.borrow_id -> V.typed_avalue
+
+ (** Parameters:
+ [ty0]
+ [mv0]
+ [bid0]
+ [av0]
+ [ty1]
+ [mv1]
+ [bid1]
+ [av1]
+ [mv]: result of matching mv0 and mv1
+ [av]: result of matching av0 and av1
+ *)
+ val match_amut_borrows :
+ T.rty ->
+ V.mvalue ->
+ V.borrow_id ->
+ V.typed_avalue ->
+ T.rty ->
+ V.mvalue ->
+ V.borrow_id ->
+ V.typed_avalue ->
+ V.mvalue ->
+ V.typed_avalue ->
+ V.typed_avalue
+
+ (** Parameters:
+ [ty0]
+ [ids0]
+ [v0]
+ [av0]
+ [ty1]
+ [ids1]
+ [v1]
+ [av1]
+ [v]: result of matching v0 and v1
+ [av]: result of matching av0 and av1
+ *)
+ val match_ashared_loans :
+ T.rty ->
+ V.loan_id_set ->
+ V.typed_value ->
+ V.typed_avalue ->
+ T.rty ->
+ V.loan_id_set ->
+ V.typed_value ->
+ V.typed_avalue ->
+ V.typed_value ->
+ V.typed_avalue ->
+ V.typed_avalue
+
+ (** Parameters:
+ [ty0]
+ [id0]
+ [av0]
+ [ty1]
+ [id1]
+ [av1]
+ [av]: result of matching av0 and av1
+ *)
+ val match_amut_loans :
+ T.rty ->
+ V.borrow_id ->
+ V.typed_avalue ->
+ T.rty ->
+ V.borrow_id ->
+ V.typed_avalue ->
+ V.typed_avalue ->
+ V.typed_avalue
+
+ (** Match two arbitrary avalues whose constructors don't match (this function
+ is typically used to raise the proper exception).
+ *)
+ val match_avalues : V.typed_avalue -> V.typed_avalue -> V.typed_avalue
end
(** Generic functor to implement matching functions between values, environments,
@@ -473,7 +565,7 @@ module Match (M : Matcher) = struct
assert (not (value_has_borrows ctx v1.V.value));
(* Merge *)
M.match_distinct_adts v0.V.ty av0 av1)
- | Bottom, Bottom -> v1
+ | Bottom, Bottom -> v0
| Borrow bc0, Borrow bc1 ->
let bc =
match (bc0, bc1) with
@@ -546,7 +638,83 @@ module Match (M : Matcher) = struct
and match_typed_avalues (ctx : C.eval_ctx) (v0 : V.typed_avalue)
(v1 : V.typed_avalue) : V.typed_avalue =
- raise (Failure "Unreachable")
+ let match_rec = match_typed_values ctx in
+ let match_arec = match_typed_avalues ctx in
+ assert (v0.V.ty = v1.V.ty);
+ match (v0.V.value, v1.V.value) with
+ | V.APrimitive _, V.APrimitive _ ->
+ (* We simply ignore - those are actually not used *)
+ assert (v0.V.ty = v1.V.ty);
+ mk_aignored v0.V.ty
+ | V.AAdt av0, V.AAdt av1 ->
+ if av0.variant_id = av1.variant_id then
+ let fields = List.combine av0.field_values av1.field_values in
+ let field_values =
+ List.map (fun (f0, f1) -> match_arec f0 f1) fields
+ in
+ let value : V.avalue =
+ V.AAdt { variant_id = av0.variant_id; field_values }
+ in
+ { V.value; ty = v1.V.ty }
+ else (* Merge *)
+ M.match_distinct_aadts v0.V.ty av0 v1.V.ty av1
+ | ABottom, ABottom -> v0
+ | ABorrow bc0, ABorrow bc1 -> (
+ match (bc0, bc1) with
+ | ASharedBorrow bid0, ASharedBorrow bid1 ->
+ M.match_ashared_borrows v0.V.ty bid0 v1.V.ty bid1
+ | AMutBorrow (mv0, bid0, av0), AMutBorrow (mv1, bid1, av1) ->
+ (* Not sure what to do with the meta-value *)
+ let mv = match_rec mv0 mv1 in
+ let av = match_arec av0 av1 in
+ M.match_amut_borrows v0.V.ty mv0 bid0 av0 v1.V.ty mv1 bid1 av1 mv av
+ | AIgnoredMutBorrow _, AIgnoredMutBorrow _ ->
+ (* The abstractions are destructured: we shouldn't get there *)
+ raise (Failure "Unexpected")
+ | AProjSharedBorrow asb0, AProjSharedBorrow asb1 -> (
+ match (asb0, asb1) with
+ | [], [] ->
+ (* This case actually stands for ignored shared borrows, when
+ there are no nested borrows *)
+ v0
+ | _ ->
+ (* We should get there only if there are nested borrows *)
+ raise (Failure "Unexpected"))
+ | _ ->
+ (* TODO: getting there is not necessarily inconsistent (it may
+ just be because the environments don't match) so we may want
+ to call a specific function (which could raise the proper
+ exception).
+ Rem.: we shouldn't get to the ended borrow cases, because
+ an abstraction should never contain ended borrows unless
+ we are *currently* ending it, in which case we need
+ to completely end it before continuing.
+ *)
+ raise (Failure "Unexpected"))
+ | ALoan lc0, ALoan lc1 -> (
+ (* TODO: maybe we should enforce that the ids are always exactly the same -
+ without matching *)
+ match (lc0, lc1) with
+ | ASharedLoan (ids0, sv0, av0), ASharedLoan (ids1, sv1, av1) ->
+ let sv = match_rec sv0 sv1 in
+ let av = match_arec av0 av1 in
+ assert (not (value_has_borrows ctx sv.V.value));
+ M.match_ashared_loans v0.V.ty ids0 sv0 av0 v1.V.ty ids1 sv1 av1 sv
+ av
+ | AMutLoan (id0, av0), AMutLoan (id1, av1) ->
+ let av = match_arec av0 av1 in
+ M.match_amut_loans v0.V.ty id0 av0 v1.V.ty id1 av1 av
+ | AIgnoredMutLoan _, AIgnoredMutLoan _
+ | AIgnoredSharedLoan _, AIgnoredSharedLoan _ ->
+ (* Those should have been filtered when destructuring the abstractions -
+ they are necessary only when there are nested borrows *)
+ raise (Failure "Unreachable")
+ | _ -> raise (Failure "Unreachable"))
+ | ASymbolic _, ASymbolic _ ->
+ (* For now, we force all the symbolic values containing borrows to
+ be eagerly expanded, and we don't support nested borrows *)
+ raise (Failure "Unreachable")
+ | _ -> M.match_avalues v0 v1
end
(* Very annoying: functors only take modules as inputs... *)
@@ -709,7 +877,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
(* Return the new borrow *)
(bid2, sv)
- let match_shared_loans (ty : T.ety) (ids0 : V.loan_id_set)
+ let match_shared_loans (_ : 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 sets of loans
@@ -732,9 +900,13 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
(* Return *)
(ids, sv)
- let match_mut_loans (_ : T.ety) (id0 : V.loan_id) (_ : V.loan_id) : V.loan_id
- =
- id0
+ let match_mut_loans (_ : T.ety) (id0 : V.loan_id) (id1 : V.loan_id) :
+ V.loan_id =
+ if id0 = id1 then id0
+ else
+ (* We forbid this case for now: if we get there, we force to end
+ both borrows *)
+ raise (ValueMatchFailure (LoanInLeft id0))
let match_symbolic_values (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) :
V.symbolic_value =
@@ -771,6 +943,13 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
else raise (ValueMatchFailure (LoanInRight id)));
(* Return a fresh symbolic value *)
mk_fresh_symbolic_typed_value V.LoopJoin sv.sv_ty
+
+ let match_distinct_aadts _ _ _ _ = raise (Failure "Unreachable")
+ let match_ashared_borrows _ _ _ _ = raise (Failure "Unreachable")
+ let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable")
+ let match_ashared_loans _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable")
+ let match_amut_loans _ _ _ _ _ _ _ = raise (Failure "Unreachable")
+ let match_avalues _ _ = raise (Failure "Unreachable")
end
(*
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-12 08:30:44 +0000