Skip to content

Commit

Permalink
Check determinism after, not during, parsing a JavaExpression
Browse files Browse the repository at this point in the history
  • Loading branch information
@mernst
mernst committed Feb 18, 2021
1 parent bd99842 commit d70dd74
Show file tree
Hide file tree
Showing 43 changed files with 553 additions and 337 deletions.
14 changes: 14 additions & 0 deletions changelog.txt
View file
Expand Up @@ -24,6 +24,20 @@ Changes to protected fields in `OverrideChecker`:

Moved JavaExpressionParseUtil#fromVariableTree to JavaExpression.

Parsing a Java expression no longer requires the formal parameters
`AnnotationProvider provider` or `boolean allowNonDeterministic`. Methods
in `JavaExpression` with simplified signatures include
* `fromArrayAccess`
* `fromNodeFieldAccess`
* `fromNode`
* `fromTree`
* `getParametersOfEnclosingMethod`
* `getReceiver`

`CFAbstractStore.insertValue` does nothing if passed a nondeterministic
expression. Use new method `CFAbstractStore.insertValuePermitNondeterministic`
to map a nondeterministic expression to a value.

**Closed issues:**

---------------------------------------------------------------------------
Expand Down
2 changes: 1 addition & 1 deletion checker/jtreg/nullness/issue1582/Foo.out
View file
@@ -1,2 +1,2 @@
Foo.java:14:20: compiler.err.proc.messager: (flowexpr.parse.error)
Foo.java:15:20: compiler.err.proc.messager: (flowexpr.parse.error)
1 error
2 changes: 2 additions & 0 deletions checker/jtreg/nullness/issue1582/foo/Foo.java
View file
Expand Up @@ -2,6 +2,7 @@

import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.qual.Pure;

public class Foo {

Expand All @@ -15,6 +16,7 @@ public boolean hasTheObject() {
return false;
}

@Pure
public @Nullable Object getTheObject() {
return null;
}
Expand Down
5 changes: 2 additions & 3 deletions checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterTransfer.java
View file
Expand Up @@ -45,8 +45,7 @@ public TransferResult<CFValue, CFStore> visitMethodInvocation(
if (cats.value() == null) {
tu.failure(cats, "i18nformat.indirect.arguments");
} else {
JavaExpression firstParam =
JavaExpression.fromNode(atypeFactory, node.getArgument(0));
JavaExpression firstParam = JavaExpression.fromNode(node.getArgument(0));
AnnotationMirror anno =
atypeFactory.treeUtil.categoriesToFormatAnnotation(cats.value());
thenStore.insertValue(firstParam, anno);
Expand All @@ -60,7 +59,7 @@ public TransferResult<CFValue, CFStore> visitMethodInvocation(
CFStore elseStore = thenStore.copy();
ConditionalTransferResult<CFValue, CFStore> newResult =
new ConditionalTransferResult<>(result.getResultValue(), thenStore, elseStore);
JavaExpression firstParam = JavaExpression.fromNode(atypeFactory, node.getArgument(0));
JavaExpression firstParam = JavaExpression.fromNode(node.getArgument(0));
AnnotationBuilder builder =
new AnnotationBuilder(tu.processingEnv, I18nInvalidFormat.class);
// No need to set a value of @I18nInvalidFormat
Expand Down
10 changes: 5 additions & 5 deletions checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanTransfer.java
View file
Expand Up @@ -51,7 +51,7 @@ protected void refineGT(
(LessThanAnnotatedTypeFactory) analysis.getTypeFactory();
// left > right so right < left
// Refine right to @LessThan("left")
JavaExpression leftJe = JavaExpression.fromNode(factory, left);
JavaExpression leftJe = JavaExpression.fromNode(left);
if (leftJe != null && leftJe.isUnassignableByOtherCode()) {
List<String> lessThanExpressions =
LessThanAnnotatedTypeFactory.getLessThanExpressions(rightAnno);
Expand All @@ -62,7 +62,7 @@ protected void refineGT(
if (!isDoubleOrFloatLiteral(leftJe)) {
lessThanExpressions.add(leftJe.toString());
}
JavaExpression rightJe = JavaExpression.fromNode(analysis.getTypeFactory(), right);
JavaExpression rightJe = JavaExpression.fromNode(right);
store.insertValue(rightJe, factory.createLessThanQualifier(lessThanExpressions));
}
}
Expand All @@ -83,7 +83,7 @@ protected void refineGTE(
(LessThanAnnotatedTypeFactory) analysis.getTypeFactory();
// left > right so right is less than left
// Refine right to @LessThan("left")
JavaExpression leftJe = JavaExpression.fromNode(factory, left);
JavaExpression leftJe = JavaExpression.fromNode(left);
if (leftJe != null && leftJe.isUnassignableByOtherCode()) {
List<String> lessThanExpressions =
LessThanAnnotatedTypeFactory.getLessThanExpressions(rightAnno);
Expand All @@ -94,7 +94,7 @@ protected void refineGTE(
if (!isDoubleOrFloatLiteral(leftJe)) {
lessThanExpressions.add(incrementedExpression(leftJe));
}
JavaExpression rightJe = JavaExpression.fromNode(analysis.getTypeFactory(), right);
JavaExpression rightJe = JavaExpression.fromNode(right);
store.insertValue(rightJe, factory.createLessThanQualifier(lessThanExpressions));
}
}
Expand All @@ -105,7 +105,7 @@ public TransferResult<CFValue, CFStore> visitNumericalSubtraction(
NumericalSubtractionNode n, TransferInput<CFValue, CFStore> in) {
LessThanAnnotatedTypeFactory factory =
(LessThanAnnotatedTypeFactory) analysis.getTypeFactory();
JavaExpression leftJe = JavaExpression.fromNode(factory, n.getLeftOperand());
JavaExpression leftJe = JavaExpression.fromNode(n.getLeftOperand());
if (leftJe != null && leftJe.isUnassignableByOtherCode()) {
ValueAnnotatedTypeFactory valueFactory = factory.getValueAnnotatedTypeFactory();
Long right = ValueCheckerUtils.getMinValue(n.getRightOperand().getTree(), valueFactory);
Expand Down
12 changes: 6 additions & 6 deletions checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundTransfer.java
View file
Expand Up @@ -205,15 +205,15 @@ private void notEqualToValue(
if (aTypeFactory.areSameByClass(otherAnno, NonNegative.class)) {
List<Node> internals = splitAssignments(otherNode);
for (Node internal : internals) {
JavaExpression je = JavaExpression.fromNode(aTypeFactory, internal);
JavaExpression je = JavaExpression.fromNode(internal);
store.insertValue(je, POS);
}
}
} else if (intLiteral == -1) {
if (aTypeFactory.areSameByClass(otherAnno, GTENegativeOne.class)) {
List<Node> internals = splitAssignments(otherNode);
for (Node internal : internals) {
JavaExpression je = JavaExpression.fromNode(aTypeFactory, internal);
JavaExpression je = JavaExpression.fromNode(internal);
store.insertValue(je, NN);
}
}
Expand Down Expand Up @@ -265,7 +265,7 @@ private void notEqualsLessThan(
if (!isNonNegative(leftAnno) || !isNonNegative(otherAnno)) {
return;
}
JavaExpression otherJe = JavaExpression.fromNode(aTypeFactory, otherNode);
JavaExpression otherJe = JavaExpression.fromNode(otherNode);
if (aTypeFactory
.getLessThanAnnotatedTypeFactory()
.isLessThanOrEqual(leftNode.getTree(), otherJe.toString())) {
Expand Down Expand Up @@ -295,7 +295,7 @@ protected void refineGT(
return;
}

JavaExpression leftJe = JavaExpression.fromNode(aTypeFactory, left);
JavaExpression leftJe = JavaExpression.fromNode(left);

if (AnnotationUtils.areSame(rightAnno, GTEN1)) {
store.insertValue(leftJe, NN);
Expand Down Expand Up @@ -332,7 +332,7 @@ protected void refineGTE(
return;
}

JavaExpression leftJe = JavaExpression.fromNode(aTypeFactory, left);
JavaExpression leftJe = JavaExpression.fromNode(left);

AnnotationMirror newLBType =
aTypeFactory.getQualifierHierarchy().greatestLowerBound(rightAnno, leftAnno);
Expand Down Expand Up @@ -717,7 +717,7 @@ protected void addInformationFromPreconditions(
for (VariableTree variableTree : paramTrees) {
if (TreeUtils.typeOf(variableTree).getKind() == TypeKind.CHAR) {
JavaExpression je = JavaExpression.fromVariableTree(variableTree);
info.insertValue(je, aTypeFactory.NN);
info.insertValuePermitNondeterministic(je, aTypeFactory.NN);
}
}
}
Expand Down
3 changes: 1 addition & 2 deletions ...src/main/java/org/checkerframework/checker/index/samelen/SameLenAnnotatedTypeFactory.java
View file
Expand Up @@ -291,8 +291,7 @@ public Void visitNewArray(NewArrayTree node, AnnotatedTypeMirror type) {
AnnotationMirror sequenceAnno =
getAnnotatedType(sequenceTree).getAnnotationInHierarchy(UNKNOWN);

JavaExpression sequenceExpr =
JavaExpression.fromTree(this.atypeFactory, sequenceTree);
JavaExpression sequenceExpr = JavaExpression.fromTree(sequenceTree);
if (mayAppearInSameLen(sequenceExpr)) {
String recString = sequenceExpr.toString();
if (areSameByClass(sequenceAnno, SameLenUnknown.class)) {
Expand Down
18 changes: 7 additions & 11 deletions checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenTransfer.java
View file
Expand Up @@ -90,10 +90,8 @@ public TransferResult<CFValue, CFStore> visitAssignment(
// "lengthNodeReceiver.length()"

// targetRec is the receiver for the left hand side of the assignment.
JavaExpression targetRec =
JavaExpression.fromNode(analysis.getTypeFactory(), node.getTarget());
JavaExpression otherRec =
JavaExpression.fromNode(analysis.getTypeFactory(), lengthNodeReceiver);
JavaExpression targetRec = JavaExpression.fromNode(node.getTarget());
JavaExpression otherRec = JavaExpression.fromNode(lengthNodeReceiver);

AnnotationMirror lengthNodeAnnotation =
aTypeFactory
Expand Down Expand Up @@ -121,11 +119,9 @@ public TransferResult<CFValue, CFStore> visitAssignment(
// If the left side of the assignment is an array or a string, then have both the right and
// left side be SameLen of each other.

JavaExpression targetRec =
JavaExpression.fromNode(analysis.getTypeFactory(), node.getTarget());
JavaExpression targetRec = JavaExpression.fromNode(node.getTarget());

JavaExpression exprRec =
JavaExpression.fromNode(analysis.getTypeFactory(), node.getExpression());
JavaExpression exprRec = JavaExpression.fromNode(node.getExpression());

if (IndexUtil.isSequenceType(node.getTarget().getType())
|| (rightAnno != null && aTypeFactory.areSameByClass(rightAnno, SameLen.class))) {
Expand Down Expand Up @@ -186,11 +182,11 @@ private void refineEq(Node left, Node right, CFStore store) {
List<JavaExpression> exprs = new ArrayList<>();
List<AnnotationMirror> annos = new ArrayList<>();
for (Node internal : splitAssignments(left)) {
exprs.add(JavaExpression.fromNode(analysis.getTypeFactory(), internal));
exprs.add(JavaExpression.fromNode(internal));
annos.add(getAnno(internal));
}
for (Node internal : splitAssignments(right)) {
exprs.add(JavaExpression.fromNode(analysis.getTypeFactory(), internal));
exprs.add(JavaExpression.fromNode(internal));
annos.add(getAnno(internal));
}

Expand Down Expand Up @@ -298,7 +294,7 @@ protected void addInformationFromPreconditions(
Collections.singletonList(paramNames.get(index)));
JavaExpression otherParamRec =
JavaExpression.fromVariableTree(paramTrees.get(otherParamIndex));
info.insertValue(otherParamRec, newSameLen);
info.insertValuePermitNondeterministic(otherParamRec, newSameLen);
}
}
}
Expand Down
2 changes: 1 addition & 1 deletion checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenVisitor.java
View file
Expand Up @@ -40,7 +40,7 @@ protected void commonAssignmentCheck(
&& !(valueType.hasAnnotation(PolySameLen.class)
&& varType.hasAnnotation(PolySameLen.class))) {

JavaExpression rhs = JavaExpression.fromTree(atypeFactory, (ExpressionTree) valueTree);
JavaExpression rhs = JavaExpression.fromTree((ExpressionTree) valueTree);
if (rhs != null && SameLenAnnotatedTypeFactory.mayAppearInSameLen(rhs)) {
String rhsExpr = rhs.toString();
AnnotationMirror am = valueType.getAnnotation(SameLen.class);
Expand Down
2 changes: 1 addition & 1 deletion ...ker/src/main/java/org/checkerframework/checker/index/searchindex/SearchIndexTransfer.java
View file
Expand Up @@ -65,7 +65,7 @@ private void refineSearchIndexToNegativeIndexFor(
List<String> arrays =
ValueCheckerUtils.getValueOfAnnotationWithStringArgument(rightSI);
AnnotationMirror nif = aTypeFactory.createNegativeIndexFor(arrays);
store.insertValue(JavaExpression.fromNode(analysis.getTypeFactory(), right), nif);
store.insertValue(JavaExpression.fromNode(right), nif);
}
}
}
Expand Down
10 changes: 9 additions & 1 deletion checker/src/main/java/org/checkerframework/checker/index/upperbound/OffsetEquation.java
View file
Expand Up @@ -426,9 +426,17 @@ public static OffsetEquation createOffsetFromNode(
return eq;
}

/**
* Updates an offset equation from a Node.
*
* @param node the Node from which to create an offset equation
* @param factory an AnnotationTypeFactory
* @param eq an OffsetEquation to update
* @param op '+' or '-'
*/
private static void createOffsetFromNode(
Node node, AnnotationProvider factory, OffsetEquation eq, char op) {
JavaExpression je = JavaExpression.fromNode(factory, node);
JavaExpression je = JavaExpression.fromNode(node);
if (je instanceof Unknown || je == null) {
if (node instanceof NumericalAdditionNode) {
createOffsetFromNode(
Expand Down

0 comments on commit d70dd74

Please sign in to comment.