Test generation for Optional<T> in the plugin (#226)

Added a check for overridden classes in `shouldMock` to avoid
access to engine classes that are not available in the plugin.

Implemented more accurate speculative marking of final fields
as not null to avoid losing paths involving `Optional.empty()`,
to enable NPE checks for final fields in user code, and to avoid
generating non-informative NPE tests for final fields in system
classes.

UtSettings.checkNpeForFinalFields is now set default (false)
in `AbstractTestCaseGEneratorTest` and `SummaryTestCaseGeneratorTest`.

Author: dtim

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

@@ -18,7 +18,6 @@ import org.utbot.engine.pc.UtSeqSort
 import org.utbot.engine.pc.UtShortSort
 import org.utbot.engine.pc.UtSolverStatusKind
 import org.utbot.engine.pc.UtSolverStatusSAT
-import org.utbot.engine.symbolic.Assumption
 import org.utbot.engine.pc.UtSort
 import org.utbot.engine.pc.mkArrayWithConst
 import org.utbot.engine.pc.mkBool
@@ -31,7 +30,6 @@ import org.utbot.engine.pc.mkLong
 import org.utbot.engine.pc.mkShort
 import org.utbot.engine.pc.mkString
 import org.utbot.engine.pc.toSort
-import org.utbot.framework.UtSettings.checkNpeForFinalFields
 import org.utbot.framework.UtSettings.checkNpeInNestedMethods
 import org.utbot.framework.UtSettings.checkNpeInNestedNotPrivateMethods
 import org.utbot.framework.plugin.api.FieldId
@@ -384,11 +382,7 @@ fun arrayTypeUpdate(addr: UtAddrExpression, type: ArrayType) =
 fun SootField.shouldBeNotNull(): Boolean {
     require(type is RefLikeType)
 
-    if (hasNotNullAnnotation()) return true
-
-    if (!checkNpeForFinalFields && isFinal) return true
-
-    return false
+    return hasNotNullAnnotation()
 }
 
 /**

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

@@ -137,7 +137,16 @@ data class Memory( // TODO: split purely symbolic memory and information about s
         UtFalse,
         UtArraySort(UtAddrSort, UtBoolSort)
     ),
-    private val instanceFieldReadOperations: PersistentSet<InstanceFieldReadOperation> = persistentHashSetOf()
+    private val instanceFieldReadOperations: PersistentSet<InstanceFieldReadOperation> = persistentHashSetOf(),
+
+    /**
+     * Storage for addresses that we speculatively consider non-nullable (e.g., final fields of system classes).
+     * See [org.utbot.engine.UtBotSymbolicEngine.createFieldOrMock] for details.
+     */
+    private val speculativelyNotNullAddresses: UtArrayExpressionBase = UtConstArrayExpression(
+        UtFalse,
+        UtArraySort(UtAddrSort, UtBoolSort)
+    )
 ) {
     val chunkIds: Set<ChunkId>
         get() = initial.keys
@@ -167,6 +176,11 @@ data class Memory( // TODO: split purely symbolic memory and information about s
      */
     fun isTouched(addr: UtAddrExpression): UtArraySelectExpression = touchedAddresses.select(addr)
 
+    /**
+     * Returns symbolic information about whether [addr] corresponds to a final field known to be not null.
+     */
+    fun isSpeculativelyNotNull(addr: UtAddrExpression): UtArraySelectExpression = speculativelyNotNullAddresses.select(addr)
+
     /**
      * @return ImmutableCollection of the initial values for all the arrays we touched during the execution
      */
@@ -260,6 +274,10 @@ data class Memory( // TODO: split purely symbolic memory and information about s
             acc.store(addr, UtTrue)
         }
 
+        val updSpeculativelyNotNullAddresses = update.speculativelyNotNullAddresses.fold(speculativelyNotNullAddresses) { acc, addr ->
+            acc.store(addr, UtTrue)
+        }
+
         return this.copy(
             initial = updInitial,
             current = updCurrent,
@@ -275,7 +293,8 @@ data class Memory( // TODO: split purely symbolic memory and information about s
             updates = updates + update,
             visitedValues = updVisitedValues,
             touchedAddresses = updTouchedAddresses,
-            instanceFieldReadOperations = instanceFieldReadOperations.addAll(update.instanceFieldReads)
+            instanceFieldReadOperations = instanceFieldReadOperations.addAll(update.instanceFieldReads),
+            speculativelyNotNullAddresses = updSpeculativelyNotNullAddresses
         )
     }
 
@@ -955,7 +974,8 @@ data class MemoryUpdate(
     val visitedValues: PersistentList<UtAddrExpression> = persistentListOf(),
     val touchedAddresses: PersistentList<UtAddrExpression> = persistentListOf(),
     val classIdToClearStatics: ClassId? = null,
-    val instanceFieldReads: PersistentSet<InstanceFieldReadOperation> = persistentHashSetOf()
+    val instanceFieldReads: PersistentSet<InstanceFieldReadOperation> = persistentHashSetOf(),
+    val speculativelyNotNullAddresses: PersistentList<UtAddrExpression> = persistentListOf()
 ) {
     operator fun plus(other: MemoryUpdate) =
         this.copy(
@@ -972,7 +992,8 @@ data class MemoryUpdate(
             visitedValues = visitedValues.addAll(other.visitedValues),
             touchedAddresses = touchedAddresses.addAll(other.touchedAddresses),
             classIdToClearStatics = other.classIdToClearStatics,
-            instanceFieldReads = instanceFieldReads.addAll(other.instanceFieldReads)
+            instanceFieldReads = instanceFieldReads.addAll(other.instanceFieldReads),
+            speculativelyNotNullAddresses = speculativelyNotNullAddresses.addAll(other.speculativelyNotNullAddresses),
         )
 }
 

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

@@ -184,9 +184,13 @@ class Mocker(
         if (mockAlways(type)) return true // always mock randoms and loggers
         if (mockInfo is UtFieldMockInfo) {
             val declaringClass = mockInfo.fieldId.declaringClass
+            val sootDeclaringClass = Scene.v().getSootClass(declaringClass.name)
 
-            if (Scene.v().getSootClass(declaringClass.name).isArtificialEntity) {
-                return false // see BaseStreamExample::minExample for an example; cannot load java class for such class
+            if (sootDeclaringClass.isArtificialEntity || sootDeclaringClass.isOverridden) {
+                // Cannot load Java class for artificial classes, see BaseStreamExample::minExample for an example.
+                // Wrapper classes that override system classes ([org.utbot.engine.overrides] package) are also
+                // unavailable to the [UtContext] class loader used by the plugin.
+                return false
             }
 
             return when {

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

@@ -34,55 +34,7 @@ import org.utbot.engine.MockStrategy.NO_MOCKS
 import org.utbot.engine.overrides.UtArrayMock
 import org.utbot.engine.overrides.UtLogicMock
 import org.utbot.engine.overrides.UtOverrideMock
-import org.utbot.engine.pc.NotBoolExpression
-import org.utbot.engine.pc.UtAddNoOverflowExpression
-import org.utbot.engine.pc.UtAddrExpression
-import org.utbot.engine.pc.UtAndBoolExpression
-import org.utbot.engine.pc.UtArrayApplyForAll
-import org.utbot.engine.pc.UtArrayExpressionBase
-import org.utbot.engine.pc.UtArraySelectExpression
-import org.utbot.engine.pc.UtArraySetRange
-import org.utbot.engine.pc.UtArraySort
-import org.utbot.engine.pc.UtBoolExpression
-import org.utbot.engine.pc.UtBoolOpExpression
-import org.utbot.engine.pc.UtBvConst
-import org.utbot.engine.pc.UtBvLiteral
-import org.utbot.engine.pc.UtByteSort
-import org.utbot.engine.pc.UtCastExpression
-import org.utbot.engine.pc.UtCharSort
-import org.utbot.engine.pc.UtContextInitializer
-import org.utbot.engine.pc.UtExpression
-import org.utbot.engine.pc.UtFalse
-import org.utbot.engine.pc.UtInstanceOfExpression
-import org.utbot.engine.pc.UtIntSort
-import org.utbot.engine.pc.UtIsExpression
-import org.utbot.engine.pc.UtIteExpression
-import org.utbot.engine.pc.UtLongSort
-import org.utbot.engine.pc.UtMkTermArrayExpression
-import org.utbot.engine.pc.UtNegExpression
-import org.utbot.engine.pc.UtOrBoolExpression
-import org.utbot.engine.pc.UtPrimitiveSort
-import org.utbot.engine.pc.UtShortSort
-import org.utbot.engine.pc.UtSolver
-import org.utbot.engine.pc.UtSolverStatusSAT
-import org.utbot.engine.pc.UtSubNoOverflowExpression
-import org.utbot.engine.pc.UtTrue
-import org.utbot.engine.pc.addrEq
-import org.utbot.engine.pc.align
-import org.utbot.engine.pc.cast
-import org.utbot.engine.pc.findTheMostNestedAddr
-import org.utbot.engine.pc.isInteger
-import org.utbot.engine.pc.mkAnd
-import org.utbot.engine.pc.mkBVConst
-import org.utbot.engine.pc.mkBoolConst
-import org.utbot.engine.pc.mkChar
-import org.utbot.engine.pc.mkEq
-import org.utbot.engine.pc.mkFpConst
-import org.utbot.engine.pc.mkInt
-import org.utbot.engine.pc.mkNot
-import org.utbot.engine.pc.mkOr
-import org.utbot.engine.pc.select
-import org.utbot.engine.pc.store
+import org.utbot.engine.pc.*
 import org.utbot.engine.selectors.PathSelector
 import org.utbot.engine.selectors.StrategyOption
 import org.utbot.engine.selectors.coveredNewSelector
@@ -115,6 +67,7 @@ import org.utbot.engine.util.statics.concrete.makeEnumStaticFieldsUpdates
 import org.utbot.engine.util.statics.concrete.makeSymbolicValuesFromEnumConcreteValues
 import org.utbot.framework.PathSelectorType
 import org.utbot.framework.UtSettings
+import org.utbot.framework.UtSettings.checkNpeForFinalFields
 import org.utbot.framework.UtSettings.checkSolverTimeoutMillis
 import org.utbot.framework.UtSettings.enableFeatureProcess
 import org.utbot.framework.UtSettings.pathSelectorStepsLimit
@@ -1993,6 +1946,10 @@ 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) {
@@ -2199,8 +2156,41 @@ class UtBotSymbolicEngine(
         val chunkId = hierarchy.chunkIdForField(objectType, field)
         val createdField = createField(objectType, addr, field.type, chunkId, mockInfoGenerator)
 
-        if (field.type is RefLikeType && field.shouldBeNotNull()) {
-            queuedSymbolicStateUpdates += mkNot(mkEq(createdField.addr, nullObjectAddr)).asHardConstraint()
+        if (field.type is RefLikeType) {
+            if (field.shouldBeNotNull()) {
+                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) {
+                markAsSpeculativelyNotNull(createdField.addr)
+            }
         }
 
         return createdField
@@ -2370,6 +2360,10 @@ class UtBotSymbolicEngine(
         queuedSymbolicStateUpdates += MemoryUpdate(touchedAddresses = persistentListOf(addr))
     }
 
+    private fun markAsSpeculativelyNotNull(addr: UtAddrExpression) {
+        queuedSymbolicStateUpdates += MemoryUpdate(speculativelyNotNullAddresses = persistentListOf(addr))
+    }
+
     /**
      * Add a memory update to reflect that a field was read.
      *
@@ -3290,9 +3284,10 @@ 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)
 
         if (environment.method.checkForNPE(environment.state.executionStack.size)) {
-            implicitlyThrowException(NullPointerException(), setOf(canBeNull))
+            implicitlyThrowException(NullPointerException(), setOf(notFinalAndNull))
         }
 
         queuedSymbolicStateUpdates += canNotBeNull.asHardConstraint()

utbot-framework/src/test/kotlin/org/utbot/examples/AbstractTestCaseGeneratorTest.kt

@@ -88,7 +88,6 @@ abstract class AbstractTestCaseGeneratorTest(
         UtSettings.checkSolverTimeoutMillis = 0
         UtSettings.checkNpeInNestedMethods = true
         UtSettings.checkNpeInNestedNotPrivateMethods = true
-        UtSettings.checkNpeForFinalFields = true
         UtSettings.substituteStaticsWithSymbolicVariable = true
         UtSettings.useAssembleModelGenerator = true
         UtSettings.saveRemainingStatesForConcreteExecution = false

utbot-framework/src/test/kotlin/org/utbot/examples/collections/OptionalsTest.kt

@@ -482,4 +482,14 @@ class OptionalsTest : AbstractTestCaseGeneratorTest(
             coverage = DoNotCalculate
         )
     }
+
+    @Test
+    fun testOptionalOfPositive() {
+        check(
+            Optionals::optionalOfPositive,
+            eq(2),
+            { value, result -> value > 0 && result != null && result.isPresent && result.get() == value },
+            { value, result -> value <= 0 && result != null && !result.isPresent }
+        )
+    }
 }

utbot-sample/src/main/java/org/utbot/examples/collections/Optionals.java

@@ -314,4 +314,8 @@ public boolean equalOptionalsDouble(OptionalDouble left, OptionalDouble right) {
             return false;
         }
     }
+
+    public Optional<Integer> optionalOfPositive(int value) {
+        return value > 0 ? Optional.of(value) : Optional.empty();
+    }
 }

utbot-summary-tests/src/test/kotlin/examples/SummaryTestCaseGeneratorTest.kt

@@ -6,7 +6,6 @@ import org.utbot.common.workaround
 import org.utbot.examples.AbstractTestCaseGeneratorTest
 import org.utbot.examples.CoverageMatcher
 import org.utbot.examples.DoNotCalculate
-import org.utbot.framework.UtSettings.checkNpeForFinalFields
 import org.utbot.framework.UtSettings.checkNpeInNestedMethods
 import org.utbot.framework.UtSettings.checkNpeInNestedNotPrivateMethods
 import org.utbot.framework.UtSettings.checkSolverTimeoutMillis
@@ -96,7 +95,6 @@ open class SummaryTestCaseGeneratorTest(
             checkSolverTimeoutMillis = 0
             checkNpeInNestedMethods = true
             checkNpeInNestedNotPrivateMethods = true
-            checkNpeForFinalFields = true
         }
         val utMethod = UtMethod.from(method)
         val testCase = executionsModel(utMethod, mockStrategy)