TS symbolic machine expansion (#201)

* [WIP] TSTypeSystem

* Enhance TSTypeSystem + jacodb version update

* TSTypeSystem + TSInterpreter skeleton + TSSimpleValueResolver

* Version hotfix

* Minor polishing

* Remove TSTypeSystem

* Remove redundant class

* Remove unfinished types processing

* Detekt fix

* [WIP] Args location tests

* Implement parameters resolver with tests

* Remove EtsMethod.localIdx method

* [WIP] Dev sync

* Implement property matchers

* Detekt fix

* Refactor comment

* TypeTransformer change with null

* Auto conversion for tests

* Remove check

* Update jacodb version

* Fix if branch index order

* Update CI

---------

Co-authored-by: Alexey Menshutin <alex.menshutin99@gmail.com>

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

@@ -29,6 +29,38 @@ jobs:
       - name: Setup Gradle
         uses: gradle/gradle-build-action@v2
 
+      - name: Set up Node
+        uses: actions/setup-node@v4
+        with:
+          node-version: '22'
+
+      - name: Set up ArkAnalyzer
+        run: |
+          REPO_URL="https://gitee.com/Lipenx/arkanalyzer.git"
+          DEST_DIR="arkanalyzer"
+          MAX_RETRIES=10
+          RETRY_DELAY=3  # Delay between retries in seconds  
+          BRANCH="neo/2024-08-07"
+
+          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
+
       - name: Install CPython optional dependencies
         run: |
           sudo apt-get update

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

@@ -0,0 +1,42 @@
+package org.usvm
+
+import io.ksmt.utils.cast
+
+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,
+) {
+
+    object Eq : TSBinaryOperator(
+        onBool = UContext<TSSizeSort>::mkEq,
+        onBv = UContext<TSSizeSort>::mkEq,
+        onFp = UContext<TSSizeSort>::mkFpEqualExpr,
+    )
+
+    object Neq : TSBinaryOperator(
+        onBool = { lhs, rhs -> lhs.neq(rhs) },
+        onBv = { lhs, rhs -> lhs.neq(rhs) },
+        onFp = { lhs, rhs -> mkFpEqualExpr(lhs, rhs).not() },
+    )
+
+    internal operator fun invoke(lhs: UExpr<out USort>, rhs: UExpr<out USort>): UExpr<out USort> {
+        val lhsSort = lhs.sort
+        val rhsSort = rhs.sort
+
+        if (lhsSort != rhsSort) TODO("Implement type coercion")
+
+        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")
+        }
+    }
+
+    companion object {
+        private val shouldNotBeCalled: TSContext.(UExpr<out USort>, UExpr<out USort>) -> UExpr<out USort> =
+            { _, _ -> error("Should not be called") }
+    }
+}

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

@@ -15,10 +15,10 @@ class TSComponents(
     private val closeableResources = mutableListOf<AutoCloseable>()
 
     override val useSolverForForks: Boolean
-        get() = TODO("Not yet implemented")
+        get() = options.useSolverForForks
 
     override fun <Context : UContext<TSSizeSort>> mkSizeExprProvider(ctx: Context): USizeExprProvider<TSSizeSort> {
-        TODO("Not yet implemented")
+        return UBv32SizeExprProvider(ctx)
     }
 
     override fun mkTypeSystem(

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

@@ -1,5 +1,24 @@
 package org.usvm
 
+import org.jacodb.ets.base.EtsBooleanType
+import org.jacodb.ets.base.EtsNumberType
+import org.jacodb.ets.base.EtsRefType
+import org.jacodb.ets.base.EtsType
+
 typealias TSSizeSort = UBv32Sort
 
-class TSContext(components: TSComponents) : UContext<TSSizeSort>(components)
+class TSContext(components: TSComponents) : UContext<TSSizeSort>(components) {
+
+    val undefinedSort: TSUndefinedSort by lazy { TSUndefinedSort(this) }
+
+    private val undefinedValue by lazy { TSUndefinedValue(this) }
+
+    fun typeToSort(type: EtsType): USort = when (type) {
+        is EtsBooleanType -> boolSort
+        is EtsNumberType -> fp64Sort
+        is EtsRefType -> addressSort
+        else -> TODO("Support all JacoDB types")
+    }
+
+    fun mkUndefinedValue(): TSUndefinedValue = undefinedValue
+}