Add the Modifiability Checker

annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/find/ConstructorInsertion.java

@@ -4,6 +4,7 @@
 import java.util.List;
 import java.util.Set;
 import org.checkerframework.afu.scenelib.type.Type;
+import org.checkerframework.checker.modifiability.qual.Growable;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
@@ -15,7 +16,7 @@ public class ConstructorInsertion extends TypedInsertion {
   private @Nullable ReceiverInsertion receiverInsertion = null;
 
   /** The declaration annotations to write on the generated constructor. */
-  private Set<Insertion> declarationInsertions = new LinkedHashSet<>();
+  private @Growable Set<Insertion> declarationInsertions = new LinkedHashSet<>();
 
   /**
    * Construct a ConstructorInsertion.
@@ -28,7 +29,8 @@ public class ConstructorInsertion extends TypedInsertion {
    * @param criteria where to insert the text
    * @param innerTypeInsertions the inner types to go on this constructor
    */
-  public ConstructorInsertion(Type type, Criteria criteria, List<Insertion> innerTypeInsertions) {
+  public ConstructorInsertion(
+      Type type, Criteria criteria, @Growable List<Insertion> innerTypeInsertions) {
     super(type, criteria, true, innerTypeInsertions);
   }
 

annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/find/Criteria.java

@@ -13,6 +13,8 @@
 import org.checkerframework.afu.scenelib.io.ASTPath;
 import org.checkerframework.afu.scenelib.io.DebugWriter;
 import org.checkerframework.checker.interning.qual.FindDistinct;
+import org.checkerframework.checker.modifiability.qual.Growable;
+import org.checkerframework.checker.modifiability.qual.Replaceable;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.signature.qual.ClassGetName;
 import org.objectweb.asm.TypePath;
@@ -28,7 +30,7 @@ public final class Criteria {
 
   // NOTE: This does not permit multiple criteria of a given kind.
   /** The set of criterion objects, indexed by kind. */
-  private final Map<Criterion.Kind, Criterion> criteria;
+  private final @Growable @Replaceable Map<Criterion.Kind, Criterion> criteria;
 
   /** Creates a new {@code Criteria} without any {@code Criterion}. */
   public Criteria() {

annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/find/Insertion.java

@@ -14,6 +14,7 @@
 import org.checkerframework.afu.scenelib.type.BoundedType;
 import org.checkerframework.afu.scenelib.type.DeclaredType;
 import org.checkerframework.afu.scenelib.type.Type;
+import org.checkerframework.checker.modifiability.qual.Growable;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.objectweb.asm.TypePath;
 import org.plumelib.util.StringsP;
@@ -46,7 +47,7 @@ public enum Kind {
    * The package names for the annotations being inserted by this Insertion. This will be empty
    * unless {@link #getText(boolean)} is called with abbreviate=true.
    */
-  protected Set<String> packageNames;
+  protected @Growable Set<String> packageNames;
 
   /**
    * Set of annotation names that should always be inserted fully-qualified, even when {@link

annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/find/TypedInsertion.java

@@ -5,6 +5,7 @@
 import org.checkerframework.afu.scenelib.type.BoundedType;
 import org.checkerframework.afu.scenelib.type.DeclaredType;
 import org.checkerframework.afu.scenelib.type.Type;
+import org.checkerframework.checker.modifiability.qual.Growable;
 
 /**
  * An insertion that may result in code generation other than just annotations. {@code
@@ -28,7 +29,7 @@ public abstract class TypedInsertion extends Insertion {
   protected boolean annotationsOnly;
 
   /** The inner types to go on this insertion. See {@link ReceiverInsertion} for more details. */
-  protected List<Insertion> innerTypeInsertions;
+  protected @Growable List<Insertion> innerTypeInsertions;
 
   /**
    * Creates a new {@code TypedInsertion} whose text is not on its own line.
@@ -37,7 +38,8 @@ public abstract class TypedInsertion extends Insertion {
    * @param criteria where to insert the text
    * @param innerTypeInsertions the inner types to go on this insertion
    */
-  public TypedInsertion(Type type, Criteria criteria, List<Insertion> innerTypeInsertions) {
+  public TypedInsertion(
+      Type type, Criteria criteria, @Growable List<Insertion> innerTypeInsertions) {
     this(type, criteria, false, innerTypeInsertions);
   }
 
@@ -50,7 +52,7 @@ public TypedInsertion(Type type, Criteria criteria, List<Insertion> innerTypeIns
    * @param innerTypeInsertions the inner types to go on this insertion
    */
   public TypedInsertion(
-      Type type, Criteria criteria, boolean b, List<Insertion> innerTypeInsertions) {
+      Type type, Criteria criteria, boolean b, @Growable List<Insertion> innerTypeInsertions) {
     super(criteria, b);
     this.type = type;
     this.innerTypeInsertions = innerTypeInsertions;
@@ -83,7 +85,7 @@ public Type getType() {
    *
    * @return a copy of the inner types
    */
-  public List<Insertion> getInnerTypeInsertions() {
+  public @Growable List<Insertion> getInnerTypeInsertions() {
     return innerTypeInsertions;
   }
 

annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/specification/IndexFileSpecification.java

@@ -46,6 +46,9 @@
 import org.checkerframework.afu.scenelib.type.Type;
 import org.checkerframework.afu.scenelib.util.coll.VivifyingMap;
 import org.checkerframework.checker.formatter.qual.FormatMethod;
+import org.checkerframework.checker.modifiability.qual.Growable;
+import org.checkerframework.checker.modifiability.qual.IteratorPolyMod;
+import org.checkerframework.checker.modifiability.qual.Shrinkable;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.signature.qual.ClassGetName;
 import org.objectweb.asm.ClassReader;
@@ -61,7 +64,8 @@ public class IndexFileSpecification {
       LinkedHashMultimap.<Insertion, Annotation>create();
 
   /** The state of this object. */
-  private final List<Insertion> insertions = new ArrayList<>();
+  private final @Growable @Shrinkable @IteratorPolyMod List<Insertion> insertions =
+      new ArrayList<>();
 
   /** An insertion for the default constructor, or null. Is a member of insertions if non-null. */
   private ConstructorInsertion constructorInsertion = null;

annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/Annotation.java

@@ -14,6 +14,8 @@
 import java.util.StringJoiner;
 import org.checkerframework.afu.scenelib.el.AnnotationDef;
 import org.checkerframework.afu.scenelib.field.AnnotationFieldType;
+import org.checkerframework.checker.modifiability.qual.Growable;
+import org.checkerframework.checker.modifiability.qual.Replaceable;
 import org.checkerframework.checker.nullness.qual.KeyFor;
 import org.checkerframework.checker.nullness.qual.NonNull;
 
@@ -114,7 +116,9 @@ public Annotation(AnnotationDef def, Map<String, ? extends Object> fields) {
    * @param ja the java.lang.annotation.Annotation to make an Annotation for
    * @param adefs a cache from which to look up (or insert into) AnnotationDefs
    */
-  public Annotation(java.lang.annotation.Annotation ja, Map<String, AnnotationDef> adefs) {
+  // TODO: `adefs` need not be `@Replaceable`.  Use the Map Key checker to avoid a warning.
+  public Annotation(
+      java.lang.annotation.Annotation ja, @Growable @Replaceable Map<String, AnnotationDef> adefs) {
     Class<? extends java.lang.annotation.Annotation> jaType = ja.annotationType();
     String name = jaType.getName();
     if (adefs.containsKey(name)) {

annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/el/ABlock.java

@@ -3,6 +3,7 @@
 import java.util.Map;
 import java.util.Objects;
 import org.checkerframework.afu.scenelib.util.coll.VivifyingMap;
+import org.checkerframework.checker.modifiability.qual.Shrinkable;
 
 /**
  * ABlock has local variables in scope. We currently directly use them only for static initializer
@@ -12,7 +13,7 @@ public class ABlock extends AExpression {
   // Currently we don't validate the local locations (e.g., that no two
   // distinct ranges for the same index overlap).
   /** The method's annotated local variables; map key contains local variable location numbers. */
-  public final VivifyingMap<LocalLocation, AField> locals =
+  public final @Shrinkable VivifyingMap<LocalLocation, AField> locals =
       AField.<LocalLocation>newVivifyingLHMap_AF();
 
   /**

annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/el/AClass.java

@@ -13,16 +13,20 @@
 import javax.lang.model.element.VariableElement;
 import org.checkerframework.afu.scenelib.Annotation;
 import org.checkerframework.afu.scenelib.util.coll.VivifyingMap;
+import org.checkerframework.checker.modifiability.qual.Growable;
+import org.checkerframework.checker.modifiability.qual.Modifiable;
+import org.checkerframework.checker.modifiability.qual.Replaceable;
+import org.checkerframework.checker.modifiability.qual.Shrinkable;
 import org.plumelib.util.MapsP;
 
 /** An annotated class. */
 public class AClass extends ADeclaration {
   /** The class's annotated type parameter bounds. */
-  public final VivifyingMap<BoundLocation, ATypeElement> bounds =
+  public final @Growable @Replaceable @Shrinkable VivifyingMap<BoundLocation, ATypeElement> bounds =
       ATypeElement.<BoundLocation>newVivifyingLHMap_ATE();
 
   /** -1 maps to superclass, non-negative integers map to implemented or extended interfaces. */
-  public final VivifyingMap<TypeIndexLocation, ATypeElement> extendsImplements =
+  public final @Shrinkable VivifyingMap<TypeIndexLocation, ATypeElement> extendsImplements =
       ATypeElement.<TypeIndexLocation>newVivifyingLHMap_ATE();
 
   /**
@@ -31,19 +35,22 @@ public class AClass extends ADeclaration {
    * The annotation scene library does not validate the keys, nor does it check that annotated
    * subelements of the {@link AMethod}s exist in the signature.
    */
-  public final VivifyingMap<String, AMethod> methods = createMethodMap();
+  public final @Growable @Shrinkable VivifyingMap<String, AMethod> methods = createMethodMap();
 
   /** The class's annotated static initializer blocks; map key is the index of the block. */
-  public final VivifyingMap<Integer, ABlock> staticInits = createInitBlockMap();
+  public final @Growable @Shrinkable VivifyingMap<Integer, ABlock> staticInits =
+      createInitBlockMap();
 
   /** The class's annotated instance initializer blocks; map key is the index of the block. */
-  public final VivifyingMap<Integer, ABlock> instanceInits = createInitBlockMap();
+  public final @Growable @Shrinkable VivifyingMap<Integer, ABlock> instanceInits =
+      createInitBlockMap();
 
   /** The class's annotated fields; map key is field name. */
-  public final VivifyingMap<String, AField> fields = AField.<String>newVivifyingLHMap_AF();
+  public final @Growable @Shrinkable VivifyingMap<String, AField> fields =
+      AField.<String>newVivifyingLHMap_AF();
 
   /** The class's annotated field initializers; map key is field name. */
-  public final VivifyingMap<String, AExpression> fieldInits = createFieldInitMap();
+  public final @Growable VivifyingMap<String, AExpression> fieldInits = createFieldInitMap();
 
   /**
    * The type element representing the class. Clients must call {@link #setTypeElement(TypeElement)}
@@ -55,23 +62,23 @@ public class AClass extends ADeclaration {
   public final String className;
 
   /** The simple class names any of this class's outer classes (or this class) that are enums. */
-  private final HashSet<String> enums = new HashSet<>();
+  private final @Growable HashSet<String> enums = new HashSet<>();
 
   /** The enum constants of this class, or null if this class is not an enum. */
   private /*@MonotonicNonNull*/ List<VariableElement> enumConstants = null;
 
   /**
    * The simple class names any of this class's outer classes (or this class) that are annotations.
    */
-  private final HashSet<String> annotationTypes = new HashSet<>();
+  private final @Growable HashSet<String> annotationTypes = new HashSet<>();
 
   /**
    * The simple class names any of this class's outer classes (or this class) that are interfaces.
    */
-  private final HashSet<String> interfaces = new HashSet<>();
+  private final @Growable HashSet<String> interfaces = new HashSet<>();
 
   /** The simple class names any of this class's outer classes (or this class) that are records. */
-  private final HashSet<String> records = new HashSet<>();
+  private final @Growable HashSet<String> records = new HashSet<>();
 
   // debug fields to keep track of all classes created
   // private static List<AClass> debugAllClasses = new ArrayList<>();
@@ -244,7 +251,9 @@ public <R, T> R accept(ElementVisitor<R, T> v, T t) {
    *
    * @return a new vivifying map from method signature to {@link AMethod}
    */
-  private static VivifyingMap<String, AMethod> createMethodMap() {
+  @SuppressWarnings("modifiability:return") // The anonymous subclass's constructor result
+  // is the top qualifier, so it does not propagate the backing map's @Modifiable type.
+  private static @Modifiable VivifyingMap<String, AMethod> createMethodMap() {
     return new VivifyingMap<>(new LinkedHashMap<>()) {
       @Override
       public AMethod createValueFor(String k) {
@@ -264,7 +273,9 @@ public boolean isEmptyValue(AMethod v) {
    *
    * @return a new vivifying map from initializer block index to {@link ABlock}
    */
-  private static VivifyingMap<Integer, ABlock> createInitBlockMap() {
+  @SuppressWarnings("modifiability:return") // The anonymous subclass's constructor result
+  // is the top qualifier, so it does not propagate the backing map's @Modifiable type.
+  private static @Modifiable VivifyingMap<Integer, ABlock> createInitBlockMap() {
     return new VivifyingMap<>(new LinkedHashMap<>()) {
       @Override
       public ABlock createValueFor(Integer k) {
@@ -284,7 +295,9 @@ public boolean isEmptyValue(ABlock v) {
    *
    * @return a new vivifying map from field name to field initializer
    */
-  private static VivifyingMap<String, AExpression> createFieldInitMap() {
+  @SuppressWarnings("modifiability:return") // The anonymous subclass's constructor result
+  // is the top qualifier, so it does not propagate the backing map's @Modifiable type.
+  private static @Modifiable VivifyingMap<String, AExpression> createFieldInitMap() {
     return new VivifyingMap<>(new LinkedHashMap<>()) {
       @Override
       public AExpression createValueFor(String k) {

annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/el/ADeclaration.java

@@ -5,13 +5,16 @@
 import java.util.TreeMap;
 import org.checkerframework.afu.scenelib.io.ASTPath;
 import org.checkerframework.afu.scenelib.util.coll.VivifyingMap;
+import org.checkerframework.checker.modifiability.qual.Modifiable;
 
 /** A declaration, as opposed to an expression. Base class for AClass, AMethod, and AField. */
 public abstract class ADeclaration extends AElement {
   /**
    * The element's insert-annotation invocations; map key is the AST path to the insertion place.
    */
-  public final VivifyingMap<ASTPath, ATypeElement> insertAnnotations =
+  @SuppressWarnings("modifiability:assignment") // The anonymous subclass's constructor result
+  // is the top qualifier, so it does not propagate the backing map's @Modifiable type.
+  public final @Modifiable VivifyingMap<ASTPath, ATypeElement> insertAnnotations =
       new VivifyingMap<>(new TreeMap<>()) {
         @Override
         public ATypeElement createValueFor(ASTPath k) {
@@ -28,7 +31,9 @@ public boolean isEmptyValue(ATypeElement v) {
    * The element's annotated insert-typecast invocations; map key is the AST path to the insertion
    * place
    */
-  public final VivifyingMap<ASTPath, ATypeElementWithType> insertTypecasts =
+  @SuppressWarnings("modifiability:assignment") // The anonymous subclass's constructor result
+  // is the top qualifier, so it does not propagate the backing map's @Modifiable type.
+  public final @Modifiable VivifyingMap<ASTPath, ATypeElementWithType> insertTypecasts =
       new VivifyingMap<>(new TreeMap<>()) {
         @Override
         public ATypeElementWithType createValueFor(ASTPath k) {

annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/el/AElement.java

@@ -7,6 +7,9 @@
 import java.util.StringJoiner;
 import org.checkerframework.afu.scenelib.Annotation;
 import org.checkerframework.afu.scenelib.util.coll.VivifyingMap;
+import org.checkerframework.checker.modifiability.qual.Growable;
+import org.checkerframework.checker.modifiability.qual.Modifiable;
+import org.checkerframework.checker.modifiability.qual.Replaceable;
 
 /**
  * An {@code AElement} represents a Java element and the annotations it carries. Some {@code
@@ -22,7 +25,7 @@ public class AElement implements Cloneable {
    * The top-level annotations directly on this element. Annotations on subelements are in those
    * subelements' {@code tlAnnotationsHere} sets, not here.
    */
-  public final Set<Annotation> tlAnnotationsHere;
+  public final @Modifiable Set<Annotation> tlAnnotationsHere;
 
   // TODO: What about methods; is `type` the return type?
   /**
@@ -201,7 +204,9 @@ public <R, T> R accept(ElementVisitor<R, T> v, T t) {
    * @param <K> the type of the map keys
    * @return a new vivifying map from keys to {@link AElement}s
    */
-  static <K extends Object> VivifyingMap<K, AElement> newVivifyingLHMap_AE() {
+  @SuppressWarnings("modifiability:return") // The anonymous subclass's constructor result
+  // is the top qualifier, so it does not propagate the backing map's @Modifiable type.
+  static <K extends Object> @Modifiable VivifyingMap<K, AElement> newVivifyingLHMap_AE() {
     return new VivifyingMap<>(new LinkedHashMap<>()) {
       @Override
       public AElement createValueFor(K k) {
@@ -245,7 +250,7 @@ public boolean isEmptyValue(AElement v) {
     // `@Nullable Object`, to `WrapperMap.get(Object)`, whose parameter is `@NonNull`.
   })
   static <K, V extends AElement> void copyMapContents(
-      VivifyingMap<K, V> orig, VivifyingMap<K, V> copy) {
+      VivifyingMap<K, V> orig, @Growable @Replaceable VivifyingMap<K, V> copy) {
     for (K key : orig.keySet()) {
       V val = orig.get(key);
       copy.put(key, (V) val.clone());

annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/el/AExpression.java

@@ -7,44 +7,47 @@
 import java.util.SortedMap;
 import java.util.TreeMap;
 import org.checkerframework.afu.scenelib.util.coll.VivifyingMap;
+import org.checkerframework.checker.modifiability.qual.Modifiable;
 
 /**
  * Manages all annotations within expressions, that is, annotations on typecasts, instanceofs, and
  * object creations. We can use this class for methods, field initializers, and static initializers.
  */
 public class AExpression extends AElement {
   /** The method's annotated typecasts; map key is the offset of the checkcast bytecode. */
-  public final VivifyingMap<RelativeLocation, ATypeElement> typecasts =
+  public final @Modifiable VivifyingMap<RelativeLocation, ATypeElement> typecasts =
       ATypeElement.<RelativeLocation>newVivifyingLHMap_ATE();
 
   /**
    * The method's annotated "instanceof" tests; map key is the offset of the instanceof bytecode.
    */
-  public final VivifyingMap<RelativeLocation, ATypeElement> instanceofs =
+  public final @Modifiable VivifyingMap<RelativeLocation, ATypeElement> instanceofs =
       ATypeElement.<RelativeLocation>newVivifyingLHMap_ATE();
 
   /** The method's annotated "new" invocations; map key is the offset of the new bytecode. */
-  public final VivifyingMap<RelativeLocation, ATypeElement> news =
+  public final @Modifiable VivifyingMap<RelativeLocation, ATypeElement> news =
       ATypeElement.<RelativeLocation>newVivifyingLHMap_ATE();
 
   /**
    * A method invocation's annotated type arguments; map key is the offset of the invokestatic
    * bytecode
    */
-  public final VivifyingMap<RelativeLocation, ATypeElement> calls =
+  public final @Modifiable VivifyingMap<RelativeLocation, ATypeElement> calls =
       ATypeElement.<RelativeLocation>newVivifyingLHMap_ATE();
 
   /**
    * A member reference's annotated type parameters; map key is the offset of the invokestatic
    * bytecode
    */
-  public final VivifyingMap<RelativeLocation, ATypeElement> refs =
+  public final @Modifiable VivifyingMap<RelativeLocation, ATypeElement> refs =
       ATypeElement.<RelativeLocation>newVivifyingLHMap_ATE();
 
   /**
    * The method's annotated lambda expressions; map key is the offset of the invokedynamic bytecode
    */
-  public final VivifyingMap<RelativeLocation, AMethod> funs =
+  @SuppressWarnings("modifiability:assignment") // The anonymous subclass's constructor result
+  // is the top qualifier, so it does not propagate the backing map's @Modifiable type.
+  public final @Modifiable VivifyingMap<RelativeLocation, AMethod> funs =
       new VivifyingMap<>(new LinkedHashMap<>()) {
         @Override
         public AMethod createValueFor(RelativeLocation k) {