Targets API (#52)

---------

Co-authored-by: Alexey Menshutin <[email protected]>

usvm-core/src/main/kotlin/org/usvm/CallStack.kt

@@ -12,7 +12,7 @@ data class UStackTraceFrame<Method, Statement>(
 
 class UCallStack<Method, Statement> private constructor(
     private val stack: ArrayDeque<UCallStackFrame<Method, Statement>>,
-) : Collection<UCallStackFrame<Method, Statement>> by stack {
+) : List<UCallStackFrame<Method, Statement>> by stack {
     constructor() : this(ArrayDeque())
     constructor(method: Method) : this(
         ArrayDeque<UCallStackFrame<Method, Statement>>().apply {

usvm-core/src/main/kotlin/org/usvm/Context.kt

@@ -348,7 +348,7 @@ open class UContext(
     // Type hack to be able to intern the initial location for inheritors.
     private val initialLocation = RootNode<Nothing, Nothing>()
 
-    fun <State : UState<*, *, Statement, *, State>, Statement> mkInitialLocation()
+    fun <State : UState<*, *, Statement, *, *, State>, Statement> mkInitialLocation()
             : PathsTrieNode<State, Statement> = initialLocation.uncheckedCast()
 
     fun mkUValueSampler(): KSortVisitor<KExpr<*>> {

usvm-core/src/main/kotlin/org/usvm/Machine.kt

@@ -6,14 +6,13 @@ import org.usvm.stopstrategies.StopStrategy
 import org.usvm.util.bracket
 import org.usvm.util.debug
 
+val logger = object : KLogging() {}.logger
+
 /**
  * An abstract symbolic machine.
  *
  * @see [run]
  */
-
-val logger = object : KLogging() {}.logger
-
 abstract class UMachine<State> : AutoCloseable {
     /**
      * Runs symbolic execution loop.

usvm-core/src/main/kotlin/org/usvm/Merging.kt

@@ -7,7 +7,7 @@ interface UMerger<Entity> {
     fun merge(left: Entity, right: Entity): Entity?
 }
 
-open class UStateMerger<State : UState<*, *, *, *, State>> : UMerger<State> {
+open class UStateMerger<State : UState<*, *, *, *, *, State>> : UMerger<State> {
     // Never merge for now
     override fun merge(left: State, right: State) = null
 }

usvm-core/src/main/kotlin/org/usvm/PathTrieNode.kt

@@ -3,7 +3,7 @@ package org.usvm
 /**
  * Symbolic execution tree node.
  */
-sealed class PathsTrieNode<State : UState<*, *, Statement, *, State>, Statement> {
+sealed class PathsTrieNode<State : UState<*, *, Statement, *, *, State>, Statement> {
     /**
      * Forked states' nodes.
      */
@@ -65,7 +65,7 @@ sealed class PathsTrieNode<State : UState<*, *, Statement, *, State>, Statement>
     }
 }
 
-class PathsTrieNodeImpl<State : UState<*, *, Statement, *, State>, Statement> private constructor(
+class PathsTrieNodeImpl<State : UState<*, *, Statement, *, *, State>, Statement> private constructor(
     override val depth: Int,
     override val states: MutableSet<State>,
     // Note: order is important for tests
@@ -101,7 +101,7 @@ class PathsTrieNodeImpl<State : UState<*, *, Statement, *, State>, Statement> pr
     override fun toString(): String = "Depth: $depth, statement: $statement"
 }
 
-class RootNode<State : UState<*, *, Statement, *, State>, Statement> : PathsTrieNode<State, Statement>() {
+class RootNode<State : UState<*, *, Statement, *, *, State>, Statement> : PathsTrieNode<State, Statement>() {
     override val children: MutableMap<Statement, PathsTrieNodeImpl<State, Statement>> = mutableMapOf()
 
     override val states: MutableSet<State> = hashSetOf()

usvm-core/src/main/kotlin/org/usvm/State.kt

@@ -1,6 +1,8 @@
 package org.usvm
 
 import io.ksmt.expr.KInterpretedValue
+import kotlinx.collections.immutable.PersistentList
+import kotlinx.collections.immutable.toPersistentList
 import org.usvm.constraints.UPathConstraints
 import org.usvm.memory.UMemory
 import org.usvm.model.UModelBase
@@ -10,15 +12,18 @@ import org.usvm.solver.UUnsatResult
 
 typealias StateId = UInt
 
-abstract class UState<Type, Method, Statement, Context : UContext, State : UState<Type, Method, Statement, Context, State>>(
+abstract class UState<Type, Method, Statement, Context, Target, State>(
     // TODO: add interpreter-specific information
     ctx: UContext,
     open val callStack: UCallStack<Method, Statement>,
     open val pathConstraints: UPathConstraints<Type, Context>,
     open val memory: UMemory<Type, Method>,
     open var models: List<UModelBase<Type>>,
     open var pathLocation: PathsTrieNode<State, Statement>,
-) {
+    targets: List<Target> = emptyList(),
+) where Context : UContext,
+        Target : UTarget<Statement, Target, State>,
+        State : UState<Type, Method, Statement, Context, Target, State> {
     /**
      * Deterministic state id.
      * TODO: Can be replaced with overridden hashCode
@@ -54,7 +59,7 @@ abstract class UState<Type, Method, Statement, Context : UContext, State : UStat
         if (this === other) return true
         if (javaClass != other?.javaClass) return false
 
-        other as UState<*, *, *, *, *>
+        other as UState<*, *, *, *, *, *>
 
         return id == other.id
     }
@@ -73,6 +78,46 @@ abstract class UState<Type, Method, Statement, Context : UContext, State : UStat
      * A property containing information about whether the state is exceptional or not.
      */
     abstract val isExceptional: Boolean
+
+    protected var targetsImpl: PersistentList<Target> = targets.toPersistentList()
+        private set
+
+    private val reachedTerminalTargetsImpl = mutableSetOf<Target>()
+
+    /**
+     * Collection of state's current targets.
+     * TODO: clean removed targets sometimes
+     */
+    val targets: Sequence<Target> get() = targetsImpl.asSequence().filterNot { it.isRemoved }
+
+    /**
+     * Reached targets with no children.
+     */
+    val reachedTerminalTargets: Set<Target> = reachedTerminalTargetsImpl
+
+    /**
+     * If the [target] is not removed and is contained in this state's target collection,
+     * removes it from there and adds there all its children.
+     *
+     * @return true if the [target] was successfully removed.
+     */
+    internal fun tryPropagateTarget(target: Target): Boolean {
+        val previousTargetCount = targetsImpl.size
+        targetsImpl = targetsImpl.remove(target)
+
+        if (previousTargetCount == targetsImpl.size || !target.isRemoved) {
+            return false
+        }
+
+        if (target.isTerminal) {
+            reachedTerminalTargetsImpl.add(target)
+            return true
+        }
+
+        targetsImpl = targetsImpl.addAll(target.children)
+
+        return true
+    }
 }
 
 data class ForkResult<T>(
@@ -96,7 +141,7 @@ private const val OriginalState = false
  * forked state.
  *
  */
-private fun <T : UState<Type, *, *, Context, T>, Type, Context : UContext> forkIfSat(
+private fun <T : UState<Type, *, *, Context, *, T>, Type, Context : UContext> forkIfSat(
     state: T,
     newConstraintToOriginalState: UBoolExpr,
     newConstraintToForkedState: UBoolExpr,
@@ -156,7 +201,7 @@ private fun <T : UState<Type, *, *, Context, T>, Type, Context : UContext> forkI
  * 2. makes not more than one query to USolver;
  * 3. if both [condition] and ![condition] are satisfiable, then [ForkResult.positiveState] === [state].
  */
-fun <T : UState<Type, *, *, Context, T>, Type, Context : UContext> fork(
+fun <T : UState<Type, *, *, Context, *, T>, Type, Context : UContext> fork(
     state: T,
     condition: UBoolExpr,
 ): ForkResult<T> {
@@ -217,7 +262,7 @@ fun <T : UState<Type, *, *, Context, T>, Type, Context : UContext> fork(
  * @return a list of states for each condition - `null` state
  * means [UUnknownResult] or [UUnsatResult] of checking condition.
  */
-fun <T : UState<Type, *, *, Context, T>, Type, Context : UContext> forkMulti(
+fun <T : UState<Type, *, *, Context, *, T>, Type, Context : UContext> forkMulti(
     state: T,
     conditions: Iterable<UBoolExpr>,
 ): List<T?> {

usvm-core/src/main/kotlin/org/usvm/StepScope.kt

@@ -18,7 +18,7 @@ import org.usvm.StepScope.StepScopeState.DEAD
  *
  * @param originalState an initial state.
  */
-class StepScope<T : UState<Type, *, *, Context, T>, Type, Context : UContext>(
+class StepScope<T : UState<Type, *, *, Context, *, T>, Type, Context : UContext>(
     private val originalState: T,
 ) {
     private val forkedStates = mutableListOf<T>()

usvm-core/src/main/kotlin/org/usvm/UTarget.kt

@@ -0,0 +1,79 @@
+package org.usvm
+
+/**
+ * Base class for a symbolic execution target. A target can be understood as a 'task' for symbolic machine
+ * which it tries to complete. For example, a task can have an attached location which should be visited by a state
+ * to consider the task completed. Also, the targets can produce some effects on states visiting them.
+ *
+ * Tasks can have 'child' tasks which should be completed only after its parent has been completed. For example,
+ * it allows to force the execution along the specific path.
+ *
+ * Targets are designed to be shared between all the symbolic execution states. Due to this, once there is
+ * a state which has reached the target which has no children, it is logically removed from the targets tree.
+ * The other states ignore such removed targets.
+ */
+abstract class UTarget<Statement, Target, State>(
+    /**
+     * Optional location of the target.
+     */
+    val location: Statement? = null,
+) where Target : UTarget<Statement, Target, State>,
+        State : UState<*, *, Statement, *, Target, State> {
+    private val childrenImpl = mutableListOf<Target>()
+    private var parent: Target? = null
+
+    /**
+     * List of the child targets which should be reached after this target.
+     */
+    val children: List<Target> = childrenImpl
+
+    /**
+     * True if this target has no children.
+     */
+    val isTerminal get() = childrenImpl.isEmpty()
+
+    /**
+     * True if this target is logically removed from the tree.
+     */
+    var isRemoved = false
+        private set
+
+    /**
+     * Adds a child target to this target.
+     * TODO: avoid possible recursion
+     *
+     * @return this target (for convenient target tree building).
+     */
+    fun addChild(child: Target): Target {
+        check(!isRemoved) { "Cannot add child to removed target" }
+        check(child.parent == null) { "Cannot add child target with existing parent" }
+        childrenImpl.add(child)
+        @Suppress("UNCHECKED_CAST")
+        child.parent = this as Target
+        return child
+    }
+
+    /**
+     * This method should be called by concrete targets to signal that [byState]
+     * should try to propagate the target. If the target without children has been
+     * visited, it is logically removed from tree.
+     */
+    protected fun propagate(byState: State) {
+        @Suppress("UNCHECKED_CAST")
+        if (byState.tryPropagateTarget(this as Target) && isTerminal) {
+            remove()
+        }
+    }
+
+    private fun remove() {
+        check(childrenImpl.all { it.isRemoved }) { "Cannot remove target when some of its children are not removed" }
+        if (isRemoved) {
+            return
+        }
+        isRemoved = true
+        val parent = parent
+        if (parent != null && parent.childrenImpl.all { it.isRemoved }) {
+            parent.remove()
+        }
+    }
+}

usvm-core/src/main/kotlin/org/usvm/api/EngineApi.kt

@@ -5,10 +5,10 @@ import org.usvm.UHeapRef
 import org.usvm.UState
 
 
-fun UState<*, *, *, *, *>.assume(expr: UBoolExpr) {
+fun UState<*, *, *, *, *, *>.assume(expr: UBoolExpr) {
     pathConstraints += expr
 }
 
-fun UState<*, *, *, *, *>.objectTypeEquals(lhs: UHeapRef, rhs: UHeapRef): UBoolExpr {
+fun UState<*, *, *, *, *, *>.objectTypeEquals(lhs: UHeapRef, rhs: UHeapRef): UBoolExpr {
     TODO("Objects types equality check: $lhs, $rhs")
 }

usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt

@@ -9,14 +9,14 @@ import org.usvm.uctx
 
 // TODO: special mock api for variables
 
-fun <Method, T : USort> UState<*, Method, *, *, *>.makeSymbolicPrimitive(
+fun <Method, T : USort> UState<*, Method, *, *, *, *>.makeSymbolicPrimitive(
     sort: T
 ): UExpr<T> {
     check(sort != sort.uctx.addressSort) { "$sort is not primitive" }
     return memory.mock { call(lastEnteredMethod, emptySequence(), sort) }
 }
 
-fun <Type, Method> UState<Type, Method, *, *, *>.makeSymbolicRef(type: Type): UHeapRef {
+fun <Type, Method> UState<Type, Method, *, *, *, *>.makeSymbolicRef(type: Type): UHeapRef {
     val ref = memory.mock { call(lastEnteredMethod, emptySequence(), memory.ctx.addressSort) }
 
     memory.types.addSubtype(ref, type)
@@ -25,7 +25,7 @@ fun <Type, Method> UState<Type, Method, *, *, *>.makeSymbolicRef(type: Type): UH
     return ref
 }
 
-fun <Type, Method> UState<Type, Method, *, *, *>.makeSymbolicArray(arrayType: Type, size: USizeExpr): UHeapRef {
+fun <Type, Method> UState<Type, Method, *, *, *, *>.makeSymbolicArray(arrayType: Type, size: USizeExpr): UHeapRef {
     val ref = memory.mock { call(lastEnteredMethod, emptySequence(), memory.ctx.addressSort) }
 
     memory.types.addSubtype(ref, arrayType)

usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt

@@ -15,7 +15,7 @@ import org.usvm.memory.map
 import org.usvm.uctx
 
 object ListCollectionApi {
-    fun <ListType> UState<ListType, *, *, *, *>.mkSymbolicList(
+    fun <ListType> UState<ListType, *, *, *, *, *>.mkSymbolicList(
         listType: ListType,
     ): UHeapRef = with(memory.ctx) {
         val ref = memory.alloc(listType)
@@ -27,12 +27,12 @@ object ListCollectionApi {
      * List size may be incorrect for input lists.
      * Use [ensureListSizeCorrect] to guarantee that list size is correct.
      * */
-    fun <ListType> UState<ListType, *, *, *, *>.symbolicListSize(
+    fun <ListType> UState<ListType, *, *, *, *, *>.symbolicListSize(
         listRef: UHeapRef,
         listType: ListType,
     ): USizeExpr = memory.readArrayLength(listRef, listType)
 
-    fun <ListType, State : UState<ListType, *, *, *, State>> StepScope<State, ListType, *>.ensureListSizeCorrect(
+    fun <ListType, State : UState<ListType, *, *, *, *, State>> StepScope<State, ListType, *>.ensureListSizeCorrect(
         listRef: UHeapRef,
         listType: ListType,
     ): Unit? {
@@ -54,14 +54,14 @@ object ListCollectionApi {
         return Unit
     }
 
-    fun <ListType, Sort : USort> UState<ListType, *, *, *, *>.symbolicListGet(
+    fun <ListType, Sort : USort> UState<ListType, *, *, *, *, *>.symbolicListGet(
         listRef: UHeapRef,
         index: USizeExpr,
         listType: ListType,
         sort: Sort,
     ): UExpr<Sort> = memory.readArrayIndex(listRef, index, listType, sort)
 
-    fun <ListType, Sort : USort> UState<ListType, *, *, *, *>.symbolicListAdd(
+    fun <ListType, Sort : USort> UState<ListType, *, *, *, *, *>.symbolicListAdd(
         listRef: UHeapRef,
         listType: ListType,
         sort: Sort,
@@ -76,7 +76,7 @@ object ListCollectionApi {
         }
     }
 
-    fun <ListType, Sort : USort> UState<ListType, *, *, *, *>.symbolicListSet(
+    fun <ListType, Sort : USort> UState<ListType, *, *, *, *, *>.symbolicListSet(
         listRef: UHeapRef,
         listType: ListType,
         sort: Sort,
@@ -86,7 +86,7 @@ object ListCollectionApi {
         memory.writeArrayIndex(listRef, index, listType, sort, value, guard = memory.ctx.trueExpr)
     }
 
-    fun <ListType, Sort : USort> UState<ListType, *, *, *, *>.symbolicListInsert(
+    fun <ListType, Sort : USort> UState<ListType, *, *, *, *, *>.symbolicListInsert(
         listRef: UHeapRef,
         listType: ListType,
         sort: Sort,
@@ -116,7 +116,7 @@ object ListCollectionApi {
         memory.writeArrayLength(listRef, updatedSize, listType)
     }
 
-    fun <ListType, Sort : USort> UState<ListType, *, *, *, *>.symbolicListRemove(
+    fun <ListType, Sort : USort> UState<ListType, *, *, *, *, *>.symbolicListRemove(
         listRef: UHeapRef,
         listType: ListType,
         sort: Sort,
@@ -142,7 +142,7 @@ object ListCollectionApi {
         memory.writeArrayLength(listRef, updatedSize, listType)
     }
 
-    fun <ListType, Sort : USort> UState<ListType, *, *, *, *>.symbolicListCopyRange(
+    fun <ListType, Sort : USort> UState<ListType, *, *, *, *, *>.symbolicListCopyRange(
         srcRef: UHeapRef,
         dstRef: UHeapRef,
         listType: ListType,