Make UtEnumConstModel and UtClassRefModel reference models #414

Historically `UtEnumConstModel` and `UtClassRefModel` have been
processed not as other reference models, but in a special way,
more like to primitive types. This approach leads to several
problems, especially to class cast errors when processing generic
collections with enums or class references as elements.

This commit makes `UtEnumConstModel` and `UtClassRefModel` subtypes of
`UtReferenceModel`.

  * Concrete executor is modified to respect the identity of static
    fields to avoid rewriting enum values and `Class<?>` instances.

  * Special processing for enums is implemented.
    When a new enum value is created, or an `Object` is being cast
    to the enum type, static values for the enum class are initialized,
    and the set of hard constraint is added to require that the new
    instance has the same address and ordinal as any one of enum
    constants to implement reference equality for enums.

  * Corresponding changes in fuzzer model providers have been
    implemented.

Author: dtim

utbot-framework-api/build.gradle

@@ -14,6 +14,12 @@ dependencies {
     implementation group: 'io.github.microutils', name: 'kotlin-logging', version: kotlin_logging_version
 }
 
+compileKotlin {
+    kotlinOptions {
+        freeCompilerArgs += "-Xopt-in=kotlin.RequiresOptIn"
+    }
+}
+
 shadowJar {
     configurations = [project.configurations.compileClasspath]
     archiveClassifier.set('')

utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/Api.kt

@@ -50,6 +50,8 @@ import soot.jimple.JimpleBody
 import soot.jimple.Stmt
 import java.io.File
 import java.lang.reflect.Modifier
+import kotlin.contracts.ExperimentalContracts
+import kotlin.contracts.contract
 import kotlin.jvm.internal.CallableReference
 import kotlin.reflect.KCallable
 import kotlin.reflect.KClass
@@ -58,6 +60,8 @@ import kotlin.reflect.full.instanceParameter
 import kotlin.reflect.jvm.javaConstructor
 import kotlin.reflect.jvm.javaType
 
+const val SYMBOLIC_NULL_ADDR: Int = 0
+
 data class UtMethod<R>(
     val callable: KCallable<R>,
     val clazz: KClass<*>
@@ -282,6 +286,27 @@ fun UtModel.hasDefaultValue() =
  */
 fun UtModel.isMockModel() = this is UtCompositeModel && isMock
 
+/**
+ * Get model id (symbolic null value for UtNullModel)
+ * or null if model has no id (e.g., a primitive model) or the id is null.
+ */
+fun UtModel.idOrNull(): Int? = when (this) {
+    is UtNullModel -> SYMBOLIC_NULL_ADDR
+    is UtReferenceModel -> id
+    else -> null
+}
+
+/**
+ * Returns the model id if it is available, or throws an [IllegalStateException].
+ */
+@OptIn(ExperimentalContracts::class)
+fun UtModel?.getIdOrThrow(): Int {
+    contract {
+        returns() implies (this@getIdOrThrow != null)
+    }
+    return this?.idOrNull() ?: throw IllegalStateException("Model id must not be null: $this")
+}
+
 /**
  * Model for nulls.
  */
@@ -323,20 +348,24 @@ object UtVoidModel : UtModel(voidClassId)
  * Model for enum constant
  */
 data class UtEnumConstantModel(
+    override val id: Int?,
     override val classId: ClassId,
     val value: Enum<*>
-) : UtModel(classId) {
-    override fun toString(): String = "$value"
+) : UtReferenceModel(id, classId) {
+    // Model id is included for debugging purposes
+    override fun toString(): String = "$value@$id"
 }
 
 /**
  * Model for class reference
  */
 data class UtClassRefModel(
+    override val id: Int?,
     override val classId: ClassId,
     val value: Class<*>
-) : UtModel(classId) {
-    override fun toString(): String = "$value"
+) : UtReferenceModel(id, classId) {
+    // Model id is included for debugging purposes
+    override fun toString(): String = "$value@$id"
 }
 
 /**

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

@@ -24,7 +24,8 @@ import org.utbot.framework.plugin.api.UtCompositeModel
 import org.utbot.framework.plugin.api.UtModel
 import org.utbot.framework.plugin.api.UtNullModel
 import org.utbot.framework.plugin.api.UtPrimitiveModel
-import org.utbot.framework.plugin.api.UtReferenceModel
+import org.utbot.framework.plugin.api.getIdOrThrow
+import org.utbot.framework.plugin.api.idOrNull
 import org.utbot.framework.plugin.api.util.id
 import org.utbot.framework.plugin.api.util.objectArrayClassId
 import org.utbot.framework.plugin.api.util.objectClassId
@@ -398,7 +399,7 @@ class AssociativeArrayWrapper : WrapperInterface {
             UtNullModel(objectClassId),
             stores = (0 until sizeValue).associateTo(mutableMapOf()) { i ->
                 val model = touchedValues.stores[i]
-                val addr = if (model is UtNullModel) 0 else (model as UtReferenceModel).id!!
+                val addr = model.getIdOrThrow()
                 addr to resolver.resolveModel(
                     ObjectValue(
                         TypeStorage(OBJECT_TYPE),

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

@@ -22,9 +22,9 @@ import org.utbot.framework.plugin.api.UtCompositeModel
 import org.utbot.framework.plugin.api.UtExecutableCallModel
 import org.utbot.framework.plugin.api.UtModel
 import org.utbot.framework.plugin.api.UtNullModel
-import org.utbot.framework.plugin.api.UtReferenceModel
 import org.utbot.framework.plugin.api.UtStatementModel
 import org.utbot.framework.plugin.api.classId
+import org.utbot.framework.plugin.api.getIdOrThrow
 import org.utbot.framework.util.graph
 import org.utbot.framework.plugin.api.id
 import org.utbot.framework.plugin.api.util.booleanClassId
@@ -373,7 +373,7 @@ private fun constructKeysAndValues(keysModel: UtModel, valuesModel: UtModel, siz
         keysModel is UtArrayModel && valuesModel is UtArrayModel -> {
             List(size) {
                 keysModel.stores[it].let { model ->
-                    val addr = if (model is UtNullModel) 0 else (model as UtReferenceModel).id
+                    val addr = model.getIdOrThrow()
                     // as we do not support generics for now, valuesModel.classId.elementClassId is unknown,
                     // but it can be known with generics support
                     val defaultValue = UtNullModel(valuesModel.classId.elementClassId ?: objectClassId)

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

@@ -56,6 +56,7 @@ import kotlinx.collections.immutable.persistentListOf
 import kotlinx.collections.immutable.persistentSetOf
 import kotlinx.collections.immutable.toPersistentList
 import kotlinx.collections.immutable.toPersistentMap
+import org.utbot.framework.plugin.api.classId
 import soot.ArrayType
 import soot.BooleanType
 import soot.ByteType
@@ -147,7 +148,8 @@ data class Memory( // TODO: split purely symbolic memory and information about s
     private val speculativelyNotNullAddresses: UtArrayExpressionBase = UtConstArrayExpression(
         UtFalse,
         UtArraySort(UtAddrSort, UtBoolSort)
-    )
+    ),
+    private val symbolicEnumValues: PersistentList<ObjectValue> = persistentListOf()
 ) {
     val chunkIds: Set<ChunkId>
         get() = initial.keys
@@ -297,7 +299,8 @@ data class Memory( // TODO: split purely symbolic memory and information about s
             visitedValues = updVisitedValues,
             touchedAddresses = updTouchedAddresses,
             instanceFieldReadOperations = instanceFieldReadOperations.addAll(update.instanceFieldReads),
-            speculativelyNotNullAddresses = updSpeculativelyNotNullAddresses
+            speculativelyNotNullAddresses = updSpeculativelyNotNullAddresses,
+            symbolicEnumValues = symbolicEnumValues.addAll(update.symbolicEnumValues)
         )
     }
 
@@ -307,7 +310,6 @@ data class Memory( // TODO: split purely symbolic memory and information about s
      */
     fun memoryForNestedMethod(): Memory = this.copy(updates = MemoryUpdate())
 
-
     /**
      * Returns copy of queued [updates] which consists only of updates of static fields.
      * This is necessary for substituting unbounded symbolic variables into the static fields.
@@ -350,6 +352,9 @@ data class Memory( // TODO: split purely symbolic memory and information about s
     fun findStaticInstanceOrNull(id: ClassId): ObjectValue? = staticInstanceStorage[id]
 
     fun findTypeForArrayOrNull(addr: UtAddrExpression): ArrayType? = addrToArrayType[addr]
+
+    fun getSymbolicEnumValues(classId: ClassId): List<ObjectValue> =
+        symbolicEnumValues.filter { it.type.classId == classId }
 }
 
 /**
@@ -967,7 +972,8 @@ data class MemoryUpdate(
     val touchedAddresses: PersistentList<UtAddrExpression> = persistentListOf(),
     val classIdToClearStatics: ClassId? = null,
     val instanceFieldReads: PersistentSet<InstanceFieldReadOperation> = persistentHashSetOf(),
-    val speculativelyNotNullAddresses: PersistentList<UtAddrExpression> = persistentListOf()
+    val speculativelyNotNullAddresses: PersistentList<UtAddrExpression> = persistentListOf(),
+    val symbolicEnumValues: PersistentList<ObjectValue> = persistentListOf()
 ) {
     operator fun plus(other: MemoryUpdate) =
         this.copy(
@@ -986,7 +992,11 @@ data class MemoryUpdate(
             classIdToClearStatics = other.classIdToClearStatics,
             instanceFieldReads = instanceFieldReads.addAll(other.instanceFieldReads),
             speculativelyNotNullAddresses = speculativelyNotNullAddresses.addAll(other.speculativelyNotNullAddresses),
+            symbolicEnumValues = symbolicEnumValues.addAll(other.symbolicEnumValues),
         )
+
+    fun getSymbolicEnumValues(classId: ClassId): List<ObjectValue> =
+        symbolicEnumValues.filter { it.type.classId == classId }
 }
 
 // array - Java Array

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

@@ -71,6 +71,7 @@ import kotlin.math.max
 import kotlin.math.min
 import kotlinx.collections.immutable.persistentListOf
 import kotlinx.collections.immutable.persistentSetOf
+import org.utbot.framework.plugin.api.SYMBOLIC_NULL_ADDR
 import soot.ArrayType
 import soot.BooleanType
 import soot.ByteType
@@ -325,7 +326,7 @@ class Resolver(
         val mockInfoEnriched = mockInfos.getValue(concreteAddr)
         val mockInfo = mockInfoEnriched.mockInfo
 
-        if (concreteAddr == NULL_ADDR) {
+        if (concreteAddr == SYMBOLIC_NULL_ADDR) {
             return UtNullModel(mockInfo.classId)
         }
 
@@ -437,7 +438,7 @@ class Resolver(
 
     private fun resolveObject(objectValue: ObjectValue): UtModel {
         val concreteAddr = holder.concreteAddr(objectValue.addr)
-        if (concreteAddr == NULL_ADDR) {
+        if (concreteAddr == SYMBOLIC_NULL_ADDR) {
             return UtNullModel(objectValue.type.sootClass.id)
         }
 
@@ -498,7 +499,7 @@ class Resolver(
         actualType: RefType,
     ): UtModel {
         val concreteAddr = holder.concreteAddr(addr)
-        if (concreteAddr == NULL_ADDR) {
+        if (concreteAddr == SYMBOLIC_NULL_ADDR) {
             return UtNullModel(defaultType.sootClass.id)
         }
 
@@ -615,7 +616,7 @@ class Resolver(
         val modeledNumDimensions = holder.eval(numDimensionsArray.select(addrExpression)).intValue()
 
         val classRef = classRefByName(modeledType, modeledNumDimensions)
-        val model = UtClassRefModel(CLASS_REF_CLASS_ID, classRef)
+        val model = UtClassRefModel(addr, CLASS_REF_CLASS_ID, classRef)
         addConstructedModel(addr, model)
 
         return model
@@ -640,7 +641,7 @@ class Resolver(
             clazz.enumConstants.indices.random()
         }
         val value = clazz.enumConstants[index] as Enum<*>
-        val model = UtEnumConstantModel(clazz.id, value)
+        val model = UtEnumConstantModel(addr, clazz.id, value)
         addConstructedModel(addr, model)
 
         return model
@@ -795,7 +796,7 @@ class Resolver(
      */
     private fun constructArrayModel(instance: ArrayValue): UtModel {
         val concreteAddr = holder.concreteAddr(instance.addr)
-        if (concreteAddr == NULL_ADDR) {
+        if (concreteAddr == SYMBOLIC_NULL_ADDR) {
             return UtNullModel(instance.type.id)
         }
 
@@ -829,7 +830,7 @@ class Resolver(
         concreteAddr: Address,
         details: ArrayExtractionDetails,
     ): UtModel {
-        if (concreteAddr == NULL_ADDR) {
+        if (concreteAddr == SYMBOLIC_NULL_ADDR) {
             return UtNullModel(actualType.id)
         }
 
@@ -903,7 +904,7 @@ class Resolver(
         elementType: ArrayType,
         details: ArrayExtractionDetails
     ): UtModel {
-        if (addr == NULL_ADDR) {
+        if (addr == SYMBOLIC_NULL_ADDR) {
             return UtNullModel(elementType.id)
         }
 
@@ -927,7 +928,7 @@ class Resolver(
      * Uses [constructTypeOrNull] to evaluate possible element type.
      */
     private fun arrayOfObjectsElementModel(concreteAddr: Address, defaultType: RefType): UtModel {
-        if (concreteAddr == NULL_ADDR) {
+        if (concreteAddr == SYMBOLIC_NULL_ADDR) {
             return UtNullModel(defaultType.id)
         }
 
@@ -976,8 +977,7 @@ private data class ArrayExtractionDetails(
     val oneDimensionalArray: UtArrayExpressionBase
 )
 
-private const val NULL_ADDR = 0
-internal val nullObjectAddr = UtAddrExpression(mkInt(NULL_ADDR))
+internal val nullObjectAddr = UtAddrExpression(mkInt(SYMBOLIC_NULL_ADDR))
 
 
 fun SymbolicValue.isNullObject() =