From a0e6fcaf25295eed75c84e2205a397bb76969466 Mon Sep 17 00:00:00 2001 From: CharlesZ-Chen Date: Mon, 27 Nov 2017 12:58:06 -0500 Subject: [PATCH] Add forbid check. Fix two false positives. --- src/read/ReadAnnotatedTypeFactory.java | 24 +++++------ src/read/ReadTransfer.java | 36 +++++++++-------- src/read/ReadVisitor.java | 40 +++++++++++++++++++ tests/false-positives/TernaryExpr.java | 9 +++++ tests/false-positives/WrongUnsafeRead.java | 9 +++++ .../forbid-assignments/ForbidFieldAssign.java | 21 ++++++++++ tests/forbid-assignments/ForbidMethodArg.java | 23 +++++++++++ tests/src/ReadTest.java | 5 ++- 8 files changed, 136 insertions(+), 31 deletions(-) create mode 100644 tests/false-positives/TernaryExpr.java create mode 100644 tests/false-positives/WrongUnsafeRead.java create mode 100644 tests/forbid-assignments/ForbidFieldAssign.java create mode 100644 tests/forbid-assignments/ForbidMethodArg.java diff --git a/src/read/ReadAnnotatedTypeFactory.java b/src/read/ReadAnnotatedTypeFactory.java index d97617f..d803dbc 100644 --- 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 { - 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 index b3da5b7..915cc2d 100644 --- 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{ - 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 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 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 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 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 index cb7e2ed..dce5eae 100644 --- a/src/read/ReadVisitor.java +++ b/src/read/ReadVisitor.java @@ -1,8 +1,15 @@ 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; @@ -10,6 +17,7 @@ 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 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 new file mode 100644 index 0000000..3d157c0 --- /dev/null +++ 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++; + } + } +} \ No newline at end of file diff --git a/tests/false-positives/WrongUnsafeRead.java b/tests/false-positives/WrongUnsafeRead.java new file mode 100644 index 0000000..921134a --- /dev/null +++ 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; + } +} \ No newline at end of file diff --git a/tests/forbid-assignments/ForbidFieldAssign.java b/tests/forbid-assignments/ForbidFieldAssign.java new file mode 100644 index 0000000..1ed5324 --- /dev/null +++ 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 new file mode 100644 index 0000000..35b2ff4 --- /dev/null +++ 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 index 2ec5aff..79f838f 100644 --- a/tests/src/ReadTest.java +++ b/tests/src/ReadTest.java @@ -15,7 +15,8 @@ public ReadTest(List 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"}; } }