diff options
Diffstat (limited to 'compiler/InterpreterLoopsMatchCtxs.mli')
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.mli | 301 |
1 files changed, 301 insertions, 0 deletions
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli new file mode 100644 index 00000000..7e585dd6 --- /dev/null +++ b/compiler/InterpreterLoopsMatchCtxs.mli @@ -0,0 +1,301 @@ +(** This module implements support to match contexts for loops. + + The matching functions are used for instance to compute joins, or + to check if two contexts are equivalent (modulo conversion). + *) + +module T = Types +module PV = PrimitiveValues +module V = Values +module E = Expressions +module C = Contexts +module Subst = Substitute +module A = LlbcAst +module Inv = Invariants +module S = SynthesizeSymbolic +open Cps +open InterpreterUtils +open InterpreterLoopsCore + +(** Compute various maps linking the abstractions and the borrows/loans they contain. + + Parameters: + - [no_duplicates]: checks that borrows/loans are not referenced more than once + (see the documentation for {!type:InterpreterLoopsCore.abs_borrows_loans_maps}). + - [explore]: this function is used to filter abstractions. + - [env] + *) +val compute_abs_borrows_loans_maps : + bool -> (V.abs -> bool) -> C.env -> abs_borrows_loans_maps + +(** Generic functor to implement matching functions between values, environments, + etc. + + We use it for joins, to check if two environments are convertible, etc. + See for instance {!MakeJoinMatcher} and {!MakeCheckEquivMatcher}. + + The functor is parameterized by a {!InterpreterLoopsCore.PrimMatcher}, which implements the + non-generic part of the match. More precisely, the role of {!InterpreterLoopsCore.PrimMatcher} is two + provide generic functions which recursively match two values (by recursively + matching the fields of ADT values for instance). When it does need to match + values in a non-trivial manner (if two ADT values don't have the same + variant for instance) it calls the corresponding specialized function from + {!InterpreterLoopsCore.PrimMatcher}. + *) +module MakeMatcher : functor (PM : PrimMatcher) -> Matcher + +(** A matcher for joins (we use joins to compute loop fixed points). + + See the explanations for {!MakeMatcher}. + + In case of loop joins: + - we match *concrete* values + - we check that the "fixed" abstractions (the abstractions to be framed + - i.e., the abstractions which are the same in the two environments to + join) are equal + - we keep the abstractions which are not in the frame, then merge those + together (if they have borrows/loans in common) later + The join matcher is used to match the *concrete* values only. For this + reason, we fail on the functions which match avalues. + *) +module MakeJoinMatcher : functor (S : MatchJoinState) -> PrimMatcher + +(** An auxiliary matcher that we use for two purposes: + - to check if two contexts are equivalent modulo id substitution (i.e., + alpha equivalent) (see {!ctxs_are_equivalent}). + - to compute a mapping between the borrows and the symbolic values in a + target context to the values and borrows in a source context (see + {!match_ctx_with_target}). + *) +module MakeCheckEquivMatcher : functor (S : MatchCheckEquivState) -> + CheckEquivMatcher + +(** Compute whether two contexts are equivalent modulo an identifier substitution. + + [fixed_ids]: ids for which we force the mapping to be the identity. + + We also take advantage of the structure of the environments, which should + have the same prefixes (we check it). See the explanations for {!InterpreterLoopsJoinCtxs.join_ctxs}. + + TODO: explanations. + + The input parameters are: + - [check_equiv]: if [true], check if the two contexts are equivalent. + If [false], compute a mapping from the first context to the second context, + in the sense of [match_ctx_with_target]. + + - [fixed_ids] + + - [lookup_shared_value_in_ctx0], [lookup_shared_value_in_ctx1]: + The lookup functions are used to match the shared values when [check_equiv] + is [false] (we sometimes use [match_ctxs] on partial environments, meaning + we have to lookup the shared values in the complete environment, otherwise + we miss some mappings). + + - [ctx0] + - [ctx1] + + We return an optional ids map: [Some] if the match succeeded, [None] otherwise. + *) +val match_ctxs : + bool -> + ids_sets -> + (V.loan_id -> V.typed_value) -> + (V.loan_id -> V.typed_value) -> + C.eval_ctx -> + C.eval_ctx -> + ids_maps option + +(** Compute whether two contexts are equivalent modulo an identifier substitution. + + We also take advantage of the structure of the environments, which should + have the same prefixes (we check it). See the explanations for + {!InterpreterLoopsJoinCtxs.join_ctxs}. + + For instance, the following environments are equivalent: + {[ + env0 = { + abs@0 { ML l0 } + ls -> MB l1 (s2 : loops::List<T>) + i -> s1 : u32 + abs@1 { MB l0, ML l1 } + } + + env1 = { + abs@0 { ML l0 } + ls -> MB l2 (s4 : loops::List<T>) + i -> s3 : u32 + abs@2 { MB l0, ML l2 } + } + ]} + + We can go from [env0] to [env1] with the substitution: + {[ + abs_id_subst: { abs@1 -> abs@2 } + borrow_id_subst: { l1 -> l2 } + symbolic_id_subst: { s1 -> s3, s2 -> s4 } + ]} + + + Parameters: + - [fixed_ids]: ids for which we force the mapping to be the identity. + - [ctx0] + - [ctx1] + *) +val ctxs_are_equivalent : ids_sets -> C.eval_ctx -> C.eval_ctx -> bool + +(** Match a context with a target context. + + This is used to compute application of loop translations: we use this + to introduce "identity" abstractions upon (re-)entering the loop. + + For instance, the fixed point for [list_nth_mut] (see the top of the file) + is: + {[ + env_fp = { + abs@0 { ML l0 } + ls -> MB l1 (s@3 : loops::List<T>) + i -> s@4 : u32 + abs@fp { + MB l0 + ML l1 + } + } + ]} + + Upon re-entering the loop, starting from the fixed point, we get the + following environment: + {[ + env = { + abs@0 { ML l0 } + ls -> MB l5 (s@6 : loops::List<T>) + i -> s@7 : u32 + abs@1 { MB l0, ML l1 } + _@1 -> MB l1 (loops::List::Cons (ML l2, ML l3)) + _@2 -> MB l3 (@Box (ML l5)) // tail + _@3 -> MB l2 (s@3 : T) // hd + } + ]} + + We want to introduce an abstraction [abs@2], which has the same shape as [abs@fp] + above (the fixed-point abstraction), and which is actually the identity. If we do so, + we get an environment which is actually also a fixed point (we can collapse + the dummy variables and [abs@1] to actually retrieve the fixed point we + computed, and we use the fact that those values and abstractions can't be + *directly* manipulated unless we end this newly introduced [abs@2], which we + forbid). + + We match the *fixed point context* with the context upon entering the loop + by doing the following. + + 1. We filter [env_fp] and [env] to remove the newly introduced dummy variables + and abstractions. We get: + + {[ + filtered_env_fp = { + abs@0 { ML l0 } + ls -> MB l1 (s@3 : loops::List<T>) + i -> s@4 : u32 + // removed abs@fp + } + + filtered_env = { + abs@0 { ML l0 } + ls -> MB l5 (s@6 : loops::List<T>) + i -> s@7 : u32 + // removed abs@1, _@1, etc. + } + ]} + + 2. We match [filtered_env_fp] with [filtered_env] to compute a map from + the FP borrows/loans to the current borrows/loans (and also from symbolic values to + values). Note that we take care to *consider loans and borrows separately*, + and we ignore the "fixed" abstractions (which are unchanged - we checked that + when computing the fixed point). + We get: + {[ + borrows_map: { l1 -> l5 } // because we matched [MB l1 ...] with [MB l5 ...] + loans_map: {} // we ignore abs@0, which is "fixed" + ]} + + 3. We want to introduce an instance of [abs@fp] which is actually the + identity. From [compute_fixed_point_id_correspondance] and looking at + [abs@fp], we know we should link the instantiation of loan [l1] with the + instantiation of loan [l0]. We substitute [l0] with [l5] (following step 2.) + and introduce a fresh borrow [l6] for [l5] that we use to instantiate [l1]. + We get the following environment: + + {[ + env = { + abs@0 { ML l0 } + ls -> MB l6 (s@6 : loops::List<T>) + i -> s@7 : u32 + abs@1 { MB l0, ML l1 } + _@1 -> MB l1 (loops::List::Cons (ML l2, ML l3)) + _@2 -> MB l3 (@Box (ML l5)) // tail + _@3 -> MB l2 (s@3 : T) // hd + abs@2 { MB l5, ML l6 } // this is actually the identity: l6 = l5 + } + ]} + + 4. As we now have a fixed point (see above comments), we can consider than + [abs@2] links the current iteration to the last one before we exit. What we + are interested in is that: + - upon inserting [abs@2] we re-entered the loop, meaning in the translation + we need to insert a recursive call to the loop forward function + - upon ending [abs@2] we need to insert a call to the loop backward function + + Because we want to ignore them, we end the loans in the newly introduced + [abs@2] abstraction (i.e., [l6]). We get: + {[ + env = { + abs@0 { ML l0 } + ls -> ⊥ + i -> s@7 : u32 + abs@1 { MB l0, ML l1 } + _@1 -> MB l1 (loops::List::Cons (ML l2, ML l3)) + _@2 -> MB l3 (@Box (ML l5)) // tail + _@3 -> MB l2 (s@3 : T) // hd + abs@2 { MB l5 } + } + ]} + + TODO: we shouldn't need to end the loans, we should actually remove them + before inserting the new abstractions (we may have issues with the symbolic + values, if they contain borrows - above i points to [s@7], but it should + be a different symbolic value...). + + Finally, we use the map from symbolic values to values to compute the list of + input values of the loop: we simply list the values, by order of increasing + symbolic value id. We *do* use the fixed values (though they are in the frame) + because they may be *read* inside the loop. + + We can then proceed to finishing the symbolic execution and doing the + synthesis. + + Rem.: we might reorganize the [tgt_ctx] by ending loans for instance. + + **Parameters**: + - [config] + - [loop_id] + - [is_loop_entry]: [true] if first entry into the loop, [false] if re-entry + (i.e., continue). + - [fp_bl_maps]: for the abstractions in the fixed-point (the source context), + the maps from loans to borrows and borrows to loans, if those abstractions + are seen as identity abstractions (for every of those abstractions, there + must be a bijection between the borrows and the loans) + - [fp_input_svalues]: the list of symbolic values appearing in the fixed + point (the source context) and which must be instantiated during the match + (this is the list of input parameters of the loop). + - [fixed_ids] + - [src_ctx] + *) +val match_ctx_with_target : + C.config -> + V.loop_id -> + bool -> + borrow_loan_corresp -> + V.symbolic_value_id list -> + ids_sets -> + C.eval_ctx -> + st_cm_fun |