summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-12-01 00:36:12 +0100
committerSon HO2023-02-03 11:21:46 +0100
commit4c30e381a96a4d1a0d2dab20fbcc08bd91cad0ec (patch)
treed35a159630f53d8a6d6c16e67ed25cffb6b9eae8
parent4412989abff237c566cad323a8a56cf08bb8e294 (diff)
Make minor modifications
-rw-r--r--compiler/InterpreterBorrows.ml8
-rw-r--r--compiler/InterpreterBorrows.mli4
2 files changed, 11 insertions, 1 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 4e05dda7..9a78e77a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -2405,7 +2405,13 @@ let ctx_merge_regions (ctx : C.eval_ctx) (rid : T.RegionId.id)
List.map (Substitute.typed_avalue_subst_rids rsubst) abs.V.avalues
in
let regions = T.RegionId.Set.diff abs.V.regions rids in
- let ancestors_regions = T.RegionId.Set.diff abs.V.ancestors_regions rids in
+ let ancestors_regions =
+ if T.RegionId.Set.disjoint abs.V.ancestors_regions rids then
+ abs.V.ancestors_regions
+ else
+ T.RegionId.Set.add rid
+ (T.RegionId.Set.diff abs.V.ancestors_regions rids)
+ in
{ abs with V.avalues; regions; ancestors_regions }
in
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 53297bc7..51c6c592 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -203,6 +203,10 @@ type merge_duplicates_funcs = {
(** Merge two abstractions together.
+ We insert the result of the merge in place of the first abstraction (this
+ helps preserving the structure of the environment, when computing loop
+ fixed points for instance).
+
When we merge two abstractions together, we remove the loans/borrows
which appear in one and whose associated loans/borrows appear in the
other. For instance: