Java: Fix bug in qltest and query for immutable types.

This commit is contained in:
Anders Schack-Mulligen
2019-01-18 11:37:38 +01:00
parent 944c082a8d
commit 17b4276699
5 changed files with 33 additions and 13 deletions

View File

@@ -17,6 +17,11 @@ import DoubleCheckedLocking
predicate allFieldsFinal(Class c) { forex(Field f | c.inherits(f) | f.isFinal()) }
predicate immutableFieldType(Type t) {
allFieldsFinal(t) or
t instanceof ImmutableType
}
from IfStmt if1, IfStmt if2, SynchronizedStmt sync, Field f
where
doubleCheckedLocking(if1, if2, sync, f) and
@@ -24,7 +29,7 @@ where
not (
// Non-volatile double-checked locking is ok when the object is immutable and
// there is only a single non-synchronized field read.
allFieldsFinal(f.getType()) and
immutableFieldType(f.getType()) and
1 = strictcount(FieldAccess fa |
fa.getField() = f and
fa.getEnclosingCallable() = sync.getEnclosingCallable() and

View File

@@ -38,6 +38,5 @@ predicate doubleCheckedLocking(IfStmt if1, IfStmt if2, SynchronizedStmt sync, Fi
if1.getThen() = sync.getParent*() and
sync.getBlock() = if2.getParent*() and
if1.getCondition() = getANullCheck(f) and
if2.getCondition() = getANullCheck(f) and
not f.getType() instanceof ImmutableType
if2.getCondition() = getANullCheck(f)
}

View File

@@ -6,16 +6,31 @@ public class A {
}
}
private String s;
public String getString() {
if (s == null) {
private String s1;
public String getString1() {
if (s1 == null) {
synchronized(this) {
if (s == null) {
s = "string"; // OK, immutable
if (s1 == null) {
s1 = "string"; // BAD, immutable but read twice outside sync
}
}
}
return s;
return s1;
}
private String s2;
public String getString2() {
String x = s2;
if (x == null) {
synchronized(this) {
x = s2;
if (x == null) {
x = "string"; // OK, immutable and read once outside sync
s2 = x;
}
}
}
return x;
}
private B b1;

View File

@@ -1,2 +1,3 @@
| A.java:25:7:30:7 | stmt | Double-checked locking on the non-volatile field $@ is not thread-safe. | A.java:21:13:21:14 | b1 | b1 |
| A.java:86:7:91:7 | stmt | Double-checked locking on the non-volatile field $@ is not thread-safe. | A.java:83:26:83:27 | b5 | b5 |
| A.java:12:7:16:7 | stmt | Double-checked locking on the non-volatile field $@ is not thread-safe. | A.java:9:18:9:19 | s1 | s1 |
| A.java:40:7:45:7 | stmt | Double-checked locking on the non-volatile field $@ is not thread-safe. | A.java:36:13:36:14 | b1 | b1 |
| A.java:101:7:106:7 | stmt | Double-checked locking on the non-volatile field $@ is not thread-safe. | A.java:98:26:98:27 | b5 | b5 |

View File

@@ -1,2 +1,2 @@
| A.java:55:11:55:22 | ...=... | Potential race condition. This assignment to $@ is visible to other threads before the subsequent statements are executed. | A.java:50:22:50:23 | b3 | b3 |
| A.java:68:11:68:22 | ...=... | Potential race condition. This assignment to $@ is visible to other threads before the subsequent statements are executed. | A.java:63:22:63:23 | b4 | b4 |
| A.java:70:11:70:22 | ...=... | Potential race condition. This assignment to $@ is visible to other threads before the subsequent statements are executed. | A.java:65:22:65:23 | b3 | b3 |
| A.java:83:11:83:22 | ...=... | Potential race condition. This assignment to $@ is visible to other threads before the subsequent statements are executed. | A.java:78:22:78:23 | b4 | b4 |