diff options
Diffstat (limited to 'src/InterpreterExpansion.ml')
-rw-r--r-- | src/InterpreterExpansion.ml | 53 |
1 files changed, 46 insertions, 7 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 18ec1ecc..3903ca14 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -60,7 +60,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) in (* Visitor to apply the expansion *) let obj = - object + object (self) inherit [_] C.map_eval_ctx as super method! visit_abs current_abs abs = @@ -70,12 +70,31 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) (** When visiting an abstraction, we remember the regions it owns to be able to properly reduce projectors when expanding symbolic values *) + method! visit_aproj current_abs aproj = + (match aproj with + | AProjLoans sv | AProjBorrows (sv, _) -> + assert (not (same_symbolic_id sv original_sv)) + | AEndedProjLoans _ | AEndedProjBorrows | AIgnoredProjBorrows -> ()); + super#visit_aproj current_abs aproj + (** We carefully updated [visit_ASymbolic] so that [visit_aproj] is called + only on child projections (i.e., projections which appear in [AEndedProjLoans]). + The role of visit_aproj is then to check we don't have to expand symbolic + values in child projections, because it should never happen + *) + method! visit_ASymbolic current_abs aproj = let current_abs = Option.get current_abs in let proj_regions = current_abs.regions in let ancestors_regions = current_abs.ancestors_regions in + (* Explore in depth first - we won't update anything: we simply + * want to check we don't have to expand inner symbolic value *) match (aproj, proj_kind) with - | (V.AEndedProjLoans | V.AEndedProjBorrows), _ -> V.ASymbolic aproj + | V.AEndedProjLoans None, _ | V.AEndedProjBorrows, _ -> + V.ASymbolic aproj + | V.AEndedProjLoans (Some child_proj), _ -> + (* Explore the child projection to make sure we don't have to expand + * anything in there *) + V.ASymbolic (self#visit_aproj (Some current_abs) child_proj) | V.AProjLoans sv, LoanProj -> (* Check if this is the symbolic value we are looking for *) if same_symbolic_id sv original_sv then @@ -111,9 +130,11 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) else (* Not the searched symbolic value: nothing to do *) super#visit_ASymbolic (Some current_abs) aproj - | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj -> + | V.AProjLoans _, BorrowProj + | V.AProjBorrows (_, _), LoanProj + | V.AIgnoredProjBorrows, _ -> (* Nothing to do *) - super#visit_ASymbolic (Some current_abs) aproj + V.ASymbolic aproj end in (* Apply the expansion *) @@ -275,7 +296,7 @@ let expand_symbolic_value_shared_borrow (config : C.config) in (* Visitor to replace the projectors on borrows *) let obj = - object + object (self) inherit [_] C.map_eval_ctx as super method! visit_Symbolic env sv = @@ -302,17 +323,35 @@ let expand_symbolic_value_shared_borrow (config : C.config) let asb = List.concat (List.map expand_asb asb) in V.AProjSharedBorrow asb + method! visit_aproj proj_regions aproj = + (match aproj with + | AProjLoans sv | AProjBorrows (sv, _) -> + assert (not (same_symbolic_id sv original_sv)) + | AEndedProjLoans _ | AEndedProjBorrows | AIgnoredProjBorrows -> ()); + super#visit_aproj proj_regions aproj + (** We carefully updated [visit_ASymbolic] so that [visit_aproj] is called + only on child projections (i.e., projections which appear in [AEndedProjLoans]). + The role of visit_aproj is then to check we don't have to expand symbolic + values in child projections, because it should never happen + *) + method! visit_ASymbolic proj_regions aproj = match aproj with + | AEndedProjBorrows | AIgnoredProjBorrows -> + (* We ignore borrows *) V.ASymbolic aproj | AProjLoans _ -> (* Loans are handled later *) - super#visit_ASymbolic proj_regions aproj + V.ASymbolic aproj | AProjBorrows (sv, proj_ty) -> ( (* Check if we need to reborrow *) match reborrow_ashared (Option.get proj_regions) sv proj_ty with | None -> super#visit_ASymbolic proj_regions aproj | Some asb -> V.ABorrow (V.AProjSharedBorrow asb)) - | AEndedProjLoans | AEndedProjBorrows -> V.ASymbolic aproj + | AEndedProjLoans None -> V.ASymbolic aproj + | AEndedProjLoans (Some child_aproj) -> + (* Sanity check: make sure there is nothing to expand inside children + * projections *) + V.ASymbolic (self#visit_aproj proj_regions child_aproj) end in (* Call the visitor *) |