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,22 @@ public class DefaultSlotManager implements SlotManager {
     private final Map<Pair<Slot, Slot>, Integer> lubSlotPairCache;
     private final Map<Pair<Slot, Slot>, Integer> glbSlotPairCache;
 
+    /**
+     * The hashcode of the latest compilation unit. This is currently used to
+     * determine whether we should reset the defaultAnnotationsCache.
+     */
+    // TODO: we may use this to clear other caches
+    private Integer currentRootHash;
+
+    /**
+     * A map of tree hashcode to {@link AnnotationMirror} for caching
+     * a set of pre-computed default types for the current compilation unit.
+     *
+     * The reason we're storing the hashcode is to avoid holding memory
+     * occupied by trees.
+     */
+    private Map<Integer, AnnotationMirror> defaultAnnotationsCache;
+
     /**
      * A map of {@link AnnotationLocation} to {@link Integer} for caching
      * {@link ArithmeticVariableSlot}s. The annotation location uniquely identifies an
@@ -122,9 +157,12 @@ 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;
+        this.currentRootHash = null;
         // sort the qualifiers so that they are always assigned the same varId
         this.realQualifiers = sortAnnotationClasses(realQualifiers);
         slots = new LinkedHashMap<>();
@@ -143,6 +181,7 @@ public DefaultSlotManager( final ProcessingEnvironment processingEnvironment,
         arithmeticSlotCache = new LinkedHashMap<>();
         comparisonThenSlotCache = new LinkedHashMap<>();
         comparisonElseSlotCache = new LinkedHashMap<>();
+        defaultAnnotationsCache = null;
 
         if (storeConstants) {
             for (Class<? extends Annotation> annoClass : this.realQualifiers) {
@@ -321,11 +360,17 @@ public int getNumberOfSlots() {
 
     @Override
     public SourceVariableSlot createSourceVariableSlot(AnnotationLocation location, TypeMirror type) {
+        AnnotationMirror defaultAnnotation = null;
+        if (InferenceOptions.ignoreDefaultAnnotations) {
+            // 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 +380,111 @@ 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) {
+            return null;
+        }
+
+        BaseAnnotatedTypeFactory realTypeFactory = InferenceMain.getInstance().getRealTypeFactory();
+        if (location instanceof AnnotationLocation.AstPathLocation) {
+            return getRealAnnotationForLocation(
+                    realTypeFactory,
+                    (AnnotationLocation.AstPathLocation) location);
+        } else if (location instanceof AnnotationLocation.ClassDeclLocation) {
+            return getRealAnnotationForLocation(
+                    realTypeFactory,
+                    (AnnotationLocation.ClassDeclLocation) location,
+                    type);
+        }
+
+        return null;
+    }
+
+    /**
+     * Find the default annotation for {@link AnnotationLocation.AstPathLocation} by
+     * checking the real type factory.
+     * @param realTypeFactory The current real {@link BaseAnnotatedTypeFactory}.
+     * @param location Location to create a new {@link SourceVariableSlot}.
+     * @return The default annotation for the given location.
+     */
+    private @Nullable AnnotationMirror getRealAnnotationForLocation(
+            BaseAnnotatedTypeFactory realTypeFactory,
+            AnnotationLocation.AstPathLocation location
+    ) {
+        ASTRecord astRecord = location.getAstRecord();
+        CompilationUnitTree root = astRecord.ast;
+        Tree tree = ASTIndex.getNode(root, astRecord);
+
+        if (tree == null) {
+            return null;
+        }
+
+        int rootHash = root.hashCode();
+        if (this.currentRootHash == null || this.currentRootHash != rootHash) {
+            // should update both root and cache
+            this.currentRootHash = rootHash;
+            this.defaultAnnotationsCache = new HashMap<>();
+
+            Map<Tree, AnnotatedTypeMirror> defaultTypes = SlotDefaultTypeResolver.resolve(root, realTypeFactory);
+            for (Map.Entry<Tree, AnnotatedTypeMirror> entry : defaultTypes.entrySet()) {
+                this.defaultAnnotationsCache.put(
+                        entry.getKey().hashCode(),
+                        entry.getValue().getAnnotationInHierarchy(this.realTop)
+                );
+            }
+        }
+
+        AnnotationMirror realAnnotation = this.defaultAnnotationsCache.get(tree.hashCode());
+        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 default annotation for ClassDeclLocation by checking the real type factory.
+     * @param realTypeFactory The current real {@link BaseAnnotatedTypeFactory}.
+     * @param location Location to create a new {@link SourceVariableSlot}.
+     * @param type Type of the associated class.
+     * @return The default annotation for the given location.
+     */
+    private AnnotationMirror getRealAnnotationForLocation(
+            BaseAnnotatedTypeFactory realTypeFactory,
+            AnnotationLocation.ClassDeclLocation location,
+            TypeMirror type
+    ) {
+        Element element = realTypeFactory.getProcessingEnv().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.getAnnotatedType(typeElement).getAnnotationInHierarchy(this.realTop);
+    }
+
     @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/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,13 @@ public void infer() {
 
         addIfTrue("--hacks", InferenceOptions.hacks, argList);
 
+        Mode mode = Mode.valueOf(InferenceOptions.mode);
+        if (InferenceOptions.ignoreDefaultAnnotations
+                && (mode == Mode.ROUNDTRIP || mode == Mode.ROUNDTRIP_TYPECHECK)) {
+            // this flag is useful only if we will insert the solutions back
+            argList.add("--ignoreDefaultAnnotations");
+        }
+
         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,29 @@ 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.compareAnnotationMirrors(defaultAnnotation, result) == 0) {
+                // Don't need to write a solution that's equivalent to the default annotation.
+                result = null;
+            }
+        }
+        return result;
+    }
+
     // ================================================================================
     // Component Initialization
     // ================================================================================
@@ -339,8 +358,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

@@ -122,6 +122,9 @@ public class InferenceOptions {
     @Option("For inference, add debug on the port indicated")
     public static String debug;
 
+    @Option("If ture, don't insert solutions that are equivalent to the default ones back to the code.")
+    public static boolean ignoreDefaultAnnotations = true;
+
     // end of command-line options
     // ------------------------------------------------------