Extract common API + comment

UnitTestBot · Oct 7, 2024 · 1dc45cf · 1dc45cf
1 parent 6e81b3c
commit 1dc45cf
Show file tree

Hide file tree

Showing 7 changed files with 78 additions and 246 deletions.
diff --git a/.github/workflows/build-and-run-tests.yml b/.github/workflows/build-and-run-tests.yml
@@ -39,7 +39,8 @@ jobs:
           REPO_URL="https://gitee.com/Lipenx/arkanalyzer.git"
           DEST_DIR="arkanalyzer"
           MAX_RETRIES=10
-          RETRY_DELAY=3  # Delay between retries in seconds  
+          RETRY_DELAY=3  # Delay between retries in seconds
+#         Set the same as in jacodb/neo branch, since we get jacodb artifact from that branch.
           BRANCH="neo/2024-08-16"
 
           for ((i=1; i<=MAX_RETRIES; i++)); do

diff --git a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt
@@ -315,9 +315,47 @@ class UIsSupertypeExpr<Type> internal constructor(
 
 //endregion
 
+//region Utility Expressions
+
+/**
+ * Utility class for merging expressions with [UBoolSort] sort.
+ *
+ * Mainly created for [not] function used in StateForker.
+ */
+class UJoinedBoolExpr(
+    ctx: UContext<*>,
+    val exprs: List<UBoolExpr>
+) : UBoolExpr(ctx) {
+    override val sort: UBoolSort
+        get() = ctx.boolSort
+
+    private val joinedExprs = ctx.mkAnd(exprs)
+
+    fun not(): UBoolExpr = ctx.mkAnd(exprs.map(ctx::mkNot))
+
+    override fun accept(transformer: KTransformerBase): KExpr<UBoolSort> {
+        return transformer.apply(joinedExprs)
+    }
+
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other)
+
+    override fun internHashCode(): Int = hash()
+
+    override fun print(printer: ExpressionPrinter) {
+        printer.append("joined(")
+        joinedExprs.print(printer)
+        printer.append(")")
+    }
+}
+
+//endregion
+
 //region Utils
 
 val UBoolExpr.isFalse get() = this == ctx.falseExpr
 val UBoolExpr.isTrue get() = this == ctx.trueExpr
 
+fun UExpr<*>.unwrapJoinedExpr(ctx: UContext<*>): UExpr<out USort> =
+    if (this is UJoinedBoolExpr) ctx.mkAnd(exprs) else this
+
 //endregion
diff --git a/usvm-core/src/main/kotlin/org/usvm/StateForker.kt b/usvm-core/src/main/kotlin/org/usvm/StateForker.kt
@@ -1,6 +1,6 @@
 package org.usvm
 
-import org.usvm.StateForker.Companion.splitModelsByCondition
+import io.ksmt.utils.cast
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.model.UModelBase
 import org.usvm.solver.USatResult
@@ -12,39 +12,7 @@ private typealias StateToCheck = Boolean
 private const val ForkedState = true
 private const val OriginalState = false
 
-interface StateForker {
-
-    companion object {
-        /**
-         * Splits the passed [models] with this [condition] to the three categories:
-         * - models that satisfy this [condition];
-         * - models that are in contradiction with this [condition];
-         * - models that can not evaluate this [condition].
-         */
-        fun <Type> splitModelsByCondition(
-            models: List<UModelBase<Type>>,
-            condition: UBoolExpr,
-        ): SplittedModels<Type> {
-            val trueModels = mutableListOf<UModelBase<Type>>()
-            val falseModels = mutableListOf<UModelBase<Type>>()
-            val unknownModels = mutableListOf<UModelBase<Type>>()
-
-            models.forEach { model ->
-                val holdsInModel = model.eval(condition)
-
-                when {
-                    holdsInModel.isTrue -> trueModels += model
-                    holdsInModel.isFalse -> falseModels += model
-                    // Sometimes we cannot evaluate the condition – for example, a result for a division by symbolic expression
-                    // that is evaluated to 0 is unknown
-                    else -> unknownModels += model
-                }
-            }
-
-            return SplittedModels(trueModels, falseModels, unknownModels)
-        }
-    }
-
+sealed interface StateForker {
     /**
      * Implements symbolic branching.
      * Checks if [condition] and ![condition] are satisfiable within [state].
@@ -78,9 +46,10 @@ object WithSolverStateForker : StateForker {
         state: T,
         condition: UBoolExpr,
     ): ForkResult<T> {
-        val (trueModels, falseModels, _) = splitModelsByCondition(state.models, condition)
+        val unwrappedCondition: UBoolExpr = condition.unwrapJoinedExpr(state.ctx).cast()
+        val (trueModels, falseModels, _) = splitModelsByCondition(state.models, unwrappedCondition)
 
-        val notCondition = state.ctx.mkNot(condition)
+        val notCondition = if (condition is UJoinedBoolExpr) condition.not() else state.ctx.mkNot(unwrappedCondition)
         val (posState, negState) = when {
 
             trueModels.isNotEmpty() && falseModels.isNotEmpty() -> {
@@ -89,23 +58,23 @@ object WithSolverStateForker : StateForker {
 
                 posState.models = trueModels
                 negState.models = falseModels
-                posState.pathConstraints += condition
+                posState.pathConstraints += unwrappedCondition
                 negState.pathConstraints += notCondition
 
                 posState to negState
             }
 
             trueModels.isNotEmpty() -> state to forkIfSat(
                 state,
-                newConstraintToOriginalState = condition,
+                newConstraintToOriginalState = unwrappedCondition,
                 newConstraintToForkedState = notCondition,
                 stateToCheck = ForkedState
             )
 
             falseModels.isNotEmpty() -> {
                 val forkedState = forkIfSat(
                     state,
-                    newConstraintToOriginalState = condition,
+                    newConstraintToOriginalState = unwrappedCondition,
                     newConstraintToForkedState = notCondition,
                     stateToCheck = OriginalState
                 )
@@ -287,12 +256,41 @@ object NoSolverStateForker : StateForker {
     }
 }
 
+/**
+ * Splits the passed [models] with this [condition] to the three categories:
+ * - models that satisfy this [condition];
+ * - models that are in contradiction with this [condition];
+ * - models that can not evaluate this [condition].
+ */
+private fun <Type> splitModelsByCondition(
+    models: List<UModelBase<Type>>,
+    condition: UBoolExpr,
+): SplittedModels<Type> {
+    val trueModels = mutableListOf<UModelBase<Type>>()
+    val falseModels = mutableListOf<UModelBase<Type>>()
+    val unknownModels = mutableListOf<UModelBase<Type>>()
+
+    models.forEach { model ->
+        val holdsInModel = model.eval(condition)
+
+        when {
+            holdsInModel.isTrue -> trueModels += model
+            holdsInModel.isFalse -> falseModels += model
+            // Sometimes we cannot evaluate the condition – for example, a result for a division by symbolic expression
+            // that is evaluated to 0 is unknown
+            else -> unknownModels += model
+        }
+    }
+
+    return SplittedModels(trueModels, falseModels, unknownModels)
+}
+
 data class ForkResult<T>(
     val positiveState: T?,
     val negativeState: T?,
 )
 
-data class SplittedModels<Type>(
+private data class SplittedModels<Type>(
     val trueModels: List<UModelBase<Type>>,
     val falseModels: List<UModelBase<Type>>,
     val unknownModels: List<UModelBase<Type>>,

diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt
@@ -6,7 +6,6 @@ import io.ksmt.symfpu.solver.KSymFpuSolver
 import org.jacodb.ets.base.EtsType
 import org.usvm.solver.USolverBase
 import org.usvm.solver.UTypeSolver
-import org.usvm.state.TSStateForker
 import org.usvm.types.UTypeSystem
 
 class TSComponents(
@@ -41,8 +40,6 @@ class TSComponents(
         return USolverBase(ctx, smtSolver, typeSolver, translator, decoder, options.solverTimeout)
     }
 
-    override fun mkStatesForkProvider(): StateForker = TSStateForker
-
     fun close() {
         closeableResources.forEach(AutoCloseable::close)
     }

diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt
@@ -36,37 +36,6 @@ class TSUndefinedValue(ctx: TSContext) : UExpr<TSUndefinedSort>(ctx) {
     }
 }
 
-/**
- * Utility class for merging expressions with [UBoolSort] sort.
- *
- * Mainly created for [not] function used in TSStateForker.
- */
-class UJoinedBoolExpr(
-    ctx: TSContext,
-    val exprs: List<UBoolExpr>
-) : UBoolExpr(ctx) {
-    override val sort: UBoolSort
-        get() = ctx.boolSort
-
-    private val joinedExprs = ctx.mkAnd(exprs)
-
-    fun not(): UBoolExpr = ctx.mkAnd(exprs.map(ctx::mkNot))
-
-    override fun accept(transformer: KTransformerBase): KExpr<UBoolSort> {
-        return transformer.apply(joinedExprs)
-    }
-
-    override fun internEquals(other: Any): Boolean = structurallyEqual(other)
-
-    override fun internHashCode(): Int = hash()
-
-    override fun print(printer: ExpressionPrinter) {
-        printer.append("joined(")
-        joinedExprs.print(printer)
-        printer.append(")")
-    }
-}
-
 /**
  * [UExpr] wrapper that handles type coercion.
  *

diff --git a/usvm-ts/src/main/kotlin/org/usvm/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/Utils.kt
@@ -16,9 +16,6 @@ fun UContext<*>.boolToFpSort(expr: UExpr<UBoolSort>) =
 fun UContext<*>.fpToBoolSort(expr: UExpr<KFp64Sort>) =
     mkIte(mkFpEqualExpr(expr, mkFp64(0.0)), mkFalse(), mkTrue())
 
-fun UExpr<*>.unwrapJoinedExpr(ctx: UContext<*>): UExpr<out USort> =
-    if (this is UJoinedBoolExpr) ctx.mkAnd(exprs) else this
-
 fun UExpr<out USort>.extractOrThis(): UExpr<out USort> = if (this is TSWrappedValue) value else this
 
 fun <K, V> MutableMap<K, MutableSet<V>>.copy(): MutableMap<K, MutableSet<V>> = this.entries.associate { (k, v) ->