Java: Add support for bitwise compound assignments in Guards.

This commit is contained in:
Anders Schack-Mulligen
2022-01-21 13:56:07 +01:00
parent b02f1c87a1
commit 41d294229d
3 changed files with 50 additions and 2 deletions

View File

@@ -23,6 +23,10 @@ predicate implies_v1(Guard g1, boolean b1, Guard g2, boolean b2) {
or
g1.(OrBitwiseExpr).getAnOperand() = g2 and b1 = false and b2 = false
or
g1.(AssignAndExpr).getSource() = g2 and b1 = true and b2 = true
or
g1.(AssignOrExpr).getSource() = g2 and b1 = false and b2 = false
or
g1.(AndLogicalExpr).getAnOperand() = g2 and b1 = true and b2 = true
or
g1.(OrLogicalExpr).getAnOperand() = g2 and b1 = false and b2 = false
@@ -61,11 +65,15 @@ predicate implies_v1(Guard g1, boolean b1, Guard g2, boolean b2) {
)
or
exists(BaseSsaUpdate vbool |
vbool.getDefiningExpr().(VariableAssign).getSource() = g2 or
vbool.getDefiningExpr().(AssignOp) = g2
|
vbool.getAUse() = g1 and
vbool.getDefiningExpr().(VariableAssign).getSource() = g2 and
(b1 = true or b1 = false) and
b2 = b1
)
or
g1.(AssignExpr).getSource() = g2 and b2 = b1 and b1 = [true, false]
}
/**
@@ -79,8 +87,10 @@ predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
implies_v1(g1, b1, g2, b2)
or
exists(SsaExplicitUpdate vbool |
vbool.getDefiningExpr().(VariableAssign).getSource() = g2 or
vbool.getDefiningExpr().(AssignOp) = g2
|
vbool.getAUse() = g1 and
vbool.getDefiningExpr().(VariableAssign).getSource() = g2 and
(b1 = true or b1 = false) and
b2 = b1
)

View File

@@ -371,4 +371,41 @@ public class B {
}
}
public void bitwise(Object x, boolean b) {
boolean notnull = x != null;
boolean g1 = notnull;
g1 &= b;
if (g1) {
x.hashCode(); // OK
}
boolean g2 = b;
g2 &= notnull;
if (g2) {
x.hashCode(); // OK
}
boolean g3 = !notnull;
g3 |= b;
if (!g3) {
x.hashCode(); // OK
}
boolean g4 = b;
g4 |= !notnull;
if (!g4) {
x.hashCode(); // OK
}
boolean g5 = g1 = b & notnull;
if (g5) {
x.hashCode(); // OK
}
g5 |= b;
if (g5) {
x.hashCode(); // NPE
}
}
}

View File

@@ -17,6 +17,7 @@
| 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:408:7:408:7 | x | Variable $@ may be null here as suggested by $@ null guard. | B.java:374:23:374:30 | x | x | B.java:375:23:375:31 | ... != ... | 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 |