Skip to content

Change read check mechanism. Initial commit. #8

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
CharlesZ-Chen wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Change read check mechanism. Initial commit. #8

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f87f55e
Change read check mechanism. Initial commit.
CharlesZ-Chen Nov 21, 2017
4a46579
Remove debug classpath in read-check.sh.
CharlesZ-Chen Nov 21, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions FooProject/src/Foo.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
//...
}
Expand All @@ -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) {
//...
}
Expand Down
20 changes: 19 additions & 1 deletion run-dljc.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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! ----"


42 changes: 20 additions & 22 deletions src/read/ReadAnnotatedTypeFactory.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,39 +2,35 @@

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;
import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator;
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<CFValue, CFStore, ReadTransfer, ReadAnalysis> {
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);
}

Expand All @@ -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
Expand Down
198 changes: 40 additions & 158 deletions src/read/ReadTransfer.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,188 +1,70 @@
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;
import org.checkerframework.framework.flow.CFStore;
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<CFValue, CFStore, ReadTransfer>{
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<CFValue, CFStore, ReadTransfer> 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<CFValue, CFStore> strengthenAnnotationOfEqualTo (
TransferResult<CFValue, CFStore> 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<Node> 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<CFValue, CFStore> visitLessThan(LessThanNode n,
TransferInput<CFValue, CFStore> p) {
TransferResult<CFValue, CFStore> 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<CFValue, CFStore> visitGreaterThanOrEqual(GreaterThanOrEqualNode n,
TransferInput<CFValue, CFStore> p) {
TransferResult<CFValue, CFStore> 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<CFValue, CFStore> strengthenAnnotationOfLessThan (
TransferResult<CFValue, CFStore> 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<Node> 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<CFValue, CFStore> visitAssignment(AssignmentNode n, TransferInput<CFValue, CFStore> in) {
TransferResult<CFValue, CFStore> 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<CFValue, CFStore> updatedRes = new RegularTransferResult<CFValue, CFStore>(updateTargetValue, updateRegularStore);
return updatedRes;
}

return res;
return result;
}
}
Loading