Add downstreams of value-inference

.ci-build.sh

@@ -92,6 +92,30 @@ if [[ "${GROUP}" == downstream* && "${SLUGOWNER}" == "opprop" ]]; then
         clone_downstream $SECURITY_GIT $SECURITY_BRANCH
         test_downstream $SECURITY_GIT $SECURITY_COMMAND
     fi
+
+    # Value inference test
+    if [[ "${GROUP}" == "downstream-value-inference" ]]; then
+        VALUE_GIT=value-inference
+        VALUE_BRANCH=master
+        VALUE_COMMAND="./gradlew build"
+
+        ./gradlew testLibJar
+
+        clone_downstream $VALUE_GIT $VALUE_BRANCH
+        test_downstream $VALUE_GIT $VALUE_COMMAND
+    fi
+
+    # Unit inference test
+    if [[ "${GROUP}" == "downstream-units-inference" ]]; then
+        UNIT_GIT=units-inference
+        UNIT_BRANCH=master
+        UNIT_COMMAND="./gradlew build"
+
+        ./gradlew testLibJar
+
+        clone_downstream $UNIT_GIT $UNIT_BRANCH
+        test_downstream $UNIT_GIT $UNIT_COMMAND
+    fi
 fi
 
 echo Exiting "$(cd "$(dirname "$0")" && pwd -P)/$(basename "$0")" in `pwd`

.github/workflows/main.yml

@@ -13,7 +13,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        group: [ cfi-tests, downstream-ontology, downstream-security-demo ]
+        group: [ cfi-tests, downstream-value-inference, downstream-units-inference ]
         jdk: [ 8, 11 ]
     runs-on: ubuntu-latest
     steps:

src/checkers/inference/DefaultSlotManager.java

@@ -26,6 +26,7 @@
 import checkers.inference.model.AnnotationLocation;
 import checkers.inference.model.ArithmeticVariableSlot;
 import checkers.inference.model.CombVariableSlot;
+import checkers.inference.model.ComparisonVariableSlot;
 import checkers.inference.model.ConstantSlot;
 import checkers.inference.model.ExistentialVariableSlot;
 import checkers.inference.model.RefinementVariableSlot;
@@ -97,6 +98,22 @@ public class DefaultSlotManager implements SlotManager {
      */
     private final Map<AnnotationLocation, Integer> arithmeticSlotCache;
 
+    /**
+     * A map of {@link AnnotationLocation} to {@link Integer} for caching
+     * {@link ComparisonVariableSlot}s. The annotation location uniquely identifies an
+     * {@link ComparisonVariableSlot}. The {@link Integer} is the Id of the corresponding
+     * {@link ComparisonVariableSlot}.
+     */
+    private final Map<AnnotationLocation, Integer> comparisonThenSlotCache;
+
+    /**
+     * A map of {@link AnnotationLocation} to {@link Integer} for caching
+     * {@link ComparisonVariableSlot}s. The annotation location uniquely identifies an
+     * {@link ComparisonVariableSlot}. The {@link Integer} is the Id of the corresponding
+     * {@link ComparisonVariableSlot}.
+     */
+    private final Map<AnnotationLocation, Integer> comparisonElseSlotCache;
+
     private final Set<Class<? extends Annotation>> realQualifiers;
     private final ProcessingEnvironment processingEnvironment;
 
@@ -119,6 +136,8 @@ public DefaultSlotManager( final ProcessingEnvironment processingEnvironment,
         combSlotPairCache = new LinkedHashMap<>();
         lubSlotPairCache = new LinkedHashMap<>();
         arithmeticSlotCache = new LinkedHashMap<>();
+        comparisonThenSlotCache = new LinkedHashMap<>();
+        comparisonElseSlotCache = new LinkedHashMap<>();
 
         if (storeConstants) {
             for (Class<? extends Annotation> annoClass : this.realQualifiers) {
@@ -436,6 +455,54 @@ public ArithmeticVariableSlot getArithmeticVariableSlot(AnnotationLocation locat
         }
     }
 
+    @Override
+    public ComparisonVariableSlot createComparisonVariableSlot(AnnotationLocation location, Slot refined, boolean thenBranch) {
+        if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) {
+            throw new BugInCF(
+                    "Cannot create an ComparisonVariableSlot with a missing annotation location.");
+        }
+
+        // create the comparison var slot if it doesn't exist for the given location
+        if (thenBranch && !comparisonThenSlotCache.containsKey(location)) {
+            ComparisonVariableSlot slot = new ComparisonVariableSlot(nextId(), location, refined);
+            addToSlots(slot);
+            comparisonThenSlotCache.put(location, slot.getId());
+            return slot;
+        }
+
+        // create the comparison var slot if it doesn't exist for the given location
+        if (!thenBranch && !comparisonElseSlotCache.containsKey(location)) {
+            ComparisonVariableSlot slot = new ComparisonVariableSlot(nextId(), location, refined);
+            addToSlots(slot);
+            comparisonElseSlotCache.put(location, slot.getId());
+            return slot;
+        }
+
+        return getComparisonVariableSlot(location, thenBranch);
+    }
+
+    @Override
+    public ComparisonVariableSlot getComparisonVariableSlot(AnnotationLocation location, boolean thenBranch) {
+        if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) {
+            throw new BugInCF(
+                    "ComparisonVariableSlot are never created with a missing annotation location.");
+        }
+        if (thenBranch) {
+            if (!comparisonThenSlotCache.containsKey(location)) {
+                return null;
+            } else {
+                return (ComparisonVariableSlot) getSlot(comparisonThenSlotCache.get(location));
+            }
+        } else {
+            if (!comparisonElseSlotCache.containsKey(location)) {
+                return null;
+            } else {
+                return (ComparisonVariableSlot) getSlot(comparisonElseSlotCache.get(location));
+            }
+        }
+    }
+
+
     @Override
     public AnnotationMirror createEquivalentVarAnno(AnnotationMirror realQualifier) {
         ConstantSlot varSlot = createConstantSlot(realQualifier);

src/checkers/inference/SlotManager.java

@@ -11,6 +11,7 @@
 import checkers.inference.model.AnnotationLocation;
 import checkers.inference.model.ArithmeticVariableSlot;
 import checkers.inference.model.CombVariableSlot;
+import checkers.inference.model.ComparisonVariableSlot;
 import checkers.inference.model.ConstantSlot;
 import checkers.inference.model.ExistentialVariableSlot;
 import checkers.inference.model.RefinementVariableSlot;
@@ -151,6 +152,31 @@ public interface SlotManager {
      */
     ArithmeticVariableSlot getArithmeticVariableSlot(AnnotationLocation location);
 
+    /**
+     * Create new ComparisonVariableSlot at the given location and return a reference to it if no
+     * ComparisonVariableSlot exists for the location. Otherwise, returns the existing
+     * ComparisonVariableSlot.
+     *
+     * @param location an AnnotationLocation used to locate this variable in code
+     * @param thenBranch true if is for the then store, false if is for the else store
+     * @return the ComparisonVariableSlot for the given location
+     */
+    ComparisonVariableSlot createComparisonVariableSlot(AnnotationLocation location, Slot refined, boolean thenBranch);
+
+    /**
+     * Retrieves the ComparisonVariableSlot created for the given location if it has been previously
+     * created, otherwise null is returned.
+     *
+     * This method allows faster retrieval of already created ComparisonVariableSlot during
+     * traversals of binary comparison trees in an InferenceTransfer subclass, which does not have direct access
+     * to the ATM containing this slot.
+     *
+     * @param location an AnnotationLocation used to locate this variable in code
+     * @param thenBranch true if is for the then store, false if is for the else store
+     * @return the ComparisonVariableSlot for the given location, or null if none exists
+     */
+    ComparisonVariableSlot getComparisonVariableSlot(AnnotationLocation location, boolean thenBranch);
+
     /**
      * Create a VarAnnot equivalent to the given realQualifier.
      *

src/checkers/inference/dataflow/InferenceTransfer.java

@@ -1,12 +1,16 @@
 package checkers.inference.dataflow;
 
+import org.checkerframework.dataflow.analysis.ConditionalTransferResult;
+import org.checkerframework.dataflow.analysis.FlowExpressions;
 import org.checkerframework.dataflow.analysis.RegularTransferResult;
 import org.checkerframework.dataflow.analysis.TransferInput;
 import org.checkerframework.dataflow.analysis.TransferResult;
 import org.checkerframework.dataflow.cfg.node.AssignmentNode;
+import org.checkerframework.dataflow.cfg.node.EqualToNode;
 import org.checkerframework.dataflow.cfg.node.FieldAccessNode;
 import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
 import org.checkerframework.dataflow.cfg.node.Node;
+import org.checkerframework.dataflow.cfg.node.NotEqualNode;
 import org.checkerframework.dataflow.cfg.node.StringConcatenateAssignmentNode;
 import org.checkerframework.dataflow.cfg.node.TernaryExpressionNode;
 import org.checkerframework.framework.flow.CFStore;
@@ -21,6 +25,7 @@
 import java.util.Map;
 import java.util.logging.Logger;
 
+import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.type.TypeKind;
 
 import com.sun.source.tree.CompoundAssignmentTree;
@@ -33,6 +38,8 @@
 import checkers.inference.SlotManager;
 import checkers.inference.VariableAnnotator;
 import checkers.inference.model.AnnotationLocation;
+import checkers.inference.model.ComparisonVariableSlot;
+import checkers.inference.model.ConstraintManager;
 import checkers.inference.model.ExistentialVariableSlot;
 import checkers.inference.model.RefinementVariableSlot;
 import checkers.inference.model.Slot;
@@ -63,8 +70,11 @@ public class InferenceTransfer extends CFTransfer {
     // case where the correct, inferred RHS has no primary annotation
     private Map<Tree, Pair<RefinementVariableSlot, RefinementVariableSlot>> createdTypeVarRefinementVariables = new HashMap<>();
 
+    private final InferenceAnnotatedTypeFactory typeFactory;
+
     public InferenceTransfer(InferenceAnalysis analysis) {
         super(analysis);
+        typeFactory = (InferenceAnnotatedTypeFactory) analysis.getTypeFactory();
     }
 
     private InferenceAnalysis getInferenceAnalysis() {
@@ -92,7 +102,6 @@ public TransferResult<CFValue, CFStore> visitAssignment(AssignmentNode assignmen
 
         Node lhs = assignmentNode.getTarget();
         CFStore store = transferInput.getRegularStore();
-        InferenceAnnotatedTypeFactory typeFactory = (InferenceAnnotatedTypeFactory) analysis.getTypeFactory();
 
         // Target tree is null for field access's
         Tree targetTree = assignmentNode.getTarget().getTree();
@@ -137,7 +146,7 @@ public TransferResult<CFValue, CFStore> visitAssignment(AssignmentNode assignmen
                 assert false;
             }
 
-            return storeDeclaration(lhs, (VariableTree) assignmentNode.getTree(), store, typeFactory);
+            return storeDeclaration(lhs, (VariableTree) assignmentNode.getTree(), store);
 
         } else if (lhs.getTree().getKind() == Tree.Kind.IDENTIFIER
                 || lhs.getTree().getKind() == Tree.Kind.MEMBER_SELECT) {
@@ -179,7 +188,6 @@ public TransferResult<CFValue, CFStore> visitAssignment(AssignmentNode assignmen
     public TransferResult<CFValue, CFStore> visitStringConcatenateAssignment(StringConcatenateAssignmentNode assignmentNode, TransferInput<CFValue, CFStore> transferInput) {
         // TODO: CompoundAssigment trees are not refined, see Issue 9
         CFStore store = transferInput.getRegularStore();
-        InferenceAnnotatedTypeFactory typeFactory = (InferenceAnnotatedTypeFactory) analysis.getTypeFactory();
 
         Tree targetTree = assignmentNode.getLeftOperand().getTree();
 
@@ -225,7 +233,7 @@ private TransferResult<CFValue, CFStore> createRefinementVar(Node lhs,
             refVar = createdRefinementVariables.get(assignmentTree);
         } else {
             AnnotationLocation location = VariableAnnotator.treeToLocation(analysis.getTypeFactory(), assignmentTree);
-            refVar = getInferenceAnalysis().getSlotManager().createRefinementVariableSlot(location, slotToRefine, refineTo);
+            refVar = slotManager.createRefinementVariableSlot(location, slotToRefine, refineTo);
 
             // Fields from library methods can be refined, but the slotToRefine is a ConstantSlot
             // which does not have a refined slots field.
@@ -236,7 +244,7 @@ private TransferResult<CFValue, CFStore> createRefinementVar(Node lhs,
             createdRefinementVariables.put(assignmentTree, refVar);
         }
 
-        atm.replaceAnnotation(getInferenceAnalysis().getSlotManager().getAnnotation(refVar));
+        atm.replaceAnnotation(slotManager.getAnnotation(refVar));
 
         // add refinement variable value to output
         CFValue result = analysis.createAbstractValue(atm);
@@ -379,12 +387,10 @@ private TransferResult<CFValue, CFStore> createTypeVarRefinementVars(Node lhs, T
      * @param lhs
      * @param assignmentTree
      * @param store
-     * @param typeFactory
      * @return
      */
     private TransferResult<CFValue, CFStore> storeDeclaration(Node lhs,
-            VariableTree assignmentTree, CFStore store,
-            InferenceAnnotatedTypeFactory typeFactory) {
+            VariableTree assignmentTree, CFStore store) {
 
         AnnotatedTypeMirror atm = typeFactory.getAnnotatedType(assignmentTree);
         CFValue result = analysis.createAbstractValue(atm);
@@ -395,4 +401,95 @@ private TransferResult<CFValue, CFStore> storeDeclaration(Node lhs,
     private boolean isDeclarationWithInitializer(AssignmentNode assignmentNode) {
         return (assignmentNode.getTree().getKind() == Tree.Kind.VARIABLE);
     }
+
+
+    private void createComparisonVariableSlot(Node node, CFStore thenStore, CFStore elseStore) {
+        // Only create refinement comparison slot for variables
+        // TODO: deal with comparison between more complex expressions
+        Node var = node;
+        if (node instanceof AssignmentNode) {
+            AssignmentNode a = (AssignmentNode) node;
+            var = a.getTarget();
+        }
+        if (!(var instanceof LocalVariableNode) && !(var instanceof FieldAccessNode)) {
+            return;
+        }
+        Tree tree = var.getTree();
+        ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager();
+        SlotManager slotManager = getInferenceAnalysis().getSlotManager();
+
+        AnnotatedTypeMirror atm = typeFactory.getAnnotatedType(tree);
+        Slot slotToRefine = slotManager.getSlot(atm);
+
+        // TODO: Understand why there are null slots
+        if (InferenceMain.isHackMode(slotToRefine == null)) {
+            logger.fine("HackMode: slotToRefine is null !");
+            return;
+        }
+
+        if (slotToRefine instanceof RefinementVariableSlot) {
+            slotToRefine = ((RefinementVariableSlot) slotToRefine).getRefined();
+            assert !(slotToRefine instanceof RefinementVariableSlot);
+        }
+
+        AnnotationLocation location =
+                VariableAnnotator.treeToLocation(analysis.getTypeFactory(), tree);
+        // TODO: find out why there are missing location
+        if (InferenceMain.isHackMode(location == AnnotationLocation.MISSING_LOCATION)) {
+            logger.fine("HackMode: create ComparisonVariableSlot on MISSING_LOCATION !");
+            return;
+        }
+        ComparisonVariableSlot thenSlot = slotManager.createComparisonVariableSlot(location, slotToRefine, true);
+        constraintManager.addSubtypeConstraint(thenSlot, slotToRefine);
+        ComparisonVariableSlot elseSlot = slotManager.createComparisonVariableSlot(location, slotToRefine, false);
+        constraintManager.addSubtypeConstraint(elseSlot, slotToRefine);
+
+        if (slotToRefine instanceof VariableSlot) {
+            // ComparisonVariableSlots stores the refined value after comparison, so add it to the "refinedTo" list
+            ((VariableSlot) slotToRefine).getRefinedToSlots().add(thenSlot);
+            ((VariableSlot) slotToRefine).getRefinedToSlots().add(elseSlot);
+        }
+
+        AnnotationMirror thenAm = slotManager.getAnnotation(thenSlot);
+        AnnotationMirror elseAm = slotManager.getAnnotation(elseSlot);
+
+        // If node is assignment, iterate over lhs; otherwise, just node.
+        FlowExpressions.Receiver rec;
+        rec = FlowExpressions.internalReprOf(getInferenceAnalysis().getTypeFactory(), var);
+        thenStore.clearValue(rec);
+        thenStore.insertValue(rec, thenAm);
+        elseStore.clearValue(rec);
+        elseStore.insertValue(rec, elseAm);
+    }
+
+    @Override
+    public TransferResult<CFValue, CFStore> visitEqualTo(
+            EqualToNode n, TransferInput<CFValue, CFStore> in) {
+        TransferResult<CFValue, CFStore> result = super.visitEqualTo(n, in);
+        CFStore thenStore = result.getThenStore();
+        CFStore elseStore = result.getElseStore();
+
+        createComparisonVariableSlot(n.getLeftOperand(), thenStore, elseStore);
+        createComparisonVariableSlot(n.getRightOperand(), thenStore, elseStore);
+
+        CFValue newResultValue =
+                getInferenceAnalysis()
+                        .createAbstractValue(typeFactory.getAnnotatedType(n.getTree()));
+        return new ConditionalTransferResult<>(newResultValue, thenStore, elseStore);
+    }
+
+    @Override
+    public TransferResult<CFValue, CFStore> visitNotEqual(
+            NotEqualNode n, TransferInput<CFValue, CFStore> in) {
+        TransferResult<CFValue, CFStore> result = super.visitNotEqual(n, in);
+        CFStore thenStore = result.getThenStore();
+        CFStore elseStore = result.getElseStore();
+
+        createComparisonVariableSlot(n.getLeftOperand(), thenStore, elseStore);
+        createComparisonVariableSlot(n.getRightOperand(), thenStore, elseStore);
+
+        CFValue newResultValue =
+                analysis.createAbstractValue(typeFactory.getAnnotatedType(n.getTree()));
+        return new ConditionalTransferResult<>(newResultValue, thenStore, elseStore);
+    }
 }