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

@@ -266,6 +266,15 @@ fun UtModel.hasDefaultValue() =
  */
 fun UtModel.isMockModel() = this is UtCompositeModel && isMock
 
+/**
+ * Get model id or null if id is null or the model has no id.
+ */
+fun UtModel.idOrNull(): Int? = when (this) {
+    is UtNullModel -> 0
+    is UtReferenceModel -> id
+    else -> null
+}
+
 /**
  * Model for nulls.
  */
@@ -307,20 +316,64 @@ 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) {
+    override fun toString(): String = "$value@$id"
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (javaClass != other?.javaClass) return false
+
+        other as UtEnumConstantModel
+
+        if (id != other.id) return false
+        if (classId != other.classId) return false
+        if (value != other.value) return false
+
+        return true
+    }
+
+
+    override fun hashCode(): Int {
+        var result = id ?: 0
+        result = 31 * result + classId.hashCode()
+        result = 31 * result + value.hashCode()
+        return result
+    }
+
 }
 
 /**
  * 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) {
+    override fun toString(): String = "$value:$id"
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (javaClass != other?.javaClass) return false
+
+        other as UtClassRefModel
+
+        if (id != other.id) return false
+        if (classId != other.classId) return false
+        if (value != other.value) return false
+
+        return true
+    }
+
+    override fun hashCode(): Int {
+        var result = id ?: 0
+        result = 31 * result + classId.hashCode()
+        result = 31 * result + value.hashCode()
+        return result
+    }
 }
 
 /**

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/Extensions.kt

@@ -484,3 +484,4 @@ val SootMethod.isUtMockAssumeOrExecuteConcretely
  */
 val SootMethod.isPreconditionCheckMethod
     get() = declaringClass.isOverridden && name == "preconditionCheck"
+

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

@@ -53,9 +53,11 @@ import kotlinx.collections.immutable.mutate
 import kotlinx.collections.immutable.persistentHashMapOf
 import kotlinx.collections.immutable.persistentHashSetOf
 import kotlinx.collections.immutable.persistentListOf
+import kotlinx.collections.immutable.persistentMapOf
 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 +149,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 +300,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 +311,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 +353,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): Collection<ObjectValue> =
+        symbolicEnumValues.filter { it.type.classId == classId }
 }
 
 /**
@@ -967,7 +973,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 +993,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): Collection<ObjectValue> =
+        symbolicEnumValues.filter { it.type.classId == classId }
 }
 
 // array - Java Array

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

@@ -615,7 +615,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 +640,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

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

utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt

@@ -5,6 +5,11 @@ import org.utbot.engine.MemoryUpdate
 import org.utbot.engine.pc.UtBoolExpression
 import kotlinx.collections.immutable.PersistentSet
 import kotlinx.collections.immutable.toPersistentSet
+import org.utbot.engine.StaticFieldMemoryUpdateInfo
+import org.utbot.engine.UtNamedStore
+import org.utbot.framework.plugin.api.ClassId
+import org.utbot.framework.plugin.api.FieldId
+import org.utbot.framework.plugin.api.classId
 
 /**
  * Represents appendable-only immutable constraints.

utbot-framework/src/main/kotlin/org/utbot/engine/util/statics/concrete/EnumConcreteUtils.kt

@@ -68,7 +68,7 @@ fun Traverser.makeEnumStaticFieldsUpdates(
     enumConstantSymbolicResultsByName: Map<String, MethodResult>,
     enumConstantSymbolicValues: List<ObjectValue>,
     enumClassValue: ObjectValue,
-    fieldId: FieldId
+    fieldId: FieldId?
 ): Pair<SymbolicStateUpdate, SymbolicValue?> {
     var staticFieldsUpdates = SymbolicStateUpdate()
     var symbolicValueForLocal: SymbolicValue? = null
@@ -101,7 +101,7 @@ fun Traverser.makeEnumStaticFieldsUpdates(
         }
 
         // save value to associate it with local if required
-        if (sootStaticField.name == fieldId.name) {
+        if (fieldId != null && sootStaticField.name == fieldId.name) {
             symbolicValueForLocal = fieldSymbolicValue
         }
     }

utbot-framework/src/main/kotlin/org/utbot/external/api/UtModelFactory.kt

@@ -67,8 +67,10 @@ class UtModelFactory(
         elements.toMutableMap()
     )
 
-    fun produceClassRefModel(clazz: Class<String>): UtModel = UtClassRefModel(
-        classIdForType(clazz), clazz
+    fun produceClassRefModel(clazz: Class<*>) = UtClassRefModel(
+        modelIdCounter.incrementAndGet(),
+        classIdForType(clazz),
+        clazz
     )
 }