TS symbolic machine expansion

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 = "30594f5f7c"
+    const val jacodb = "4164b3cc64"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "1.9.20"

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

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

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
+}