Basic USVM TS type system with type coercion

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

@@ -37,27 +37,27 @@ jobs:
       - name: Set up ArkAnalyzer
         run: |
           REPO_URL="https://gitee.com/Lipenx/arkanalyzer.git"
-          DEST_DIR="arkanalyzer"
+          DEST_DIR="arkanalyzer" 
           MAX_RETRIES=10
           RETRY_DELAY=3  # Delay between retries in seconds  
-          BRANCH="neo/2024-08-07"
+          BRANCH="neo/2024-08-16" # Set the same as in jacodb/neo branch, since we get jacodb artifact from that branch.
 
           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/Expressions.kt

@@ -315,9 +315,53 @@
 
 //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)
+
+    // Size of exprs is not big since it generates from all sorts supported by machine [n]
+    // (small number even when finished)
+    // plus possible additional constraints which are C(n - 1, 2) in size,
+    // so no need to cache this value as its use is also limited.
+    fun not(): UBoolExpr = ctx.mkAnd(exprs.map(ctx::mkNot))
+
+    override fun accept(transformer: KTransformerBase): KExpr<UBoolSort> {
+        return transformer.apply(joinedExprs)
+    }
+
+    // TODO: draft
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other)
+
+    // TODO: draft
+    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

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

@@ -1,5 +1,6 @@
 package org.usvm
 
+import io.ksmt.utils.cast
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.model.UModelBase
 import org.usvm.solver.USatResult
@@ -45,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() -> {
@@ -56,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
                 )

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

@@ -2,36 +2,132 @@
 
 import io.ksmt.utils.cast
 
+/**
+ * @param[desiredSort] accepts two [USort] instances of the expression operands.
+ * It defines a desired [USort] for the binary operator to cast both of its operands to.
+ *
+ * @param[banSorts] accepts two [UExpr] instances of the expression operands.
+ * It returns a [Set] of [USort] that are restricted to be coerced to.
+ */
+
+// TODO: desiredSort and banSorts achieve the same goal, although have different semantics. Possible to merge them.
 sealed class TSBinaryOperator(
     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,
+    // Some binary operations like '==' and '!=' can operate on any pair of equal sorts.
+    // However, '+' casts both operands to Number in TypeScript (no considering string currently),
+    // so fp64sort is required for both sides.
+    // This function allows to filter out excess expressions in type coercion.
+    val desiredSort: TSContext.(USort, USort) -> USort = { _, _ -> error("Should not be called") },
+    // This function specifies a set of banned sorts pre-coercion.
+    // Usage of it is limited and was introduced for Neq operation.
+    // Generally designed to filter out excess expressions in type coercion.
+    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>::mkHeapRefEq,
+        desiredSort = { lhs, _ -> lhs }
     )
 
+    // Neq must not be applied to a pair of expressions
+    // containing generated ones during coercion initialization (exprCache intersection).
+    // For example,
+    // "a (ref reg reading) != 1.0 (fp64 number)"
+    // can't yield a list of type coercion bool expressions containing:
+    // "a (bool reg reading) != true (bool)",
+    // since "1.0.toBool() = true" is a new value for TSExprTransformer(1.0) exprCache.
+    //
+    // So, that's the reason why banSorts in Neq throws out all primitive types except one of the expressions' one.
+    // (because obviously we must be able to coerce to expression's base sort)
+
+    // TODO: banSorts is still draft here, it only handles specific operands' configurations. General solution required.
     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 -> mkHeapRefEq(lhs, rhs).not() },
+        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.
+                    // For example, supporting language structures could produce
+                    // incorrect additional sort constraints here if addressSort expressions
+                    // do not return empty set.
+                    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,
+        // TODO: support string concatenation here by resolving stringSort.
+        desiredSort = { _, _ -> fp64Sort },
+    )
+
+    object And : TSBinaryOperator(
+        onBool = UContext<TSSizeSort>::mkAnd,
+        desiredSort = { _, _ -> boolSort },
     )
 
-    internal operator fun invoke(lhs: UExpr<out USort>, rhs: UExpr<out USort>): UExpr<out USort> {
+    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
+            if (lhsSort != rhsSort) error("Sorts must be equal: $lhsSort != $rhsSort")
+
+            // banSorts filtering.
+            if (lhsSort in bannedSorts) return null
+            // desiredSort filtering.
+            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
+        // Chosen sort is only used to intersect both exprCaches and have at least one sort to apply binary operation to.
+        // All sorts are examined in TSExprTransformer class and not limited by this "chosen one".
+        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/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")
     }