From f87f55e97954a3f25c36309202dfae2e41998d40 Mon Sep 17 00:00:00 2001 From: CharlesZ-Chen Date: Tue, 21 Nov 2017 14:34:02 -0500 Subject: [PATCH 1/2] Change read check mechanism. Initial commit. --- FooProject/src/Foo.java | 4 +- read-check.sh | 4 +- run-dljc.sh | 20 +- src/read/ReadAnnotatedTypeFactory.java | 42 ++-- src/read/ReadTransfer.java | 198 ++++-------------- src/read/ReadVisitor.java | 43 ++-- src/read/jdk.astub | 68 +++--- src/read/qual/EnsureSafeIf.java | 32 --- .../{UnsafeRead.java => NarrowerReadInt.java} | 2 +- src/read/qual/{SafeRead.java => ReadInt.java} | 4 +- src/read/qual/SafetyBottom.java | 2 +- src/read/qual/UnknownSafetyLiterals.java | 4 +- tests/casting/ErrorCasting.java | 4 +- tests/casting/NormalCasting.java | 6 +- tests/cs-examples/CS4InputStream.java | 4 +- tests/cs-examples/CS4Reader.java | 4 +- tests/customize-reader/MyReader.java | 5 +- tests/noc-examples/NOCE4InputStream.java | 2 +- tests/noc-examples/NOCE4Reader.java | 2 +- tests/read-typeHierarchy/TypeHierarchy.java | 40 ++-- tests/src/ReadTest.java | 3 +- tests/wtfCodeSOD061102/WTFCodeSOD061102.java | 8 +- 22 files changed, 193 insertions(+), 308 deletions(-) delete mode 100644 src/read/qual/EnsureSafeIf.java rename src/read/qual/{UnsafeRead.java => NarrowerReadInt.java} (87%) rename src/read/qual/{SafeRead.java => ReadInt.java} (77%) diff --git a/FooProject/src/Foo.java b/FooProject/src/Foo.java index 60a2640..b26970e 100644 --- a/FooProject/src/Foo.java +++ b/FooProject/src/Foo.java @@ -9,7 +9,7 @@ public void unsafeWayOfCastingByte() throws IOException { InputStream in = new FileInputStream("afile"); @SuppressWarnings("unused") byte data; - //:: error: (cast.unsafe) + // :: error: (unsafe.eof.comparision) while ((data = (byte) in.read()) != -1) { //... } @@ -20,7 +20,7 @@ public void unsafeWayOfCastingChar() throws IOException { Reader in = new FileReader("afile"); @SuppressWarnings("unused") char data; - //:: error: (cast.unsafe) + // :: error: (unsafe.eof.comparision) while ((data = (char) in.read()) != -1) { //... } diff --git a/read-check.sh b/read-check.sh index 8970195..527eeb5 100755 --- a/read-check.sh +++ b/read-check.sh @@ -16,4 +16,6 @@ do shift done -$JAVAC -processor read.ReadChecker -cp $READ_CHECKER/bin:$READ_CHECKER/lib $java_files +target_classpath="/Users/charleszhuochen/Programming/UWaterloo/jsr308/opprop-benchmarks/commons-jcs/commons-jcs-core/target/classes:/Users/charleszhuochen/.m2/repository/commons-logging/commons-logging/1.2/commons-logging-1.2.jar:/Users/charleszhuochen/.m2/repository/commons-dbcp/commons-dbcp/1.4/commons-dbcp-1.4.jar:/Users/charleszhuochen/.m2/repository/commons-pool/commons-pool/1.6/commons-pool-1.6.jar:/Users/charleszhuochen/.m2/repository/org/apache/velocity/velocity-tools/2.0/velocity-tools-2.0.jar:/Users/charleszhuochen/.m2/repository/commons-beanutils/commons-beanutils/1.7.0/commons-beanutils-1.7.0.jar:/Users/charleszhuochen/.m2/repository/commons-digester/commons-digester/1.8/commons-digester-1.8.jar:/Users/charleszhuochen/.m2/repository/commons-chain/commons-chain/1.1/commons-chain-1.1.jar:/Users/charleszhuochen/.m2/repository/commons-collections/commons-collections/3.2/commons-collections-3.2.jar:/Users/charleszhuochen/.m2/repository/commons-validator/commons-validator/1.3.1/commons-validator-1.3.1.jar:/Users/charleszhuochen/.m2/repository/dom4j/dom4j/1.1/dom4j-1.1.jar:/Users/charleszhuochen/.m2/repository/oro/oro/2.0.8/oro-2.0.8.jar:/Users/charleszhuochen/.m2/repository/sslext/sslext/1.2-0/sslext-1.2-0.jar:/Users/charleszhuochen/.m2/repository/org/apache/struts/struts-core/1.3.8/struts-core-1.3.8.jar:/Users/charleszhuochen/.m2/repository/antlr/antlr/2.7.2/antlr-2.7.2.jar:/Users/charleszhuochen/.m2/repository/org/apache/struts/struts-taglib/1.3.8/struts-taglib-1.3.8.jar:/Users/charleszhuochen/.m2/repository/org/apache/struts/struts-tiles/1.3.8/struts-tiles-1.3.8.jar:/Users/charleszhuochen/.m2/repository/org/apache/velocity/velocity/1.6.2/velocity-1.6.2.jar:/Users/charleszhuochen/.m2/repository/commons-lang/commons-lang/2.4/commons-lang-2.4.jar:/Users/charleszhuochen/.m2/repository/commons-httpclient/commons-httpclient/3.1/commons-httpclient-3.1.jar:/Users/charleszhuochen/.m2/repository/commons-codec/commons-codec/1.2/commons-codec-1.2.jar:/Users/charleszhuochen/.m2/repository/javax/servlet/servlet-api/2.5/servlet-api-2.5.jar:/Users/charleszhuochen/Programming/UWaterloo/jsr308/opprop-benchmarks/commons-jcs/commons-jcs-core/target/test-classes:/Users/charleszhuochen/Programming/UWaterloo/jsr308/opprop-benchmarks/commons-jcs/commons-jcs-core/target/classes:/Users/charleszhuochen/.m2/repository/commons-logging/commons-logging/1.2/commons-logging-1.2.jar:/Users/charleszhuochen/.m2/repository/commons-dbcp/commons-dbcp/1.4/commons-dbcp-1.4.jar:/Users/charleszhuochen/.m2/repository/commons-pool/commons-pool/1.6/commons-pool-1.6.jar:/Users/charleszhuochen/.m2/repository/hsqldb/hsqldb/1.8.0.10/hsqldb-1.8.0.10.jar:/Users/charleszhuochen/.m2/repository/org/apache/commons/commons-collections4/4.1/commons-collections4-4.1.jar:/Users/charleszhuochen/.m2/repository/junit/junit/4.11/junit-4.11.jar:/Users/charleszhuochen/.m2/repository/org/hamcrest/hamcrest-core/1.3/hamcrest-core-1.3.jar:/Users/charleszhuochen/.m2/repository/org/hamcrest/hamcrest-library/1.3/hamcrest-library-1.3.jar:/Users/charleszhuochen/.m2/repository/log4j/log4j/1.2.17/log4j-1.2.17.jar:/Users/charleszhuochen/.m2/repository/org/apache/velocity/velocity-tools/2.0/velocity-tools-2.0.jar:/Users/charleszhuochen/.m2/repository/commons-beanutils/commons-beanutils/1.7.0/commons-beanutils-1.7.0.jar:/Users/charleszhuochen/.m2/repository/commons-digester/commons-digester/1.8/commons-digester-1.8.jar:/Users/charleszhuochen/.m2/repository/commons-chain/commons-chain/1.1/commons-chain-1.1.jar:/Users/charleszhuochen/.m2/repository/commons-collections/commons-collections/3.2/commons-collections-3.2.jar:/Users/charleszhuochen/.m2/repository/commons-validator/commons-validator/1.3.1/commons-validator-1.3.1.jar:/Users/charleszhuochen/.m2/repository/dom4j/dom4j/1.1/dom4j-1.1.jar:/Users/charleszhuochen/.m2/repository/oro/oro/2.0.8/oro-2.0.8.jar:/Users/charleszhuochen/.m2/repository/sslext/sslext/1.2-0/sslext-1.2-0.jar:/Users/charleszhuochen/.m2/repository/org/apache/struts/struts-core/1.3.8/struts-core-1.3.8.jar:/Users/charleszhuochen/.m2/repository/antlr/antlr/2.7.2/antlr-2.7.2.jar:/Users/charleszhuochen/.m2/repository/org/apache/struts/struts-taglib/1.3.8/struts-taglib-1.3.8.jar:/Users/charleszhuochen/.m2/repository/org/apache/struts/struts-tiles/1.3.8/struts-tiles-1.3.8.jar:/Users/charleszhuochen/.m2/repository/org/apache/velocity/velocity/1.6.2/velocity-1.6.2.jar:/Users/charleszhuochen/.m2/repository/commons-lang/commons-lang/2.4/commons-lang-2.4.jar:/Users/charleszhuochen/.m2/repository/commons-httpclient/commons-httpclient/3.1/commons-httpclient-3.1.jar:/Users/charleszhuochen/.m2/repository/commons-codec/commons-codec/1.2/commons-codec-1.2.jar:/Users/charleszhuochen/.m2/repository/javax/servlet/servlet-api/2.5/servlet-api-2.5.jar::/Users/charleszhuochen/Programming/UWaterloo/jsr308/opprop-benchmarks/commons-jcs/inferDebugBuild::/Users/charleszhuochen/Programming/UWaterloo/jsr308/ReadChecker/bin:/Users/charleszhuochen/Programming/UWaterloo/jsr308/ReadChecker/lib" + +$JAVAC -processor read.ReadChecker -cp $READ_CHECKER/bin:$READ_CHECKER/lib:$target_classpath $java_files diff --git a/run-dljc.sh b/run-dljc.sh index ce7d049..644cf96 100755 --- a/run-dljc.sh +++ b/run-dljc.sh @@ -29,4 +29,22 @@ done cd $CUR_DIR -python $DLJC/dljc -t checker --checker read.ReadChecker -- $build_cmd +# debug_onlyCompile="--onlyCompileBytecodeBase true" +debug_cmd="python $DLJC/dljc -t testminimizer --debuggedTool check --expectReturnCode 1 --checker org.checkerframework.checker.nullness.NullnessChecker --expectOutputRegex 'error: cannot find symbol' -- $build_cmd " + +infer_cmd="python $DLJC/dljc -t checker --checker read.ReadChecker -- $build_cmd " + +running_cmd=$infer_cmd + +echo "============ Important variables =============" +echo "JSR308: $JSR308" +echo "CLASSPATH: $CLASSPATH" +echo "build cmd: $build_cmd" +echo "running cmd: $running_cmd" +echo "=============================================" + +eval "$running_cmd" + +echo "---- Reminder: do not forget to clean up the project! ----" + + diff --git a/src/read/ReadAnnotatedTypeFactory.java b/src/read/ReadAnnotatedTypeFactory.java index d97617f..29dc466 100644 --- a/src/read/ReadAnnotatedTypeFactory.java +++ b/src/read/ReadAnnotatedTypeFactory.java @@ -2,15 +2,11 @@ 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; import org.checkerframework.framework.flow.CFValue; import org.checkerframework.framework.type.AnnotatedTypeFactory; -import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; import org.checkerframework.framework.type.treeannotator.ImplicitsTreeAnnotator; import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; @@ -18,23 +14,23 @@ import org.checkerframework.framework.type.treeannotator.TreeAnnotator; import org.checkerframework.javacutil.AnnotationBuilder; -import read.qual.SafeRead; +import read.qual.NarrowerReadInt; +import read.qual.ReadInt; import read.qual.SafetyBottom; 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 final AnnotationMirror SAFETY_BOTTOM; + protected final AnnotationMirror READ_INT; + protected final AnnotationMirror NARROWER_READ_INT; + protected final AnnotationMirror UNKNOWN_SAFETY; 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); + READ_INT = AnnotationBuilder.fromClass(elements, ReadInt.class); + NARROWER_READ_INT = AnnotationBuilder.fromClass(elements, NarrowerReadInt.class); UNKNOWN_SAFETY = AnnotationBuilder.fromClass(elements, UnknownSafety.class); } @@ -48,17 +44,19 @@ public ReadTreeAnnotator(AnnotatedTypeFactory atypeFactory) { super(atypeFactory); } - @Override - public Void visitUnary(UnaryTree node, AnnotatedTypeMirror type) { - type.replaceAnnotation(UNKNOWN_SAFETY); - return null; - } +// @Override +// public Void visitUnary(UnaryTree node, AnnotatedTypeMirror type) { +// System.err.println(" --- node: " + node + " type: " + type); +// type.replaceAnnotation(UNKNOWN_SAFETY); +// System.err.println(" === node: " + node + " type: " + type); +// return null; +// } - @Override - public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) { - type.replaceAnnotation(UNKNOWN_SAFETY); - return null; - } +// @Override +// public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) { +// type.replaceAnnotation(UNKNOWN_SAFETY); +// return null; +// } } @Override diff --git a/src/read/ReadTransfer.java b/src/read/ReadTransfer.java index b3da5b7..54a1b86 100644 --- a/src/read/ReadTransfer.java +++ b/src/read/ReadTransfer.java @@ -1,17 +1,15 @@ package read; -import java.util.List; +import java.util.Collections; import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; -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.analysis.FlowExpressions.Receiver; -import org.checkerframework.dataflow.cfg.node.GreaterThanOrEqualNode; -import org.checkerframework.dataflow.cfg.node.IntegerLiteralNode; -import org.checkerframework.dataflow.cfg.node.LessThanNode; +import org.checkerframework.dataflow.cfg.node.AssignmentNode; import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.framework.flow.CFAbstractAnalysis; import org.checkerframework.framework.flow.CFAbstractTransfer; @@ -19,170 +17,54 @@ import org.checkerframework.framework.flow.CFValue; import org.checkerframework.javacutil.AnnotationBuilder; -import read.qual.UnsafeRead; -import read.qual.SafeRead; +import read.qual.NarrowerReadInt; +import read.qual.ReadInt; +import read.qual.UnknownSafety; public class ReadTransfer extends CFAbstractTransfer{ - protected AnnotationMirror UNSAFE_READ; - protected AnnotationMirror SAFE_READ; + protected final AnnotationMirror READ_INT; + protected final AnnotationMirror NARROWER_READ_INT; + protected final AnnotationMirror UNKNOWN_SAFETY; public ReadTransfer(ReadAnalysis analysis) { super(analysis); - UNSAFE_READ = AnnotationBuilder.fromClass(analysis.getTypeFactory() - .getElementUtils(), UnsafeRead.class); - SAFE_READ = AnnotationBuilder.fromClass(analysis.getTypeFactory() - .getElementUtils(), SafeRead.class); + READ_INT = AnnotationBuilder.fromClass(analysis.getTypeFactory() + .getElementUtils(), ReadInt.class); + NARROWER_READ_INT = AnnotationBuilder.fromClass(analysis.getTypeFactory() + .getElementUtils(), NarrowerReadInt.class); + UNKNOWN_SAFETY = AnnotationBuilder.fromClass(analysis.getTypeFactory() + .getElementUtils(), UnknownSafety.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); + READ_INT = AnnotationBuilder.fromClass(analysis.getTypeFactory() + .getElementUtils(), ReadInt.class); + NARROWER_READ_INT = AnnotationBuilder.fromClass(analysis.getTypeFactory() + .getElementUtils(), NarrowerReadInt.class); + UNKNOWN_SAFETY = AnnotationBuilder.fromClass(analysis.getTypeFactory() + .getElementUtils(), UnknownSafety.class); } @Override - protected TransferResult strengthenAnnotationOfEqualTo ( - TransferResult res, Node firstNode, - Node secondNode, CFValue firstValue, CFValue secondValue, - boolean notEqualTo) { - res = super.strengthenAnnotationOfEqualTo(res, firstNode, secondNode, - firstValue, secondValue, notEqualTo); - - if (firstNode instanceof IntegerLiteralNode && - ((IntegerLiteralNode) firstNode).getValue() == -1) { - - // This is a trade off for implementing the post-condition @EnsureSafeIf. - // If we refine a qualifier to @SafeRead only if the related value has @UnsafeRead, - // then a programmer has to write a @UnsafeRead annotation to the method's argument - // he/she wants to ensure about. The good part of this is we may only want - // the passing argument has type of @SafeRead, which is reasonable. However, the - // bad part of this is it needs explicit annotation from the programmer side. - // Because programmers don't like writing annotations (let's admit that we all don't like annotations:-<) - // Thus here I loosing the restriction, that is to refine all types to @SafeRead as long as - // it check against with -1. -// if (!secondValue.getType().hasAnnotation(UNSAFE_READ)) { -// return res; //this Equal To doesn't check a read byte or char, thus do nothing. -// } - - CFStore thenStore = res.getThenStore(); - CFStore elseStore = res.getElseStore(); - - List secondParts = splitAssignments(secondNode); - for (Node secondPart : secondParts) { - Receiver secondInternal = FlowExpressions.internalReprOf( - analysis.getTypeFactory(), secondPart); - if (CFStore.canInsertReceiver(secondInternal)) { - thenStore = thenStore == null ? res.getThenStore() - : thenStore; - elseStore = elseStore == null ? res.getElseStore() - : elseStore; - if (notEqualTo) { - thenStore.insertValue(secondInternal, SAFE_READ); - } else { - elseStore.insertValue(secondInternal, SAFE_READ); - } - } - } - - if (thenStore != null) { - return new ConditionalTransferResult<>(res.getResultValue(), - thenStore, elseStore); - } - } - - return res; - } - - @Override - public TransferResult visitLessThan(LessThanNode n, - TransferInput p) { - TransferResult res = super.visitLessThan(n, p); - - Node leftN = n.getLeftOperand(); - Node rightN = n.getRightOperand(); - CFValue leftV = p.getValueOfSubNode(leftN); - CFValue rightV = p.getValueOfSubNode(rightN); - - // case: leftN < 0 - res = strengthenAnnotationOfLessThan(res, leftN, rightN, leftV, rightV, false); - - return res; - } - - @Override - public TransferResult visitGreaterThanOrEqual(GreaterThanOrEqualNode n, - TransferInput p) { - TransferResult res = super.visitGreaterThanOrEqual(n, p); - - Node leftN = n.getLeftOperand(); - Node rightN = n.getRightOperand(); - CFValue leftV = p.getValueOfSubNode(leftN); - CFValue rightV = p.getValueOfSubNode(rightN); - - // case: leftN >= 0 - res = strengthenAnnotationOfLessThan(res, leftN, rightN, leftV, rightV, true); - - return res; - } - - /** - * For expression leftN < rightN or leftN >= rightN: - * refine the annotation of {@code leftN} if {@code rightN} is integer literal 0. - * @param res - * The previous result - * @param leftN - * @param rightN - * @param firstValue - * not used in ReadTransfer. leave for possible up-integration - * @param secondValue - * not used in ReadTransfer. leave for possible up-integration - * @param notLessThan - * If true, indicates the logic is flipped i.e (GreaterOrEqualThan) - * @return - */ - protected TransferResult strengthenAnnotationOfLessThan ( - TransferResult res, Node leftN, - Node rightN, CFValue firstValue, CFValue secondValue, - boolean notLessThan) { - // case: firstNode < 0 - if (rightN instanceof IntegerLiteralNode && - ((IntegerLiteralNode) rightN).getValue() == 0) { - CFStore thenStore = res.getThenStore(); - CFStore elseStore = res.getElseStore(); - List secondParts = splitAssignments(leftN); - for (Node secondPart : secondParts) { - Receiver secondInternal = FlowExpressions.internalReprOf( - analysis.getTypeFactory(), secondPart); - if (CFStore.canInsertReceiver(secondInternal)) { - thenStore = thenStore == null ? res.getThenStore() - : thenStore; - elseStore = elseStore == null ? res.getElseStore() - : elseStore; - if (notLessThan) { - thenStore.insertValue(secondInternal, SAFE_READ); - } else { - elseStore.insertValue(secondInternal, SAFE_READ); - } - } - } - - // case: 0 < rightN - // currently I don't process this part, because of two reasons: - // 1. Doesn't find real code need this case - // 2. although 0 < rightN would imply rightN is safe for casting, - // it still has a bug: the 0x00 byte or 0x0000 char will be missed - - // TODO: should ReadChecker issue a warning like `warning.missed.read.zero` - // in this case? i.e. code like {@code while ((intbuff = in.read()) > 0) {...}} - - if (thenStore != null) { - return new ConditionalTransferResult<>(res.getResultValue(), - thenStore, elseStore); - } + public TransferResult visitAssignment(AssignmentNode n, TransferInput in) { + TransferResult result = super.visitAssignment(n, in); + Node target = n.getTarget(); + Node expression = n.getExpression(); + CFValue expressionValue = getValueFromFactory(expression.getTree(), expression); + CFValue originalTargetValue = getValueFromFactory(target.getTree(), target); + TypeMirror targetType = originalTargetValue.getUnderlyingType(); + +// System.err.println(" ---- expression: " +expression + " value: " + expressionValue); + if (expressionValue.getAnnotations().contains(READ_INT) && + (targetType.getKind() == TypeKind.CHAR || targetType.getKind() == TypeKind.BYTE)) { + CFValue updateTargetValue = analysis.createAbstractValue(Collections.singleton(NARROWER_READ_INT), targetType); + CFStore updateRegularStore = result.getRegularStore(); + updateRegularStore.updateForAssignment(target, updateTargetValue); + TransferResult updatedRes = new RegularTransferResult(updateTargetValue, updateRegularStore); + return updatedRes; } - return res; + return result; } } diff --git a/src/read/ReadVisitor.java b/src/read/ReadVisitor.java index cb7e2ed..a21f2fb 100644 --- a/src/read/ReadVisitor.java +++ b/src/read/ReadVisitor.java @@ -1,25 +1,30 @@ package read; import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.type.TypeKind; - -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 read.qual.UnsafeRead; +import com.sun.source.tree.BinaryTree; +import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.LiteralTree; +import com.sun.source.tree.Tree; +import com.sun.source.tree.Tree.Kind; + +import read.qual.NarrowerReadInt; +import read.qual.ReadInt; public class ReadVisitor extends BaseTypeVisitor { - protected AnnotationMirror UNSAFE_READ; + protected AnnotationMirror READ_INT; + protected AnnotationMirror NARROWER_READ_INT; public ReadVisitor(BaseTypeChecker checker) { super(checker); - UNSAFE_READ = AnnotationBuilder.fromClass(elements, UnsafeRead.class); + READ_INT = AnnotationBuilder.fromClass(elements, ReadInt.class); + NARROWER_READ_INT = AnnotationBuilder.fromClass(elements, NarrowerReadInt.class); } @Override @@ -28,14 +33,24 @@ public ReadAnnotatedTypeFactory createTypeFactory() { } @Override - protected void checkTypecastSafety(TypeCastTree node, Void p) { - AnnotatedTypeMirror castType = atypeFactory.getAnnotatedType(node); - AnnotatedTypeMirror exprType = atypeFactory.getAnnotatedType(node.getExpression()); - if (((castType.getUnderlyingType().getKind() == TypeKind.BYTE || castType.getUnderlyingType().getKind() == TypeKind.CHAR) && - castType.hasAnnotation(UNSAFE_READ))) { - checker.report(Result.failure("cast.unsafe", exprType, castType), node); + public Void visitBinary(BinaryTree node, Void p) { + ExpressionTree lhs = node.getLeftOperand(); + ExpressionTree rhs = node.getRightOperand(); + if (node.getKind() == Kind.NOT_EQUAL_TO || node.getKind() == Kind.EQUAL_TO) { + if ((isReadCharOrByte(lhs) && isEOFIntLiteral(rhs)) + || (isReadCharOrByte(rhs) && isEOFIntLiteral(lhs))) { + checker.report(Result.failure("unsafe.eof.comparision"), node); + } } + return super.visitBinary(node, p); + } - super.checkTypecastSafety(node, p); + private boolean isReadCharOrByte(Tree node) { + return atypeFactory.getAnnotatedType(node).hasAnnotation(NARROWER_READ_INT); } + + private boolean isEOFIntLiteral(Tree node) { + return node.getKind() == Kind.INT_LITERAL && ((LiteralTree) node).getValue().equals(Integer.valueOf(-1)); + } + } diff --git a/src/read/jdk.astub b/src/read/jdk.astub index 957a8c4..d8d0e7e 100644 --- a/src/read/jdk.astub +++ b/src/read/jdk.astub @@ -3,122 +3,122 @@ import read.qual.*; // InputStream stubs package java.io; public abstract class InputStream implements Closeable { - public abstract @UnsafeRead int read() throws IOException; + public abstract @ReadInt int read() throws IOException; } public class FilterInputStream extends InputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class SequenceInputStream extends InputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class PipedInputStream extends InputStream { - public @UnsafeRead synchronized int read() throws IOException; + public @ReadInt synchronized int read() throws IOException; } public class LineNumberInputStream extends FilterInputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class FileInputStream extends InputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class PushbackInputStream extends FilterInputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class ByteArrayInputStream extends InputStream { - public @UnsafeRead synchronized int read(); + public @ReadInt synchronized int read(); } public class StringBufferInputStream extends InputStream { - public @UnsafeRead synchronized int read(); + public @ReadInt synchronized int read(); } public class BufferedInputStream extends FilterInputStream { - public @UnsafeRead synchronized int read() throws IOException; + public @ReadInt synchronized int read() throws IOException; } public class ObjectInputStream extends InputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class ObjectInputStream extends InputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class ObjectInputStream extends InputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } package java.net; public class SocketInputStream extends FileInputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } package javax.swing; public class ProgressMonitorInputStream extends FilterInputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } package javax.sound.sampled; public class AudioInputStream extends InputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } package javax.imageio; public interface ImageInputStream extends DataInput, Closeable { - @UnsafeRead int read() throws IOException; + @ReadInt int read() throws IOException; } public class FileImageInputStream extends ImageInputStreamImpl { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class FileCacheImageInputStream extends ImageInputStreamImpl { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class MemoryCacheImageInputStream extends ImageInputStreamImpl { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } package org.omg.CORBA; public abstract class InputStream extends java.io.InputStream { - public @UnsafeRead int read() throws java.io.IOException; + public @ReadInt int read() throws java.io.IOException; } package java.util.zip; class CheckedInputStream extends FilterInputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class DeflaterInputStream extends FilterInputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } class InflaterInputStream extends FilterInputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } package java.security; public class DigestInputStream extends FilterInputStream { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } // Reader stubs package java.io; public abstract class Reader implements Readable, Closeable { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public abstract class FilterReader extends Reader { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class CharArrayReader extends Reader { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class LineNumberReader extends BufferedReader { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class StringReader extends Reader { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class InputStreamReader extends Reader { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class BufferedReader extends Reader { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } public class PipedReader extends Reader { - public synchronized @UnsafeRead int read() throws IOException; + public synchronized @ReadInt int read() throws IOException; } public class PushbackReader extends FilterReader { - public @UnsafeRead int read() throws IOException; + public @ReadInt int read() throws IOException; } diff --git a/src/read/qual/EnsureSafeIf.java b/src/read/qual/EnsureSafeIf.java deleted file mode 100644 index 1cee0b5..0000000 --- a/src/read/qual/EnsureSafeIf.java +++ /dev/null @@ -1,32 +0,0 @@ -package read.qual; - -import java.lang.annotation.Documented; -import java.lang.annotation.ElementType; -import java.lang.annotation.Retention; -import java.lang.annotation.RetentionPolicy; -import java.lang.annotation.Target; - -import org.checkerframework.framework.qual.ConditionalPostconditionAnnotation; -import org.checkerframework.framework.qual.InheritedAnnotation; - -@Documented -@Retention(RetentionPolicy.RUNTIME) -@Target({ ElementType.METHOD }) -@ConditionalPostconditionAnnotation(qualifier = SafeRead.class) -@InheritedAnnotation -public @interface EnsureSafeIf { - /** - * The Java expressions for which the qualifier holds if the method - * terminates with return value {@link #result()}. - * - * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions - */ - String[] expression(); - - /** - * The return value of the method that needs to hold for the postcondition - * to hold. - */ - boolean result(); -} - diff --git a/src/read/qual/UnsafeRead.java b/src/read/qual/NarrowerReadInt.java similarity index 87% rename from src/read/qual/UnsafeRead.java rename to src/read/qual/NarrowerReadInt.java index 3c79c96..f4abef5 100644 --- a/src/read/qual/UnsafeRead.java +++ b/src/read/qual/NarrowerReadInt.java @@ -7,6 +7,6 @@ @SubtypeOf({UnknownSafety.class}) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) -public @interface UnsafeRead { +public @interface NarrowerReadInt { } diff --git a/src/read/qual/SafeRead.java b/src/read/qual/ReadInt.java similarity index 77% rename from src/read/qual/SafeRead.java rename to src/read/qual/ReadInt.java index 5f2d8a2..4774b8a 100644 --- a/src/read/qual/SafeRead.java +++ b/src/read/qual/ReadInt.java @@ -5,8 +5,8 @@ import org.checkerframework.framework.qual.SubtypeOf; -@SubtypeOf({UnsafeRead.class}) +@SubtypeOf({NarrowerReadInt.class}) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) -public @interface SafeRead { +public @interface ReadInt { } diff --git a/src/read/qual/SafetyBottom.java b/src/read/qual/SafetyBottom.java index 2d3e234..d456b08 100644 --- a/src/read/qual/SafetyBottom.java +++ b/src/read/qual/SafetyBottom.java @@ -7,7 +7,7 @@ import org.checkerframework.framework.qual.LiteralKind; import org.checkerframework.framework.qual.SubtypeOf; -@SubtypeOf({UnknownSafetyLiterals.class, SafeRead.class}) +@SubtypeOf({UnknownSafetyLiterals.class}) @ImplicitFor(literals = { LiteralKind.NULL }) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) public @interface SafetyBottom { diff --git a/src/read/qual/UnknownSafetyLiterals.java b/src/read/qual/UnknownSafetyLiterals.java index 987447b..0e9914d 100644 --- a/src/read/qual/UnknownSafetyLiterals.java +++ b/src/read/qual/UnknownSafetyLiterals.java @@ -7,11 +7,11 @@ import org.checkerframework.framework.qual.SubtypeOf; import org.checkerframework.framework.qual.LiteralKind; -@SubtypeOf({UnsafeRead.class}) +@SubtypeOf({ReadInt.class}) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) @ImplicitFor ( literals = { LiteralKind.INT, LiteralKind.LONG } ) public @interface UnknownSafetyLiterals { -} +} \ No newline at end of file diff --git a/tests/casting/ErrorCasting.java b/tests/casting/ErrorCasting.java index d2b4f49..7ff7480 100644 --- a/tests/casting/ErrorCasting.java +++ b/tests/casting/ErrorCasting.java @@ -7,11 +7,11 @@ import java.io.InputStream; import java.io.Reader; -import read.qual.UnsafeRead; +import read.qual.ReadInt; //@skip-test public class ErrorCasting { - + @SuppressWarnings("unused") public void readCharMethod(@UnsafeRead int unsafeReadBuff, int unknownInt) { int bar = unknownInt = unsafeReadBuff; diff --git a/tests/casting/NormalCasting.java b/tests/casting/NormalCasting.java index c12cd3e..33d52a2 100644 --- a/tests/casting/NormalCasting.java +++ b/tests/casting/NormalCasting.java @@ -6,7 +6,7 @@ import java.io.InputStream; import java.io.Reader; -import read.qual.UnsafeRead; +import read.qual.ReadInt; public class NormalCasting { @SuppressWarnings("unused") @@ -20,7 +20,7 @@ public void method(int foo) { } @SuppressWarnings("unused") - public void readMethod(@UnsafeRead int inbuff, int unkownInt) throws IOException { + public void readMethod(@ReadInt int inbuff, int unkownInt) throws IOException { char unknownSafetyChar_1 = (char) (inbuff + 1); // Should cast up to UnknownSafety, OK char unknownSafetyChar_2 = (char) (inbuff + inbuff); // Should cast up to UnknownSafety, OK char unknownSafetyChar_3 = (char) (inbuff + unkownInt); // Should cast up to UnknownSafety, OK @@ -29,4 +29,4 @@ public void readMethod(@UnsafeRead int inbuff, int unkownInt) throws IOException byte unknownSafetyByte_2 = (byte) (inbuff + inbuff); // Should cast up to UnknownSafety, OK byte unknownSafetyByte_3 = (byte) (inbuff + unkownInt); // Should cast up to UnknownSafety, OK } -} +} \ No newline at end of file diff --git a/tests/cs-examples/CS4InputStream.java b/tests/cs-examples/CS4InputStream.java index ce75506..133ed9b 100644 --- a/tests/cs-examples/CS4InputStream.java +++ b/tests/cs-examples/CS4InputStream.java @@ -10,8 +10,8 @@ public void compliantSolution() throws IOException { int inbuff; @SuppressWarnings("unused") byte data; - while ((inbuff = in.read()) != -1) { - data = (byte) inbuff; // OK + while ((inbuff = in.read()) != -1) { // OK + data = (byte) inbuff; } in.close(); } diff --git a/tests/cs-examples/CS4Reader.java b/tests/cs-examples/CS4Reader.java index 55a9491..9a882ef 100644 --- a/tests/cs-examples/CS4Reader.java +++ b/tests/cs-examples/CS4Reader.java @@ -10,8 +10,8 @@ public void compliantSolution() throws IOException { int inbuff; @SuppressWarnings("unused") char data; - while ((inbuff = in.read()) != -1) { - data = (char) inbuff; // OK + while ((inbuff = in.read()) != -1) { // OK + data = (char) inbuff; } in.close(); } diff --git a/tests/customize-reader/MyReader.java b/tests/customize-reader/MyReader.java index 7ae7bb6..18f9631 100644 --- a/tests/customize-reader/MyReader.java +++ b/tests/customize-reader/MyReader.java @@ -6,8 +6,7 @@ import java.io.InputStream; import java.io.Reader; -import read.qual.EnsureSafeIf; -import read.qual.UnsafeRead; +import read.qual.ReadInt; public class MyReader { InputStream reader; @@ -16,7 +15,7 @@ public class MyReader { this.reader = reader; } - public @UnsafeRead int read() { + public @ReadInt int read() { int inbuff; try { inbuff = this.reader.read(); diff --git a/tests/noc-examples/NOCE4InputStream.java b/tests/noc-examples/NOCE4InputStream.java index 22884cd..9b3a60b 100644 --- a/tests/noc-examples/NOCE4InputStream.java +++ b/tests/noc-examples/NOCE4InputStream.java @@ -10,7 +10,7 @@ public void unsafeWayOfCasting() throws IOException { InputStream in = new FileInputStream("afile"); @SuppressWarnings("unused") byte data; - // :: error: (cast.unsafe) + // :: error: (unsafe.eof.comparision) while ((data = (byte) in.read()) != -1) { //... } diff --git a/tests/noc-examples/NOCE4Reader.java b/tests/noc-examples/NOCE4Reader.java index 5e962ba..905cd8d 100644 --- a/tests/noc-examples/NOCE4Reader.java +++ b/tests/noc-examples/NOCE4Reader.java @@ -9,7 +9,7 @@ public void unsafeWayOfCasting() throws IOException { Reader in = new FileReader("afile"); @SuppressWarnings("unused") char data; - // :: error: (cast.unsafe) + // :: error: (unsafe.eof.comparision) while ((data = (char) in.read()) != -1) { //... } diff --git a/tests/read-typeHierarchy/TypeHierarchy.java b/tests/read-typeHierarchy/TypeHierarchy.java index 433f0e0..6d198ed 100644 --- a/tests/read-typeHierarchy/TypeHierarchy.java +++ b/tests/read-typeHierarchy/TypeHierarchy.java @@ -1,19 +1,18 @@ package read.typeHierarchy; -import read.qual.SafeRead; +import read.qual.ReadInt; import read.qual.SafetyBottom; import read.qual.UnknownSafety; import read.qual.UnknownSafetyLiterals; -import read.qual.UnsafeRead; +import read.qual.NarrowerReadInt; // javac-dev -processorpath ./bin:./build-deps/framework.jar -processor read.ReadChecker -cp ./bin tests/read-typeHierarchy/TypeHierarchy.java /** * type hierarchy is: * - * UnsafeRead <: UnknownSafety - * SafeRead <: UnsafeRead - * UnknownSafetyLiterals <: UnsafeRead - * SafetyBottom <: SafeRead + * NarrowerReadInt <: UnknowSafety + * ReadInt <: NarrowerReadInt + * UnknownSafetyLiterals <: ReadInt * SafetyBottom <: UnknownSafetyLiterals * * @author charleszhuochen @@ -21,28 +20,33 @@ */ public class TypeHierarchy { - void testMethod(int i, @UnsafeRead int unsafeRead, @SafeRead int safeRead, @SafetyBottom int safetyBottom) { + void testMethod(int i, @ReadInt int readInt, @NarrowerReadInt byte narrowerReadInt, + @SafetyBottom int safetyBottom, byte readData) { + int a = readInt; // OK: ReadInt <: UnknownSafety - // :: error: (assignment.type.incompatible) - unsafeRead = i; // ERROR: violate type rule UnsafeRead <: UnknownSafety + a = narrowerReadInt; // OK: NarrowerReadInt <: UnknownSafety - // :: error: (assignment.type.incompatible) - safeRead = unsafeRead; // ERROR: violate type rule SafeRead <: UnsafeRead + a = -1; // OK: UnknownSafetyLiterals <: UnknownSafety + + readData = (byte) readInt; // OK: ReadInt <: UnknownSafety, and lhs will be refined by dataflow to NarrowerReadInt // :: error: (assignment.type.incompatible) - safetyBottom = safeRead; // ERROR: violate type rule SafetyBottom <: SafeRead + readInt = i; // ERROR: violate type rule ReadInt <: UnknownSafety // :: error: (assignment.type.incompatible) - safetyBottom = 1; // ERROR: violate type rule SafetyBottom <: UnknownSafetyLiterals + readInt = narrowerReadInt; // ERROR: violate type rule ReadInt <: NarrowerReadInt - int a = unsafeRead; // OK: UnsafeRead <: UnknownSafety + readInt = -1; // OK: UnknownSafetyLiterals <: ReadInt - unsafeRead = safeRead; // OK: SafeRead <: UnsafeRead + narrowerReadInt = (byte) readInt; // OK: ReadInt <: NarrowerReadInt - unsafeRead = -1; // OK: UnknownSafetyLiterals <: UnsafeRead + // :: error: (assignment.type.incompatible) + safetyBottom = readInt; //ERROR: violate type rule SafetyBottom <: ReadInt - safeRead = safetyBottom; // OK: SafetyBottom <: UnknownSafetyLiterals + // :: error: (assignment.type.incompatible) + safetyBottom = narrowerReadInt; // ERROR: violate type rule SafetyBottom <: NarrowerReadInt + // :: error: (assignment.type.incompatible) + safetyBottom = 1; // ERROR: violate type rule SafetyBottom <: UnknownSafetyLiterals } - } diff --git a/tests/src/ReadTest.java b/tests/src/ReadTest.java index 2ec5aff..4052741 100644 --- a/tests/src/ReadTest.java +++ b/tests/src/ReadTest.java @@ -15,7 +15,6 @@ 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"}; + return new String[]{ "read-typeHierarchy", "noc-examples", "cs-examples", "wtfCodeSOD061102" , "customize-reader", "casting"}; } } diff --git a/tests/wtfCodeSOD061102/WTFCodeSOD061102.java b/tests/wtfCodeSOD061102/WTFCodeSOD061102.java index 5f90a62..549af5b 100644 --- a/tests/wtfCodeSOD061102/WTFCodeSOD061102.java +++ b/tests/wtfCodeSOD061102/WTFCodeSOD061102.java @@ -10,26 +10,26 @@ public void test(boolean _validConnection, InputStream _inputStream) throws IOEx while (true) { char _char; _stringBuffer.append( - // :: error: (cast.unsafe) _char = (char)_inputStream.read()); + // :: error: (unsafe.eof.comparision) if (_char == -1) { break; } else if (_char == '\r') { _stringBuffer.append( - // :: error: (cast.unsafe) _char = (char)_inputStream.read()); + // :: error: (unsafe.eof.comparision) if (_char == -1) { break; } else if (_char == '\n') { _stringBuffer.append( - // :: error: (cast.unsafe) _char = (char)_inputStream.read()); + // :: error: (unsafe.eof.comparision) if (_char == -1) { break; } else if (_char == '\r') { _stringBuffer.append( - // :: error: (cast.unsafe) _char = (char)_inputStream.read()); + // :: error: (unsafe.eof.comparision) if (_char == -1) { break; } else if (_char == '\n') { From 4a46579df10697582aa18128139545230e01812a Mon Sep 17 00:00:00 2001 From: CharlesZ-Chen Date: Tue, 21 Nov 2017 16:38:47 -0500 Subject: [PATCH 2/2] Remove debug classpath in read-check.sh. --- read-check.sh | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/read-check.sh b/read-check.sh index 527eeb5..8970195 100755 --- a/read-check.sh +++ b/read-check.sh @@ -16,6 +16,4 @@ do shift done -target_classpath="/Users/charleszhuochen/Programming/UWaterloo/jsr308/opprop-benchmarks/commons-jcs/commons-jcs-core/target/classes:/Users/charleszhuochen/.m2/repository/commons-logging/commons-logging/1.2/commons-logging-1.2.jar:/Users/charleszhuochen/.m2/repository/commons-dbcp/commons-dbcp/1.4/commons-dbcp-1.4.jar:/Users/charleszhuochen/.m2/repository/commons-pool/commons-pool/1.6/commons-pool-1.6.jar:/Users/charleszhuochen/.m2/repository/org/apache/velocity/velocity-tools/2.0/velocity-tools-2.0.jar:/Users/charleszhuochen/.m2/repository/commons-beanutils/commons-beanutils/1.7.0/commons-beanutils-1.7.0.jar:/Users/charleszhuochen/.m2/repository/commons-digester/commons-digester/1.8/commons-digester-1.8.jar:/Users/charleszhuochen/.m2/repository/commons-chain/commons-chain/1.1/commons-chain-1.1.jar:/Users/charleszhuochen/.m2/repository/commons-collections/commons-collections/3.2/commons-collections-3.2.jar:/Users/charleszhuochen/.m2/repository/commons-validator/commons-validator/1.3.1/commons-validator-1.3.1.jar:/Users/charleszhuochen/.m2/repository/dom4j/dom4j/1.1/dom4j-1.1.jar:/Users/charleszhuochen/.m2/repository/oro/oro/2.0.8/oro-2.0.8.jar:/Users/charleszhuochen/.m2/repository/sslext/sslext/1.2-0/sslext-1.2-0.jar:/Users/charleszhuochen/.m2/repository/org/apache/struts/struts-core/1.3.8/struts-core-1.3.8.jar:/Users/charleszhuochen/.m2/repository/antlr/antlr/2.7.2/antlr-2.7.2.jar:/Users/charleszhuochen/.m2/repository/org/apache/struts/struts-taglib/1.3.8/struts-taglib-1.3.8.jar:/Users/charleszhuochen/.m2/repository/org/apache/struts/struts-tiles/1.3.8/struts-tiles-1.3.8.jar:/Users/charleszhuochen/.m2/repository/org/apache/velocity/velocity/1.6.2/velocity-1.6.2.jar:/Users/charleszhuochen/.m2/repository/commons-lang/commons-lang/2.4/commons-lang-2.4.jar:/Users/charleszhuochen/.m2/repository/commons-httpclient/commons-httpclient/3.1/commons-httpclient-3.1.jar:/Users/charleszhuochen/.m2/repository/commons-codec/commons-codec/1.2/commons-codec-1.2.jar:/Users/charleszhuochen/.m2/repository/javax/servlet/servlet-api/2.5/servlet-api-2.5.jar:/Users/charleszhuochen/Programming/UWaterloo/jsr308/opprop-benchmarks/commons-jcs/commons-jcs-core/target/test-classes:/Users/charleszhuochen/Programming/UWaterloo/jsr308/opprop-benchmarks/commons-jcs/commons-jcs-core/target/classes:/Users/charleszhuochen/.m2/repository/commons-logging/commons-logging/1.2/commons-logging-1.2.jar:/Users/charleszhuochen/.m2/repository/commons-dbcp/commons-dbcp/1.4/commons-dbcp-1.4.jar:/Users/charleszhuochen/.m2/repository/commons-pool/commons-pool/1.6/commons-pool-1.6.jar:/Users/charleszhuochen/.m2/repository/hsqldb/hsqldb/1.8.0.10/hsqldb-1.8.0.10.jar:/Users/charleszhuochen/.m2/repository/org/apache/commons/commons-collections4/4.1/commons-collections4-4.1.jar:/Users/charleszhuochen/.m2/repository/junit/junit/4.11/junit-4.11.jar:/Users/charleszhuochen/.m2/repository/org/hamcrest/hamcrest-core/1.3/hamcrest-core-1.3.jar:/Users/charleszhuochen/.m2/repository/org/hamcrest/hamcrest-library/1.3/hamcrest-library-1.3.jar:/Users/charleszhuochen/.m2/repository/log4j/log4j/1.2.17/log4j-1.2.17.jar:/Users/charleszhuochen/.m2/repository/org/apache/velocity/velocity-tools/2.0/velocity-tools-2.0.jar:/Users/charleszhuochen/.m2/repository/commons-beanutils/commons-beanutils/1.7.0/commons-beanutils-1.7.0.jar:/Users/charleszhuochen/.m2/repository/commons-digester/commons-digester/1.8/commons-digester-1.8.jar:/Users/charleszhuochen/.m2/repository/commons-chain/commons-chain/1.1/commons-chain-1.1.jar:/Users/charleszhuochen/.m2/repository/commons-collections/commons-collections/3.2/commons-collections-3.2.jar:/Users/charleszhuochen/.m2/repository/commons-validator/commons-validator/1.3.1/commons-validator-1.3.1.jar:/Users/charleszhuochen/.m2/repository/dom4j/dom4j/1.1/dom4j-1.1.jar:/Users/charleszhuochen/.m2/repository/oro/oro/2.0.8/oro-2.0.8.jar:/Users/charleszhuochen/.m2/repository/sslext/sslext/1.2-0/sslext-1.2-0.jar:/Users/charleszhuochen/.m2/repository/org/apache/struts/struts-core/1.3.8/struts-core-1.3.8.jar:/Users/charleszhuochen/.m2/repository/antlr/antlr/2.7.2/antlr-2.7.2.jar:/Users/charleszhuochen/.m2/repository/org/apache/struts/struts-taglib/1.3.8/struts-taglib-1.3.8.jar:/Users/charleszhuochen/.m2/repository/org/apache/struts/struts-tiles/1.3.8/struts-tiles-1.3.8.jar:/Users/charleszhuochen/.m2/repository/org/apache/velocity/velocity/1.6.2/velocity-1.6.2.jar:/Users/charleszhuochen/.m2/repository/commons-lang/commons-lang/2.4/commons-lang-2.4.jar:/Users/charleszhuochen/.m2/repository/commons-httpclient/commons-httpclient/3.1/commons-httpclient-3.1.jar:/Users/charleszhuochen/.m2/repository/commons-codec/commons-codec/1.2/commons-codec-1.2.jar:/Users/charleszhuochen/.m2/repository/javax/servlet/servlet-api/2.5/servlet-api-2.5.jar::/Users/charleszhuochen/Programming/UWaterloo/jsr308/opprop-benchmarks/commons-jcs/inferDebugBuild::/Users/charleszhuochen/Programming/UWaterloo/jsr308/ReadChecker/bin:/Users/charleszhuochen/Programming/UWaterloo/jsr308/ReadChecker/lib" - -$JAVAC -processor read.ReadChecker -cp $READ_CHECKER/bin:$READ_CHECKER/lib:$target_classpath $java_files +$JAVAC -processor read.ReadChecker -cp $READ_CHECKER/bin:$READ_CHECKER/lib $java_files