Solver optimizations

Author: CaelmBleidd

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

@@ -395,6 +395,35 @@ object UtSettings : AbstractSettings(
      * therefore, you will be unable to test UtBot classes.
      */
     var removeUtBotClassesFromHierarchy by getBooleanProperty(true)
+
+    /**
+     * Use this option to enable calculation and logging of MD5 for dropped states by statistics.
+     * Example of such logging:
+     *     Dropping state (lastStatus=UNDEFINED) by the distance statistics. MD5: 5d0bccc242e87d53578ca0ef64aa5864
+     *
+     * Default value is false.
+     */
+    var enableLoggingForDroppedStates by getBooleanProperty(false)
+
+    /**
+     * If this option set in true, depending on the number of possible types for
+     * a particular object will be used either type system based on conjunction
+     * or on bit vectors.
+     *
+     * @see useBitVecBasedTypeSystem
+     */
+    var useBitVecBasedTypeSystem by getBooleanProperty(true)
+
+    /**
+     * The number of types on which the choice of the type system depends.
+     */
+    var maxTypeNumberForEnumeration by getIntProperty(64)
+
+    /**
+     * The threshold for numbers of types for which they will be encoded into solver.
+     * It is used to do not encode big type storages due to significand performance degradation.
+     */
+    var maxNumberOfTypesToEncode by getIntProperty(512)
 }
 
 /**

utbot-framework-test/src/test/kotlin/org/utbot/examples/arrays/ArrayOfArraysTest.kt

@@ -1,5 +1,6 @@
 package org.utbot.examples.arrays
 
+import org.junit.jupiter.api.Disabled
 import org.utbot.tests.infrastructure.UtValueTestCaseChecker
 import org.utbot.tests.infrastructure.DoNotCalculate
 import org.utbot.tests.infrastructure.atLeast
@@ -268,10 +269,13 @@ internal class ArrayOfArraysTest : UtValueTestCaseChecker(testClass = ArrayOfArr
     }
 
     @Test
+    @Disabled("https://github.com/UnitTestBot/UTBotJava/issues/1267")
     fun testArrayWithItselfAnAsElement() {
         check(
             ArrayOfArrays::arrayWithItselfAnAsElement,
             eq(2),
+            { a, r -> a !== a[0] && r == null },
+            { a, r -> a === a[0] && a.contentDeepEquals(r) },
             coverage = atLeast(percents = 94)
             // because of the assumption
         )

utbot-framework-test/src/test/kotlin/org/utbot/examples/mixed/PrivateConstructorExampleTest.kt

@@ -3,9 +3,24 @@ package org.utbot.examples.mixed
 import org.utbot.tests.infrastructure.UtValueTestCaseChecker
 import org.utbot.tests.infrastructure.DoNotCalculate
 import org.junit.jupiter.api.Test
+import org.utbot.framework.plugin.api.CodegenLanguage
 import org.utbot.testcheckers.eq
+import org.utbot.tests.infrastructure.Compilation
 
-internal class PrivateConstructorExampleTest : UtValueTestCaseChecker(testClass = PrivateConstructorExample::class) {
+// TODO parameterized tests disabled due to https://github.com/UnitTestBot/UTBotJava/issues/1266
+internal class PrivateConstructorExampleTest : UtValueTestCaseChecker(
+    testClass = PrivateConstructorExample::class,
+    pipelines = listOf(
+        TestLastStage(
+            CodegenLanguage.JAVA,
+            parameterizedModeLastStage = Compilation
+        ),
+        TestLastStage(
+            CodegenLanguage.KOTLIN,
+            parameterizedModeLastStage = Compilation
+        )
+    )
+) {
 
     /**
      * Two branches need to be covered:

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

@@ -18,6 +18,8 @@ import org.utbot.engine.pc.mkInt
 import org.utbot.engine.pc.select
 import org.utbot.engine.pc.store
 import org.utbot.engine.symbolic.asHardConstraint
+import org.utbot.engine.types.OBJECT_TYPE
+import org.utbot.engine.types.TypeRegistry
 import org.utbot.framework.plugin.api.ClassId
 import org.utbot.framework.plugin.api.UtArrayModel
 import org.utbot.framework.plugin.api.UtCompositeModel

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

@@ -1,5 +1,7 @@
 package org.utbot.engine
 
+import org.utbot.engine.types.OBJECT_TYPE
+import org.utbot.engine.types.STRING_TYPE
 import soot.ArrayType
 import soot.IntType
 import soot.PrimType

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

@@ -1,16 +1,18 @@
 package org.utbot.engine
 
-import org.utbot.common.WorkaroundReason
-import org.utbot.common.workaround
-import org.utbot.engine.TypeRegistry.Companion.objectTypeStorage
+import org.utbot.api.mock.UtMock
+import org.utbot.engine.overrides.UtOverrideMock
+import org.utbot.engine.types.TypeRegistry.Companion.objectTypeStorage
 import org.utbot.engine.pc.UtAddrExpression
 import org.utbot.engine.pc.UtBoolExpression
+import org.utbot.engine.pc.UtFalse
 import org.utbot.engine.pc.UtInstanceOfExpression
 import org.utbot.engine.pc.UtIsExpression
 import org.utbot.engine.pc.UtTrue
 import org.utbot.engine.pc.mkAnd
 import org.utbot.engine.pc.mkOr
 import org.utbot.engine.symbolic.*
+import org.utbot.engine.types.TypeResolver
 import org.utbot.framework.plugin.api.FieldId
 import org.utbot.framework.plugin.api.UtInstrumentation
 import soot.RefType
@@ -125,6 +127,9 @@ class TypeStorage private constructor(val leastCommonType: Type, val possibleCon
         "(leastCommonType=$leastCommonType, ${possibleConcreteTypes.size} possibleTypes=${possibleConcreteTypes.take(10)})"
     }
 
+    operator fun component1(): Type = leastCommonType
+    operator fun component2(): Set<Type> = possibleConcreteTypes
+
     companion object {
         /**
          * Constructs a type storage with particular leastCommonType and set of possibleConcreteTypes.
@@ -307,7 +312,16 @@ data class TypeConstraint(
     /**
      * Returns a conjunction of the [isConstraint] and [correctnessConstraint]. Suitable for an object creation.
      */
-    fun all(): UtBoolExpression = mkAnd(isOrNullConstraint(), correctnessConstraint)
+    fun all(): UtBoolExpression {
+        // There is no need in constraint for UtMock and UtOverrideMock instances
+        val className = (isConstraint.type as? RefType)?.sootClass?.toString()
+
+        if (className == utMockClassName || className == utOverrideMockClassName) {
+            return UtTrue
+        }
+
+        return mkAnd(isOrNullConstraint(), correctnessConstraint)
+    }
 
     /**
      * Returns a condition that either the object is an instance of the types in [isConstraint], or it is null.
@@ -319,7 +333,13 @@ data class TypeConstraint(
      * For example, it is suitable for instanceof checks or negation of equality with some types.
      * NOTE: for Object we always return UtTrue.
      */
-    fun isConstraint(): UtBoolExpression = if (isConstraint.typeStorage.isObjectTypeStorage()) UtTrue else isConstraint
+    fun isConstraint(): UtBoolExpression {
+        if (isConstraint.typeStorage.possibleConcreteTypes.isEmpty()) {
+            return UtFalse
+        }
+
+        return if (isConstraint.typeStorage.isObjectTypeStorage()) UtTrue else isConstraint
+    }
 
     override fun hashCode(): Int = this.hashcode
 
@@ -344,3 +364,6 @@ data class TypeConstraint(
  * should be initialized. We don't need to initialize fields that are not accessed in the method being tested.
  */
 data class InstanceFieldReadOperation(val addr: UtAddrExpression, val fieldId: FieldId)
+
+private val utMockClassName: String = UtMock::class.java.name
+private val utOverrideMockClassName: String = UtOverrideMock::class.java.name

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

@@ -18,7 +18,6 @@ import soot.SootMethod
 import soot.jimple.Stmt
 import java.util.Objects
 import org.utbot.engine.symbolic.Assumption
-import org.utbot.framework.plugin.api.UtSymbolicExecution
 
 const val RETURN_DECISION_NUM = -1
 const val CALL_DECISION_NUM = -2

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

@@ -14,7 +14,6 @@ import org.utbot.engine.pc.UtFp32Sort
 import org.utbot.engine.pc.UtFp64Sort
 import org.utbot.engine.pc.UtIntSort
 import org.utbot.engine.pc.UtLongSort
-import org.utbot.engine.pc.UtSeqSort
 import org.utbot.engine.pc.UtShortSort
 import org.utbot.engine.pc.UtSolverStatusKind
 import org.utbot.engine.pc.UtSolverStatusSAT
@@ -67,6 +66,7 @@ import java.util.Queue
 import java.util.concurrent.ConcurrentHashMap
 import kotlinx.collections.immutable.PersistentMap
 import kotlinx.collections.immutable.persistentHashMapOf
+import org.utbot.engine.types.OBJECT_TYPE
 
 val JIdentityStmt.lines: String
     get() = tags.joinToString { "$it" }

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

@@ -1,5 +1,6 @@
 package org.utbot.engine
 
+import org.utbot.engine.types.TypeRegistry
 import org.utbot.framework.plugin.api.ClassId
 import org.utbot.framework.plugin.api.id
 import soot.RefType