diff options
Diffstat (limited to 'compiler/InterpreterLoops.ml')
| -rw-r--r-- | compiler/InterpreterLoops.ml | 396 |
1 files changed, 369 insertions, 27 deletions
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 702420cd..08607deb 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -28,8 +28,38 @@ type cnt_thresholds = { sid : V.SymbolicValueId.id; bid : V.BorrowId.id; did : C.DummyVarId.id; + rid : T.RegionId.id; } +(* TODO: document. + TODO: we might not use the bounds properly, use sets instead. + TODO: actually, bounds are good +*) +type match_ctx = { + ctx : C.eval_ctx; + aids : V.AbstractionId.Set.t; + sids : V.SymbolicValueId.Set.t; + bids : V.BorrowId.Set.t; +} + +let mk_match_ctx (ctx : C.eval_ctx) : match_ctx = + let aids = V.AbstractionId.Set.empty in + let sids = V.SymbolicValueId.Set.empty in + let bids = V.BorrowId.Set.empty in + { ctx; aids; sids; bids } + +type updt_env_kind = + | EndAbsInSrc of V.AbstractionId.id + | EndBorrowsInSrc of V.BorrowId.Set.t + | EndBorrowInSrc of V.BorrowId.id + | EndBorrowInTgt of V.BorrowId.id + | EndBorrowsInTgt of V.BorrowId.Set.t + +(** Utility exception *) +exception ValueMatchFailure of updt_env_kind + +type joined_ctx_or_update = (match_ctx, updt_env_kind) result + (** Union Find *) module UnionFind = UF.Make (UF.StoreMap) @@ -248,26 +278,328 @@ let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds) (* Return the new context *) !ctx -(* TODO: document. - TODO: we might not use the bounds properly, use sets instead. -*) -type match_ctx = { - ctx : C.eval_ctx; - aids : V.AbstractionId.Set.t; - sids : V.SymbolicValueId.Set.t; - bids : V.BorrowId.Set.t; -} +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 mk_match_ctx (ctx : C.eval_ctx) : match_ctx = - let aids = V.AbstractionId.Set.empty in - let sids = V.SymbolicValueId.Set.empty in - let bids = V.BorrowId.Set.empty in - { ctx; aids; sids; bids } +(** This function raises exceptions of kind {!ValueMatchFailue}. + + [convertible]: the function updates it to [false] if the result of the + merge is not the result of an alpha-conversion. For instance, if we + match two primitive values which are not equal, and thus introduce a + symbolic value for the result: + {[ + 0 : u32, 1 : u32 ~~> s : u32 where s fresh + ]} + *) +let rec match_typed_values (config : C.config) (thresh : cnt_thresholds) + (convertible : bool ref) (rid_map : T.RegionId.InjSubst.t ref) + (bid_map : V.BorrowId.InjSubst.t ref) + (sid_map : V.SymbolicValueId.InjSubst.t ref) (ctx : C.eval_ctx) + (v0 : V.typed_value) (v1 : V.typed_value) : V.typed_value = + let match_rec = + match_typed_values config thresh convertible rid_map bid_map sid_map ctx + in + let lookup_bid (id : V.BorrowId.id) : V.BorrowId.id = + V.BorrowId.InjSubst.find_with_default id id !bid_map + in + let lookup_bids (ids : V.BorrowId.Set.t) : V.BorrowId.Set.t = + V.BorrowId.Set.map lookup_bid ids + in + let map_bid (id0 : V.BorrowId.id) (id1 : V.BorrowId.id) : V.BorrowId.id = + assert (V.BorrowId.Ord.compare id0 thresh.bid >= 0); + assert (V.BorrowId.Ord.compare id1 thresh.bid >= 0); + assert (not (V.BorrowId.InjSubst.mem id0 !bid_map)); + bid_map := V.BorrowId.InjSubst.add id0 id1 !bid_map; + id1 + in + let lookup_sid (id : V.SymbolicValueId.id) : V.SymbolicValueId.id = + match V.SymbolicValueId.InjSubst.find_opt id !sid_map with + | None -> id + | Some id -> id + in + assert (v0.V.ty = v1.V.ty); + match (v0.V.value, v1.V.value) with + | V.Primitive pv0, V.Primitive pv1 -> + if pv0 = pv1 then v1 else raise (Failure "Unimplemented") + | V.Adt av0, V.Adt 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_rec f0 f1) fields in + let value : V.value = + V.Adt { variant_id = av0.variant_id; field_values } + in + { V.value; ty = v1.V.ty } + else ( + convertible := false; + (* For now, we don't merge values which contain borrows *) + (* TODO: *) + raise (Failure "Unimplemented")) + | Bottom, Bottom -> v1 + | Borrow bc0, Borrow bc1 -> + let bc = + match (bc0, bc1) with + | SharedBorrow (mv0, bid0), SharedBorrow (mv1, bid1) -> + let bid0 = lookup_bid bid0 in + (* Not completely sure what to do with the meta-value. If a shared + symbolic value gets expanded in a branch, it may be simplified + (by being folded back to a symbolic value) upon doing the join, + which as a result would lead to code where it is considered as + mutable (which is sound). On the other hand, if we access a + symbolic value in a loop, the translated loop should take it as + input anyway, so maybe this actually leads to equivalent + code. + *) + let mv = match_rec mv0 mv1 in + let bid = if bid0 = bid1 then bid1 else map_bid bid0 bid1 in + V.SharedBorrow (mv, bid) + | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) -> + let bid0 = lookup_bid bid0 in + let bv = match_rec bv0 bv1 in + let bid = if bid0 = bid1 then bid1 else map_bid bid0 bid1 in + V.MutBorrow (bid, bv) + | ReservedMutBorrow _, _ + | _, ReservedMutBorrow _ + | SharedBorrow _, MutBorrow _ + | MutBorrow _, SharedBorrow _ -> + (* If we get here, either there is a typing inconsistency, or we are + trying to match a reserved borrow, which shouldn't happen because + reserved borrow should be eliminated very quickly - they are introduced + just before function calls which activate them *) + raise (Failure "Unexpected") + in + { V.value = V.Borrow bc; V.ty = v1.V.ty } + | Loan lc0, Loan lc1 -> + (* TODO: maybe we should enforce that the ids are always exactly the same - + without matching *) + let lc = + match (lc0, lc1) with + | SharedLoan (ids0, sv0), SharedLoan (ids1, sv1) -> + let ids0 = lookup_bids ids0 in + (* Not sure what to do if the ids don't match *) + let ids = + if ids0 = ids1 then ids1 else raise (Failure "Unimplemented") + in + let sv = match_rec sv0 sv1 in + V.SharedLoan (ids, sv) + | MutLoan id0, MutLoan id1 -> + let id0 = lookup_bid id0 in + let id = if id0 = id1 then id1 else map_bid id0 id1 in + V.MutLoan id + | SharedLoan _, MutLoan _ | MutLoan _, SharedLoan _ -> + raise (Failure "Unreachable") + in + { V.value = Loan lc; ty = v1.V.ty } + | Symbolic sv0, Symbolic sv1 -> + (* 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 (EndBorrowsInSrc ids)) + | MutLoan id -> raise (ValueMatchFailure (EndBorrowInSrc id))) + | _, Loan lc -> ( + match lc with + | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInTgt ids)) + | MutLoan id -> raise (ValueMatchFailure (EndBorrowInTgt id))) + | Symbolic _, _ -> raise (Failure "Unimplemented") + | _, Symbolic _ -> raise (Failure "Unimplemented") + | _ -> raise (Failure "Unreachable") + +(*(** This function raises exceptions of kind {!ValueMatchFailue} *) + let rec match_typed_avalues (config : C.config) (thresh : cnt_thresholds) + (rid_map : T.RegionId.InjSubst.t ref) (bid_map : V.BorrowId.InjSubst.t ref) + (sid_map : V.SymbolicValueId.InjSubst.t ref) + (aid_map : V.AbstractionId.InjSubst.t ref) (ctx : C.eval_ctx) + (v0 : V.typed_avalue) (v1 : V.typed_avalue) : V.typed_avalue = + let match_rec = + match_typed_avalues config thresh rid_map bid_map sid_map ctx + in + (* TODO: factorize those helpers with [match_typed_values] (write a functor?) *) + let lookup_bid (id : V.BorrowId.id) : V.BorrowId.id = + V.BorrowId.InjSubst.find_with_default id id !bid_map + in + let lookup_bids (ids : V.BorrowId.Set.t) : V.BorrowId.Set.t = + V.BorrowId.Set.map lookup_bid ids + in + let map_bid (id0 : V.BorrowId.id) (id1 : V.BorrowId.id) : V.BorrowId.id = + assert (V.BorrowId.Ord.compare id0 thresh.bid >= 0); + assert (V.BorrowId.Ord.compare id1 thresh.bid >= 0); + assert (not (V.BorrowId.InjSubst.mem id0 !bid_map)); + bid_map := V.BorrowId.InjSubst.add id0 id1 !bid_map; + id1 + in + let lookup_sid (id : V.SymbolicValueId.id) : V.SymbolicValueId.id = + match V.SymbolicValueId.InjSubst.find_opt id !sid_map with + | None -> id + | Some id -> id + in + assert (v0.V.ty = v1.V.ty); + match (v0.V.value, v1.V.value) with + | V.APrimitive pv0, V.APrimitive pv1 -> + if pv0 = pv1 then v1 else raise (Failure "Unimplemented") + | 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_rec f0 f1) fields in + let value : V.value = + V.Adt { variant_id = av0.variant_id; field_values } + in + { V.value; ty = v1.V.ty } + else raise (Failure "Unimplemented") + | Bottom, Bottom -> v1 + | Borrow bc0, Borrow bc1 -> + let bc = + match (bc0, bc1) with + | SharedBorrow (mv0, bid0), SharedBorrow (mv1, bid1) -> + let bid0 = lookup_bid bid0 in + (* Not completely sure what to do with the meta-value. If a shared + symbolic value gets expanded in a branch, it may be simplified + (by being folded back to a symbolic value) upon doing the join, + which as a result would lead to code where it is considered as + mutable (which is sound). On the other hand, if we access a + symbolic value in a loop, the translated loop should take it as + input anyway, so maybe this actually leads to equivalent + code. + *) + let mv = match_rec mv0 mv1 in + let bid = if bid0 = bid1 then bid1 else map_bid bid0 bid1 in + V.SharedBorrow (mv, bid) + | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) -> + let bid0 = lookup_bid bid0 in + let bv = match_rec bv0 bv1 in + let bid = if bid0 = bid1 then bid1 else map_bid bid0 bid1 in + V.MutBorrow (bid, bv) + | ReservedMutBorrow _, _ + | _, ReservedMutBorrow _ + | SharedBorrow _, MutBorrow _ + | MutBorrow _, SharedBorrow _ -> + (* If we get here, either there is a typing inconsistency, or we are + trying to match a reserved borrow, which shouldn't happen because + reserved borrow should be eliminated very quickly - they are introduced + just before function calls which activate them *) + raise (Failure "Unexpected") + in + { V.value = V.Borrow bc; V.ty = v1.V.ty } + | Loan lc0, Loan lc1 -> + (* TODO: maybe we should enforce that the ids are always exactly the same - + without matching *) + let lc = + match (lc0, lc1) with + | SharedLoan (ids0, sv0), SharedLoan (ids1, sv1) -> + let ids0 = lookup_bids ids0 in + (* Not sure what to do if the ids don't match *) + let ids = + if ids0 = ids1 then ids1 else raise (Failure "Unimplemented") + in + let sv = match_rec sv0 sv1 in + V.SharedLoan (ids, sv) + | MutLoan id0, MutLoan id1 -> + let id0 = lookup_bid id0 in + let id = if id0 = id1 then id1 else map_bid id0 id1 in + V.MutLoan id + | SharedLoan _, MutLoan _ | MutLoan _, SharedLoan _ -> + raise (Failure "Unreachable") + in + { V.value = Loan lc; ty = v1.V.ty } + | Symbolic sv0, Symbolic sv1 -> + (* 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 (EndBorrowsInSrc ids)) + | MutLoan id -> raise (ValueMatchFailure (EndBorrowInSrc id))) + | _, Loan lc -> ( + match lc with + | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInTgt ids)) + | MutLoan id -> raise (ValueMatchFailure (EndBorrowInTgt id))) + | _ -> raise (Failure "Unreachable")*) + +(** Apply substitutions in the first abstraction, then merge the abstractions together. *) +let subst_merge_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds) + (rid_map : T.RegionId.InjSubst.t) (bid_map : V.BorrowId.InjSubst.t) + (sid_map : V.SymbolicValueId.InjSubst.t) (ctx : C.eval_ctx) (abs0 : V.abs) + (abs1 : V.abs) : V.abs = + (* Apply the substitutions in the first abstraction *) + let rsubst id = + assert (T.RegionId.Ord.compare id thresh.rid >= 0); + T.RegionId.InjSubst.find_with_default id id rid_map + in + let rvsubst id = id in + let tsubst id = id in + let ssubst id = + assert (V.SymbolicValueId.Ord.compare id thresh.sid >= 0); + V.SymbolicValueId.InjSubst.find_with_default id id sid_map + in + let bsubst id = + assert (V.BorrowId.Ord.compare id thresh.bid >= 0); + V.BorrowId.InjSubst.find_with_default id id bid_map + in + let asubst id = id in + let abs0 = + Substitute.abs_subst_ids rsubst rvsubst tsubst ssubst bsubst asubst abs0 + in -type joined_ctx_or_update = - | EndAbs of V.AbstractionId.id - | EndBorrow of V.BorrowId.id - | JoinedCtx of match_ctx + (* Merge the two abstractions *) + let abs_kind = V.Loop loop_id in + let can_end = false in + merge_abstractions abs_kind can_end ctx abs0 abs1 (** Merge a borrow with the abstraction containing the associated loan, where the abstraction must be a *loop abstraction* (we don't synthesize code during @@ -306,8 +638,10 @@ let rec merge_borrows_with_parent_loop_abs (config : C.config) (* TODO: we probably don't need an [match_ctx], and actually we might not use the bounds propertly. + TODO: remove *) -let match_ctx_with_target (config : C.config) (tgt_mctx : match_ctx) : cm_fun = +let match_ctx_with_target_old (config : C.config) (tgt_mctx : match_ctx) : + cm_fun = fun cf src_ctx -> (* We first reorganize [ctx] so that we can match it with [tgt_mctx] *) (* First, collect all the borrows and abstractions which are in [ctx] @@ -351,12 +685,12 @@ let loop_join_entry_ctx_with_continue_ctx (ctx0 : match_ctx) (ctx1 : C.eval_ctx) let rec loop_join_entry_ctx_with_continue_ctxs (ctx0 : match_ctx) (ctxs : C.eval_ctx list) : joined_ctx_or_update = match ctxs with - | [] -> JoinedCtx ctx0 + | [] -> Ok ctx0 | ctx1 :: ctxs -> ( let res = loop_join_entry_ctx_with_continue_ctx ctx0 ctx1 in match res with - | EndAbs _ | EndBorrow _ -> res - | JoinedCtx ctx0 -> loop_join_entry_ctx_with_continue_ctxs ctx0 ctxs) + | Error _ -> res + | Ok ctx0 -> loop_join_entry_ctx_with_continue_ctxs ctx0 ctxs) let compute_loop_entry_fixed_point (config : C.config) (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : match_ctx = @@ -416,17 +750,25 @@ let compute_loop_entry_fixed_point (config : C.config) (* Check if the join succeeded, or if we need to end abstractions/borrows in the original environment first *) match join_ctxs mctx with - | EndAbs id -> + | Error (EndAbsInSrc id) -> let ctx1 = InterpreterBorrows.end_abstraction_no_synth config id mctx.ctx in eval_iteration_then_join { mctx with ctx = ctx1 } - | EndBorrow id -> + | Error (EndBorrowInSrc id) -> let ctx1 = InterpreterBorrows.end_borrow_no_synth config id mctx.ctx in eval_iteration_then_join { mctx with ctx = ctx1 } - | JoinedCtx mctx1 -> + | Error (EndBorrowsInSrc ids) -> + let ctx1 = + InterpreterBorrows.end_borrows_no_synth config ids mctx.ctx + in + eval_iteration_then_join { mctx with ctx = ctx1 } + | Error (EndBorrowInTgt _ | EndBorrowsInTgt _) -> + (* Shouldn't happen here *) + raise (Failure "Unreachable") + | Ok mctx1 -> (* The join succeeded: check if we reached a fixed point, otherwise iterate *) if equiv_ctxs mctx mctx1 then mctx1 @@ -487,7 +829,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : (* Compute the fixed point at the loop entrance *) let mctx = compute_loop_entry_fixed_point config eval_loop_body ctx in (* Synthesize the end of the function *) - let end_expr = match_ctx_with_target config mctx (cf EndEnterLoop) ctx in + let end_expr = match_ctx_with_target_old config mctx (cf EndEnterLoop) ctx in (* Synthesize the loop body by evaluating it, with the continuation for after the loop starting at the *fixed point*, but with a special treatment for the [Break] and [Continue] cases *) @@ -502,7 +844,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : | Continue i -> (* We don't support nested loops for now *) assert (i = 0); - match_ctx_with_target config mctx (cf EndContinue) ctx + match_ctx_with_target_old config mctx (cf EndContinue) ctx | Unit | EndEnterLoop | EndContinue -> (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}. For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now. |