Track state fork points (#178)

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

@@ -1,16 +1,11 @@
 package org.usvm
 
-import io.ksmt.expr.KInterpretedValue
 import org.usvm.constraints.UPathConstraints
 import org.usvm.memory.UMemory
 import org.usvm.merging.UMergeable
 import org.usvm.model.UModelBase
-import org.usvm.solver.USatResult
-import org.usvm.solver.USolverResult
-import org.usvm.solver.UUnknownResult
-import org.usvm.solver.UUnsatResult
-import org.usvm.targets.UTargetsSet
 import org.usvm.targets.UTarget
+import org.usvm.targets.UTargetsSet
 
 typealias StateId = UInt
 
@@ -26,6 +21,7 @@ abstract class UState<Type, Method, Statement, Context, Target, State>(
      */
     open var models: List<UModelBase<Type>>,
     open var pathNode: PathNode<Statement>,
+    open var forkPoints: PathNode<PathNode<Statement>>,
     open val targets: UTargetsSet<Target, Statement>,
 ) : UMergeable<State, Unit>
     where Context : UContext<*>,

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

@@ -78,6 +78,8 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
     ): Unit? {
         check(canProcessFurtherOnCurrentStep)
 
+        val possibleForkPoint = originalState.pathNode
+
         val (posState, negState) = ctx.statesForkProvider.fork(originalState, condition)
 
         posState?.blockOnTrueState()
@@ -93,6 +95,9 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
             negState.blockOnFalseState()
             if (negState !== originalState) {
                 forkedStates += negState
+
+                originalState.forkPoints += possibleForkPoint
+                negState.forkPoints += possibleForkPoint
             }
         }
 
@@ -106,9 +111,20 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
      *
      * NOTE: always sets the [stepScopeState] to the [CANNOT_BE_PROCESSED] value.
      */
-    fun forkMulti(conditionsWithBlockOnStates: List<Pair<UBoolExpr, T.() -> Unit>>) {
+    fun forkMulti(conditionsWithBlockOnStates: List<Pair<UBoolExpr, T.() -> Unit>>) =
+        forkMulti(conditionsWithBlockOnStates, skipForkPointIfPossible = true)
+
+    /**
+     * @param skipForkPointIfPossible determines whether it is allowed to skip fork point registration.
+     * */
+    private fun forkMulti(
+        conditionsWithBlockOnStates: List<Pair<UBoolExpr, T.() -> Unit>>,
+        skipForkPointIfPossible: Boolean
+    ) {
         check(canProcessFurtherOnCurrentStep)
 
+        val possibleForkPoint = originalState.pathNode
+
         val conditions = conditionsWithBlockOnStates.map { it.first }
 
         val conditionStates = ctx.statesForkProvider.forkMulti(originalState, conditions)
@@ -132,18 +148,35 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
 
         // Interpret the first state as original and others as forked
         this.forkedStates += forkedStates.subList(1, forkedStates.size)
+
+        if (skipForkPointIfPossible && forkedStates.size < 2) return
+
+        forkedStates.forEach { it.forkPoints += possibleForkPoint }
     }
 
-    fun assert(
+    fun assert(constraint: UBoolExpr, block: T.() -> Unit = {}): Unit? =
+        assert(constraint, registerForkPoint = false, block)
+
+    /**
+     * @param registerForkPoint register a fork point if assert was successful.
+     * */
+    private fun assert(
         constraint: UBoolExpr,
-        block: T.() -> Unit = {},
+        registerForkPoint: Boolean,
+        block: T.() -> Unit,
     ): Unit? {
         check(canProcessFurtherOnCurrentStep)
 
+        val possibleForkPoint = originalState.pathNode
+
         val (posState) = ctx.statesForkProvider.forkMulti(originalState, listOf(constraint))
 
         posState?.block()
 
+        if (registerForkPoint && posState != null) {
+            posState.forkPoints += possibleForkPoint
+        }
+
         if (posState == null) {
             stepScopeState = DEAD
         }
@@ -180,12 +213,15 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
             return fork(condition, blockOnTrueState, blockOnFalseState)
         }
 
+        // If condition is concrete there is no fork point possibility
+        val registerForkPoint = !condition.isConcrete
+
         // TODO: asserts are implemented via forkMulti and create an unused copy of state
         if (shouldForkOnTrue) {
-            return assert(condition, blockOnTrueState)
+            return assert(condition, registerForkPoint, blockOnTrueState)
         }
 
-        return assert(condition.uctx.mkNot(condition), blockOnFalseState)
+        return assert(condition.uctx.mkNot(condition), registerForkPoint, blockOnFalseState)
     }
 
     /**
@@ -208,9 +244,13 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
             return
         }
 
-        return forkMulti(filteredConditionsWithBlockOnStates)
+        // If all conditions are concrete there is no fork point possibility
+        val skipForkPoint = forkCases.all { it.condition.isConcrete }
+        return forkMulti(filteredConditionsWithBlockOnStates, skipForkPoint)
     }
 
+    private val UBoolExpr.isConcrete get() = isTrue || isFalse
+
     /**
      * [assert]s the [condition] on the scope with the cloned [originalState]. Returns this cloned state,
      * if this [condition] is satisfiable, and returns `null` otherwise.

usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt

@@ -303,13 +303,13 @@ private fun <Method, Statement, State : UState<*, Method, Statement, *, *, State
     if (random == null) {
         return WeightedPathSelector(
             priorityCollectionFactory = { DeterministicPriorityCollection(Comparator.naturalOrder()) },
-            weighter = { it.pathNode.depth }
+            weighter = { it.forkPoints.depth }
         )
     }
 
     return WeightedPathSelector(
         priorityCollectionFactory = { RandomizedPriorityCollection(compareById()) { random.nextDouble() } },
-        weighter = { 1.0 / max(it.pathNode.depth.toDouble(), 1.0) }
+        weighter = { 1.0 / max(it.forkPoints.depth.toDouble(), 1.0) }
     )
 }
 

usvm-core/src/test/kotlin/org/usvm/TestUtil.kt

@@ -44,7 +44,7 @@ internal class TestState(
     pathLocation: PathNode<TestInstruction>,
     targetTrees: UTargetsSet<TestTarget, TestInstruction> = UTargetsSet.empty(),
     override val entrypoint: TestMethod = ""
-) : UState<Any, TestMethod, TestInstruction, UContext<*>, TestTarget, TestState>(ctx, callStack, pathConstraints, memory, models, pathLocation, targetTrees) {
+) : UState<Any, TestMethod, TestInstruction, UContext<*>, TestTarget, TestState>(ctx, callStack, pathConstraints, memory, models, pathLocation, PathNode.root(), targetTrees) {
 
     override fun clone(newConstraints: UPathConstraints<Any>?): TestState = this
 

usvm-core/src/test/kotlin/org/usvm/api/collections/SymbolicCollectionTestBase.kt

@@ -68,7 +68,7 @@ abstract class SymbolicCollectionTestBase {
         memory: UMemory<SingleTypeSystem.SingleType, Any?>,
     ) : UState<SingleTypeSystem.SingleType, Any?, Any?, UContext<USizeSort>, TargetStub, StateStub>(
         ctx, UCallStack(),
-        pathConstraints, memory, emptyList(), PathNode.root(), UTargetsSet.empty()
+        pathConstraints, memory, emptyList(), PathNode.root(), PathNode.root(), UTargetsSet.empty()
     ) {
         override fun clone(newConstraints: UPathConstraints<SingleTypeSystem.SingleType>?): StateStub {
             val clonedConstraints = newConstraints ?: pathConstraints.clone()

usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt

@@ -22,6 +22,7 @@ class JcState(
     memory: UMemory<JcType, JcMethod> = UMemory(ctx, pathConstraints.typeConstraints),
     models: List<UModelBase<JcType>> = listOf(),
     pathNode: PathNode<JcInst> = PathNode.root(),
+    forkPoints: PathNode<PathNode<JcInst>> = PathNode.root(),
     var methodResult: JcMethodResult = JcMethodResult.NoCall,
     targets: UTargetsSet<JcTarget, JcInst> = UTargetsSet.empty(),
 ) : UState<JcType, JcMethod, JcInst, JcContext, JcTarget, JcState>(
@@ -31,6 +32,7 @@ class JcState(
     memory,
     models,
     pathNode,
+    forkPoints,
     targets
 ) {
     override fun clone(newConstraints: UPathConstraints<JcType>?): JcState {
@@ -43,6 +45,7 @@ class JcState(
             memory.clone(clonedConstraints.typeConstraints),
             models,
             pathNode,
+            forkPoints,
             methodResult,
             targets.clone(),
         )
@@ -58,6 +61,7 @@ class JcState(
         // TODO: copy-paste
 
         val mergedPathNode = pathNode.mergeWith(other.pathNode, Unit) ?: return null
+        val mergedForkPoints = forkPoints.mergeWith(other.forkPoints, Unit) ?: return null
 
         val mergeGuard = MutableMergeGuard(ctx)
         val mergedCallStack = callStack.mergeWith(other.callStack, Unit) ?: return null
@@ -82,6 +86,7 @@ class JcState(
             mergedMemory,
             mergedModels,
             mergedPathNode,
+            mergedForkPoints,
             methodResult,
             mergedTargets
         )

usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/LongWrapperTest.kt

@@ -2,19 +2,24 @@ package org.usvm.samples.wrappers
 
 import org.junit.jupiter.api.Disabled
 import org.junit.jupiter.api.Test
+import org.usvm.PathSelectionStrategy
 import org.usvm.samples.JavaMethodTestRunner
 import org.usvm.test.util.checkers.eq
 
 
 internal class LongWrapperTest : JavaMethodTestRunner() {
     @Test
     fun primitiveToWrapperTest() {
-        checkDiscoveredProperties(
-            LongWrapper::primitiveToWrapper,
-            eq(2),
-            { _, x, r -> x >= 0 && r != null && r <= 0 },
-            { _, x, r -> x < 0 && r != null && r < 0 },
-        )
+        // todo: investigate why only BFS works
+        val options = options.copy(pathSelectionStrategies = listOf(PathSelectionStrategy.BFS))
+        withOptions(options) {
+            checkDiscoveredProperties(
+                LongWrapper::primitiveToWrapper,
+                eq(2),
+                { _, x, r -> x >= 0 && r != null && r <= 0 },
+                { _, x, r -> x < 0 && r != null && r < 0 },
+            )
+        }
     }
 
     @Test

usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/ShortWrapperTest.kt

@@ -2,19 +2,24 @@ package org.usvm.samples.wrappers
 
 import org.junit.jupiter.api.Disabled
 import org.junit.jupiter.api.Test
+import org.usvm.PathSelectionStrategy
 import org.usvm.samples.JavaMethodTestRunner
 import org.usvm.test.util.checkers.eq
 
 
 internal class ShortWrapperTest : JavaMethodTestRunner() {
     @Test
     fun primitiveToWrapperTest() {
-        checkDiscoveredProperties(
-            ShortWrapper::primitiveToWrapper,
-            eq(2),
-            { _, x, r -> x >= 0 && r != null && r <= 0 },
-            { _, x, r -> x < 0 && r != null && r < 0 },
-        )
+        // todo: investigate why only BFS works
+        val options = options.copy(pathSelectionStrategies = listOf(PathSelectionStrategy.BFS))
+        withOptions(options) {
+            checkDiscoveredProperties(
+                ShortWrapper::primitiveToWrapper,
+                eq(2),
+                { _, x, r -> x >= 0 && r != null && r <= 0 },
+                { _, x, r -> x < 0 && r != null && r < 0 },
+            )
+        }
     }
 
     @Test

usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt

@@ -26,6 +26,7 @@ class SampleState(
     memory: UMemory<SampleType, Method<*>> = UMemory(ctx, pathConstraints.typeConstraints),
     models: List<UModelBase<SampleType>> = listOf(),
     pathNode: PathNode<Stmt> = PathNode.root(),
+    forkPoints: PathNode<PathNode<Stmt>> = PathNode.root(),
     var returnRegister: UExpr<out USort>? = null,
     var exceptionRegister: ProgramException? = null,
     targets: UTargetsSet<SampleTarget, Stmt> = UTargetsSet.empty(),
@@ -36,6 +37,7 @@ class SampleState(
     memory,
     models,
     pathNode,
+    forkPoints,
     targets
 ) {
     override fun clone(newConstraints: UPathConstraints<SampleType>?): SampleState {
@@ -48,6 +50,7 @@ class SampleState(
             memory.clone(clonedConstraints.typeConstraints),
             models,
             pathNode,
+            forkPoints,
             returnRegister,
             exceptionRegister,
             targets
@@ -63,6 +66,7 @@ class SampleState(
         require(entrypoint == other.entrypoint) { "Cannot merge states with different entrypoints" }
 
         val mergedPathNode = pathNode.mergeWith(other.pathNode, Unit) ?: return null
+        val mergedForkPoints = forkPoints.mergeWith(other.forkPoints, Unit) ?: return null
 
         val mergeGuard = MutableMergeGuard(ctx)
         val mergedCallStack = callStack.mergeWith(other.callStack, Unit) ?: return null
@@ -92,6 +96,7 @@ class SampleState(
             mergedMemory,
             mergedModels,
             mergedPathNode,
+            mergedForkPoints,
             mergedReturnRegister,
             mergedExceptionRegister,
             mergedTargets