summaryrefslogtreecommitdiff
path: root/compiler/InterpreterLoopsCore.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterLoopsCore.ml')
-rw-r--r--compiler/InterpreterLoopsCore.ml386
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