Add downstreams of value-inference

.ci-build.sh

@@ -92,7 +92,7 @@ if [[ "${GROUP}" == downstream* && "${SLUGOWNER}" == "opprop" ]]; then
         clone_downstream $SECURITY_GIT $SECURITY_BRANCH
         test_downstream $SECURITY_GIT $SECURITY_COMMAND
     fi
-    
+
     # Universe test
     if [[ "${GROUP}" == "downstream-universe" ]]; then
         UNIVERSE_GIT=universe
@@ -102,6 +102,18 @@ if [[ "${GROUP}" == downstream* && "${SLUGOWNER}" == "opprop" ]]; then
         clone_downstream $UNIVERSE_GIT $UNIVERSE_BRANCH
         test_downstream $UNIVERSE_GIT $UNIVERSE_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
 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, downstream-universe ]
+        group: [ cfi-tests, downstream-ontology, downstream-security-demo, downstream-universe, downstream-value-inference ]
         jdk: [ 8, 11 ]
     runs-on: ubuntu-latest
     steps:

src/checkers/inference/DefaultSlotManager.java

@@ -581,10 +581,7 @@ public ExistentialVariableSlot createExistentialVariableSlot(Slot potentialSlot,
      * @param rhsAtm atm of right operand
      * @return type kind of the arithmetic operation
      */
-    private TypeKind getArithmeticResultKind(AnnotatedTypeMirror lhsAtm, AnnotatedTypeMirror rhsAtm) {
-        TypeMirror lhsType = lhsAtm.getUnderlyingType();
-        TypeMirror rhsType = rhsAtm.getUnderlyingType();
-
+    private TypeKind getArithmeticResultKind(TypeMirror lhsType, TypeMirror rhsType) {
         assert (TypesUtils.isPrimitiveOrBoxed(lhsType) && TypesUtils.isPrimitiveOrBoxed(rhsType));
 
         if (TypesUtils.isFloatingPoint(lhsType) || TypesUtils.isFloatingPoint(rhsType)) {
@@ -601,7 +598,7 @@ private TypeKind getArithmeticResultKind(AnnotatedTypeMirror lhsAtm, AnnotatedTy
 
     @Override
     public ArithmeticVariableSlot createArithmeticVariableSlot(
-            AnnotationLocation location, AnnotatedTypeMirror lhsAtm, AnnotatedTypeMirror rhsAtm) {
+            AnnotationLocation location, TypeMirror lhs, TypeMirror rhs) {
         if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) {
             throw new BugInCF(
                     "Cannot create an ArithmeticVariableSlot with a missing annotation location.");
@@ -612,7 +609,7 @@ public ArithmeticVariableSlot createArithmeticVariableSlot(
         }
 
         // create the arithmetic var slot if it doesn't exist for the given location
-        TypeKind kind = getArithmeticResultKind(lhsAtm, rhsAtm);
+        TypeKind kind = getArithmeticResultKind(lhs, rhs);
         ArithmeticVariableSlot slot = new ArithmeticVariableSlot(nextId(), location, kind);
         addToSlots(slot);
         arithmeticSlotCache.put(location, slot.getId());

src/checkers/inference/SlotManager.java

@@ -155,7 +155,7 @@ public interface SlotManager {
      * @return the ArithmeticVariableSlot for the given location
      */
     ArithmeticVariableSlot createArithmeticVariableSlot(
-            AnnotationLocation location, AnnotatedTypeMirror lhsAtm, AnnotatedTypeMirror rhsAtm);
+            AnnotationLocation location, TypeMirror lhsType, TypeMirror rhsType);
 
     /**
      * Create new ComparisonVariableSlot at the given location and return a reference to it if no

src/checkers/inference/dataflow/InferenceTransfer.java

@@ -1,14 +1,18 @@
 package checkers.inference.dataflow;
 
+import org.checkerframework.dataflow.analysis.ConditionalTransferResult;
 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.dataflow.expression.JavaExpression;
 import org.checkerframework.framework.flow.CFStore;
 import org.checkerframework.framework.flow.CFTransfer;
 import org.checkerframework.framework.flow.CFValue;
@@ -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.Tree;
@@ -31,6 +36,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;
@@ -401,4 +408,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.
+        JavaExpression rec;
+        rec = JavaExpression.fromNode(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);
+    }
 }

src/checkers/inference/dataflow/InferenceValue.java

@@ -1,5 +1,6 @@
 package checkers.inference.dataflow;
 
+import checkers.inference.model.ComparisonVariableSlot;
 import checkers.inference.util.InferenceUtil;
 import javax.lang.model.type.TypeVariable;
 import org.checkerframework.framework.flow.CFValue;
@@ -153,9 +154,18 @@ public CFValue mostSpecificFromSlot(final Slot thisSlot, final Slot otherSlot, f
             return other;
         }
 
+        if (thisSlot instanceof ComparisonVariableSlot
+                && ((ComparisonVariableSlot) thisSlot).getRefined().equals(otherSlot)) {
+            return this;
+        }
+        if (otherSlot instanceof ComparisonVariableSlot
+                && ((ComparisonVariableSlot) otherSlot).getRefined().equals(thisSlot)) {
+            return other;
+        }
+
         if (thisSlot instanceof VariableSlot) {
             // Check if one of these has refinement variables that were merged to the other.
-            for (RefinementVariableSlot slot : ((VariableSlot) thisSlot).getRefinedToSlots()) {
+            for (VariableSlot slot : ((VariableSlot) thisSlot).getRefinedToSlots()) {
                 if (slot.isMergedTo(otherSlot)) {
                     return other;
                 }
@@ -164,7 +174,7 @@ public CFValue mostSpecificFromSlot(final Slot thisSlot, final Slot otherSlot, f
 
         if (otherSlot instanceof VariableSlot) {
             // Same as above
-            for (RefinementVariableSlot slot : ((VariableSlot) otherSlot).getRefinedToSlots()) {
+            for (VariableSlot slot : ((VariableSlot) otherSlot).getRefinedToSlots()) {
                 if (slot.isMergedTo(thisSlot)) {
                     return this;
                 }

src/checkers/inference/model/ArithmeticConstraint.java

@@ -57,6 +57,16 @@ public static ArithmeticOperationKind fromTreeKind(Kind kind) {
                     return OR;
                 case XOR:
                     return XOR;
+                case PLUS_ASSIGNMENT:
+                    return PLUS;
+                case MINUS_ASSIGNMENT:
+                    return MINUS;
+                case MULTIPLY_ASSIGNMENT:
+                    return MULTIPLY;
+                case DIVIDE_ASSIGNMENT:
+                    return DIVIDE;
+                case REMAINDER_ASSIGNMENT:
+                    return REMAINDER;
                 default:
                     throw new BugInCF("There are no defined ArithmeticOperationKinds "
                             + "for the given com.sun.source.tree.Tree.Kind: " + kind);

src/checkers/inference/model/VariableSlot.java

@@ -31,7 +31,7 @@ public abstract class VariableSlot extends Slot {
     private AnnotationLocation location;
 
     /** Refinement variables that refine this slot. */
-    private final Set<RefinementVariableSlot> refinedToSlots = new HashSet<>();
+    private final Set<VariableSlot> refinedToSlots = new HashSet<>();
 
     /**
      * Create a Slot with the given annotation location.
@@ -53,7 +53,7 @@ public void setLocation(AnnotationLocation location) {
         this.location = location;
     }
 
-    public Set<RefinementVariableSlot> getRefinedToSlots() {
+    public Set<VariableSlot> getRefinedToSlots() {
         return refinedToSlots;
     }
 

src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java

@@ -1,19 +1,15 @@
 package checkers.inference.solver.backend.z3smt.encoder;
 
 import java.util.Collection;
+import java.util.logging.Logger;
 
+import checkers.inference.InferenceMain;
 import com.microsoft.z3.Context;
 import com.microsoft.z3.Expr;
 
-import checkers.inference.model.ArithmeticConstraint;
-import checkers.inference.model.CombineConstraint;
-import checkers.inference.model.ComparableConstraint;
 import checkers.inference.model.Constraint;
 import checkers.inference.model.EqualityConstraint;
-import checkers.inference.model.ExistentialConstraint;
-import checkers.inference.model.ImplicationConstraint;
 import checkers.inference.model.InequalityConstraint;
-import checkers.inference.model.PreferenceConstraint;
 import checkers.inference.model.SubtypeConstraint;
 import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator;
 import checkers.inference.solver.frontend.Lattice;
@@ -22,6 +18,8 @@
 public abstract class Z3SmtSoftConstraintEncoder<SlotEncodingT, SlotSolutionT>
         extends Z3SmtAbstractConstraintEncoder<SlotEncodingT, SlotSolutionT> {
 
+    private static final Logger logger = Logger.getLogger(Z3SmtSoftConstraintEncoder.class.getName());
+
     protected final StringBuilder softConstraints;
 
     public Z3SmtSoftConstraintEncoder(
@@ -60,7 +58,11 @@ public String encodeAndGetSoftConstraints(Collection<Constraint> constraints) {
                 encodeSoftInequalityConstraint((InequalityConstraint) constraint);
 
             } else {
-                throw new BugInCF("Soft constraint for " + constraint.getClass().getName() + " is not supported");
+                if (InferenceMain.isHackMode()) {
+                    logger.warning("Soft constraint for " + constraint.getClass().getName() + " is not supported");
+                } else {
+                    throw new BugInCF("Soft constraint for " + constraint.getClass().getName() + " is not supported");
+                }
             }
         }
         String res = softConstraints.toString();

testdata/ostrusted-inferrable-test/Comparison.java

@@ -0,0 +1,19 @@
+import ostrusted.qual.OsTrusted;
+import ostrusted.qual.OsUntrusted;
+
+public class Comparison {
+
+    void foo(@OsUntrusted Object o) {
+        if (o == null) {
+            bar(o);
+        } 
+    }
+
+    @OsTrusted
+    Object bar(Object o) {
+        // :: fixable-error: (return.type.incompatible)
+        return o;
+    }
+
+}
+