diff options
Diffstat (limited to 'compiler/InterpreterLoopsCore.ml')
-rw-r--r-- | compiler/InterpreterLoopsCore.ml | 386 |
1 files changed, 386 insertions, 0 deletions
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml new file mode 100644 index 00000000..209fce1c --- /dev/null +++ b/compiler/InterpreterLoopsCore.ml @@ -0,0 +1,386 @@ +(** Core definitions for the [IntepreterLoops*] *) + +module T = Types +module PV = PrimitiveValues +module V = Values +module E = Expressions +module C = Contexts +module Subst = Substitute +module A = LlbcAst +module L = Logging +module Inv = Invariants +module S = SynthesizeSymbolic +module UF = UnionFind +open InterpreterUtils +open InterpreterExpressions + +type updt_env_kind = + | AbsInLeft of V.AbstractionId.id + | LoanInLeft of V.BorrowId.id + | LoansInLeft of V.BorrowId.Set.t + | AbsInRight of V.AbstractionId.id + | LoanInRight of V.BorrowId.id + | LoansInRight of V.BorrowId.Set.t + +(** Utility exception *) +exception ValueMatchFailure of updt_env_kind + +(** Utility exception *) +exception Distinct of string + +type ctx_or_update = (C.eval_ctx, updt_env_kind) result + +(** Union Find *) +module UnionFind = UF.Make (UF.StoreMap) + +(** A small utility - + + Rem.: some environments may be ill-formed (they may contain several times + the same loan or borrow - this happens for instance when merging + environments). This is the reason why we use sets in some places (for + instance, [borrow_to_abs] maps to a *set* of ids). +*) +type abs_borrows_loans_maps = { + abs_ids : V.AbstractionId.id list; + abs_to_borrows : V.BorrowId.Set.t V.AbstractionId.Map.t; + abs_to_loans : V.BorrowId.Set.t V.AbstractionId.Map.t; + abs_to_borrows_loans : V.BorrowId.Set.t V.AbstractionId.Map.t; + borrow_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t; + loan_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t; + borrow_loan_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t; +} + +(** See {!InterpreterLoopsMatchCtxs.MakeMatcher} and {!InterpreterLoopsCore.Matcher}. + + This module contains primitive match functions to instantiate the generic + {!InterpreterLoopsMatchCtxs.MakeMatcher} functor. + *) +module type PrimMatcher = sig + val match_etys : T.ety -> T.ety -> T.ety + val match_rtys : T.rty -> T.rty -> T.rty + + (** The input primitive values are not equal *) + val match_distinct_primitive_values : + T.ety -> V.primitive_value -> V.primitive_value -> V.typed_value + + (** The input ADTs don't have the same variant *) + val match_distinct_adts : T.ety -> V.adt_value -> V.adt_value -> V.typed_value + + (** The meta-value is the result of a match. + + We take an additional function as input, which acts as a matcher over + typed values, to be able to lookup the shared values and match them. + We do this for shared borrows (and not, e.g., mutable borrows) because + shared borrows introduce indirections, while mutable borrows carry the + borrowed values with them: we might want to explore and match those + borrowed values, in which case we have to manually look them up before + calling the match function. + *) + val match_shared_borrows : + (V.typed_value -> V.typed_value -> V.typed_value) -> + T.ety -> + V.borrow_id -> + V.borrow_id -> + V.borrow_id + + (** The input parameters are: + - [ty] + - [bid0]: first borrow id + - [bv0]: first borrowed value + - [bid1] + - [bv1] + - [bv]: the result of matching [bv0] with [bv1] + *) + val match_mut_borrows : + T.ety -> + V.borrow_id -> + V.typed_value -> + V.borrow_id -> + V.typed_value -> + V.typed_value -> + V.borrow_id * V.typed_value + + (** 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 -> + V.loan_id_set -> + V.typed_value -> + V.loan_id_set * V.typed_value + + val match_mut_loans : T.ety -> V.loan_id -> V.loan_id -> V.loan_id + + (** 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 + + (** Match a bottom value with a value which is not bottom. + + If the boolean is [true], it means the bottom 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_bottom_with_other : bool -> 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 -> T.rty -> V.typed_avalue + + (** Parameters: + [ty0] + [bid0] + [ty1] + [bid1] + [ty]: result of matching ty0 and ty1 + *) + val match_ashared_borrows : + T.rty -> V.borrow_id -> T.rty -> V.borrow_id -> T.rty -> V.typed_avalue + + (** Parameters: + [ty0] + [bid0] + [av0] + [ty1] + [bid1] + [av1] + [ty]: result of matching ty0 and ty1 + [av]: result of matching av0 and av1 + *) + val match_amut_borrows : + T.rty -> + V.borrow_id -> + V.typed_avalue -> + T.rty -> + V.borrow_id -> + V.typed_avalue -> + T.rty -> + V.typed_avalue -> + V.typed_avalue + + (** Parameters: + [ty0] + [ids0] + [v0] + [av0] + [ty1] + [ids1] + [v1] + [av1] + [ty]: result of matching ty0 and ty1 + [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 -> + T.rty -> + V.typed_value -> + V.typed_avalue -> + V.typed_avalue + + (** Parameters: + [ty0] + [id0] + [av0] + [ty1] + [id1] + [av1] + [ty]: result of matching ty0 and ty1 + [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 -> + T.rty -> + 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 + +module type Matcher = sig + (** Match two values. + + Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}. + *) + val match_typed_values : + C.eval_ctx -> V.typed_value -> V.typed_value -> V.typed_value + + (** Match two avalues. + + Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}. + *) + val match_typed_avalues : + C.eval_ctx -> V.typed_avalue -> V.typed_avalue -> V.typed_avalue +end + +(** See {!InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and + {!InterpreterLoopsCore.CheckEquivMatcher}. + + Very annoying: functors only take modules as inputs... + *) +module type MatchCheckEquivState = sig + (** [true] if we check equivalence between contexts, [false] if we match + a source context with a target context. *) + val check_equiv : bool + + val ctx : C.eval_ctx + val rid_map : T.RegionId.InjSubst.t ref + + (** Substitution for the loan and borrow ids - used only if [check_equiv] is true *) + val blid_map : V.BorrowId.InjSubst.t ref + + (** Substitution for the borrow ids - used only if [check_equiv] is false *) + val borrow_id_map : V.BorrowId.InjSubst.t ref + + (** Substitution for the loans ids - used only if [check_equiv] is false *) + val loan_id_map : V.BorrowId.InjSubst.t ref + + val sid_map : V.SymbolicValueId.InjSubst.t ref + val sid_to_value_map : V.typed_value V.SymbolicValueId.Map.t ref + val aid_map : V.AbstractionId.InjSubst.t ref + val lookup_shared_value_in_ctx0 : V.BorrowId.id -> V.typed_value + val lookup_shared_value_in_ctx1 : V.BorrowId.id -> V.typed_value +end + +module type CheckEquivMatcher = sig + include PrimMatcher + + val match_aid : V.abstraction_id -> V.abstraction_id -> V.abstraction_id + + val match_aidl : + V.abstraction_id list -> V.abstraction_id list -> V.abstraction_id list + + val match_aids : + V.abstraction_id_set -> V.abstraction_id_set -> V.abstraction_id_set + + val match_rid : V.region_id -> V.region_id -> V.region_id + val match_rids : V.region_id_set -> V.region_id_set -> V.region_id_set + val match_borrow_id : V.borrow_id -> V.borrow_id -> V.borrow_id + + val match_borrow_idl : + V.borrow_id list -> V.borrow_id list -> V.borrow_id list + + val match_borrow_ids : V.borrow_id_set -> V.borrow_id_set -> V.borrow_id_set + val match_loan_id : V.loan_id -> V.loan_id -> V.loan_id + val match_loan_idl : V.loan_id list -> V.loan_id list -> V.loan_id list + val match_loan_ids : V.loan_id_set -> V.loan_id_set -> V.loan_id_set +end + +(** See {!InterpreterLoopsMatchCtxs.match_ctxs} *) +type ids_maps = { + aid_map : V.AbstractionId.InjSubst.t; + blid_map : V.BorrowId.InjSubst.t; + (** Substitution for the loan and borrow ids *) + borrow_id_map : V.BorrowId.InjSubst.t; (** Substitution for the borrow ids *) + loan_id_map : V.BorrowId.InjSubst.t; (** Substitution for the loan ids *) + rid_map : T.RegionId.InjSubst.t; + sid_map : V.SymbolicValueId.InjSubst.t; + sid_to_value_map : V.typed_value V.SymbolicValueId.Map.t; +} +[@@deriving show] + +type borrow_loan_corresp = { + borrow_to_loan_id_map : V.BorrowId.InjSubst.t; + loan_to_borrow_id_map : V.BorrowId.InjSubst.t; +} +[@@deriving show] + +(* Very annoying: functors only take modules as inputs... *) +module type MatchJoinState = sig + (** The current context *) + val ctx : C.eval_ctx + + (** The current loop *) + val loop_id : V.LoopId.id + + (** The abstractions introduced when performing the matches *) + val nabs : V.abs list ref +end + +(** Split an environment between the fixed abstractions, values, etc. and + the new abstractions, values, etc. + + Returns: (fixed, new abs, new dummies) + *) +let ctx_split_fixed_new (fixed_ids : ids_sets) (ctx : C.eval_ctx) : + C.env * V.abs list * V.typed_value list = + let is_fresh_did (id : C.DummyVarId.id) : bool = + not (C.DummyVarId.Set.mem id fixed_ids.dids) + in + let is_fresh_abs_id (id : V.AbstractionId.id) : bool = + not (V.AbstractionId.Set.mem id fixed_ids.aids) + in + (* Filter the new abstractions and dummy variables (there shouldn't be any new dummy variable + though) in the target context *) + let is_fresh (ee : C.env_elem) : bool = + match ee with + | C.Var (VarBinder _, _) | C.Frame -> false + | C.Var (DummyBinder bv, _) -> is_fresh_did bv + | C.Abs abs -> is_fresh_abs_id abs.abs_id + in + let new_eel, filt_env = List.partition is_fresh ctx.env in + let is_abs ee = match ee with C.Abs _ -> true | _ -> false in + let new_absl, new_dummyl = List.partition is_abs new_eel in + let new_absl = + List.map + (fun ee -> + match ee with C.Abs abs -> abs | _ -> raise (Failure "Unreachable")) + new_absl + in + let new_dummyl = + List.map + (fun ee -> + match ee with + | C.Var (DummyBinder _, v) -> v + | _ -> raise (Failure "Unreachable")) + new_dummyl + in + (filt_env, new_absl, new_dummyl) + +let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets = + let { aids; blids = _; borrow_ids = _; loan_ids = _; dids; rids; sids } = + ids + in + let empty = V.BorrowId.Set.empty in + let ids = + { + aids; + blids = empty; + borrow_ids = empty; + loan_ids = empty; + dids; + rids; + sids; + } + in + ids |