diff options
Diffstat (limited to 'compiler/InterpreterLoopsCore.ml')
| -rw-r--r-- | compiler/InterpreterLoopsCore.ml | 266 |
1 files changed, 126 insertions, 140 deletions
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index 6e33c75b..d14230c6 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -1,26 +1,17 @@ (** 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 Types +open Values +open Contexts 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 + | AbsInLeft of AbstractionId.id + | LoanInLeft of BorrowId.id + | LoansInLeft of BorrowId.Set.t + | AbsInRight of AbstractionId.id + | LoanInRight of BorrowId.id + | LoansInRight of BorrowId.Set.t (** Utility exception *) exception ValueMatchFailure of updt_env_kind @@ -28,10 +19,10 @@ exception ValueMatchFailure of updt_env_kind (** Utility exception *) exception Distinct of string -type ctx_or_update = (C.eval_ctx, updt_env_kind) result +type ctx_or_update = (eval_ctx, updt_env_kind) result (** Union Find *) -module UnionFind = UF.Make (UF.StoreMap) +module UF = UnionFind.Make (UnionFind.StoreMap) (** A small utility - @@ -41,13 +32,13 @@ module UnionFind = UF.Make (UF.StoreMap) 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; + abs_ids : AbstractionId.id list; + abs_to_borrows : BorrowId.Set.t AbstractionId.Map.t; + abs_to_loans : BorrowId.Set.t AbstractionId.Map.t; + abs_to_borrows_loans : BorrowId.Set.t AbstractionId.Map.t; + borrow_to_abs : AbstractionId.Set.t BorrowId.Map.t; + loan_to_abs : AbstractionId.Set.t BorrowId.Map.t; + borrow_loan_to_abs : AbstractionId.Set.t BorrowId.Map.t; } (** See {!InterpreterLoopsMatchCtxs.MakeMatcher} and {!InterpreterLoopsCore.Matcher}. @@ -56,14 +47,14 @@ type abs_borrows_loans_maps = { {!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 + val match_etys : ety -> ety -> ety + val match_rtys : rty -> rty -> rty (** The input primitive values are not equal *) - val match_distinct_literals : T.ety -> V.literal -> V.literal -> V.typed_value + val match_distinct_literals : ety -> literal -> literal -> 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 + val match_distinct_adts : ety -> adt_value -> adt_value -> typed_value (** The meta-value is the result of a match. @@ -76,11 +67,11 @@ module type PrimMatcher = sig 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 + (typed_value -> typed_value -> typed_value) -> + ety -> + borrow_id -> + borrow_id -> + borrow_id (** The input parameters are: - [ty] @@ -91,13 +82,13 @@ module type PrimMatcher = sig - [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 + ety -> + borrow_id -> + typed_value -> + borrow_id -> + typed_value -> + typed_value -> + borrow_id * typed_value (** Parameters: [ty] @@ -106,17 +97,16 @@ module type PrimMatcher = sig [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 + ety -> + loan_id_set -> + loan_id_set -> + typed_value -> + loan_id_set * typed_value - val match_mut_loans : T.ety -> V.loan_id -> V.loan_id -> V.loan_id + val match_mut_loans : ety -> loan_id -> loan_id -> loan_id (** There are no constraints on the input symbolic values *) - val match_symbolic_values : - V.symbolic_value -> V.symbolic_value -> V.symbolic_value + val match_symbolic_values : symbolic_value -> symbolic_value -> symbolic_value (** Match a symbolic value with a value which is not symbolic. @@ -126,7 +116,7 @@ module type PrimMatcher = sig end loans in one of the two environments). *) val match_symbolic_with_other : - bool -> V.symbolic_value -> V.typed_value -> V.typed_value + bool -> symbolic_value -> typed_value -> typed_value (** Match a bottom value with a value which is not bottom. @@ -135,11 +125,11 @@ module type PrimMatcher = sig 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 + val match_bottom_with_other : bool -> typed_value -> 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 + rty -> adt_avalue -> rty -> adt_avalue -> rty -> typed_avalue (** Parameters: [ty0] @@ -149,7 +139,7 @@ module type PrimMatcher = sig [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 + rty -> borrow_id -> rty -> borrow_id -> rty -> typed_avalue (** Parameters: [ty0] @@ -162,15 +152,15 @@ module type PrimMatcher = sig [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 + rty -> + borrow_id -> + typed_avalue -> + rty -> + borrow_id -> + typed_avalue -> + rty -> + typed_avalue -> + typed_avalue (** Parameters: [ty0] @@ -186,18 +176,18 @@ module type PrimMatcher = sig [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 + rty -> + loan_id_set -> + typed_value -> + typed_avalue -> + rty -> + loan_id_set -> + typed_value -> + typed_avalue -> + rty -> + typed_value -> + typed_avalue -> + typed_avalue (** Parameters: [ty0] @@ -210,20 +200,20 @@ module type PrimMatcher = sig [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 + rty -> + borrow_id -> + typed_avalue -> + rty -> + borrow_id -> + typed_avalue -> + rty -> + typed_avalue -> + 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 + val match_avalues : typed_avalue -> typed_avalue -> typed_avalue end module type Matcher = sig @@ -231,15 +221,14 @@ module type Matcher = sig 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 + val match_typed_values : eval_ctx -> typed_value -> typed_value -> 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 + eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue end (** See {!InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and @@ -252,78 +241,75 @@ module type MatchCheckEquivState = sig a source context with a target context. *) val check_equiv : bool - val ctx : C.eval_ctx - val rid_map : T.RegionId.InjSubst.t ref + val ctx : eval_ctx + val rid_map : 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 + val blid_map : 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 + val borrow_id_map : 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 loan_id_map : 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 + val sid_map : SymbolicValueId.InjSubst.t ref + val sid_to_value_map : typed_value SymbolicValueId.Map.t ref + val aid_map : AbstractionId.InjSubst.t ref + val lookup_shared_value_in_ctx0 : BorrowId.id -> typed_value + val lookup_shared_value_in_ctx1 : BorrowId.id -> typed_value end module type CheckEquivMatcher = sig include PrimMatcher - val match_aid : V.abstraction_id -> V.abstraction_id -> V.abstraction_id + val match_aid : abstraction_id -> abstraction_id -> abstraction_id val match_aidl : - V.abstraction_id list -> V.abstraction_id list -> V.abstraction_id list + abstraction_id list -> abstraction_id list -> 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 + abstraction_id_set -> abstraction_id_set -> abstraction_id_set + + val match_rid : region_id -> region_id -> region_id + val match_rids : region_id_set -> region_id_set -> region_id_set + val match_borrow_id : borrow_id -> borrow_id -> borrow_id + val match_borrow_idl : borrow_id list -> borrow_id list -> borrow_id list + val match_borrow_ids : borrow_id_set -> borrow_id_set -> borrow_id_set + val match_loan_id : loan_id -> loan_id -> loan_id + val match_loan_idl : loan_id list -> loan_id list -> loan_id list + val match_loan_ids : loan_id_set -> loan_id_set -> loan_id_set end (** See {!InterpreterLoopsMatchCtxs.match_ctxs} *) type ids_maps = { - aid_map : V.AbstractionId.InjSubst.t; - blid_map : V.BorrowId.InjSubst.t; + aid_map : AbstractionId.InjSubst.t; + blid_map : 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; + borrow_id_map : BorrowId.InjSubst.t; (** Substitution for the borrow ids *) + loan_id_map : BorrowId.InjSubst.t; (** Substitution for the loan ids *) + rid_map : RegionId.InjSubst.t; + sid_map : SymbolicValueId.InjSubst.t; + sid_to_value_map : typed_value 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; + borrow_to_loan_id_map : BorrowId.InjSubst.t; + loan_to_borrow_id_map : 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 + val ctx : eval_ctx (** The current loop *) - val loop_id : V.LoopId.id + val loop_id : LoopId.id (** The abstractions introduced when performing the matches *) - val nabs : V.abs list ref + val nabs : abs list ref end (** Split an environment between the fixed abstractions, values, etc. and @@ -331,36 +317,36 @@ end 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) +let ctx_split_fixed_new (fixed_ids : ids_sets) (ctx : eval_ctx) : + env * abs list * typed_value list = + let is_fresh_did (id : DummyVarId.id) : bool = + not (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) + let is_fresh_abs_id (id : AbstractionId.id) : bool = + not (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 = + let is_fresh (ee : 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 + | EBinding (BVar _, _) | EFrame -> false + | EBinding (BDummy bv, _) -> is_fresh_did bv + | EAbs 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 is_abs ee = match ee with EAbs _ -> 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")) + match ee with EAbs abs -> abs | _ -> raise (Failure "Unreachable")) new_absl in let new_dummyl = List.map (fun ee -> match ee with - | C.Var (DummyBinder _, v) -> v + | EBinding (BDummy _, v) -> v | _ -> raise (Failure "Unreachable")) new_dummyl in @@ -370,7 +356,7 @@ 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 empty = BorrowId.Set.empty in let ids = { aids; |