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

@@ -1,5 +1,6 @@
 package org.usvm
 
+import io.ksmt.expr.KBitVec32Value
 import io.ksmt.solver.yices.KYicesSolver
 import io.ksmt.solver.z3.KZ3Solver
 import io.ksmt.symfpu.solver.KSymFpuSolver
@@ -15,10 +16,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 TSFpSortSizeExprProvider(ctx as TSContext)
     }
 
     override fun mkTypeSystem(
@@ -44,3 +45,30 @@ class TSComponents(
         closeableResources.forEach(AutoCloseable::close)
     }
 }
+
+class TSFpSortSizeExprProvider(
+    override val ctx: TSContext,
+) : USizeExprProvider<TSSizeSort> {
+    override val sizeSort: TSSizeSort = ctx.sizeSort
+
+    override fun mkSizeExpr(size: Int): UExpr<TSSizeSort> = ctx.mkBv(size, sizeSort)
+    override fun getIntValue(expr: UExpr<TSSizeSort>): Int? = (expr as? KBitVec32Value)?.numberValue
+
+    override fun mkSizeSubExpr(lhs: UExpr<TSSizeSort>, rhs: UExpr<TSSizeSort>): UExpr<TSSizeSort> =
+        ctx.mkBvSubExpr(lhs, rhs)
+
+    override fun mkSizeAddExpr(lhs: UExpr<TSSizeSort>, rhs: UExpr<TSSizeSort>): UExpr<TSSizeSort> =
+        ctx.mkBvAddExpr(lhs, rhs)
+
+    override fun mkSizeGtExpr(lhs: UExpr<TSSizeSort>, rhs: UExpr<TSSizeSort>): UBoolExpr =
+        ctx.mkBvUnsignedGreaterExpr(lhs, rhs)
+
+    override fun mkSizeGeExpr(lhs: UExpr<TSSizeSort>, rhs: UExpr<TSSizeSort>): UBoolExpr =
+        ctx.mkBvUnsignedGreaterOrEqualExpr(lhs, rhs)
+
+    override fun mkSizeLtExpr(lhs: UExpr<TSSizeSort>, rhs: UExpr<TSSizeSort>): UBoolExpr =
+        ctx.mkBvUnsignedLessExpr(lhs, rhs)
+
+    override fun mkSizeLeExpr(lhs: UExpr<TSSizeSort>, rhs: UExpr<TSSizeSort>): UBoolExpr =
+        ctx.mkBvUnsignedLessOrEqualExpr(lhs, rhs)
+}

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

@@ -1,5 +1,34 @@
 package org.usvm
 
+import org.jacodb.ets.base.EtsAnyType
+import org.jacodb.ets.base.EtsBooleanType
+import org.jacodb.ets.base.EtsNumberType
+import org.jacodb.ets.base.EtsRefType
+import org.jacodb.ets.base.EtsStringType
+import org.jacodb.ets.base.EtsType
+import org.jacodb.ets.base.EtsUndefinedType
+import org.jacodb.ets.base.EtsVoidType
+
 typealias TSSizeSort = UBv32Sort
 
-class TSContext(components: TSComponents) : UContext<TSSizeSort>(components)
+class TSContext(components: TSComponents) : UContext<TSSizeSort>(components) {
+
+    val voidSort: TSVoidSort by lazy { TSVoidSort(this) }
+    val undefinedSort: TSUndefinedSort by lazy { TSUndefinedSort(this) }
+    val stringSort: TSStringSort by lazy { TSStringSort(this) }
+
+    private val undefinedValue by lazy { TSUndefinedValue(this) }
+
+    fun typeToSort(type: EtsType): USort = when (type) {
+        is EtsAnyType -> addressSort
+        is EtsVoidType -> voidSort
+        is EtsUndefinedType -> undefinedSort
+        is EtsRefType -> addressSort
+        is EtsBooleanType -> boolSort
+        is EtsNumberType -> fp64Sort
+        is EtsStringType -> stringSort
+        else -> error("Unknown type: $type")
+    }
+
+    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)
+    }
+
+}