working prototypes

utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt

@@ -335,6 +335,12 @@ object UtSettings {
      */
     var singleSelector by getBooleanProperty(true)
 
+
+    /**
+     * Flag for enabling model synthesis
+     */
+    var enableSynthesis = true
+
     override fun toString(): String =
         properties
             .entries

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

@@ -102,6 +102,7 @@ import org.utbot.framework.PathSelectorType
 import org.utbot.framework.UtSettings
 import org.utbot.framework.UtSettings.checkSolverTimeoutMillis
 import org.utbot.framework.UtSettings.enableFeatureProcess
+import org.utbot.framework.UtSettings.enableSynthesis
 import org.utbot.framework.UtSettings.pathSelectorStepsLimit
 import org.utbot.framework.UtSettings.pathSelectorType
 import org.utbot.framework.UtSettings.preferredCexOption
@@ -3684,12 +3685,14 @@ class UtBotSymbolicEngine(
         val stateAfter = modelsAfter.constructStateForMethod(state.executionStack.first().method)
         require(stateBefore.parameters.size == stateAfter.parameters.size)
 
-        val resolvedConstraints = ConstraintResolver(
-            updatedMemory,
-            holder,
-            typeRegistry,
-            typeResolver
-        ).run { resolveModels(resolvedParameters) }
+        val resolvedConstraints = if (enableSynthesis) {
+            ConstraintResolver(
+                updatedMemory,
+                holder,
+                typeRegistry,
+                typeResolver
+            ).run { resolveModels(resolvedParameters) }
+        } else null
 
         val symbolicUtExecution = UtExecution(
             stateBefore,

utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtVarBuilder.kt

@@ -4,49 +4,51 @@ import org.utbot.engine.*
 import org.utbot.engine.z3.intValue
 import org.utbot.framework.plugin.api.*
 import org.utbot.framework.plugin.api.UtConstraintParameter
-import org.utbot.framework.plugin.api.util.objectClassId
+import org.utbot.framework.plugin.api.util.*
 import soot.ArrayType
 import soot.PrimType
 import soot.RefType
 import soot.Type
 
 
-
 class UtVarBuilder(
     val holder: UtSolverStatusSAT,
     val typeRegistry: TypeRegistry,
     val typeResolver: TypeResolver,
 ) : UtExpressionVisitor<UtConstraintVariable> {
     private val internalAddrs = mutableMapOf<Address, UtConstraintVariable>()
 
-    override fun visit(expr: UtArraySelectExpression): UtConstraintVariable {
-        when (val array = expr.arrayExpression) {
-            is UtMkArrayExpression -> {
-                when (array.name) {
-                    "arraysLength" -> {
-                        val instance = expr.index.accept(this)
-                        return UtConstraintArrayLengthAccess(instance)
-                    }
-                    "RefValues_Arrays" -> {
-                        val instance = expr.index.accept(this)
-                        return instance
-                    }
-                    else -> {
-                        val (type, field) = array.name.split("_")
-                        val instance = expr.index.accept(this)
-                        return UtConstraintFieldAccess(instance, FieldId(ClassId(type), field))
-                    }
+    override fun visit(expr: UtArraySelectExpression): UtConstraintVariable = when (val array = expr.arrayExpression) {
+        is UtMkArrayExpression -> {
+            when (array.name) {
+                "arraysLength" -> {
+                    val instance = expr.index.accept(this)
+                    UtConstraintArrayLengthAccess(instance)
                 }
-            }
-            is UtArraySelectExpression -> when (val array2 = array.arrayExpression) {
-                is UtMkArrayExpression -> when (array2.name) {
-                    "RefValues_Arrays" -> return expr.index.accept(this)
-                    else -> error("Unexpected")
+                "RefValues_Arrays" -> {
+                    val instance = expr.index.accept(this)
+                    instance
+                }
+                else -> {
+                    val (type, field) = array.name.split("_")
+                    val instance = expr.index.accept(this)
+                    UtConstraintFieldAccess(instance, FieldId(ClassId(type), field))
                 }
+            }
+        }
+        is UtArraySelectExpression -> when (val array2 = array.arrayExpression) {
+            is UtMkArrayExpression -> when (array2.name) {
+                "RefValues_Arrays" -> expr.index.accept(this)
+                "int_Arrays" -> expr.index.accept(this)
                 else -> error("Unexpected")
             }
             else -> error("Unexpected")
         }
+        else -> {
+            val array2 = expr.arrayExpression.accept(this)
+            val index = expr.index.accept(this)
+            UtConstraintArrayAccess(array2, index, array2.classId.elementClassId!!)
+        }
     }
 
     override fun visit(expr: UtConstArrayExpression): UtConstraintVariable {
@@ -80,11 +82,17 @@ class UtVarBuilder(
 
     override fun visit(expr: UtAddrExpression): UtConstraintVariable {
         return when (val internal = expr.internal) {
-            is UtBvConst -> UtConstraintParameter((expr.internal as UtBvConst).name, holder.findBaseTypeOrNull(expr)?.classId ?: objectClassId)
+            is UtBvConst -> UtConstraintParameter(
+                (expr.internal as UtBvConst).name,
+                holder.findBaseTypeOrNull(expr)?.classId ?: objectClassId
+            )
             is UtBvLiteral -> when (internal.value) {
                 0 -> NullUtConstraintVariable(objectClassId)
                 else -> internalAddrs.getOrPut(internal.value.toInt()) {
-                    UtConstraintParameter("object${internal.value}", holder.findBaseTypeOrNull(expr)?.classId ?: objectClassId)
+                    UtConstraintParameter(
+                        "object${internal.value}",
+                        holder.findBaseTypeOrNull(expr)?.classId ?: objectClassId
+                    )
                 }
             }
             else -> expr.internal.accept(this)

utbot-framework/src/main/kotlin/org/utbot/framework/plugin/api/UtBotTestCaseGenerator.kt

@@ -44,6 +44,7 @@ import kotlinx.coroutines.yield
 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.Synthesizer
@@ -404,36 +405,39 @@ object UtBotTestCaseGenerator : TestCaseGenerator {
         method: UtMethod<*>,
         mockStrategy: MockStrategyApi,
     ): UtTestCase {
-        val executions = generateWithPostCondition(
-            method.toSootMethod(), mockStrategy, EmptyPostCondition, ScoringStrategyBuilder()
-        )
+        if (enableSynthesis) {
+            val executions = generateWithPostCondition(
+                method.toSootMethod(), mockStrategy, EmptyPostCondition, ScoringStrategyBuilder()
+            )
 
-        return UtTestCase(
-            method,
-            executions.toAssemble(),
-            jimpleBody(method),
-        )
-//        logger.trace { "UtSettings:${System.lineSeparator()}" + UtSettings.toString() }
-//
-//        if (isCanceled()) return UtTestCase(method)
-//
-//        val executions = mutableListOf<UtExecution>()
-//        val errors = mutableMapOf<String, Int>()
-//
-//
-//        runIgnoringCancellationException {
-//            runBlockingWithCancellationPredicate(isCanceled) {
-//                generateAsync(EngineController(), method.toSootMethod(), mockStrategy).collect {
-//                    when (it) {
-//                        is UtExecution -> executions += it
-//                        is UtError -> errors.merge(it.description, 1, Int::plus)
-//                    }
-//                }
-//            }
-//        }
-//
-//        val minimizedExecutions = minimizeExecutions(executions)
-//        return UtTestCase(method, minimizedExecutions, jimpleBody(method), errors)
+            return UtTestCase(
+                method,
+                executions.toAssemble(),
+                jimpleBody(method),
+            )
+        } else {
+            logger.trace { "UtSettings:${System.lineSeparator()}" + UtSettings.toString() }
+
+            if (isCanceled()) return UtTestCase(method)
+
+            val executions = mutableListOf<UtExecution>()
+            val errors = mutableMapOf<String, Int>()
+
+
+            runIgnoringCancellationException {
+                runBlockingWithCancellationPredicate(isCanceled) {
+                    generateAsync(EngineController(), method.toSootMethod(), mockStrategy).collect {
+                        when (it) {
+                            is UtExecution -> executions += it
+                            is UtError -> errors.merge(it.description, 1, Int::plus)
+                        }
+                    }
+                }
+            }
+
+            val minimizedExecutions = minimizeExecutions(executions)
+            return UtTestCase(method, minimizedExecutions, jimpleBody(method), errors)
+        }
     }
 
     private fun toAssembleModel(model: UtModel) = (model as? UtCompositeModel)?.let {
@@ -487,10 +491,10 @@ object UtBotTestCaseGenerator : TestCaseGenerator {
             System.err.println((execution.hole as ResolvedExecution).modelsAfter)
             System.err.println("-------------------------------")
             val aa = ConstrainedSynthesizer((execution.hole as ResolvedExecution).modelsAfter)
-            aa.synthesize()
+            val synthesizedModels = aa.synthesize() ?: return this
 
-            val newThisModel = oldStateBefore.thisInstance?.let { toAssembleModel(it) }
-            val newParameters = oldStateBefore.parameters.map { toAssembleModel(it) }
+            val newThisModel = oldStateBefore.thisInstance?.let { synthesizedModels.first() }
+            val newParameters = oldStateBefore.thisInstance?.let { synthesizedModels.drop(1) } ?: synthesizedModels
 
             execution.copy(
                 stateBefore = EnvironmentModels(

utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/ConstrainedJimpleMethodSynthesizer.kt

@@ -1,8 +1,10 @@
 package org.utbot.framework.synthesis
 
 import org.utbot.engine.*
+import org.utbot.engine.ConstraintResolver
 import org.utbot.framework.plugin.api.ConstructorId
 import org.utbot.framework.plugin.api.MethodId
+import org.utbot.framework.plugin.api.UtModel
 import org.utbot.framework.synthesis.postcondition.constructors.toSoot
 import org.utbot.framework.synthesis.postcondition.constructors.toSootType
 import soot.RefType
@@ -61,6 +63,11 @@ class ConstrainedJimpleMethodSynthesizer {
             }
         }
 
+        fun resolve(parameterModels: List<UtModel>): List<UtModel> {
+            val resolver = Resolver(parameterModels, rootUnits, unitToParameter)
+            return rootUnits.map { resolver.resolve(it) }
+        }
+
         private fun synthesizeUnit(unit: SynthesisUnit): JimpleLocal = when (unit) {
             is ObjectUnit -> synthesizeCompositeUnit(unit)
             is MethodUnit -> synthesizeMethodUnit(unit)

utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/ConstrainedSynthesisUnitChecker.kt

@@ -6,6 +6,7 @@ import org.utbot.engine.selectors.strategies.ScoringStrategyBuilder
 import org.utbot.engine.variable
 import org.utbot.framework.PathSelectorType
 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.UtModel
@@ -21,7 +22,7 @@ class ConstrainedSynthesisUnitChecker(
 
     var id = 0
 
-    fun tryGenerate(units: List<SynthesisUnit>, parameters: ResolvedModels): UtModel? {
+    fun tryGenerate(units: List<SynthesisUnit>, parameters: ResolvedModels): List<UtModel>? {
         if (units.any { !it.isFullyDefined() }) return null
 
         val context = synthesizer.synthesize(units)
@@ -35,6 +36,7 @@ class ConstrainedSynthesisUnitChecker(
             emptyMap()
         )
         val execution = withPathSelector(PathSelectorType.INHERITORS_SELECTOR) {
+            enableSynthesis = false
             UtBotTestCaseGenerator.generateWithPostCondition(
                 method,
                 MockStrategyApi.NO_MOCKS,
@@ -43,16 +45,14 @@ class ConstrainedSynthesisUnitChecker(
                     units.map { context.unitToParameter[it] },
                     units.map { context.unitToLocal[it]?.variable }),
                 scoringStrategy
-            ).firstOrNull()
+            ).firstOrNull().also {
+                enableSynthesis = true
+            }
         } ?: return null
 
 
         logger.error { execution }
-        return null
-//        return context.resolve(listOfNotNull(execution.stateBefore.thisInstance) + execution.stateBefore.parameters)
-//            .also {
-//                println("Method body:\n ${method.activeBody}")
-//            }
+        return context.resolve(listOfNotNull(execution.stateBefore.thisInstance) + execution.stateBefore.parameters)
     }
 
     private fun <T> withPathSelector(pathSelectorType: PathSelectorType, body: () -> T): T {

utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/ConstrainedSynthesizer.kt

@@ -5,17 +5,21 @@ import org.utbot.engine.ResolvedModels
 import org.utbot.engine.UtBotSymbolicEngine
 import org.utbot.framework.modifications.StatementsStorage
 import org.utbot.framework.plugin.api.*
+import org.utbot.framework.plugin.api.util.isArray
+import org.utbot.framework.plugin.api.util.isPrimitive
 import org.utbot.framework.plugin.api.util.objectClassId
 import org.utbot.framework.synthesis.postcondition.constructors.ConstraintBasedPostConditionConstructor
 import org.utbot.framework.synthesis.postcondition.constructors.toSoot
 
+internal fun Collection<ClassId>.expandable() = filter { !it.isArray && !it.isPrimitive }.toSet()
+
 class ConstrainedSynthesizer(
     val parameters: ResolvedModels,
     val depth: Int = 4
 ) {
     private val logger = KotlinLogging.logger("ConstrainedSynthesizer")
     private val statementStorage = StatementsStorage().also { storage ->
-        storage.update(parameters.parameters.map { it.classId }.toSet())
+        storage.update(parameters.parameters.map { it.classId }.expandable())
     }
 
     private val queue = MultipleSynthesisUnitQueue(
@@ -25,7 +29,7 @@ class ConstrainedSynthesizer(
     )
     private val unitChecker = ConstrainedSynthesisUnitChecker(objectClassId.toSoot())
 
-    fun synthesize(): UtModel? {
+    fun synthesize(): List<UtModel>? {
         while (!queue.isEmpty()) {
             val units = queue.poll()
             logger.debug { "Visiting state: $units" }

utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/JimpleMethodSynthesizer.kt

@@ -75,7 +75,7 @@ class JimpleMethodSynthesizer {
         }
 
         fun resolve(parameterModels: List<UtModel>): UtModel {
-            val resolver = Resolver(parameterModels, unitToParameter)
+            val resolver = Resolver(parameterModels, listOf(), unitToParameter)
             return resolver.resolve(rootUnit)
         }
 

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

@@ -1,18 +1,14 @@
 package org.utbot.framework.synthesis
 
 import org.utbot.engine.nextDefaultModelId
-import org.utbot.framework.plugin.api.ConstructorId
-import org.utbot.framework.plugin.api.MethodId
-import org.utbot.framework.plugin.api.UtAssembleModel
-import org.utbot.framework.plugin.api.UtExecutableCallModel
-import org.utbot.framework.plugin.api.UtModel
-import org.utbot.framework.plugin.api.UtStatementModel
+import org.utbot.framework.plugin.api.*
 import org.utbot.framework.util.nextModelName
 import java.util.IdentityHashMap
 
 class Resolver(
     parameterModels: List<UtModel>,
-    unitToParameter: IdentityHashMap<SynthesisUnit, SynthesisParameter>
+    val rootUnits: List<SynthesisUnit>,
+    unitToParameter: IdentityHashMap<SynthesisUnit, SynthesisParameter>,
 ) {
     private val unitToModel = IdentityHashMap<SynthesisUnit, UtModel>().apply {
         unitToParameter.toList().forEach { (it, parameter) -> this[it] = parameterModels[parameter.number] }
@@ -21,9 +17,10 @@ class Resolver(
 
     fun resolve(unit: SynthesisUnit): UtModel =
         when (unit) {
-            is MethodUnit -> resolveMethodUnit(unit)
+            is MethodUnit -> unitToModel.getOrPut(unit) { resolveMethodUnit(unit) }
             is ObjectUnit -> unitToModel[unit] ?: error("Can't map $unit")
-            else -> TODO()
+            is NullUnit -> UtNullModel(unit.classId)
+            is RefUnit -> resolve(rootUnits[unit.referenceParam])
         }
 
     private fun resolveMethodUnit(unit: MethodUnit): UtModel =

utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/StateProducer.kt

@@ -43,7 +43,7 @@ class CompositeUnitExpander(
             return emptyList()
         }
         if (objectUnit.classId !in statementsStorage.items.keys.map { it.classId }.toSet()) {
-            statementsStorage.update(setOf(objectUnit.classId))
+            statementsStorage.update(setOf(objectUnit.classId).expandable())
         }
         val mutators = findMutators(objectUnit.classId)
 

utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/SynthesisUnit.kt

@@ -2,6 +2,7 @@ package org.utbot.framework.synthesis
 
 import org.utbot.framework.plugin.api.ClassId
 import org.utbot.framework.plugin.api.ExecutableId
+import org.utbot.framework.plugin.api.util.isArray
 import org.utbot.framework.plugin.api.util.primitives
 
 sealed class SynthesisUnit {