Stop writing solutions that are equivalent to default annotations

src/checkers/inference/DefaultSlotManager.java

@@ -1,13 +1,23 @@
 package checkers.inference;
 
+import checkers.inference.util.SlotDefaultTypeResolver;
+import com.sun.source.tree.CompilationUnitTree;
+import com.sun.source.tree.Tree;
+import com.sun.tools.javac.code.Symbol;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
+import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.javacutil.AnnotationBuilder;
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.BugInCF;
+import org.checkerframework.javacutil.TypeKindUtils;
+import org.checkerframework.javacutil.TypesUtils;
 
 import java.lang.annotation.Annotation;
 import java.util.ArrayList;
 import java.util.Comparator;
+import java.util.HashMap;
 import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
@@ -17,6 +27,9 @@
 import javax.annotation.processing.ProcessingEnvironment;
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.AnnotationValue;
+import javax.lang.model.element.Element;
+import javax.lang.model.element.Name;
+import javax.lang.model.element.TypeElement;
 import javax.lang.model.type.TypeKind;
 import javax.lang.model.type.TypeMirror;
 
@@ -35,8 +48,8 @@
 import checkers.inference.model.SourceVariableSlot;
 import checkers.inference.model.VariableSlot;
 import checkers.inference.qual.VarAnnot;
-import org.checkerframework.javacutil.TypeKindUtils;
-import org.checkerframework.javacutil.TypesUtils;
+import scenelib.annotations.io.ASTIndex;
+import scenelib.annotations.io.ASTRecord;
 
 /**
  * The default implementation of SlotManager.
@@ -46,6 +59,12 @@ public class DefaultSlotManager implements SlotManager {
 
     private final AnnotationMirror varAnnot;
 
+    /**
+     * The top annotation in the real qualifier hierarchy.
+     * Currently, we assume there's only one top.
+     */
+    private final AnnotationMirror realTop;
+
     // This id starts at 1 because in some serializer's
     // (CnfSerializer) 0 is used as line delimiters.
     // Monotonically increasing id for all VariableSlots (including
@@ -94,6 +113,12 @@ public class DefaultSlotManager implements SlotManager {
     private final Map<Pair<Slot, Slot>, Integer> lubSlotPairCache;
     private final Map<Pair<Slot, Slot>, Integer> glbSlotPairCache;
 
+    /**
+     * A map of tree to {@link AnnotationMirror} for caching
+     * a set of pre-computed default types for the current compilation unit.
+     */
+    private final Map<Tree, AnnotationMirror> defaultAnnotationsCache;
+
     /**
      * A map of {@link AnnotationLocation} to {@link Integer} for caching
      * {@link ArithmeticVariableSlot}s. The annotation location uniquely identifies an
@@ -122,9 +147,11 @@ public class DefaultSlotManager implements SlotManager {
     private final ProcessingEnvironment processingEnvironment;
 
     public DefaultSlotManager( final ProcessingEnvironment processingEnvironment,
+                               final AnnotationMirror realTop,
                                final Set<Class<? extends Annotation>> realQualifiers,
                                boolean storeConstants) {
         this.processingEnvironment = processingEnvironment;
+        this.realTop = realTop;
         // sort the qualifiers so that they are always assigned the same varId
         this.realQualifiers = sortAnnotationClasses(realQualifiers);
         slots = new LinkedHashMap<>();
@@ -143,6 +170,7 @@ public DefaultSlotManager( final ProcessingEnvironment processingEnvironment,
         arithmeticSlotCache = new LinkedHashMap<>();
         comparisonThenSlotCache = new LinkedHashMap<>();
         comparisonElseSlotCache = new LinkedHashMap<>();
+        defaultAnnotationsCache = new LinkedHashMap<>();
 
         if (storeConstants) {
             for (Class<? extends Annotation> annoClass : this.realQualifiers) {
@@ -319,13 +347,38 @@ public int getNumberOfSlots() {
         return nextId - 1;
     }
 
+    @Override
+    public void setRoot(CompilationUnitTree compilationUnit) {
+        this.defaultAnnotationsCache.clear();
+
+        BaseAnnotatedTypeFactory realTypeFactory = InferenceMain.getInstance().getRealTypeFactory();
+        Map<Tree, AnnotatedTypeMirror> defaultTypes = SlotDefaultTypeResolver.resolve(
+                compilationUnit,
+                realTypeFactory
+        );
+
+        for (Map.Entry<Tree, AnnotatedTypeMirror> entry : defaultTypes.entrySet()) {
+            // find default types in the current hierarchy and save them to the cache
+            this.defaultAnnotationsCache.put(
+                    entry.getKey(),
+                    entry.getValue().getAnnotationInHierarchy(this.realTop)
+            );
+        }
+    }
+
     @Override
     public SourceVariableSlot createSourceVariableSlot(AnnotationLocation location, TypeMirror type) {
+        AnnotationMirror defaultAnnotation = null;
+        if (!InferenceOptions.makeDefaultsExplicit) {
+            // retrieve the default annotation when needed
+            defaultAnnotation = getDefaultAnnotationForLocation(location, type);
+        }
+
         SourceVariableSlot sourceVarSlot;
         if (location.getKind() == AnnotationLocation.Kind.MISSING) {
             if (InferenceMain.isHackMode()) {
                 //Don't cache slot for MISSING LOCATION. Just create a new one and return.
-                sourceVarSlot = new SourceVariableSlot(nextId(), location, type, true);
+                sourceVarSlot = new SourceVariableSlot(nextId(), location, type, defaultAnnotation, true);
                 addToSlots(sourceVarSlot);
             } else {
                 throw new BugInCF("Creating SourceVariableSlot on MISSING_LOCATION!");
@@ -335,13 +388,95 @@ public SourceVariableSlot createSourceVariableSlot(AnnotationLocation location,
             int id = locationCache.get(location);
             sourceVarSlot = (SourceVariableSlot) getSlot(id);
         } else {
-            sourceVarSlot = new SourceVariableSlot(nextId(), location, type, true);
+            sourceVarSlot = new SourceVariableSlot(nextId(), location, type, defaultAnnotation, true);
             addToSlots(sourceVarSlot);
             locationCache.put(location, sourceVarSlot.getId());
         }
         return sourceVarSlot;
     }
 
+    /**
+     * Find the default annotation for this location by checking the real type factory.
+     * @param location location to create a new {@link SourceVariableSlot}
+     * @return the default annotation for the given location
+     */
+    private @Nullable AnnotationMirror getDefaultAnnotationForLocation(AnnotationLocation location, TypeMirror type) {
+        if (location == AnnotationLocation.MISSING_LOCATION) {
+            if (InferenceMain.isHackMode()) {
+                return null;
+            } else {
+                throw new BugInCF("Getting default annotation for missing location!");
+            }
+        }
+
+        final Tree tree; // the tree associated with the location
+        BaseAnnotatedTypeFactory realTypeFactory = InferenceMain.getInstance().getRealTypeFactory();
+
+        if (location instanceof AnnotationLocation.AstPathLocation) {
+            tree = getTreeForLocation((AnnotationLocation.AstPathLocation) location);
+        } else if (location instanceof AnnotationLocation.ClassDeclLocation) {
+            tree = getTreeForLocation(
+                    (AnnotationLocation.ClassDeclLocation) location,
+                    type,
+                    realTypeFactory
+            );
+        } else {
+            throw new BugInCF("Unable to find default annotation for location " + location);
+        }
+
+        AnnotationMirror realAnnotation = null;
+        if (tree != null) {
+            realAnnotation = this.defaultAnnotationsCache.get(tree);
+            if (realAnnotation == null) {
+                // If its default type can't be found in the cache, we can
+                // fallback to the simplest method.
+                realAnnotation = realTypeFactory.getAnnotatedType(tree).getAnnotationInHierarchy(this.realTop);
+            }
+        }
+        return realAnnotation;
+    }
+
+    /**
+     * Find the tree associated with the given {@link AnnotationLocation.AstPathLocation}.
+     * @param location location to find the tree
+     * @return the tree associated with the given location, which can be null if the location
+     *      is not under the current compilation unit
+     */
+    private @Nullable Tree getTreeForLocation(AnnotationLocation.AstPathLocation location) {
+        ASTRecord astRecord = location.getAstRecord();
+        CompilationUnitTree root = astRecord.ast;
+        return ASTIndex.getNode(root, astRecord);
+    }
+
+    /**
+     * Find the class tree associated with the given {@link AnnotationLocation.ClassDeclLocation}.
+     * @param realTypeFactory the current real {@link BaseAnnotatedTypeFactory}
+     * @param location location to find the tree
+     * @param type type of the associated class
+     * @return the class tree associated with the given location
+     */
+    private Tree getTreeForLocation(
+            AnnotationLocation.ClassDeclLocation location,
+            TypeMirror type,
+            BaseAnnotatedTypeFactory realTypeFactory
+    ) {
+        Element element = processingEnvironment.getTypeUtils().asElement(type);
+        if (!(element instanceof TypeElement)) {
+            throw new BugInCF(
+                    "Expected to get a TypeElement for %s at %s, but received %s.", type, location, element);
+        }
+
+        TypeElement typeElement = (TypeElement) element;
+        Name fullyQualifiedName = ((Symbol.ClassSymbol)typeElement).flatName();
+        if (!fullyQualifiedName.contentEquals(location.getFullyQualifiedClassName())) {
+            throw new BugInCF(
+                    "TypeElement for %s has qualified name %s, and it doesn't match with the location %s",
+                    type, fullyQualifiedName, location);
+        }
+
+        return realTypeFactory.declarationFromElement(typeElement);
+    }
+
     @Override
     public RefinementVariableSlot createRefinementVariableSlot(AnnotationLocation location, Slot declarationSlot, Slot valueSlot) {
         // If the location is already cached, return the corresponding refinement slot in the cache

src/checkers/inference/InferenceAnnotatedTypeFactory.java

@@ -550,6 +550,7 @@ public void setRoot(final CompilationUnitTree root) {
         compilationUnitsHandled += 1;
         this.realTypeFactory.setRoot( root );
         this.variableAnnotator.clearTreeInfo();
+        this.slotManager.setRoot(root);
         super.setRoot(root);
     }
 

src/checkers/inference/InferenceLauncher.java

@@ -3,7 +3,6 @@
 
 import org.checkerframework.framework.util.CheckerMain;
 import org.checkerframework.framework.util.ExecUtil;
-import org.checkerframework.javacutil.SystemUtil;
 
 import java.io.BufferedReader;
 import java.io.ByteArrayOutputStream;
@@ -190,6 +189,15 @@ public void infer() {
 
         addIfTrue("--hacks", InferenceOptions.hacks, argList);
 
+        Mode mode = Mode.valueOf(InferenceOptions.mode);
+        if (InferenceOptions.makeDefaultsExplicit
+                && (mode == Mode.ROUNDTRIP || mode == Mode.ROUNDTRIP_TYPECHECK)) {
+            // 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`)
+            argList.add("--makeDefaultsExplicit");
+        }
+
         argList.add("--");
 
         String compilationBcp = getInferenceCompilationBootclassPath();

src/checkers/inference/InferenceMain.java

@@ -1,5 +1,7 @@
 package checkers.inference;
 
+import checkers.inference.model.SourceVariableSlot;
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 
 import java.io.FileOutputStream;
@@ -26,6 +28,8 @@
 import checkers.inference.qual.VarAnnot;
 import checkers.inference.util.InferenceUtil;
 import checkers.inference.util.JaifBuilder;
+import org.checkerframework.javacutil.AnnotationUtils;
+import org.checkerframework.javacutil.BugInCF;
 import org.checkerframework.javacutil.SystemUtil;
 
 /**
@@ -233,21 +237,13 @@ private void writeJaif() {
                     annotationClasses.add(annotation);
                 }
             }
+
             for (VariableSlot slot : varSlots) {
-                if (slot.getLocation() != null && slot.isInsertable()
-                 && (solverResult == null || solverResult.containsSolutionForVariable(slot.getId()))) {
+                if (slot.getLocation() != null) {
                     // TODO: String serialization of annotations.
-                    if (solverResult != null) {
-                        // Not all VariableSlots will have an inferred value.
-                        // This happens for VariableSlots that have no constraints.
-                        AnnotationMirror result = solverResult.getSolutionForVariable(slot.getId());
-                        if (result != null) {
-                            values.put(slot.getLocation(), result.toString());
-                        }
-                    } else {
-                        // Just use the VarAnnot in the jaif.
-                        String value = slotManager.getAnnotation(slot).toString();
-                        values.put(slot.getLocation(), value);
+                    AnnotationMirror annotationToWrite = getAnnotationToWrite(slot);
+                    if (annotationToWrite != null) {
+                        values.put(slot.getLocation(), annotationToWrite.toString());
                     }
                 }
             }
@@ -285,6 +281,28 @@ private void solve() {
         }
     }
 
+    private @Nullable AnnotationMirror getAnnotationToWrite(VariableSlot slot) {
+        if (!slot.isInsertable()) {
+            return null;
+        } else if (solverResult == null) {
+            // Just use the VarAnnot in the jaif.
+            return slotManager.getAnnotation(slot);
+        }
+
+        // Not all VariableSlots will have an inferred value.
+        // This happens for VariableSlots that have no constraints.
+        AnnotationMirror result = solverResult.getSolutionForVariable(slot.getId());
+        if (result != null && slot instanceof SourceVariableSlot) {
+            AnnotationMirror defaultAnnotation = ((SourceVariableSlot) slot).getDefaultAnnotation();
+
+            if (defaultAnnotation != null && AnnotationUtils.areSame(defaultAnnotation, result)) {
+                // Don't need to write a solution that's equivalent to the default annotation.
+                result = null;
+            }
+        }
+        return result;
+    }
+
     // ================================================================================
     // Component Initialization
     // ================================================================================
@@ -339,8 +357,17 @@ public BaseAnnotatedTypeFactory getRealTypeFactory() {
 
     public SlotManager getSlotManager() {
         if (slotManager == null ) {
-            slotManager = new DefaultSlotManager(inferenceChecker.getProcessingEnvironment(),
-                    realTypeFactory.getSupportedTypeQualifiers(), true );
+            Set<? extends AnnotationMirror> tops = realTypeFactory.getQualifierHierarchy().getTopAnnotations();
+            if (tops.size() != 1) {
+                throw new BugInCF("Expected 1 real top qualifier, but received %d instead", tops.size());
+            }
+
+            slotManager = new DefaultSlotManager(
+                    inferenceChecker.getProcessingEnvironment(),
+                    tops.iterator().next(),
+                    realTypeFactory.getSupportedTypeQualifiers(),
+                    true
+            );
             logger.finer("Created slot manager" + slotManager);
         }
         return slotManager;

src/checkers/inference/InferenceOptions.java

@@ -100,6 +100,9 @@ public class InferenceOptions {
     @Option("Additional AFU options")
     public static String afuOptions;
 
+    @Option("If true, insert solutions that are equivalent to the default ones back to the code.")
+    public static boolean makeDefaultsExplicit;
+
     // ------------------------------------------------------
     @OptionGroup("Help")
 

src/checkers/inference/SlotManager.java

@@ -1,6 +1,7 @@
 package checkers.inference;
 
 import checkers.inference.model.LubVariableSlot;
+import com.sun.source.tree.CompilationUnitTree;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 
 import java.util.List;
@@ -218,4 +219,12 @@ ArithmeticVariableSlot createArithmeticVariableSlot(
     List<VariableSlot> getVariableSlots();
 
     List<ConstantSlot> getConstantSlots();
+
+    /**
+     * Informs this manager that we are working on a new file, so
+     * it can preprocess and cache useful information.
+     *
+     * @param compilationUnit the current compilation tree
+     */
+    void setRoot(CompilationUnitTree compilationUnit);
 }