CharlesZ-Chen · CharlesZ-Chen · Nov 27, 2017
diff --git a/src/read/ReadAnnotatedTypeFactory.java b/src/read/ReadAnnotatedTypeFactory.java
@@ -2,9 +2,6 @@
 
 import javax.lang.model.element.AnnotationMirror;
 
-import com.sun.source.tree.BinaryTree;
-import com.sun.source.tree.UnaryTree;
-
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.framework.flow.CFAbstractAnalysis;
 import org.checkerframework.framework.flow.CFStore;
@@ -18,24 +15,21 @@
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
 import org.checkerframework.javacutil.AnnotationBuilder;
 
-import read.qual.SafeRead;
-import read.qual.SafetyBottom;
+import com.sun.source.tree.BinaryTree;
+import com.sun.source.tree.UnaryTree;
+
 import read.qual.UnknownSafety;
 import read.qual.UnsafeRead;
 
 public class ReadAnnotatedTypeFactory extends GenericAnnotatedTypeFactory<CFValue, CFStore, ReadTransfer, ReadAnalysis> {
-    protected AnnotationMirror SAFETY_BOTTOM;
-    protected AnnotationMirror UNSAFE_READ;
-    protected AnnotationMirror SAFE_READ;
     protected AnnotationMirror UNKNOWN_SAFETY;
+    protected AnnotationMirror UNSAFE_READ;
 
     public ReadAnnotatedTypeFactory(BaseTypeChecker checker) {
         super(checker);
         this.postInit();
-        SAFETY_BOTTOM = AnnotationBuilder.fromClass(elements, SafetyBottom.class);
-        UNSAFE_READ = AnnotationBuilder.fromClass(elements, UnsafeRead.class);
-        SAFE_READ = AnnotationBuilder.fromClass(elements, SafeRead.class);
         UNKNOWN_SAFETY = AnnotationBuilder.fromClass(elements, UnknownSafety.class);
+        UNSAFE_READ = AnnotationBuilder.fromClass(elements, UnsafeRead.class);
     }
 
     @Override
@@ -50,13 +44,17 @@ public ReadTreeAnnotator(AnnotatedTypeFactory atypeFactory) {
 
         @Override
         public Void visitUnary(UnaryTree node, AnnotatedTypeMirror type) {
-            type.replaceAnnotation(UNKNOWN_SAFETY);
+            if (type.hasAnnotation(UNSAFE_READ)) {
+                type.replaceAnnotation(UNKNOWN_SAFETY);
+            }
             return null;
         }
 
         @Override
         public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) {
-            type.replaceAnnotation(UNKNOWN_SAFETY);
+            if (type.hasAnnotation(UNSAFE_READ)) {
+                type.replaceAnnotation(UNKNOWN_SAFETY);
+            }
             return null;
         }
     }

diff --git a/src/read/ReadTransfer.java b/src/read/ReadTransfer.java
@@ -6,9 +6,9 @@
 
 import org.checkerframework.dataflow.analysis.ConditionalTransferResult;
 import org.checkerframework.dataflow.analysis.FlowExpressions;
+import org.checkerframework.dataflow.analysis.FlowExpressions.Receiver;
 import org.checkerframework.dataflow.analysis.TransferInput;
 import org.checkerframework.dataflow.analysis.TransferResult;
-import org.checkerframework.dataflow.analysis.FlowExpressions.Receiver;
 import org.checkerframework.dataflow.cfg.node.GreaterThanOrEqualNode;
 import org.checkerframework.dataflow.cfg.node.IntegerLiteralNode;
 import org.checkerframework.dataflow.cfg.node.LessThanNode;
@@ -18,26 +18,26 @@
 import org.checkerframework.framework.flow.CFStore;
 import org.checkerframework.framework.flow.CFValue;
 import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.AnnotationUtils;
 
-import read.qual.UnsafeRead;
 import read.qual.SafeRead;
+import read.qual.UnsafeRead;
 
 public class ReadTransfer extends CFAbstractTransfer<CFValue, CFStore, ReadTransfer>{
-    protected AnnotationMirror UNSAFE_READ;
+
     protected AnnotationMirror SAFE_READ;
+    protected AnnotationMirror UNSAFE_READ;
 
     public ReadTransfer(ReadAnalysis analysis) {
         super(analysis);
-        UNSAFE_READ = AnnotationBuilder.fromClass(analysis.getTypeFactory()
-                .getElementUtils(), UnsafeRead.class);
         SAFE_READ = AnnotationBuilder.fromClass(analysis.getTypeFactory()
                 .getElementUtils(), SafeRead.class);
+        UNSAFE_READ = AnnotationBuilder.fromClass(analysis.getTypeFactory()
+                .getElementUtils(), UnsafeRead.class);
     }
 
     public ReadTransfer(CFAbstractAnalysis<CFValue, CFStore, ReadTransfer> analysis) {
         super(analysis);
-        UNSAFE_READ = AnnotationBuilder.fromClass(analysis.getTypeFactory()
-                .getElementUtils(), UnsafeRead.class);
         SAFE_READ = AnnotationBuilder.fromClass(analysis.getTypeFactory()
                 .getElementUtils(), SafeRead.class);
     }
@@ -78,10 +78,12 @@ protected TransferResult<CFValue, CFStore> strengthenAnnotationOfEqualTo (
                             : thenStore;
                     elseStore = elseStore == null ? res.getElseStore()
                             : elseStore;
-                    if (notEqualTo) {
-                        thenStore.insertValue(secondInternal, SAFE_READ);
-                    } else {
-                        elseStore.insertValue(secondInternal, SAFE_READ);
+                    if (AnnotationUtils.containsSame(secondValue.getAnnotations(), UNSAFE_READ)) {
+                        if (notEqualTo) {
+                            thenStore.insertValue(secondInternal, SAFE_READ);
+                        } else {
+                            elseStore.insertValue(secondInternal, SAFE_READ);
+                        }
                     }
                 }
             }
@@ -122,8 +124,8 @@ public TransferResult<CFValue, CFStore> visitGreaterThanOrEqual(GreaterThanOrEqu
         CFValue rightV = p.getValueOfSubNode(rightN);
 
         // case: leftN >= 0
-        res = strengthenAnnotationOfLessThan(res, leftN, rightN, leftV, rightV, true);
 
+        res = strengthenAnnotationOfLessThan(res, leftN, rightN, leftV, rightV, true);
         return res;
     }
 
@@ -160,10 +162,12 @@ protected TransferResult<CFValue, CFStore> strengthenAnnotationOfLessThan (
                             : thenStore;
                     elseStore = elseStore == null ? res.getElseStore()
                             : elseStore;
-                    if (notLessThan) {
-                        thenStore.insertValue(secondInternal, SAFE_READ);
-                    } else {
-                        elseStore.insertValue(secondInternal, SAFE_READ);
+                    if (AnnotationUtils.containsSame(firstValue.getAnnotations(), UNSAFE_READ)) {
+                        if (notLessThan) {
+                            thenStore.insertValue(secondInternal, SAFE_READ);
+                        } else {
+                            elseStore.insertValue(secondInternal, SAFE_READ);
+                        }
                     }
                 }
             }

diff --git a/src/read/ReadVisitor.java b/src/read/ReadVisitor.java
@@ -1,15 +1,23 @@
 package read;
 
+import java.util.List;
+
 import javax.lang.model.element.AnnotationMirror;
+import javax.lang.model.element.Element;
+import javax.lang.model.element.ElementKind;
 import javax.lang.model.type.TypeKind;
 
+import com.sun.source.tree.AssignmentTree;
+import com.sun.source.tree.ExpressionTree;
+import com.sun.source.tree.MethodInvocationTree;
 import com.sun.source.tree.TypeCastTree;
 
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.common.basetype.BaseTypeVisitor;
 import org.checkerframework.framework.source.Result;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.TreeUtils;
 
 import read.qual.UnsafeRead;
 
@@ -38,4 +46,36 @@ protected void checkTypecastSafety(TypeCastTree node, Void p) {
 
         super.checkTypecastSafety(node, p);
     }
+
+    @Override
+    public Void visitAssignment(AssignmentTree node, Void p) {
+      ExpressionTree variableTree = node.getVariable();
+      AnnotatedTypeMirror variableType = atypeFactory.getAnnotatedType(variableTree);
+      AnnotatedTypeMirror expressionType = atypeFactory.getAnnotatedType(node.getExpression());
+
+      Element variableDeclartion = TreeUtils.elementFromUse(variableTree);
+
+      if (variableDeclartion.getKind() == ElementKind.FIELD
+              && variableType.getUnderlyingType().getKind() == TypeKind.INT
+              && expressionType.hasAnnotation(UNSAFE_READ)) {
+          checker.report(Result.failure("assignment.unsafe", variableType, expressionType), node);
+      }
+
+      return super.visitAssignment(node, p);
+    }
+
+    @Override
+    public Void visitMethodInvocation(MethodInvocationTree node, Void p) {
+        List<? extends ExpressionTree> arguments = node.getArguments();
+
+        for (ExpressionTree argument : arguments) {
+            AnnotatedTypeMirror argType = atypeFactory.getAnnotatedType(argument);
+            if (argType.getUnderlyingType().getKind() == TypeKind.INT
+                    && argType.hasAnnotation(UNSAFE_READ)) {
+                checker.report(Result.failure("method.arg.unsafe", argType), argument);
+            }
+        }
+
+        return super.visitMethodInvocation(node, p);
+    }
 }
diff --git a/tests/false-positives/TernaryExpr.java b/tests/false-positives/TernaryExpr.java
@@ -0,0 +1,9 @@
+class TernaryExpr {
+    public int read(int c) {
+        int i = 0;
+        for ( ; true;) {
+                i = i == 0 ? -1 : i;
+                i++;
+        }
+    }
+}
diff --git a/tests/false-positives/WrongUnsafeRead.java b/tests/false-positives/WrongUnsafeRead.java
@@ -0,0 +1,9 @@
+class WrongUnsafeRead {
+    void m(int t, int bt) {
+        bt = -1;
+        if (t >= 0) {
+                bt = t;
+        }
+        byte b = (byte) bt;
+    }
+}
diff --git a/tests/forbid-assignments/ForbidFieldAssign.java b/tests/forbid-assignments/ForbidFieldAssign.java
@@ -0,0 +1,21 @@
+package read;
+
+import java.io.FileInputStream;
+import java.io.IOException;
+import java.io.InputStream;
+
+class ForbidFieldAssign {
+    static int readInt;
+
+    public void compliantSolution() throws IOException {
+        InputStream in = new FileInputStream("afile");
+        int inbuff;
+        int localReadInt;
+        localReadInt = in.read();
+    }
+
+    void readData(InputStream in) throws IOException {
+        // :: error: (assignment.unsafe)
+        readInt = in.read();
+    }
+}
diff --git a/tests/forbid-assignments/ForbidMethodArg.java b/tests/forbid-assignments/ForbidMethodArg.java
@@ -0,0 +1,23 @@
+package read;
+
+import java.io.FileInputStream;
+import java.io.IOException;
+import java.io.InputStream;
+
+class ForbidMethodArg {
+    static int readInt;
+
+    public void compliantSolution() throws IOException {
+        InputStream in = new FileInputStream("afile");
+        int inbuff;
+        int localReadInt;
+        localReadInt = in.read();
+        // :: error: (method.arg.unsafe)
+        storeData(localReadInt);
+    }
+
+    void storeData( int readInt ) {
+        byte data;
+        data = (byte) readInt;
+    } 
+}
diff --git a/tests/src/ReadTest.java b/tests/src/ReadTest.java
@@ -15,7 +15,8 @@ public ReadTest(List<File> testFiles) {
 
     @Parameters
     public static String[] getTestDirs() {
-        return new String[]{"read-typeHierarchy", "post-condition", "binaryOpRefine", "customize-reader", "noc-examples",
-                "cs-examples", "casting", "teamed-quiz", "wtfCodeSOD061102"};
+        //, "post-condition"
+        return new String[]{"read-typeHierarchy", "binaryOpRefine", "customize-reader", "noc-examples",
+                "cs-examples", "casting", "teamed-quiz", "wtfCodeSOD061102", "false-positives", "forbid-assignments"};
     }
 }