java: understand more initializers

Whne a fiels is assigned a safe type in a constructor,
that field is not exposed.
This commit is contained in:
yoff
2025-11-25 15:46:18 +01:00
parent a65d385297
commit c6240e5a99
3 changed files with 16 additions and 8 deletions

View File

@@ -63,12 +63,23 @@ class ExposedField extends Field {
not this.getType() instanceof LockType and
// field is not thread-safe
not isThreadSafeType(this.getType()) and
not isThreadSafeType(this.getInitializer().getType()) and
not isThreadSafeType(initialValue(this).getType()) and
// the initializer guarantees thread safety
not isThreadSafeInitializer(this.getInitializer())
not isThreadSafeInitializer(initialValue(this))
}
}
/**
* Gets the initial value for the field `f`.
* This is either a static initializer or an assignment in a constructor.
*/
Expr initialValue(Field f) {
result = f.getInitializer()
or
result = f.getAnAssignedValue() and
result.getEnclosingCallable() = f.getDeclaringType().getAConstructor()
}
/**
* A field access that is exposed to potential data races.
* We require the field to be in a class that is annotated as `@ThreadSafe`.