src/checkers/typestate/TransitionElement.java tests/typestate/BooleanMethodReceiverState.java tests/typestate/BooleanMethodReceiverState.out @@ -7,7 +7,7 @@ export DEBUGOPTS="-J-Xms48m -J-Xdebug -J-Xrunjdwp:transport=dt_socket,server=y,s #CHECKER=checkers.javari.JavariChecker CHECKER=checkers.typestate.TypestateChecker -SOURCES=tests/work/work/Test1.java +SOURCES=tests/work/work/Test6.java #SOURCES=src/checkers/typestate/Any.java javac $DEBUGOPTS -processor $CHECKER -sourcepath src -cp $CLASSPATH -d build $SOURCES debug.sh @@ -26,6 +26,7 @@ import javax.lang.model.util.Elements; * - removed the {@code Map<Location, AnnotationMirror> flowResults} field and all its usages * - removed the {@code void recordBits(TreePath path)} method and all its usages * - modified the analysis of try-catch-finally to be more accurate + * - modified {@code alive} to be protected * * @author Adam Warski (adam at warski dot org) * @author The authors of the {@link Flow} class. @@ -98,7 +99,7 @@ public class MainFlow extends TreePathScanner<Void, Void> { * Stores the result of liveness analysis, required by the GEN-KILL analysis * for proper handling of jumps (break, return, throw, etc.). */ - private boolean alive = true; + protected boolean alive = true; /** * Tracks annotations in potential exception-throwing statements in try blocks. src/checkers/flow/MainFlow.java @@ -57,9 +57,9 @@ public class StateAnnotationsDetector extends TreePathScanner<Void, Set<Annotati if (typestateUtil.isAnyStateAnnotation(annotation) || isStateAnnotation) { // Checking if the annotation doesn't define a transition to another state. If so, adding that state. // Also checking conditional transition states. - AnnotationMirror afterAnnotation = typestateUtil.getAfterElementValue(annotation); - AnnotationMirror afterTrueAnnotation = typestateUtil.getAfterTrueElementValue(annotation); - AnnotationMirror afterFalseAnnotation = typestateUtil.getAfterFalseElementValue(annotation); + AnnotationMirror afterAnnotation = typestateUtil.getTransitionElementValue(annotation, TransitionElement.AFTER); + AnnotationMirror afterTrueAnnotation = typestateUtil.getTransitionElementValue(annotation, TransitionElement.AFTER_TRUE); + AnnotationMirror afterFalseAnnotation = typestateUtil.getTransitionElementValue(annotation, TransitionElement.AFTER_FALSE); if (afterAnnotation != null) { addStateAnnotation(afterAnnotation, true, to); } if (afterTrueAnnotation != null) { addStateAnnotation(afterTrueAnnotation, true, to); } if (afterFalseAnnotation != null) { addStateAnnotation(afterFalseAnnotation, true, to); } src/checkers/typestate/StateAnnotationsDetector.java @@ -6,9 +6,11 @@ import checkers.types.AnnotatedTypeMirror; import checkers.types.AnnotatedTypeFactory; import checkers.util.InternalUtils; import checkers.util.AnnotationUtils; +import checkers.util.TreeUtils; import checkers.source.Result; import checkers.source.SourceChecker; import com.sun.source.tree.*; +import com.sun.source.util.TreeScanner; import javax.lang.model.element.*; import javax.lang.model.type.DeclaredType; @@ -28,6 +30,9 @@ public class TypestateFlow extends MainFlow { private final TypestateUtil typestateUtil; + // The transition element which should be read. + protected TransitionElement transitionElement = TransitionElement.AFTER; + public TypestateFlow(SourceChecker checker, Set<AnnotationMirror> annotations, AnnotatedTypeFactory factory, CompilationUnitTree root, TypestateUtil typestateUtil) { super(checker, root, annotations, factory); @@ -167,7 +172,12 @@ public class TypestateFlow extends MainFlow { } } - AnnotationMirror afterAnnotation = typestateUtil.getAfterElementValue(declaredAnnotation); + // Trying to read the specific transition element + AnnotationMirror afterAnnotation = typestateUtil.getTransitionElementValue(declaredAnnotation, transitionElement); + // If no value was found, and the element wasn't the normal one ('after'), trying to read it. + if (afterAnnotation == null && transitionElement != TransitionElement.AFTER) { + afterAnnotation = typestateUtil.getTransitionElementValue(declaredAnnotation, TransitionElement.AFTER); + } // Currently the transitions will only work for variables - hence checking the elementIdx. if (elementIdx >= 0 && afterAnnotation != null && annotations.contains(afterAnnotation)) { // If the "after" annotation is a state annotation, changing the state of the @@ -225,4 +235,131 @@ public class TypestateFlow extends MainFlow { protected void updateExceptionBits() { // Exception states are handled already. Doing nothing here. } + + @Override + protected void scanCond(Tree tree) { + // So far only simple or negated comparisions of a method call to a constant are supported. + boolean supported = isSupportedLogic(tree); + + if (!supported) { + super.scanCond(tree); + return; + } + + if (tree == null) { + return; + } + + GenKillBits<AnnotationMirror> before = GenKillBits.copy(annos); + + // Scanning the condition twice: once with the after-true element active, once with the active-false element + // active. + transitionElement = TransitionElement.AFTER_TRUE; + alive = true; + scan(tree, null); + GenKillBits<AnnotationMirror> afterTrue = annos; + + transitionElement = TransitionElement.AFTER_FALSE; + annos = before; + alive = true; + scan(tree, null); + GenKillBits<AnnotationMirror> afterFalse = annos; + + transitionElement = TransitionElement.AFTER; + + // Now splitting the annotation set appropriately + if (annos != null) { + // In case of a complement, we have to switch the true and false + if (inverted(tree)) { + annosWhenTrue = afterFalse; + annosWhenFalse = afterTrue; + } else { + annosWhenTrue = afterTrue; + annosWhenFalse = afterFalse; + } + + annos = null; + } + } + + /** + * @param tree Tree to check. + * @return True if the result of the method is checked to be false (not true). + */ + private static boolean inverted(Tree tree) { + tree = TreeUtils.skipParens(tree); + final boolean[] inverted = new boolean[1]; + switch (tree.getKind()) { + case METHOD_INVOCATION: + return false; + case EQUAL_TO: + inverted[0] = false; + break; + case NOT_EQUAL_TO: + inverted[0] = true; + break; + case LOGICAL_COMPLEMENT: + return !inverted(((UnaryTree)tree).getExpression()); + default: + throw new RuntimeException("Unsupported tree kind: " + tree.getKind()); + } + + // Now checking if the constant to which the method invocation is compared is true or false. + // In case of false - we have to invert the result. + tree.accept(new TreeScanner<Void, Void>() { + @Override + public Void visitLiteral(LiteralTree node, Void aVoid) { + Object value = node.getValue(); + if (value instanceof Boolean && !((Boolean) value)) { + inverted[0] = !inverted[0]; + } + return null; + } + }, null); + + + return inverted[0]; + } + + /** + * Copied and adapted from <code>NullnessFlow</code> as it is private there. + * + * @param tree The tree to check. + * @return True if the logical statement in the given tree is supported. + */ + private static boolean isSupportedLogic(Tree tree) { + tree = TreeUtils.skipParens(tree); + // First checking the kind of the tree + switch (tree.getKind()) { + case EQUAL_TO: + case NOT_EQUAL_TO: + break; + case METHOD_INVOCATION: + return true; + case LOGICAL_COMPLEMENT: + return isSupportedLogic(((UnaryTree)tree).getExpression()); + default: + return false; + } + + // And now checking that the tree contains a method invocation and a constant + final int[] methodInvoked = new int[]{0}; + final int[] constant = new int[]{0}; + + tree.accept(new TreeScanner<Void, Void>() { + @Override + public Void visitMethodInvocation(MethodInvocationTree node, Void aVoid) { + methodInvoked[0]++; + return null; + } + + @Override + public Void visitLiteral(LiteralTree node, Void aVoid) { + constant[0]++; + return null; + } + }, null); + + return methodInvoked[0] == 1 && constant[0] == 1; + } } src/checkers/typestate/TypestateFlow.java @@ -15,11 +15,8 @@ import java.util.Set; * @author Adam Warski (adam at warski dot org) */ public class TypestateUtil { - public static final String TRANSITION_ELEMENT_NAME = "after"; public static final String EXCEPT_ELEMENT_NAME = "except"; - public static final String EXCEPTION_ELEMENT_NAME = "onException"; - public static final String AFTER_TRUE_ELEMENT_NAME = "afterTrue"; - public static final String AFTER_FALSE_ELEMENT_NAME = "afterFalse"; + public static final String EXCEPTION_ELEMENT_NAME = "onException"; private final TypeMirror stateAnnotationType; private final TypeMirror anyStateAnnotationType; @@ -109,30 +106,13 @@ public class TypestateUtil { } /** - * @param stateAnnotation State annotation from which to read the "after" element. - * @return The state annotation representing the value of the "after" element of the given annotation or null, - * if the element is not specified or is not a (state) annotation. - */ - public @Nullable AnnotationMirror getAfterElementValue(AnnotationMirror stateAnnotation) { - return getSingleAnnotationElementValue(stateAnnotation, TRANSITION_ELEMENT_NAME); - } - - /** - * @param stateAnnotation State annotation from which to read the "afterTrue" element. - * @return The state annotation representing the value of the "afterTrue" element of the given annotation or null, - * if the element is not specified or is not a (state) annotation. - */ - public @Nullable AnnotationMirror getAfterTrueElementValue(AnnotationMirror stateAnnotation) { - return getSingleAnnotationElementValue(stateAnnotation, AFTER_TRUE_ELEMENT_NAME); - } - - /** - * @param stateAnnotation State annotation from which to read the "afterFalse" element. - * @return The state annotation representing the value of the "afterFalse" element of the given annotation or null, + * @param stateAnnotation State annotation from which to read the transition element. + * @param element The transition element to read. + * @return The state annotation representing the value of the transition element of the given annotation or null, * if the element is not specified or is not a (state) annotation. */ - public @Nullable AnnotationMirror getAfterFalseElementValue(AnnotationMirror stateAnnotation) { - return getSingleAnnotationElementValue(stateAnnotation, AFTER_FALSE_ELEMENT_NAME); + public @Nullable AnnotationMirror getTransitionElementValue(AnnotationMirror stateAnnotation, TransitionElement element) { + return getSingleAnnotationElementValue(stateAnnotation, element.getElementName()); } /** src/checkers/typestate/TypestateUtil.java @@ -6,7 +6,7 @@ export CLASSPATH=/Users/adamw/jsr308/checkers/checkers.jar:/Users/adamw/jsr308/j #CHECKER=checkers.javari.JavariChecker CHECKER=checkers.typestate.TypestateChecker -SOURCES=tests/work/work/Test1.java +SOURCES=tests/work/work/Test6.java #SOURCES=src/checkers/typestate/Any.java #SOURCES=tests/typestate/SimpleReceiverTransitionState.java test.sh @@ -106,4 +106,10 @@ public class TypestateTest extends CheckerTest { public void testFinallyExceptionState() { test(); } + + /** Test checking results of boolean methods invoked on receiver with afterTrue and afterFalse transitions */ + @Test + public void testBooleanMethodReceiverState() { + test(); + } } tests/src/checkers/typestate/test/TypestateTest.java 754729199c9238a628990f1a031fe4daf9d2f961 Adam Warski adam@warski.org http://github.com/adamw/jsr308-typestate-checker/commit/818810d1c4023e690fae1bc6d9a349e7e9101aa4 818810d1c4023e690fae1bc6d9a349e7e9101aa4 2009-09-21T11:16:40-07:00 2009-09-21T11:16:40-07:00 Implementing the logic of afterTrue and afterFalse checking plus test ba42d0c0d66663573f352d2163719f0bafb921c7 Adam Warski adam@warski.org