diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 1e312d34fe..09d1e6cdbd 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "5acbadfed0" + const val jacodb = "213f9a1aee" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" diff --git a/buildSrc/src/main/kotlin/usvm.kotlin-conventions.gradle.kts b/buildSrc/src/main/kotlin/usvm.kotlin-conventions.gradle.kts index 1ae09d4c0e..3ab7152463 100644 --- a/buildSrc/src/main/kotlin/usvm.kotlin-conventions.gradle.kts +++ b/buildSrc/src/main/kotlin/usvm.kotlin-conventions.gradle.kts @@ -44,17 +44,25 @@ tasks { } } -tasks.named("test") { - // Use JUnit Platform for unit tests. - useJUnitPlatform() - +tasks.withType { maxHeapSize = "4G" - testLogging { events("passed") } } +tasks.test { + useJUnitPlatform { + excludeTags("manual") + } +} + +tasks.create("manualTest", Test::class) { + useJUnitPlatform { + includeTags("manual") + } +} + publishing { repositories { maven { diff --git a/settings.gradle.kts b/settings.gradle.kts index 6af778f65f..428d679fce 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -52,7 +52,7 @@ findProject(":usvm-python:usvm-python-runner")?.name = "usvm-python-runner" include("usvm-python:usvm-python-commons") findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons" -// Actually, `includeBuild("../jacodb")` is enough, but there is a bug in IDEA when path is a symlink. +// Actually, relative path is enough, but there is a bug in IDEA when the path is a symlink. // As a workaround, we convert it to a real absolute path. // See IDEA bug: https://youtrack.jetbrains.com/issue/IDEA-329756 // val jacodbPath = file("jacodb").takeIf { it.exists() } diff --git a/usvm-ts-dataflow/build.gradle.kts b/usvm-ts-dataflow/build.gradle.kts index af70818e26..14d188e0b6 100644 --- a/usvm-ts-dataflow/build.gradle.kts +++ b/usvm-ts-dataflow/build.gradle.kts @@ -30,6 +30,7 @@ dependencies { testFixturesImplementation(Libs.kotlin_logging) testFixturesImplementation(Libs.junit_jupiter_api) + testFixturesImplementation(Libs.kotlinx_coroutines_core) } tasks.withType { diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt index f530d25418..a9cd0ec33a 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt @@ -52,6 +52,7 @@ import org.usvm.dataflow.ts.infer.createApplicationGraph import org.usvm.dataflow.ts.infer.toType import org.usvm.dataflow.ts.loadEtsProjectFromResources import org.usvm.dataflow.ts.testFactory +import org.usvm.dataflow.ts.testForEach import org.usvm.dataflow.ts.util.EtsTraits import org.usvm.dataflow.ts.util.sortedBy import org.usvm.dataflow.ts.util.sortedByBase @@ -353,70 +354,67 @@ class EtsTypeInferenceTest { val allCases = project.projectClasses.filter { it.name.startsWith("Case") } - for (cls in allCases) { - if (cls.name in disabledTests) continue - test(name = cls.name) { - logger.info { "Analyzing testcase: ${cls.name}" } - - val inferMethod = cls.methods.single { it.name == "infer" } - logger.info { "Found infer: ${inferMethod.signature}" } - - val expectedTypeString = mutableMapOf() - var expectedReturnTypeString = "" - for (inst in inferMethod.cfg.stmts) { - if (inst is EtsAssignStmt) { - val lhv = inst.lhv - if (lhv is EtsLocal) { - val rhv = inst.rhv - if (lhv.name.startsWith("EXPECTED_ARG_")) { - check(rhv is EtsStringConstant) - val arg = lhv.name.removePrefix("EXPECTED_ARG_").toInt() - val pos = AccessPathBase.Arg(arg) - expectedTypeString[pos] = rhv.value - logger.info { "Expected type for $pos: ${rhv.value}" } - } else if (lhv.name == "EXPECTED_RETURN") { - check(rhv is EtsStringConstant) - expectedReturnTypeString = rhv.value - logger.info { "Expected return type: ${rhv.value}" } - } else if (lhv.name.startsWith("EXPECTED")) { - logger.error { "Skipping unexpected local: $lhv" } - } + testForEach(allCases.filterNot { it.name in disabledTests }, { it.name }) { cls -> + logger.info { "Analyzing testcase: ${cls.name}" } + + val inferMethod = cls.methods.single { it.name == "infer" } + logger.info { "Found infer: ${inferMethod.signature}" } + + val expectedTypeString = mutableMapOf() + var expectedReturnTypeString = "" + for (inst in inferMethod.cfg.stmts) { + if (inst is EtsAssignStmt) { + val lhv = inst.lhv + if (lhv is EtsLocal) { + val rhv = inst.rhv + if (lhv.name.startsWith("EXPECTED_ARG_")) { + check(rhv is EtsStringConstant) + val arg = lhv.name.removePrefix("EXPECTED_ARG_").toInt() + val pos = AccessPathBase.Arg(arg) + expectedTypeString[pos] = rhv.value + logger.info { "Expected type for $pos: ${rhv.value}" } + } else if (lhv.name == "EXPECTED_RETURN") { + check(rhv is EtsStringConstant) + expectedReturnTypeString = rhv.value + logger.info { "Expected return type: ${rhv.value}" } + } else if (lhv.name.startsWith("EXPECTED")) { + logger.error { "Skipping unexpected local: $lhv" } } } } + } - val entrypoint = cls.methods.single { it.name == "entrypoint" } - logger.info { "Found entrypoint: ${entrypoint.signature}" } - - val manager = TypeInferenceManager(EtsTraits(), graph) - val result = manager.analyze(listOf(entrypoint), doAddKnownTypes = false) - - val inferredTypes = result.inferredTypes[inferMethod] - ?: error( - "No inferred types for method ${ - inferMethod.signature.enclosingClass.name - }::${inferMethod.name}" - ) - - for ((position, expected) in expectedTypeString.sortedByBase()) { - val inferred = inferredTypes[position] - logger.info { "Inferred type for $position: $inferred" } - val passed = inferred.toString() == expected - assertTrue( - passed, - "Inferred type for $position does not match: inferred = $inferred, expected = $expected" - ) - } - if (expectedReturnTypeString.isNotBlank()) { - val expected = expectedReturnTypeString - val inferred = result.inferredReturnType[inferMethod] - logger.info { "Inferred return type: $inferred" } - val passed = inferred.toString() == expected - assertTrue( - passed, - "Inferred return type does not match: inferred = $inferred, expected = $expected" - ) - } + val entrypoint = cls.methods.single { it.name == "entrypoint" } + logger.info { "Found entrypoint: ${entrypoint.signature}" } + + val manager = TypeInferenceManager(EtsTraits(), graph) + val result = manager.analyze(listOf(entrypoint), doAddKnownTypes = false) + + val inferredTypes = result.inferredTypes[inferMethod] + ?: error( + "No inferred types for method ${ + inferMethod.signature.enclosingClass.name + }::${inferMethod.name}" + ) + + for ((position, expected) in expectedTypeString.sortedByBase()) { + val inferred = inferredTypes[position] + logger.info { "Inferred type for $position: $inferred" } + val passed = inferred.toString() == expected + assertTrue( + passed, + "Inferred type for $position does not match: inferred = $inferred, expected = $expected" + ) + } + if (expectedReturnTypeString.isNotBlank()) { + val expected = expectedReturnTypeString + val inferred = result.inferredReturnType[inferMethod] + logger.info { "Inferred return type: $inferred" } + val passed = inferred.toString() == expected + assertTrue( + passed, + "Inferred return type does not match: inferred = $inferred, expected = $expected" + ) } } } @@ -440,191 +438,188 @@ class EtsTypeInferenceTest { logger.warn { "No projects found" } return@testFactory } - for (projectName in availableProjectNames) { - // if (projectName != "...") continue + testForEach(availableProjectNames, { it }) { projectName -> // skip 'PrintSpooler' project for now, it has issues with types if (projectName == "PrintSpooler") { logger.info { "Skipping project: $projectName" } - continue + return@testForEach } - test("infer types in $projectName") { - logger.info { "Loading project: $projectName" } - val projectPath = getResourcePath("/projects/$projectName") - val etsirPath = projectPath / "etsir" - if (!etsirPath.exists()) { - logger.warn { "No etsir directory found for project $projectName" } - return@test - } - val modules = etsirPath.listDirectoryEntries().filter { it.isDirectory() }.map { it.name } - logger.info { "Found ${modules.size} modules: $modules" } - if (modules.isEmpty()) { - logger.warn { "No modules found for project $projectName" } - return@test - } - val project = loadEtsProjectFromResources(modules, "/projects/$projectName/etsir") + logger.info { "Loading project: $projectName" } + val projectPath = getResourcePath("/projects/$projectName") + val etsirPath = projectPath / "etsir" + if (!etsirPath.exists()) { + logger.warn { "No etsir directory found for project $projectName" } + return@testForEach + } + val modules = etsirPath.listDirectoryEntries().filter { it.isDirectory() }.map { it.name } + logger.info { "Found ${modules.size} modules: $modules" } + if (modules.isEmpty()) { + logger.warn { "No modules found for project $projectName" } + return@testForEach + } + val project = loadEtsProjectFromResources(modules, "/projects/$projectName/etsir") + logger.info { + "Loaded project with ${ + project.projectClasses.size + } classes and ${project.projectClasses.sumOf { it.methods.size }} methods" + } + for (cls in project.projectClasses.sortedBy { it.name }) { logger.info { - "Loaded project with ${ - project.projectClasses.size - } classes and ${project.projectClasses.sumOf { it.methods.size }} methods" - } - for (cls in project.projectClasses.sortedBy { it.name }) { - logger.info { - buildString { - appendLine("Class ${cls.name} has ${cls.methods.size} methods") - for (method in cls.methods.sortedBy { it.name }) { - appendLine("- $method") - } + buildString { + appendLine("Class ${cls.name} has ${cls.methods.size} methods") + for (method in cls.methods.sortedBy { it.name }) { + appendLine("- $method") } } } - val graph = createApplicationGraph(project) - - val entrypoints = project.projectClasses - .flatMap { it.methods } - .filter { it.isPublic } - logger.info { "Found ${entrypoints.size} entrypoints" } - - val manager = TypeInferenceManager(EtsTraits(), graph) - val result = manager.analyze(entrypoints) - - logger.info { - buildString { - appendLine("Inferred types: ${result.inferredTypes.size}") - for ((method, types) in result.inferredTypes.sortedBy { it.key.toString() }) { - appendLine() - appendLine("- $method") - for ((pos, type) in types.sortedByBase()) { - appendLine("$pos: ${type.toStringLimited()}") - } + } + val graph = createApplicationGraph(project) + + val entrypoints = project.projectClasses + .flatMap { it.methods } + .filter { it.isPublic } + logger.info { "Found ${entrypoints.size} entrypoints" } + + val manager = TypeInferenceManager(EtsTraits(), graph) + val result = manager.analyze(entrypoints) + + logger.info { + buildString { + appendLine("Inferred types: ${result.inferredTypes.size}") + for ((method, types) in result.inferredTypes.sortedBy { it.key.toString() }) { + appendLine() + appendLine("- $method") + for ((pos, type) in types.sortedByBase()) { + appendLine("$pos: ${type.toStringLimited()}") } } } - logger.info { - buildString { + } + logger.info { + buildString { + appendLine( + "Inferred return types: ${ + result.inferredReturnType.size + }" + ) + val res = result.inferredReturnType.sortedBy { it.key.toString() } + for ((method, returnType) in res) { appendLine( - "Inferred return types: ${ - result.inferredReturnType.size + "${ + method.signature.enclosingClass.name + }::${ + method.name + }: ${ + returnType.toStringLimited() }" ) - val res = result.inferredReturnType.sortedBy { it.key.toString() } - for ((method, returnType) in res) { - appendLine( - "${ - method.signature.enclosingClass.name - }::${ - method.name - }: ${ - returnType.toStringLimited() - }" - ) - } } } - logger.info { - buildString { + } + logger.info { + buildString { + appendLine( + "Inferred combined this types: ${ + result.inferredCombinedThisType.size + }" + ) + val res = result.inferredCombinedThisType.sortedBy { it.key.toString() } + for ((clazz, thisType) in res) { appendLine( - "Inferred combined this types: ${ - result.inferredCombinedThisType.size + "${clazz.name} in ${clazz.file}: ${ + thisType.toStringLimited() }" ) - val res = result.inferredCombinedThisType.sortedBy { it.key.toString() } - for ((clazz, thisType) in res) { - appendLine( - "${clazz.name} in ${clazz.file}: ${ - thisType.toStringLimited() - }" - ) - } } } + } - var totalNumMatchedNormal = 0 - var totalNumMatchedUnknown = 0 - var totalNumMismatchedNormal = 0 - var totalNumLostNormal = 0 - var totalNumBetterThanUnknown = 0 - - for ((method, inferredTypes) in result.inferredTypes) { - var numMatchedNormal = 0 - var numMatchedUnknown = 0 - var numMismatchedNormal = 0 - var numLostNormal = 0 - var numBetterThanUnknown = 0 - - for (local in method.getLocals()) { - val inferredType = inferredTypes[AccessPathBase.Local(local.name)]?.toType() - val verdict = if (inferredType != null) { - if (local.type.isUnknown()) { - if (inferredType.isUnknown()) { - numMatchedUnknown++ - "Matched unknown" - } else { - numBetterThanUnknown++ - "Better than unknown" - } + var totalNumMatchedNormal = 0 + var totalNumMatchedUnknown = 0 + var totalNumMismatchedNormal = 0 + var totalNumLostNormal = 0 + var totalNumBetterThanUnknown = 0 + + for ((method, inferredTypes) in result.inferredTypes) { + var numMatchedNormal = 0 + var numMatchedUnknown = 0 + var numMismatchedNormal = 0 + var numLostNormal = 0 + var numBetterThanUnknown = 0 + + for (local in method.getLocals()) { + val inferredType = inferredTypes[AccessPathBase.Local(local.name)]?.toType() + val verdict = if (inferredType != null) { + if (local.type.isUnknown()) { + if (inferredType.isUnknown()) { + numMatchedUnknown++ + "Matched unknown" } else { - if (inferredType == local.type) { - numMatchedNormal++ - "Matched normal" - } else { - numMismatchedNormal++ - "Mismatched normal" - } + numBetterThanUnknown++ + "Better than unknown" } } else { - if (local.type.isUnknown()) { - numMatchedUnknown++ - "Matched (lost) unknown" + if (inferredType == local.type) { + numMatchedNormal++ + "Matched normal" } else { - numLostNormal++ - "Lost normal" + numMismatchedNormal++ + "Mismatched normal" } } - logger.info { - "Local $local in $method, type: ${ - local.type.toStringLimited() - }, inferred: ${ - inferredType?.toStringLimited() - }, verdict: $verdict" + } else { + if (local.type.isUnknown()) { + numMatchedUnknown++ + "Matched (lost) unknown" + } else { + numLostNormal++ + "Lost normal" } } - logger.info { - buildString { - appendLine( - "Local type matching for ${ - method.signature.enclosingClass.name - }::${method.name}:" - ) - appendLine(" Matched normal: $numMatchedNormal") - appendLine(" Matched unknown: $numMatchedUnknown") - appendLine(" Mismatched normal: $numMismatchedNormal") - appendLine(" Lost normal: $numLostNormal") - appendLine(" Better than unknown: $numBetterThanUnknown") - } + "Local $local in $method, type: ${ + local.type.toStringLimited() + }, inferred: ${ + inferredType?.toStringLimited() + }, verdict: $verdict" } - totalNumMatchedNormal += numMatchedNormal - totalNumMatchedUnknown += numMatchedUnknown - totalNumMismatchedNormal += numMismatchedNormal - totalNumLostNormal += numLostNormal - totalNumBetterThanUnknown += numBetterThanUnknown } logger.info { buildString { - appendLine("Total local type matching statistics:") - appendLine(" Matched normal: $totalNumMatchedNormal") - appendLine(" Matched unknown: $totalNumMatchedUnknown") - appendLine(" Mismatched normal: $totalNumMismatchedNormal") - appendLine(" Lost normal: $totalNumLostNormal") - appendLine(" Better than unknown: $totalNumBetterThanUnknown") + appendLine( + "Local type matching for ${ + method.signature.enclosingClass.name + }::${method.name}:" + ) + appendLine(" Matched normal: $numMatchedNormal") + appendLine(" Matched unknown: $numMatchedUnknown") + appendLine(" Mismatched normal: $numMismatchedNormal") + appendLine(" Lost normal: $numLostNormal") + appendLine(" Better than unknown: $numBetterThanUnknown") } } + totalNumMatchedNormal += numMatchedNormal + totalNumMatchedUnknown += numMatchedUnknown + totalNumMismatchedNormal += numMismatchedNormal + totalNumLostNormal += numLostNormal + totalNumBetterThanUnknown += numBetterThanUnknown + } - logger.info { "Done analyzing project: $projectName" } + logger.info { + buildString { + appendLine("Total local type matching statistics:") + appendLine(" Matched normal: $totalNumMatchedNormal") + appendLine(" Matched unknown: $totalNumMatchedUnknown") + appendLine(" Mismatched normal: $totalNumMismatchedNormal") + appendLine(" Lost normal: $totalNumLostNormal") + appendLine(" Better than unknown: $totalNumBetterThanUnknown") + } } + + logger.info { "Done analyzing project: $projectName" } } } } diff --git a/usvm-ts-dataflow/src/testFixtures/kotlin/org/usvm/dataflow/ts/TestFactoryDsl.kt b/usvm-ts-dataflow/src/testFixtures/kotlin/org/usvm/dataflow/ts/TestFactoryDsl.kt index a710f1c896..67c084d03d 100644 --- a/usvm-ts-dataflow/src/testFixtures/kotlin/org/usvm/dataflow/ts/TestFactoryDsl.kt +++ b/usvm-ts-dataflow/src/testFixtures/kotlin/org/usvm/dataflow/ts/TestFactoryDsl.kt @@ -1,52 +1,77 @@ package org.usvm.dataflow.ts +import kotlinx.coroutines.ExperimentalCoroutinesApi +import kotlinx.coroutines.channels.Channel import org.junit.jupiter.api.DynamicContainer import org.junit.jupiter.api.DynamicNode import org.junit.jupiter.api.DynamicTest -import org.junit.jupiter.api.function.Executable -import java.util.stream.Stream -private interface TestProvider { - fun test(name: String, test: () -> Unit) -} - -private interface ContainerProvider { - fun container(name: String, init: TestContainerBuilder.() -> Unit) -} +@DslMarker +annotation class TestFactoryDsl -class TestContainerBuilder(var name: String) : TestProvider, ContainerProvider { - private val nodes: MutableList = mutableListOf() +@TestFactoryDsl +abstract class TestNodeBuilder { + private val nodeChannel = Channel<() -> DynamicNode>(Channel.UNLIMITED) - override fun test(name: String, test: () -> Unit) { - nodes += dynamicTest(name, test) + fun test(name: String, test: () -> Unit) { + nodeChannel.trySend { dynamicTest(name, test) } } - override fun container(name: String, init: TestContainerBuilder.() -> Unit) { - nodes += containerBuilder(name, init) + fun container(name: String, init: TestContainerBuilder.() -> Unit) { + nodeChannel.trySend { dynamicContainer(name, init) } } - fun build(): DynamicContainer = DynamicContainer.dynamicContainer(name, nodes) -} + protected fun createNodes(): Iterable = + Iterable { DynamicNodeIterator() } -private fun containerBuilder(name: String, init: TestContainerBuilder.() -> Unit): DynamicContainer = - TestContainerBuilder(name).apply(init).build() + private inner class DynamicNodeIterator : Iterator { + @OptIn(ExperimentalCoroutinesApi::class) + override fun hasNext(): Boolean = !nodeChannel.isEmpty -class TestFactoryBuilder : TestProvider, ContainerProvider { - private val nodes: MutableList = mutableListOf() - - override fun test(name: String, test: () -> Unit) { - nodes += dynamicTest(name, test) + override fun next(): DynamicNode { + val node = nodeChannel.tryReceive().getOrThrow() + return node() + } } +} - override fun container(name: String, init: TestContainerBuilder.() -> Unit) { - nodes += containerBuilder(name, init) +class TestContainerBuilder(var name: String) : TestNodeBuilder() { + fun build(): DynamicContainer { + return DynamicContainer.dynamicContainer(name, createNodes()) } +} - fun build(): Stream = nodes.stream() +class TestFactoryBuilder : TestNodeBuilder() { + fun build(): Iterable { + return createNodes() + } } -fun testFactory(init: TestFactoryBuilder.() -> Unit): Stream = +inline fun testFactory(init: TestFactoryBuilder.() -> Unit): Iterable = TestFactoryBuilder().apply(init).build() private fun dynamicTest(name: String, test: () -> Unit): DynamicTest = - DynamicTest.dynamicTest(name, Executable(test)) + DynamicTest.dynamicTest(name, test) + +private fun dynamicContainer(name: String, init: TestContainerBuilder.() -> Unit): DynamicContainer = + TestContainerBuilder(name).apply(init).build() + +inline fun TestNodeBuilder.testForEach( + data: Iterable, + crossinline nameProvider: (T) -> String = { it.toString() }, + crossinline test: (T) -> Unit, +) { + data.forEach { item -> + test(nameProvider(item)) { test(item) } + } +} + +inline fun TestNodeBuilder.containerForEach( + data: Iterable, + crossinline nameProvider: (T) -> String = { it.toString() }, + crossinline init: TestContainerBuilder.(T) -> Unit, +) { + data.forEach { item -> + container(nameProvider(item)) { init(item) } + } +} diff --git a/usvm-ts/build.gradle.kts b/usvm-ts/build.gradle.kts index 088ddb8710..96de26034a 100644 --- a/usvm-ts/build.gradle.kts +++ b/usvm-ts/build.gradle.kts @@ -25,6 +25,7 @@ dependencies { testImplementation(Libs.mockk) testImplementation(Libs.junit_jupiter_params) testImplementation(Libs.logback) + testImplementation(testFixtures(project(":usvm-ts-dataflow"))) // https://mvnrepository.com/artifact/org.burningwave/core // Use it to export all modules to all diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt index 27a86eb396..7bfb729748 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt @@ -1,75 +1,74 @@ package org.usvm.project +import mu.KotlinLogging import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.ANONYMOUS_CLASS_PREFIX import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME -import org.jacodb.ets.utils.loadEtsProjectFromIR -import org.junit.jupiter.api.condition.EnabledIf +import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.junit.jupiter.api.Tag import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.TsMethodTestRunner import org.usvm.util.getResourcePath -import org.usvm.util.getResourcePathOrNull import kotlin.test.Test -@EnabledIf("projectAvailable") +private val logger = KotlinLogging.logger {} + +@Tag("manual") class RunOnDemoCalcProject : TsMethodTestRunner() { companion object { - private const val PROJECT_PATH = "/projects/Demo_Calc/etsir/entry" - private const val SDK_PATH = "/sdk/ohos/etsir" - - @JvmStatic - private fun projectAvailable(): Boolean { - val isProjectPresent = getResourcePathOrNull(PROJECT_PATH) != null - val isSdkPreset = getResourcePathOrNull(SDK_PATH) != null - return isProjectPresent && isSdkPreset - } + private const val PROJECT_PATH = "/projects/Demo_Calc/source/entry" + private const val SDK_OHOS_PATH = "/sdk/ohos/5.0.1.111/ets" } override val scene: EtsScene = run { - val projectPath = getResourcePath(PROJECT_PATH) - val sdkPath = getResourcePathOrNull(SDK_PATH) - ?: error( - "Could not load SDK from resources '$SDK_PATH'. " + - "Try running './gradlew generateSdkIR' to generate it." - ) - loadEtsProjectFromIR(projectPath, sdkPath) + val project = loadEtsProjectAutoConvert(getResourcePath(PROJECT_PATH)) + val sdkFiles = listOf(SDK_OHOS_PATH).flatMap { sdk -> + val sdkPath = getResourcePath(sdk) + val sdkProject = loadEtsProjectAutoConvert(sdkPath, useArkAnalyzerTypeInference = null) + sdkProject.projectFiles + } + EtsScene(project.projectFiles, sdkFiles, projectName = project.projectName) } @Test - fun `test run on each method`() { + fun `test run on each class`() { val exceptions = mutableListOf() - val classes = scene.projectClasses.filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) } + val classes = scene.projectClasses + .filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) } println("Total classes: ${classes.size}") - classes - .forEach { cls -> - val methods = cls.methods - .filterNot { it.cfg.stmts.isEmpty() } - .filterNot { it.isStatic } - .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) } - .filterNot { it.name == "build" } - .filterNot { it.name == INSTANCE_INIT_METHOD_NAME } - .filterNot { it.name == STATIC_INIT_METHOD_NAME } - .filterNot { it.name == CONSTRUCTOR_NAME } - - if (methods.isEmpty()) return@forEach - - runCatching { - val tsOptions = TsOptions() - TsMachine(scene, options, tsOptions).use { machine -> - val states = machine.analyze(methods) - states.let {} - } - }.onFailure { - exceptions += it + for (cls in classes) { + logger.info { + "Analyzing class ${cls.name} with ${cls.methods.size} methods" + } + + val methods = cls.methods + .filterNot { it.cfg.stmts.isEmpty() } + .filterNot { it.isStatic } + .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) } + .filterNot { it.name == "build" } + .filterNot { it.name == INSTANCE_INIT_METHOD_NAME } + .filterNot { it.name == STATIC_INIT_METHOD_NAME } + .filterNot { it.name == CONSTRUCTOR_NAME } + + if (methods.isEmpty()) continue + + runCatching { + val tsOptions = TsOptions() + TsMachine(scene, options, tsOptions).use { machine -> + val states = machine.analyze(methods) + states.let {} } + }.onFailure { + exceptions += it } + } val exc = exceptions.groupBy { it } println("Total exceptions: ${exc.size}") diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt index a85aeed078..a8df42eb06 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt @@ -8,6 +8,7 @@ import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.junit.jupiter.api.Tag import org.junit.jupiter.api.condition.EnabledIf import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions @@ -18,29 +19,22 @@ import kotlin.test.Test private val logger = KotlinLogging.logger {} -@EnabledIf("projectAvailable") +@Tag("manual") class RunOnDemoPhotosProject : TsMethodTestRunner() { companion object { private const val PROJECT_PATH = "/projects/Demo_Photos/source/entry" - private const val SDK_PATH = "/sdk/ohos/etsir" - - @JvmStatic - private fun projectAvailable(): Boolean { - val isProjectPresent = getResourcePathOrNull(PROJECT_PATH) != null - val isSdkPreset = getResourcePathOrNull(SDK_PATH) != null - return isProjectPresent && isSdkPreset - } + private const val SDK_OHOS_PATH = "/sdk/ohos/5.0.1.111/ets" } override val scene: EtsScene = run { - val projectPath = getResourcePath(PROJECT_PATH) - val sdkPath = getResourcePathOrNull(SDK_PATH) - ?: error( - "Could not load SDK from resources '$SDK_PATH'. " + - "Try running './gradlew generateSdkIR' to generate it." - ) - loadEtsProjectAutoConvert(projectPath, sdkPath) + val project = loadEtsProjectAutoConvert(getResourcePath(PROJECT_PATH)) + val sdkFiles = listOf(SDK_OHOS_PATH).flatMap { sdk -> + val sdkPath = getResourcePath(sdk) + val sdkProject = loadEtsProjectAutoConvert(sdkPath, useArkAnalyzerTypeInference = null) + sdkProject.projectFiles + } + EtsScene(project.projectFiles, sdkFiles, projectName = project.projectName) } @Test @@ -112,8 +106,9 @@ class RunOnDemoPhotosProject : TsMethodTestRunner() { @Test fun `test on particular method`() { val method = scene.projectClasses + .filter { it.toString() == "@entry/utils/ResourceUtils: %dflt" } .flatMap { it.methods } - .single { it.name == "onCreate" && it.enclosingClass?.name == "EntryAbility" } + .single { it.name == "getResourceString" && it.enclosingClass?.name == "%dflt" } val tsOptions = TsOptions() TsMachine(scene, options, tsOptions).use { machine -> diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/ProjectRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/project/ProjectRunner.kt new file mode 100644 index 0000000000..da081d6fcb --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/project/ProjectRunner.kt @@ -0,0 +1,217 @@ +package org.usvm.project + +import mu.KotlinLogging +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.ANONYMOUS_CLASS_PREFIX +import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME +import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME +import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.junit.jupiter.api.Tag +import org.junit.jupiter.api.TestFactory +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.dataflow.ts.TestNodeBuilder +import org.usvm.dataflow.ts.containerForEach +import org.usvm.dataflow.ts.testFactory +import org.usvm.dataflow.ts.testForEach +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.getResourcePath +import kotlin.io.path.isDirectory +import kotlin.io.path.listDirectoryEntries +import kotlin.io.path.name +import kotlin.test.assertTrue +import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds + +private val logger = KotlinLogging.logger {} + +@Tag("manual") +class ProjectRunner { + companion object { + private const val PROJECTS_ROOT = "/projects" + private const val SDK_OHOS_PATH = "/sdk/ohos/5.0.1.111/ets" + + // Instructions for getting SDK: + // + // 1. Visit https://repo.huaweicloud.com/harmonyos/os/ + // + // 2. Download the latest version (e.g., `5.0.3`): + // ```sh + // curl -OL https://repo.huaweicloud.com/openharmony/os/5.0.3-Release/ohos-sdk-windows_linux-public.tar.gz + // ``` + // + // 3. Extract the archive and find the folder `ets` with sub-folders `api`, `arkts`, `component`, `kits`. + // Everything else can be thrown away. + // + // 4. Place the SDK into resources as follows: + // ``` + // src/ + // test/ + // resources/ + // sdk/ + // ohos/ + // / (e.g., `5.0.1.111`) + // ets/ + // api/ + // arkts/ + // component/ + // kits/ + // ``` + // + // 5. Update the `SDK_OHOS_PATH` const to point to the correct version. + + val machineOptions: UMachineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM), + timeout = 10.seconds, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, // we do not need the timeout for a solver in tests + typeOperationsTimeout = Duration.INFINITE, // we do not need the timeout for type operations in tests + ) + } + + private val sdkFiles: List by lazy { + listOf(SDK_OHOS_PATH).flatMap { sdk -> + logger.info { "Loading SDK from path: $sdk" } + val sdkPath = getResourcePath(sdk) + val sdkProject = loadEtsProjectAutoConvert(sdkPath, useArkAnalyzerTypeInference = null) + sdkProject.projectFiles + }.also { + logger.info { "Loaded total ${it.size} SDK files" } + } + } + + private fun createScene(projectName: String): EtsScene { + logger.info { "Creating scene for project: $projectName" } + val projectPath = "$PROJECTS_ROOT/$projectName/source" + logger.info { "Loading project from path: $projectPath" } + val project = loadEtsProjectAutoConvert(getResourcePath(projectPath)) + logger.info { "Loaded project $projectName with ${project.projectFiles.size} files" } + return EtsScene(project.projectFiles, sdkFiles, projectName = projectName) + } + + private fun runMachineOnClass(scene: EtsScene, cls: EtsClass) { + logger.info { "Running on class $cls in project ${scene.projectName}" } + val methods = cls.methods + .filterNot { it.cfg.stmts.isEmpty() } + .filterNot { it.isStatic } + .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) } + .filterNot { it.name == "build" } + .filterNot { it.name == INSTANCE_INIT_METHOD_NAME } + .filterNot { it.name == STATIC_INIT_METHOD_NAME } + .filterNot { it.name == CONSTRUCTOR_NAME } + if (methods.isEmpty()) return + logger.info { "Running on ${methods.size} methods in class $cls" } + + val tsOptions = TsOptions() + TsMachine(scene, machineOptions, tsOptions).use { machine -> + val states = machine.analyze(methods) + states.let {} + } + } + + private fun TestNodeBuilder.testOnEachClass(scene: EtsScene) { + container("Run on each class in ${scene.projectName}") { + logger.info { "Running on each class in project ${scene.projectName}" } + val classes = scene.projectClasses + .filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) } + logger.info { "Running on ${classes.size} classes in project ${scene.projectName}" } + + val exceptions = mutableListOf() + + testForEach( + classes, // .take(3) + { "Run on class ${it.name} @${it.signature.file.fileName}" } + ) { cls -> + try { + runMachineOnClass(scene, cls) + } catch (e: Throwable) { + exceptions += e + } + } + + test("@afterAll") { + val exc = exceptions.groupBy { it } + logger.info { "Total exceptions: ${exc.size}" } + for (es in exc.values.sortedBy { it.size }.asReversed()) { + logger.info { "${es.first()}" } + } + assertTrue(exc.isEmpty(), "There are exceptions!") + } + } + } + + private fun runMachineOnAllMethods(scene: EtsScene) { + logger.info { "Running on all methods in project ${scene.projectName}" } + val methods = scene.projectClasses + .filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) } + .flatMap { cls -> + cls.methods + .filterNot { it.cfg.stmts.isEmpty() } + .filterNot { it.isStatic } + .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) } + .filterNot { it.name == "build" } + } + logger.info { "Running on ${methods.size} methods in project ${scene.projectName}" } + + val tsOptions = TsOptions() + TsMachine(scene, machineOptions, tsOptions).use { machine -> + val states = machine.analyze(methods) + states.let {} + } + } + + private fun TestNodeBuilder.testOnAllMethods(scene: EtsScene) { + test("Run on all methods in ${scene.projectName}") { + runMachineOnAllMethods(scene) + } + } + + @TestFactory + fun dynamicTestsForAllProjects() = testFactory { + val projects = getResourcePath(PROJECTS_ROOT) + .listDirectoryEntries() + .filter { it.isDirectory() } + .map { it.name } + logger.info { "Found ${projects.size} projects: ${projects.joinToString(", ")}" } + + containerForEach( + projects.take(3), + { "Project $it" } + ) { projectName -> + logger.info { "Processing project: $projectName" } + val scene = createScene(projectName) + + testOnEachClass(scene) + + testOnAllMethods(scene) + } + } + + private val particularProjectName: String = run { + // "Demo_Calc" + "Demo_Photos" + } + + @TestFactory + fun `run on each class in particular project`() = testFactory { + logger.info { "Processing project: $particularProjectName" } + val scene = createScene(particularProjectName) + + testOnEachClass(scene) + } + + @TestFactory + fun `run on all methods in particular project`() = testFactory { + logger.info { "Processing project: $particularProjectName" } + val scene = createScene(particularProjectName) + + testOnAllMethods(scene) + } +}