Basic USVM TS type system with type coercion

.github/workflows/build-and-run-tests.yml

@@ -40,24 +40,24 @@ jobs:
           DEST_DIR="arkanalyzer"
           MAX_RETRIES=10
           RETRY_DELAY=3  # Delay between retries in seconds  
-          BRANCH="neo/2024-08-07"
-
+          BRANCH="neo/2024-08-16"
+          
           for ((i=1; i<=MAX_RETRIES; i++)); do
               git clone --depth=1 --branch $BRANCH $REPO_URL $DEST_DIR && break
               echo "Clone failed, retrying in $RETRY_DELAY seconds..."
               sleep "$RETRY_DELAY"
           done
-
+          
           if [[ $i -gt $MAX_RETRIES ]]; then
               echo "Failed to clone the repository after $MAX_RETRIES attempts."
               exit 1
           else
               echo "Repository cloned successfully."
           fi
-
+          
           echo "ARKANALYZER_DIR=$(realpath $DEST_DIR)" >> $GITHUB_ENV
           cd $DEST_DIR
-
+          
           npm install
           npm run build
 

buildSrc/src/main/kotlin/Dependencies.kt

@@ -5,7 +5,7 @@ import org.gradle.plugin.use.PluginDependenciesSpec
 object Versions {
     const val detekt = "1.18.1"
     const val ini4j = "0.5.4"
-    const val jacodb = "ae2716b3f8"
+    const val jacodb = "3377c0cb88"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "1.9.20"

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

@@ -1,5 +1,6 @@
 package org.usvm
 
+import org.usvm.StateForker.Companion.splitModelsByCondition
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.model.UModelBase
 import org.usvm.solver.USatResult
@@ -11,7 +12,39 @@
 private const val ForkedState = true
 private const val OriginalState = false
 
-sealed interface StateForker {
+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)
+        }
+    }
+
     /**
      * Implements symbolic branching.
      * Checks if [condition] and ![condition] are satisfiable within [state].
@@ -254,41 +287,12 @@
     }
 }
 
-/**
- * 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?,
 )
 
-private data class SplittedModels<Type>(
+data class SplittedModels<Type>(
     val trueModels: List<UModelBase<Type>>,
     val falseModels: List<UModelBase<Type>>,
     val unknownModels: List<UModelBase<Type>>,

usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt

@@ -2,11 +2,11 @@ package org.usvm
 
 import org.jacodb.ets.base.EtsStmt
 import org.jacodb.ets.graph.EtsApplicationGraphImpl
-import org.jacodb.ets.model.EtsFile
 import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsScene
 import org.usvm.statistics.ApplicationGraph
 
-class TSApplicationGraph(project: EtsFile) : ApplicationGraph<EtsMethod, EtsStmt> {
+class TSApplicationGraph(project: EtsScene) : ApplicationGraph<EtsMethod, EtsStmt> {
     private val applicationGraph = EtsApplicationGraphImpl(project)
 
     override fun predecessors(node: EtsStmt): Sequence<EtsStmt> =

usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt

@@ -6,32 +6,93 @@
     val onBool: TSContext.(UExpr<UBoolSort>, UExpr<UBoolSort>) -> UExpr<out USort> = shouldNotBeCalled,
     val onBv: TSContext.(UExpr<UBvSort>, UExpr<UBvSort>) -> UExpr<out USort> = shouldNotBeCalled,
     val onFp: TSContext.(UExpr<UFpSort>, UExpr<UFpSort>) -> UExpr<out USort> = shouldNotBeCalled,
+    val onRef: TSContext.(UExpr<UAddressSort>, UExpr<UAddressSort>) -> UExpr<out USort> = shouldNotBeCalled,
+    val desiredSort: TSContext.(USort, USort) -> USort = { _, _ -> error("Should not be called") },
+    val banSorts: TSContext.(UExpr<out USort>, UExpr<out USort>) -> Set<USort> = {_, _ -> emptySet() },
 ) {
 
     object Eq : TSBinaryOperator(
         onBool = UContext<TSSizeSort>::mkEq,
         onBv = UContext<TSSizeSort>::mkEq,
         onFp = UContext<TSSizeSort>::mkFpEqualExpr,
+        onRef = UContext<TSSizeSort>::mkEq,
+        desiredSort = { lhs, _ -> lhs }
     )
 
+    // Neq must not be applied to a pair of expressions generated while initial Neq application.
+    // For example,
+    // "a (untyped arg) != 1.0 (fp64 number)"
+    // can't yield
+    // "a (bool reg reading) != true", since "1.0.toBool() = true" is a new value for 1.0.
+    //
+    // So, that's the reason why banSorts in Neq throws out all primitive types except one of the expressions' one.
     object Neq : TSBinaryOperator(
         onBool = { lhs, rhs -> lhs.neq(rhs) },
         onBv = { lhs, rhs -> lhs.neq(rhs) },
         onFp = { lhs, rhs -> mkFpEqualExpr(lhs, rhs).not() },
+        onRef = { lhs, rhs -> lhs.neq(rhs) },
+        desiredSort = { lhs, _ -> lhs },
+        banSorts = { lhs, rhs ->
+            when {
+                lhs is TSWrappedValue ->
+                    // rhs.sort == addressSort is a mock not to cause undefined
+                    // behaviour with support of new language features.
+                    if (rhs is TSWrappedValue || rhs.sort == addressSort) emptySet() else
+                        TSTypeSystem.primitiveTypes
+                        .map(::typeToSort).toSet()
+                        .minus(rhs.sort)
+                rhs is TSWrappedValue ->
+                    // lhs.sort == addressSort explained as above.
+                    if (lhs.sort == addressSort) emptySet() else
+                        TSTypeSystem.primitiveTypes
+                        .map(::typeToSort).toSet()
+                        .minus(lhs.sort)
+                else -> emptySet()
+            }
+        }
+    )
+
+    object Add : TSBinaryOperator(
+        onFp = { lhs, rhs -> mkFpAddExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) },
+        onBv = UContext<TSSizeSort>::mkBvAddExpr,
+        desiredSort = { _, _ -> fp64Sort },
     )
 
-    internal operator fun invoke(lhs: UExpr<out USort>, rhs: UExpr<out USort>): UExpr<out USort> {
+    object And : TSBinaryOperator(
+        onBool = UContext<TSSizeSort>::mkAnd,
+        desiredSort = { _, _ -> boolSort },
+    )
+
+    internal operator fun invoke(lhs: UExpr<out USort>, rhs: UExpr<out USort>, scope: TSStepScope): UExpr<out USort> {
+        val bannedSorts = lhs.tctx.banSorts(lhs, rhs)
+
+        fun apply(lhs: UExpr<out USort>, rhs: UExpr<out USort>): UExpr<out USort>? {
+            val ctx = lhs.tctx
+            val lhsSort = lhs.sort
+            val rhsSort = rhs.sort
+            assert(lhsSort == rhsSort)
+
+            if (lhsSort in bannedSorts) return null
+            if (ctx.desiredSort(lhsSort, rhsSort) != lhsSort) return null
+
+            return when (lhs.sort) {
+                is UBoolSort -> ctx.onBool(lhs.cast(), rhs.cast())
+                is UBvSort -> ctx.onBv(lhs.cast(), rhs.cast())
+                is UFpSort -> ctx.onFp(lhs.cast(), rhs.cast())
+                is UAddressSort -> ctx.onRef(lhs.cast(), rhs.cast())
+                else -> error("Unexpected sorts: $lhsSort, $rhsSort")
+            }
+        }
+
         val lhsSort = lhs.sort
         val rhsSort = rhs.sort
 
-        if (lhsSort != rhsSort) TODO("Implement type coercion")
+        val ctx = lhs.tctx
+        val sort = ctx.desiredSort(lhsSort, rhsSort)
 
         return when {
-            lhsSort is UBoolSort -> lhs.tctx.onBool(lhs.cast(), rhs.cast())
-            lhsSort is UBvSort -> lhs.tctx.onBv(lhs.cast(), rhs.cast())
-            lhsSort is UFpSort -> lhs.tctx.onFp(lhs.cast(), rhs.cast())
-
-            else -> error("Unexpected sorts: $lhsSort, $rhsSort")
+            lhs is TSWrappedValue -> lhs.coerceWithSort(rhs, ::apply, sort)
+            else -> TSWrappedValue(ctx, lhs, scope).coerceWithSort(rhs, ::apply, sort)
         }
     }
 

usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt

@@ -6,6 +6,7 @@ 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(
@@ -40,6 +41,8 @@ class TSComponents(
         return USolverBase(ctx, smtSolver, typeSolver, translator, decoder, options.solverTimeout)
     }
 
+    override fun mkStatesForkProvider(): StateForker = TSStateForker
+
     fun close() {
         closeableResources.forEach(AutoCloseable::close)
     }

usvm-ts/src/main/kotlin/org/usvm/TSContext.kt

@@ -4,6 +4,7 @@ import org.jacodb.ets.base.EtsBooleanType
 import org.jacodb.ets.base.EtsNumberType
 import org.jacodb.ets.base.EtsRefType
 import org.jacodb.ets.base.EtsType
+import org.jacodb.ets.base.EtsUnknownType
 
 typealias TSSizeSort = UBv32Sort
 
@@ -17,6 +18,7 @@ class TSContext(components: TSComponents) : UContext<TSSizeSort>(components) {
         is EtsBooleanType -> boolSort
         is EtsNumberType -> fp64Sort
         is EtsRefType -> addressSort
+        is EtsUnknownType -> addressSort
         else -> TODO("Support all JacoDB types")
     }