first support of lists

UnitTestBot · AbdullinAM · Jun 20, 2022 · Jun 20, 2022 · Jun 22, 2022 · Jun 28, 2022
commit 60df4a42393ba0ca8fe97f89cdd7c58d5afc8506
diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/Api.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/Api.kt
@@ -455,14 +455,14 @@ sealed class UtConstraintModel(
 
 data class UtPrimitiveConstraintModel(
     override val variable: UtConstraintVariable,
-    override val utConstraints: Set<UtConstraint>
+    override val utConstraints: Set<UtConstraint>,
+    val  concrete: Any? = null
 ) : UtConstraintModel(variable, utConstraints) {
 }
 
 data class UtReferenceConstraintModel(
     override val variable: UtConstraintVariable,
     override val utConstraints: Set<UtConstraint>,
-    val concrete: Any? = null
 ) : UtConstraintModel(variable, utConstraints) {
     fun isNull() = utConstraints.any {
         it is UtRefEqConstraint && it.lhv == variable && it.rhv is UtConstraintNull
@@ -475,20 +475,35 @@ data class UtReferenceToConstraintModel(
     override val utConstraints: Set<UtConstraint> = emptySet()
 ) : UtConstraintModel(variable, utConstraints)
 
-data class UtArrayConstraintModel(
+sealed class UtElementContainerConstraintModel(
     override val variable: UtConstraintVariable,
-    val length: UtModel,
-    val elements: Map<UtModel, UtModel>,
+    open val length: UtModel,
+    open val elements: Map<UtModel, UtModel>,
     override val utConstraints: Set<UtConstraint> = emptySet()
 ) : UtConstraintModel(variable, utConstraints) {
-    val allConstraints: Set<UtConstraint> get() = elements.toList().fold((length as UtConstraintModel).utConstraints) { acc, pair ->
-        acc +
-        ((pair.first as? UtConstraintModel)?.utConstraints ?: emptySet()) +
-        ((pair.second as? UtConstraintModel)?.utConstraints ?: emptySet()) +
-        ((pair.second as? UtArrayConstraintModel)?.allConstraints ?: emptySet())
-    }
+    val allConstraints: Set<UtConstraint>
+        get() = elements.toList().fold((length as UtConstraintModel).utConstraints) { acc, pair ->
+            acc +
+                    ((pair.first as? UtConstraintModel)?.utConstraints ?: emptySet()) +
+                    ((pair.second as? UtConstraintModel)?.utConstraints ?: emptySet()) +
+                    ((pair.second as? UtArrayConstraintModel)?.allConstraints ?: emptySet())
+        }
 }
 
+data class UtArrayConstraintModel(
+    override val variable: UtConstraintVariable,
+    override val length: UtModel,
+    override val elements: Map<UtModel, UtModel>,
+    override val utConstraints: Set<UtConstraint> = emptySet()
+) : UtElementContainerConstraintModel(variable, length, elements, utConstraints)
+
+data class UtListConstraintModel(
+    override val variable: UtConstraintVariable,
+    override val length: UtModel,
+    override val elements: Map<UtModel, UtModel>,
+    override val utConstraints: Set<UtConstraint> = emptySet()
+) : UtElementContainerConstraintModel(variable, length, elements, utConstraints)
+
 /**
  * Model for complex objects with assemble instructions.
  *
@@ -588,12 +603,12 @@ data class UtDirectSetFieldModel(
     val fieldModel: UtModel,
 ) : UtStatementModel(instance) {
     override fun toString(): String = withToStringThreadLocalReentrancyGuard {
-            val modelRepresentation = when (fieldModel) {
-                is UtAssembleModel -> fieldModel.modelName
-                else -> fieldModel.toString()
-            }
-            "${instance.modelName}.${fieldId.name} = $modelRepresentation"
+        val modelRepresentation = when (fieldModel) {
+            is UtAssembleModel -> fieldModel.modelName
+            else -> fieldModel.toString()
         }
+        "${instance.modelName}.${fieldId.name} = $modelRepresentation"
+    }
 
 }
 
@@ -1058,7 +1073,7 @@ class BuiltinMethodId(
 
 open class TypeParameters(val parameters: List<ClassId> = emptyList())
 
-class WildcardTypeParameter: TypeParameters(emptyList())
+class WildcardTypeParameter : TypeParameters(emptyList())
 
 interface TestCaseGenerator {
     fun init(
@@ -1199,6 +1214,7 @@ enum class CodegenLanguage(
                 "-cp", classPath,
                 "-XDignore.symbol.file" // to let javac use classes from rt.jar
             ).plus(sourcesFiles)
+
             KOTLIN -> listOf("-d", buildDirectory, "-jvm-target", jvmTarget, "-cp", classPath).plus(sourcesFiles)
         }
         if (this == KOTLIN && System.getenv("KOTLIN_HOME") == null) {

diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/constraints/ConstraintResolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/constraints/ConstraintResolver.kt
@@ -9,6 +9,8 @@ import org.utbot.framework.plugin.api.*
 import org.utbot.framework.plugin.api.constraint.UtConstraintTransformer
 import org.utbot.framework.plugin.api.constraint.UtConstraintVariableCollector
 import org.utbot.framework.plugin.api.util.intClassId
+import org.utbot.framework.plugin.api.util.isPrimitive
+import org.utbot.framework.plugin.api.util.objectClassId
 
 /**
  * Constructs path conditions using calculated model. Can construct them for initial and current memory states that reflect
@@ -122,7 +124,7 @@ class ConstraintResolver(
             value.addr.variable,
             collectAtoms(value, addrs),
             addrs[value.addr.variable.addr]!!.map { it.variable }.toSet(),
-            value.concrete?.value
+            value.concrete
         )
     }
 
@@ -154,27 +156,31 @@ class ConstraintResolver(
         variable: UtConstraintVariable,
         atoms: Set<UtConstraint>,
         aliases: Set<UtConstraintVariable>,
-        concrete: Any? = null
+        concrete: Concrete? = null
     ): UtModel = when {
-        variable.isPrimitive -> buildPrimitiveModel(atoms, variable, aliases)
+        variable.isPrimitive -> buildPrimitiveModel(variable, atoms, aliases)
         variable.addr == NULL_ADDR -> UtNullModel(variable.classId)
         variable.addr in resolvedConstraints -> UtReferenceToConstraintModel(
             variable,
             resolvedConstraints.getValue(variable.addr)
         )
 
-        variable.isArray -> buildArrayModel(atoms, variable, aliases).also {
+        variable.isArray -> buildArrayModel(variable, atoms, aliases).also {
             resolvedConstraints[variable.addr] = it
         }
 
-        else -> buildObjectModel(atoms, variable, aliases, concrete).also {
-            resolvedConstraints[variable.addr] = it
+        else -> when (concrete) {
+            null -> buildObjectModel(variable, atoms, aliases).also {
+                resolvedConstraints[variable.addr] = it
+            }
+
+            else -> buildConcreteModel(concrete, variable, atoms, aliases)
         }
     }
 
     private fun buildPrimitiveModel(
-        atoms: Set<UtConstraint>,
         variable: UtConstraintVariable,
+        atoms: Set<UtConstraint>,
         aliases: Set<UtConstraintVariable>
     ): UtModel {
         assert(variable.isPrimitive)
@@ -185,15 +191,14 @@ class ConstraintResolver(
         }.map { it.accept(UtConstraintTransformer(aliases.associateWith { variable })) }.toSet()
 
         return UtPrimitiveConstraintModel(
-            variable, primitiveConstraints
+            variable, primitiveConstraints, concrete = holder.eval(variable.expr).value()
         )
     }
 
     private fun buildObjectModel(
-        atoms: Set<UtConstraint>,
         variable: UtConstraintVariable,
-        aliases: Set<UtConstraintVariable>,
-        concrete: Any? = null
+        atoms: Set<UtConstraint>,
+        aliases: Set<UtConstraintVariable>
     ): UtModel {
         assert(!variable.isPrimitive && !variable.isArray)
         assert(aliases.all { !it.isPrimitive && !it.isArray })
@@ -204,13 +209,13 @@ class ConstraintResolver(
         }.toSet()
 
         return UtReferenceConstraintModel(
-            variable, refConstraints, concrete
+            variable, refConstraints
         )
     }
 
     private fun buildArrayModel(
-        atoms: Set<UtConstraint>,
         variable: UtConstraintVariable,
+        atoms: Set<UtConstraint>,
         aliases: Set<UtConstraintVariable>
     ): UtModel {
         assert(variable.isArray)
@@ -226,43 +231,46 @@ class ConstraintResolver(
         val concreteLength = lengths.firstOrNull()?.let { holder.eval(it.expr).value() as Int } ?: 100
 
         val indexMap = atoms
-            .flatMap {
-                it.accept(UtConstraintVariableCollector { index ->
-                    index is UtConstraintArrayAccess && index.instance in allAliases
-                })
+            .flatten { index ->
+                index is UtConstraintArrayAccess && index.instance in allAliases
             }
             .map { (it as UtConstraintArrayAccess).index }
             .filter { (holder.eval(it.expr).value() as Int) < concreteLength }
-            .groupBy { holder.eval(varBuilder[it]) }
-            .map { it.value.toSet() }
+            .groupBy { holder.eval(varBuilder[it]).value() }
+            .mapValues { it.value.toSet() }
 
         var indexCount = 0
-        val elements = indexMap.associate { indices ->
+        val elements = indexMap.map { (key, indices) ->
             val indexVariable = UtConstraintParameter(
                 "${variable}_index${indexCount++}", intClassId
             )
 
             val indexModel = UtPrimitiveConstraintModel(
                 indexVariable,
-                indices.map { UtEqConstraint(indexVariable, it) }.toSet()
+                indices.map { UtEqConstraint(indexVariable, it) }.toSet(),
+                concrete = key
             )
 
-            val arrayAccess = UtConstraintArrayAccess(variable, indexVariable, elementClassId)
-            val actualExpr = aliases.flatMap { base ->
+            val actualExpr = allAliases.flatMap { base ->
                 indices.map { UtConstraintArrayAccess(base, it, elementClassId) }
             }.mapNotNull { varBuilder.backMapping[it] }.first()
+            val elementType = when {
+                elementClassId.isPrimitive -> elementClassId
+                else -> varBuilder.evalType(actualExpr as UtAddrExpression)!!.classId
+            }
+            val arrayAccess = UtConstraintArrayAccess(variable, indexVariable, elementType)
             varBuilder.backMapping[arrayAccess] = actualExpr
             val indexAliases = indices.flatMap { idx ->
                 allAliases.map { UtConstraintArrayAccess(it, idx, elementClassId) }
             }.toSet()
-            val res = buildModel(arrayAccess, atoms, indexAliases, null).withConstraints(
+            val res = buildModel(arrayAccess, atoms, indexAliases).withConstraints(
                 indices.map { UtEqConstraint(it, indexVariable) }.toSet() + setOf(
                     UtGeConstraint(indexVariable, UtConstraintNumericConstant(0)),
                     UtLtConstraint(indexVariable, lengthVariable)
                 )
             )
             (indexModel as UtModel) to res
-        }
+        }.toMap()
 
         return UtArrayConstraintModel(
             variable,
@@ -272,6 +280,60 @@ class ConstraintResolver(
         )
     }
 
+    private fun buildConcreteModel(
+        concrete: Concrete,
+        variable: UtConstraintVariable,
+        atoms: Set<UtConstraint>,
+        aliases: Set<UtConstraintVariable>
+    ): UtModel = when (concrete.value) {
+        is ListWrapper -> buildListModel(concrete.value, variable, atoms, aliases)
+        else -> TODO()
+    }
+
+    private fun buildListModel(
+        concrete: ListWrapper,
+        variable: UtConstraintVariable,
+        atoms: Set<UtConstraint>,
+        aliases: Set<UtConstraintVariable>
+    ): UtModel {
+        val allAliases = aliases + variable
+        val refConstraints = atoms.filter { constraint ->
+            allAliases.any { it in constraint }
+        }.toSet()
+
+        val default = { buildObjectModel(variable, atoms, aliases) }
+        val elementData = atoms
+            .flatten { it is UtConstraintFieldAccess && it.instance == variable && it.fieldId.name == "elementData" }
+            .firstOrNull() as? UtConstraintFieldAccess ?: return default()
+        val storageArray = atoms
+            .flatten { it is UtConstraintFieldAccess && it.instance == elementData && it.fieldId.name == "storage" }
+            .firstOrNull() as? UtConstraintFieldAccess ?: return default()
+        val aliasArrays = aliases.map {
+            UtConstraintFieldAccess(UtConstraintFieldAccess(it, elementData.fieldId), storageArray.fieldId)
+        }.toSet()
+        val array = buildArrayModel(storageArray, atoms, aliasArrays) as UtArrayConstraintModel
+        val concreteLength = (array.length as UtPrimitiveConstraintModel).concrete as Int
+        val concreteIndices = array.elements.toList().associate { (index, value) ->
+            (index as UtPrimitiveConstraintModel).concrete as Int to ((index as UtModel) to value)
+        }
+        val completedElements = (0 until concreteLength).associate {
+            if (it in concreteIndices) concreteIndices[it]!!
+            else {
+                UtPrimitiveConstraintModel(
+                    UtConstraintNumericConstant(it),
+                    emptySet(),
+                    it
+                ) to UtNullModel(objectClassId)
+            }
+        }
+        return UtListConstraintModel(
+            variable,
+            array.length,
+            completedElements,
+            array.utConstraints + refConstraints
+        )
+    }
+
     private val UtExpression.variable get() = accept(varBuilder)
     private val UtConstraintVariable.expr get() = varBuilder[this]
     private val UtConstraintVariable.addr get() = holder.concreteAddr(expr as UtAddrExpression)
@@ -283,4 +345,9 @@ class ConstraintResolver(
         is UtArrayConstraintModel -> copy(utConstraints = utConstraints + constraints)
         else -> this
     }
+
+    private fun Set<UtConstraint>.flatten(predicate: (UtConstraintVariable) -> Boolean): Set<UtConstraintVariable> =
+        this.flatMap {
+            it.accept(UtConstraintVariableCollector(predicate))
+        }.toSet()
 }
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/constraint/UtVarBuilder.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/constraint/UtVarBuilder.kt
@@ -24,6 +24,8 @@ class UtVarBuilder(
     operator fun get(variable: UtConstraintVariable) = backMapping[variable]
         ?: throw IllegalArgumentException()
 
+    fun evalType(addr: UtAddrExpression) = holder.findTypeOrNull(addr)
+
     override fun visit(expr: UtArraySelectExpression): UtConstraintVariable {
         val res = when (val base = expr.arrayExpression.accept(this)) {
             is UtConstraintParameter -> when (base.name) {

diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/Resolver.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/Resolver.kt
@@ -23,6 +23,7 @@ class Resolver(
             is NullUnit -> UtNullModel(unit.classId)
             is ReferenceToUnit -> resolve(synthesisUnitContext[unit.reference])
             is ArrayUnit -> unitToModel.getOrPut(unit) { resolveArray(unit) }
+            is ListUnit -> unitToModel.getOrPut(unit) { resolveList(unit) }
         }
 
     private fun resolveMethodUnit(unit: MethodUnit): UtModel =
@@ -76,6 +77,37 @@ class Resolver(
         return model
     }
 
+    private fun resolveList(unit: ListUnit): UtModel {
+        val elements = unit.elements.associate {
+            resolve(synthesisUnitContext[it.first]) to resolve(synthesisUnitContext[it.second])
+        }
+
+        val instantiationChain = mutableListOf<UtStatementModel>()
+        val modificationChain = mutableListOf<UtStatementModel>()
+
+        val model = UtAssembleModel(
+            nextDefaultModelId++,
+            unit.classId,
+            nextModelName("refModel_${unit.classId.simpleName}"),
+            instantiationChain,
+            modificationChain
+        )
+
+        instantiationChain.add(
+            UtExecutableCallModel(model, unit.constructorId, listOf(), model)
+        )
+
+        for ((_, value) in elements) {
+            modificationChain.add(
+                UtExecutableCallModel(
+                    model, unit.addId, listOf(value),
+                )
+            )
+        }
+
+        return model
+    }
+
     private fun resolveArray(unit: ArrayUnit): UtModel {
         val lengthModel = resolve(synthesisUnitContext[unit.length]) as UtPrimitiveModel
         val elements = unit.elements.associate {

diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/StateProducer.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/StateProducer.kt
@@ -32,7 +32,7 @@ class CompositeUnitExpander(
         statementsStorage.items
             .filter { (method, info) ->
                 val sameClass = method.classId == classId
-                val modifiesSomething = info.modifiedFields.any { it.declaringClass == classId }
+                val modifiesSomething = true//info.modifiedFields.any { it.declaringClass == classId }
                 sameClass && modifiesSomething
             }
             .keys