From 554d6b6b8f727163f23d26f17bedef42a74f48a7 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 22:48:07 +0300 Subject: [PATCH] Preflight original class retention before experiment treatments --- .../ts/pbt/cli/CampaignFrontendPreflight.kt | 109 ++++++++++++++++++ .../org/usvm/ts/pbt/cli/FastCheckCli.kt | 8 +- .../pbt/cli/CampaignFrontendPreflightTest.kt | 60 ++++++++++ 3 files changed, 173 insertions(+), 4 deletions(-) create mode 100644 usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignFrontendPreflight.kt create mode 100644 usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignFrontendPreflightTest.kt diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignFrontendPreflight.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignFrontendPreflight.kt new file mode 100644 index 0000000000..fc9c8b93fb --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignFrontendPreflight.kt @@ -0,0 +1,109 @@ +package org.usvm.ts.pbt.cli + +import kotlinx.serialization.Serializable +import kotlinx.serialization.json.decodeFromJsonElement +import kotlinx.serialization.json.jsonObject +import kotlinx.serialization.json.jsonPrimitive +import org.jacodb.ets.model.EtsClassCategory +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.generateEtsIR +import org.jacodb.ets.utils.loadEtsProjectFromIR +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.encodeToUtf8SafeString +import org.usvm.ts.pbt.usvm.UsvmProjectionCapabilityResolver +import org.usvm.ts.pbt.usvm.UsvmProjectionOptions +import java.io.IOException +import java.nio.file.Files +import java.nio.file.Path +import kotlin.time.Duration.Companion.seconds + +/** Inspects the unchanged experiment source before any treatment can influence eligibility. */ +internal object CampaignFrontendPreflight { + @Serializable + data class Result( + val supported: Boolean, + val classDeclarations: Int = 0, + val classStatements: Int = 0, + val predicateMapping: String? = null, + val preconditionMapping: String? = null, + val symbolicLevel: ProjectionLevel? = null, + val diagnostics: List = emptyList(), + ) + + fun run(args: Array, errors: Appendable = System.err): Int { + require(args.size == 2) { "campaign-preflight requires a case JSON and a result destination" } + val requestFile = Path.of(args[0]).toRealPath() + val request = PropertyManifestJson.json.parseToJsonElement(Files.readString(requestFile)).jsonObject + val root = requestFile.parent.resolve(request.getValue("sourceRoot").jsonPrimitive.content).toRealPath() + val classSource = request.getValue("classSource").jsonPrimitive.content + val className = request.getValue("className").jsonPrimitive.content + val property = PropertyManifestJson.json.decodeFromJsonElement(request.getValue("property")) + val result = try { + inspect(root, classSource, className, property) + } catch (error: IOException) { + Result(supported = false, diagnostics = listOf(error.message.orEmpty())) + } catch (error: IllegalArgumentException) { + Result(supported = false, diagnostics = listOf(error.message.orEmpty())) + } catch (error: IllegalStateException) { + Result(supported = false, diagnostics = listOf(error.message.orEmpty())) + } + + Files.writeString(Path.of(args[1]), PropertyManifestJson.json.encodeToUtf8SafeString(result)) + if (!result.supported) errors.appendLine(result.diagnostics.joinToString()) + return if (result.supported) 0 else 2 + } + + private fun inspect(root: Path, classSource: String, className: String, property: PropertyDefinition): Result { + val generated = generateEtsIR( + keepPartialOutputOnFailure = false, + projectPath = root, + isProject = true, + loadEntrypoints = false, + useArkAnalyzerTypeInference = 1, + timeout = 30.seconds, + provider = EtsIrProvider.TS_FRONTEND, + ) + val scene = try { + loadEtsProjectFromIR(projectFilesPath = generated, sdkFilesPath = null) + } finally { + generated.toFile().deleteRecursively() + } + val expectedFile = root.resolve(classSource).normalize().toRealPath() + val classes = scene.projectClasses.filter { owner -> + val source = root.resolve(owner.signature.file.fileName).normalize() + owner.name == className && owner.category == EtsClassCategory.CLASS && source == expectedFile + } + val statements = classes.sumOf { owner -> owner.methods.sumOf { it.cfg.stmts.size } } + val manifest = property.toManifest() + val mapping = PropertyEtsMapper(scene = scene, sourceRoots = listOf(root)).map(manifest) + val capability = UsvmProjectionCapabilityResolver(scene).resolve( + manifest = manifest, + mapping = mapping, + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + options = UsvmProjectionOptions(), + ) + val exactProperty = mapping.predicate.status == EtsMappingStatus.EXACT && + (mapping.precondition == null || mapping.precondition?.status == EtsMappingStatus.EXACT) + val diagnostics = capability.symbolic.diagnostics.map { it.message }.toMutableList() + if (classes.size != 1 || statements == 0) { + diagnostics += "The original class has ${classes.size} IR declarations and " + + "$statements executable IR statements" + } + return Result( + supported = classes.size == 1 && statements > 0 && exactProperty && + capability.symbolic.level != ProjectionLevel.UNSUPPORTED, + classDeclarations = classes.size, + classStatements = statements, + predicateMapping = mapping.predicate.status.name, + preconditionMapping = mapping.precondition?.status?.name, + symbolicLevel = capability.symbolic.level, + diagnostics = diagnostics, + ) + } +} diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt index cc350566f1..71280b2efe 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt @@ -337,10 +337,10 @@ class FastCheckCli( /** Process entry point used by Gradle application and installed distributions. */ fun main(args: Array) { - val exitCode = if (args.firstOrNull() == "campaign-file") { - runCampaignFile(args.drop(1).toTypedArray()) - } else { - FastCheckCli().run(args) + val exitCode = when (args.firstOrNull()) { + "campaign-file" -> runCampaignFile(args.drop(1).toTypedArray()) + "campaign-preflight" -> CampaignFrontendPreflight.run(args.drop(1).toTypedArray()) + else -> FastCheckCli().run(args) } exitProcess(exitCode) } diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignFrontendPreflightTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignFrontendPreflightTest.kt new file mode 100644 index 0000000000..03d9870791 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignFrontendPreflightTest.kt @@ -0,0 +1,60 @@ +package org.usvm.ts.pbt.cli + +import kotlinx.serialization.json.encodeToJsonElement +import kotlinx.serialization.json.jsonObject +import kotlinx.serialization.json.jsonPrimitive +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcesRoot +import java.nio.file.Files +import java.nio.file.Path +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class CampaignFrontendPreflightTest { + @TempDir + lateinit var directory: Path + + @Test + fun `preflight distinguishes a retained executable class from a missing class without changing source`() { + val root = testResourcesRoot().resolve("properties/campaign") + val source = root.resolve("CompletedSubject.ts") + val original = Files.readString(source) + val property = PropertyDefinition( + id = PropertyId(value = "preflight.healthy"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = -100, max = 100))), + predicate = TypeScriptEntryPoint(module = "CompletedProperties.ts", exportName = "healthy"), + ) + val propertyJson = PropertyManifestJson.json.encodeToJsonElement(property) + val rootJson = PropertyManifestJson.json.encodeToJsonElement(root.toString()) + val request = directory.resolve("case.json") + val destination = directory.resolve("preflight.json") + + for ((className, expectedExit) in listOf("BranchingCounter" to 0, "MissingClass" to 2)) { + Files.writeString( + request, + """{"sourceRoot":$rootJson,"classSource":"CompletedSubject.ts","className":"$className", + "property":$propertyJson} """, + ) + + val exit = CampaignFrontendPreflight.run( + args = arrayOf(request.toString(), destination.toString()), + errors = StringBuilder(), + ) + val result = PropertyManifestJson.json.parseToJsonElement(Files.readString(destination)).jsonObject + + assertEquals(expectedExit, exit) + assertEquals(expectedExit == 0, result.getValue("supported").jsonPrimitive.content.toBooleanStrict()) + assertEquals(original, Files.readString(source)) + if (expectedExit == 0) { + assertTrue(result.getValue("classStatements").jsonPrimitive.content.toInt() > 0) + } + } + } +}