Merge branch 'master' into makeDefaultsExplicit

README.md

@@ -1,11 +1,8 @@
-Continuous integration status of master:
-![CFI status](https://github.com/opprop/checker-framework-inference/workflows/CI/badge.svg)
-
-Checker Framework Inference
+Checker Framework Inference [![Build Status](https://github.com/opprop/checker-framework-inference/workflows/CI/badge.svg)](https://github.com/opprop/checker-framework-inference/actions/workflows/main.yml)
 ===========================
 
 This project is a general type inference framework,
-built upon the [Checker Framework](https://checkerframework.org/).
+built upon the [EISOP Checker Framework](https://eisop.github.io/).
 
 Given a program with no type annotations, Checker Framework Inference produces a program with type annotations.
 
@@ -31,7 +28,7 @@ Configure Eclipse to edit Checker Framework Inference
 
 The instructions here assumes you have cloned this project into a folder called `checker-framework-inference`.
 
-1) Follow the instructions in the [Checker Framework Manual](https://checkerframework.org/manual/#building-eclipse)
+1) Follow the instructions in the [EISOP Checker Framework Manual](https://eisop.github.io/cf/manual/manual.html#eclipse)
 to download, build, and configure Eclipse to edit the Checker Framework. The Checker Framework Inference Eclipse
 project depends on the eclipse projects from Checker Framework.
 
@@ -95,7 +92,7 @@ To test the build:
 Execution
 ---------
 
-Verify you have all of the requirements.
+Verify you have all the requirements.
 
 ````
 ./scripts/inference
@@ -119,7 +116,7 @@ Available options are [INFER, TYPECHECK, ROUNDTRIP, ROUNDTRIP_TYPECHECK]
     Generates and solves the constraints and writes the results to default.jaif file
 
   * `TYPECHECK`:
-    Typechecks the existin code
+    Typechecks the existing code
 
   * `ROUNDTRIP`:
     Generates and solves the constraints and then inserts the results
@@ -146,10 +143,10 @@ The classpath that is required by target program.
 `checkers.inference.solver.PropagationSolver` and `checkers.inference.solver.SolverEngine` are real solvers
 at the moment.
 
-Omiting the solver will create an output that numbers all of the
+Omitting the solver will create an output that numbers all the
 annotation positions in the program.
 
-`checkers.inference.solver.DebugSolver` will output all of the
+`checkers.inference.solver.DebugSolver` will output all the
 constraints generated.
 
 
@@ -178,7 +175,7 @@ Specifies what concrete solver is going to use.
 
   * `LogiQL`: Encodes constraints as statements of LogiQL language and use LogicBlox to solve.
 
-  * `Z3` with bit vector theory: Encodes constraints as Max-SMT problem with bit vectory theory, and use Z3 library to solve.
+  * `Z3` with bit vector theory: Encodes constraints as Max-SMT problem with bit vector theory, and use Z3 library to solve.
 
 
   `MaxSat` solver is used by default.
@@ -187,7 +184,7 @@ Specifies what concrete solver is going to use.
 Specifies whether to separate constraints into multiple components through constraint graph and solve them respectively. The default value is true.
 
 * `solveInParallel`
-If constraints are separated by constraint graph, this arguments indicates whether to solve the components in parallel (multithreading). The default value is true.
+If constraints are separated by constraint graph, this argument indicates whether to solve the components in parallel (multithreading). The default value is true.
 
 * `collectStatistics`
 Specifies whether to collect statistic with respect to timing, size of constraints, size of encoding, etc. The default value is false.

build.gradle

@@ -210,7 +210,6 @@ task dist(dependsOn: shadowJar, type: Copy) {
             "will build checker-framework-inference.jar, copy all the relevant runtime jars into " +
             "the dist directory."
     from files(
-            "${checkerFrameworkPath}/checker/dist/jdk8.jar",
             "${checkerFrameworkPath}/checker/dist/checker.jar",
             "${checkerFrameworkPath}/checker/dist/checker-qual.jar",
             "${checkerFrameworkPath}/checker/dist/checker-util.jar",

gradle/wrapper/gradle-wrapper.properties

@@ -1,6 +1,6 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.0.1-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.1.1-bin.zip
 networkTimeout=10000
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

gradlew

@@ -85,9 +85,6 @@ done
 APP_BASE_NAME=${0##*/}
 APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit
 
-# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
-DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
-
 # Use the maximum available, or set MAX_FD != -1 to use that value.
 MAX_FD=maximum
 
@@ -197,6 +194,10 @@ if "$cygwin" || "$msys" ; then
     done
 fi
 
+
+# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
+DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
+
 # Collect all arguments for the java command;
 #   * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of
 #     shell script including quotes and variable substitutions, so put them in

scripts/inference-dev

@@ -34,7 +34,7 @@ libDir="$cfiDir"/lib
 CFBuild="${cfDir}"/dataflow/"${classes}":"${cfDir}"/javacutil/"${classes}":"${cfDir}"/framework/"${classes}":"${cfDir}"/framework/"${resources}"
 CFBuild="${CFBuild}":"${cfDir}"/checker/"${classes}":"${cfDir}"/checker/"${resources}":"${annoToolsDir}"/scene-lib/bin
 
-CFDepJars="${stubparserDir}"/javaparser-core/target/stubparser-3.24.7.jar:"${afuDir}"/annotation-file-utilities-all.jar
+CFDepJars="${stubparserDir}"/javaparser-core/target/stubparser-3.25.1.jar:"${afuDir}"/annotation-file-utilities-all.jar
 
 # sanity check: ensure each jar in CFDepJars actually exists in the file system
 # total number of jars

src/checkers/inference/DefaultSlotManager.java

@@ -11,6 +11,7 @@
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.AnnotationMirrorMap;
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.BugInCF;
 import org.checkerframework.javacutil.TreeUtils;
@@ -164,7 +165,7 @@ public DefaultSlotManager( final ProcessingEnvironment processingEnvironment,
         this.varAnnot = builder.build();
 
         // Construct empty caches
-        constantCache = AnnotationUtils.createAnnotationMap();
+        constantCache = new AnnotationMirrorMap<>();
         locationCache = new LinkedHashMap<>();
         existentialSlotPairCache = new LinkedHashMap<>();
         combSlotPairCache = new LinkedHashMap<>();

src/checkers/inference/InferenceAnnotatedTypeFactory.java

@@ -24,10 +24,10 @@
 import org.checkerframework.framework.type.typeannotator.TypeAnnotator;
 import org.checkerframework.framework.type.visitor.AnnotatedTypeScanner;
 import org.checkerframework.framework.util.AnnotatedTypes;
-import org.checkerframework.framework.util.AnnotationMirrorSet;
 import org.checkerframework.framework.util.defaults.QualifierDefaults;
 import org.checkerframework.framework.util.dependenttypes.DependentTypesHelper;
 import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.AnnotationMirrorSet;
 import org.checkerframework.javacutil.BugInCF;
 import org.checkerframework.javacutil.ElementUtils;
 import org.checkerframework.javacutil.Pair;
@@ -342,8 +342,19 @@ public ParameterizedExecutableType methodFromUse(final MethodInvocationTree meth
             viewpointAdapter.viewpointAdaptMethod(receiverType, methodElem, methodOfReceiver);
         }
         ParameterizedExecutableType mType = substituteTypeArgs(methodInvocationTree, methodElem, methodOfReceiver);
-
         AnnotatedExecutableType method = mType.executableType;
+
+        // Take adapt parameter logic from AnnotatedTypeFactory#methodFromUse to
+        // InferenceAnnotatedTypeFactory#methodFromUse.
+        // Store varargType before calling setParameterTypes, otherwise we may lose the varargType
+        // as it is the last element of the original parameterTypes.
+        method.computeVarargType();
+        // Adapt parameters, which makes parameters and arguments be the same size for later
+        // checking.
+        List<AnnotatedTypeMirror> parameters =
+                AnnotatedTypes.adaptParameters(this, method, methodInvocationTree.getArguments());
+        method.setParameterTypes(parameters);
+
         inferencePoly.replacePolys(methodInvocationTree, method);
 
         if (methodInvocationTree.getKind() == Tree.Kind.METHOD_INVOCATION &&
@@ -383,7 +394,19 @@ public ParameterizedExecutableType constructorFromUse(final NewClassTree newClas
         addComputedTypeAnnotations(newClassTree, constructorReturnType);
 
         final AnnotatedExecutableType constructorType = AnnotatedTypes.asMemberOf(types, this, constructorReturnType, constructorElem);
-
+        // Take adapt parameter logic from AnnotatedTypeFactory#constructorFromUse to
+        // InferenceAnnotatedTypeFactory#constructorFromUse.
+        // Store varargType before calling setParameterTypes, otherwise we may lose the
+        // varargType as it is the last element of the original parameterTypes.
+        // AnnotatedTypes.asMemberOf handles vararg type properly, so we do not need to compute
+        // vararg type again.
+        constructorType.computeVarargType();
+        // Adapt parameters, which makes parameters and arguments be the same size for later
+        // checking. The vararg type of con has been already computed and stored when calling
+        // typeVarSubstitutor.substitute.
+        List<AnnotatedTypeMirror> parameters =
+                AnnotatedTypes.adaptParameters(this, constructorType, newClassTree.getArguments());
+        constructorType.setParameterTypes(parameters);
         if (viewpointAdapter != null) {
             viewpointAdapter.viewpointAdaptConstructor(constructorReturnType, constructorElem, constructorType);
         }
@@ -570,11 +593,11 @@ protected InferenceViewpointAdapter createViewpointAdapter() {
      * @return the singleton set with the {@link VarAnnot} on the class bound
      */
     @Override
-    public Set<AnnotationMirror> getTypeDeclarationBounds(TypeMirror type) {
+    public AnnotationMirrorSet getTypeDeclarationBounds(TypeMirror type) {
         final TypeElement elt = (TypeElement) getProcessingEnv().getTypeUtils().asElement(type);
         AnnotationMirror vAnno = variableAnnotator.getClassDeclVarAnnot(elt);
         if (vAnno != null) {
-            return Collections.singleton(vAnno);
+            return AnnotationMirrorSet.singleton(vAnno);
         }
 
         // This is to handle the special case of anonymous classes when the super class (or interface)
@@ -587,11 +610,11 @@ public Set<AnnotationMirror> getTypeDeclarationBounds(TypeMirror type) {
         if (realAnno != null) {
             Slot slot = slotManager.getSlot(realAnno);
             vAnno = slotManager.getAnnotation(slot);
-            return Collections.singleton(vAnno);
+            return AnnotationMirrorSet.singleton(vAnno);
         }
 
         // If the declaration bound of the underlying type is not cached, use default
-        return (Set<AnnotationMirror>) getDefaultTypeDeclarationBounds();
+        return (AnnotationMirrorSet) getDefaultTypeDeclarationBounds();
     }
 
     /**

src/checkers/inference/InferenceQualifierHierarchy.java

@@ -10,10 +10,10 @@
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.framework.type.ElementQualifierHierarchy;
 import org.checkerframework.framework.type.QualifierHierarchy;
-import org.checkerframework.framework.util.AnnotationMirrorSet;
 import org.checkerframework.framework.util.DefaultQualifierKindHierarchy;
 import org.checkerframework.framework.util.QualifierKind;
 import org.checkerframework.framework.util.QualifierKindHierarchy;
+import org.checkerframework.javacutil.AnnotationMirrorSet;
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.BugInCF;
 import org.plumelib.util.StringsPlume;
@@ -196,7 +196,7 @@ public Set<? extends AnnotationMirror> leastUpperBounds(
             Collection<? extends AnnotationMirror> annos1,
             Collection<? extends AnnotationMirror> annos2) {
         if (InferenceMain.isHackMode(annos1.size() != annos2.size())) {
-            Set<AnnotationMirror> result = AnnotationUtils.createAnnotationSet();
+            Set<AnnotationMirror> result = new AnnotationMirrorSet();
             for (AnnotationMirror a1 : annos1) {
                 for (AnnotationMirror a2 : annos2) {
                     AnnotationMirror lub = leastUpperBound(a1, a2);

src/checkers/inference/VariableAnnotator.java

@@ -13,6 +13,7 @@
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType;
 import org.checkerframework.framework.type.visitor.AnnotatedTypeScanner;
 import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.AnnotationMirrorSet;
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.ElementUtils;
 import org.checkerframework.javacutil.BugInCF;
@@ -239,7 +240,7 @@ private SourceVariableSlot createVariable(final Tree tree) {
 
         final Pair<Slot, Set<? extends AnnotationMirror>> varATMPair = Pair
                 .<Slot, Set<? extends AnnotationMirror>> of(varSlot,
-                AnnotationUtils.createAnnotationSet());
+                        new AnnotationMirrorSet());
         treeToVarAnnoPair.put(tree, varATMPair);
         logger.fine("Created variable for tree:\n" + varSlot.getId() + " => " + tree);
         return varSlot;
@@ -270,7 +271,7 @@ public ConstantSlot createConstant(final AnnotationMirror value, final Tree tree
 //
 //            }
 //        }
-        Set<AnnotationMirror> annotations = AnnotationUtils.createAnnotationSet();
+        Set<AnnotationMirror> annotations = new AnnotationMirrorSet();
         annotations.add(constantSlot.getValue());
         final Pair<Slot, Set<? extends AnnotationMirror>> varATMPair = Pair
                 .<Slot, Set<? extends AnnotationMirror>> of(constantSlot,
@@ -518,7 +519,7 @@ private Slot addPrimaryVariable(AnnotatedTypeMirror atm, final Tree tree) {
 
             final Pair<Slot, Set<? extends AnnotationMirror>> varATMPair = Pair
                     .of(variable,
-                    AnnotationUtils.createAnnotationSet());
+                    new AnnotationMirrorSet());
 
             treeToVarAnnoPair.put(tree, varATMPair);
         }

src/checkers/inference/dataflow/InferenceAnalysis.java

@@ -15,6 +15,7 @@
 import org.checkerframework.framework.flow.CFTransfer;
 import org.checkerframework.framework.flow.CFValue;
 import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
+import org.checkerframework.javacutil.AnnotationMirrorSet;
 import org.checkerframework.javacutil.BugInCF;
 import org.checkerframework.javacutil.Pair;
 
@@ -71,7 +72,7 @@ public InferenceAnalysis(
      */
     @Override
     public CFValue defaultCreateAbstractValue(CFAbstractAnalysis<CFValue, ?, ?> analysis,
-                                              Set<AnnotationMirror> annos,
+                                              AnnotationMirrorSet annos,
                                               TypeMirror underlyingType) {
 
         if (annos.size() == 0 && underlyingType.getKind() != TypeKind.TYPEVAR) {

src/checkers/inference/dataflow/InferenceValue.java

@@ -7,6 +7,7 @@
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable;
 import org.checkerframework.framework.type.QualifierHierarchy;
 import org.checkerframework.framework.util.AnnotationFormatter;
+import org.checkerframework.javacutil.AnnotationMirrorSet;
 import org.checkerframework.javacutil.TypesUtils;
 
 import java.util.Collections;
@@ -37,7 +38,7 @@
 public class InferenceValue extends CFValue {
 
 
-    public InferenceValue(InferenceAnalysis analysis, Set<AnnotationMirror> annotations, TypeMirror underlyingType) {
+    public InferenceValue(InferenceAnalysis analysis, AnnotationMirrorSet annotations, TypeMirror underlyingType) {
         super(analysis, annotations, underlyingType);
     }
 
@@ -69,7 +70,7 @@ public CFValue leastUpperBound(CFValue other) {
         // the two VarAnnos getting from slotManager.
         final AnnotationMirror lub = qualifierHierarchy.leastUpperBound(anno1, anno2);
 
-        return analysis.createAbstractValue(Collections.singleton(lub), getLubType(other, null));
+        return analysis.createAbstractValue(AnnotationMirrorSet.singleton(lub), getLubType(other, null));
     }
 
     public Slot getEffectiveSlot(final CFValue value) {

src/checkers/inference/solver/backend/maxsat/MaxSatFormatTranslator.java

@@ -12,6 +12,7 @@
 import checkers.inference.solver.backend.AbstractFormatTranslator;
 import checkers.inference.solver.backend.encoder.ConstraintEncoderFactory;
 import checkers.inference.solver.backend.maxsat.encoder.MaxSATConstraintEncoderFactory;
+import org.checkerframework.javacutil.AnnotationMirrorMap;
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.sat4j.core.VecInt;
 
@@ -41,7 +42,7 @@ public class MaxSatFormatTranslator extends AbstractFormatTranslator<VecInt[], V
     public MaxSatFormatTranslator(Lattice lattice) {
         super(lattice);
         // Initialize mappings between type and int.
-        Map<AnnotationMirror, Integer>typeToIntRes = AnnotationUtils.createAnnotationMap();
+        Map<AnnotationMirror, Integer>typeToIntRes = new AnnotationMirrorMap<>();
         Map<Integer, AnnotationMirror> intToTypeRes = new HashMap<Integer, AnnotationMirror>();
 
         int curInt = 0;

src/checkers/inference/solver/frontend/LatticeBuilder.java

@@ -12,6 +12,8 @@
 import checkers.inference.InferenceMain;
 import org.checkerframework.framework.type.QualifierHierarchy;
 import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.AnnotationMirrorMap;
+import org.checkerframework.javacutil.AnnotationMirrorSet;
 import org.checkerframework.javacutil.AnnotationUtils;
 
 import checkers.inference.model.ConstantSlot;
@@ -66,10 +68,10 @@ public class LatticeBuilder {
     public final Collection<AnnotationMirror> allAnnotations;
 
     public LatticeBuilder() {
-        subType = AnnotationUtils .createAnnotationMap();
-        superType = AnnotationUtils.createAnnotationMap();
-        incomparableType = AnnotationUtils.createAnnotationMap();
-        allAnnotations = AnnotationUtils.createAnnotationSet();
+        subType = new AnnotationMirrorMap<>();
+        superType = new AnnotationMirrorMap<>();
+        incomparableType = new AnnotationMirrorMap<>();
+        allAnnotations = new AnnotationMirrorSet();
 
     }
 
@@ -82,7 +84,7 @@ public LatticeBuilder() {
     public Lattice buildLattice(QualifierHierarchy qualHierarchy, Collection<Slot> slots) {
         clear();
 
-        Set<AnnotationMirror> supportedAnnos = AnnotationUtils.createAnnotationSet();
+        Set<AnnotationMirror> supportedAnnos = new AnnotationMirrorSet();
         Set<Class<? extends Annotation>> annoClasses =
                 InferenceMain.getInstance().getRealTypeFactory().getSupportedTypeQualifiers();
         for (Class<? extends Annotation> ac: annoClasses) {
@@ -145,7 +147,7 @@ public Lattice buildLattice(QualifierHierarchy qualHierarchy, Collection<Slot> s
      */
     public TwoQualifiersLattice buildTwoTypeLattice(AnnotationMirror top, AnnotationMirror bottom) {
         clear();
-        Set<AnnotationMirror> tempSet = AnnotationUtils.createAnnotationSet();
+        Set<AnnotationMirror> tempSet = new AnnotationMirrorSet();
         tempSet.add(top);
         tempSet.add(bottom);
         allTypes = Collections.unmodifiableSet(tempSet);
@@ -154,8 +156,8 @@ public TwoQualifiersLattice buildTwoTypeLattice(AnnotationMirror top, Annotation
         numTypes = 2;
 
         // Calculate subertypes map and supertypes map.
-        Set<AnnotationMirror> topSet = AnnotationUtils.createAnnotationSet();
-        Set<AnnotationMirror> bottomSet = AnnotationUtils.createAnnotationSet();
+        Set<AnnotationMirror> topSet = new AnnotationMirrorSet();
+        Set<AnnotationMirror> bottomSet = new AnnotationMirrorSet();
         topSet.add(top);
         bottomSet.add(bottom);
         subType.put(top, Collections.unmodifiableSet(allTypes));