Implement FreshCap Handling for Classes and Objects #24136
Add this suggestion to a batch that can be applied as a single commit. This suggestion is invalid because no changes were made to the code. Suggestions cannot be applied while the pull request is closed. Suggestions cannot be applied while viewing a subset of changes. Only one suggestion per line can be applied in a batch. Add this suggestion to a batch that can be applied as a single commit. Applying suggestions on deleted lines is not supported. You must change the existing code in this line in order to create a valid suggestion. Outdated suggestions cannot be applied. This suggestion has been applied or marked resolved. Suggestions cannot be applied from pending reviews. Suggestions cannot be applied on multi-line comments. Suggestions cannot be applied while the pull request is queued to merge. Suggestion cannot be applied right now. Please check back later.
This is a complete implementation of https://github.com/lampepfl/papers/pull/155. It consists of the following major parts:
Let fresh caps in field types contribute to class captures
A fresh in the capture set of a class field now causes a fresh
to be added to the capture set of every instance of that class.
This caused 18 failures in stdlib of which 2 were significant (the rest was deprecated stuff). So far, we make
this compile with the
@caps.unsafe.untrackedCaptures
annotation. #24137 explains what would be neededto fix this in a safer way.
Add prefixes to fresh caps and relate class and field fresh caps
Fresh created in classes now carry a prefix referring to the
this
of the class. The prefix gets mappedby TypeMaps, including
asSeenFrom
. We establish a "covers" relation between a fresh for an object and a fresh for one of its fields. We use the same relation for subsumption.Example:
Here the type of
a.f
isA^{a.cap2}
. Furthermorecap1
, the cap captured by the type ofa
, both covers and subsumesa.cap2
.Make sure that private fields with inferred types don't capture a fresh cap
Fields contribute fresh caps to the class. The problem is what to do with capsets in inferred types of fields. These pose problems of separate compilation. We already demand explicit declarations of capsets of non-private fields. We need to also demand an explicit declaration when a private field has an inferred capset that is not otherwise accounted for in the capset of the enclosing class. That condition can be checked post-cc, when all capsets are known. I.e. it is checked at the same time as when we check non-private fields.