Skip to content

Commit fa7993f

Browse files
committed
Added docs
1 parent 2a3cb0b commit fa7993f

File tree

2 files changed

+26
-10
lines changed

2 files changed

+26
-10
lines changed

docs/SpeculativeFieldNonNullability.md

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -17,14 +17,15 @@ most of generated branches would be `NPE` branches, while useful paths could be
1717

1818
Beyond that, in many cases the `null` value of a field can't be generated using the public API
1919
of the class. This is particularly true for final fields, especially in system classes.
20-
Automatically generated tests assign `null` values to fields in questions using reflection,
20+
it is also often true for non-public fields from standard library and third-party libraries (even setters often do not
21+
allow `null` values). Automatically generated tests assign `null` values to fields in questions using reflection,
2122
but these tests may be uninformative as the corresponding `NPE` branches would never occur
2223
in the real code that limits itself to the public API.
2324

2425
## The solution
2526

2627
To discard irrelevant `NPE` branches, we can speculatively mark fields we as non-nullable even they
27-
do not have an explicit `@NotNull` annotation. In particular, we can use this approach to final
28+
do not have an explicit `@NotNull` annotation. In particular, we can use this approach to final and non-public
2829
fields of system classes, as they are usually correctly initialized and are not equal `null`.
2930

3031
At the same time, we can't always add the "not null" hard constraint for the field: it would break
@@ -38,18 +39,18 @@ no way to check whether the address corresponds to a final field, as the corresp
3839
of the global graph would refer to a local variable. The only place where we have the complete
3940
information about the field is this method.
4041

41-
We use the following approach. If the field is final and belongs to a system class,
42-
we mark it as a speculatively non-nullable in the memory
42+
We use the following approach. If the field belongs to a library class (according to `soot.SootClass.isLibraryClass`)
43+
and is final or non-public, we mark it as a speculatively non-nullable in the memory
4344
(see `org.utbot.engine.Memory.speculativelyNotNullAddresses`). During the NPE check
4445
we will add the `!isSpeculativelyNotNull(addr(field))` constraint
4546
to the `NPE` branch together with the usual `addr(field) == null` constraint.
4647

47-
For final fields, these two conditions can't be satisfied at the same time, as we speculatively
48-
mark final fields as non-nullable. As a result, the NPE branch would be discarded. If a field
49-
is not final, the condition is satisfiable, so the NPE branch would stay alive.
48+
For final/non-public fields, these two conditions can't be satisfied at the same time, as we speculatively
49+
mark such fields as non-nullable. As a result, the NPE branch would be discarded. If a field
50+
is public or not final, the condition is satisfiable, so the NPE branch would stay alive.
5051

51-
We limit this approach to the system classes only, because it is hard to speculatively assume
52-
something about non-nullability of final fields in the user code.
52+
We limit this approach to the library classes only, because it is hard to speculatively assume
53+
something about non-nullability of final/non-public fields in the user code.
5354

5455
The same approach can be extended for other cases where we want to speculatively consider some
5556
fields as non-nullable to prevent `NPE` branch generation.

utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2235,16 +2235,31 @@ class UtBotSymbolicEngine(
22352235
return createdField
22362236
}
22372237

2238+
/**
2239+
* Marks the [createdField] as speculatively not null if the [field] is considering as
2240+
* not producing [NullPointerException].
2241+
*
2242+
* @see [SootField.speculativelyCannotProduceNullPointerException], [markAsSpeculativelyNotNull]
2243+
*/
22382244
private fun checkAndMarkLibraryFieldSpeculativelyNotNull(field: SootField, createdField: SymbolicValue) {
22392245
if (maximizeCoverageUsingReflection || !field.declaringClass.isLibraryClass) {
22402246
return
22412247
}
22422248

2243-
if (field.isFinal || !field.isPublic) {
2249+
if (field.speculativelyCannotProduceNullPointerException()) {
22442250
markAsSpeculativelyNotNull(createdField.addr)
22452251
}
22462252
}
22472253

2254+
/**
2255+
* Checks whether accessing [this] field (with a method invocation or field access) speculatively can produce
2256+
* [NullPointerException] (according to its finality or accessibility).
2257+
*
2258+
* @see docs/SpeculativeFieldNonNullability.md for more information.
2259+
*/
2260+
@Suppress("KDocUnresolvedReference")
2261+
private fun SootField.speculativelyCannotProduceNullPointerException(): Boolean = isFinal || !isPublic
2262+
22482263
private fun createArray(pName: String, type: ArrayType): ArrayValue {
22492264
val addr = UtAddrExpression(mkBVConst(pName, UtIntSort))
22502265
return createArray(addr, type, useConcreteType = false)

0 commit comments

Comments
 (0)