Solver optimizations (#1265)

* 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 sootClass = (isConstraint.type as? RefType)?.sootClass
+
+ if (sootClass == utMockClass || sootClass == utOverrideMockClass) {
+ 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