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 = "4b15fc6452"
     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/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,22 @@
 package org.usvm
 
+import org.jacodb.ets.base.EtsBooleanType
+import org.jacodb.ets.base.EtsNumberType
+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
+        else -> TODO("Support all JacoDB types")
+    }
+
+    fun mkUndefinedValue(): TSUndefinedValue = undefinedValue
+}

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

@@ -0,0 +1,267 @@
+package org.usvm
+
+import org.jacodb.ets.base.EtsArrayAccess
+import org.jacodb.ets.base.EtsArrayLiteral
+import org.jacodb.ets.base.EtsBinaryOperation
+import org.jacodb.ets.base.EtsBooleanConstant
+import org.jacodb.ets.base.EtsCastExpr
+import org.jacodb.ets.base.EtsDeleteExpr
+import org.jacodb.ets.base.EtsEntity
+import org.jacodb.ets.base.EtsInstanceCallExpr
+import org.jacodb.ets.base.EtsInstanceFieldRef
+import org.jacodb.ets.base.EtsInstanceOfExpr
+import org.jacodb.ets.base.EtsLengthExpr
+import org.jacodb.ets.base.EtsLocal
+import org.jacodb.ets.base.EtsNewArrayExpr
+import org.jacodb.ets.base.EtsNewExpr
+import org.jacodb.ets.base.EtsNullConstant
+import org.jacodb.ets.base.EtsNumberConstant
+import org.jacodb.ets.base.EtsObjectLiteral
+import org.jacodb.ets.base.EtsParameterRef
+import org.jacodb.ets.base.EtsRelationOperation
+import org.jacodb.ets.base.EtsStaticCallExpr
+import org.jacodb.ets.base.EtsStaticFieldRef
+import org.jacodb.ets.base.EtsStringConstant
+import org.jacodb.ets.base.EtsThis
+import org.jacodb.ets.base.EtsType
+import org.jacodb.ets.base.EtsTypeOfExpr
+import org.jacodb.ets.base.EtsUnaryOperation
+import org.jacodb.ets.base.EtsUndefinedConstant
+import org.jacodb.ets.base.EtsValue
+import org.jacodb.ets.model.EtsMethod
+import org.usvm.memory.URegisterStackLValue
+
+@Suppress("UNUSED_PARAMETER")
+class TSExprResolver(
+    private val ctx: TSContext,
+    private val scope: TSStepScope,
+    private val localToIdx: (EtsMethod, EtsValue) -> Int,
+) : EtsEntity.Visitor<UExpr<out USort>> {
+
+    val simpleValueResolver: TSSimpleValueResolver = TSSimpleValueResolver(
+        ctx,
+        scope,
+        localToIdx
+    )
+
+    fun resolveTSExpr(expr: EtsEntity, type: EtsType = expr.type): UExpr<out USort>? {
+        TODO()
+    }
+
+    override fun visit(value: EtsLocal): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(value: EtsArrayLiteral): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(value: EtsBooleanConstant): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(value: EtsNullConstant): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(value: EtsNumberConstant): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(value: EtsObjectLiteral): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(value: EtsStringConstant): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(value: EtsUndefinedConstant): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsBinaryOperation): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsCastExpr): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsDeleteExpr): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsInstanceCallExpr): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsInstanceOfExpr): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsLengthExpr): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsNewArrayExpr): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsNewExpr): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsRelationOperation): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsStaticCallExpr): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsTypeOfExpr): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsUnaryOperation): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(ref: EtsArrayAccess): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(ref: EtsInstanceFieldRef): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(ref: EtsParameterRef): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(ref: EtsStaticFieldRef): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(ref: EtsThis): UExpr<out USort> {
+        TODO("Not yet implemented")
+    }
+}
+
+class TSSimpleValueResolver(
+    private val ctx: TSContext,
+    private val scope: TSStepScope,
+    private val localToIdx: (EtsMethod, EtsValue) -> Int,
+) : EtsEntity.Visitor<UExpr<out USort>> {
+
+    override fun visit(value: EtsLocal): UExpr<out USort> = with(ctx) {
+        val lValue = resolveLocal(value)
+        return scope.calcOnState { memory.read(lValue) }
+    }
+
+    override fun visit(value: EtsArrayLiteral): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(value: EtsBooleanConstant): UExpr<out USort> = with(ctx) {
+        mkBool(value.value)
+    }
+
+    override fun visit(value: EtsNullConstant): UExpr<out USort> = with(ctx) {
+        nullRef
+    }
+
+    override fun visit(value: EtsNumberConstant): UExpr<out USort> = with(ctx) {
+        mkFp64(value.value)
+    }
+
+    override fun visit(value: EtsObjectLiteral): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(value: EtsStringConstant): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(value: EtsUndefinedConstant): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsBinaryOperation): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsCastExpr): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsDeleteExpr): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsInstanceCallExpr): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsInstanceOfExpr): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsLengthExpr): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsNewArrayExpr): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsNewExpr): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsRelationOperation): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsStaticCallExpr): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsTypeOfExpr): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(expr: EtsUnaryOperation): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(ref: EtsArrayAccess): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(ref: EtsInstanceFieldRef): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(ref: EtsParameterRef): UExpr<out USort> = with(ctx) {
+        val lValue = resolveLocal(ref)
+        return scope.calcOnState { memory.read(lValue) }
+    }
+
+    override fun visit(ref: EtsStaticFieldRef): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    override fun visit(ref: EtsThis): UExpr<out USort> = with(ctx) {
+        TODO("Not yet implemented")
+    }
+
+    fun resolveLocal(local: EtsValue): URegisterStackLValue<*> {
+        val method = requireNotNull(scope.calcOnState { lastEnteredMethod })
+        val localIdx = localToIdx(method, local)
+        val sort = ctx.typeToSort(local.type)
+        return URegisterStackLValue(sort, localIdx)
+    }
+
+}

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

@@ -0,0 +1,34 @@
+package org.usvm
+
+import io.ksmt.KAst
+import io.ksmt.cache.hash
+import io.ksmt.cache.structurallyEqual
+import io.ksmt.expr.printer.ExpressionPrinter
+import io.ksmt.expr.transformer.KTransformerBase
+import io.ksmt.sort.KSortVisitor
+
+val KAst.tctx get() = ctx as TSContext
+
+class TSUndefinedSort(ctx: TSContext) : USort(ctx) {
+    override fun print(builder: StringBuilder) {
+        builder.append("undefined sort")
+    }
+
+    override fun <T> accept(visitor: KSortVisitor<T>): T = error("Should not be called")
+}
+
+class TSUndefinedValue(ctx: TSContext) : UExpr<TSUndefinedSort>(ctx) {
+    override val sort: TSUndefinedSort
+        get() = tctx.undefinedSort
+
+    override fun accept(transformer: KTransformerBase): TSUndefinedValue = this
+
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other)
+
+    override fun internHashCode(): Int = hash()
+
+    override fun print(printer: ExpressionPrinter) {
+        printer.append("undefined")
+    }
+
+}