Code review fixes

 * Moved the design description from a comment to a separate document `docs/SpeculativeFieldNonNullability.md` * Extracted intermediate expressions in `nullPointerExceptionCheck` * Removed obsolete temporary comment in `Value.resolve` * Replaced package import to class imports to conform the coding style * Replaced negated call to `isApplicationClass` with `isLibraryClass`

Author: dtim

docs/SpeculativeFieldNonNullability.md

@@ -0,0 +1,55 @@
+# Speculative field non-nullability assumptions
+
+## The problem
+
+When a field is used as a base for a dot call (i.e., a method call or a field access),
+the symbolic engine creates a branch corresponding to the potential `NullPointerException`
+that can occur if the value of the field is `null`. For this path, the engine generates
+the hard constraint `addr(field) == null`.
+
+If the field is marked as `@NotNull`, a hard constraint `addr(field) != null` is generated
+for it. If both constraints have been generated simultaneously, the `NPE` branch is discarded
+as the constraint set is unsatisfiable. 
+
+If a field does not have `@NotNull` annotation, the `NPE` branch will be kept. This behavior
+is desirable, as it increases the coverage, but it has a downside. It is possible that
+most of generated branches would be `NPE` branches, while useful paths could be lost due to timeout.
+
+Beyond that, in many cases the `null` value of a field can't be generated using the public API
+of the class. This is particularly true for final fields, especially in system classes.
+Automatically generated tests assign `null` values to fields in questions using reflection,
+but these tests may be uninformative as the corresponding `NPE` branches would never occur
+in the real code that limits itself to the public API.
+
+## The solution
+
+To discard irrelevant `NPE` branches, we can speculatively mark fields we as non-nullable even they
+do not have an explicit `@NotNull` annotation. In particular, we can use this approach to final
+fields of system classes, as they are usually correctly initialized and are not equal `null`.
+
+At the same time, we can't always add the "not null" hard constraint for the field: it would break
+some special cases like `Optional<T>` class, which uses the `null` value of its final field
+as a marker of an empty value.
+
+The engine checks for NPE and creates an NPE branch every time the address is used
+as a base of a dot call (i.e., a method call or a field access);
+see `UtBotSymbolicEngine.nullPointerExceptionCheck`). The problem is what at that moment, we would have
+no way to check whether the address corresponds to a final field, as the corresponding node
+of the global graph would refer to a local variable. The only place where we have the complete
+information about the field is this method.
+
+We use the following approach. If the field is final and belongs to a system class,
+we mark it as a speculatively non-nullable in the memory
+(see `org.utbot.engine.Memory.speculativelyNotNullAddresses`). During the NPE check
+we will add the `!isSpeculativelyNotNull(addr(field))` constraint
+to the `NPE` branch together with the usual `addr(field) == null` constraint.
+
+For final fields, these two conditions can't be satisfied at the same time, as we speculatively
+mark final fields as non-nullable. As a result, the NPE branch would be discarded. If a field
+is not final, the condition is satisfiable, so the NPE branch would stay alive.
+
+We limit this approach to the system classes only, because it is hard to speculatively assume
+something about non-nullability of final fields in the user code.
+
+The same approach can be extended for other cases where we want to speculatively consider some
+fields as non-nullable to prevent `NPE` branch generation.

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

@@ -141,7 +141,8 @@ data class Memory( // TODO: split purely symbolic memory and information about s
 
  /**
  * Storage for addresses that we speculatively consider non-nullable (e.g., final fields of system classes).
- * See [org.utbot.engine.UtBotSymbolicEngine.createFieldOrMock] for details.
+ * See [org.utbot.engine.UtBotSymbolicEngine.createFieldOrMock] for usage,
+ * and [docs/SpeculativeFieldNonNullability.md] for details.
  */
  private val speculativelyNotNullAddresses: UtArrayExpressionBase = UtConstArrayExpression(
  UtFalse,

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

@@ -1938,10 +1938,6 @@ class UtBotSymbolicEngine(
  is JInstanceFieldRef -> {
  val instance = (base.resolve() as ObjectValue)
  recordInstanceFieldRead(instance.addr, field)
-
- // We know that [base] is not null as we are accessing its field (dot access).
- // At the same time, we don't want to check for NPE if [base] is a final field
- // (or if it is a non-nullable field).
  nullPointerExceptionCheck(instance.addr)
 
  val objectType = if (instance.concrete?.value is BaseOverriddenWrapper) {
@@ -2153,34 +2149,8 @@ class UtBotSymbolicEngine(
  queuedSymbolicStateUpdates += mkNot(mkEq(createdField.addr, nullObjectAddr)).asHardConstraint()
  }
 
- // We suppose that accessing final fields in system classes can't produce NullPointerException
- // because they are properly initialized in corresponding constructors. It is therefore
- // desirable to avoid the generation of redundant test cases for NPE branches.
- //
- // At the same time, we can't always add the "not null" hard constraint for the field: it would break
- // some special cases like `Optional<T>` class, which uses the null value of its final field
- // as a marker of an empty value.
- //
- // The engine checks for NPE and creates an NPE branch every time the address is used
- // as a base of a dot call (i.e., a method call or a field access);
- // see [UtBotSymbolicEngine.nullPointerExceptionCheck]). The problem is what at that moment, we would have
- // no way to check whether the address corresponds to a final field, as the corresponding node
- // of the global graph would refer to a local variable. The only place where we have the complete
- // information about the field is this method.
- //
- // We use the following approach. If the field is final and belongs to a system class,
- // we mark it as a speculatively non-nullable in the memory. During the NPE check
- // we will add two constraints to the NPE branch: "address has not been speculatively marked
- // as non-nullable", and "address is null".
- //
- // For final fields, this condition can't be satisfied, as we speculatively mark final fields
- // as non-nullable here. As a result, the NPE branch would be discarded. If a field is not final,
- // the condition is satisfiable, so the NPE branch would stay alive.
- //
- // We limit this approach to the system classes only, because it is hard to speculatively assume
- // something about non-nullability of final fields in the user code.
-
- if (field.isFinal && !field.declaringClass.isApplicationClass && !checkNpeForFinalFields) {
+ // See docs/SpeculativeFieldNonNullability.md for details
+ if (field.isFinal && field.declaringClass.isLibraryClass && !checkNpeForFinalFields) {
  markAsSpeculativelyNotNull(createdField.addr)
  }
  }
@@ -3274,10 +3244,11 @@ class UtBotSymbolicEngine(
  private fun nullPointerExceptionCheck(addr: UtAddrExpression) {
  val canBeNull = addrEq(addr, nullObjectAddr)
  val canNotBeNull = mkNot(canBeNull)
- val notFinalAndNull = mkAnd(mkEq(memory.isSpeculativelyNotNull(addr), mkFalse()), canBeNull)
+ val notMarked = mkEq(memory.isSpeculativelyNotNull(addr), mkFalse())
+ val notMarkedAndNull = mkAnd(notMarked, canBeNull)
 
  if (environment.method.checkForNPE(environment.state.executionStack.size)) {
- implicitlyThrowException(NullPointerException(), setOf(notFinalAndNull))
+ implicitlyThrowException(NullPointerException(), setOf(notMarkedAndNull))
  }
 
  queuedSymbolicStateUpdates += canNotBeNull.asHardConstraint()