Introduction of TypeScript symbolic machine

buildSrc/src/main/kotlin/Dependencies.kt

@@ -126,6 +126,11 @@ object Libs {
         name = "jacodb-api-jvm",
         version = Versions.jacodb
     )
+    val jacodb_ets = dep(
+        group = jacodbPackage,
+        name = "jacodb-ets",
+        version =  Versions.jacodb
+    )
     val jacodb_api_common = dep(
         group = jacodbPackage,
         name = "jacodb-api-common",

settings.gradle.kts

@@ -2,6 +2,7 @@ rootProject.name = "usvm"
 
 include("usvm-core")
 include("usvm-jvm")
+include("usvm-ts")
 include("usvm-util")
 include("usvm-jvm-instrumentation")
 include("usvm-sample-language")

usvm-ts/build.gradle.kts

@@ -0,0 +1,23 @@
+plugins {
+    id("usvm.kotlin-conventions")
+}
+
+dependencies {
+    implementation(project(":usvm-core"))
+
+    implementation(Libs.jacodb_core)
+    implementation(Libs.jacodb_ets)
+
+    implementation(Libs.ksmt_yices)
+    implementation(Libs.ksmt_cvc5)
+    implementation(Libs.ksmt_symfpu)
+    implementation(Libs.ksmt_runner)
+
+    testImplementation(Libs.mockk)
+    testImplementation(Libs.junit_jupiter_params)
+    testImplementation(Libs.logback)
+
+    // https://mvnrepository.com/artifact/org.burningwave/core
+    // Use it to export all modules to all
+    testImplementation("org.burningwave:core:12.62.7")
+}

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

@@ -0,0 +1,35 @@
+package org.usvm
+
+import org.jacodb.ets.base.EtsStmt
+import org.jacodb.ets.graph.EtsApplicationGraph
+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)
+
+    override fun predecessors(node: EtsStmt): Sequence<EtsStmt> =
+        applicationGraph.predecessors(node)
+
+    override fun successors(node: EtsStmt): Sequence<EtsStmt> =
+        applicationGraph.successors(node)
+
+    override fun callees(node: EtsStmt): Sequence<EtsMethod> =
+        applicationGraph.callees(node)
+
+    override fun callers(method: EtsMethod): Sequence<EtsStmt> =
+        applicationGraph.callers(method)
+
+    override fun entryPoints(method: EtsMethod): Sequence<EtsStmt> =
+        applicationGraph.entryPoints(method)
+
+    override fun exitPoints(method: EtsMethod): Sequence<EtsStmt> =
+        applicationGraph.exitPoints(method)
+
+    override fun methodOf(node: EtsStmt): EtsMethod =
+        applicationGraph.methodOf(node)
+
+    override fun statementsOf(method: EtsMethod): Sequence<EtsStmt> =
+        method.cfg.stmts.asSequence()
+}

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

@@ -0,0 +1,46 @@
+package org.usvm
+
+import io.ksmt.solver.yices.KYicesSolver
+import io.ksmt.solver.z3.KZ3Solver
+import io.ksmt.symfpu.solver.KSymFpuSolver
+import org.jacodb.ets.base.EtsType
+import org.usvm.solver.USolverBase
+import org.usvm.solver.UTypeSolver
+import org.usvm.types.UTypeSystem
+
+class TSComponents(
+    private val typeSystem: TSTypeSystem,
+    private val options: UMachineOptions,
+) : UComponents<EtsType, TSSizeSort> {
+    private val closeableResources = mutableListOf<AutoCloseable>()
+
+    override val useSolverForForks: Boolean
+        get() = TODO("Not yet implemented")
+
+    override fun <Context : UContext<TSSizeSort>> mkSizeExprProvider(ctx: Context): USizeExprProvider<TSSizeSort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun mkTypeSystem(
+        ctx: UContext<TSSizeSort>,
+    ): UTypeSystem<EtsType> = typeSystem
+
+    override fun <Context : UContext<TSSizeSort>> mkSolver(ctx: Context): USolverBase<EtsType> {
+        val (translator, decoder) = buildTranslatorAndLazyDecoder(ctx)
+
+        val smtSolver = when (options.solverType) {
+            SolverType.YICES -> KSymFpuSolver(KYicesSolver(ctx), ctx)
+            SolverType.Z3 -> KZ3Solver(ctx)
+        }
+
+        closeableResources += smtSolver
+
+        val typeSolver = UTypeSolver(typeSystem)
+
+        return USolverBase(ctx, smtSolver, typeSolver, translator, decoder, options.solverTimeout)
+    }
+
+    fun close() {
+        closeableResources.forEach(AutoCloseable::close)
+    }
+}

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

@@ -0,0 +1,5 @@
+package org.usvm
+
+typealias TSSizeSort = UBv32Sort
+
+class TSContext(components: TSComponents) : UContext<TSSizeSort>(components)

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

@@ -0,0 +1,77 @@
+package org.usvm
+
+import io.ksmt.utils.asExpr
+import org.jacodb.ets.base.EtsStmt
+import org.jacodb.ets.base.EtsType
+import org.jacodb.ets.model.EtsMethod
+import org.usvm.forkblacklists.UForkBlackList
+import org.usvm.memory.URegisterStackLValue
+import org.usvm.solver.USatResult
+import org.usvm.state.TSMethodResult
+import org.usvm.state.TSState
+import org.usvm.state.lastStmt
+import org.usvm.targets.UTargetsSet
+
+class TSInterpreter(
+    private val ctx: TSContext,
+    private val applicationGraph: TSApplicationGraph,
+) : UInterpreter<TSState>() {
+    private val forkBlackList: UForkBlackList<TSState, EtsStmt> = UForkBlackList.createDefault()
+
+    override fun step(state: TSState): StepResult<TSState> {
+        val stmt = state.lastStmt
+        val scope = StepScope(state, forkBlackList)
+
+        val result = state.methodResult
+        if (result is TSMethodResult.TSException) {
+            // TODO catch processing
+            scope.doWithState {
+                val returnSite = callStack.pop()
+
+                if (callStack.isNotEmpty()) {
+                    memory.stack.pop()
+                }
+
+                if (returnSite != null) {
+                    newStmt(returnSite)
+                }
+            }
+
+            return scope.stepResult()
+        }
+
+        // TODO: interpreter
+        stmt.nextStmt?.let { nextStmt ->
+            scope.doWithState { newStmt(nextStmt) }
+        }
+
+        return scope.stepResult()
+    }
+
+    fun getInitialState(method: EtsMethod, targets: List<TSTarget>): TSState {
+        val state = TSState(ctx, method, targets = UTargetsSet.from(targets))
+
+        with(ctx) {
+            val params = List(method.parameters.size) { idx ->
+                URegisterStackLValue(addressSort, idx)
+            }
+            val refs = params.map { state.memory.read(it) }
+
+            // TODO check correctness of constraints and process this instance
+            state.pathConstraints += mkAnd(refs.map { mkEq(it.asExpr(addressSort), nullRef).not() })
+        }
+
+        val solver = ctx.solver<EtsType>()
+        val model = (solver.check(state.pathConstraints) as USatResult).model
+        state.models = listOf(model)
+
+        state.callStack.push(method, returnSite = null)
+        state.memory.stack.push(method.parameters.size, method.localsCount)
+        state.pathNode += method.cfg.instructions.first()
+
+        return state
+    }
+
+    // TODO: expand with interpreter implementation
+    private val EtsStmt.nextStmt get() = applicationGraph.successors(this).firstOrNull()
+}

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

@@ -0,0 +1,110 @@
+package org.usvm
+
+import org.jacodb.ets.base.EtsStmt
+import org.jacodb.ets.model.EtsFile
+import org.jacodb.ets.model.EtsMethod
+import org.usvm.ps.createPathSelector
+import org.usvm.state.TSMethodResult
+import org.usvm.state.TSState
+import org.usvm.statistics.CompositeUMachineObserver
+import org.usvm.statistics.CoverageStatistics
+import org.usvm.statistics.StepsStatistics
+import org.usvm.statistics.TimeStatistics
+import org.usvm.statistics.UMachineObserver
+import org.usvm.statistics.collectors.AllStatesCollector
+import org.usvm.statistics.collectors.CoveredNewStatesCollector
+import org.usvm.statistics.collectors.TargetsReachedStatesCollector
+import org.usvm.statistics.distances.CfgStatisticsImpl
+import org.usvm.statistics.distances.PlainCallGraphStatistics
+import org.usvm.stopstrategies.createStopStrategy
+import kotlin.time.Duration.Companion.seconds
+
+class TSMachine(
+    private val project: EtsFile,
+    private val options: UMachineOptions,
+) : UMachine<TSState>() {
+    private val typeSystem = TSTypeSystem(typeOperationsTimeout = 1.seconds, project)
+    private val components = TSComponents(typeSystem, options)
+    private val ctx = TSContext(components)
+    private val applicationGraph = TSApplicationGraph(project)
+    private val interpreter = TSInterpreter(ctx, applicationGraph)
+    private val cfgStatistics = CfgStatisticsImpl(applicationGraph)
+
+    fun analyze(
+        methods: List<EtsMethod>,
+        targets: List<TSTarget> = emptyList(),
+    ): List<TSState> {
+        val initialStates = mutableMapOf<EtsMethod, TSState>()
+        methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) }
+
+        val methodsToTrackCoverage =
+            when (options.coverageZone) {
+                CoverageZone.METHOD, CoverageZone.TRANSITIVE -> methods.toHashSet()
+                CoverageZone.CLASS -> TODO("Unsupported yet")
+            }
+
+        val coverageStatistics = CoverageStatistics<EtsMethod, EtsStmt, TSState>(
+            methodsToTrackCoverage,
+            applicationGraph
+        )
+
+        val callGraphStatistics: PlainCallGraphStatistics<EtsMethod> =
+            when (options.targetSearchDepth) {
+                0u -> PlainCallGraphStatistics()
+                else -> TODO("Unsupported yet")
+            }
+
+        val timeStatistics = TimeStatistics<EtsMethod, TSState>()
+
+        val pathSelector = createPathSelector(
+            initialStates,
+            options,
+            applicationGraph,
+            timeStatistics,
+            { coverageStatistics },
+            { cfgStatistics },
+            { callGraphStatistics },
+        )
+
+        val statesCollector =
+            when (options.stateCollectionStrategy) {
+                StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector<TSState>(coverageStatistics) {
+                    it.methodResult is TSMethodResult.TSException
+                }
+
+                StateCollectionStrategy.REACHED_TARGET -> TargetsReachedStatesCollector()
+                StateCollectionStrategy.ALL -> AllStatesCollector()
+            }
+
+        val observers = mutableListOf<UMachineObserver<TSState>>(coverageStatistics)
+        observers.add(statesCollector)
+
+        val stepsStatistics = StepsStatistics<EtsMethod, TSState>()
+
+        val stopStrategy = createStopStrategy(
+            options,
+            targets,
+            timeStatisticsFactory = { timeStatistics },
+            stepsStatisticsFactory = { stepsStatistics },
+            coverageStatisticsFactory = { coverageStatistics },
+            getCollectedStatesCount = { statesCollector.collectedStates.size }
+        )
+
+        observers.add(timeStatistics)
+        observers.add(stepsStatistics)
+
+        run(
+            interpreter,
+            pathSelector,
+            observer = CompositeUMachineObserver(observers),
+            isStateTerminated = { state -> state.callStack.isEmpty() },
+            stopStrategy = stopStrategy
+        )
+
+        return statesCollector.collectedStates
+    }
+
+    override fun close() {
+        components.close()
+    }
+}

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

@@ -0,0 +1,6 @@
+package org.usvm
+
+import org.jacodb.ets.base.EtsStmt
+import org.usvm.targets.UTarget
+
+class TSTarget : UTarget<EtsStmt, TSTarget>()

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

@@ -0,0 +1,11 @@
+package org.usvm
+
+import org.jacodb.ets.base.EtsStmt
+
+class TSTest(
+    val parameters: List<Any>,
+    val resultValue: Any?,
+    val trace: List<EtsStmt>? = null,
+)
+
+class TSMethodCoverage

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

@@ -0,0 +1,36 @@
+package org.usvm
+
+import org.jacodb.ets.base.EtsType
+import org.jacodb.ets.model.EtsFile
+import org.usvm.types.UTypeStream
+import org.usvm.types.UTypeSystem
+import kotlin.time.Duration
+
+class TSTypeSystem(
+    override val typeOperationsTimeout: Duration,
+    val project: EtsFile,
+) : UTypeSystem<EtsType> {
+    override fun isSupertype(supertype: EtsType, type: EtsType): Boolean {
+        TODO("Not yet implemented")
+    }
+
+    override fun hasCommonSubtype(type: EtsType, types: Collection<EtsType>): Boolean {
+        TODO("Not yet implemented")
+    }
+
+    override fun isFinal(type: EtsType): Boolean {
+        TODO("Not yet implemented")
+    }
+
+    override fun isInstantiable(type: EtsType): Boolean {
+        TODO("Not yet implemented")
+    }
+
+    override fun findSubtypes(type: EtsType): Sequence<EtsType> {
+        TODO("Not yet implemented")
+    }
+
+    override fun topTypeStream(): UTypeStream<EtsType> {
+        TODO("Not yet implemented")
+    }
+}

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

@@ -0,0 +1,8 @@
+package org.usvm
+
+import org.jacodb.ets.base.EtsStmt
+import org.usvm.state.TSState
+
+fun TSState.newStmt(stmt: EtsStmt) {
+    pathNode += stmt
+}