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

@@ -1946,10 +1946,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) {
@@ -2161,34 +2157,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)
             }
         }
@@ -3284,10 +3254,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()