Skip to content

Improve UTestValueDescriptor to UtModel conversion and state change asserts generation #2691

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Nov 18, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ import org.utbot.framework.plugin.api.UtNullModel
import org.utbot.framework.plugin.api.UtPrimitiveModel
import org.utbot.framework.plugin.api.UtReferenceModel
import org.utbot.framework.plugin.api.UtVoidModel
import java.util.IdentityHashMap

/**
* Performs deep mapping of [UtModel]s.
Expand All @@ -30,7 +31,7 @@ class UtModelDeepMapper private constructor(
* Values are models that have been deeply mapped by this [UtModelDeepMapper].
* Models are only associated with models of the same type (i.e. the cache type is actually `MutableMap<T, T>`)
*/
private val cache = mutableMapOf<UtModel, UtModel>()
private val cache = IdentityHashMap<UtModel, UtModel>()

private val allInputtedModels get() = cache.keys
private val allOutputtedModels get() = cache.values
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@ import org.utbot.framework.plugin.api.UtPrimitiveModel
import org.utbot.framework.plugin.api.UtReferenceModel
import org.utbot.framework.plugin.api.UtSymbolicExecution
import org.utbot.framework.plugin.api.UtVoidModel
import org.utbot.framework.plugin.api.util.id
import org.utbot.framework.plugin.api.util.isSubtypeOf
import org.utbot.framework.util.UtModelVisitor
import org.utbot.framework.util.hasThisInstance
import org.utbot.fuzzer.UtFuzzedExecution
Expand Down Expand Up @@ -104,31 +106,23 @@ class ExecutionStateAnalyzer(val execution: UtExecution) {
initialPath: FieldPath = FieldPath()
): FieldStatesInfo {
var modelBefore = before
var modelAfter = after

if (before::class != after::class) {
if (before is UtModelWithCompositeOrigin && after is UtModelWithCompositeOrigin && before.origin != null) {
modelBefore = before.origin ?: unreachableBranch("We have already checked the origin for a null value")
} else {
doNotRun {
// it is ok because we might have modelBefore with some absent fields (i.e. statics), but
// modelAfter (constructed by concrete executor) will consist all these fields,
// therefore, AssembleModelGenerator won't be able to transform the given composite model

val reason = if (before is UtModelWithCompositeOrigin && after is UtCompositeModel) {
"ModelBefore is an UtModelWithOrigin and ModelAfter " +
"is a CompositeModel, but modelBefore doesn't have an origin model."
} else {
"The model before and the model after have different types: " +
"model before is ${before::class}, but model after is ${after::class}."
}
if (before is UtModelWithCompositeOrigin)
modelBefore = before.origin ?: before
if (after is UtModelWithCompositeOrigin)
modelAfter = after.origin ?: after
}

error("Cannot analyze fields modification. $reason")
}
if (modelBefore::class != modelAfter::class) {
doNotRun {
error("Cannot analyze model fields modification, before: [$before], after: [$after]")
}

// remove it when we will fix assemble models in the resolver JIRA:1464
workaround(WorkaroundReason.IGNORE_MODEL_TYPES_INEQUALITY) {
return FieldStatesInfo(fieldsBefore = emptyMap(), fieldsAfter = emptyMap())
}
// remove it when we will fix assemble models in the resolver JIRA:1464
workaround(WorkaroundReason.IGNORE_MODEL_TYPES_INEQUALITY) {
return FieldStatesInfo(fieldsBefore = emptyMap(), fieldsAfter = emptyMap())
}
}

Expand All @@ -139,7 +133,7 @@ class ExecutionStateAnalyzer(val execution: UtExecution) {
modelBefore.accept(FieldStateVisitor(), dataBefore)

val dataAfter = FieldData(FieldsVisitorMode.AFTER, fieldsAfter, initialPath, previousFields = fieldsBefore)
after.accept(FieldStateVisitor(), dataAfter)
modelAfter.accept(FieldStateVisitor(), dataAfter)

return FieldStatesInfo(fieldsBefore, fieldsAfter)
}
Expand Down Expand Up @@ -260,6 +254,13 @@ private class FieldStateVisitor : UtModelVisitor<FieldData>() {
// sometimes we don't have initial state of the field, e.g. if it is static and we didn't `touch` it
// during the analysis, but the concrete executor included it in the modelAfter
val initial = previousFields[path] ?: return false

// TODO usvm-sbft: In USVM descriptors for classes, enums, and throwables don't implement `UTestRefDescriptor`
// and don't have `refId`, which causes `UtReferenceModel.id` to diverge in `stateBefore` and `stateAfter`
if (initial is UtClassRefModel) return initial.value != ((model as? UtClassRefModel)?.value)
if (initial is UtEnumConstantModel) return initial.value != ((model as? UtEnumConstantModel)?.value)
if (initial.classId isSubtypeOf java.lang.Throwable::class.id) return initial.classId != model.classId

return initial != model
}
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
package org.utbot.contest.usvm

enum class EnvironmentStateKind {
INITIAL, FINAL
}
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ import org.utbot.framework.plugin.api.Coverage
import org.utbot.framework.plugin.api.EnvironmentModels
import org.utbot.framework.plugin.api.ExecutableId
import org.utbot.framework.plugin.api.Instruction
import org.utbot.framework.plugin.api.UtArrayModel
import org.utbot.framework.plugin.api.UtAssembleModel
import org.utbot.framework.plugin.api.UtExecutableCallModel
import org.utbot.framework.plugin.api.UtExecution
Expand All @@ -34,12 +35,14 @@ import org.utbot.framework.plugin.api.UtExplicitlyThrownException
import org.utbot.framework.plugin.api.UtImplicitlyThrownException
import org.utbot.framework.plugin.api.UtInstrumentation
import org.utbot.framework.plugin.api.UtPrimitiveModel
import org.utbot.framework.plugin.api.UtStatementCallModel
import org.utbot.framework.plugin.api.UtVoidModel
import org.utbot.framework.plugin.api.mapper.UtModelDeepMapper
import org.utbot.framework.plugin.api.util.executableId
import org.utbot.framework.plugin.api.util.jClass
import org.utbot.framework.plugin.api.util.utContext
import org.utbot.fuzzer.IdGenerator
import java.util.IdentityHashMap

private val logger = KotlinLogging.logger {}

Expand Down Expand Up @@ -68,17 +71,19 @@ class JcToUtExecutionConverter(

val utUsvmExecution: UtUsvmExecution = when (val executionResult = jcExecution.uTestExecutionResult) {
is UTestExecutionSuccessResult -> UtUsvmExecution(
stateBefore = convertState(executionResult.initialState, jcExecution.method, jcToUtModelConverter),
stateAfter = convertState(executionResult.resultState, jcExecution.method, jcToUtModelConverter),
stateBefore = convertState(executionResult.initialState, EnvironmentStateKind.INITIAL, jcExecution.method),
stateAfter = convertState(executionResult.resultState, EnvironmentStateKind.FINAL, jcExecution.method),
// TODO usvm-sbft: ask why `UTestExecutionSuccessResult.result` is nullable
result = UtExecutionSuccess(executionResult.result?.let { jcToUtModelConverter.convert(it) } ?: UtVoidModel),
result = UtExecutionSuccess(executionResult.result?.let {
jcToUtModelConverter.convert(it, EnvironmentStateKind.FINAL)
} ?: UtVoidModel),
coverage = coverage,
instrumentation = instrumentation,
)
is UTestExecutionExceptionResult -> {
UtUsvmExecution(
stateBefore = convertState(executionResult.initialState, jcExecution.method, jcToUtModelConverter),
stateAfter = convertState(executionResult.resultState, jcExecution.method, jcToUtModelConverter),
stateBefore = convertState(executionResult.initialState, EnvironmentStateKind.INITIAL, jcExecution.method),
stateAfter = convertState(executionResult.resultState, EnvironmentStateKind.FINAL, jcExecution.method),
result = createExecutionFailureResult(
executionResult.cause,
jcExecution.method,
Expand Down Expand Up @@ -108,7 +113,10 @@ class JcToUtExecutionConverter(
}
} ?: return null

return utUsvmExecution.mapModels(constructAssemblingMapper())
return utUsvmExecution
.mapModels(constructAssemblingMapper())
.mapModels(constructAssembleToCompositeModelMapper())
.mapModels(constructConstArrayModelMapper())
}

private fun constructAssemblingMapper(): UtModelDeepMapper = UtModelDeepMapper { model ->
Expand Down Expand Up @@ -145,6 +153,31 @@ class JcToUtExecutionConverter(
} ?: model
}

private fun constructConstArrayModelMapper(): UtModelDeepMapper = UtModelDeepMapper { model ->
if (model is UtArrayModel) {
val storeGroups = model.stores.entries.groupByTo(IdentityHashMap()) { it.value }
val mostCommonStore = storeGroups.maxBy { it.value.size }
if (mostCommonStore.value.size > 1) {
model.constModel = mostCommonStore.key
mostCommonStore.value.forEach { (index, _) -> model.stores.remove(index) }
}
}
model
}

private fun constructAssembleToCompositeModelMapper(): UtModelDeepMapper = UtModelDeepMapper { model ->
if (model is UtAssembleModel
&& utilMethodProvider.createInstanceMethodId == model.instantiationCall.statement
&& model.modificationsChain.all {
utilMethodProvider.setFieldMethodId == (it as? UtStatementCallModel)?.statement
}
) {
model.origin ?: model
} else {
model
}
}

private fun convertException(exceptionDescriptor: UTestExceptionDescriptor): Throwable =
toValueConverter.buildObjectFromDescriptor(exceptionDescriptor.dropStaticFields(
cache = mutableMapOf()
Expand All @@ -160,18 +193,20 @@ class JcToUtExecutionConverter(

private fun convertState(
state: UTestExecutionState,
stateKind: EnvironmentStateKind,
method: JcTypedMethod,
modelConverter: JcToUtModelConverter,
): EnvironmentModels {
): EnvironmentModels {
val thisInstance =
if (method.isStatic) null
else if (method.method.isConstructor) null
else modelConverter.convert(state.instanceDescriptor ?: error("Unexpected null instanceDescriptor"))
val parameters = state.argsDescriptors.map { modelConverter.convert(it ?: error("Unexpected null argDescriptor")) }
else jcToUtModelConverter.convert(state.instanceDescriptor ?: error("Unexpected null instanceDescriptor"), stateKind)
val parameters = state.argsDescriptors.map {
jcToUtModelConverter.convert(it ?: error("Unexpected null argDescriptor"), stateKind)
}
val statics = state.statics
.entries
.associate { (jcField, uTestDescr) ->
jcField.fieldId to modelConverter.convert(uTestDescr)
jcField.fieldId to jcToUtModelConverter.convert(uTestDescr, stateKind)
}
val executableId: ExecutableId = method.method.toExecutableId(jcClasspath)
return EnvironmentModels(thisInstance, parameters, statics, executableId)
Expand Down
Loading