Features to enable PICO

src/checkers/inference/InferenceLauncher.java

@@ -223,7 +223,9 @@ public void infer() {
 
         Mode mode = Mode.valueOf(InferenceOptions.mode);
         if (InferenceOptions.makeDefaultsExplicit
-                && (mode == Mode.ROUNDTRIP || mode == Mode.ROUNDTRIP_TYPECHECK)) {
+                && (mode == Mode.ROUNDTRIP
+                        || mode == Mode.ROUNDTRIP_TYPECHECK
+                        || mode == Mode.INFER)) {
             // Two conditions have to be met to make defaults explicit:
             // 1. the command-line flag `makeDefaultsExplicit` is provided
             // 2. the inference solution will be written back to the source code (roundtrip `mode`)

src/checkers/inference/InferenceVisitor.java

@@ -25,12 +25,14 @@
 import org.checkerframework.framework.type.AnnotatedTypeParameterBounds;
 import org.checkerframework.framework.util.AnnotatedTypes;
 import org.checkerframework.javacutil.*;
+import org.checkerframework.javacutil.TreeUtils;
 import org.plumelib.util.ArraysPlume;
 
 import java.lang.annotation.Annotation;
 import java.util.Arrays;
 import java.util.HashMap;
 import java.util.HashSet;
+import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
@@ -79,12 +81,11 @@ public class InferenceVisitor<
     protected final boolean infer;
 
     protected final Checker realChecker;
-
-    /**
+    /*
      * Map from type-use location to a list of qualifiers which cannot be used on that location.
      * This is used to create the inequality constraint in inference.
      */
-    protected final Map<TypeUseLocation, Set<AnnotationMirror>> locationToIllegalQuals;
+    protected final Map<TypeUseLocation, AnnotationMirrorSet> locationToIllegalQuals;
 
     public InferenceVisitor(
             Checker checker, InferenceChecker ichecker, Factory factory, boolean infer) {
@@ -307,6 +308,50 @@ public void mainIsNoneOf(
         }
     }
 
+    private void addDeepPreferenceImpl(
+            AnnotatedTypeMirror ty,
+            AnnotationMirror goal,
+            int weight,
+            java.util.List<AnnotatedTypeMirror> visited,
+            Tree node) {
+        if (infer) {
+            if (visited.contains(ty)) {
+                return;
+            }
+            visited.add(ty);
+
+            final SlotManager slotManager = InferenceMain.getInstance().getSlotManager();
+            Slot el = slotManager.getSlot(ty);
+
+            if (el == null) {
+                logger.warning(
+                        "InferenceVisitor::addDeepPreferenceImpl: no annotation in type: " + ty);
+            } else {
+                addPreference(ty, goal, weight);
+            }
+
+            if (ty.getKind() == TypeKind.DECLARED) {
+                AnnotatedDeclaredType declaredType = (AnnotatedDeclaredType) ty;
+                for (AnnotatedTypeMirror typearg : declaredType.getTypeArguments()) {
+                    addDeepPreferenceImpl(typearg, goal, weight, visited, node);
+                }
+            } else if (ty.getKind() == TypeKind.ARRAY) {
+                AnnotatedArrayType arrayType = (AnnotatedArrayType) ty;
+                addDeepPreferenceImpl(arrayType.getComponentType(), goal, weight, visited, node);
+            } else if (ty.getKind() == TypeKind.TYPEVAR) {
+                AnnotatedTypeVariable atv = (AnnotatedTypeVariable) ty;
+                addDeepPreferenceImpl(atv.getUpperBound(), goal, weight, visited, node);
+                addDeepPreferenceImpl(atv.getLowerBound(), goal, weight, visited, node);
+            }
+        }
+        // Else, do nothing
+    }
+
+    public void addDeepPreference(
+            AnnotatedTypeMirror ty, AnnotationMirror goal, int weight, Tree node) {
+        addDeepPreferenceImpl(ty, goal, weight, new LinkedList<>(), node);
+    }
+
     public void addPreference(AnnotatedTypeMirror type, AnnotationMirror anno, int weight) {
         if (infer) {
             ConstraintManager cManager = InferenceMain.getInstance().getConstraintManager();
@@ -983,18 +1028,18 @@ protected void checkConstructorResult(
      * @return a mapping from type-use locations to a set of qualifiers which cannot be applied to
      *     that location
      */
-    protected Map<TypeUseLocation, Set<AnnotationMirror>> createMapForIllegalQuals() {
-        Map<TypeUseLocation, Set<AnnotationMirror>> locationToIllegalQuals = new HashMap<>();
+    protected Map<TypeUseLocation, AnnotationMirrorSet> createMapForIllegalQuals() {
+        Map<TypeUseLocation, AnnotationMirrorSet> locationToIllegalQuals = new HashMap<>();
         // First, init each type-use location to contain all type qualifiers.
         Set<Class<? extends Annotation>> supportQualifiers =
                 atypeFactory.getSupportedTypeQualifiers();
-        Set<AnnotationMirror> supportedAnnos = new AnnotationMirrorSet();
+        AnnotationMirrorSet supportedAnnos = new AnnotationMirrorSet();
         for (Class<? extends Annotation> qual : supportQualifiers) {
             supportedAnnos.add(
                     new AnnotationBuilder(atypeFactory.getProcessingEnv(), qual).build());
         }
         for (TypeUseLocation location : TypeUseLocation.values()) {
-            locationToIllegalQuals.put(location, new HashSet<>(supportedAnnos));
+            locationToIllegalQuals.put(location, new AnnotationMirrorSet(supportedAnnos));
         }
         // Then, delete some qualifiers which can be applied to that type-use location.
         // this leaves only qualifiers not allowed on that location.
@@ -1005,7 +1050,7 @@ protected Map<TypeUseLocation, Set<AnnotationMirror>> createMapForIllegalQuals()
             // the qualifier can be written on any type use.
             if (tls == null) {
                 for (TypeUseLocation location : TypeUseLocation.values()) {
-                    Set<AnnotationMirror> amSet = locationToIllegalQuals.get(location);
+                    AnnotationMirrorSet amSet = locationToIllegalQuals.get(location);
                     amSet.remove(
                             AnnotationUtils.getAnnotationByName(
                                     supportedAnnos, qual.getCanonicalName()));
@@ -1015,14 +1060,14 @@ protected Map<TypeUseLocation, Set<AnnotationMirror>> createMapForIllegalQuals()
             for (TypeUseLocation location : tls.value()) {
                 if (location == TypeUseLocation.ALL) {
                     for (TypeUseLocation val : TypeUseLocation.values()) {
-                        Set<AnnotationMirror> amSet = locationToIllegalQuals.get(val);
+                        AnnotationMirrorSet amSet = locationToIllegalQuals.get(val);
                         amSet.remove(
                                 AnnotationUtils.getAnnotationByName(
                                         supportedAnnos, qual.getCanonicalName()));
                     }
                     break;
                 }
-                Set<AnnotationMirror> amSet = locationToIllegalQuals.get(location);
+                AnnotationMirrorSet amSet = locationToIllegalQuals.get(location);
                 amSet.remove(
                         AnnotationUtils.getAnnotationByName(
                                 supportedAnnos, qual.getCanonicalName()));
@@ -1037,7 +1082,6 @@ protected void validateVariablesTargetLocation(Tree tree, AnnotatedTypeMirror ty
             super.validateVariablesTargetLocation(tree, type);
             return;
         }
-
         if (ignoreTargetLocations) {
             return;
         }
@@ -1068,6 +1112,9 @@ protected void validateVariablesTargetLocation(Tree tree, AnnotatedTypeMirror ty
                     break;
                 case ENUM_CONSTANT:
                     location = TypeUseLocation.CONSTRUCTOR_RESULT;
+                    // TODO: Add ? mainIsNoneOf(type,
+                    // targetLocationToAnno.get(TypeUseLocation.FIELD).toArray(mirrors),
+                    // "type.invalid.annotations.on.location", tree);
                     break;
                 default:
                     throw new BugInCF("Location not matched");

src/checkers/inference/VariableAnnotator.java

@@ -793,7 +793,7 @@ public Void visitDeclared(final AnnotatedDeclaredType adt, final Tree tree) {
         return null;
     }
 
-    private boolean handleWasRawDeclaredTypes(AnnotatedDeclaredType adt) {
+    protected boolean handleWasRawDeclaredTypes(AnnotatedDeclaredType adt) {
         if (adt.isUnderlyingTypeRaw() && adt.getTypeArguments().size() != 0) {
             // the type arguments should be wildcards AND if I get the real type of "tree"
             // it corresponds to the declaration of adt.getUnderlyingType
@@ -1855,7 +1855,7 @@ public AnnotationMirror getClassDeclVarAnnot(TypeElement ele) {
         return null;
     }
 
-    private void addDeclarationConstraints(Slot declSlot, Slot instanceSlot) {
+    protected void addDeclarationConstraints(Slot declSlot, Slot instanceSlot) {
         constraintManager.addSubtypeConstraint(instanceSlot, declSlot);
     }
 

src/checkers/inference/util/SlotDefaultTypeResolver.java

@@ -3,6 +3,7 @@
 import com.sun.source.tree.AnnotatedTypeTree;
 import com.sun.source.tree.ArrayTypeTree;
 import com.sun.source.tree.ClassTree;
+import com.sun.source.tree.NewClassTree;
 import com.sun.source.tree.ParameterizedTypeTree;
 import com.sun.source.tree.PrimitiveTypeTree;
 import com.sun.source.tree.Tree;
@@ -181,5 +182,22 @@ public Void visitAnnotatedType(AnnotatedTypeTree tree, Void unused) {
 
             return super.visitAnnotatedType(tree, unused);
         }
+
+        @Override
+        public Void visitNewClass(NewClassTree tree, Void unused) {
+            AnnotatedTypeMirror defaultType = getDefaultTypeFor(tree);
+            if (InferenceUtil.isAnonymousClass(tree)) {
+                // don't associate the identifier with the defaultType if it's an anonymousclass
+                // should associate the identifier with the direct super type of the defaultType.
+                // choose the last one of the directSupertypes, which is either the direct super
+                // class
+                // or implemented interface
+                List<? extends AnnotatedTypeMirror> superTypes = defaultType.directSupertypes();
+                defaultTypes.put(tree.getIdentifier(), superTypes.get(superTypes.size() - 1));
+            } else {
+                defaultTypes.put(tree.getIdentifier(), defaultType);
+            }
+            return super.visitNewClass(tree, unused);
+        }
     }
 }

tests/checkers/inference/test/CFInferenceTest.java

@@ -33,6 +33,10 @@ public boolean useHacks() {
         return SystemPlume.getBooleanSystemProperty("use.hacks");
     }
 
+    public boolean makeDefaultsExplicit() {
+        return false;
+    }
+
     public abstract IPair<String, List<String>> getSolverNameAndOptions();
 
     public List<String> getAdditionalInferenceOptions() {
@@ -66,6 +70,7 @@ public void run() {
                         solverArgs.first,
                         solverArgs.second,
                         useHacks(),
+                        makeDefaultsExplicit(),
                         shouldEmitDebugInfo,
                         getPathToAfuScripts(),
                         getPathToInferenceScript());

tests/checkers/inference/test/ImmutableInferenceTestConfiguration.java

@@ -16,6 +16,7 @@ public class ImmutableInferenceTestConfiguration implements InferenceTestConfigu
     private final String solver;
     private final Map<String, String> solverArgs;
     private final boolean shouldUseHacks;
+    private final boolean makeDefaultsExplicit;
     private final String pathToAfuScripts;
     private final String pathToInferenceScript;
     private final TestConfiguration initialConfig;
@@ -28,6 +29,7 @@ public ImmutableInferenceTestConfiguration(
             String solver,
             Map<String, String> solverArgs,
             boolean shouldUseHacks,
+            boolean makeDefaultsExplicit,
             String pathToAfuScripts,
             String pathToInferenceScript,
             TestConfiguration initialConfig) {
@@ -38,6 +40,7 @@ public ImmutableInferenceTestConfiguration(
         this.solver = solver;
         this.solverArgs = solverArgs;
         this.shouldUseHacks = shouldUseHacks;
+        this.makeDefaultsExplicit = makeDefaultsExplicit;
         this.pathToAfuScripts = pathToAfuScripts;
         this.initialConfig = initialConfig;
         this.pathToInferenceScript = pathToInferenceScript;
@@ -76,6 +79,10 @@ public boolean shouldUseHacks() {
         return shouldUseHacks;
     }
 
+    public boolean makeDefaultsExplicit() {
+        return makeDefaultsExplicit;
+    }
+
     public String getPathToAfuScripts() {
         return pathToAfuScripts;
     }

tests/checkers/inference/test/InferenceTestConfiguration.java

@@ -26,6 +26,8 @@ public interface InferenceTestConfiguration {
 
     boolean shouldUseHacks();
 
+    boolean makeDefaultsExplicit();
+
     String getPathToAfuScripts();
 
     String getPathToInferenceScript();

tests/checkers/inference/test/InferenceTestConfigurationBuilder.java

@@ -17,6 +17,7 @@ public class InferenceTestConfigurationBuilder {
     private File testDataDir = null;
     private String solver = null;
     private boolean shouldUseHacks;
+    private boolean makeDefaultsExplicit;
     private String pathToAfuScripts = "";
     private String pathToInferenceScript = "";
 
@@ -60,6 +61,11 @@ public InferenceTestConfigurationBuilder setShouldUseHacks(boolean shouldUseHack
         return this;
     }
 
+    public InferenceTestConfigurationBuilder setMakeDefaultsExplicit(boolean makeDefaultsExplicit) {
+        this.makeDefaultsExplicit = makeDefaultsExplicit;
+        return this;
+    }
+
     public InferenceTestConfigurationBuilder setPathToAfuScripts(String pathToAfuScripts) {
         this.pathToAfuScripts = pathToAfuScripts;
         return this;
@@ -166,6 +172,7 @@ public InferenceTestConfiguration build() {
                 solver,
                 new LinkedHashMap<>(solverArgs.getOptions()),
                 shouldUseHacks,
+                makeDefaultsExplicit,
                 pathToAfuScripts,
                 pathToInferenceScript,
                 initialConfiguration);
@@ -196,6 +203,7 @@ public static InferenceTestConfiguration buildDefaultConfiguration(
             String solverName,
             List<String> solverOptions,
             boolean shouldUseHacks,
+            boolean makeDefaultsExplicit,
             boolean shouldEmitDebugInfo,
             String pathToAfuScripts,
             String pathToInferenceScript) {
@@ -216,6 +224,7 @@ public static InferenceTestConfiguration buildDefaultConfiguration(
                         .setAnnotatedSourceDir(defaultAnnotatedSourceDir)
                         .setSolver(solverName)
                         .setShouldUseHacks(shouldUseHacks)
+                        .setMakeDefaultsExplicit(makeDefaultsExplicit)
                         .setPathToAfuScripts(pathToAfuScripts)
                         .setPathToInferenceScript(pathToInferenceScript);
 

tests/checkers/inference/test/InferenceTestExecutor.java

@@ -82,6 +82,9 @@ public static InferenceResult infer(InferenceTestConfiguration configuration) {
         if (configuration.shouldUseHacks()) {
             options.add("--hacks");
         }
+        if (configuration.makeDefaultsExplicit()) {
+            options.add("--makeDefaultsExplicit");
+        }
 
         options.add("--jaifFile=" + configuration.getOutputJaif().getAbsolutePath());