Coverage guided selector

kex-annotation-processor/src/main/resources/SMTExpr.vm

@@ -573,7 +573,7 @@ class Ifer {
             inline fun < reified T : $valexpr > `else`(`false`: T): T {
                 val ctx = cond.ctx
                 val expr = engine().ite(ctx, cond.expr, `true`.expr, `false`.expr)
-                val axiom = spliceAxioms(ctx, `true`.axiom, `false`.axiom)
+                val axiom = spliceAxioms(ctx, cond.axiom, `true`.axiom, `false`.axiom)
                 return ${valexpr}.forceCast< T >($valexpr(ctx, expr, axiom))
             }
             inline fun < reified T : $valexpr > else_(`false`: () -> T) = `else`(`false`())

kex-core/src/main/kotlin/org/vorpal/research/kex/asm/manager/ClassInstantiationManager.kt

@@ -39,6 +39,18 @@ interface ClassInstantiationManager {
             else -> type
         }
 
+    fun getAll(type: Type, accessLevel: AccessModifier, excludes: Set<Class>): Set<Type> =
+        when (type) {
+            is ClassType -> getAllConcreteSubtypes(type.klass, accessLevel)
+                .filter { it !in excludes }
+                .mapTo(mutableSetOf()) { it.asType }
+
+            is ArrayType -> getAll(type.component, accessLevel, excludes)
+                .mapTo(mutableSetOf()) { it.asArray }
+
+            else -> setOf(type)
+        }
+
     fun getAllConcreteSubtypes(klass: Class, accessLevel: AccessModifier): Set<Class>
 
     fun getConcreteClass(klass: KexClass, cm: ClassManager, accessLevel: AccessModifier, random: Random): KexClass =

kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt

@@ -64,7 +64,7 @@ class Object2DescriptorConverter : DescriptorBuilder() {
                 is LongArray -> KexLong.asArray()
                 is FloatArray -> KexFloat.asArray()
                 is DoubleArray -> KexDouble.asArray()
-                is Array<*> -> any.javaClass.componentType.kex
+                is Array<*> -> any.javaClass.componentType.kex.asArray()
                 is String -> KexString()
                 else -> any.javaClass.kex
             }

kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/descriptor.kt

@@ -54,6 +54,7 @@ sealed class Descriptor(term: Term, type: KexType) {
         }
 
     val query: PredicateState get() = collectQuery(mutableSetOf())
+    val initializerState: PredicateState get() = collectInitializerState(mutableSetOf())
     val depth: Int get() = countDepth(setOf(), mutableMapOf())
 
     val typeInfo: PredicateState get() = generateTypeInfo(mutableSetOf())
@@ -67,6 +68,7 @@ sealed class Descriptor(term: Term, type: KexType) {
     abstract fun print(map: MutableMap<Descriptor, String>): String
     abstract fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean
     abstract fun collectQuery(set: MutableSet<Descriptor>): PredicateState
+    abstract fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState
 
     abstract fun countDepth(visited: Set<Descriptor>, cache: MutableMap<Descriptor, Int>): Int
     abstract fun concretize(
@@ -105,6 +107,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality null }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality null }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>) =
             other is Null
     }
@@ -116,6 +122,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Bool) return false
             return this.value == other.value
@@ -129,6 +139,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Byte) return false
             return this.value == other.value
@@ -142,6 +156,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Char) return false
             return this.value == other.value
@@ -155,6 +173,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Short) return false
             return this.value == other.value
@@ -168,6 +190,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Int) return false
             return this.value == other.value
@@ -181,6 +207,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Long) return false
             return this.value == other.value
@@ -194,6 +224,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Float) return false
             return this.value == other.value
@@ -207,6 +241,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Double) return false
             return this.value == other.value
@@ -283,6 +321,19 @@ sealed class FieldContainingDescriptor<T : FieldContainingDescriptor<T>>(
         }
     }
 
+    override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState {
+        if (this in set) return emptyState()
+        set += this
+        return basic {
+            state { term.initializeNew() }
+            for ((field, value) in fields) {
+                val fieldTerm = term.field(field.second, field.first)
+                append(value.collectInitializerState(set))
+                state { fieldTerm.initialize(value.term) }
+            }
+        }
+    }
+
     override fun concretize(
         cm: ClassManager,
         accessLevel: AccessModifier,
@@ -483,6 +534,16 @@ class ArrayDescriptor(val elementType: KexType, val length: Int) :
         }
     }
 
+    override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState {
+        if (this in set) return emptyState()
+        set += this
+        return basic {
+            val fullElements = (0 until length).map { elements[it] ?: descriptor { default(elementType) } }
+            fullElements.forEach { append(it.collectInitializerState(set)) }
+            state { term.initializeNew(length, fullElements.map { it.term }) }
+        }
+    }
+
 
     override fun concretize(
         cm: ClassManager,

kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt

@@ -179,6 +179,8 @@ data class PersistentClauseList(
 
     override fun plus(other: ClauseList): PersistentClauseList = PersistentClauseList(state.addAll(other.state))
     override fun plus(other: Clause): PersistentClauseList = PersistentClauseList(state.add(other))
+
+    fun dropLast(n: Int): PersistentClauseList = subState(0, maxOf(0, size - n))
 }
 
 @Serializable
@@ -268,6 +270,8 @@ data class PersistentPathCondition(
 
     override fun plus(other: PathCondition): PersistentPathCondition = PersistentPathCondition(path.addAll(other.path))
     override fun plus(other: PathClause): PersistentPathCondition = PersistentPathCondition(path.add(other))
+
+    fun dropLast(n: Int): PersistentPathCondition = subPath(0, maxOf(0, size - n))
 }
 
 @Serializable
@@ -297,11 +301,29 @@ abstract class SymbolicState {
     abstract operator fun plus(other: PathClause): SymbolicState
     abstract operator fun plus(other: ClauseList): SymbolicState
     abstract operator fun plus(other: PathCondition): SymbolicState
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (javaClass != other?.javaClass) return false
+
+        other as SymbolicState
+
+        if (clauses != other.clauses) return false
+        if (path != other.path) return false
+
+        return true
+    }
+
+    override fun hashCode(): Int {
+        var result = clauses.hashCode()
+        result = 31 * result + path.hashCode()
+        return result
+    }
 }
 
 @Serializable
 @SerialName("SymbolicStateImpl")
-internal data class SymbolicStateImpl(
+internal class SymbolicStateImpl(
     override val clauses: ClauseList,
     override val path: PathCondition,
     override val concreteTypes: @Contextual Map<Term, KexType>,
@@ -315,33 +337,48 @@ internal data class SymbolicStateImpl(
         concreteValues = concreteValues + other.concreteValues,
         termMap = termMap + other.termMap
     )
+
     override fun plus(other: StateClause): SymbolicState = copy(
         clauses = clauses + other
     )
+
     override fun plus(other: PathClause): SymbolicState = copy(
         path = path + other,
     )
+
     override fun plus(other: ClauseList): SymbolicState = copy(
         clauses = clauses + other
     )
+
     override fun plus(other: PathCondition): SymbolicState = copy(
         path = path + other,
     )
 
     override fun toString(): String {
         return "SymbolicStateImpl(clauses=$clauses, path=$path)"
     }
+
+    fun copy(
+        clauses: ClauseList = this.clauses,
+        path: PathCondition = this.path,
+        concreteTypes: Map<Term, KexType> = this.concreteTypes,
+        concreteValues: Map<Term, Descriptor> = this.concreteValues,
+        termMap: Map<Term, WrappedValue> = this.termMap,
+    ): SymbolicState = SymbolicStateImpl(
+        clauses, path, concreteTypes, concreteValues, termMap
+    )
 }
 
 @Serializable
 @SerialName("PersistentSymbolicState")
-data class PersistentSymbolicState(
+class PersistentSymbolicState(
     override val clauses: PersistentClauseList,
     override val path: PersistentPathCondition,
     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(
@@ -351,18 +388,32 @@ data class PersistentSymbolicState(
         concreteValues = concreteValues.putAll(other.concreteValues),
         termMap = termMap.putAll(other.termMap)
     )
+
     override fun plus(other: StateClause): PersistentSymbolicState = copy(
         clauses = clauses + other
     )
+
     override fun plus(other: PathClause): PersistentSymbolicState = copy(
         path = path + other,
     )
+
     override fun plus(other: ClauseList): PersistentSymbolicState = copy(
         clauses = clauses + other
     )
+
     override fun plus(other: PathCondition): PersistentSymbolicState = copy(
         path = path + other,
     )
+
+    fun copy(
+        clauses: PersistentClauseList = this.clauses,
+        path: PersistentPathCondition = this.path,
+        concreteTypes: PersistentMap<Term, KexType> = this.concreteTypes,
+        concreteValues: PersistentMap<Term, Descriptor> = this.concreteValues,
+        termMap: PersistentMap<Term, WrappedValue> = this.termMap,
+    ): PersistentSymbolicState = PersistentSymbolicState(
+        clauses, path, concreteTypes, concreteValues, termMap
+    )
 }