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 index ad0abba414..936ea631b7 100644 --- a/utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt +++ b/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) } /** diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/examples/arrays/ArrayOfArraysTest.kt b/utbot-framework-test/src/test/kotlin/org/utbot/examples/arrays/ArrayOfArraysTest.kt index 1ffe1baf69..0e63fec970 100644 --- a/utbot-framework-test/src/test/kotlin/org/utbot/examples/arrays/ArrayOfArraysTest.kt +++ b/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 ) diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/examples/mixed/PrivateConstructorExampleTest.kt b/utbot-framework-test/src/test/kotlin/org/utbot/examples/mixed/PrivateConstructorExampleTest.kt index 6884cb0d09..7cda4f638a 100644 --- a/utbot-framework-test/src/test/kotlin/org/utbot/examples/mixed/PrivateConstructorExampleTest.kt +++ b/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: diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ArrayObjectWrappers.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ArrayObjectWrappers.kt index 533ce540bf..855e98de83 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/ArrayObjectWrappers.kt +++ b/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 diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ConstructedSootMethods.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ConstructedSootMethods.kt index 5cd7db37d3..67a5e89e45 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/ConstructedSootMethods.kt +++ b/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 diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt index 3621b7d7a3..8c964717ce 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt +++ b/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 = 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 \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt index 998ab1bbb1..4adba75615 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt +++ b/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 diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt index 1ae6418cec..b958d1650f 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt +++ b/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" } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Hierarchy.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Hierarchy.kt index c610ab822c..9265fa8dba 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Hierarchy.kt +++ b/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 diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt index 8c39a326ec..ef92b7a419 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt @@ -1,8 +1,5 @@ package org.utbot.engine -import com.google.common.collect.HashBiMap -import org.utbot.common.WorkaroundReason.MAKE_SYMBOLIC -import org.utbot.common.workaround import org.utbot.engine.MemoryState.CURRENT import org.utbot.engine.MemoryState.INITIAL import org.utbot.engine.MemoryState.STATIC_INITIAL @@ -12,38 +9,24 @@ import org.utbot.engine.pc.UtAddrSort import org.utbot.engine.pc.UtArrayExpressionBase import org.utbot.engine.pc.UtArraySelectExpression import org.utbot.engine.pc.UtArraySort -import org.utbot.engine.pc.UtBoolExpression import org.utbot.engine.pc.UtBoolSort import org.utbot.engine.pc.UtConstArrayExpression -import org.utbot.engine.pc.UtEqGenericTypeParametersExpression import org.utbot.engine.pc.UtExpression import org.utbot.engine.pc.UtFalse -import org.utbot.engine.pc.UtGenericExpression import org.utbot.engine.pc.UtInt32Sort import org.utbot.engine.pc.UtIntSort -import org.utbot.engine.pc.UtIsExpression -import org.utbot.engine.pc.UtIsGenericTypeExpression import org.utbot.engine.pc.UtMkArrayExpression import org.utbot.engine.pc.UtMkTermArrayExpression import org.utbot.engine.pc.UtSeqSort import org.utbot.engine.pc.UtSort import org.utbot.engine.pc.UtTrue -import org.utbot.engine.pc.mkAnd import org.utbot.engine.pc.mkArrayConst -import org.utbot.engine.pc.mkArrayWithConst -import org.utbot.engine.pc.mkEq import org.utbot.engine.pc.mkInt -import org.utbot.engine.pc.mkNot -import org.utbot.engine.pc.mkOr import org.utbot.engine.pc.select import org.utbot.engine.pc.store import org.utbot.engine.pc.toSort -import org.utbot.engine.symbolic.asHardConstraint import org.utbot.framework.plugin.api.ClassId import org.utbot.framework.plugin.api.FieldId -import java.math.BigInteger -import java.util.concurrent.atomic.AtomicInteger -import java.util.concurrent.atomic.AtomicLong import kotlinx.collections.immutable.ImmutableCollection import kotlinx.collections.immutable.PersistentList import kotlinx.collections.immutable.PersistentMap @@ -55,24 +38,15 @@ import kotlinx.collections.immutable.persistentListOf import kotlinx.collections.immutable.persistentSetOf import kotlinx.collections.immutable.toPersistentList import kotlinx.collections.immutable.toPersistentMap +import org.utbot.engine.types.STRING_TYPE +import org.utbot.engine.types.SeqType import org.utbot.framework.plugin.api.classId import soot.ArrayType -import soot.BooleanType -import soot.ByteType import soot.CharType -import soot.DoubleType -import soot.FloatType import soot.IntType -import soot.LongType import soot.RefLikeType -import soot.RefType import soot.Scene -import soot.ShortType -import soot.SootClass -import soot.SootField -import soot.SootMethod import soot.Type -import soot.tagkit.AnnotationClassElem /** @@ -356,584 +330,6 @@ data class Memory( // TODO: split purely symbolic memory and information about s symbolicEnumValues.filter { it.type.classId == classId } } -/** - * Types/classes registry. - * - * Registers and keeps two mappings: - * - Type <-> unique type id (int) - * - Object address -> to type id - */ -class TypeRegistry { - init { - // initializes type storage for OBJECT_TYPE from current scene - objectTypeStorage = TypeStorage.constructTypeStorageUnsafe( - OBJECT_TYPE, - Scene.v().classes.mapTo(mutableSetOf()) { it.type } - ) - } - - private val typeIdBiMap = HashBiMap.create() - - // A cache for strings representing bit-vectors for some collection of types. - private val typesToBitVecString = mutableMapOf, String>() - private val typeToRating = mutableMapOf() - private val typeToInheritorsTypes = mutableMapOf>() - private val typeToAncestorsTypes = mutableMapOf>() - - /** - * Contains types storages for type parameters of object by its address. - */ - private val genericTypeStorageByAddr = mutableMapOf>() - - // A BiMap containing bijection from every type to an address of the object - // presenting its classRef and vise versa - private val classRefBiMap = HashBiMap.create() - - /** - * Contains mapping from a class to the class containing substitutions for its methods. - */ - private val targetToSubstitution: Map by lazy { - val classesWithTargets = Scene.v().classes.mapNotNull { clazz -> - val annotation = clazz.findMockAnnotationOrNull - ?.elems - ?.singleOrNull { it.name == "target" } as? AnnotationClassElem - - val classNameFromSignature = classBytecodeSignatureToClassNameOrNull(annotation?.desc) - - if (classNameFromSignature == null) { - null - } else { - val target = Scene.v().getSootClass(classNameFromSignature) - target to clazz - } - } - classesWithTargets.toMap() - } - - /** - * Contains mapping from a class with substitutions of the methods of the target class to the target class itself. - */ - private val substitutionToTarget: Map by lazy { - targetToSubstitution.entries.associate { (k, v) -> v to k } - } - - private val typeToFields = mutableMapOf>() - - /** - * An array containing information about whether the object with particular addr could throw a [ClassCastException]. - * - * Note: all objects can throw it by default. - * @see disableCastClassExceptionCheck - */ - private var isClassCastExceptionAllowed: UtArrayExpressionBase = - mkArrayWithConst(UtArraySort(UtAddrSort, UtBoolSort), UtTrue) - - - /** - * Contains information about types for ReferenceValues. - * An element on some position k contains information about type for an object with address == k - * Each element in addrToTypeId is in range [1..numberOfTypes] - */ - private val addrToTypeId: UtArrayExpressionBase by lazy { - mkArrayConst( - "addrToTypeId", - UtAddrSort, - UtInt32Sort - ) - } - - private val genericAddrToTypeArrays = mutableMapOf() - - private fun genericAddrToType(i: Int) = genericAddrToTypeArrays.getOrPut(i) { - mkArrayConst( - "genericAddrToTypeId_$i", - UtAddrSort, - UtInt32Sort - ) - } - - /** - * Contains information about number of dimensions for ReferenceValues. - */ - private val addrToNumDimensions: UtArrayExpressionBase by lazy { - mkArrayConst( - "addrToNumDimensions", - UtAddrSort, - UtInt32Sort - ) - } - - private val genericAddrToNumDimensionsArrays = mutableMapOf() - - private fun genericAddrToNumDimensions(i: Int) = genericAddrToNumDimensionsArrays.getOrPut(i) { - mkArrayConst( - "genericAddrToNumDimensions_$i", - UtAddrSort, - UtInt32Sort - ) - } - - /** - * Contains information about whether the object with some addr is a mock or not. - */ - private val isMockArray: UtArrayExpressionBase by lazy { - mkArrayConst( - "isMock", - UtAddrSort, - UtBoolSort - ) - } - - /** - * Takes information about whether the object with [addr] is mock or not. - * - * @see isMockArray - */ - fun isMock(addr: UtAddrExpression) = isMockArray.select(addr) - - /** - * Makes the numbers of dimensions for every object in the program equal to zero by default - */ - fun softZeroNumDimensions() = UtMkTermArrayExpression(addrToNumDimensions) - - /** - * addrToTypeId is created as const array of the emptyType. If such type occurs anywhere in the program, it means - * we haven't touched the element that this type belongs to - * @see emptyTypeId - */ - fun softEmptyTypes() = UtMkTermArrayExpression(addrToTypeId, mkInt(emptyTypeId)) - - /** - * Calculates type 'rating' for a particular type. Used for ordering ObjectValue's possible types. - * The type with a higher rating is more likely than the one with a lower rating. - */ - fun findRating(type: RefType) = typeToRating.getOrPut(type) { - var finalCost = 0 - - val sootClass = type.sootClass - - // TODO: let's have "preferred types" - if (sootClass.name == "java.util.ArrayList") finalCost += 4096 - if (sootClass.name == "java.util.LinkedList") finalCost += 2048 - if (sootClass.name == "java.util.HashMap") finalCost += 4096 - if (sootClass.name == "java.util.TreeMap") finalCost += 2048 - if (sootClass.name == "java.util.HashSet") finalCost += 2048 - if (sootClass.name == "java.lang.Integer") finalCost += 8192 - if (sootClass.name == "java.lang.Character") finalCost += 8192 - if (sootClass.name == "java.lang.Double") finalCost += 8192 - if (sootClass.name == "java.lang.Long") finalCost += 8192 - - if (sootClass.packageName.startsWith("java.lang")) finalCost += 1024 - - if (sootClass.packageName.startsWith("java.util")) finalCost += 512 - - if (sootClass.packageName.startsWith("java")) finalCost += 128 - - if (sootClass.isPublic) finalCost += 16 - - if (sootClass.isPrivate) finalCost += -16 - - if ("blocking" in sootClass.name.toLowerCase()) finalCost -= 32 - - if (sootClass.type.isJavaLangObject()) finalCost += -32 - - if (sootClass.isAnonymous) finalCost += -128 - - if (sootClass.name.contains("$")) finalCost += -4096 - - if (sootClass.type.sootClass.isInappropriate) finalCost += -8192 - - finalCost - } - - private val classRefCounter = AtomicInteger(classRefAddrsInitialValue) - private fun nextClassRefAddr() = UtAddrExpression(classRefCounter.getAndIncrement()) - - private val symbolicReturnNameCounter = AtomicLong(symbolicReturnNameCounterInitialValue) - fun findNewSymbolicReturnValueName() = - workaround(MAKE_SYMBOLIC) { "symbolicReturnValue\$${symbolicReturnNameCounter.incrementAndGet()}" } - - private val typeCounter = AtomicInteger(typeCounterInitialValue) - private fun nextTypeId() = typeCounter.getAndIncrement() - - /** - * Returns unique typeId for the given type - */ - fun findTypeId(type: Type): Int = typeIdBiMap.getOrPut(type) { nextTypeId() } - - /** - * Returns type for the given typeId - * - * @return If there is such typeId in the program, returns the corresponding type, otherwise returns null - */ - fun typeByIdOrNull(typeId: Int): Type? = typeIdBiMap.getByValue(typeId) - - /** - * Returns symbolic representation for a typeId corresponding to the given address - */ - fun symTypeId(addr: UtAddrExpression) = addrToTypeId.select(addr) - - /** - * Returns a symbolic representation for an [i]th type parameter - * corresponding to the given address - */ - fun genericTypeId(addr: UtAddrExpression, i: Int) = genericAddrToType(i).select(addr) - - /** - * Returns symbolic representation for a number of dimensions corresponding to the given address - */ - fun symNumDimensions(addr: UtAddrExpression) = addrToNumDimensions.select(addr) - - fun genericNumDimensions(addr: UtAddrExpression, i: Int) = genericAddrToNumDimensions(i).select(addr) - - /** - * Returns a constraint stating that number of dimensions for the given address is zero - */ - fun zeroDimensionConstraint(addr: UtAddrExpression) = mkEq(symNumDimensions(addr), mkInt(objectNumDimensions)) - - /** - * Constructs a binary bit-vector by the given types with length 'numberOfTypes'. Each position - * corresponding to one of the typeId. - * - * @param types the collection of possible type - * @return decimal string representing the binary bit-vector - */ - fun constructBitVecString(types: Collection) = typesToBitVecString.getOrPut(types) { - val initialValue = BigInteger(ByteArray(numberOfTypes) { 0 }) - - return types.fold(initialValue) { acc, type -> - val typeId = if (type is ArrayType) findTypeId(type.baseType) else findTypeId(type) - acc.setBit(typeId) - }.toString() - } - - /** - * Creates class reference, i.e. Class<Integer> - * - * Note: Uses type id as an address to have the one and the same class reference for all objects of one class - */ - fun createClassRef(baseType: Type, numDimensions: Int = 0): MethodResult { - val addr = classRefBiMap.getOrPut(baseType) { nextClassRefAddr() } - - val classRefTypeStorage = TypeStorage.constructTypeStorageWithSingleType(CLASS_REF_TYPE) - val objectValue = ObjectValue(objectTypeStorage, addr) - - val typeConstraint = typeConstraint(addr, classRefTypeStorage).all() - - val typeId = mkInt(findTypeId(baseType)) - val symNumDimensions = mkInt(numDimensions) - - val stores = persistentListOf( - simplifiedNamedStore(CLASS_REF_TYPE_DESCRIPTOR, addr, typeId), - simplifiedNamedStore(CLASS_REF_NUM_DIMENSIONS_DESCRIPTOR, addr, symNumDimensions) - ) - - val touchedDescriptors = persistentSetOf(CLASS_REF_TYPE_DESCRIPTOR, CLASS_REF_NUM_DIMENSIONS_DESCRIPTOR) - - val memoryUpdate = MemoryUpdate(stores = stores, touchedChunkDescriptors = touchedDescriptors) - - return MethodResult(objectValue, typeConstraint.asHardConstraint(), memoryUpdates = memoryUpdate) - } - - /** - * Returns a list of inheritors for the given [type], including itself. - */ - fun findInheritorsIncludingTypes(type: RefType, defaultValue: () -> Set) = - typeToInheritorsTypes.getOrPut(type, defaultValue) - - /** - * Returns a list of ancestors for the given [type], including itself. - */ - fun findAncestorsIncludingTypes(type: RefType, defaultValue: () -> Set) = - typeToAncestorsTypes.getOrPut(type, defaultValue) - - fun findFields(type: RefType, defaultValue: () -> List) = - typeToFields.getOrPut(type, defaultValue) - - /** - * Returns a [TypeConstraint] instance for the given [addr] and [typeStorage]. - */ - fun typeConstraint(addr: UtAddrExpression, typeStorage: TypeStorage): TypeConstraint = - TypeConstraint( - constructIsExpression(addr, typeStorage), - mkEq(addr, nullObjectAddr), - constructCorrectnessConstraint(addr, typeStorage) - ) - - private fun constructIsExpression(addr: UtAddrExpression, typeStorage: TypeStorage): UtIsExpression = - UtIsExpression(addr, typeStorage, numberOfTypes) - - /** - * Returns a conjunction of the constraints responsible for the type construction: - * * typeId must be in range [[emptyTypeId]..[numberOfTypes]]; - * * numDimensions must be in range [0..[MAX_NUM_DIMENSIONS]]; - * * if the baseType for [TypeStorage.leastCommonType] is a [java.lang.Object], - * should be added constraints for primitive arrays to prevent - * impossible resolved types: Object[] must be at least primType[][]. - */ - private fun constructCorrectnessConstraint(addr: UtAddrExpression, typeStorage: TypeStorage): UtBoolExpression { - val symType = symTypeId(addr) - val symNumDimensions = symNumDimensions(addr) - val type = typeStorage.leastCommonType - - val constraints = mutableListOf() - - // add constraints for typeId, it must be in 0..numberOfTypes - constraints += Ge(symType.toIntValue(), emptyTypeId.toPrimitiveValue()) - constraints += Le(symType.toIntValue(), numberOfTypes.toPrimitiveValue()) - - // add constraints for number of dimensions, it must be in 0..MAX_NUM_DIMENSIONS - constraints += Ge(symNumDimensions.toIntValue(), 0.toPrimitiveValue()) - constraints += Le(symNumDimensions.toIntValue(), MAX_NUM_DIMENSIONS.toPrimitiveValue()) - - // add constraints for object and arrays of primitives - if (type.baseType.isJavaLangObject()) { - primTypes.forEach { - val typesAreEqual = mkEq(symType, mkInt(findTypeId(it))) - val numDimensions = Gt(symNumDimensions.toIntValue(), type.numDimensions.toPrimitiveValue()) - constraints += mkOr(mkNot(typesAreEqual), numDimensions) - } - } - - // there are no arrays of anonymous classes - typeStorage.possibleConcreteTypes - .mapNotNull { (it.baseType as? RefType) } - .filter { it.sootClass.isAnonymous } - .forEach { - val typesAreEqual = mkEq(symType, mkInt(findTypeId(it))) - val numDimensions = mkEq(symNumDimensions.toIntValue(), mkInt(objectNumDimensions).toIntValue()) - constraints += mkOr(mkNot(typesAreEqual), numDimensions) - } - - return mkAnd(constraints) - } - - /** - * returns constraint representing, that object with address [addr] is parametrized by [types] type parameters. - * @see UtGenericExpression - */ - fun genericTypeParameterConstraint(addr: UtAddrExpression, types: List) = - UtGenericExpression(addr, types, numberOfTypes) - - /** - * returns constraint representing that type parameters of an object with address [firstAddr] are equal to - * type parameters of an object with address [secondAddr], corresponding to [indexInjection] - * @see UtEqGenericTypeParametersExpression - */ - @Suppress("unused") - fun eqGenericTypeParametersConstraint( - firstAddr: UtAddrExpression, - secondAddr: UtAddrExpression, - vararg indexInjection: Pair - ): UtEqGenericTypeParametersExpression { - setParameterTypeStoragesEquality(firstAddr, secondAddr, indexInjection) - - return UtEqGenericTypeParametersExpression(firstAddr, secondAddr, mapOf(*indexInjection)) - } - - /** - * returns constraint representing that type parameters of an object with address [firstAddr] are equal to - * the corresponding type parameters of an object with address [secondAddr] - * @see UtEqGenericTypeParametersExpression - */ - fun eqGenericTypeParametersConstraint( - firstAddr: UtAddrExpression, - secondAddr: UtAddrExpression, - parameterSize: Int - ) : UtEqGenericTypeParametersExpression { - val injections = Array(parameterSize) { it to it } - - return eqGenericTypeParametersConstraint(firstAddr, secondAddr, *injections) - } - - /** - * returns constraint representing that the first type parameter of an object with address [firstAddr] are equal to - * the first type parameter of an object with address [secondAddr] - * @see UtEqGenericTypeParametersExpression - */ - fun eqGenericSingleTypeParameterConstraint(firstAddr: UtAddrExpression, secondAddr: UtAddrExpression) = - eqGenericTypeParametersConstraint(firstAddr, secondAddr, 0 to 0) - - /** - * Associates provided [typeStorages] with an object with the provided [addr]. - */ - fun saveObjectParameterTypeStorages(addr: UtAddrExpression, typeStorages: List) { - genericTypeStorageByAddr += addr to typeStorages - } - - /** - * Retrieves parameter type storages of an object with the given [addr] if present, or null otherwise. - */ - fun getTypeStoragesForObjectTypeParameters(addr: UtAddrExpression): List? = genericTypeStorageByAddr[addr] - - /** - * Set types storages for [firstAddr]'s type parameters equal to type storages for [secondAddr]'s type parameters - * according to provided types injection represented by [indexInjection]. - */ - private fun setParameterTypeStoragesEquality( - firstAddr: UtAddrExpression, - secondAddr: UtAddrExpression, - indexInjection: Array> - ) { - val existingGenericTypes = genericTypeStorageByAddr[secondAddr] ?: return - - val currentGenericTypes = mutableMapOf() - - indexInjection.forEach { (from, to) -> - require(from >= 0 && from < existingGenericTypes.size) { - "Type injection is out of bounds: should be in [0; ${existingGenericTypes.size}) but is $from" - } - - currentGenericTypes[to] = existingGenericTypes[from] - } - - genericTypeStorageByAddr[firstAddr] = currentGenericTypes - .entries - .sortedBy { it.key } - .mapTo(mutableListOf()) { it.value } - } - - /** - * Returns constraint representing that an object with address [addr] has the same type as the type parameter - * with index [i] of an object with address [baseAddr]. - * - * For a SomeCollection the type parameters are [A, B], where A and B are type variables - * with indices zero and one respectively. To connect some element of the collection with its generic type - * add to the constraints `typeConstraintToGenericTypeParameter(elementAddr, collectionAddr, typeParamIndex)`. - * - * @see UtIsGenericTypeExpression - */ - fun typeConstraintToGenericTypeParameter( - addr: UtAddrExpression, - baseAddr: UtAddrExpression, - i: Int - ): UtIsGenericTypeExpression = UtIsGenericTypeExpression(addr, baseAddr, i) - - /** - * Looks for a substitution for the given [method]. - * - * @param method a method to be substituted. - * @return substituted method if the given [method] has substitution, null otherwise. - * - * Note: all the methods in the class with substitutions will be returned instead of methods of the target class - * with the same name and parameters' types without any additional annotations. The only exception is `` - * method, substitutions will be returned only for constructors marked by [org.utbot.api.annotation.UtConstructorMock] - * annotation. - */ - fun findSubstitutionOrNull(method: SootMethod): SootMethod? { - val declaringClass = method.declaringClass - val classWithSubstitutions = targetToSubstitution[declaringClass] - - val substitutedMethod = classWithSubstitutions - ?.methods - ?.singleOrNull { it.name == method.name && it.parameterTypes == method.parameterTypes } - // Note: subSignature is not used in order to support `this` as method's return value. - // Otherwise we'd have to check for wrong `this` type in the subSignature - - if (method.isConstructor) { - // if the constructor doesn't have the mock annotation do not substitute it - substitutedMethod?.findMockAnnotationOrNull ?: return null - } - return substitutedMethod - } - - /** - * Returns a class containing substitutions for the methods belong to the target class, null if there is not such class. - */ - @Suppress("unused") - fun findSubstitutionByTargetOrNull(targetClass: SootClass): SootClass? = targetToSubstitution[targetClass] - - /** - * Returns a target class by given class with methods substitutions. - */ - @Suppress("MemberVisibilityCanBePrivate") - fun findTargetBySubstitutionOrNull(classWithSubstitutions: SootClass): SootClass? = - substitutionToTarget[classWithSubstitutions] - - /** - * Looks for 'real' type. - * - * For example, we have two classes: A and B, B contains substitutions for A's methods. - * `findRealType(a.type)` will return `a.type`, but `findRealType(b.type)` will return `a.type` as well. - * - * Returns: - * * [type] if it is not a RefType; - * * [type] if it is a RefType and it doesn't have a target class to substitute; - * * otherwise a type of the target class, which methods should be substituted. - */ - fun findRealType(type: Type): Type = - if (type !is RefType) type else findTargetBySubstitutionOrNull(type.sootClass)?.type ?: type - - /** - * Returns a select expression containing information about whether [ClassCastException] is allowed or not - * for an object with the given [addr]. - * - * True means that [ClassCastException] might be thrown, false will restrict it. - */ - fun isClassCastExceptionAllowed(addr: UtAddrExpression) = isClassCastExceptionAllowed.select(addr) - - /** - * Modify [isClassCastExceptionAllowed] to make impossible for a [ClassCastException] to be thrown for an object - * with the given [addr]. - */ - fun disableCastClassExceptionCheck(addr: UtAddrExpression) { - isClassCastExceptionAllowed = isClassCastExceptionAllowed.store(addr, UtFalse) - } - - /** - * Returns chunkId for the given [arrayType]. - * - * Examples: - * * Object[] -> RefValues_Arrays - * * int[] -> intArrays - * * int[][] -> MultiArrays - */ - fun arrayChunkId(arrayType: ArrayType) = when (arrayType.numDimensions) { - 1 -> if (arrayType.baseType is RefType) { - ChunkId("RefValues", "Arrays") - } else { - ChunkId("${findRealType(arrayType.baseType)}", "Arrays") - } - else -> ChunkId("Multi", "Arrays") - } - - companion object { - // we use different shifts to distinguish easily types from objects in z3 listings - const val objectCounterInitialValue = 0x00000001 // 0x00000000 is reserved for NULL - - // we want to reserve addresses for every ClassRef in the program starting from this one - // Note: the number had been chosen randomly and can be changes without any consequences - const val classRefAddrsInitialValue = -16777216 // -(2 ^ 24) - - // since we use typeId as addr for ConstRef, we can not use 0x00000000 because of NULL value - const val typeCounterInitialValue = 0x00000001 - const val symbolicReturnNameCounterInitialValue = 0x80000000 - const val objectNumDimensions = 0 - const val emptyTypeId = 0 - private const val primitivesNumber = 8 - - internal val primTypes - get() = listOf( - ByteType.v(), - ShortType.v(), - IntType.v(), - LongType.v(), - FloatType.v(), - DoubleType.v(), - BooleanType.v(), - CharType.v() - ) - - val numberOfTypes get() = Scene.v().classes.size + primitivesNumber + typeCounterInitialValue - - /** - * Stores [TypeStorage] for [OBJECT_TYPE]. As it should be changed when Soot scene changes, - * it is loaded each time when [TypeRegistry] is created in init section. - */ - lateinit var objectTypeStorage: TypeStorage - } -} - private fun initialArray(descriptor: MemoryChunkDescriptor) = mkArrayConst(descriptor.id.toId(), UtAddrSort, descriptor.itemSort()) diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Mocks.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Mocks.kt index 63c32a753f..52061cc752 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Mocks.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Mocks.kt @@ -18,6 +18,7 @@ import kotlin.reflect.KFunction2 import kotlin.reflect.KFunction5 import kotlinx.collections.immutable.persistentListOf import org.utbot.common.nameOfPackage +import org.utbot.engine.types.OBJECT_TYPE import org.utbot.engine.util.mockListeners.MockListenerController import org.utbot.framework.util.isInaccessibleViaReflection import soot.BooleanType @@ -25,7 +26,6 @@ import soot.RefType import soot.Scene import soot.SootClass import soot.SootMethod -import kotlin.reflect.KFunction4 /** * Generates mock with address provided. diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt index 2116009cf1..c0551d7c11 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt @@ -7,7 +7,7 @@ import org.utbot.common.workaround import org.utbot.engine.MemoryState.CURRENT import org.utbot.engine.MemoryState.INITIAL import org.utbot.engine.MemoryState.STATIC_INITIAL -import org.utbot.engine.TypeRegistry.Companion.objectNumDimensions +import org.utbot.engine.types.TypeRegistry.Companion.objectNumDimensions import org.utbot.engine.pc.UtAddrExpression import org.utbot.engine.pc.UtArrayExpressionBase import org.utbot.engine.pc.UtArraySort @@ -90,6 +90,15 @@ import kotlin.math.max import kotlin.math.min import kotlinx.collections.immutable.persistentListOf import kotlinx.collections.immutable.persistentSetOf +import org.utbot.engine.types.CLASS_REF_CLASSNAME +import org.utbot.engine.types.CLASS_REF_CLASS_ID +import org.utbot.engine.types.CLASS_REF_NUM_DIMENSIONS_DESCRIPTOR +import org.utbot.engine.types.CLASS_REF_TYPE_DESCRIPTOR +import org.utbot.engine.types.ENUM_ORDINAL +import org.utbot.engine.types.OBJECT_TYPE +import org.utbot.engine.types.STRING_TYPE +import org.utbot.engine.types.TypeRegistry +import org.utbot.engine.types.TypeResolver import org.utbot.framework.plugin.api.visible.UtStreamConsumingException import org.utbot.framework.plugin.api.UtStreamConsumingFailure @@ -829,9 +838,14 @@ class Resolver( // as const or store model. if (defaultBaseType is PrimType) return null + // In case when we have `actualType` equal to `byte` and defaultType is `java.lang.Object` + if (defaultType.isJavaLangObject() && actualType is PrimType) { + return defaultType + } + // There is no way you have java.lang.Object as a defaultType here, since it'd mean that // some actualType is not an inheritor of it - require(!defaultType.isJavaLangObject()) { + require(!defaultType.isJavaLangObject() || actualType is PrimType) { "Object type $defaultType is unexpected in fallback to default type" } @@ -842,6 +856,14 @@ class Resolver( return null } + val baseTypeIsAnonymous = (actualType.baseType as? RefType)?.sootClass?.isAnonymous == true + val actualTypeIsArrayOfAnonymous = actualType is ArrayType && baseTypeIsAnonymous + + // There must be no arrays of anonymous classes + if (defaultType.isJavaLangObject() && actualTypeIsArrayOfAnonymous) { + return defaultType + } + // All cases with `java.lang.Object` as default base type should have been already processed require(!defaultBaseType.isJavaLangObject()) { "Unexpected `java.lang.Object` as a default base type" @@ -849,6 +871,20 @@ class Resolver( val actualBaseType = actualType.baseType + // It is a tricky case: we might have a method with a parameter like `List`. + // Inside we will transform it into a wrapper with internal field `RangeModifiableArray` + // with Objects inside. Since we do not support generics for nested fields, it won't + // have type information and there will be no type constraints for its elements (because + // it contains java.lang.Objects inside). But, during the resolving, we will use type information + // from org.utbot.engine.types.TypeRegistry.getTypeStoragesForObjectTypeParameters. + // Therefore, we will encounter an object that will try to be resolved as an instance of `Integer`, + // but there will be no type constraints for it. Therefore, it might get `actualType` equal to some + // primitive type. In this case, we will return the default type (actually, it is not clear whether + // we should return null or defaultType, and maybe here some inconsistency exists). + if (actualType is PrimType && defaultType !is PrimType) { + return defaultType + } + require(actualBaseType is RefType) { "Expected RefType, but $actualBaseType found" } require(defaultBaseType is RefType) { "Expected RefType, but $defaultBaseType found" } @@ -1237,8 +1273,9 @@ private fun Traverser.arrayToMethodResult( val memoryUpdate = MemoryUpdate( stores = persistentListOf(simplifiedNamedStore(descriptor, newAddr, updatedArray)), - touchedChunkDescriptors = persistentSetOf(descriptor) + touchedChunkDescriptors = persistentSetOf(descriptor), ) + return MethodResult( ArrayValue(typeStorage, newAddr), constraints.asHardConstraint(), diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt index b694feb53c..06f953230a 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt @@ -18,6 +18,7 @@ import org.utbot.engine.pc.mkNot import org.utbot.engine.pc.select import org.utbot.engine.pc.toConcrete import org.utbot.engine.symbolic.asHardConstraint +import org.utbot.engine.types.STRING_TYPE import org.utbot.framework.plugin.api.UtArrayModel import org.utbot.framework.plugin.api.UtAssembleModel import org.utbot.framework.plugin.api.UtExecutableCallModel diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt index 057f02ff13..3c5bda0c03 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt @@ -74,6 +74,15 @@ import org.utbot.engine.symbolic.asHardConstraint import org.utbot.engine.symbolic.asSoftConstraint import org.utbot.engine.symbolic.asAssumption import org.utbot.engine.symbolic.asUpdate +import org.utbot.engine.types.ENUM_ORDINAL +import org.utbot.engine.types.EQUALS_SIGNATURE +import org.utbot.engine.types.HASHCODE_SIGNATURE +import org.utbot.engine.types.METHOD_FILTER_MAP_FIELD_SIGNATURE +import org.utbot.engine.types.NUMBER_OF_PREFERRED_TYPES +import org.utbot.engine.types.OBJECT_TYPE +import org.utbot.engine.types.SECURITY_FIELD_SIGNATURE +import org.utbot.engine.types.TypeRegistry +import org.utbot.engine.types.TypeResolver import org.utbot.engine.util.trusted.isFromTrustedLibrary import org.utbot.engine.util.statics.concrete.associateEnumSootFieldsWithConcreteValues import org.utbot.engine.util.statics.concrete.isEnumAffectingExternalStatics @@ -849,8 +858,10 @@ class Traverser( } val typeStorage = typeResolver.constructTypeStorage(OBJECT_TYPE, arrayPossibleTypes) - queuedSymbolicStateUpdates += typeRegistry.typeConstraint(arrayInstance.addr, typeStorage) - .isConstraint().asHardConstraint() + queuedSymbolicStateUpdates += typeRegistry + .typeConstraint(arrayInstance.addr, typeStorage) + .isConstraint() + .asHardConstraint() } val elementType = arrayInstance.type.elementType @@ -3428,6 +3439,7 @@ class Traverser( val preferredTypes = typeResolver.findTopRatedTypes(possibleTypes, take = NUMBER_OF_PREFERRED_TYPES) val mostCommonType = preferredTypes.singleOrNull() ?: OBJECT_TYPE val typeStorage = typeResolver.constructTypeStorage(mostCommonType, preferredTypes) + return typeRegistry.typeConstraint(value.addr, typeStorage).isOrNullConstraint() } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt index 4c5388d30b..590c6f69bb 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt @@ -101,6 +101,8 @@ import kotlinx.coroutines.flow.onStart import kotlinx.coroutines.isActive import kotlinx.coroutines.job import kotlinx.coroutines.yield +import org.utbot.engine.types.TypeRegistry +import org.utbot.engine.types.TypeResolver import org.utbot.framework.plugin.api.UtExecutionSuccess import org.utbot.framework.plugin.api.UtLambdaModel import org.utbot.framework.plugin.api.UtSandboxFailure diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt index e573ada66b..c6a7ca7c1f 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt @@ -8,7 +8,7 @@ import org.utbot.common.md5 import org.utbot.common.trace import org.utbot.engine.Eq import org.utbot.engine.PrimitiveValue -import org.utbot.engine.TypeRegistry +import org.utbot.engine.types.TypeRegistry import org.utbot.engine.pc.UtSolverStatusKind.SAT import org.utbot.engine.pc.UtSolverStatusKind.UNKNOWN import org.utbot.engine.pc.UtSolverStatusKind.UNSAT diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSort.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSort.kt index c30c20eb12..f5af719fb8 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSort.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSort.kt @@ -1,6 +1,6 @@ package org.utbot.engine.pc -import org.utbot.engine.SeqType +import org.utbot.engine.types.SeqType import com.microsoft.z3.Context import com.microsoft.z3.Sort import java.util.Objects diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt index 68a3be82fc..376ceec294 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt @@ -2,8 +2,7 @@ package org.utbot.engine.pc import org.utbot.common.WorkaroundReason import org.utbot.common.workaround -import org.utbot.engine.MAX_STRING_LENGTH_SIZE_BITS -import org.utbot.engine.TypeRegistry +import org.utbot.engine.types.TypeRegistry import org.utbot.engine.TypeStorage import org.utbot.engine.baseType import org.utbot.engine.defaultValue @@ -22,11 +21,11 @@ import com.microsoft.z3.Expr import com.microsoft.z3.FPSort import com.microsoft.z3.IntExpr import com.microsoft.z3.Model -import com.microsoft.z3.SeqExpr -import com.microsoft.z3.mkSeqNth +import org.utbot.engine.types.TypeRegistry.Companion.numberOfTypes +import org.utbot.framework.UtSettings +import org.utbot.framework.UtSettings.maxTypeNumberForEnumeration +import org.utbot.framework.UtSettings.useBitVecBasedTypeSystem import java.util.IdentityHashMap -import soot.ByteType -import soot.CharType import soot.PrimType import soot.RefType import soot.Type @@ -153,7 +152,7 @@ open class Z3TranslatorVisitor( * @param expr the type expression * @return the type expression translated into z3 assertions * @see UtIsExpression - * @see MAX_TYPE_NUMBER_FOR_ENUMERATION + * @see UtSettings.maxTypeNumberForEnumeration */ override fun visit(expr: UtIsExpression): Expr = expr.run { val symNumDimensions = translate(typeRegistry.symNumDimensions(addr)) as BitVecExpr @@ -164,33 +163,8 @@ open class Z3TranslatorVisitor( // TODO remove it JIRA:1321 val filteredPossibleTypes = workaround(WorkaroundReason.HACK) { typeStorage.filterInappropriateTypes() } - // add constraints for typeId - if (typeStorage.possibleConcreteTypes.size < MAX_TYPE_NUMBER_FOR_ENUMERATION) { - val symType = translate(typeRegistry.symTypeId(addr)) - val possibleBaseTypes = filteredPossibleTypes.map { it.baseType } - - val typeConstraint = z3Context.mkOr( - *possibleBaseTypes - .map { z3Context.mkEq(z3Context.mkBV(typeRegistry.findTypeId(it), Int.SIZE_BITS), symType) } - .toTypedArray() - ) - - constraints += typeConstraint - } else { - val shiftedExpression = z3Context.mkBVSHL( - z3Context.mkZeroExt(numberOfTypes - 1, z3Context.mkBV(1, 1)), - z3Context.mkZeroExt(numberOfTypes - Int.SIZE_BITS, symTypeId) - ) - - val bitVecString = typeRegistry.constructBitVecString(filteredPossibleTypes) - val possibleTypesBitVector = z3Context.mkBV(bitVecString, numberOfTypes) - - val typeConstraint = z3Context.mkEq( - z3Context.mkBVAND(shiftedExpression, z3Context.mkBVNot(possibleTypesBitVector)), - z3Context.mkBV(0, numberOfTypes) - ) - - constraints += typeConstraint + if (filteredPossibleTypes.size > UtSettings.maxNumberOfTypesToEncode) { + return@run z3Context.mkTrue() } val exprBaseType = expr.type.baseType @@ -202,6 +176,8 @@ open class Z3TranslatorVisitor( z3Context.mkEq(symNumDimensions, numDimensions) } + constraints += encodePossibleTypes(symTypeId, filteredPossibleTypes) + z3Context.mkAnd(*constraints.toTypedArray()) } @@ -227,23 +203,11 @@ open class Z3TranslatorVisitor( val constraints = mutableListOf() for (i in types.indices) { val symType = translate(typeRegistry.genericTypeId(addr, i)) + val possibleConcreteTypes = types[i].possibleConcreteTypes - if (types[i].leastCommonType.isJavaLangObject()) { - continue - } - - val possibleBaseTypes = types[i].possibleConcreteTypes.map { it.baseType } - - val typeConstraint = z3Context.mkOr( - *possibleBaseTypes.map { - z3Context.mkEq( - z3Context.mkBV(typeRegistry.findTypeId(it), Int.SIZE_BITS), - symType - ) - }.toTypedArray() - ) + if (possibleConcreteTypes.size > UtSettings.maxNumberOfTypesToEncode) continue - constraints += typeConstraint + constraints += encodePossibleTypes(symType, possibleConcreteTypes) } z3Context.mkOr( @@ -252,6 +216,35 @@ open class Z3TranslatorVisitor( ) } + private fun encodePossibleTypes(symType: Expr, possibleConcreteTypes: Collection): BoolExpr { + val possibleBaseTypes = possibleConcreteTypes.map { it.baseType } + + return if (!useBitVecBasedTypeSystem || possibleConcreteTypes.size < maxTypeNumberForEnumeration) { + z3Context.mkOr( + *possibleBaseTypes + .map { + val typeId = typeRegistry.findTypeId(it) + val typeIdBv = z3Context.mkBV(typeId, Int.SIZE_BITS) + z3Context.mkEq(typeIdBv, symType) + } + .toTypedArray() + ) + } else { + val shiftedExpression = z3Context.mkBVSHL( + z3Context.mkZeroExt(numberOfTypes - 1, z3Context.mkBV(1, 1)), + z3Context.mkZeroExt(numberOfTypes - Int.SIZE_BITS, symType as BitVecExpr) + ) + + val bitVecString = typeRegistry.constructBitVecString(possibleBaseTypes) + val possibleTypesBitVector = z3Context.mkBV(bitVecString, numberOfTypes) + + z3Context.mkEq( + z3Context.mkBVAND(shiftedExpression, z3Context.mkBVNot(possibleTypesBitVector)), + z3Context.mkBV(0, numberOfTypes) + ) + } + } + override fun visit(expr: UtIsGenericTypeExpression): Expr = expr.run { val symType = translate(typeRegistry.symTypeId(addr)) val symNumDimensions = translate(typeRegistry.symNumDimensions(addr)) @@ -312,10 +305,6 @@ open class Z3TranslatorVisitor( mkBV2Int(translate(expr) as BitVecExpr, true) } - companion object { - const val MAX_TYPE_NUMBER_FOR_ENUMERATION = 64 - } - override fun visit(expr: UtArrayInsert): Expr = error("translate of UtArrayInsert expression") override fun visit(expr: UtArrayInsertRange): Expr = error("translate of UtArrayInsertRange expression") diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathSelectorBuilder.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathSelectorBuilder.kt index b529e6d456..5516d5480b 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathSelectorBuilder.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathSelectorBuilder.kt @@ -4,7 +4,7 @@ package org.utbot.engine.selectors import org.utbot.analytics.EngineAnalyticsContext import org.utbot.engine.InterProceduralUnitGraph -import org.utbot.engine.TypeRegistry +import org.utbot.engine.types.TypeRegistry import org.utbot.engine.selectors.StrategyOption.DISTANCE import org.utbot.engine.selectors.StrategyOption.VISIT_COUNTING import org.utbot.engine.selectors.nurs.CPInstSelector diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/InheritorsSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/InheritorsSelector.kt index 8550c3c46e..611f9e0cb6 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/InheritorsSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/InheritorsSelector.kt @@ -1,7 +1,7 @@ package org.utbot.engine.selectors.nurs import org.utbot.engine.ExecutionState -import org.utbot.engine.TypeRegistry +import org.utbot.engine.types.TypeRegistry import org.utbot.engine.selectors.strategies.DistanceStatistics import org.utbot.engine.selectors.strategies.StoppingStrategy import kotlin.math.pow diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/DistanceStatistics.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/DistanceStatistics.kt index 448bdc82b3..9c3e7163d8 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/DistanceStatistics.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/DistanceStatistics.kt @@ -9,6 +9,7 @@ import org.utbot.engine.stmts import kotlin.math.min import kotlinx.collections.immutable.PersistentList import kotlinx.collections.immutable.persistentListOf +import org.utbot.framework.UtSettings.enableLoggingForDroppedStates import soot.jimple.Stmt import soot.toolkits.graph.ExceptionalUnitGraph @@ -43,8 +44,11 @@ class DistanceStatistics( val shouldDrop = state.edges.all { graph.isCoveredWithAllThrowStatements(it) } && distanceToUncovered(state) == Int.MAX_VALUE if (shouldDrop) { - pathLogger.debug { - "Dropping state (lastStatus=${state.solver.lastStatus}) by the distance statistics. MD5: ${state.md5()}" + if (enableLoggingForDroppedStates) { + pathLogger.debug { + val lastStatus = state.solver.lastStatus + "Dropping state (lastStatus=$lastStatus) by the distance statistics. MD5: ${state.md5()}" + } } } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/EdgeVisitCountingStatistics.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/EdgeVisitCountingStatistics.kt index 1a0ad21348..b38e1b2b94 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/EdgeVisitCountingStatistics.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/EdgeVisitCountingStatistics.kt @@ -4,6 +4,7 @@ import org.utbot.engine.Edge import org.utbot.engine.ExecutionState import org.utbot.engine.InterProceduralUnitGraph import org.utbot.engine.pathLogger +import org.utbot.framework.UtSettings.enableLoggingForDroppedStates import soot.jimple.Stmt import soot.jimple.internal.JReturnStmt import soot.jimple.internal.JReturnVoidStmt @@ -35,9 +36,12 @@ class EdgeVisitCountingStatistics( val shouldDrop = state.edges.all { graph.isCoveredWithAllThrowStatements(it) } && state.isComplete() if (shouldDrop) { - pathLogger.debug { - "Dropping state (lastStatus=${state.solver.lastStatus}) " + - "by the edge visit counting statistics. MD5: ${state.md5()}" + if (enableLoggingForDroppedStates) { + pathLogger.debug { + val lastStatus = state.solver.lastStatus + val md5 = state.md5() + "Dropping state (lastStatus=$lastStatus) by the edge visit counting statistics. MD5: $md5" + } } } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeRegistry.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeRegistry.kt new file mode 100644 index 0000000000..568cb45f77 --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeRegistry.kt @@ -0,0 +1,656 @@ +package org.utbot.engine.types + +import com.google.common.collect.HashBiMap +import kotlinx.collections.immutable.persistentListOf +import kotlinx.collections.immutable.persistentSetOf +import org.utbot.common.WorkaroundReason +import org.utbot.common.doNotRun +import org.utbot.common.workaround +import org.utbot.engine.ChunkId +import org.utbot.engine.MAX_NUM_DIMENSIONS +import org.utbot.engine.MemoryUpdate +import org.utbot.engine.MethodResult +import org.utbot.engine.ObjectValue +import org.utbot.engine.TypeConstraint +import org.utbot.engine.TypeStorage +import org.utbot.engine.baseType +import org.utbot.engine.classBytecodeSignatureToClassNameOrNull +import org.utbot.engine.findMockAnnotationOrNull +import org.utbot.engine.getByValue +import org.utbot.engine.isAnonymous +import org.utbot.engine.isInappropriate +import org.utbot.engine.isJavaLangObject +import org.utbot.engine.nullObjectAddr +import org.utbot.engine.numDimensions +import org.utbot.engine.pc.UtAddrExpression +import org.utbot.engine.pc.UtAddrSort +import org.utbot.engine.pc.UtArrayExpressionBase +import org.utbot.engine.pc.UtArraySort +import org.utbot.engine.pc.UtBoolExpression +import org.utbot.engine.pc.UtBoolSort +import org.utbot.engine.pc.UtEqGenericTypeParametersExpression +import org.utbot.engine.pc.UtFalse +import org.utbot.engine.pc.UtGenericExpression +import org.utbot.engine.pc.UtInt32Sort +import org.utbot.engine.pc.UtIsExpression +import org.utbot.engine.pc.UtIsGenericTypeExpression +import org.utbot.engine.pc.UtMkTermArrayExpression +import org.utbot.engine.pc.UtTrue +import org.utbot.engine.pc.mkAnd +import org.utbot.engine.pc.mkArrayConst +import org.utbot.engine.pc.mkArrayWithConst +import org.utbot.engine.pc.mkEq +import org.utbot.engine.pc.mkInt +import org.utbot.engine.pc.mkNot +import org.utbot.engine.pc.mkOr +import org.utbot.engine.pc.select +import org.utbot.engine.pc.store +import org.utbot.engine.simplifiedNamedStore +import org.utbot.engine.symbolic.asHardConstraint +import org.utbot.engine.toIntValue +import org.utbot.engine.toPrimitiveValue +import soot.ArrayType +import soot.BooleanType +import soot.ByteType +import soot.CharType +import soot.DoubleType +import soot.FloatType +import soot.IntType +import soot.LongType +import soot.RefType +import soot.Scene +import soot.ShortType +import soot.SootClass +import soot.SootField +import soot.SootMethod +import soot.Type +import soot.tagkit.AnnotationClassElem +import java.math.BigInteger +import java.util.concurrent.atomic.AtomicInteger +import java.util.concurrent.atomic.AtomicLong + +/** + * Types/classes registry. + * + * Registers and keeps two mappings: + * - Type <-> unique type id (int) + * - Object address -> to type id + */ +class TypeRegistry { + init { + // initializes type storage for OBJECT_TYPE from current scene + objectTypeStorage = TypeStorage.constructTypeStorageUnsafe( + OBJECT_TYPE, + Scene.v().classes.mapTo(mutableSetOf()) { it.type } + ) + } + + private val typeIdBiMap = HashBiMap.create() + + // A cache for strings representing bit-vectors for some collection of types. + private val typesToBitVecString = mutableMapOf, String>() + private val typeToRating = mutableMapOf() + private val typeToInheritorsTypes = mutableMapOf>() + private val typeToAncestorsTypes = mutableMapOf>() + + /** + * Contains types storages for type parameters of object by its address. + */ + private val genericTypeStorageByAddr = mutableMapOf>() + + // A BiMap containing bijection from every type to an address of the object + // presenting its classRef and vise versa + private val classRefBiMap = HashBiMap.create() + + /** + * Contains mapping from a class to the class containing substitutions for its methods. + */ + private val targetToSubstitution: Map by lazy { + val classesWithTargets = Scene.v().classes.mapNotNull { clazz -> + val annotation = clazz.findMockAnnotationOrNull + ?.elems + ?.singleOrNull { it.name == "target" } as? AnnotationClassElem + + val classNameFromSignature = classBytecodeSignatureToClassNameOrNull(annotation?.desc) + + if (classNameFromSignature == null) { + null + } else { + val target = Scene.v().getSootClass(classNameFromSignature) + target to clazz + } + } + classesWithTargets.toMap() + } + + /** + * Contains mapping from a class with substitutions of the methods of the target class to the target class itself. + */ + private val substitutionToTarget: Map by lazy { + targetToSubstitution.entries.associate { (k, v) -> v to k } + } + + private val typeToFields = mutableMapOf>() + + /** + * An array containing information about whether the object with particular addr could throw a [ClassCastException]. + * + * Note: all objects can throw it by default. + * @see disableCastClassExceptionCheck + */ + private var isClassCastExceptionAllowed: UtArrayExpressionBase = + mkArrayWithConst(UtArraySort(UtAddrSort, UtBoolSort), UtTrue) + + + /** + * Contains information about types for ReferenceValues. + * An element on some position k contains information about type for an object with address == k + * Each element in addrToTypeId is in range [1..numberOfTypes] + */ + private val addrToTypeId: UtArrayExpressionBase by lazy { + mkArrayConst( + "addrToTypeId", + UtAddrSort, + UtInt32Sort + ) + } + + private val genericAddrToTypeArrays = mutableMapOf() + + private fun genericAddrToType(i: Int) = genericAddrToTypeArrays.getOrPut(i) { + mkArrayConst( + "genericAddrToTypeId_$i", + UtAddrSort, + UtInt32Sort + ) + } + + /** + * Contains information about number of dimensions for ReferenceValues. + */ + private val addrToNumDimensions: UtArrayExpressionBase by lazy { + mkArrayConst( + "addrToNumDimensions", + UtAddrSort, + UtInt32Sort + ) + } + + private val genericAddrToNumDimensionsArrays = mutableMapOf() + + private fun genericAddrToNumDimensions(i: Int) = genericAddrToNumDimensionsArrays.getOrPut(i) { + mkArrayConst( + "genericAddrToNumDimensions_$i", + UtAddrSort, + UtInt32Sort + ) + } + + /** + * Contains information about whether the object with some addr is a mock or not. + */ + private val isMockArray: UtArrayExpressionBase by lazy { + mkArrayConst( + "isMock", + UtAddrSort, + UtBoolSort + ) + } + + /** + * Takes information about whether the object with [addr] is mock or not. + * + * @see isMockArray + */ + fun isMock(addr: UtAddrExpression) = isMockArray.select(addr) + + /** + * Makes the numbers of dimensions for every object in the program equal to zero by default + */ + fun softZeroNumDimensions() = UtMkTermArrayExpression(addrToNumDimensions) + + /** + * addrToTypeId is created as const array of the emptyType. If such type occurs anywhere in the program, it means + * we haven't touched the element that this type belongs to + * @see emptyTypeId + */ + fun softEmptyTypes() = UtMkTermArrayExpression(addrToTypeId, mkInt(emptyTypeId)) + + /** + * Calculates type 'rating' for a particular type. Used for ordering ObjectValue's possible types. + * The type with a higher rating is more likely than the one with a lower rating. + */ + fun findRating(type: RefType) = typeToRating.getOrPut(type) { + var finalCost = 0 + + val sootClass = type.sootClass + + // TODO: let's have "preferred types" + if (sootClass.name == "java.util.ArrayList") finalCost += 4096 + if (sootClass.name == "java.util.LinkedList") finalCost += 2048 + if (sootClass.name == "java.util.HashMap") finalCost += 4096 + if (sootClass.name == "java.util.TreeMap") finalCost += 2048 + if (sootClass.name == "java.util.HashSet") finalCost += 2048 + if (sootClass.name == "java.lang.Integer") finalCost += 8192 + if (sootClass.name == "java.lang.Character") finalCost += 8192 + if (sootClass.name == "java.lang.Double") finalCost += 8192 + if (sootClass.name == "java.lang.Long") finalCost += 8192 + + if (sootClass.packageName.startsWith("java.lang")) finalCost += 1024 + + if (sootClass.packageName.startsWith("java.util")) finalCost += 512 + + if (sootClass.packageName.startsWith("java")) finalCost += 128 + + if (sootClass.isPublic) finalCost += 16 + + if (sootClass.isPrivate) finalCost += -16 + + if ("blocking" in sootClass.name.toLowerCase()) finalCost -= 32 + + if (sootClass.type.isJavaLangObject()) finalCost += -32 + + if (sootClass.isAnonymous) finalCost += -128 + + if (sootClass.name.contains("$")) finalCost += -4096 + + if (sootClass.type.sootClass.isInappropriate) finalCost += -8192 + + finalCost + } + + private val classRefCounter = AtomicInteger(classRefAddrsInitialValue) + private fun nextClassRefAddr() = UtAddrExpression(classRefCounter.getAndIncrement()) + + private val symbolicReturnNameCounter = AtomicLong(symbolicReturnNameCounterInitialValue) + fun findNewSymbolicReturnValueName() = + workaround(WorkaroundReason.MAKE_SYMBOLIC) { "symbolicReturnValue\$${symbolicReturnNameCounter.incrementAndGet()}" } + + private val typeCounter = AtomicInteger(typeCounterInitialValue) + private fun nextTypeId() = typeCounter.getAndIncrement() + + /** + * Returns unique typeId for the given type + */ + fun findTypeId(type: Type): Int = typeIdBiMap.getOrPut(type) { nextTypeId() } + + /** + * Returns type for the given typeId + * + * @return If there is such typeId in the program, returns the corresponding type, otherwise returns null + */ + fun typeByIdOrNull(typeId: Int): Type? = typeIdBiMap.getByValue(typeId) + + /** + * Returns symbolic representation for a typeId corresponding to the given address + */ + fun symTypeId(addr: UtAddrExpression) = addrToTypeId.select(addr) + + /** + * Returns a symbolic representation for an [i]th type parameter + * corresponding to the given address + */ + fun genericTypeId(addr: UtAddrExpression, i: Int) = genericAddrToType(i).select(addr) + + /** + * Returns symbolic representation for a number of dimensions corresponding to the given address + */ + fun symNumDimensions(addr: UtAddrExpression) = addrToNumDimensions.select(addr) + + fun genericNumDimensions(addr: UtAddrExpression, i: Int) = genericAddrToNumDimensions(i).select(addr) + + /** + * Returns a constraint stating that number of dimensions for the given address is zero + */ + fun zeroDimensionConstraint(addr: UtAddrExpression) = mkEq(symNumDimensions(addr), mkInt(objectNumDimensions)) + + /** + * Constructs a binary bit-vector by the given types with length 'numberOfTypes'. Each position + * corresponding to one of the typeId. + * + * @param types the collection of possible type + * @return decimal string representing the binary bit-vector + */ + fun constructBitVecString(types: Collection) = typesToBitVecString.getOrPut(types) { + val initialValue = BigInteger(ByteArray(numberOfTypes) { 0 }) + + return types.fold(initialValue) { acc, type -> + val typeId = if (type is ArrayType) findTypeId(type.baseType) else findTypeId(type) + acc.setBit(typeId) + }.toString() + } + + /** + * Creates class reference, i.e. Class<Integer> + * + * Note: Uses type id as an address to have the one and the same class reference for all objects of one class + */ + fun createClassRef(baseType: Type, numDimensions: Int = 0): MethodResult { + val addr = classRefBiMap.getOrPut(baseType) { nextClassRefAddr() } + + val typeStorage = TypeStorage.constructTypeStorageWithSingleType(CLASS_REF_TYPE) + val objectValue = ObjectValue(typeStorage, addr) + + val typeConstraint = typeConstraint(addr, typeStorage).all() + + val typeId = mkInt(findTypeId(baseType)) + val symNumDimensions = mkInt(numDimensions) + + val stores = persistentListOf( + simplifiedNamedStore(CLASS_REF_TYPE_DESCRIPTOR, addr, typeId), + simplifiedNamedStore(CLASS_REF_NUM_DIMENSIONS_DESCRIPTOR, addr, symNumDimensions) + ) + + val touchedDescriptors = persistentSetOf(CLASS_REF_TYPE_DESCRIPTOR, CLASS_REF_NUM_DIMENSIONS_DESCRIPTOR) + + val memoryUpdate = MemoryUpdate( + stores = stores, + touchedChunkDescriptors = touchedDescriptors, + ) + + return MethodResult(objectValue, typeConstraint.asHardConstraint(), memoryUpdates = memoryUpdate) + } + + /** + * Returns a list of inheritors for the given [type], including itself. + */ + fun findInheritorsIncludingTypes(type: RefType, defaultValue: () -> Set) = + typeToInheritorsTypes.getOrPut(type, defaultValue) + + /** + * Returns a list of ancestors for the given [type], including itself. + */ + fun findAncestorsIncludingTypes(type: RefType, defaultValue: () -> Set) = + typeToAncestorsTypes.getOrPut(type, defaultValue) + + fun findFields(type: RefType, defaultValue: () -> List) = + typeToFields.getOrPut(type, defaultValue) + + /** + * Returns a [TypeConstraint] instance for the given [addr] and [typeStorage]. + */ + fun typeConstraint(addr: UtAddrExpression, typeStorage: TypeStorage): TypeConstraint = + TypeConstraint( + constructIsExpression(addr, typeStorage), + mkEq(addr, nullObjectAddr), + constructCorrectnessConstraint(addr, typeStorage) + ) + + private fun constructIsExpression(addr: UtAddrExpression, typeStorage: TypeStorage): UtIsExpression = + UtIsExpression(addr, typeStorage, numberOfTypes) + + /** + * Returns a conjunction of the constraints responsible for the type construction: + * * typeId must be in range [[emptyTypeId]..[numberOfTypes]]; + * * numDimensions must be in range [0..[MAX_NUM_DIMENSIONS]]; + * * if the baseType for [TypeStorage.leastCommonType] is a [java.lang.Object], + * should be added constraints for primitive arrays to prevent + * impossible resolved types: Object[] must be at least primType[][]. + */ + private fun constructCorrectnessConstraint(addr: UtAddrExpression, typeStorage: TypeStorage): UtBoolExpression { + val symType = symTypeId(addr) + val symNumDimensions = symNumDimensions(addr) + val type = typeStorage.leastCommonType + + val constraints = mutableListOf() + + // add constraints for typeId, it must be in 0..numberOfTypes + constraints += org.utbot.engine.Ge(symType.toIntValue(), emptyTypeId.toPrimitiveValue()) + constraints += org.utbot.engine.Le(symType.toIntValue(), numberOfTypes.toPrimitiveValue()) + + // add constraints for number of dimensions, it must be in 0..MAX_NUM_DIMENSIONS + constraints += org.utbot.engine.Ge(symNumDimensions.toIntValue(), 0.toPrimitiveValue()) + constraints += org.utbot.engine.Le(symNumDimensions.toIntValue(), MAX_NUM_DIMENSIONS.toPrimitiveValue()) + + doNotRun { + // add constraints for object and arrays of primitives + if (type.baseType.isJavaLangObject()) { + primTypes.forEach { + val typesAreEqual = mkEq(symType, mkInt(findTypeId(it))) + val numDimensions = + org.utbot.engine.Gt(symNumDimensions.toIntValue(), type.numDimensions.toPrimitiveValue()) + constraints += mkOr(mkNot(typesAreEqual), numDimensions) + } + } + + // there are no arrays of anonymous classes + typeStorage.possibleConcreteTypes + .mapNotNull { (it.baseType as? RefType) } + .filter { it.sootClass.isAnonymous } + .forEach { + val typesAreEqual = mkEq(symType, mkInt(findTypeId(it))) + val numDimensions = mkEq(symNumDimensions.toIntValue(), mkInt(objectNumDimensions).toIntValue()) + constraints += mkOr(mkNot(typesAreEqual), numDimensions) + } + } + + return mkAnd(constraints) + } + + + + /** + * returns constraint representing, that object with address [addr] is parametrized by [types] type parameters. + * @see UtGenericExpression + */ + fun genericTypeParameterConstraint(addr: UtAddrExpression, types: List) = + UtGenericExpression(addr, types, numberOfTypes) + + /** + * returns constraint representing that type parameters of an object with address [firstAddr] are equal to + * type parameters of an object with address [secondAddr], corresponding to [indexInjection] + * @see UtEqGenericTypeParametersExpression + */ + @Suppress("unused") + fun eqGenericTypeParametersConstraint( + firstAddr: UtAddrExpression, + secondAddr: UtAddrExpression, + vararg indexInjection: Pair + ): UtEqGenericTypeParametersExpression { + setParameterTypeStoragesEquality(firstAddr, secondAddr, indexInjection) + + return UtEqGenericTypeParametersExpression(firstAddr, secondAddr, mapOf(*indexInjection)) + } + + /** + * returns constraint representing that type parameters of an object with address [firstAddr] are equal to + * the corresponding type parameters of an object with address [secondAddr] + * @see UtEqGenericTypeParametersExpression + */ + fun eqGenericTypeParametersConstraint( + firstAddr: UtAddrExpression, + secondAddr: UtAddrExpression, + parameterSize: Int + ) : UtEqGenericTypeParametersExpression { + val injections = Array(parameterSize) { it to it } + + return eqGenericTypeParametersConstraint(firstAddr, secondAddr, *injections) + } + + /** + * returns constraint representing that the first type parameter of an object with address [firstAddr] are equal to + * the first type parameter of an object with address [secondAddr] + * @see UtEqGenericTypeParametersExpression + */ + fun eqGenericSingleTypeParameterConstraint(firstAddr: UtAddrExpression, secondAddr: UtAddrExpression) = + eqGenericTypeParametersConstraint(firstAddr, secondAddr, 0 to 0) + + /** + * Associates provided [typeStorages] with an object with the provided [addr]. + */ + fun saveObjectParameterTypeStorages(addr: UtAddrExpression, typeStorages: List) { + genericTypeStorageByAddr += addr to typeStorages + } + + /** + * Retrieves parameter type storages of an object with the given [addr] if present, or null otherwise. + */ + fun getTypeStoragesForObjectTypeParameters(addr: UtAddrExpression): List? = genericTypeStorageByAddr[addr] + + /** + * Set types storages for [firstAddr]'s type parameters equal to type storages for [secondAddr]'s type parameters + * according to provided types injection represented by [indexInjection]. + */ + private fun setParameterTypeStoragesEquality( + firstAddr: UtAddrExpression, + secondAddr: UtAddrExpression, + indexInjection: Array> + ) { + val existingGenericTypes = genericTypeStorageByAddr[secondAddr] ?: return + + val currentGenericTypes = mutableMapOf() + + indexInjection.forEach { (from, to) -> + require(from >= 0 && from < existingGenericTypes.size) { + "Type injection is out of bounds: should be in [0; ${existingGenericTypes.size}) but is $from" + } + + currentGenericTypes[to] = existingGenericTypes[from] + } + + genericTypeStorageByAddr[firstAddr] = currentGenericTypes + .entries + .sortedBy { it.key } + .mapTo(mutableListOf()) { it.value } + } + + /** + * Returns constraint representing that an object with address [addr] has the same type as the type parameter + * with index [i] of an object with address [baseAddr]. + * + * For a SomeCollection the type parameters are [A, B], where A and B are type variables + * with indices zero and one respectively. To connect some element of the collection with its generic type + * add to the constraints `typeConstraintToGenericTypeParameter(elementAddr, collectionAddr, typeParamIndex)`. + * + * @see UtIsGenericTypeExpression + */ + fun typeConstraintToGenericTypeParameter( + addr: UtAddrExpression, + baseAddr: UtAddrExpression, + i: Int + ): UtIsGenericTypeExpression = UtIsGenericTypeExpression(addr, baseAddr, i) + + /** + * Looks for a substitution for the given [method]. + * + * @param method a method to be substituted. + * @return substituted method if the given [method] has substitution, null otherwise. + * + * Note: all the methods in the class with substitutions will be returned instead of methods of the target class + * with the same name and parameters' types without any additional annotations. The only exception is `` + * method, substitutions will be returned only for constructors marked by [org.utbot.api.annotation.UtConstructorMock] + * annotation. + */ + fun findSubstitutionOrNull(method: SootMethod): SootMethod? { + val declaringClass = method.declaringClass + val classWithSubstitutions = targetToSubstitution[declaringClass] + + val substitutedMethod = classWithSubstitutions + ?.methods + ?.singleOrNull { it.name == method.name && it.parameterTypes == method.parameterTypes } + // Note: subSignature is not used in order to support `this` as method's return value. + // Otherwise we'd have to check for wrong `this` type in the subSignature + + if (method.isConstructor) { + // if the constructor doesn't have the mock annotation do not substitute it + substitutedMethod?.findMockAnnotationOrNull ?: return null + } + return substitutedMethod + } + + /** + * Returns a class containing substitutions for the methods belong to the target class, null if there is not such class. + */ + @Suppress("unused") + fun findSubstitutionByTargetOrNull(targetClass: SootClass): SootClass? = targetToSubstitution[targetClass] + + /** + * Returns a target class by given class with methods substitutions. + */ + @Suppress("MemberVisibilityCanBePrivate") + fun findTargetBySubstitutionOrNull(classWithSubstitutions: SootClass): SootClass? = + substitutionToTarget[classWithSubstitutions] + + /** + * Looks for 'real' type. + * + * For example, we have two classes: A and B, B contains substitutions for A's methods. + * `findRealType(a.type)` will return `a.type`, but `findRealType(b.type)` will return `a.type` as well. + * + * Returns: + * * [type] if it is not a RefType; + * * [type] if it is a RefType and it doesn't have a target class to substitute; + * * otherwise a type of the target class, which methods should be substituted. + */ + fun findRealType(type: Type): Type = + if (type !is RefType) type else findTargetBySubstitutionOrNull(type.sootClass)?.type ?: type + + /** + * Returns a select expression containing information about whether [ClassCastException] is allowed or not + * for an object with the given [addr]. + * + * True means that [ClassCastException] might be thrown, false will restrict it. + */ + fun isClassCastExceptionAllowed(addr: UtAddrExpression) = isClassCastExceptionAllowed.select(addr) + + /** + * Modify [isClassCastExceptionAllowed] to make impossible for a [ClassCastException] to be thrown for an object + * with the given [addr]. + */ + fun disableCastClassExceptionCheck(addr: UtAddrExpression) { + isClassCastExceptionAllowed = isClassCastExceptionAllowed.store(addr, UtFalse) + } + + /** + * Returns chunkId for the given [arrayType]. + * + * Examples: + * * Object[] -> RefValues_Arrays + * * int[] -> intArrays + * * int[][] -> MultiArrays + */ + fun arrayChunkId(arrayType: ArrayType) = when (arrayType.numDimensions) { + 1 -> if (arrayType.baseType is RefType) { + ChunkId("RefValues", "Arrays") + } else { + ChunkId("${findRealType(arrayType.baseType)}", "Arrays") + } + else -> ChunkId("Multi", "Arrays") + } + + companion object { + // we use different shifts to distinguish easily types from objects in z3 listings + const val objectCounterInitialValue = 0x00000001 // 0x00000000 is reserved for NULL + + // we want to reserve addresses for every ClassRef in the program starting from this one + // Note: the number had been chosen randomly and can be changes without any consequences + const val classRefAddrsInitialValue = -16777216 // -(2 ^ 24) + + // since we use typeId as addr for ConstRef, we can not use 0x00000000 because of NULL value + const val typeCounterInitialValue = 0x00000001 + const val symbolicReturnNameCounterInitialValue = 0x80000000 + const val objectNumDimensions = 0 + const val emptyTypeId = 0 + private const val primitivesNumber = 8 + + internal val primTypes + get() = listOf( + ByteType.v(), + ShortType.v(), + IntType.v(), + LongType.v(), + FloatType.v(), + DoubleType.v(), + BooleanType.v(), + CharType.v() + ) + + val numberOfTypes get() = Scene.v().classes.size + primitivesNumber + typeCounterInitialValue + + /** + * Stores [TypeStorage] for [OBJECT_TYPE]. As it should be changed when Soot scene changes, + * it is loaded each time when [TypeRegistry] is created in init section. + */ + lateinit var objectTypeStorage: TypeStorage + } +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/TypeResolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeResolver.kt similarity index 94% rename from utbot-framework/src/main/kotlin/org/utbot/engine/TypeResolver.kt rename to utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeResolver.kt index 62868da773..0e58067e2d 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/TypeResolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeResolver.kt @@ -1,11 +1,35 @@ -package org.utbot.engine +package org.utbot.engine.types import org.utbot.common.WorkaroundReason import org.utbot.common.workaround +import org.utbot.engine.ArrayValue +import org.utbot.engine.ChunkId +import org.utbot.engine.Hierarchy +import org.utbot.engine.MemoryChunkDescriptor +import org.utbot.engine.ObjectValue +import org.utbot.engine.ReferenceValue +import org.utbot.engine.TypeStorage +import org.utbot.engine.appropriateClasses +import org.utbot.engine.baseType +import org.utbot.engine.findMockAnnotationOrNull +import org.utbot.engine.isAppropriate +import org.utbot.engine.isArtificialEntity +import org.utbot.engine.isInappropriate +import org.utbot.engine.isJavaLangObject +import org.utbot.engine.isLambda +import org.utbot.engine.isLocal +import org.utbot.engine.isOverridden +import org.utbot.engine.isUtMock +import org.utbot.engine.makeArrayType +import org.utbot.engine.nullObjectAddr +import org.utbot.engine.numDimensions import org.utbot.engine.pc.UtAddrExpression import org.utbot.engine.pc.UtBoolExpression import org.utbot.engine.pc.mkAnd import org.utbot.engine.pc.mkEq +import org.utbot.engine.rawType +import org.utbot.engine.wrapper +import org.utbot.engine.wrapperToClass import org.utbot.framework.plugin.api.id import org.utbot.framework.plugin.api.util.id import org.utbot.framework.util.UTBOT_FRAMEWORK_API_VISIBLE_PACKAGE diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/util/statics/concrete/EnumConcreteUtils.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/util/statics/concrete/EnumConcreteUtils.kt index f4ca0a88be..f369526901 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/util/statics/concrete/EnumConcreteUtils.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/util/statics/concrete/EnumConcreteUtils.kt @@ -9,6 +9,7 @@ import org.utbot.engine.pc.mkNot import org.utbot.engine.pc.select import org.utbot.engine.symbolic.SymbolicStateUpdate import org.utbot.engine.symbolic.asHardConstraint +import org.utbot.engine.types.TypeResolver import org.utbot.framework.plugin.api.FieldId import org.utbot.framework.plugin.api.util.jField import soot.SootClass