From 5941abd21b5cf9a8053c7a38b2f5361f7121c0e2 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Fri, 10 Nov 2023 17:43:51 +0100 Subject: [PATCH 1/2] optimize trace collector, so it only collects concrete values on request --- .../transform/SymbolicTraceInstrumenter.kt | 15 +++ .../research/kex/descriptor/converter.kt | 40 +++++++ .../symbolic/InstructionTraceCollector.kt | 2 + .../kex/trace/symbolic/SymbolicState.kt | 25 ++-- .../trace/symbolic/SymbolicTraceBuilder.kt | 109 +++++++++++------- .../kex/trace/symbolic/TraceCollectorProxy.kt | 6 +- .../kex/launcher/WorkerLauncherDebug.kt | 2 +- .../analysis/concolic/bfs/BfsPathSelector.kt | 5 +- .../concolic/cgs/ContextGuidedSelector.kt | 3 +- .../analysis/concolic/gui/GUIProxySelector.kt | 3 +- .../kex/asm/analysis/util/extensions.kt | 12 +- 11 files changed, 157 insertions(+), 65 deletions(-) diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/transform/SymbolicTraceInstrumenter.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/transform/SymbolicTraceInstrumenter.kt index 644b65717..219d43d60 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/transform/SymbolicTraceInstrumenter.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/transform/SymbolicTraceInstrumenter.kt @@ -839,6 +839,21 @@ class SymbolicTraceInstrumenter( inst.insertAfter(after.mapLocation()) } + private fun track(value: Value): List = buildList { + val trackMethod = collectorClass.getMethod( + "track", types.voidType, stringType, objectType + ) + add( + collectorClass.interfaceCall( + trackMethod, traceCollector, + listOf( + "$value".asValue, + value.wrapped(this) + ) + ) + ) + } + private fun addNullityConstraint(inst: Instruction, value: Value): List = buildList { if (inst.parent.method.isConstructor && value is ThisRef) return@buildList diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt index 4658e91ac..d66453854 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt @@ -11,7 +11,11 @@ import org.vorpal.research.kex.ktype.KexDouble import org.vorpal.research.kex.ktype.KexFloat import org.vorpal.research.kex.ktype.KexInt import org.vorpal.research.kex.ktype.KexLong +import org.vorpal.research.kex.ktype.KexNull import org.vorpal.research.kex.ktype.KexShort +import org.vorpal.research.kex.ktype.KexString +import org.vorpal.research.kex.ktype.KexType +import org.vorpal.research.kex.ktype.asArray import org.vorpal.research.kex.util.allFields import org.vorpal.research.kex.util.isStatic import org.vorpal.research.kex.util.kex @@ -31,6 +35,42 @@ private val maxArrayLength by lazy { class Object2DescriptorConverter : DescriptorBuilder() { private val objectToDescriptor = IdentityHashMap() + fun type(any: Any?): KexType { + if (any == null) return KexNull() + + return when (any.javaClass) { + Boolean::class.javaObjectType -> KexClass(SystemTypeNames.booleanClass) + Byte::class.javaObjectType -> KexClass(SystemTypeNames.byteClass) + Char::class.javaObjectType -> KexClass(SystemTypeNames.charClass) + Short::class.javaObjectType -> KexClass(SystemTypeNames.shortClass) + Int::class.javaObjectType -> KexClass(SystemTypeNames.integerClass) + Long::class.javaObjectType -> KexClass(SystemTypeNames.longClass) + Float::class.javaObjectType -> KexClass(SystemTypeNames.floatClass) + Double::class.javaObjectType -> KexClass(SystemTypeNames.doubleClass) + else -> when (any) { + is Boolean -> KexBool + is Byte -> KexByte + is Char -> KexChar + is Short -> KexShort + is Int -> KexInt + is Long -> KexLong + is Float -> KexFloat + is Double -> KexDouble + is BooleanArray -> KexBool.asArray() + is ByteArray -> KexByte.asArray() + is CharArray -> KexChar.asArray() + is ShortArray -> KexShort.asArray() + is IntArray -> KexInt.asArray() + is LongArray -> KexLong.asArray() + is FloatArray -> KexFloat.asArray() + is DoubleArray -> KexDouble.asArray() + is Array<*> -> any.javaClass.componentType.kex + is String -> KexString() + else -> any.javaClass.kex + } + } + } + fun convert(any: Any?, depth: Int = 0): Descriptor { if (any == null) return `null` if (any in objectToDescriptor) return objectToDescriptor[any]!! diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/InstructionTraceCollector.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/InstructionTraceCollector.kt index 5f6f9af21..3bba8c568 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/InstructionTraceCollector.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/InstructionTraceCollector.kt @@ -3,6 +3,8 @@ package org.vorpal.research.kex.trace.symbolic interface InstructionTraceCollector { val symbolicState: SymbolicState + fun track(value: String, concreteValue: Any?) + fun methodEnter( className: String, methodName: String, diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt index b5e5a6248..4cb1ce7a5 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt @@ -12,6 +12,7 @@ import kotlinx.serialization.Contextual import kotlinx.serialization.SerialName import kotlinx.serialization.Serializable import org.vorpal.research.kex.descriptor.Descriptor +import org.vorpal.research.kex.ktype.KexType import org.vorpal.research.kex.state.BasicState import org.vorpal.research.kex.state.predicate.Predicate import org.vorpal.research.kex.state.term.Term @@ -276,7 +277,8 @@ data class WrappedValue(val method: @Contextual Method, val value: @Contextual V abstract class SymbolicState { abstract val clauses: ClauseList abstract val path: PathCondition - abstract val concreteValueMap: Map + abstract val concreteTypes: Map + abstract val concreteValues: Map abstract val termMap: Map operator fun get(term: Term) = termMap.getValue(term) @@ -298,13 +300,15 @@ abstract class SymbolicState { internal data class SymbolicStateImpl( override val clauses: ClauseList, override val path: PathCondition, - override val concreteValueMap: @Contextual Map, + override val concreteTypes: @Contextual Map, + override val concreteValues: @Contextual Map, override val termMap: @Contextual Map, ) : SymbolicState() { override fun plus(other: SymbolicState): SymbolicState = SymbolicStateImpl( clauses = clauses + other.clauses, path = path + other.path, - concreteValueMap = concreteValueMap + other.concreteValueMap, + concreteTypes = concreteTypes + other.concreteTypes, + concreteValues = concreteValues + other.concreteValues, termMap = termMap + other.termMap ) override fun plus(other: StateClause): SymbolicState = copy( @@ -330,7 +334,8 @@ internal data class SymbolicStateImpl( data class PersistentSymbolicState( override val clauses: PersistentClauseList, override val path: PersistentPathCondition, - override val concreteValueMap: @Contextual PersistentMap, + override val concreteTypes: @Contextual PersistentMap, + override val concreteValues: @Contextual PersistentMap, override val termMap: @Contextual PersistentMap, ) : SymbolicState() { override fun toString() = clauses.joinToString("\n") { it.predicate.toString() } @@ -338,7 +343,8 @@ data class PersistentSymbolicState( override fun plus(other: SymbolicState): PersistentSymbolicState = PersistentSymbolicState( clauses = clauses + other.clauses, path = path + other.path, - concreteValueMap = concreteValueMap.putAll(other.concreteValueMap), + concreteTypes = concreteTypes.putAll(other.concreteTypes), + concreteValues = concreteValues.putAll(other.concreteValues), termMap = termMap.putAll(other.termMap) ) override fun plus(other: StateClause): PersistentSymbolicState = copy( @@ -359,19 +365,21 @@ data class PersistentSymbolicState( fun symbolicState( state: ClauseList = ClauseListImpl(), path: PathCondition = PathConditionImpl(), + concreteTypeMap: Map = emptyMap(), concreteValueMap: Map = emptyMap(), termMap: Map = emptyMap(), ): SymbolicState = SymbolicStateImpl( - state, path, concreteValueMap, termMap + state, path, concreteTypeMap, concreteValueMap, termMap ) fun persistentSymbolicState( state: PersistentClauseList = PersistentClauseList(), path: PersistentPathCondition = PersistentPathCondition(), + concreteTypeMap: PersistentMap = persistentMapOf(), concreteValueMap: PersistentMap = persistentMapOf(), termMap: PersistentMap = persistentMapOf(), ): PersistentSymbolicState = PersistentSymbolicState( - state, path, concreteValueMap, termMap + state, path, concreteTypeMap, concreteValueMap, termMap ) fun List.toClauseState(): ClauseList = ClauseListImpl(this.toList()) @@ -401,7 +409,8 @@ fun SymbolicState.toPersistentState(): PersistentSymbolicState = when (this) { else -> PersistentSymbolicState( this.clauses.toPersistentClauseState(), this.path.toPersistentPathCondition(), - this.concreteValueMap.toPersistentMap(), + this.concreteTypes.toPersistentMap(), + this.concreteValues.toPersistentMap(), this.termMap.toPersistentMap() ) } diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicTraceBuilder.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicTraceBuilder.kt index b8f464dbf..e7b5f4880 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicTraceBuilder.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicTraceBuilder.kt @@ -111,8 +111,10 @@ class SymbolicTraceBuilder( get() = stateBuilder.toClauseState() override val path: PathCondition get() = pathBuilder.toPathCondition() - override val concreteValueMap: Map - get() = concreteValues.toMap() + override val concreteTypes: Map + get() = concreteTypeMap.toMap() + override val concreteValues: Map + get() = concreteValueMap.toMap() override val termMap: Map get() = terms.toMap() @@ -122,7 +124,8 @@ class SymbolicTraceBuilder( return SymbolicStateImpl( clauses, path, - concreteValueMap, + concreteTypes, + concreteValues, termMap ) } @@ -135,7 +138,8 @@ class SymbolicTraceBuilder( private val stateBuilder = arrayListOf() private val traceBuilder = arrayListOf() private val pathBuilder = arrayListOf() - private val concreteValues = mutableMapOf() + private val concreteTypeMap = mutableMapOf() + private val concreteValueMap = mutableMapOf() private val terms = mutableMapOf() private val nullChecked = mutableSetOf() @@ -374,16 +378,26 @@ class SymbolicTraceBuilder( else -> this } + private fun KexType.unwrapped(type: KexType) = when (type) { + is KexInteger, is KexReal -> when (this) { + is KexClass -> type + else -> this + } + else -> this + } + private fun Value.wrapped(): WrappedValue = WrappedValue(currentMethod, this) - private fun Term.updateInfo(value: Value, concreteValue: Descriptor) { + private fun Term.updateInfo(value: Value, concreteType: KexType) { terms.getOrPut(this) { value.wrapped() } - concreteValues.getOrPut(this) { concreteValue } + concreteTypeMap[this] = concreteType } private fun Any?.getAsDescriptor() = converter.convert(this) private fun Any?.getAsDescriptor(type: KexType) = converter.convert(this).unwrapped(type) + private fun Any?.getConcreteType(type: KexType): KexType = converter.type(this).unwrapped(type) + private val Method.parameterValues: Parameters get() = Parameters( if (!isStatic) ctx.values.getThis(klass) else null, @@ -402,6 +416,13 @@ class SymbolicTraceBuilder( else -> true } + override fun track(value: String, concreteValue: Any?) { + val kfgValue = parseValue(value) + val termValue = mkValue(kfgValue) + val descriptor = concreteValue.getAsDescriptor(termValue.type) + concreteValueMap[termValue] = descriptor + } + override fun methodEnter( className: String, methodName: String, @@ -430,7 +451,7 @@ class SymbolicTraceBuilder( for ((index, argType) in method.argTypes.withIndex()) { val argValue = cm.value.getArgument(index, method, argType) val argTerm = mkNewValue(argValue) - concreteValues[argTerm] = args[index].getAsDescriptor() + concreteTypeMap[argTerm] = args[index].getConcreteType(argTerm.type) } } } @@ -534,10 +555,10 @@ class SymbolicTraceBuilder( val termIndex = mkValue(kfgIndex) terms[termValue] = kfgValue.wrapped() - concreteValues[termValue] = concreteValue.getAsDescriptor(termValue.type) + concreteTypeMap[termValue] = concreteValue.getConcreteType(termValue.type) - termRef.updateInfo(kfgRef, concreteRef.getAsDescriptor(termRef.type)) - termIndex.updateInfo(kfgIndex, concreteIndex.getAsDescriptor(termIndex.type)) + termRef.updateInfo(kfgRef, concreteRef.getConcreteType(termRef.type)) + termIndex.updateInfo(kfgIndex, concreteIndex.getConcreteType(termIndex.type)) val predicate = state(kfgValue.location) { termValue equality termRef[termIndex].load() @@ -569,9 +590,9 @@ class SymbolicTraceBuilder( val termIndex = mkValue(kfgIndex) val termValue = mkValue(kfgValue) - termRef.updateInfo(kfgRef, concreteRef.getAsDescriptor(termRef.type)) - termIndex.updateInfo(kfgIndex, concreteIndex.getAsDescriptor(termIndex.type)) - termValue.updateInfo(kfgValue, concreteValue.getAsDescriptor(termValue.type)) + termRef.updateInfo(kfgRef, concreteRef.getConcreteType(termRef.type)) + termIndex.updateInfo(kfgIndex, concreteIndex.getConcreteType(termIndex.type)) + termValue.updateInfo(kfgValue, concreteValue.getConcreteType(termValue.type)) val predicate = state(instruction.location) { termRef[termIndex].store(termValue) @@ -602,10 +623,10 @@ class SymbolicTraceBuilder( val termRhv = mkValue(kfgRhv) terms[termValue] = kfgValue.wrapped() - concreteValues[termValue] = concreteValue.getAsDescriptor(termValue.type) + concreteTypeMap[termValue] = concreteValue.getConcreteType(termValue.type) - termLhv.updateInfo(kfgLhv, concreteLhv.getAsDescriptor(termLhv.type)) - termRhv.updateInfo(kfgRhv, concreteRhv.getAsDescriptor(termRhv.type)) + termLhv.updateInfo(kfgLhv, concreteLhv.getConcreteType(termLhv.type)) + termRhv.updateInfo(kfgRhv, concreteRhv.getConcreteType(termRhv.type)) val predicate = state(kfgValue.location) { termValue equality termLhv.apply(cm.type, kfgValue.opcode, termRhv) @@ -626,7 +647,7 @@ class SymbolicTraceBuilder( val kfgCondition = parseValue(condition) val termCondition = mkValue(kfgCondition) - val booleanValue = (concreteValues[termCondition] as? ConstantDescriptor.Bool)?.value + val booleanValue = (concreteValueMap[termCondition] as? ConstantDescriptor.Bool)?.value ?: unreachable { log.error("Unknown boolean value in branch") } val predicate = path(instruction.location) { @@ -670,7 +691,7 @@ class SymbolicTraceBuilder( terms.getOrPut(this) { kfgCallee.wrapped() } } termArguments.withIndex().forEach { (index, term) -> - term.updateInfo(kfgArguments[index], concreteArguments[index].getAsDescriptor(term.type)) + term.updateInfo(kfgArguments[index], concreteArguments[index].getConcreteType(term.type)) } val predicate = state(instruction.location) { @@ -713,9 +734,9 @@ class SymbolicTraceBuilder( val termOperand = mkValue(kfgOperand) terms[termValue] = kfgValue.wrapped() - concreteValues[termValue] = concreteValue.getAsDescriptor(termValue.type) + concreteTypeMap[termValue] = concreteValue.getConcreteType(termValue.type) - termOperand.updateInfo(kfgOperand, concreteOperand.getAsDescriptor(termOperand.type)) + termOperand.updateInfo(kfgOperand, concreteOperand.getConcreteType(termOperand.type)) copyTermInfo(termOperand, termValue) val predicate = state(kfgValue.location) { @@ -741,7 +762,8 @@ class SymbolicTraceBuilder( val termException = thrownException ?: mkNewValue(kfgException) terms[termException] = kfgException.wrapped() - concreteValues[termException] = exceptionDescriptor + concreteTypeMap[termException] = exceptionDescriptor.type + concreteValueMap[termException] = exceptionDescriptor val predicate = state(kfgException.location) { catch(termException) @@ -773,10 +795,11 @@ class SymbolicTraceBuilder( val termRhv = mkValue(kfgRhv) terms[termValue] = kfgValue.wrapped() - concreteValues[termValue] = concreteLhv.cmp(kfgValue.opcode, concreteRhv).getAsDescriptor(termValue.type) + concreteValueMap[termValue] = concreteLhv.cmp(kfgValue.opcode, concreteRhv).getAsDescriptor(termValue.type) + concreteTypeMap[termValue] = concreteLhv.cmp(kfgValue.opcode, concreteRhv).getConcreteType(termValue.type) - termLhv.updateInfo(kfgLhv, concreteLhv.getAsDescriptor(termLhv.type)) - termRhv.updateInfo(kfgRhv, concreteRhv.getAsDescriptor(termRhv.type)) + termLhv.updateInfo(kfgLhv, concreteLhv.getConcreteType(termLhv.type)) + termRhv.updateInfo(kfgRhv, concreteRhv.getConcreteType(termRhv.type)) val predicate = state(kfgValue.location) { termValue equality termLhv.apply(kfgValue.opcode, termRhv) @@ -798,7 +821,7 @@ class SymbolicTraceBuilder( val kfgMonitor = parseValue(operand) val termMonitor = mkValue(kfgMonitor) - termMonitor.updateInfo(kfgMonitor, concreteOperand.getAsDescriptor(termMonitor.type)) + termMonitor.updateInfo(kfgMonitor, concreteOperand.getConcreteType(termMonitor.type)) val predicate = state(instruction.location) { enterMonitor(termMonitor) @@ -820,7 +843,7 @@ class SymbolicTraceBuilder( val kfgMonitor = parseValue(operand) val termMonitor = mkValue(kfgMonitor) - termMonitor.updateInfo(kfgMonitor, concreteOperand.getAsDescriptor(termMonitor.type)) + termMonitor.updateInfo(kfgMonitor, concreteOperand.getConcreteType(termMonitor.type)) val predicate = state(instruction.location) { exitMonitor(termMonitor) @@ -851,9 +874,9 @@ class SymbolicTraceBuilder( val termOwner = kfgOwner?.let { mkValue(it) } terms[termValue] = kfgValue.wrapped() - concreteValues[termValue] = concreteValue.getAsDescriptor(termValue.type) + concreteTypeMap[termValue] = concreteValue.getConcreteType(termValue.type) - termOwner?.apply { this.updateInfo(kfgOwner, concreteOwner.getAsDescriptor(termOwner.type)) } + termOwner?.apply { this.updateInfo(kfgOwner, concreteOwner.getConcreteType(termOwner.type)) } if (kfgField.isOuterThis()) { nullChecked += termValue } @@ -889,8 +912,8 @@ class SymbolicTraceBuilder( val termOwner = kfgOwner?.let { mkValue(it) } val termValue = mkValue(kfgValue) - termOwner?.apply { this.updateInfo(kfgOwner, concreteOwner.getAsDescriptor(termOwner.type)) } - termValue.updateInfo(kfgValue, concreteValue.getAsDescriptor(termValue.type)) + termOwner?.apply { this.updateInfo(kfgOwner, concreteOwner.getConcreteType(termOwner.type)) } + termValue.updateInfo(kfgValue, concreteValue.getConcreteType(termValue.type)) val predicate = state(instruction.location) { val actualOwner = termOwner ?: staticRef(kfgField.klass) @@ -918,9 +941,9 @@ class SymbolicTraceBuilder( val termOperand = mkValue(kfgOperand) terms[termValue] = kfgValue.wrapped() - concreteValues[termValue] = concreteValue.getAsDescriptor(termValue.type) + concreteTypeMap[termValue] = concreteValue.getConcreteType(termValue.type) - termOperand.updateInfo(kfgOperand, concreteOperand.getAsDescriptor(termOperand.type)) + termOperand.updateInfo(kfgOperand, concreteOperand.getConcreteType(termOperand.type)) val predicate = state(kfgValue.location) { termValue equality (termOperand `is` kfgValue.targetType.kexType) @@ -947,10 +970,10 @@ class SymbolicTraceBuilder( val termOperands = kfgOperands.map { mkValue(it) } terms[termValue] = kfgValue.wrapped() - concreteValues[termValue] = concreteValue.getAsDescriptor(termValue.type) + concreteTypeMap[termValue] = concreteValue.getConcreteType(termValue.type) termOperands.withIndex().forEach { (index, term) -> - term.updateInfo(kfgOperands[index], concreteOperands[index].getAsDescriptor(term.type)) + term.updateInfo(kfgOperands[index], concreteOperands[index].getConcreteType(term.type)) } val predicate = state(kfgValue.location) { @@ -1011,10 +1034,10 @@ class SymbolicTraceBuilder( nullChecked += termValue typeChecked[termValue] = kfgValue.type terms[termValue] = kfgValue.wrapped() - concreteValues[termValue] = concreteValue.getAsDescriptor(termValue.type) + concreteTypeMap[termValue] = concreteValue.getConcreteType(termValue.type) termDimensions.withIndex().forEach { (index, term) -> - term.updateInfo(kfgDimensions[index], concreteDimensions[index].getAsDescriptor(term.type)) + term.updateInfo(kfgDimensions[index], concreteDimensions[index].getConcreteType(term.type)) } val predicate = state(kfgValue.location) { @@ -1063,7 +1086,7 @@ class SymbolicTraceBuilder( terms[termValue] = kfgValue.wrapped() terms[termIncoming] = kfgIncoming.wrapped() - concreteValues[termValue] = concreteValue.getAsDescriptor(termValue.type) + concreteTypeMap[termValue] = concreteValue.getConcreteType(termValue.type) val predicate = state(kfgValue.location) { termValue equality termIncoming @@ -1095,7 +1118,7 @@ class SymbolicTraceBuilder( termReceiver equality termReturn } terms[termReceiver] = kfgReceiver.wrapped() - concreteValues[termReceiver] = concreteValue.getAsDescriptor(termReceiver.type) + concreteTypeMap[termReceiver] = concreteValue.getConcreteType(termReceiver.type) stateBuilder += StateClause(instruction, predicate) } @@ -1135,7 +1158,7 @@ class SymbolicTraceBuilder( val intValue = numericValue(concreteValue).toInt() val kfgConstant = ctx.values.getInt(intValue) - termValue.updateInfo(kfgValue, concreteValue.getAsDescriptor(termValue.type)) + termValue.updateInfo(kfgValue, concreteValue.getConcreteType(termValue.type)) val predicate = path(instruction.location) { if (kfgConstant in instruction.branches) termValue equality intValue @@ -1161,7 +1184,7 @@ class SymbolicTraceBuilder( val termValue = mkValue(kfgValue) val intValue = numericValue(concreteValue).toInt() - termValue.updateInfo(kfgValue, concreteValue.getAsDescriptor(termValue.type)) + termValue.updateInfo(kfgValue, concreteValue.getConcreteType(termValue.type)) val predicate = path(instruction.location) { termValue equality intValue @@ -1185,7 +1208,7 @@ class SymbolicTraceBuilder( val kfgException = parseValue(exception) val termException = mkValue(kfgException) - termException.updateInfo(kfgException, concreteException.getAsDescriptor(termException.type)) + termException.updateInfo(kfgException, concreteException.getConcreteType(termException.type)) val predicate = state(instruction.location) { `throw`(termException) @@ -1214,9 +1237,9 @@ class SymbolicTraceBuilder( val termOperand = mkValue(kfgOperand) terms[termValue] = kfgValue.wrapped() - concreteValues[termValue] = concreteValue.getAsDescriptor(termValue.type) + concreteTypeMap[termValue] = concreteValue.getConcreteType(termValue.type) - termOperand.updateInfo(kfgOperand, concreteOperand.getAsDescriptor(termOperand.type)) + termOperand.updateInfo(kfgOperand, concreteOperand.getConcreteType(termOperand.type)) val predicate = state(kfgValue.location) { termValue equality termOperand.apply(kfgValue.opcode) diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/TraceCollectorProxy.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/TraceCollectorProxy.kt index 73badd8c4..4f890c8c0 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/TraceCollectorProxy.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/TraceCollectorProxy.kt @@ -4,6 +4,7 @@ import kotlinx.serialization.ExperimentalSerializationApi import kotlinx.serialization.InternalSerializationApi import org.vorpal.research.kex.ExecutionContext import org.vorpal.research.kex.descriptor.Descriptor +import org.vorpal.research.kex.ktype.KexType import org.vorpal.research.kex.serialization.KexSerializer import org.vorpal.research.kex.state.term.Term import org.vorpal.research.kfg.ir.value.NameMapperContext @@ -14,7 +15,8 @@ private class EmptyTraceCollector : InstructionTraceCollector { class EmptyState : SymbolicState() { override val clauses = ClauseListImpl() override val path = PathConditionImpl() - override val concreteValueMap = emptyMap() + override val concreteTypes = emptyMap() + override val concreteValues = emptyMap() override val termMap = emptyMap() override fun plus(other: SymbolicState): SymbolicState = other @@ -26,6 +28,8 @@ private class EmptyTraceCollector : InstructionTraceCollector { override val symbolicState = EmptyState() + override fun track(value: String, concreteValue: Any?) {} + override fun methodEnter( className: String, methodName: String, diff --git a/kex-executor/src/main/kotlin/org/vorpal/research/kex/launcher/WorkerLauncherDebug.kt b/kex-executor/src/main/kotlin/org/vorpal/research/kex/launcher/WorkerLauncherDebug.kt index da7773165..23b7bc512 100644 --- a/kex-executor/src/main/kotlin/org/vorpal/research/kex/launcher/WorkerLauncherDebug.kt +++ b/kex-executor/src/main/kotlin/org/vorpal/research/kex/launcher/WorkerLauncherDebug.kt @@ -109,7 +109,7 @@ class WorkerLauncherDebug(args: Array) { override suspend fun receive(): TestExecutionRequest { return TestExecutionRequest( - "org.apache.commons.collections4.map.LinkedMap_init_20033568880", + "org.vorpal.research.kex.test.concolic.ListConcolicTests_testArrayList_21314842770", testMethod = "test", setupMethod = "setup" ) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt index cdfa19ac9..34cda0c9e 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt @@ -14,8 +14,8 @@ import org.vorpal.research.kex.trace.symbolic.PersistentClauseList import org.vorpal.research.kex.trace.symbolic.PersistentPathCondition import org.vorpal.research.kex.trace.symbolic.PersistentSymbolicState import org.vorpal.research.kex.trace.symbolic.persistentSymbolicState -import org.vorpal.research.kex.trace.symbolic.toPersistentState import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionCompletedResult +import org.vorpal.research.kex.trace.symbolic.toPersistentState import org.vorpal.research.kfg.ir.Method import org.vorpal.research.kfg.ir.value.IntConstant import org.vorpal.research.kfg.ir.value.instruction.BranchInst @@ -61,7 +61,8 @@ class BfsPathSelectorImpl( val new = persistentSymbolicState( currentState + reversed, newPath, - state.concreteValueMap, + state.concreteTypes, + state.concreteValues, state.termMap ) deque += new diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt index cc267cb38..b4b733b48 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt @@ -88,7 +88,8 @@ class ContextGuidedSelector( return persistentSymbolicState( state, currentState.path + currentState.revertedClause, - currentStateState.concreteValueMap, + currentStateState.concreteTypes, + currentStateState.concreteValues, currentStateState.termMap ) } diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt index c6dee7355..49ebf1a7c 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt @@ -75,7 +75,8 @@ class GUIProxySelector(private val concolicPathSelector: ConcolicPathSelector) : return persistentSymbolicState( clauses, path + revertedClause, - state.concreteValueMap, + state.concreteTypes, + state.concreteValues, state.termMap ) } diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/util/extensions.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/util/extensions.kt index 47cfcf6d8..ad87dffe7 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/util/extensions.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/util/extensions.kt @@ -57,8 +57,7 @@ suspend fun Method.checkAsync( val checker = AsyncChecker(this, ctx) val clauses = state.clauses.asState() val query = state.path.asState() - val concreteTypeInfo = state.concreteValueMap - .mapValues { it.value.type } + val concreteTypeInfo = state.concreteTypes .filterValues { it.isJavaRt } .mapValues { it.value.rtMapped } .toTypeMap() @@ -89,8 +88,7 @@ suspend fun Method.checkAsyncAndSlice( val checker = AsyncChecker(this, ctx) val clauses = state.clauses.asState() val query = state.path.asState() - val concreteTypeInfo = state.concreteValueMap - .mapValues { it.value.type } + val concreteTypeInfo = state.concreteTypes .filterValues { it.isJavaRt } .mapValues { it.value.rtMapped } .toTypeMap() @@ -132,8 +130,7 @@ suspend fun Method.checkAsyncIncremental( val checker = AsyncIncrementalChecker(this, ctx) val clauses = state.clauses.asState() val query = state.path.asState() - val concreteTypeInfo = state.concreteValueMap - .mapValues { it.value.type } + val concreteTypeInfo = state.concreteTypes .filterValues { it.isJavaRt } .mapValues { it.value.rtMapped } .toTypeMap() @@ -179,8 +176,7 @@ suspend fun Method.checkAsyncIncrementalAndSlice( val checker = AsyncIncrementalChecker(this, ctx) val clauses = state.clauses.asState() val query = state.path.asState() - val concreteTypeInfo = state.concreteValueMap - .mapValues { it.value.type } + val concreteTypeInfo = state.concreteTypes .filterValues { it.isJavaRt } .mapValues { it.value.rtMapped } .toTypeMap() From c6aa286b40e4ad2cc5228c19d897967b60b3a1d3 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Mon, 13 Nov 2023 12:41:07 +0100 Subject: [PATCH 2/2] collecting concrete values of object instance and arguments at the end of the method --- .../kex/asm/transform/SymbolicTraceInstrumenter.kt | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/transform/SymbolicTraceInstrumenter.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/transform/SymbolicTraceInstrumenter.kt index 219d43d60..8f0c13039 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/transform/SymbolicTraceInstrumenter.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/transform/SymbolicTraceInstrumenter.kt @@ -738,6 +738,16 @@ class SymbolicTraceInstrumenter( else -> values.nullConstant to values.nullConstant } val instrumented = buildList { + if (inst.hasReturnValue) { + addAll(track(inst.returnValue)) + } + val currentMethod = inst.parent.method + if (!currentMethod.isStatic) { + addAll(track(values.getThis(currentMethod.klass))) + } + for ((index, type) in currentMethod.argTypes.withIndex()) { + addAll(track(values.getArgument(index, currentMethod, type))) + } add( collectorClass.interfaceCall( returnMethod, traceCollector,