Java: Switch to the shared Guards library.

This commit is contained in:
Anders Schack-Mulligen
2025-05-15 16:23:21 +02:00
parent cc13193cb6
commit 5c0dcd980d
19 changed files with 488 additions and 788 deletions

View File

@@ -26,7 +26,7 @@ public class Guards {
}
int sz = a != null ? a.length : 0;
for (int i = 0; i < sz; i++) {
chk(); // $ guarded='a != null:true' guarded='i < sz:true'
chk(); // $ guarded='a != null:true' guarded='i < sz:true' guarded='sz:not 0' guarded='...?...:...:not 0' guarded='a.length:not 0' guarded='a:not null'
int e = a[i];
if (e > 2) break;
}
@@ -36,26 +36,26 @@ public class Guards {
s = "bar";
switch (s) {
case "bar":
chk(); // $ guarded='s:match "bar"'
chk(); // $ guarded='s:match "bar"' guarded='s:bar'
break;
case "foo":
chk(); // $ guarded='s:match "foo"' guarded=g(3):false
chk(); // $ guarded='s:match "foo"' guarded='s:foo' guarded=g(3):false
break;
default:
chk(); // $ guarded='s:non-match "bar"' guarded='s:non-match "foo"' guarded='s:match default' guarded=g(3):false
chk(); // $ guarded='s:non-match "bar"' guarded='s:non-match "foo"' guarded='s:not bar' guarded='s:not foo' guarded='s:match default' guarded=g(3):false
break;
}
Object o = g(4) ? null : s;
if (o instanceof String) {
chk(); // $ guarded=...instanceof...:true guarded=g(4):false
chk(); // $ guarded=...instanceof...:true guarded='o:not null' guarded='...?...:...:not null' guarded=g(4):false guarded='s:not null'
}
}
void t2() {
checkTrue(g(1), "A");
checkFalse(g(2), "B");
chk(); // $ guarded=checkTrue(A):true guarded=g(1):true guarded=checkFalse(B):false guarded=g(2):false
chk(); // $ guarded='checkTrue(...):no exception' guarded=g(1):true guarded='checkFalse(...):no exception' guarded=g(2):false
}
void t3() {
@@ -86,23 +86,23 @@ public class Guards {
if (g("Alt2")) x = Val.E2;
if (g(3)) x = Val.E3; // unique value
if (x == null)
chk(); // $ guarded='x == null:true' guarded=g(3):false
chk(); // $ guarded='x == null:true' guarded='x:null' guarded=g(1):false guarded=g(2):false guarded=g(Alt2):false guarded=g(3):false
switch (x) {
case E1:
chk(); // $ guarded='x:match E1' guarded=g(1):true guarded=g(3):false
chk(); // $ guarded='x:match E1' guarded='x:E1' guarded=g(1):true guarded=g(2):false guarded=g(Alt2):false guarded=g(3):false
break;
case E2:
chk(); // $ guarded='x:match E2' guarded=g(3):false
chk(); // $ guarded='x:match E2' guarded='x:E2' guarded=g(3):false
break;
case E3:
chk(); // $ guarded='x:match E3' guarded=g(3):true
chk(); // $ guarded='x:match E3' guarded='x:E3' guarded=g(3):true
break;
}
Object o = g(4) ? new Object() : null;
if (o == null) {
chk(); // $ guarded='o == null:true' guarded=g(4):false
chk(); // $ guarded='o == null:true' guarded='o:null' guarded='...?...:...:null' guarded=g(4):false
} else {
chk(); // $ guarded='o == null:false' guarded=g(4):true
chk(); // $ guarded='o == null:false' guarded='o:not null' guarded='...?...:...:not null' guarded=g(4):true
}
}
@@ -112,7 +112,7 @@ public class Guards {
base = "/user";
}
if (base.equals("/"))
chk(); // $ guarded=equals(/):true guarded='base == null:false'
chk(); // $ guarded=equals(/):true guarded='base:/' guarded='base:not null' guarded='base == null:false' guarded='foo:/' guarded='foo:not null'
}
void t6() {
@@ -122,9 +122,9 @@ public class Guards {
if (g(2)) { }
}
if (o != null) {
chk(); // $ guarded='o != null:true'
chk(); // $ guarded='o != null:true' guarded='o:not null' guarded=g(1):true
} else {
chk(); // $ guarded='o != null:false' guarded=g(1):false
chk(); // $ guarded='o != null:false' guarded='o:null' guarded=g(1):false
}
}

View File

@@ -8,19 +8,30 @@
| Guards.java:25:7:25:11 | chk(...) | b:false |
| Guards.java:25:7:25:11 | chk(...) | g(1):true |
| Guards.java:25:7:25:11 | chk(...) | g(2):false |
| Guards.java:29:7:29:11 | chk(...) | '...?...:...:not 0' |
| Guards.java:29:7:29:11 | chk(...) | 'a != null:true' |
| Guards.java:29:7:29:11 | chk(...) | 'a.length:not 0' |
| Guards.java:29:7:29:11 | chk(...) | 'a:not null' |
| Guards.java:29:7:29:11 | chk(...) | 'i < sz:true' |
| Guards.java:29:7:29:11 | chk(...) | 'sz:not 0' |
| Guards.java:39:9:39:13 | chk(...) | 's:bar' |
| Guards.java:39:9:39:13 | chk(...) | 's:match "bar"' |
| Guards.java:42:9:42:13 | chk(...) | 's:foo' |
| Guards.java:42:9:42:13 | chk(...) | 's:match "foo"' |
| Guards.java:42:9:42:13 | chk(...) | g(3):false |
| Guards.java:45:9:45:13 | chk(...) | 's:match default' |
| Guards.java:45:9:45:13 | chk(...) | 's:non-match "bar"' |
| Guards.java:45:9:45:13 | chk(...) | 's:non-match "foo"' |
| Guards.java:45:9:45:13 | chk(...) | 's:not bar' |
| Guards.java:45:9:45:13 | chk(...) | 's:not foo' |
| Guards.java:45:9:45:13 | chk(...) | g(3):false |
| Guards.java:51:7:51:11 | chk(...) | '...?...:...:not null' |
| Guards.java:51:7:51:11 | chk(...) | 'o:not null' |
| Guards.java:51:7:51:11 | chk(...) | 's:not null' |
| Guards.java:51:7:51:11 | chk(...) | ...instanceof...:true |
| Guards.java:51:7:51:11 | chk(...) | g(4):false |
| Guards.java:58:5:58:9 | chk(...) | checkFalse(B):false |
| Guards.java:58:5:58:9 | chk(...) | checkTrue(A):true |
| Guards.java:58:5:58:9 | chk(...) | 'checkFalse(...):no exception' |
| Guards.java:58:5:58:9 | chk(...) | 'checkTrue(...):no exception' |
| Guards.java:58:5:58:9 | chk(...) | g(1):true |
| Guards.java:58:5:58:9 | chk(...) | g(2):false |
| Guards.java:64:7:64:11 | chk(...) | 'g(...) && ... \|\| ...:true' |
@@ -37,22 +48,42 @@
| Guards.java:72:7:72:11 | chk(...) | g(4):false |
| Guards.java:72:7:72:11 | chk(...) | g(5):true |
| Guards.java:89:7:89:11 | chk(...) | 'x == null:true' |
| Guards.java:89:7:89:11 | chk(...) | 'x:null' |
| Guards.java:89:7:89:11 | chk(...) | g(1):false |
| Guards.java:89:7:89:11 | chk(...) | g(2):false |
| Guards.java:89:7:89:11 | chk(...) | g(3):false |
| Guards.java:89:7:89:11 | chk(...) | g(Alt2):false |
| Guards.java:92:9:92:13 | chk(...) | 'x:E1' |
| Guards.java:92:9:92:13 | chk(...) | 'x:match E1' |
| Guards.java:92:9:92:13 | chk(...) | g(1):true |
| Guards.java:92:9:92:13 | chk(...) | g(2):false |
| Guards.java:92:9:92:13 | chk(...) | g(3):false |
| Guards.java:92:9:92:13 | chk(...) | g(Alt2):false |
| Guards.java:95:9:95:13 | chk(...) | 'x:E2' |
| Guards.java:95:9:95:13 | chk(...) | 'x:match E2' |
| Guards.java:95:9:95:13 | chk(...) | g(3):false |
| Guards.java:98:9:98:13 | chk(...) | 'x:E3' |
| Guards.java:98:9:98:13 | chk(...) | 'x:match E3' |
| Guards.java:98:9:98:13 | chk(...) | g(3):true |
| Guards.java:103:7:103:11 | chk(...) | '...?...:...:null' |
| Guards.java:103:7:103:11 | chk(...) | 'o == null:true' |
| Guards.java:103:7:103:11 | chk(...) | 'o:null' |
| Guards.java:103:7:103:11 | chk(...) | g(4):false |
| Guards.java:105:7:105:11 | chk(...) | '...?...:...:not null' |
| Guards.java:105:7:105:11 | chk(...) | 'o == null:false' |
| Guards.java:105:7:105:11 | chk(...) | 'o:not null' |
| Guards.java:105:7:105:11 | chk(...) | g(4):true |
| Guards.java:115:7:115:11 | chk(...) | 'base == null:false' |
| Guards.java:115:7:115:11 | chk(...) | 'base:/' |
| Guards.java:115:7:115:11 | chk(...) | 'base:not null' |
| Guards.java:115:7:115:11 | chk(...) | 'foo:/' |
| Guards.java:115:7:115:11 | chk(...) | 'foo:not null' |
| Guards.java:115:7:115:11 | chk(...) | equals(/):true |
| Guards.java:125:7:125:11 | chk(...) | 'o != null:true' |
| Guards.java:125:7:125:11 | chk(...) | 'o:not null' |
| Guards.java:125:7:125:11 | chk(...) | g(1):true |
| Guards.java:127:7:127:11 | chk(...) | 'o != null:false' |
| Guards.java:127:7:127:11 | chk(...) | 'o:null' |
| Guards.java:127:7:127:11 | chk(...) | g(1):false |
| Guards.java:139:9:139:13 | chk(...) | 'i < a.length:true' |
| Guards.java:139:9:139:13 | chk(...) | found:true |

View File

@@ -39,4 +39,13 @@ query predicate guarded(MethodCall mc, string guard) {
not exists(ppGuard(g, branch)) and
guard = g.toString() + ":" + branch
)
or
mc.getMethod().hasName("chk") and
exists(Guard g, BasicBlock bb, GuardValue val |
g.valueControls(bb, val) and
not exists(val.asBooleanValue()) and
mc.getBasicBlock() = bb
|
guard = "'" + g.toString() + ":" + val + "'"
)
}

View File

@@ -51,13 +51,5 @@ hasBranchEdge
| Test.java:12:7:12:17 | case ... | Test.java:9:13:9:13 | s | Test.java:12:12:12:14 | "d" | true | false | Test.java:13:7:13:16 | default |
| Test.java:12:7:12:17 | case ... | Test.java:9:13:9:13 | s | Test.java:12:12:12:14 | "d" | true | true | Test.java:12:7:12:17 | case ... |
| Test.java:17:26:17:33 | ... == ... | Test.java:17:26:17:28 | len | Test.java:17:33:17:33 | 4 | true | true | Test.java:17:38:17:40 | { ... } |
| Test.java:18:7:18:17 | case ... | Test.java:16:13:16:13 | s | Test.java:18:12:18:14 | "e" | true | false | Test.java:19:7:19:16 | default |
| Test.java:18:7:18:17 | case ... | Test.java:16:13:16:13 | s | Test.java:18:12:18:14 | "e" | true | true | Test.java:18:7:18:17 | case ... |
| Test.java:22:7:22:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:22:12:22:14 | "f" | true | false | Test.java:25:7:25:16 | default |
| Test.java:22:7:22:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:22:12:22:14 | "f" | true | true | Test.java:22:7:22:17 | case ... |
| Test.java:23:27:23:34 | ... == ... | Test.java:23:27:23:29 | len | Test.java:23:34:23:34 | 4 | true | true | Test.java:23:39:23:41 | { ... } |
| Test.java:24:7:24:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:24:12:24:14 | "g" | true | false | Test.java:25:7:25:16 | default |
| Test.java:24:7:24:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:24:12:24:14 | "g" | true | true | Test.java:24:7:24:17 | case ... |
| Test.java:28:7:28:15 | case ... | Test.java:27:13:27:13 | s | Test.java:28:12:28:14 | "h" | true | false | Test.java:33:7:33:14 | default |
| Test.java:28:7:28:15 | case ... | Test.java:27:13:27:13 | s | Test.java:28:12:28:14 | "h" | true | true | Test.java:28:7:28:15 | case ... |
| Test.java:30:7:30:15 | case ... | Test.java:27:13:27:13 | s | Test.java:30:12:30:14 | "i" | true | false | Test.java:33:7:33:14 | default |

View File

@@ -1,8 +1,8 @@
import java
import semmle.code.java.controlflow.Guards
query predicate hasBranchEdge(Guard g, BasicBlock bb1, BasicBlock bb2, boolean branch) {
g.hasBranchEdge(bb1, bb2, branch)
query predicate hasBranchEdge(Guard g, BasicBlock bb1, BasicBlock bb2, GuardValue branch) {
g.hasValueBranchEdge(bb1, bb2, branch)
}
from Guard g, BasicBlock bb, boolean branch, Expr e1, Expr e2, boolean pol

View File

@@ -60,7 +60,7 @@ public class C {
arrLen = arr == null ? 0 : arr.length;
}
if (arrLen > 0) {
arr[0] = 0; // NPE - false positive
arr[0] = 0; // OK
}
}

View File

@@ -24,7 +24,6 @@
| C.java:10:17:10:18 | a3 | Variable $@ may be null at this access because of $@ assignment. | C.java:8:5:8:21 | long[] a3 | a3 | C.java:8:12:8:20 | a3 | this |
| C.java:21:7:21:8 | s1 | Variable $@ may be null at this access because of $@ assignment. | C.java:14:5:14:30 | String s1 | s1 | C.java:17:7:17:24 | ...=... | this |
| C.java:51:7:51:11 | slice | Variable $@ may be null at this access because of $@ assignment. | C.java:43:5:43:30 | List<String> slice | slice | C.java:43:18:43:29 | slice | this |
| C.java:63:7:63:9 | arr | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:57:35:57:43 | arr | arr | C.java:60:16:60:26 | ... == ... | this |
| C.java:100:7:100:10 | arr2 | Variable $@ may be null at this access because of $@ assignment. | C.java:95:5:95:22 | int[] arr2 | arr2 | C.java:95:11:95:21 | arr2 | this |
| C.java:110:25:110:27 | obj | Variable $@ may be null at this access because of $@ assignment. | C.java:106:5:106:30 | Object obj | obj | C.java:118:13:118:22 | ...=... | this |
| C.java:137:7:137:10 | obj2 | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:131:5:131:23 | Object obj2 | obj2 | C.java:132:9:132:20 | ... != ... | this |