Make UtEnumConstModel and UtClassRefModel reference models #414

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

@@ -51,6 +51,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
@@ -59,6 +61,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<*>
@@ -267,6 +271,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.
  */
@@ -308,20 +333,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-api/src/main/kotlin/org/utbot/framework/plugin/api/util/IdUtil.kt

@@ -117,6 +117,9 @@ val ClassId.isFloatType: Boolean
 val ClassId.isDoubleType: Boolean
     get() = this == doubleClassId || this == doubleWrapperClassId
 
+val ClassId.isClassType: Boolean
+    get() = this == classClassId
+
 val voidClassId = ClassId("void")
 val booleanClassId = ClassId("boolean")
 val byteClassId = ClassId("byte")
@@ -138,6 +141,8 @@ val longWrapperClassId = java.lang.Long::class.id
 val floatWrapperClassId = java.lang.Float::class.id
 val doubleWrapperClassId = java.lang.Double::class.id
 
+val classClassId = java.lang.Class::class.id
+
 // We consider void wrapper as primitive wrapper
 // because voidClassId is considered primitive here
 val primitiveWrappers = setOf(
@@ -285,6 +290,9 @@ val ClassId.isMap: Boolean
 val ClassId.isIterableOrMap: Boolean
     get() = isIterable || isMap
 
+val ClassId.isEnum: Boolean
+    get() = jClass.isEnum
+
 fun ClassId.findFieldByIdOrNull(fieldId: FieldId): Field? {
     if (isNotSubtypeOf(fieldId.declaringClass)) {
         return null

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() =