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/src/main/kotlin/org/utbot/framework/plugin/api/Api.kt

@@ -58,6 +58,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 +284,16 @@ 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
+}
+
 /**
  * Model for nulls.
  */
@@ -323,20 +335,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,7 @@ 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.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 +398,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?.idOrNull() ?: throw IllegalStateException("Unsupported model: $model")
                 addr to resolver.resolveModel(
                     ObjectValue(
                         TypeStorage(OBJECT_TYPE),

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

@@ -27,6 +27,7 @@ import org.utbot.framework.plugin.api.UtStatementModel
 import org.utbot.framework.plugin.api.classId
 import org.utbot.framework.util.graph
 import org.utbot.framework.plugin.api.id
+import org.utbot.framework.plugin.api.idOrNull
 import org.utbot.framework.plugin.api.util.booleanClassId
 import org.utbot.framework.plugin.api.util.constructorId
 import org.utbot.framework.plugin.api.util.id
@@ -373,7 +374,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?.idOrNull() ?: throw IllegalStateException("Unsupported model: $model")
                     // 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() =

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

@@ -497,7 +497,7 @@ class Traverser(
         val declaringClass = field.declaringClass
 
         val updates = if (declaringClass.isEnum) {
-            makeConcreteUpdatesForEnums(fieldId, declaringClass, stmt)
+            makeConcreteUpdatesForEnumsWithStmt(fieldId, declaringClass, stmt)
         } else {
             makeConcreteUpdatesForNonEnumStaticField(field, fieldId, declaringClass, stmt)
         }
@@ -518,13 +518,10 @@ class Traverser(
         return true
     }
 
-    @Suppress("UnnecessaryVariable")
-    private fun makeConcreteUpdatesForEnums(
-        fieldId: FieldId,
-        declaringClass: SootClass,
-        stmt: Stmt
-    ): SymbolicStateUpdate {
-        val type = declaringClass.type
+    private fun makeConcreteUpdatesForEnum(
+        type: RefType,
+        fieldId: FieldId? = null
+    ): Pair<SymbolicStateUpdate, SymbolicValue?> {
         val jClass = type.id.jClass
 
         // symbolic value for enum class itself
@@ -545,7 +542,7 @@ class Traverser(
 
         val (staticFieldUpdates, curFieldSymbolicValueForLocalVariable) = makeEnumStaticFieldsUpdates(
             staticFields,
-            declaringClass,
+            type.sootClass,
             enumConstantSymbolicResultsByName,
             enumConstantSymbolicValues,
             enumClassValue,
@@ -564,14 +561,25 @@ class Traverser(
 
         val initializedStaticFieldsMemoryUpdate = MemoryUpdate(
             initializedStaticFields = staticFields.associate { it.first.fieldId to it.second.single() }.toPersistentMap(),
-            meaningfulStaticFields = meaningfulStaticFields.map { it.first.fieldId }.toPersistentSet()
+            meaningfulStaticFields = meaningfulStaticFields.map { it.first.fieldId }.toPersistentSet(),
+            symbolicEnumValues = enumConstantSymbolicValues.toPersistentList()
         )
 
-        val allUpdates = staticFieldUpdates +
-                nonStaticFieldsUpdates +
-                initializedStaticFieldsMemoryUpdate +
-                createConcreteLocalValueUpdate(stmt, curFieldSymbolicValueForLocalVariable)
+        return Pair(
+            staticFieldUpdates + nonStaticFieldsUpdates + initializedStaticFieldsMemoryUpdate,
+            curFieldSymbolicValueForLocalVariable
+        )
+    }
 
+    @Suppress("UnnecessaryVariable")
+    private fun makeConcreteUpdatesForEnumsWithStmt(
+        fieldId: FieldId,
+        declaringClass: SootClass,
+        stmt: Stmt
+    ): SymbolicStateUpdate {
+        val (enumUpdates, curFieldSymbolicValueForLocalVariable) =
+            makeConcreteUpdatesForEnum(declaringClass.type, fieldId)
+        val allUpdates = enumUpdates + createConcreteLocalValueUpdate(stmt, curFieldSymbolicValueForLocalVariable)
         return allUpdates
     }
 
@@ -1373,6 +1381,39 @@ class Traverser(
         queuedSymbolicStateUpdates = queuedSymbolicStateUpdates.copy(memoryUpdates = MemoryUpdate())
     }
 
+    /**
+     * Return a symbolic value of the ordinal corresponding to the enum value with the given address.
+     */
+    private fun findEnumOrdinal(type: RefType, addr: UtAddrExpression): PrimitiveValue {
+        val array = memory.findArray(MemoryChunkDescriptor(ENUM_ORDINAL, type, IntType.v()))
+        return array.select(addr).toIntValue()
+    }
+
+    /**
+     * Initialize enum class: create symbolic values for static enum values and generate constraints
+     * that restrict the new instance to match one of enum values.
+     */
+    private fun initEnum(type: RefType, addr: UtAddrExpression, ordinal: PrimitiveValue) {
+        val classId = type.id
+        var predefinedEnumValues = memory.getSymbolicEnumValues(classId)
+        if (predefinedEnumValues.isEmpty()) {
+            val (enumValuesUpdate, _) = makeConcreteUpdatesForEnum(type)
+            queuedSymbolicStateUpdates += enumValuesUpdate
+            predefinedEnumValues = enumValuesUpdate.memoryUpdates.getSymbolicEnumValues(classId)
+        }
+
+        val enumValueConstraints = mkOr(
+            listOf(addrEq(addr, nullObjectAddr)) + predefinedEnumValues.map {
+                mkAnd(
+                    addrEq(addr, it.addr),
+                    mkEq(ordinal, findEnumOrdinal(it.type, it.addr))
+                )
+            }
+        )
+
+        queuedSymbolicStateUpdates += enumValueConstraints.asHardConstraint()
+    }
+
     private fun arrayInstanceOf(value: ArrayValue, checkType: Type): PrimitiveValue {
         val notNullConstraint = mkNot(addrEq(value.addr, nullObjectAddr))
 
@@ -1530,6 +1571,11 @@ class Traverser(
         queuedSymbolicStateUpdates += typeConstraint.asHardConstraint()
         queuedSymbolicStateUpdates += typeRegistry.zeroDimensionConstraint(objectValue.addr).asHardConstraint()
 
+        // If we are casting to an enum class, we should initialize enum values and add value equality constraints
+        if (typeAfterCast.sootClass?.isEnum == true) {
+            initEnum(typeAfterCast, castedObject.addr, findEnumOrdinal(typeAfterCast, castedObject.addr))
+        }
+
         // TODO add memory constraints JIRA:1523
         return castedObject
     }
@@ -1978,13 +2024,13 @@ class Traverser(
 
         queuedSymbolicStateUpdates += typeRegistry.typeConstraint(addr, typeStorage).all().asHardConstraint()
 
-        val array = memory.findArray(MemoryChunkDescriptor(ENUM_ORDINAL, type, IntType.v()))
-        val ordinal = array.select(addr).toIntValue()
+        val ordinal = findEnumOrdinal(type, addr)
         val enumSize = classLoader.loadClass(type.sootClass.name).enumConstants.size
 
         queuedSymbolicStateUpdates += mkOr(Ge(ordinal, 0), addrEq(addr, nullObjectAddr)).asHardConstraint()
         queuedSymbolicStateUpdates += mkOr(Lt(ordinal, enumSize), addrEq(addr, nullObjectAddr)).asHardConstraint()
 
+        initEnum(type, addr, ordinal)
         touchAddress(addr)
 
         return ObjectValue(typeStorage, addr)