Merge pull request #96 from vorpal-research/concrete-value-collection…

…-api

Concrete value collection api

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,
@@ -839,6 +849,21 @@ class SymbolicTraceInstrumenter(
         inst.insertAfter(after.mapLocation())
     }
 
+    private fun track(value: Value): List<Instruction> = 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<Instruction> = buildList {
         if (inst.parent.method.isConstructor && value is ThisRef) return@buildList
 

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<Any, Descriptor>()
 
+    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]!!

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,

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<Term, @Contextual Descriptor>
+    abstract val concreteTypes: Map<Term, KexType>
+    abstract val concreteValues: Map<Term, @Contextual Descriptor>
     abstract val termMap: Map<Term, @Contextual WrappedValue>
 
     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<Term, @Contextual Descriptor>,
+    override val concreteTypes: @Contextual Map<Term, KexType>,
+    override val concreteValues: @Contextual Map<Term, @Contextual Descriptor>,
     override val termMap: @Contextual Map<Term, @Contextual WrappedValue>,
 ) : 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,15 +334,17 @@ internal data class SymbolicStateImpl(
 data class PersistentSymbolicState(
     override val clauses: PersistentClauseList,
     override val path: PersistentPathCondition,
-    override val concreteValueMap: @Contextual PersistentMap<Term, @Contextual Descriptor>,
+    override val concreteTypes: @Contextual PersistentMap<Term, KexType>,
+    override val concreteValues: @Contextual PersistentMap<Term, @Contextual Descriptor>,
     override val termMap: @Contextual PersistentMap<Term, @Contextual WrappedValue>,
 ) : SymbolicState() {
     override fun toString() = clauses.joinToString("\n") { it.predicate.toString() }
 
     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<Term, KexType> = emptyMap(),
     concreteValueMap: Map<Term, Descriptor> = emptyMap(),
     termMap: Map<Term, WrappedValue> = emptyMap(),
 ): SymbolicState = SymbolicStateImpl(
-    state, path, concreteValueMap, termMap
+    state, path, concreteTypeMap, concreteValueMap, termMap
 )
 
 fun persistentSymbolicState(
     state: PersistentClauseList = PersistentClauseList(),
     path: PersistentPathCondition = PersistentPathCondition(),
+    concreteTypeMap: PersistentMap<Term, KexType> = persistentMapOf(),
     concreteValueMap: PersistentMap<Term, Descriptor> = persistentMapOf(),
     termMap: PersistentMap<Term, WrappedValue> = persistentMapOf(),
 ): PersistentSymbolicState = PersistentSymbolicState(
-    state, path, concreteValueMap, termMap
+    state, path, concreteTypeMap, concreteValueMap, termMap
 )
 
 fun List<Clause>.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()
     )
 }