Nullness: Track correlated conditions of equality tests of variables.

This commit is contained in:
Cornelius Riemenschneider
2019-11-21 19:24:40 +01:00
parent 92f32a12d8
commit 5d4b6c3a8c
3 changed files with 27 additions and 3 deletions

View File

@@ -30,6 +30,27 @@ InstanceOfExpr instanceofExpr(SsaVariable v, Expr type) {
result.getExpr() = v.getAUse()
}
/**
* Gets an expression of the form `v1` == `v2` or `v1` != `v2`.
* The predicate is symmetric in `v1` and `v2`.
*/
BinaryExpr varComparisonExpr(SsaVariable v1, SsaVariable v2, boolean isEqualExpr) {
(
result.getLeftOperand() = v1.getAUse() and
result.getRightOperand() = v2.getAUse()
or
result.getLeftOperand() = v2.getAUse() and
result.getRightOperand() = v1.getAUse()
) and
(
result instanceof EQExpr and
isEqualExpr = true
or
result instanceof NEExpr and
isEqualExpr = false
)
}
/** Gets an expression that is provably not `null`. */
Expr clearlyNotNullExpr(Expr reason) {
result instanceof ClassInstanceExpr and reason = result

View File

@@ -522,6 +522,12 @@ private predicate correlatedConditions(
t1.getType() = t2.getType() and
inverted = false
)
or
exists(SsaVariable v1, SsaVariable v2, boolean branch1, boolean branch2 |
cond1.getCondition() = varComparisonExpr(v1, v2, branch1) and
cond2.getCondition() = varComparisonExpr(v1, v2, branch2) and
inverted = branch1.booleanXor(branch2)
)
)
}

View File

@@ -17,9 +17,6 @@
| B.java:190:7:190:7 | o | Variable $@ may be null here because of $@ assignment. | B.java:178:5:178:20 | Object o | o | B.java:186:5:186:12 | ...=... | this |
| B.java:279:7:279:7 | a | Variable $@ may be null here because of $@ assignment. | B.java:276:5:276:19 | int[] a | a | B.java:276:11:276:18 | a | this |
| B.java:292:7:292:7 | b | Variable $@ may be null here because of $@ assignment. | B.java:287:5:287:44 | int[] b | b | B.java:287:11:287:43 | b | this |
| B.java:354:7:354:7 | x | Variable $@ may be null here because of $@ assignment. | B.java:349:5:349:20 | Object x | x | B.java:349:12:349:19 | x | this |
| B.java:362:7:362:8 | x2 | Variable $@ may be null here because of $@ assignment. | B.java:357:5:357:21 | Object x2 | x2 | B.java:357:12:357:20 | x2 | this |
| B.java:370:7:370:8 | x3 | Variable $@ may be null here because of $@ assignment. | B.java:365:5:365:21 | Object x3 | x3 | B.java:365:12:365:20 | x3 | this |
| C.java:9:44:9:45 | a2 | Variable $@ may be null here as suggested by $@ null guard. | C.java:6:5:6:23 | long[][] a2 | a2 | C.java:7:34:7:54 | ... != ... | this |
| C.java:9:44:9:45 | a2 | Variable $@ may be null here because of $@ assignment. | C.java:6:5:6:23 | long[][] a2 | a2 | C.java:6:14:6:22 | a2 | this |
| C.java:10:17:10:18 | a3 | Variable $@ may be null here as suggested by $@ null guard. | C.java:8:5:8:21 | long[] a3 | a3 | C.java:9:38:9:58 | ... != ... | this |