first working protoype with arrays

UnitTestBot · AbdullinAM · Jun 20, 2022 · Jun 20, 2022 · Jun 22, 2022 · Jun 28, 2022
commit ba9bb6281c3c042c41096c8cfe38f61759f8b4f3
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
@@ -173,7 +173,7 @@ data class UtExecution(
     var summary: List<DocStatement>? = null,
     var testMethodName: String? = null,
     var displayName: String? = null,
-    val hole: Any? = null
+    val constrainedExecution: ConstrainedExecution? = null
 ) : UtResult() {
     /**
      * By design the 'before' and 'after' states contain info about the same fields.
@@ -479,7 +479,12 @@ data class UtArrayConstraintModel(
     val length: UtModel,
     val elements: Map<UtModel, UtModel>,
     override val utConstraints: Set<UtConstraint> = emptySet()
-) : UtConstraintModel(variable, utConstraints)
+) : UtConstraintModel(variable, utConstraints) {
+    val allConstraints get() = elements.toList().fold((length as UtConstraintModel).utConstraints) { acc, pair ->
+        acc + ((pair.first as? UtConstraintModel)?.utConstraints
+            ?: emptySet()) + ((pair.second as? UtConstraintModel)?.utConstraints ?: emptySet())
+    }
+}
 
 /**
  * Model for complex objects with assemble instructions.

diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/ConstraintApi.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/ConstraintApi.kt
@@ -425,6 +425,11 @@ data class UtOrConstraint(val lhv: UtConstraint, val rhv: UtConstraint) : UtPrim
     }
 }
 
+data class ConstrainedExecution(
+    val modelsBefore: List<UtModel>,
+    val modelsAfter: List<UtModel>
+)
+
 
 val ClassId.defaultVariable: UtConstraintVariable
     get() = when (this) {

diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ConstraintResolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ConstraintResolver.kt
@@ -4,6 +4,7 @@ import org.utbot.engine.MemoryState.CURRENT
 import org.utbot.engine.MemoryState.INITIAL
 import org.utbot.engine.MemoryState.STATIC_INITIAL
 import org.utbot.engine.pc.*
+import org.utbot.engine.z3.value
 import org.utbot.framework.plugin.api.*
 import org.utbot.framework.plugin.api.util.intClassId
 
@@ -58,7 +59,7 @@ class ConstraintResolver(
         }
     }
 
-    internal fun resolveModels(parameters: List<SymbolicValue>): ResolvedExecution {
+    internal fun resolveModels(parameters: List<SymbolicValue>): ConstrainedExecution {
         varBuilder = UtVarBuilder(holder, typeRegistry, typeResolver)
         val allAddresses = UtExprCollector { it is UtAddrExpression }.let {
             holder.constraints.hard.forEach { constraint -> constraint.accept(it) }
@@ -77,7 +78,7 @@ class ConstraintResolver(
             resolvedModels
         }
 
-        return ResolvedExecution(modelsBefore, modelsAfter, emptyList())
+        return ConstrainedExecution(modelsBefore.parameters, modelsAfter.parameters)
     }
 
     private fun internalResolveModel(
@@ -103,6 +104,7 @@ class ConstraintResolver(
             value.expr.variable,
             emptySet()
         )
+
         is ReferenceValue -> buildModel(
             collectAtoms(value, addrs),
             value.addr.variable,
@@ -143,9 +145,11 @@ class ConstraintResolver(
             variable,
             resolvedConstraints.getValue(variable.addr)
         )
+
         variable.isArray -> buildArrayModel(atoms, variable, aliases).also {
             resolvedConstraints[variable.addr] = it
         }
+
         else -> buildObjectModel(atoms, variable, aliases).also {
             resolvedConstraints[variable.addr] = it
         }
@@ -199,15 +203,20 @@ class ConstraintResolver(
         val lengths = atoms.flatMap { it.flatMap() }.filter {
             it is UtConstraintArrayLength && it.instance in allAliases
         }.toSet()
-        val lengthModel = buildModel(atoms, UtConstraintArrayLength(variable), lengths)
-
-        val indexMap = atoms.flatMap {
-            it.accept(UtConstraintVariableCollector { indx ->
-                indx is UtConstraintArrayAccess && indx.instance in allAliases
-            })
-        }.map { (it as UtConstraintArrayAccess).index }.groupBy {
-            holder.eval(varBuilder[it])
-        }.map { it.value.toSet() }
+        val lengthVariable = UtConstraintArrayLength(variable)
+        val lengthModel = buildModel(atoms, lengthVariable, lengths)
+        val concreteLength = holder.eval(lengths.first().expr).value() as Int
+
+        val indexMap = atoms
+            .flatMap {
+                it.accept(UtConstraintVariableCollector { indx ->
+                    indx is UtConstraintArrayAccess && indx.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() }
 
         var indexCount = 0
         val elements = indexMap.associate { indices ->
@@ -221,25 +230,25 @@ class ConstraintResolver(
             )
 
             val arrayAccess = UtConstraintArrayAccess(variable, indexVariable, elementClassId)
-            varBuilder.backMapping[arrayAccess] = varBuilder.backMapping[UtConstraintArrayAccess(variable, indices.first(), elementClassId)]!!
+            varBuilder.backMapping[arrayAccess] =
+                varBuilder.backMapping[UtConstraintArrayAccess(variable, indices.first(), elementClassId)]!!
             val indexAliases = indices.flatMap { idx ->
                 allAliases.map { UtConstraintArrayAccess(it, idx, elementClassId) }
             }.toSet()
             val res = buildModel(atoms, arrayAccess, indexAliases).withConstraints(
-                indices.map { UtEqConstraint(it, indexVariable) }.toSet()
+                indices.map { UtEqConstraint(it, indexVariable) }.toSet() + setOf(
+                    UtGeConstraint(indexVariable, UtConstraintNumericConstant(0)),
+                    UtLtConstraint(indexVariable, lengthVariable)
+                )
             )
             (indexModel as UtModel) to res
         }
 
-        val allConstraints = elements.toList().fold((lengthModel as UtConstraintModel).utConstraints) { acc, pair ->
-            acc + ((pair.first as? UtConstraintModel)?.utConstraints ?: emptySet()) + ((pair.second as? UtConstraintModel)?.utConstraints ?: emptySet())
-        }
-
         return UtArrayConstraintModel(
             variable,
             lengthModel,
             elements,
-            atoms
+            setOf()
         )
     }
 

diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt
@@ -3607,10 +3607,10 @@ class UtBotSymbolicEngine(
         }
 
         if (!isInNestedMethod()) {
-            val postConditionUpdates =
-                postConditionConstructor.constructPostCondition(this@UtBotSymbolicEngine, symbolicResult)
-            logger.error { "HARD POST CONDITION" }
-            logger.error { postConditionUpdates.hardConstraints.constraints.joinToString("\n") }
+            val postConditionUpdates = postConditionConstructor.constructPostCondition(
+                this@UtBotSymbolicEngine,
+                symbolicResult
+            )
             queuedSymbolicStateUpdates += postConditionUpdates
         }
 
@@ -3701,7 +3701,7 @@ class UtBotSymbolicEngine(
             instrumentation,
             entryMethodPath(),
             state.fullPath(),
-            hole = resolvedConstraints
+            constrainedExecution = resolvedConstraints
         )
 
         globalGraph.traversed(state)

diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/UtConstraintTransformer.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/UtConstraintTransformer.kt
@@ -154,7 +154,7 @@ class UtConstraintTransformer(
     }
 
     override fun visitUtRefNeqConstraint(expr: UtRefNeqConstraint) = with(expr) {
-        UtRefEqConstraint(
+        UtRefNeqConstraint(
             lhv.accept(this@UtConstraintTransformer),
             rhv.accept(this@UtConstraintTransformer)
         )

diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/plugin/api/UtBotTestCaseGenerator.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/plugin/api/UtBotTestCaseGenerator.kt
@@ -45,7 +45,6 @@ import mu.KotlinLogging
 import org.utbot.engine.*
 import org.utbot.engine.selectors.strategies.ScoringStrategyBuilder
 import org.utbot.framework.UtSettings.enableSynthesis
-import org.utbot.framework.modifications.StatementsStorage
 import org.utbot.framework.synthesis.ConstrainedSynthesizer
 import org.utbot.framework.synthesis.postcondition.constructors.EmptyPostCondition
 import org.utbot.framework.synthesis.postcondition.constructors.PostConditionConstructor
@@ -478,11 +477,8 @@ object UtBotTestCaseGenerator : TestCaseGenerator {
         map { execution ->
             val oldStateBefore = execution.stateBefore
 
-            System.err.println("-------------------------------")
-            System.err.println("CONSTRAINTS")
-            System.err.println((execution.hole as ResolvedExecution).modelsAfter)
-            System.err.println("-------------------------------")
-            val aa = ConstrainedSynthesizer((execution.hole as ResolvedExecution).modelsAfter)
+            val constrainedExecution = execution.constrainedExecution ?: return@map execution
+            val aa = ConstrainedSynthesizer(constrainedExecution.modelsAfter)
             val synthesizedModels = try {
                 aa.synthesize() ?: return@map execution
             } catch (e: Throwable) {

diff --git a/...ramework/src/main/kotlin/org/utbot/framework/synthesis/ConstrainedSynthesisUnitChecker.kt b/...ramework/src/main/kotlin/org/utbot/framework/synthesis/ConstrainedSynthesisUnitChecker.kt
@@ -7,6 +7,7 @@ import org.utbot.framework.UtSettings
 import org.utbot.framework.UtSettings.enableSynthesis
 import org.utbot.framework.plugin.api.MockStrategyApi
 import org.utbot.framework.plugin.api.UtBotTestCaseGenerator
+import org.utbot.framework.plugin.api.UtExecutionSuccess
 import org.utbot.framework.plugin.api.UtModel
 import org.utbot.framework.synthesis.postcondition.constructors.ConstraintBasedPostConditionConstructor
 import soot.SootClass
@@ -42,7 +43,7 @@ class ConstrainedSynthesisUnitChecker(
                     synthesisMethodContext
                 ),
                 scoringStrategy
-            ).firstOrNull().also {
+            ).firstOrNull { it.result is UtExecutionSuccess }.also {
                 enableSynthesis = true
             }
         } ?: return null

diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/ConstrainedSynthesizer.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/ConstrainedSynthesizer.kt
@@ -13,11 +13,9 @@ import org.utbot.framework.synthesis.postcondition.constructors.toSoot
 internal fun Collection<ClassId>.expandable() = filter { !it.isArray && !it.isPrimitive }.toSet()
 
 class ConstrainedSynthesizer(
-    models: ResolvedModels,
+    val parameters: List<UtModel>,
     val depth: Int = 4
 ) {
-    val parameters = models.parameters
-
     companion object {
         private val logger = KotlinLogging.logger("ConstrainedSynthesizer")
         private var attempts = 0

diff --git a/...framework/synthesis/postcondition/constructors/ConstraintBasedPostConditionConstructor.kt b/...framework/synthesis/postcondition/constructors/ConstraintBasedPostConditionConstructor.kt
@@ -8,7 +8,6 @@ import org.utbot.engine.symbolic.asSoftConstraint
 import org.utbot.framework.plugin.api.*
 import org.utbot.framework.plugin.api.UtConstraintParameter
 import org.utbot.framework.plugin.api.util.*
-import org.utbot.framework.synthesis.ArrayUnit
 import org.utbot.framework.synthesis.SynthesisMethodContext
 import org.utbot.framework.synthesis.SynthesisUnitContext
 import soot.ArrayType
@@ -64,6 +63,9 @@ class ConstraintBasedPostConditionConstructor(
                         addAll(buildPostCondition(element, builder, parameters, localVariableMemory))
                     }
                 }
+                for (constraint in model.utConstraints) {
+                    add(constraint.accept(builder))
+                }
                 add(mkEq(symbolicValue, model.variable.accept(builder)))
             }
             else -> error("Unknown model: ${model::class}")