Skip to content

Commit d9178da

Browse files
dtimdenis-fokin
authored andcommitted
Make UtEnumConstModel and UtClassRefModel reference models #414 (#611)
Make UtEnumConstModel and UtClassRefModel reference models #414 Historically `UtEnumConstModel` and `UtClassRefModel` have been processed not as other reference models, but in a special way, more like to primitive types. This approach leads to several problems, especially to class cast errors when processing generic collections with enums or class references as elements. This commit makes `UtEnumConstModel` and `UtClassRefModel` subtypes of `UtReferenceModel`. * Concrete executor is modified to respect the identity of static fields to avoid rewriting enum values and `Class<?>` instances. * Special processing for enums is implemented. When a new enum value is created, or an `Object` is being cast to the enum type, static values for the enum class are initialized, and the set of hard constraint is added to require that the new instance has the same address and ordinal as any one of enum constants to implement reference equality for enums. * `UtModelVisitor` has been updated to reflect the new inheritance hierarchy. * Corresponding changes in the fuzzer have been implemented, including id generation refactoring. A custom id generator interface hierarchy is now used instead of `IntSupplier`: - `IdGenerator` that allows to create fresh identifiers, - `IdentityPreservingIdGenerator`: `IdGenerator` that can return the same id for the same object. A default implementation of `IdentityPreservingIdGenerator` is used in fuzzer. It uses reference equality for object comparison, that allows to create distinct models of equal object (in `equals` sense), and to always assign the same id to the same enum value.
1 parent 17d3467 commit d9178da

File tree

32 files changed

+813
-146
lines changed

32 files changed

+813
-146
lines changed

utbot-framework-api/build.gradle

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,12 @@ dependencies {
2828
implementation group: 'io.github.microutils', name: 'kotlin-logging', version: kotlin_logging_version
2929
}
3030

31+
compileKotlin {
32+
kotlinOptions {
33+
freeCompilerArgs += "-Xopt-in=kotlin.RequiresOptIn"
34+
}
35+
}
36+
3137
shadowJar {
3238
configurations = [project.configurations.compileClasspath]
3339
archiveClassifier.set('')

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

Lines changed: 33 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,8 @@ import soot.jimple.JimpleBody
5151
import soot.jimple.Stmt
5252
import java.io.File
5353
import java.lang.reflect.Modifier
54+
import kotlin.contracts.ExperimentalContracts
55+
import kotlin.contracts.contract
5456
import kotlin.jvm.internal.CallableReference
5557
import kotlin.reflect.KCallable
5658
import kotlin.reflect.KClass
@@ -59,6 +61,8 @@ import kotlin.reflect.full.instanceParameter
5961
import kotlin.reflect.jvm.javaConstructor
6062
import kotlin.reflect.jvm.javaType
6163

64+
const val SYMBOLIC_NULL_ADDR: Int = 0
65+
6266
data class UtMethod<R>(
6367
val callable: KCallable<R>,
6468
val clazz: KClass<*>
@@ -267,6 +271,27 @@ fun UtModel.hasDefaultValue() =
267271
*/
268272
fun UtModel.isMockModel() = this is UtCompositeModel && isMock
269273

274+
/**
275+
* Get model id (symbolic null value for UtNullModel)
276+
* or null if model has no id (e.g., a primitive model) or the id is null.
277+
*/
278+
fun UtModel.idOrNull(): Int? = when (this) {
279+
is UtNullModel -> SYMBOLIC_NULL_ADDR
280+
is UtReferenceModel -> id
281+
else -> null
282+
}
283+
284+
/**
285+
* Returns the model id if it is available, or throws an [IllegalStateException].
286+
*/
287+
@OptIn(ExperimentalContracts::class)
288+
fun UtModel?.getIdOrThrow(): Int {
289+
contract {
290+
returns() implies (this@getIdOrThrow != null)
291+
}
292+
return this?.idOrNull() ?: throw IllegalStateException("Model id must not be null: $this")
293+
}
294+
270295
/**
271296
* Model for nulls.
272297
*/
@@ -308,20 +333,24 @@ object UtVoidModel : UtModel(voidClassId)
308333
* Model for enum constant
309334
*/
310335
data class UtEnumConstantModel(
336+
override val id: Int?,
311337
override val classId: ClassId,
312338
val value: Enum<*>
313-
) : UtModel(classId) {
314-
override fun toString(): String = "$value"
339+
) : UtReferenceModel(id, classId) {
340+
// Model id is included for debugging purposes
341+
override fun toString(): String = "$value@$id"
315342
}
316343

317344
/**
318345
* Model for class reference
319346
*/
320347
data class UtClassRefModel(
348+
override val id: Int?,
321349
override val classId: ClassId,
322350
val value: Class<*>
323-
) : UtModel(classId) {
324-
override fun toString(): String = "$value"
351+
) : UtReferenceModel(id, classId) {
352+
// Model id is included for debugging purposes
353+
override fun toString(): String = "$value@$id"
325354
}
326355

327356
/**

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,9 @@ val ClassId.isFloatType: Boolean
114114
val ClassId.isDoubleType: Boolean
115115
get() = this == doubleClassId || this == doubleWrapperClassId
116116

117+
val ClassId.isClassType: Boolean
118+
get() = this == classClassId
119+
117120
val voidClassId = ClassId("void")
118121
val booleanClassId = ClassId("boolean")
119122
val byteClassId = ClassId("byte")
@@ -135,6 +138,8 @@ val longWrapperClassId = java.lang.Long::class.id
135138
val floatWrapperClassId = java.lang.Float::class.id
136139
val doubleWrapperClassId = java.lang.Double::class.id
137140

141+
val classClassId = java.lang.Class::class.id
142+
138143
// We consider void wrapper as primitive wrapper
139144
// because voidClassId is considered primitive here
140145
val primitiveWrappers = setOf(
@@ -289,6 +294,9 @@ val ClassId.isMap: Boolean
289294
val ClassId.isIterableOrMap: Boolean
290295
get() = isIterable || isMap
291296

297+
val ClassId.isEnum: Boolean
298+
get() = jClass.isEnum
299+
292300
fun ClassId.findFieldByIdOrNull(fieldId: FieldId): Field? {
293301
if (isNotSubtypeOf(fieldId.declaringClass)) {
294302
return null

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,8 @@ import org.utbot.framework.plugin.api.UtCompositeModel
2424
import org.utbot.framework.plugin.api.UtModel
2525
import org.utbot.framework.plugin.api.UtNullModel
2626
import org.utbot.framework.plugin.api.UtPrimitiveModel
27-
import org.utbot.framework.plugin.api.UtReferenceModel
27+
import org.utbot.framework.plugin.api.getIdOrThrow
28+
import org.utbot.framework.plugin.api.idOrNull
2829
import org.utbot.framework.plugin.api.util.id
2930
import org.utbot.framework.plugin.api.util.objectArrayClassId
3031
import org.utbot.framework.plugin.api.util.objectClassId
@@ -398,7 +399,7 @@ class AssociativeArrayWrapper : WrapperInterface {
398399
UtNullModel(objectClassId),
399400
stores = (0 until sizeValue).associateTo(mutableMapOf()) { i ->
400401
val model = touchedValues.stores[i]
401-
val addr = if (model is UtNullModel) 0 else (model as UtReferenceModel).id!!
402+
val addr = model.getIdOrThrow()
402403
addr to resolver.resolveModel(
403404
ObjectValue(
404405
TypeStorage(OBJECT_TYPE),

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,9 @@ import org.utbot.framework.plugin.api.UtCompositeModel
2222
import org.utbot.framework.plugin.api.UtExecutableCallModel
2323
import org.utbot.framework.plugin.api.UtModel
2424
import org.utbot.framework.plugin.api.UtNullModel
25-
import org.utbot.framework.plugin.api.UtReferenceModel
2625
import org.utbot.framework.plugin.api.UtStatementModel
2726
import org.utbot.framework.plugin.api.classId
27+
import org.utbot.framework.plugin.api.getIdOrThrow
2828
import org.utbot.framework.util.graph
2929
import org.utbot.framework.plugin.api.id
3030
import org.utbot.framework.plugin.api.util.booleanClassId
@@ -373,7 +373,7 @@ private fun constructKeysAndValues(keysModel: UtModel, valuesModel: UtModel, siz
373373
keysModel is UtArrayModel && valuesModel is UtArrayModel -> {
374374
List(size) {
375375
keysModel.stores[it].let { model ->
376-
val addr = if (model is UtNullModel) 0 else (model as UtReferenceModel).id
376+
val addr = model.getIdOrThrow()
377377
// as we do not support generics for now, valuesModel.classId.elementClassId is unknown,
378378
// but it can be known with generics support
379379
val defaultValue = UtNullModel(valuesModel.classId.elementClassId ?: objectClassId)

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

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,7 @@ import kotlinx.collections.immutable.persistentListOf
5656
import kotlinx.collections.immutable.persistentSetOf
5757
import kotlinx.collections.immutable.toPersistentList
5858
import kotlinx.collections.immutable.toPersistentMap
59+
import org.utbot.framework.plugin.api.classId
5960
import soot.ArrayType
6061
import soot.BooleanType
6162
import soot.ByteType
@@ -147,7 +148,8 @@ data class Memory( // TODO: split purely symbolic memory and information about s
147148
private val speculativelyNotNullAddresses: UtArrayExpressionBase = UtConstArrayExpression(
148149
UtFalse,
149150
UtArraySort(UtAddrSort, UtBoolSort)
150-
)
151+
),
152+
private val symbolicEnumValues: PersistentList<ObjectValue> = persistentListOf()
151153
) {
152154
val chunkIds: Set<ChunkId>
153155
get() = initial.keys
@@ -297,7 +299,8 @@ data class Memory( // TODO: split purely symbolic memory and information about s
297299
visitedValues = updVisitedValues,
298300
touchedAddresses = updTouchedAddresses,
299301
instanceFieldReadOperations = instanceFieldReadOperations.addAll(update.instanceFieldReads),
300-
speculativelyNotNullAddresses = updSpeculativelyNotNullAddresses
302+
speculativelyNotNullAddresses = updSpeculativelyNotNullAddresses,
303+
symbolicEnumValues = symbolicEnumValues.addAll(update.symbolicEnumValues)
301304
)
302305
}
303306

@@ -307,7 +310,6 @@ data class Memory( // TODO: split purely symbolic memory and information about s
307310
*/
308311
fun memoryForNestedMethod(): Memory = this.copy(updates = MemoryUpdate())
309312

310-
311313
/**
312314
* Returns copy of queued [updates] which consists only of updates of static fields.
313315
* This is necessary for substituting unbounded symbolic variables into the static fields.
@@ -350,6 +352,9 @@ data class Memory( // TODO: split purely symbolic memory and information about s
350352
fun findStaticInstanceOrNull(id: ClassId): ObjectValue? = staticInstanceStorage[id]
351353

352354
fun findTypeForArrayOrNull(addr: UtAddrExpression): ArrayType? = addrToArrayType[addr]
355+
356+
fun getSymbolicEnumValues(classId: ClassId): List<ObjectValue> =
357+
symbolicEnumValues.filter { it.type.classId == classId }
353358
}
354359

355360
/**
@@ -967,7 +972,8 @@ data class MemoryUpdate(
967972
val touchedAddresses: PersistentList<UtAddrExpression> = persistentListOf(),
968973
val classIdToClearStatics: ClassId? = null,
969974
val instanceFieldReads: PersistentSet<InstanceFieldReadOperation> = persistentHashSetOf(),
970-
val speculativelyNotNullAddresses: PersistentList<UtAddrExpression> = persistentListOf()
975+
val speculativelyNotNullAddresses: PersistentList<UtAddrExpression> = persistentListOf(),
976+
val symbolicEnumValues: PersistentList<ObjectValue> = persistentListOf()
971977
) {
972978
operator fun plus(other: MemoryUpdate) =
973979
this.copy(
@@ -986,7 +992,11 @@ data class MemoryUpdate(
986992
classIdToClearStatics = other.classIdToClearStatics,
987993
instanceFieldReads = instanceFieldReads.addAll(other.instanceFieldReads),
988994
speculativelyNotNullAddresses = speculativelyNotNullAddresses.addAll(other.speculativelyNotNullAddresses),
995+
symbolicEnumValues = symbolicEnumValues.addAll(other.symbolicEnumValues),
989996
)
997+
998+
fun getSymbolicEnumValues(classId: ClassId): List<ObjectValue> =
999+
symbolicEnumValues.filter { it.type.classId == classId }
9901000
}
9911001

9921002
// array - Java Array

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

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,7 @@ import kotlin.math.max
7171
import kotlin.math.min
7272
import kotlinx.collections.immutable.persistentListOf
7373
import kotlinx.collections.immutable.persistentSetOf
74+
import org.utbot.framework.plugin.api.SYMBOLIC_NULL_ADDR
7475
import soot.ArrayType
7576
import soot.BooleanType
7677
import soot.ByteType
@@ -324,7 +325,7 @@ class Resolver(
324325
val mockInfoEnriched = mockInfos.getValue(concreteAddr)
325326
val mockInfo = mockInfoEnriched.mockInfo
326327

327-
if (concreteAddr == NULL_ADDR) {
328+
if (concreteAddr == SYMBOLIC_NULL_ADDR) {
328329
return UtNullModel(mockInfo.classId)
329330
}
330331

@@ -436,7 +437,7 @@ class Resolver(
436437

437438
private fun resolveObject(objectValue: ObjectValue): UtModel {
438439
val concreteAddr = holder.concreteAddr(objectValue.addr)
439-
if (concreteAddr == NULL_ADDR) {
440+
if (concreteAddr == SYMBOLIC_NULL_ADDR) {
440441
return UtNullModel(objectValue.type.sootClass.id)
441442
}
442443

@@ -497,7 +498,7 @@ class Resolver(
497498
actualType: RefType,
498499
): UtModel {
499500
val concreteAddr = holder.concreteAddr(addr)
500-
if (concreteAddr == NULL_ADDR) {
501+
if (concreteAddr == SYMBOLIC_NULL_ADDR) {
501502
return UtNullModel(defaultType.sootClass.id)
502503
}
503504

@@ -614,7 +615,7 @@ class Resolver(
614615
val modeledNumDimensions = holder.eval(numDimensionsArray.select(addrExpression)).intValue()
615616

616617
val classRef = classRefByName(modeledType, modeledNumDimensions)
617-
val model = UtClassRefModel(CLASS_REF_CLASS_ID, classRef)
618+
val model = UtClassRefModel(addr, CLASS_REF_CLASS_ID, classRef)
618619
addConstructedModel(addr, model)
619620

620621
return model
@@ -639,7 +640,7 @@ class Resolver(
639640
clazz.enumConstants.indices.random()
640641
}
641642
val value = clazz.enumConstants[index] as Enum<*>
642-
val model = UtEnumConstantModel(clazz.id, value)
643+
val model = UtEnumConstantModel(addr, clazz.id, value)
643644
addConstructedModel(addr, model)
644645

645646
return model
@@ -794,7 +795,7 @@ class Resolver(
794795
*/
795796
private fun constructArrayModel(instance: ArrayValue): UtModel {
796797
val concreteAddr = holder.concreteAddr(instance.addr)
797-
if (concreteAddr == NULL_ADDR) {
798+
if (concreteAddr == SYMBOLIC_NULL_ADDR) {
798799
return UtNullModel(instance.type.id)
799800
}
800801

@@ -828,7 +829,7 @@ class Resolver(
828829
concreteAddr: Address,
829830
details: ArrayExtractionDetails,
830831
): UtModel {
831-
if (concreteAddr == NULL_ADDR) {
832+
if (concreteAddr == SYMBOLIC_NULL_ADDR) {
832833
return UtNullModel(actualType.id)
833834
}
834835

@@ -902,7 +903,7 @@ class Resolver(
902903
elementType: ArrayType,
903904
details: ArrayExtractionDetails
904905
): UtModel {
905-
if (addr == NULL_ADDR) {
906+
if (addr == SYMBOLIC_NULL_ADDR) {
906907
return UtNullModel(elementType.id)
907908
}
908909

@@ -926,7 +927,7 @@ class Resolver(
926927
* Uses [constructTypeOrNull] to evaluate possible element type.
927928
*/
928929
private fun arrayOfObjectsElementModel(concreteAddr: Address, defaultType: RefType): UtModel {
929-
if (concreteAddr == NULL_ADDR) {
930+
if (concreteAddr == SYMBOLIC_NULL_ADDR) {
930931
return UtNullModel(defaultType.id)
931932
}
932933

@@ -975,8 +976,7 @@ private data class ArrayExtractionDetails(
975976
val oneDimensionalArray: UtArrayExpressionBase
976977
)
977978

978-
private const val NULL_ADDR = 0
979-
internal val nullObjectAddr = UtAddrExpression(mkInt(NULL_ADDR))
979+
internal val nullObjectAddr = UtAddrExpression(mkInt(SYMBOLIC_NULL_ADDR))
980980

981981

982982
fun SymbolicValue.isNullObject() =

0 commit comments

Comments
 (0)