squash constraint model synthesis

UnitTestBot · AbdullinAM · Sep 28, 2022 · Sep 28, 2022 · Sep 29, 2022 · Sep 29, 2022
commit 1175678f49ba52b8b61ee86d9fd7bc81a3649208
diff --git a/utbot-cli/src/main/kotlin/org/utbot/cli/GenerateTestsAbstractCommand.kt b/utbot-cli/src/main/kotlin/org/utbot/cli/GenerateTestsAbstractCommand.kt
@@ -222,10 +222,12 @@ abstract class GenerateTestsAbstractCommand(name: String, help: String) :
 
     protected fun saveToFile(snippet: String, outputPath: String?) =
         outputPath?.let {
-            Files.write(it.toPath(), listOf(snippet))
+            val path = it.toPath()
+            path.toFile().parentFile?.mkdirs()
+            Files.write(path, listOf(snippet))
         }
 
     protected fun now(): LocalDateTime = LocalDateTime.now()
 
     protected fun newline(): String = System.lineSeparator()
-}
+}
diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt
@@ -380,6 +380,28 @@ object UtSettings : AbstractSettings(
      */
     var ignoreStaticsFromTrustedLibraries by getBooleanProperty(true)
 
+    /**
+     * Flag for enabling model synthesis
+     */
+    var enableSynthesis by getBooleanProperty(false)
+
+    /**
+     * Flag for enabling model synthesis
+     */
+    var enableSynthesisCache by getBooleanProperty(true)
+
+    /**
+     * Timeout model synthesis
+     *
+     */
+    var synthesisTimeoutInMillis by getLongProperty(60000L)
+
+    /**
+     * Max depth for synthesis search
+     *
+     */
+    var synthesisMaxDepth by getIntProperty(10)
+
     /**
      * Use the sandbox in the concrete executor.
      *
@@ -439,7 +461,12 @@ enum class PathSelectorType {
     /**
      * [RandomPathSelector]
      */
-    RANDOM_PATH_SELECTOR
+    RANDOM_PATH_SELECTOR,
+
+    /**
+     * [ScoringPathSelector]
+     */
+    SCORING_PATH_SELECTOR
 }
 
 enum class TestSelectionStrategyType {

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
@@ -136,7 +136,8 @@ class UtSymbolicExecution(
     coverage: Coverage? = null,
     summary: List<DocStatement>? = null,
     testMethodName: String? = null,
-    displayName: String? = null
+    displayName: String? = null,
+    val constrainedExecution: ConstrainedExecution? = null
 ) : UtExecution(stateBefore, stateAfter, result, coverage, summary, testMethodName, displayName) {
     /**
      * By design the 'before' and 'after' states contain info about the same fields.
@@ -169,7 +170,12 @@ class UtSymbolicExecution(
         append(")")
     }
 
-    fun copy(stateAfter: EnvironmentModels, result: UtExecutionResult, coverage: Coverage): UtResult {
+    fun copy(
+        stateBefore: EnvironmentModels,
+        stateAfter: EnvironmentModels,
+        result: UtExecutionResult,
+        coverage: Coverage?,
+    ): UtExecution {
         return UtSymbolicExecution(
             stateBefore,
             stateAfter,
@@ -180,7 +186,8 @@ class UtSymbolicExecution(
             coverage,
             summary,
             testMethodName,
-            displayName
+            displayName,
+            constrainedExecution
         )
     }
 }
@@ -468,6 +475,80 @@ data class UtArrayModel(
     }
 }
 
+/**
+ * Models for values with constraints
+ */
+sealed class UtConstraintModel(
+    open val variable: UtConstraintVariable
+) : UtModel(variable.classId) {
+    abstract val utConstraints: Set<UtConstraint>
+}
+
+data class UtPrimitiveConstraintModel(
+    override val variable: UtConstraintVariable,
+    override val utConstraints: Set<UtConstraint>,
+    val concrete: Any? = null
+) : UtConstraintModel(variable) {
+}
+
+data class UtReferenceConstraintModel(
+    override val variable: UtConstraintVariable,
+    override val utConstraints: Set<UtConstraint>,
+) : UtConstraintModel(variable) {
+    fun isNull() = utConstraints.any {
+        it is UtRefEqConstraint && it.lhv == variable && it.rhv is UtConstraintNull
+    }
+}
+
+data class UtReferenceToConstraintModel(
+    override val variable: UtConstraintVariable,
+    val reference: UtModel,
+    override val utConstraints: Set<UtConstraint> = emptySet()
+) : UtConstraintModel(variable)
+
+sealed class UtElementContainerConstraintModel(
+    override val variable: UtConstraintVariable,
+    open val length: UtModel,
+    open val elements: Map<UtModel, UtModel>,
+    open val baseConstraints: Set<UtConstraint> = emptySet()
+) : UtConstraintModel(variable) {
+    final override val utConstraints: Set<UtConstraint> get() =
+        baseConstraints + elements.toList().fold((length as UtConstraintModel).utConstraints) { acc, pair ->
+            acc +
+                    ((pair.first as? UtConstraintModel)?.utConstraints ?: emptySet()) +
+                    ((pair.second as? UtConstraintModel)?.utConstraints ?: emptySet())
+        }
+}
+
+data class UtArrayConstraintModel(
+    override val variable: UtConstraintVariable,
+    override val length: UtModel,
+    override val elements: Map<UtModel, UtModel>,
+    override val baseConstraints: Set<UtConstraint> = emptySet()
+) : UtElementContainerConstraintModel(variable, length, elements)
+
+data class UtListConstraintModel(
+    override val variable: UtConstraintVariable,
+    override val length: UtModel,
+    override val elements: Map<UtModel, UtModel>,
+    override val baseConstraints: Set<UtConstraint> = emptySet()
+) : UtElementContainerConstraintModel(variable, length, elements)
+
+data class UtSetConstraintModel(
+    override val variable: UtConstraintVariable,
+    override val length: UtModel,
+    override val elements: Map<UtModel, UtModel>,
+    override val baseConstraints: Set<UtConstraint> = emptySet()
+) : UtElementContainerConstraintModel(variable, length, elements)
+
+data class UtMapConstraintModel(
+    override val variable: UtConstraintVariable,
+    override val length: UtModel,
+    override val elements: Map<UtModel, UtModel>,
+    override val baseConstraints: Set<UtConstraint> = emptySet()
+) : UtElementContainerConstraintModel(variable, length, elements)
+
+
 /**
  * Model for complex objects with assemble instructions.
  *

diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/IdUtil.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/IdUtil.kt
@@ -267,6 +267,7 @@ val atomicIntegerGetAndIncrement = MethodId(atomicIntegerClassId, "getAndIncreme
 
 val iterableClassId = java.lang.Iterable::class.id
 val mapClassId = java.util.Map::class.id
+val setClassId = java.util.Set::class.id
 
 val dateClassId = java.util.Date::class.id
 
@@ -357,6 +358,9 @@ val ClassId.isIterable: Boolean
 val ClassId.isMap: Boolean
     get() = isSubtypeOf(mapClassId)
 
+val ClassId.isSet: Boolean
+    get() = isSubtypeOf(setClassId)
+
 val ClassId.isIterableOrMap: Boolean
     get() = isIterable || isMap
 
@@ -540,4 +544,4 @@ fun builtinConstructorId(classId: BuiltinClassId, vararg arguments: ClassId): Bu
 
 fun builtinStaticMethodId(classId: ClassId, name: String, returnType: ClassId, vararg arguments: ClassId): BuiltinMethodId {
     return BuiltinMethodId(classId, name, returnType, arguments.toList(), isStatic = true)
-}
+}
diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/UtContext.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/UtContext.kt
@@ -51,7 +51,7 @@ class UtContext(val classLoader: ClassLoader) : ThreadContextElement<UtContext?>
         fun currentContext(): UtContext? = threadLocalContextHolder.get()
         fun setUtContext(context: UtContext): AutoCloseable = Cookie(context)
 
-        private fun restore(contextToRestore : UtContext?) {
+        private fun restore(contextToRestore: UtContext?) {
             if (contextToRestore != null) {
                 threadLocalContextHolder.set(contextToRestore)
             } else {

diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/JimpleCreation.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/JimpleCreation.kt
@@ -1,28 +1,47 @@
 package org.utbot.engine
 
+import soot.Local
+import soot.Modifier
+import soot.RefType
 import soot.SootClass
 import soot.SootMethod
 import soot.Type
 import soot.Unit
 import soot.Value
 import soot.jimple.AddExpr
+import soot.jimple.ArrayRef
 import soot.jimple.AssignStmt
+import soot.jimple.DynamicInvokeExpr
 import soot.jimple.GeExpr
 import soot.jimple.GotoStmt
 import soot.jimple.IdentityStmt
 import soot.jimple.IfStmt
 import soot.jimple.IntConstant
+import soot.jimple.InterfaceInvokeExpr
 import soot.jimple.InvokeExpr
 import soot.jimple.InvokeStmt
 import soot.jimple.Jimple
 import soot.jimple.JimpleBody
 import soot.jimple.NewArrayExpr
+import soot.jimple.NewExpr
 import soot.jimple.ParameterRef
 import soot.jimple.ReturnStmt
 import soot.jimple.ReturnVoidStmt
+import soot.jimple.SpecialInvokeExpr
 import soot.jimple.StaticInvokeExpr
+import soot.jimple.VirtualInvokeExpr
 
-fun SootMethod.toStaticInvokeExpr(): StaticInvokeExpr = Jimple.v().newStaticInvokeExpr(this.makeRef())
+fun SootMethod.toStaticInvokeExpr(parameters: List<Value> = emptyList()): StaticInvokeExpr =
+    Jimple.v().newStaticInvokeExpr(this.makeRef(), parameters)
+
+fun SootMethod.toSpecialInvoke(base: Local, parameters: List<Value> = emptyList()): SpecialInvokeExpr =
+    Jimple.v().newSpecialInvokeExpr(base, this.makeRef(), parameters)
+
+fun SootMethod.toVirtualInvoke(base: Local, parameters: List<Value> = emptyList()): VirtualInvokeExpr =
+    Jimple.v().newVirtualInvokeExpr(base, this.makeRef(), parameters)
+
+fun SootMethod.toInterfaceInvoke(base: Local, parameters: List<Value> = emptyList()): InterfaceInvokeExpr =
+    Jimple.v().newInterfaceInvokeExpr(base, this.makeRef(), parameters)
 
 fun InvokeExpr.toInvokeStmt(): InvokeStmt = Jimple.v().newInvokeStmt(this)
 
@@ -36,6 +55,10 @@ fun identityStmt(local: Value, identityRef: Value): IdentityStmt = Jimple.v().ne
 
 fun newArrayExpr(type: Type, size: Value): NewArrayExpr = Jimple.v().newNewArrayExpr(type, size)
 
+fun newArrayRef(base: Value, index: Value): ArrayRef = Jimple.v().newArrayRef(base, index)
+
+fun newExpr(type: RefType): NewExpr = Jimple.v().newNewExpr(type)
+
 fun assignStmt(variable: Value, rValue: Value): AssignStmt = Jimple.v().newAssignStmt(variable, rValue)
 
 fun intConstant(value: Int): IntConstant = IntConstant.v(value)
@@ -60,11 +83,15 @@ fun createSootMethod(
     argsTypes: List<Type>,
     returnType: Type,
     declaringClass: SootClass,
-    graphBody: JimpleBody
-) = SootMethod(name, argsTypes, returnType)
+    graphBody: JimpleBody,
+    isStatic: Boolean = false
+) = SootMethod(name, argsTypes, returnType, Modifier.STATIC.takeIf { isStatic } ?: 0)
     .also {
         it.declaringClass = declaringClass
+        if (declaringClass.declaresMethod(it.subSignature)) {
+            declaringClass.removeMethod(declaringClass.getMethod(it.subSignature))
+        }
         declaringClass.addMethod(it)
         graphBody.method = it
         it.activeBody = graphBody
-    }
+    }
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt
@@ -79,6 +79,7 @@ import soot.Scene
 import soot.ShortType
 import soot.SootClass
 import soot.SootField
+import soot.SootMethod
 import soot.Type
 import soot.VoidType
 import java.awt.color.ICC_ProfileRGB
@@ -118,7 +119,7 @@ class Resolver(
     val typeRegistry: TypeRegistry,
     private val typeResolver: TypeResolver,
     val holder: UtSolverStatusSAT,
-    methodUnderTest: ExecutableId,
+    packageName: String,
     private val softMaxArraySize: Int
 ) {
 
@@ -133,7 +134,7 @@ class Resolver(
     private val instrumentation = mutableListOf<UtInstrumentation>()
     private val requiredInstanceFields = mutableMapOf<Address, Set<FieldId>>()
 
-    private val assembleModelGenerator = AssembleModelGenerator(methodUnderTest.classId.packageName)
+    private val assembleModelGenerator = AssembleModelGenerator(packageName)
 
     /**
      * Contains FieldId of the static field which is construction at the moment and null of there is no such field.
@@ -1235,4 +1236,4 @@ private fun List<MockInfoEnriched>.mergeExecutables(): MockInfoEnriched {
     return mockInfoEnriched.copy(executables = methodToExecutables)
 }
 
-data class ResolvedModels(val parameters: List<UtModel>, val statics: Map<FieldId, UtModel>)
+data class ResolvedModels(val parameters: List<UtModel>, val statics: Map<FieldId, UtModel>)