From b29e7d07edb12d12b4dfd511efbb6d2cf1e3d5a0 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 15 Oct 2026 23:26:15 +0300 Subject: [PATCH 1/3] [TS] Make string models cheaper for symbolic execution (#525) --- .../intrinsic/TsStringEtsIrModelFamily.kt | 104 ++++++++- .../machine/expr/StringCodeUnitConversion.kt | 20 +- .../org/usvm/machine/expr/TsExprResolver.kt | 5 +- .../kotlin/org/usvm/util/StringStorage.kt | 28 +++ .../usvm/machine/call/models/StringModels.ts | 94 +++++---- .../call/TsPrimitiveOwnerBoundaryTest.kt | 6 + .../call/TsSymbolicStringModelsTest.kt | 197 ++++++++++++++++++ .../call/TsUnknownCallModelCatalogTest.kt | 2 + .../models/ForeignPrimitiveHelpers.ts | 10 + .../resources/models/SymbolicStringModels.ts | 53 +++++ 10 files changed, 461 insertions(+), 58 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSymbolicStringModelsTest.kt create mode 100644 usvm-ts/src/test/resources/models/SymbolicStringModels.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt index 03cffaef8d..825a59432d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt @@ -19,12 +19,15 @@ import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact import org.usvm.machine.call.resolvedInstanceInputs import org.usvm.machine.expr.mkEcmaScriptToUint32 +import org.usvm.machine.expr.mkEcmaScriptWhitespace import org.usvm.machine.state.TsState import org.usvm.sizeSort +import org.usvm.util.copyStringRange import org.usvm.util.mkStringBackingElementLValue import org.usvm.util.mkStringBackingLValue import org.usvm.util.mkStringBackingLengthLValue import org.usvm.util.stringFromCodeUnit +import org.usvm.util.stringLength /** Built-in String algorithms implemented by ordinary TypeScript bodies. */ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { @@ -359,6 +362,16 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { arity = 1, implementation = ::stringFromCodeUnit, ), + primitiveModel( + methodName = "isWhitespace", + arity = 1, + implementation = ::stringIsWhitespace, + ), + primitiveModel( + methodName = "copyNormalizedRange", + arity = 3, + implementation = ::stringCopyNormalizedRange, + ), ) } @@ -382,20 +395,25 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { add("ts.array.primitive.allocateStrings") add("ts.array.primitive.truncateDense") } - val convertsCase = methodName in setOf("toUpperCase", "toLowerCase") - if (convertsCase) { + if (methodName != "charAt" && methodName != "slice" && methodName != "substring") { add(PRIMITIVE_CODE_UNIT_AT_ID) + } + if (methodName in setOf("toUpperCase", "toLowerCase", "replaceAll")) { add(PRIMITIVE_FROM_CODE_UNIT_ID) - } else { - add(MATH_FLOOR_MODEL_ID) - if (methodName == "charCodeAt") { - add(PRIMITIVE_CODE_UNIT_AT_ID) - } } - if (methodName in setOf("trim", "trimStart", "trimEnd", "replaceAll")) { - add(PRIMITIVE_CODE_UNIT_AT_ID) + if (methodName in setOf("trim", "trimStart", "trimEnd")) { + add(PRIMITIVE_IS_WHITESPACE_ID) + } + if (methodName in setOf("slice", "substring", "split", "trim", "trimStart", "trimEnd", "replaceAll")) { + add(PRIMITIVE_COPY_NORMALIZED_RANGE_ID) + } + val normalizesPosition = methodName in setOf( + "charAt", "charCodeAt", "indexOf", "includes", "slice", "substring", + "startsWith", "endsWith", "lastIndexOf", + ) + if (normalizesPosition) { + add(MATH_FLOOR_MODEL_ID) } - if (methodName == "replaceAll") add(PRIMITIVE_FROM_CODE_UNIT_ID) }, ) @@ -499,6 +517,70 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } + private fun stringIsWhitespace( + state: TsState, + inputs: List>, + ): TsUnknownCallModelExecution? = with(state.ctx) { + val code = inputs.singleOrNull()?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null + // The owning source models pass only values read from their UTF-16 backing. + val codeUnit = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = code, + bvSize = bv16Sort.sizeBits.toInt(), + isSigned = false, + ).asExpr(bv16Sort) + + singleSuccessor(state = state, guard = trueExpr, result = mkEcmaScriptWhitespace(codeUnit)) + } + + private fun stringCopyNormalizedRange( + state: TsState, + inputs: List>, + ): TsUnknownCallModelExecution? = with(state.ctx) { + val receiver = inputs.getOrNull(0)?.takeIf { it.sort == addressSort }?.asExpr(addressSort) ?: return null + val fpFrom = inputs.getOrNull(1)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null + val fpTo = inputs.getOrNull(2)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null + val hasBacking = receiver in state.boundedStringBackingRefs && !receiver.hasFakeValueBranch() + if (!hasBacking) return null + + val startIndex = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = fpFrom, + bvSize = sizeSort.sizeBits.toInt(), + isSigned = true, + ).asExpr(sizeSort) + val endIndex = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = fpTo, + bvSize = sizeSort.sizeBits.toInt(), + isSigned = true, + ).asExpr(sizeSort) + val integralBounds = listOf(fpFrom to startIndex, fpTo to endIndex).map { (number, index) -> + val converted = mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = index.cast(), + signed = true, + ) + mkFpEqualExpr(number, converted) + } + val receiverIsString = state.memory.types.evalTypeEquals(receiver, EtsStringType) + val boundsAreIntegral = mkAnd(integralBounds) + val nonNegativeStart = mkBvSignedGreaterOrEqualExpr(startIndex, mkBv(0)) + val orderedBounds = mkBvSignedLessOrEqualExpr(startIndex, endIndex) + val receiverLength = state.stringLength(receiver) + val endWithinLength = mkBvSignedLessOrEqualExpr(endIndex, receiverLength) + val guard = mkAnd(receiverIsString, boundsAreIntegral, nonNegativeStart, orderedBounds, endWithinLength) + val successor = TsUnknownCallModelSuccessor( + guard = guard, + completion = TsUnknownCallModelCompletion.Normal { + copyStringRange(receiver = receiver, from = startIndex, to = endIndex) + }, + ) + + TsUnknownCallModelExecution(successors = listOf(successor), residualGuard = mkNot(guard)) + } + private fun singleSuccessor( state: TsState, guard: org.usvm.UBoolExpr, @@ -517,6 +599,8 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { private const val PRIMITIVE_CODE_UNIT_AT_ID = "ts.string.primitive.codeUnitAt" private const val PRIMITIVE_FROM_CODE_UNIT_ID = "ts.string.primitive.fromCodeUnit" + private const val PRIMITIVE_IS_WHITESPACE_ID = "ts.string.primitive.isWhitespace" + private const val PRIMITIVE_COPY_NORMALIZED_RANGE_ID = "ts.string.primitive.copyNormalizedRange" private const val MATH_FLOOR_MODEL_ID = "ts.math.floor" private const val MAX_ASCII_CASE_LENGTH = 16 private const val ASCII_MAX_CODE_UNIT = 0x7f diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringCodeUnitConversion.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringCodeUnitConversion.kt index 7705f4b459..0761bd4694 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringCodeUnitConversion.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringCodeUnitConversion.kt @@ -1,7 +1,9 @@ package org.usvm.machine.expr +import io.ksmt.sort.KBv16Sort import io.ksmt.sort.KFp64Sort import io.ksmt.utils.cast +import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.machine.TsContext @@ -10,11 +12,20 @@ import org.usvm.util.mkStringBackingElementLValue import org.usvm.util.stringCharacters import org.usvm.util.stringLength -private val singleCodeUnitWhitespace = listOf( +private val ecmaScriptWhitespace = listOf( '\t', '\n', '\u000b', '\u000c', '\r', ' ', '\u00a0', '\u1680', '\u2028', '\u2029', '\u202f', '\u205f', '\u3000', '\ufeff', ) + ('\u2000'..'\u200a') +/** ECMAScript WhiteSpace and LineTerminator, kept as one predicate rather than execution branches. */ +internal fun TsContext.mkEcmaScriptWhitespace(codeUnit: UExpr): UBoolExpr { + val matches = ecmaScriptWhitespace.map { character -> + mkEq(codeUnit, mkBv(character.code, bv16Sort)) + } + + return mkOr(matches) +} + /** ToNumber for the zero- or one-code-unit Strings produced by indexing and charAt. */ internal fun TsContext.singleCodeUnitToNumber(scope: TsStepScope, string: UHeapRef): UExpr? { val lengthBound = scope.calcOnState { boundedStringBackingRefs[string] } ?: return null @@ -41,12 +52,7 @@ internal fun TsContext.singleCodeUnitToNumber(scope: TsStepScope, string: UHeapR value = digit.cast(), signed = false, ) - val whitespaceGuards = singleCodeUnitWhitespace.map { character -> - val whitespace = mkBv(character.code, bv16Sort) - - mkEq(codeUnit, whitespace) - } - val isWhitespace = mkOr(whitespaceGuards) + val isWhitespace = mkEcmaScriptWhitespace(codeUnit) val zero = mkFp64(0.0) val nonDigitNumber = mkIte(isWhitespace, zero, mkFp64NaN()) val nonEmptyNumber = mkIte(isDigit, digitNumber, nonDigitNumber) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 0c6f005906..9c7d7f35ea 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -828,7 +828,10 @@ class TsExprResolver( guard = trueExpr, ) memory.write(mkStringBackingLengthLValue(resultChars), resultLength, guard = trueExpr) - boundedStringBackingRefs += result to options.maxArraySize + val leftBound = boundedStringBackingRefs.getValue(left) + val rightBound = boundedStringBackingRefs.getValue(right) + val resultBound = minOf(options.maxArraySize.toLong(), leftBound.toLong() + rightBound) + boundedStringBackingRefs += result to resultBound.toInt() memory.memcpy( srcRef = leftChars, diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt index 69003e86b9..0e702b0f15 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt @@ -1,5 +1,6 @@ package org.usvm.util +import io.ksmt.expr.KBitVec32Value import io.ksmt.sort.KBv16Sort import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr @@ -10,6 +11,7 @@ import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.api.initializeArrayLength +import org.usvm.api.memcpy import org.usvm.machine.TsSizeSort import org.usvm.machine.state.TsState import org.usvm.sizeSort @@ -47,6 +49,32 @@ private fun TsState.allocateString( string to characters } +/** Copies an already validated range: 0 <= from <= to <= receiver.length. */ +internal fun TsState.copyStringRange( + receiver: UHeapRef, + from: UExpr, + to: UExpr, +): UConcreteHeapRef = with(ctx) { + val length = mkBvSubExpr(to, from) + val receiverBound = boundedStringBackingRefs.getValue(receiver) + val constantLength = (length as? KBitVec32Value)?.intValue + val resultBound = minOf(receiverBound, constantLength ?: receiverBound) + val sourceCharacters = stringCharacters(receiver) + val (result, characters) = allocateString(length = length, maxLength = resultBound) + + memory.memcpy( + srcRef = sourceCharacters, + dstRef = characters, + type = stringBackingArrayDescriptor, + elementSort = bv16Sort, + fromSrc = from, + fromDst = mkBv(0), + length = length, + ) + + result +} + internal fun TsState.stringFromCodeUnit(codeUnit: UExpr): UConcreteHeapRef = with(ctx) { val value = mkFpToBvExpr( roundingMode = fpRoundingModeSortDefaultValue(), diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts index 2e7c6a05c1..f364396024 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts @@ -1,6 +1,9 @@ declare class StringModelPrimitives { static codeUnitAt(receiver: string, index: number): number; static fromCodeUnit(codeUnit: number): string; + static isWhitespace(codeUnit: number): boolean; + // Bounds have already been normalized: 0 <= from <= to <= receiver.length. + static copyNormalizedRange(receiver: string, from: number, to: number): string; } declare class ArrayModelPrimitives { @@ -33,13 +36,15 @@ export class StringModels { let position = 0; while (position + separatorLength <= length) { let offset = 0; - while (offset < separatorLength && - receiver[position + offset] === - separator[offset]) { + while (offset < separatorLength) { + const actual = StringModelPrimitives.codeUnitAt(receiver, position + offset); + const expected = StringModelPrimitives.codeUnitAt(separator, offset); + if (actual !== expected) break; + offset++; } if (offset === separatorLength) { - result[count] = StringModels.slice(receiver, start, position); + result[count] = StringModelPrimitives.copyNormalizedRange(receiver, start, position); count++; if (count === limit) return ArrayModelPrimitives.truncateDense(result, count); position += separatorLength; @@ -48,7 +53,7 @@ export class StringModels { position++; } } - result[count] = StringModels.slice(receiver, start, length); + result[count] = StringModelPrimitives.copyNormalizedRange(receiver, start, length); return ArrayModelPrimitives.truncateDense(result, count + 1); } @@ -75,8 +80,8 @@ export class StringModels { while (index + searchLength <= length) { let searchIndex = 0; while (searchIndex < searchLength) { - const character = receiver[index + searchIndex]; - const expectedCharacter = searchString[searchIndex]; + const character = StringModelPrimitives.codeUnitAt(receiver, index + searchIndex); + const expectedCharacter = StringModelPrimitives.codeUnitAt(searchString, searchIndex); const matches = character === expectedCharacter; if (!matches) { break; @@ -114,14 +119,11 @@ export class StringModels { const from = StringModels.normalizeSliceIndex(start, length); const to = StringModels.normalizeSliceIndex(end, length); - let result = ""; - let index = from; - while (index < to) { - result += receiver[index]; - index++; + if (to <= from) { + return ""; } - return result; + return StringModelPrimitives.copyNormalizedRange(receiver, from, to); } static substring(receiver: string, start: number, end: number): string { @@ -129,38 +131,58 @@ export class StringModels { const from = StringModels.normalizePosition(start, length); const to = StringModels.normalizePosition(end, length); return from <= to - ? StringModels.slice(receiver, from, to) - : StringModels.slice(receiver, to, from); + ? StringModelPrimitives.copyNormalizedRange(receiver, from, to) + : StringModelPrimitives.copyNormalizedRange(receiver, to, from); } static trim(receiver: string): string { const length = receiver.length; let start = 0; let end = length; - while (start < end && StringModels.isWhitespace(StringModelPrimitives.codeUnitAt(receiver, start))) { + while (start < end) { + const codeUnit = StringModelPrimitives.codeUnitAt(receiver, start); + const whitespace = StringModelPrimitives.isWhitespace(codeUnit); + if (!whitespace) break; + start++; } - while (end > start && StringModels.isWhitespace(StringModelPrimitives.codeUnitAt(receiver, end - 1))) { + + while (end > start) { + const codeUnit = StringModelPrimitives.codeUnitAt(receiver, end - 1); + const whitespace = StringModelPrimitives.isWhitespace(codeUnit); + if (!whitespace) break; + end--; } - return StringModels.slice(receiver, start, end); + + return StringModelPrimitives.copyNormalizedRange(receiver, start, end); } static trimStart(receiver: string): string { const length = receiver.length; let start = 0; - while (start < length && StringModels.isWhitespace(StringModelPrimitives.codeUnitAt(receiver, start))) { + while (start < length) { + const codeUnit = StringModelPrimitives.codeUnitAt(receiver, start); + const whitespace = StringModelPrimitives.isWhitespace(codeUnit); + if (!whitespace) break; + start++; } - return StringModels.slice(receiver, start, length); + + return StringModelPrimitives.copyNormalizedRange(receiver, start, length); } static trimEnd(receiver: string): string { let end = receiver.length; - while (end > 0 && StringModels.isWhitespace(StringModelPrimitives.codeUnitAt(receiver, end - 1))) { + while (end > 0) { + const codeUnit = StringModelPrimitives.codeUnitAt(receiver, end - 1); + const whitespace = StringModelPrimitives.isWhitespace(codeUnit); + if (!whitespace) break; + end--; } - return StringModels.slice(receiver, 0, end); + + return StringModelPrimitives.copyNormalizedRange(receiver, 0, end); } static replaceAll(receiver: string, search: string, replacement: string): string { @@ -177,7 +199,7 @@ export class StringModels { offset++; } if (offset === searchLength) { - result += StringModels.slice(receiver, endOfLastMatch, position); + result += StringModelPrimitives.copyNormalizedRange(receiver, endOfLastMatch, position); result += StringModels.substitution(receiver, search, replacement, position); endOfLastMatch = position + searchLength; position = endOfLastMatch + (searchLength === 0 ? 1 : 0); @@ -185,7 +207,7 @@ export class StringModels { position++; } } - return result + StringModels.slice(receiver, endOfLastMatch, length); + return result + StringModelPrimitives.copyNormalizedRange(receiver, endOfLastMatch, length); } private static substitution(receiver: string, search: string, replacement: string, position: number): string { @@ -207,13 +229,13 @@ export class StringModels { continue; } if (next === 96) { - result += StringModels.slice(receiver, 0, position); + result += StringModelPrimitives.copyNormalizedRange(receiver, 0, position); index += 2; continue; } if (next === 39) { const matchEnd = position + search.length; - result += StringModels.slice(receiver, matchEnd, receiver.length); + result += StringModelPrimitives.copyNormalizedRange(receiver, matchEnd, receiver.length); index += 2; continue; } @@ -224,14 +246,6 @@ export class StringModels { return result; } - private static isWhitespace(codeUnit: number): boolean { - return (codeUnit >= 0x09 && codeUnit <= 0x0d) - || codeUnit === 0x20 || codeUnit === 0xa0 || codeUnit === 0x1680 - || (codeUnit >= 0x2000 && codeUnit <= 0x200a) - || codeUnit === 0x2028 || codeUnit === 0x2029 || codeUnit === 0x202f - || codeUnit === 0x205f || codeUnit === 0x3000 || codeUnit === 0xfeff; - } - static toUpperCase(receiver: string): string { const length = receiver.length; let result = ""; @@ -272,8 +286,8 @@ export class StringModels { let searchIndex = 0; while (searchIndex < searchLength) { - const character = receiver[start + searchIndex]; - const expectedCharacter = searchString[searchIndex]; + const character = StringModelPrimitives.codeUnitAt(receiver, start + searchIndex); + const expectedCharacter = StringModelPrimitives.codeUnitAt(searchString, searchIndex); const matches = character === expectedCharacter; if (!matches) { return false; @@ -296,8 +310,8 @@ export class StringModels { let searchIndex = 0; while (searchIndex < searchLength) { - const character = receiver[start + searchIndex]; - const expectedCharacter = searchString[searchIndex]; + const character = StringModelPrimitives.codeUnitAt(receiver, start + searchIndex); + const expectedCharacter = StringModelPrimitives.codeUnitAt(searchString, searchIndex); const matches = character === expectedCharacter; if (!matches) { return false; @@ -320,8 +334,8 @@ export class StringModels { while (index >= 0) { let searchIndex = 0; while (searchIndex < searchLength) { - const character = receiver[index + searchIndex]; - const expectedCharacter = searchString[searchIndex]; + const character = StringModelPrimitives.codeUnitAt(receiver, index + searchIndex); + const expectedCharacter = StringModelPrimitives.codeUnitAt(searchString, searchIndex); const matches = character === expectedCharacter; if (!matches) { break; diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsPrimitiveOwnerBoundaryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsPrimitiveOwnerBoundaryTest.kt index bf22cda55f..dd75e7400d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsPrimitiveOwnerBoundaryTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsPrimitiveOwnerBoundaryTest.kt @@ -32,6 +32,12 @@ class TsPrimitiveOwnerBoundaryTest { assertForeignHelperResidual("foreignArray") } + @Test + fun `foreign declarations cannot use string predicate or range helpers`() { + assertForeignHelperResidual("foreignWhitespace") + assertForeignHelperResidual("foreignStringRange") + } + private fun assertForeignHelperResidual(methodName: String) { val method = scene.projectClasses.single { it.name == "ForeignPrimitiveHelpers" } .methods diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSymbolicStringModelsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSymbolicStringModelsTest.kt new file mode 100644 index 0000000000..e47a9e7d76 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSymbolicStringModelsTest.kt @@ -0,0 +1,197 @@ +package org.usvm.machine.call + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import org.usvm.util.jsString +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue + +class TsSymbolicStringModelsTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/SymbolicStringModels.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + override val tsOptions = TsOptions(maxArraySize = 4) + override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> + val tests = TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + val analysis = machine.analyzeWithOutcome(methods = listOf(method)) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.isEmpty(), "${method.name}: ${analysis.unsupportedPaths}") + + analysis.states.map { state -> TsTestResolver().resolve(method, state) } + } + + replay(method = method, tests = tests) + tests + } + + init { + options = options.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + } + + @Test + fun `symbolic trim variants preserve the full ECMAScript whitespace set`() { + val whitespaceCharacters = "\t\n\u000b\u000c\r \u00a0\u1680\u2028\u2029\u202f\u205f\u3000\ufeff" + + ('\u2000'..'\u200a').joinToString(separator = "") + val whitespace = whitespaceCharacters.toSet() + val transforms = mapOf String>( + "trim" to { value -> value.trim { it in whitespace } }, + "trimStart" to { value -> value.trimStart { it in whitespace } }, + "trimEnd" to { value -> value.trimEnd { it in whitespace } }, + ) + + for ((name, transform) in transforms) { + discoverProperties( + method = method(name), + { input, result -> input.value.isEmpty() && result.value.isEmpty() }, + { input, result -> input.value.isNotEmpty() && result.value == transform(input.value) }, + invariants = arrayOf({ input, result -> result.value == transform(input.value) }), + ) + } + } + + @Test + fun `symbolic slice and substring normalize numeric bounds and replay UTF16 witnesses`() { + for (name in listOf("slice", "substring")) { + discoverProperties( + method = method(name), + { _, _, _, result -> result.value.isEmpty() }, + { _, _, _, result -> result.value.isNotEmpty() }, + ) + } + } + + @Test + fun `symbolic searches compare UTF16 units and preserve match positions`() { + fun expected(value: String): Double { + val first = value.indexOf('\ud800') + val last = value.lastIndexOf('\ud800') + val included = if ('\ud800' in value) 1 else 0 + val starts = if (value.startsWith('\ud800')) 1 else 0 + val ends = if (value.endsWith('\ud800')) 1 else 0 + + return (first + 10 * last + 100 * included + 1000 * starts + 10_000 * ends).toDouble() + } + + discoverProperties( + method = method("searches"), + { input, result -> '\ud800' !in input.value && result.number == -11.0 }, + { input, result -> '\ud800' in input.value && result.number == expected(input.value) }, + invariants = arrayOf({ input, result -> result.number == expected(input.value) }), + ) + } + + @Test + fun `symbolic split and substitution preserve copied ranges and lone surrogates`() { + val transforms = mapOf String>( + "split" to { value -> value.split('\u0000').take(3).joinToString(separator = "|") }, + "replaceAll" to { value -> if (value.length > 2) "" else value.replace("\ud800", "\$\ud800") }, + ) + + for ((name, transform) in transforms) { + discoverProperties( + method = method(name), + { input, result -> input.value.isEmpty() && result.value == transform(input.value) }, + { input, result -> input.value.isNotEmpty() && result.value == transform(input.value) }, + invariants = arrayOf({ input, result -> result.value == transform(input.value) }), + ) + } + } + + @Test + fun `single character trim does not enumerate whitespace spellings`() { + val method = method("trimSingle") + + val tests = runner(method, options) + + assertEquals(3, tests.size, "Only wrong length, whitespace, and non-whitespace paths are needed") + assertEquals(setOf(-1.0, 0.0, 1.0), tests.map { assertIs(it.returnValue).number }.toSet()) + } + + @Test + fun `copied ranges and concatenation keep their proven length bounds`() { + val method = method("boundedCopy") + + val tests = TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> + val analysis = machine.analyzeWithOutcome(methods = listOf(method)) + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.isEmpty(), analysis.unsupportedPaths.toString()) + + analysis.states.map { state -> + val test = TsTestResolver().resolve(method, state) + val result = assertIs(test.returnValue).value + if (result.isNotEmpty()) { + val completion = assertIs(state.methodResult) + val reference = completion.value.asExpr(state.ctx.addressSort) + assertEquals(3, state.boundedStringBackingRefs[reference]) + val input = assertIs(test.before.parameters.single()).value + assertEquals(input.substring(1, 3) + "!", result) + } + + test + } + } + + assertTrue(tests.any { assertIs(it.returnValue).value.isNotEmpty() }) + replay(method = method, tests = tests) + } + + private fun method(name: String): EtsMethod = getMethod(methodName = name, className = "SymbolicStringModels") + + private fun replay(method: EtsMethod, tests: List) { + assertTrue(tests.isNotEmpty(), "No witnesses for ${method.name}") + + val script = buildString { + appendLine(source.readText()) + for ((index, test) in tests.withIndex()) { + val arguments = test.before.parameters.joinToString { literal(it) } + val expected = literal(test.returnValue) + + appendLine("if (new SymbolicStringModels().${method.name}($arguments) !== $expected) {") + appendLine(" throw Error('${method.name} witness $index');") + appendLine("}") + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "symbolic-string-model-${method.name}", + timeoutMessage = "String model witness replay timed out", + ) + } + + private fun literal(value: TsTestValue): String = when (value) { + is TsTestValue.TsString -> jsString(value.value) + is TsTestValue.TsNumber -> value.number.toString() + else -> error("Unexpected string model test value: $value") + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt index 140475c707..252c729ebb 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -225,7 +225,9 @@ class TsUnknownCallModelCatalogTest { "ts.string.indexOf", "ts.string.lastIndexOf", "ts.string.primitive.codeUnitAt", + "ts.string.primitive.copyNormalizedRange", "ts.string.primitive.fromCodeUnit", + "ts.string.primitive.isWhitespace", "ts.string.replaceAll", "ts.string.slice", "ts.string.split", diff --git a/usvm-ts/src/test/resources/models/ForeignPrimitiveHelpers.ts b/usvm-ts/src/test/resources/models/ForeignPrimitiveHelpers.ts index 06ee55696e..0a63e2cd47 100644 --- a/usvm-ts/src/test/resources/models/ForeignPrimitiveHelpers.ts +++ b/usvm-ts/src/test/resources/models/ForeignPrimitiveHelpers.ts @@ -1,5 +1,7 @@ declare class StringModelPrimitives { static codeUnitAt(value: string, index: number): number; + static isWhitespace(codeUnit: number): boolean; + static copyNormalizedRange(value: string, from: number, to: number): string; } declare class ArrayModelPrimitives { @@ -11,6 +13,14 @@ export class ForeignPrimitiveHelpers { return StringModelPrimitives.codeUnitAt("ab", 0); } + foreignWhitespace(): boolean { + return StringModelPrimitives.isWhitespace(32); + } + + foreignStringRange(): string { + return StringModelPrimitives.copyNormalizedRange("ab", 0, 1); + } + foreignArray(): number { const values = [1]; ArrayModelPrimitives.grow(values, 2); diff --git a/usvm-ts/src/test/resources/models/SymbolicStringModels.ts b/usvm-ts/src/test/resources/models/SymbolicStringModels.ts new file mode 100644 index 0000000000..7593856b92 --- /dev/null +++ b/usvm-ts/src/test/resources/models/SymbolicStringModels.ts @@ -0,0 +1,53 @@ +export class SymbolicStringModels { + trim(value: string): string { + return value.trim(); + } + + trimStart(value: string): string { + return value.trimStart(); + } + + trimEnd(value: string): string { + return value.trimEnd(); + } + + trimSingle(value: string): number { + if (value.length !== 1) return -1; + + return value.trim().length; + } + + slice(value: string, start: number, end: number): string { + return value.slice(start, end); + } + + substring(value: string, start: number, end: number): string { + return value.substring(start, end); + } + + searches(value: string): number { + const first = value.indexOf("\ud800"); + const last = value.lastIndexOf("\ud800"); + const included = value.includes("\ud800") ? 1 : 0; + const starts = value.startsWith("\ud800") ? 1 : 0; + const ends = value.endsWith("\ud800") ? 1 : 0; + + return first + 10 * last + 100 * included + 1000 * starts + 10000 * ends; + } + + split(value: string): string { + return value.split("\u0000", 3).join("|"); + } + + replaceAll(value: string): string { + if (value.length > 2) return ""; + + return value.replaceAll("\ud800", "$$$&"); + } + + boundedCopy(value: string): string { + if (value.length !== 4) return ""; + + return value.slice(1, 3) + "!"; + } +} From 25f663469ad27929f41fe55146b8736762465210 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 11:04:20 +0300 Subject: [PATCH 2/3] Preserve TypeScript analysis work across bounded phases --- .../org/usvm/machine/TsAnalysisSession.kt | 51 +++ .../main/kotlin/org/usvm/machine/TsMachine.kt | 240 ++++++++---- .../org/usvm/machine/TsAnalysisSessionTest.kt | 359 ++++++++++++++++++ 3 files changed, 577 insertions(+), 73 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/TsAnalysisSession.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsAnalysisSessionTest.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsAnalysisSession.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsAnalysisSession.kt new file mode 100644 index 0000000000..d416647c4e --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsAnalysisSession.kt @@ -0,0 +1,51 @@ +package org.usvm.machine + +/** + * One analysis whose queue and statistics survive a phase yield. The owning [TsMachine] must stay open. + * Closing the session discards pending work without closing the machine or its solvers. + */ +class TsAnalysisSession internal constructor( + advancePhase: (ULong?) -> TsMachineAnalysisResult, + analysisFinished: () -> Boolean, + release: () -> Unit, +) : AutoCloseable { + private var advancePhase: ((ULong?) -> TsMachineAnalysisResult)? = advancePhase + private var analysisFinished: (() -> Boolean)? = analysisFinished + private var release: (() -> Unit)? = release + private var advancing = false + + /** True after path exhaustion or a configured analysis limit, rather than a phase yield. */ + val isFinished: Boolean + get() = analysisFinished?.invoke() ?: true + + /** + * Runs at most [maxSteps] additional interpreter steps. Analysis-wide limits remain cumulative. + * A finished analysis returns its last snapshot without executing or notifying observers again. + * Bounded phases currently require one runnable entry point; multi-entry scheduling is uninterrupted. + */ + fun advance(maxSteps: ULong? = null): TsMachineAnalysisResult { + val phase = checkNotNull(advancePhase) { "Analysis session is closed" } + check(!advancing) { "Analysis session is already advancing" } + + advancing = true + var succeeded = false + try { + val result = phase(maxSteps) + succeeded = true + return result + } finally { + advancing = false + if (!succeeded) close() + } + } + + override fun close() { + check(!advancing) { "Cannot close an advancing analysis session" } + val releaseAnalysis = release ?: return + + advancePhase = null + analysisFinished = null + release = null + releaseAnalysis() + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 80e389983f..32c1df3928 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -143,6 +143,9 @@ class TsMachine( throwExceptionOnStepFailure = options.throwExceptionOnStepFailure, ) private val cfgStatistics = CfgStatisticsImpl(graph) + private var activeAnalysis: TsAnalysisSession? = null + private var preparingAnalysis = false + private var closed = false /** Returns supported states only. Call [analyzeWithOutcome] to inspect excluded unsupported paths. */ fun analyze( @@ -185,7 +188,38 @@ class TsMachine( methods: List, targets: List = emptyList(), configureInitialState: (EtsMethod, TsState) -> Unit = { _, _ -> }, - ): TsMachineAnalysisResult { + ): TsMachineAnalysisResult = openAnalysis( + methods = methods, + targets = targets, + configureInitialState = configureInitialState, + ).use { session -> session.advance() } + + /** Prepares one retained analysis; close it before starting another analysis on this machine. */ + fun openAnalysis( + methods: List, + targets: List = emptyList(), + configureInitialState: (EtsMethod, TsState) -> Unit = { _, _ -> }, + ): TsAnalysisSession { + check(!closed) { "Machine is closed" } + check(activeAnalysis == null && !preparingAnalysis) { + "Close the current analysis session before starting another" + } + + preparingAnalysis = true + try { + val session = prepareAnalysis(methods.toList(), targets.toList(), configureInitialState) + activeAnalysis = session + return session + } finally { + preparingAnalysis = false + } + } + + private fun prepareAnalysis( + methods: List, + targets: List, + configureInitialState: (EtsMethod, TsState) -> Unit, + ): TsAnalysisSession { interpreter.resetStepFailure() failureTrackingUnknownCallObserver.reset() @@ -193,52 +227,27 @@ class TsMachine( createInitialStates(methods, targets, configureInitialState) if (initialStates.isEmpty()) { - return emptyAnalysisResult(unsupportedPaths, infeasibleEntryPoints) + val result = emptyAnalysisResult(unsupportedPaths, infeasibleEntryPoints) + return TsAnalysisSession( + advancePhase = { result }, + analysisFinished = { true }, + release = { activeAnalysis = null }, + ) } - val methodsToTrackCoverage = - when (options.coverageZone) { - CoverageZone.METHOD, CoverageZone.TRANSITIVE -> initialStates.keys.toHashSet() - CoverageZone.CLASS -> classCoverageMethods(entryMethods = initialStates.keys) - } - - val coverageStatistics = CoverageStatistics( - methods = methodsToTrackCoverage, - applicationGraph = graph, - ) - - val callGraphStatistics: PlainCallGraphStatistics = - when (options.targetSearchDepth) { - 0u -> PlainCallGraphStatistics() - else -> TODO("Unsupported yet") - } - + val coverageStatistics = createCoverageStatistics(entryMethods = initialStates.keys) val timeStatistics = createTimeStatistics() - - val pathSelector = createPathSelector( + val pathSelector = createAnalysisPathSelector( initialStates = initialStates, - options = options, - applicationGraph = graph, timeStatistics = timeStatistics, - coverageStatisticsFactory = { coverageStatistics }, - cfgStatisticsFactory = { cfgStatistics }, - callGraphStatisticsFactory = { callGraphStatistics }, + coverageStatistics = coverageStatistics, ) val statesCollector = createStatesCollector(coverageStatistics) - val observers = mutableListOf>(coverageStatistics) - observers.add(statesCollector) - if (tsOptions.enableVisualization) { - observers += TsStateVisualizer() - } - - if (options.useSoftConstraints) { - observers.add(SoftConstraintsObserver()) - } - val stepsStatistics = StepsStatistics() var timedOut = false + var finished = false val stopStrategy = object : StopStrategy { val strategy = createStopStrategy( options, @@ -252,15 +261,14 @@ class TsMachine( override fun shouldStop(): Boolean { if (options.timeout <= kotlin.time.Duration.ZERO) { timedOut = true + finished = true return true } val result = strategy.shouldStop() - if (result && timeStatistics.runningTime >= options.timeout) { - timedOut = true - } - if (result) { + timedOut = timeStatistics.runningTime >= options.timeout + finished = true logger.warn { "Stop strategy finished execution: ${strategy.stopReason()}" } } @@ -268,6 +276,118 @@ class TsMachine( } } + val supportedObserver = createAnalysisObserver( + initialStates = initialStates, + coverageStatistics = coverageStatistics, + statesCollector = statesCollector, + timeStatistics = timeStatistics, + stepsStatistics = stepsStatistics, + ) + val outcomeObserver = UnsupportedPathsObserver( + delegate = supportedObserver, + unsupportedPaths = unsupportedPaths, + ) + val factoryObserver = machineObserverFactory?.invoke(pathSelector) + val executionObserver = if (factoryObserver == null) { + outcomeObserver + } else { + CompositeUMachineObserver(outcomeObserver, factoryObserver) + } + + var lastResult: TsMachineAnalysisResult? = null + return TsAnalysisSession( + advancePhase = { maxSteps -> + if (finished) { + requireNotNull(lastResult) + } else { + require(maxSteps == null || initialStates.size == 1) { + "Bounded analysis phases require one runnable entry point" + } + + val phaseStartSteps = stepsStatistics.totalSteps + val phaseStopStrategy = StopStrategy { + val analysisStopped = stopStrategy.shouldStop() + val phaseStopped = maxSteps != null && stepsStatistics.totalSteps - phaseStartSteps >= maxSteps + analysisStopped || phaseStopped + } + + run( + interpreter = interpreter, + pathSelector = pathSelector, + observer = executionObserver, + isStateTerminated = { state -> state.callStack.isEmpty() }, + stopStrategy = phaseStopStrategy, + ) + + val exhausted = pathSelector.isEmpty() + finished = finished || exhausted + val stopReason = if (exhausted) TsAnalysisStopReason.EXHAUSTED else TsAnalysisStopReason.STOPPED + val result = TsMachineAnalysisResult( + states = statesCollector.collectedStates.toList(), + stopReason = stopReason, + timedOut = timedOut, + unsupportedCall = failureTrackingUnknownCallObserver.pathStopped, + engineFailed = interpreter.stepFailed, + unsupportedPaths = unsupportedPaths.toList(), + infeasibleEntryPoints = infeasibleEntryPoints, + ) + lastResult = result + result + } + }, + analysisFinished = { finished }, + release = { activeAnalysis = null }, + ) + } + + private fun createCoverageStatistics( + entryMethods: Set, + ): CoverageStatistics { + val methodsToTrackCoverage = when (options.coverageZone) { + CoverageZone.METHOD, CoverageZone.TRANSITIVE -> entryMethods.toHashSet() + CoverageZone.CLASS -> classCoverageMethods(entryMethods = entryMethods) + } + + return CoverageStatistics(methods = methodsToTrackCoverage, applicationGraph = graph) + } + + private fun createAnalysisPathSelector( + initialStates: Map, + timeStatistics: TimeStatistics, + coverageStatistics: CoverageStatistics, + ): UPathSelector { + val callGraphStatistics: PlainCallGraphStatistics = when (options.targetSearchDepth) { + 0u -> PlainCallGraphStatistics() + else -> TODO("Unsupported yet") + } + + return createPathSelector( + initialStates = initialStates, + options = options, + applicationGraph = graph, + timeStatistics = timeStatistics, + coverageStatisticsFactory = { coverageStatistics }, + cfgStatisticsFactory = { cfgStatistics }, + callGraphStatisticsFactory = { callGraphStatistics }, + ) + } + + private fun createAnalysisObserver( + initialStates: Map, + coverageStatistics: CoverageStatistics, + statesCollector: StatesCollector, + timeStatistics: TimeStatistics, + stepsStatistics: StepsStatistics, + ): UMachineObserver { + val observers = mutableListOf>(coverageStatistics, statesCollector) + if (tsOptions.enableVisualization) { + observers += TsStateVisualizer() + } + + if (options.useSoftConstraints) { + observers.add(SoftConstraintsObserver()) + } + observers.add(timeStatistics) observers.add(stepsStatistics) machineObserver?.let { observers.add(it) } @@ -280,43 +400,12 @@ class TsMachine( getMethodSignature = { it.humanReadableSignature }, coverageStatistics = coverageStatistics, timeStatistics = timeStatistics, - stepsStatistics = stepsStatistics + stepsStatistics = stepsStatistics, ) ) } - val supportedObserver = CompositeUMachineObserver(observers) - val outcomeObserver = UnsupportedPathsObserver( - delegate = supportedObserver, - unsupportedPaths = unsupportedPaths, - ) - val factoryObserver = machineObserverFactory?.invoke(pathSelector) - val executionObserver = if (factoryObserver == null) { - outcomeObserver - } else { - CompositeUMachineObserver(outcomeObserver, factoryObserver) - } - - run( - interpreter = interpreter, - pathSelector = pathSelector, - observer = executionObserver, - isStateTerminated = { state -> state.callStack.isEmpty() }, - stopStrategy = stopStrategy, - ) - - val exhausted = pathSelector.isEmpty() - val stopReason = if (exhausted) TsAnalysisStopReason.EXHAUSTED else TsAnalysisStopReason.STOPPED - - return TsMachineAnalysisResult( - states = statesCollector.collectedStates, - stopReason = stopReason, - timedOut = timedOut, - unsupportedCall = failureTrackingUnknownCallObserver.pathStopped, - engineFailed = interpreter.stepFailed, - unsupportedPaths = unsupportedPaths.toList(), - infeasibleEntryPoints = infeasibleEntryPoints, - ) + return CompositeUMachineObserver(observers) } private fun createStatesCollector( @@ -412,6 +501,11 @@ class TsMachine( } override fun close() { + if (closed) return + check(!preparingAnalysis) { "Cannot close the machine while preparing an analysis" } + + activeAnalysis?.close() + closed = true components.close() } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsAnalysisSessionTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsAnalysisSessionTest.kt new file mode 100644 index 0000000000..2a213e14cb --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsAnalysisSessionTest.kt @@ -0,0 +1,359 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.PathSelectorFairnessStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.state.TsState +import org.usvm.statistics.UMachineObserver +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds + +/** Queue, budget and ownership contracts; generated witnesses are also checked in the native runtime. */ +class TsAnalysisSessionTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/samples/lang/Exceptions.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + private val method by lazy { getMethod(methodName = "conditionalCatch", className = "Exceptions") } + private val analysisOptions = UMachineOptions( + solverType = SolverType.YICES, + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + throwExceptionOnStepFailure = true, + ) + + @Test + fun `one step phases reuse the initial state and prefix queries and preserve native outcomes`() { + val direct = execute(phased = false) + + val phased = execute(phased = true) + + assertEquals(expected = 1, actual = phased.initializations) + assertEquals(expected = direct.steps, actual = phased.steps) + assertEquals(expected = direct.queries, actual = phased.queries) + assertTrue(phased.phases > 1) + assertEquals(expected = setOf(1.0, 2.0), actual = phased.tests.map(::resultNumber).toSet()) + assertEquals( + expected = direct.tests.map(::resultNumber).toSet(), + actual = phased.tests.map(::resultNumber).toSet(), + ) + + val script = buildString { + appendLine(source.readText()) + phased.tests.forEach { test -> + val input = assertIs(test.before.parameters.single()).number + val expected = if (input == 0.0) 2.0 else 1.0 + assertEquals(expected = expected, actual = resultNumber(test)) + + appendLine("if (new Exceptions().conditionalCatch($input) !== $expected) {") + appendLine(" throw Error('session witness');") + appendLine("}") + } + } + assertNodeReplay( + source = script, + directory = directory, + name = "analysis-session", + timeoutMessage = "Native replay of retained-session witnesses timed out", + ) + } + + @Test + fun `analysis step limit is cumulative and cannot be reset by another advance`() { + var steps = 0 + val observer = object : UMachineObserver { + override fun onState(parent: TsState, forks: Sequence) { + steps++ + } + } + val options = analysisOptions.copy(stepLimit = 2uL) + + TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + machineObserver = observer, + ).use { machine -> + machine.openAnalysis(methods = listOf(method)).use { session -> + val first = session.advance(maxSteps = 1uL) + assertEquals(expected = TsAnalysisStopReason.STOPPED, actual = first.stopReason) + assertFalse(session.isFinished) + + val second = session.advance(maxSteps = 1uL) + assertEquals(expected = TsAnalysisStopReason.STOPPED, actual = second.stopReason) + assertTrue(session.isFinished) + assertFalse(second.timedOut) + assertEquals(expected = 2, actual = steps) + + assertEquals(expected = second, actual = session.advance()) + assertEquals(expected = 2, actual = steps) + } + } + } + + @Test + fun `phase snapshots do not acquire states collected by later advances`() { + TsMachine(scene = scene, options = analysisOptions, tsOptions = TsOptions()).use { machine -> + machine.openAnalysis(methods = listOf(method)).use { session -> + var snapshot = session.advance(maxSteps = 1uL) + var phases = 1 + while (snapshot.states.isEmpty() && !session.isFinished) { + assertTrue(phases++ < MAX_PHASES) + snapshot = session.advance(maxSteps = 1uL) + } + assertEquals(expected = 1, actual = snapshot.states.size) + val firstState = snapshot.states.single() + + val final = session.advance() + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = final.stopReason) + assertEquals(expected = 2, actual = final.states.size) + assertEquals(expected = listOf(firstState), actual = snapshot.states) + } + } + } + + @Test + fun `closing a session releases the machine and closing the machine invalidates the session`() { + val machine = TsMachine(scene = scene, options = analysisOptions, tsOptions = TsOptions()) + machine.use { + val session = machine.openAnalysis(methods = listOf(method)) + session.advance(maxSteps = 1uL) + assertFailsWith { machine.openAnalysis(methods = listOf(method)) } + assertFailsWith { machine.analyzeWithMetadata(methods = listOf(method)) } + + session.close() + session.close() + + assertTrue(session.isFinished) + assertFailsWith { session.advance() } + assertEquals( + expected = TsAnalysisStopReason.EXHAUSTED, + actual = machine.analyzeWithMetadata(methods = listOf(method)).stopReason, + ) + + val next = machine.openAnalysis(methods = listOf(method)) + machine.close() + + assertTrue(next.isFinished) + assertFailsWith { next.advance() } + assertFailsWith { machine.openAnalysis(methods = listOf(method)) } + } + } + + @Test + fun `timeout stops the analysis rather than yielding a resumable phase`() { + var steps = 0 + val observer = object : UMachineObserver { + override fun onState(parent: TsState, forks: Sequence) { + steps++ + } + } + val options = analysisOptions.copy(timeout = Duration.ZERO) + + TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + machineObserver = observer, + ).use { machine -> + machine.openAnalysis(methods = listOf(method)).use { session -> + val result = session.advance(maxSteps = 1uL) + + assertTrue(result.timedOut) + assertTrue(session.isFinished) + assertEquals(expected = 0, actual = steps) + assertEquals(expected = result, actual = session.advance()) + } + } + } + + @Test + fun `empty analysis is finished without invoking machine lifecycle observers`() { + var starts = 0 + val observer = object : UMachineObserver { + override fun onMachineStarted() { + starts++ + } + } + + TsMachine( + scene = scene, + options = analysisOptions, + tsOptions = TsOptions(), + machineObserver = observer, + ).use { machine -> + machine.openAnalysis(methods = emptyList()).use { session -> + assertTrue(session.isFinished) + + val result = session.advance() + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = result.stopReason) + assertTrue(result.states.isEmpty()) + assertEquals(expected = 0, actual = starts) + } + } + } + + @Test + fun `bounded phases reject multiple runnable entries without changing uninterrupted scheduling`() { + val other = getMethod(methodName = "caughtValue", className = "Exceptions") + val methods = listOf(method, other) + + for (fairness in PathSelectorFairnessStrategy.entries) { + val options = analysisOptions.copy(pathSelectorFairnessStrategy = fairness, timeout = 10.seconds) + TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine -> + val session = machine.openAnalysis(methods = methods) + + val failure = assertFailsWith { session.advance(maxSteps = 1uL) } + + assertTrue(failure.message.orEmpty().contains("one runnable entry point")) + assertTrue(session.isFinished) + + val result = machine.analyzeWithMetadata(methods = methods) + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = result.stopReason) + assertEquals(expected = methods.toSet(), actual = result.states.map { it.entrypoint }.toSet()) + } + } + } + + @Test + fun `initial state callbacks cannot open a nested analysis and failed preparation releases the owner`() { + TsMachine(scene = scene, options = analysisOptions, tsOptions = TsOptions()).use { machine -> + val failure = assertFailsWith { + machine.openAnalysis(methods = listOf(method), configureInitialState = { _, _ -> + machine.openAnalysis(methods = emptyList()) + }) + } + + assertTrue(failure.message.orEmpty().contains("current analysis session")) + val result = machine.analyzeWithMetadata(methods = listOf(method)) + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = result.stopReason) + } + } + + @Test + fun `an exceptional advance invalidates its session and releases the machine`() { + var failNextStep = true + val observer = object : UMachineObserver { + override fun onStatePeeked(state: TsState) { + if (failNextStep) { + failNextStep = false + error("phase observer failed") + } + } + } + + TsMachine( + scene = scene, + options = analysisOptions, + tsOptions = TsOptions(), + machineObserver = observer, + ).use { machine -> + val session = machine.openAnalysis(methods = listOf(method)) + + val failure = assertFailsWith { session.advance(maxSteps = 1uL) } + + assertEquals(expected = "phase observer failed", actual = failure.message) + assertTrue(session.isFinished) + assertFailsWith { session.advance() } + assertEquals( + expected = TsAnalysisStopReason.EXHAUSTED, + actual = machine.analyzeWithMetadata(methods = listOf(method)).stopReason, + ) + } + } + + private fun execute(phased: Boolean): Execution { + var initializations = 0 + var steps = 0 + var queries = 0 + var phases = 0 + val machineObserver = object : UMachineObserver { + override fun onState(parent: TsState, forks: Sequence) { + steps++ + } + } + val interpreterObserver = object : TsInterpreterObserver { + override fun onSolverQuery(event: TsSolverQueryEvent) { + queries++ + } + } + + val outcome = TsMachine( + scene = scene, + options = analysisOptions, + tsOptions = TsOptions(), + machineObserver = machineObserver, + observer = interpreterObserver, + ).use { machine -> + machine.openAnalysis(methods = listOf(method), configureInitialState = { _, _ -> initializations++ }) + .use { session -> + var result: TsMachineAnalysisResult + do { + assertTrue(phases++ < MAX_PHASES) + result = session.advance(maxSteps = if (phased) 1uL else null) + } while (!session.isFinished) + + val stepsAtFinish = steps + val queriesAtFinish = queries + session.advance() + assertEquals(expected = stepsAtFinish, actual = steps) + assertEquals(expected = queriesAtFinish, actual = queries) + result + } + } + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = outcome.stopReason) + assertFalse(outcome.engineFailed) + assertFalse(outcome.unsupportedCall) + assertTrue(outcome.unsupportedPaths.isEmpty()) + + return Execution( + initializations = initializations, + steps = steps, + queries = queries, + phases = phases, + tests = outcome.states.map { state -> TsTestResolver().resolve(method, state) }, + ) + } + + private fun resultNumber(test: TsTest): Double = assertIs(test.returnValue).number + + private data class Execution( + val initializations: Int, + val steps: Int, + val queries: Int, + val phases: Int, + val tests: List, + ) + + companion object { + private const val MAX_PHASES = 200 + } +} From c3ce550489f13b2200b406f77cde471bcb516552 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 11:25:22 +0300 Subject: [PATCH 3/3] [TS PBT] Retain property analysis across native coverage updates Keep the original manifest, projection, observers, pending queue and solver resources across bounded advances. Validate later native evidence against a pinned environment, invalidate changed source, and retain early counterexamples in partial results. --- .../pbt/usvm/UsvmPropertySearchSessionTest.kt | 325 ++++++++++++++++++ .../retained-session/retained-branches.ts | 15 + .../retained-session/retained-property.ts | 26 ++ .../org/usvm/ts/pbt/PbtDiagnosticCode.kt | 1 + .../usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt | 16 + .../org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt | 84 ++++- .../ts/pbt/usvm/UsvmPropertySearchModel.kt | 5 +- .../ts/pbt/usvm/UsvmPropertySearchSession.kt | 55 +++ .../usvm/ts/pbt/usvm/UsvmPropertySearcher.kt | 207 +++++++++-- 9 files changed, 690 insertions(+), 44 deletions(-) create mode 100644 usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchSessionTest.kt create mode 100644 usvm-ts-fast-check/src/test/resources/properties/retained-session/retained-branches.ts create mode 100644 usvm-ts-fast-check/src/test/resources/properties/retained-session/retained-property.ts create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchSession.kt diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchSessionTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchSessionTest.kt new file mode 100644 index 0000000000..edc71b4d32 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchSessionTest.kt @@ -0,0 +1,325 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.PropertyCoverageArtifact +import org.usvm.ts.pbt.backend.PropertyCoverageRequest +import org.usvm.ts.pbt.backend.PropertyFailureKind +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +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.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertNotEquals +import kotlin.test.assertNotNull +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class UsvmPropertySearchSessionTest { + @Test + fun `native coverage between advances changes the existing pending queue for the original predicate`() { + val positive = resumeWithNativeEvidence(value = 1) + val negative = resumeWithNativeEvidence(value = -1) + + val positivePrefix = positive.first.selections.map { Triple(it.statement, it.pendingStates, it.goal) } + val negativePrefix = negative.first.selections.map { Triple(it.statement, it.pendingStates, it.goal) } + assertEquals(positivePrefix, negativePrefix) + assertNotEquals(positive.selectedGoal, negative.selectedGoal) + assertEquals(positive.first.initialGoals, negative.first.initialGoals) + } + + @Test + fun `stale incompatible and rejected-input artifacts leave the retained analysis usable`() { + val initial = initialCoverage() + val identity = assertNotNull(initial.identity) + val rejected = listOf( + initial.copy(identity = identity.copy(manifestSha256 = "0".repeat(64))) to UsvmCoverageUpdateStatus.STALE, + initial.copy(provenance = initial.provenance.copy(runtimeVersion = "different")) to + UsvmCoverageUpdateStatus.INCOMPATIBLE, + initial.copy(admittedInvocations = 0) to UsvmCoverageUpdateStatus.NO_ADMITTED_INPUTS, + initial.copy(identity = null) to UsvmCoverageUpdateStatus.UNSUPPORTED, + ) + + openSession(initial).use { session -> + val first = session.advance(maxSteps = 1uL) + for ((artifact, status) in rejected) { + val update = session.applyCoverage(artifact) + + assertEquals(status, update.status, first.edgeGuidance.toString()) + assertTrue(update.additions.isEmpty()) + assertFalse(session.isFinished) + } + val next = session.advance(maxSteps = 1uL) + + assertEquals(UsvmPropertySearchStatus.IN_PROGRESS, first.status) + assertEquals(UsvmPropertySearchStatus.IN_PROGRESS, next.status) + val firstTrace = assertNotNull(first.edgeGuidance) + val nextTrace = assertNotNull(next.edgeGuidance) + assertEquals(firstTrace.selections, nextTrace.selections.take(firstTrace.selections.size)) + assertEquals(firstTrace.confirmedCovered, nextTrace.confirmedCovered) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, session.advance().status) + } + } + + @Test + fun `caller collection mutations cannot replace the original property or native environment`() { + val initial = initialCoverage() + val sourceRoots = initial.provenance.sourceRoots.toMutableList() + val patterns = initial.provenance.request.includePatterns.toMutableList() + val anchor = initial.copy( + provenance = initial.provenance.copy( + sourceRoots = sourceRoots, + request = initial.provenance.request.copy(includePatterns = patterns), + ), + ) + val inputs = property.inputs.toMutableList() + val definition = property.copy(inputs = inputs) + + openSession(anchor, definition = definition).use { session -> + sourceRoots += "changed-by-caller" + patterns += "**/changed-by-caller" + inputs.clear() + val update = session.applyCoverage(initial) + val changed = session.applyCoverage(anchor) + val progress = session.advance(maxSteps = 1uL) + + assertEquals(UsvmCoverageUpdateStatus.ACCEPTED, update.status) + assertEquals(UsvmCoverageUpdateStatus.INCOMPATIBLE, changed.status) + assertEquals(UsvmPropertySearchStatus.IN_PROGRESS, progress.status) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, session.advance().status) + } + } + + @Test + fun `an unsupported completed path leaves a partial phase in progress until pending work finishes`() { + val definition = property.copy( + predicate = TypeScriptEntryPoint(module = MODULE, exportName = "partialUnsupported"), + ) + val initial = assertNotNull(backend.run(definition, configuration).coverage) + + openSession(initial, definition = definition).use { session -> + var progress = session.advance(maxSteps = 0uL) + var observedUnsupported = false + var steps = 0 + while (!observedUnsupported && !session.isFinished && steps < 200) { + progress = session.advance(maxSteps = 1uL) + observedUnsupported = progress.diagnostics.any { it.code == "usvm.execution.unsupported" } + steps += 1 + } + + assertTrue(observedUnsupported, progress.toString()) + assertFalse(session.isFinished, progress.toString()) + assertEquals(UsvmPropertySearchStatus.IN_PROGRESS, progress.status) + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, session.advance().status) + assertTrue(session.isFinished) + } + } + + @Test + fun `a partial phase retains its reached violation while another path remains pending`() { + val definition = property.copy(predicate = TypeScriptEntryPoint(module = MODULE, exportName = "earlyViolation")) + val initial = assertNotNull(backend.run(definition, configuration).coverage) + + openSession(initial, definition = definition, stopOnTargetsReached = false).use { session -> + var progress = session.advance(maxSteps = 0uL) + var steps = 0 + while (progress.inputs == null && !session.isFinished && steps < 200) { + progress = session.advance(maxSteps = 1uL) + steps += 1 + } + + val candidate = assertNotNull(progress.inputs, progress.toString()) + assertEquals(UsvmPropertySearchStatus.IN_PROGRESS, progress.status) + assertEquals(UsvmPropertyViolationTarget.PREDICATE_FALSE, progress.target) + assertFalse(session.isFinished) + val next = session.advance(maxSteps = 1uL) + val replay = backend.run( + property = definition, + configuration = configuration.copy(examples = listOf(candidate), exactReplay = true), + ) + + assertEquals(candidate, next.inputs) + assertEquals(progress.target, next.target) + assertEquals(PropertyFailureKind.PROPERTY, replay.failure?.kind) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, session.advance().status) + } + } + + @Test + fun `a current source change invalidates reuse instead of merely rejecting a stale report`() { + for (applyFirst in listOf(false, true)) { + withCopiedSources { root -> + val roots = listOf(root) + val backend = FastCheckBackend(sourceRoots = roots) + val scene = loadEtsProjectAutoConvert(root, provider = EtsIrProvider.TS_FRONTEND) + val initial = assertNotNull(backend.run(property, configuration).coverage) + val source = root.resolve(MODULE) + val original = Files.readString(source) + + openSession(initial, scene, roots).use { session -> + val first = session.advance(maxSteps = 1uL) + Files.writeString(source, original + "\n// changed after analysis preparation\n") + if (applyFirst) { + assertEquals(UsvmCoverageUpdateStatus.SOURCE_CHANGED, session.applyCoverage(initial).status) + } + val invalidated = session.advance(maxSteps = 1uL) + Files.writeString(source, original) + val afterRestore = session.advance() + + assertEquals(UsvmPropertySearchStatus.SOURCE_INVALIDATED, invalidated.status) + assertEquals(UsvmPropertySearchStatus.SOURCE_INVALIDATED, afterRestore.status) + assertTrue(session.isFinished) + assertTrue(invalidated.diagnostics.any { it.code == "usvm.session.source.changed" }) + assertEquals(first.edgeGuidance?.selections, invalidated.edgeGuidance?.selections) + } + } + } + } + + @Test + fun `closing a paused session releases it and forbids later work`() { + val initial = initialCoverage() + val session = openSession(initial) + session.advance(maxSteps = 1uL) + + session.close() + session.close() + + assertTrue(session.isFinished) + assertFailsWith { session.advance() } + assertFailsWith { session.applyCoverage(initial) } + } + + private fun resumeWithNativeEvidence(value: Int): ResumeObservation { + val initial = initialCoverage() + openSession(initial).use { session -> + val first = pauseWithThreeStates(session) + val trace = assertNotNull(first.edgeGuidance) + assertEquals(2, trace.initialGoals.size, trace.toString()) + val beforeIds = trace.selections.map { it.stateId }.toSet() + val example = listOf(JsConcreteValue.number(value.toDouble())) + val later = assertNotNull( + backend.run( + property = property, + configuration = configuration.copy(examples = listOf(example)), + ).coverage, + ) + + val update = session.applyCoverage(later) + val second = session.advance(maxSteps = 2uL) + + assertEquals(UsvmPropertySearchStatus.IN_PROGRESS, first.status) + assertEquals(UsvmPropertySearchStatus.IN_PROGRESS, second.status) + assertEquals(UsvmCoverageUpdateStatus.ACCEPTED, update.status) + assertEquals(1, update.additions.size) + val expectedGoal = (trace.initialGoals - update.additions).single() + val secondTrace = assertNotNull(second.edgeGuidance) + assertEquals(trace.selections, secondTrace.selections.take(trace.selections.size)) + val selected = secondTrace.selections.drop(trace.selections.size).first { !it.originalObjectiveTurn } + assertEquals(expectedGoal, selected.goal) + assertTrue(selected.stateId in beforeIds) + val completed = session.advance() + val repeated = session.advance() + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, completed.status) + assertTrue(session.isFinished) + assertEquals(completed.edgeGuidance?.selections, repeated.edgeGuidance?.selections) + assertEquals(property.id, completed.propertyId) + assertEquals(null, completed.inputs) + return ResumeObservation(first = trace, selectedGoal = expectedGoal) + } + } + + private fun pauseWithThreeStates(session: UsvmPropertySearchSession): UsvmPropertySearchResult { + var result = session.advance(maxSteps = 0uL) + repeat(200) { + result = session.advance(maxSteps = 1uL) + val trace = assertNotNull(result.edgeGuidance) + val seenThreeStates = trace.selections.map { selection -> selection.stateId }.distinct().size >= 3 + val threeStatesPending = trace.selections.last().pendingStates >= 3 + if (seenThreeStates && threeStatesPending) return result + + assertFalse(session.isFinished, trace.toString()) + } + error("Three pending states were not observed: $result") + } + + private fun initialCoverage(): PropertyCoverageArtifact = assertNotNull( + backend.run(property = property, configuration = configuration).coverage, + ) + + private fun openSession( + coverage: PropertyCoverageArtifact, + scene: EtsScene = Companion.scene, + roots: List = Companion.roots, + definition: PropertyDefinition = property, + stopOnTargetsReached: Boolean = false, + ): UsvmPropertySearchSession { + val manifest = definition.toManifest() + val mapping = PropertyEtsMapper(scene = scene, sourceRoots = roots).map(manifest, coverage) + val searcher = UsvmPropertySearcher( + scene = scene, + machineOptions = UMachineOptions( + solverType = SolverType.YICES, + timeout = 20.seconds, + stopOnTargetsReached = stopOnTargetsReached, + ), + ) + return searcher.openSession( + manifest = manifest, + mapping = mapping, + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + coverageFeedback = UsvmCoverageFeedback(initialCoverage = coverage) { null }, + ) + } + + private fun withCopiedSources(action: (Path) -> Unit) { + val directory = Files.createTempDirectory("usvm-retained-property-") + try { + Files.copy(roots.single().resolve(MODULE), directory.resolve(MODULE)) + Files.copy(roots.single().resolve("retained-branches.ts"), directory.resolve("retained-branches.ts")) + action(directory) + } finally { + Files.walk(directory).use { paths -> + paths.sorted(Comparator.reverseOrder()).forEach(Files::deleteIfExists) + } + } + } + + private data class ResumeObservation(val first: UsvmEdgeGuidanceTrace, val selectedGoal: UsvmCoverageEdge) + + private companion object { + const val MODULE = "retained-property.ts" + val roots = listOf(testResourcesRoot().resolve("properties/retained-session")) + val scene: EtsScene by lazy { loadEtsProjectAutoConvert(roots.single(), provider = EtsIrProvider.TS_FRONTEND) } + val backend = FastCheckBackend(sourceRoots = roots) + val property = PropertyDefinition( + id = PropertyId("retained.original"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = -100, max = 100))), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = "valid"), + ) + val configuration = PropertyRunConfiguration( + seed = 42, + numRuns = 1, + timeoutMillis = 10_000, + examples = listOf(listOf(JsConcreteValue.number(0.0))), + coverageRequest = PropertyCoverageRequest(admittedOnly = true), + ) + } +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/retained-session/retained-branches.ts b/usvm-ts-fast-check/src/test/resources/properties/retained-session/retained-branches.ts new file mode 100644 index 0000000000..b9eecace6f --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/retained-session/retained-branches.ts @@ -0,0 +1,15 @@ +export function positive(value: number): number { + if (value > 0) { + return 1; + } else { + return 0; + } +} + +export function negative(value: number): number { + if (value < 0) { + return 1; + } else { + return 0; + } +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/retained-session/retained-property.ts b/usvm-ts-fast-check/src/test/resources/properties/retained-session/retained-property.ts new file mode 100644 index 0000000000..29c14f27a8 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/retained-session/retained-property.ts @@ -0,0 +1,26 @@ +import { negative, positive } from './retained-branches'; + +export function valid(value: number): boolean { + let result = positive(value) + negative(value); + result = result + 1; + result = result + 1; + result = result + 1; + return result >= 0; +} + +export function partialUnsupported(value: number): boolean { + if (value > 0) { + const values = { present: 1 }; + return values[value] === 1; + } else { + return valid(value); + } +} + +export function earlyViolation(value: number): boolean { + if (value > 0) { + return false; + } else { + return valid(value); + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt index 834f33602e..c6e7a87e79 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt @@ -44,6 +44,7 @@ internal object PbtDiagnosticCode { const val USVM_PREDICATE_MAPPING_NON_EXACT = "usvm.predicate.mapping.non-exact" const val USVM_PREDICATE_RESULT_NON_BOOLEAN = "usvm.predicate.result.non-boolean" const val USVM_SOLVER_UNKNOWN = "usvm.solver.unknown" + const val USVM_SESSION_SOURCE_CHANGED = "usvm.session.source.changed" const val PROPERTY_ID_INVALID = "property.id.invalid" const val PROPERTY_ASSERTION_INVALID = "property.assertion.invalid" diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt index 55fc793b43..0493c7367f 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt @@ -10,6 +10,22 @@ data class UsvmCoverageFeedback( val replay: (inputs: List) -> PropertyRunResult?, ) +/** Outcome of applying a later native report to the original property session. */ +enum class UsvmCoverageUpdateStatus { + ACCEPTED, + STALE, + INCOMPATIBLE, + NO_ADMITTED_INPUTS, + UNSUPPORTED, + SOURCE_CHANGED, +} + +/** Only accepted, exactly mapped native hits can appear in [additions]. */ +data class UsvmCoverageUpdateResult( + val status: UsvmCoverageUpdateStatus, + val additions: Set = emptySet(), +) + /** Why a report can or cannot supply exact coverage goals for this property/source snapshot. */ enum class UsvmCoverageEvidenceStatus { ABSENT, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt index 2cc5a46522..977d2372a2 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt @@ -11,6 +11,8 @@ import org.usvm.machine.TsMethodCall import org.usvm.machine.state.TsState import org.usvm.ps.BfsPathSelector import org.usvm.ps.CoverageGuidedPathSelector +import org.usvm.ts.pbt.backend.CoverageArtifactKind +import org.usvm.ts.pbt.backend.CoverageProvenance import org.usvm.ts.pbt.backend.PropertyCoverageArtifact import org.usvm.ts.pbt.backend.PropertyFailureKind import org.usvm.ts.pbt.backend.PropertyRunResult @@ -22,6 +24,7 @@ import org.usvm.ts.pbt.mapping.EtsMappingStatus import org.usvm.ts.pbt.mapping.PropertyEtsMapper import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact import org.usvm.ts.pbt.model.JsConcreteValue +import java.io.IOException import java.nio.file.Path import java.util.concurrent.CancellationException import kotlin.time.TimeSource @@ -37,6 +40,25 @@ internal class UsvmEdgeGuidance( private val roots = mapping.provenance.sourceRoots.map(Path::of) private val started = TimeSource.Monotonic.markNow() private val identity = captureCoverageIdentity(manifest, roots) + private val environment = feedback.initialCoverage?.let { coverage -> + val provenance = coverage.provenance + val request = provenance.request + val pinnedRequest = request.copy( + scopes = request.scopes.toSet(), + includePatterns = request.includePatterns.toList(), + excludePatterns = request.excludePatterns.toList(), + ) + val pinnedProvenance = provenance.copy( + sourceRoots = provenance.sourceRoots.toList(), + request = pinnedRequest, + ) + NativeEnvironment( + backendId = coverage.backendId, + backendVersion = coverage.backendVersion, + kind = coverage.kind, + provenance = pinnedProvenance, + ) + } private val targets = linkedMapOf() private val covered = linkedSetOf() private val attempted = linkedSetOf() @@ -143,7 +165,6 @@ internal class UsvmEdgeGuidance( val replayStarted = TimeSource.Monotonic.markNow() val decision = replay(inputs, claimed, expectsViolation) - activeSelector?.updateCoverage() val exhaustedRetry = claimed.any { attemptsByGoal.getValue(it) == MAX_REPLAY_ATTEMPTS_PER_GOAL } if (exhaustedRetry && decision.status != UsvmEdgeReplayStatus.CONFIRMED) { activeSelector?.refreshPriorities() @@ -158,6 +179,36 @@ internal class UsvmEdgeGuidance( ) } + fun sourceUnchanged(): Boolean = try { + captureCoverageIdentity(manifest, roots) == identity + } catch (_: IOException) { + false + } + + fun applyCoverage(coverage: PropertyCoverageArtifact): UsvmCoverageUpdateResult { + if (!sourceUnchanged()) return UsvmCoverageUpdateResult(status = UsvmCoverageUpdateStatus.SOURCE_CHANGED) + + val anchored = evidenceStatus == UsvmCoverageEvidenceStatus.EXACT || + evidenceStatus == UsvmCoverageEvidenceStatus.PARTIAL + if (!anchored) return UsvmCoverageUpdateResult(status = UsvmCoverageUpdateStatus.UNSUPPORTED) + + val incomingStatus = evidenceStatus(coverage) + val rejection = when (incomingStatus) { + UsvmCoverageEvidenceStatus.STALE -> UsvmCoverageUpdateStatus.STALE + UsvmCoverageEvidenceStatus.NO_ADMITTED_INPUTS -> UsvmCoverageUpdateStatus.NO_ADMITTED_INPUTS + UsvmCoverageEvidenceStatus.EXACT, UsvmCoverageEvidenceStatus.PARTIAL -> null + else -> UsvmCoverageUpdateStatus.UNSUPPORTED + } + if (rejection != null) return UsvmCoverageUpdateResult(status = rejection) + + if (!compatibleEnvironment(coverage)) { + return UsvmCoverageUpdateResult(status = UsvmCoverageUpdateStatus.INCOMPATIBLE) + } + + val additions = updateEdges(exactEdges(coverage)) + return UsvmCoverageUpdateResult(status = UsvmCoverageUpdateStatus.ACCEPTED, additions = additions) + } + // Feedback is optional: an arbitrary backend/transport exception must not // abort the original symbolic property objective or manufacture coverage. @Suppress("TooGenericExceptionCaught") @@ -201,11 +252,18 @@ internal class UsvmEdgeGuidance( val confirmed = observed.filter { it.hits > 0 }.mapTo(hashSetOf()) { it.edge } if (!confirmed.containsAll(claimed)) return ReplayDecision(status = UsvmEdgeReplayStatus.EDGE_MISMATCH) + val additions = updateEdges(observed) + return ReplayDecision(status = UsvmEdgeReplayStatus.CONFIRMED, additions = additions) + } + + private fun updateEdges(observed: List): Set { observed.forEach { targets.putIfAbsent(it.edge, it.target) } - val additions = confirmed - covered + val additions = observed.filter { it.hits > 0 }.mapTo(linkedSetOf()) { it.edge } - covered covered += additions if (additions.isNotEmpty()) revision += 1 - return ReplayDecision(status = UsvmEdgeReplayStatus.CONFIRMED, additions = additions) + + activeSelector?.updateCoverage() + return additions } private fun matchesOracle( @@ -221,13 +279,16 @@ internal class UsvmEdgeGuidance( } private fun isCompatible(coverage: PropertyCoverageArtifact): Boolean { - val original = feedback.initialCoverage ?: return false + val fresh = coverage.identity == identity && sourceUnchanged() && + coverage.diagnostics.none { it.code == "coverage.source.stale" } + return compatibleEnvironment(coverage) && fresh && coverage.admittedInvocations == 1 + } + + private fun compatibleEnvironment(coverage: PropertyCoverageArtifact): Boolean { + val original = environment ?: return false val sameBackend = coverage.backendId == original.backendId && coverage.backendVersion == original.backendVersion && coverage.kind == original.kind - val fresh = coverage.identity == identity && captureCoverageIdentity(manifest, roots) == identity && - coverage.diagnostics.none { it.code == "coverage.source.stale" } - val sameRuntime = coverage.provenance == original.provenance && coverage.admittedInvocations == 1 - return sameBackend && fresh && sameRuntime + return sameBackend && coverage.provenance == original.provenance } private fun pendingGoals(): Set = targets.keys - covered @@ -266,6 +327,13 @@ internal class UsvmEdgeGuidance( ) private data class ObservedEdge(val edge: UsvmCoverageEdge, val target: EtsBranchArmTarget, val hits: Long) + private data class NativeEnvironment( + val backendId: String, + val backendVersion: String, + val kind: CoverageArtifactKind, + val provenance: CoverageProvenance, + ) + private data class GoalDistance(val goal: UsvmCoverageEdge, val distance: Int) private data class ReplayDecision( val status: UsvmEdgeReplayStatus, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt index 4f88c78aba..6fd4696415 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt @@ -4,8 +4,9 @@ import org.usvm.ts.pbt.backend.CapabilityDiagnostic import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyId -/** Terminal outcome of one USVM property-violation search. */ +/** Current search outcome; IN_PROGRESS can retain a reached candidate while other paths remain queued. */ enum class UsvmPropertySearchStatus { + IN_PROGRESS, VIOLATION_REACHED, NO_VIOLATION_REACHED, PRECONDITION_REJECTED, @@ -15,6 +16,7 @@ enum class UsvmPropertySearchStatus { UNSUPPORTED, ENGINE_FAILURE, FAILED_INPUT_RESOLUTION, + SOURCE_INVALIDATED, } /** Supported ways in which a mapped predicate can violate its property. */ @@ -46,6 +48,7 @@ data class UsvmPropertySearchResult( require(inputs == null) { "An input-resolution failure cannot contain candidate inputs" } } + UsvmPropertySearchStatus.IN_PROGRESS, UsvmPropertySearchStatus.PROPERTY_ERROR, UsvmPropertySearchStatus.UNSUPPORTED, UsvmPropertySearchStatus.ENGINE_FAILURE, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchSession.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchSession.kt new file mode 100644 index 0000000000..aec3356f13 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchSession.kt @@ -0,0 +1,55 @@ +package org.usvm.ts.pbt.usvm + +import org.usvm.ts.pbt.backend.PropertyCoverageArtifact + +/** Owns one original-property analysis, including its pending queue, completed paths and solver resources. */ +class UsvmPropertySearchSession internal constructor( + advanceSearch: (ULong?) -> UsvmPropertySearchResult, + searchFinished: () -> Boolean, + applyCoverage: (PropertyCoverageArtifact) -> UsvmCoverageUpdateResult, + release: () -> Unit, +) : AutoCloseable { + private var advanceSearch: ((ULong?) -> UsvmPropertySearchResult)? = advanceSearch + private var searchFinished: (() -> Boolean)? = searchFinished + private var applyCoverage: ((PropertyCoverageArtifact) -> UsvmCoverageUpdateResult)? = applyCoverage + private var release: (() -> Unit)? = release + private var advancing = false + + val isFinished: Boolean + get() = searchFinished?.invoke() ?: true + + /** Advances the retained machine; a phase yield reports IN_PROGRESS rather than a completed search. */ + fun advance(maxSteps: ULong? = null): UsvmPropertySearchResult { + val advance = checkNotNull(advanceSearch) { "Property search session is closed" } + check(!advancing) { "Property search session is already advancing" } + + advancing = true + var succeeded = false + try { + val result = advance(maxSteps) + succeeded = true + return result + } finally { + advancing = false + if (!succeeded) close() + } + } + + /** Rejects incompatible evidence without changing the declared predicate or its path constraints. */ + fun applyCoverage(artifact: PropertyCoverageArtifact): UsvmCoverageUpdateResult { + val apply = checkNotNull(applyCoverage) { "Property search session is closed" } + check(!advancing) { "Cannot apply coverage while property search is advancing" } + return apply(artifact) + } + + override fun close() { + check(!advancing) { "Cannot close an advancing property search session" } + val releaseSearch = release ?: return + + advanceSearch = null + searchFinished = null + applyCoverage = null + release = null + releaseSearch() + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt index e768adf824..21eef58458 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt @@ -23,10 +23,14 @@ import org.usvm.ts.pbt.PbtDiagnosticCode import org.usvm.ts.pbt.backend.CapabilityDiagnostic import org.usvm.ts.pbt.backend.ProjectionCapability import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.coverage.captureCoverageIdentity import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.manifest.PropertyManifestJson import org.usvm.ts.pbt.mapping.EtsEntryPointTarget import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact import org.usvm.ts.pbt.model.PropertyId +import java.io.IOException +import java.nio.file.Path /** Searches mapped TypeScript predicates for concrete property violations with USVM. */ class UsvmPropertySearcher( @@ -52,7 +56,20 @@ class UsvmPropertySearcher( mapping: PropertyEtsMappingArtifact, concreteCapability: ProjectionCapability, coverageFeedback: UsvmCoverageFeedback? = null, - ): UsvmPropertySearchResult { + ): UsvmPropertySearchResult = openSession( + manifest = manifest, + mapping = mapping, + concreteCapability = concreteCapability, + coverageFeedback = coverageFeedback, + ).use { session -> session.advance() } + + /** Prepares the declared property once; later advances keep its pending and completed symbolic work. */ + fun openSession( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + coverageFeedback: UsvmCoverageFeedback? = null, + ): UsvmPropertySearchSession { val capability = capabilityResolver.resolve( manifest = manifest, mapping = mapping, @@ -60,15 +77,17 @@ class UsvmPropertySearcher( options = projectionOptions, ) if (capability.symbolic.level == ProjectionLevel.UNSUPPORTED) { - return result( + val unsupported = result( manifest = manifest, status = UsvmPropertySearchStatus.UNSUPPORTED, capability = capability, ) + return completedSession(unsupported) } val predicate = mapping.predicate.exactTargetOrNull() - ?: return result( + if (predicate == null) { + val unavailable = result( manifest = manifest, status = UsvmPropertySearchStatus.ENGINE_FAILURE, capability = capability, @@ -78,35 +97,49 @@ class UsvmPropertySearcher( path = "predicate", ), ) + return completedSession(unavailable) + } + + val pinnedManifest = PropertyManifestJson.decode(PropertyManifestJson.encode(manifest)) val precondition = mapping.precondition?.exactTargetOrNull() val guidedSelectionSupported = !machineOptions.useMerging && !machineOptions.loopIterativeDeepening && machineOptions.loopIterationLimit == null val guidance = coverageFeedback?.let { feedback -> UsvmEdgeGuidance( scene = scene, - manifest = manifest, + manifest = pinnedManifest, mapping = mapping, feedback = feedback, selectionSupported = guidedSelectionSupported, ) } - return executeSearch( - manifest = manifest, + return prepareSession( + manifest = pinnedManifest, predicate = predicate, precondition = precondition, capability = capability, guidance = guidance, - ).copy(edgeGuidance = guidance?.snapshot()) + sourceRoots = mapping.provenance.sourceRoots.map(Path::of), + ) } - private fun executeSearch( + private fun completedSession(result: UsvmPropertySearchResult) = UsvmPropertySearchSession( + advanceSearch = { result }, + searchFinished = { true }, + applyCoverage = { UsvmCoverageUpdateResult(status = UsvmCoverageUpdateStatus.UNSUPPORTED) }, + release = {}, + ) + + private fun prepareSession( manifest: PropertyManifest, predicate: EtsEntryPointTarget, precondition: EtsEntryPointTarget?, capability: UsvmPropertyProjectionCapability, guidance: UsvmEdgeGuidance?, - ): UsvmPropertySearchResult { + sourceRoots: List, + ): UsvmPropertySearchSession { + val identity = captureCoverageIdentity(manifest, sourceRoots) lateinit var projection: UsvmDeclaredDomainProjection val target = UsvmViolationTsTarget() lateinit var observer: UsvmViolationObserver @@ -125,15 +158,17 @@ class UsvmPropertySearcher( val objectShapes = PlainObjectInputShapes(scene, manifest.inputs.map { it.domain }) val domainProjector = UsvmDomainProjector(projectionOptions, objectShapes) - return TsMachine( + val machine = TsMachine( scene = objectShapes.scene, options = machineOptions, tsOptions = tsOptions, machineObserver = observer, deadlineReached = deadlineReached, pathSelectorFactory = guidance?.takeIf { it.selectionSupported }?.let { it::selector }, - ).use { machine -> - val analysis = machine.analyzeWithMetadata( + ) + var prepared = false + val analysis = try { + val retained = machine.openAnalysis( methods = listOf(predicate.method), targets = listOf(target), configureInitialState = { method, state -> @@ -152,34 +187,136 @@ class UsvmPropertySearcher( } }, ) - val violationState = observer.violationStates.firstOrNull { state -> - state.methodResult is TsMethodResult.Success - } ?: observer.violationStates.firstOrNull() - val candidate = violationState?.let { state -> - violationResult( - manifest = manifest, - capability = capability, - violationState = state, - projection = projection, - ) + prepared = true + retained + } finally { + if (!prepared) machine.close() + } + var released = false + var invalidated = false + + fun release() { + if (released) return + + released = true + try { + analysis.close() + } finally { + machine.close() + } + } + + fun invalidateChangedSource(): Boolean { + if (invalidated) return true + + val unchanged = try { + captureCoverageIdentity(manifest, sourceRoots) == identity + } catch (_: IOException) { + false } - val terminalFailure = classifyTerminalFailure( + if (!unchanged) { + invalidated = true + release() + } + return invalidated + } + + return UsvmPropertySearchSession( + advanceSearch = { maxSteps -> + val sourceChanged = invalidateChangedSource() + val result = if (sourceChanged) { + invalidatedSourceResult(manifest, capability) + } else { + val snapshot = analysis.advance(maxSteps) + classifySearchResult( + manifest = manifest, + capability = capability, + analysis = snapshot, + observer = observer, + projection = { projection }, + finished = analysis.isFinished, + ) + } + result.copy(edgeGuidance = guidance?.snapshot()) + }, + searchFinished = { invalidated || analysis.isFinished }, + applyCoverage = { artifact -> + val sourceChanged = invalidateChangedSource() + val update = if (sourceChanged) { + UsvmCoverageUpdateResult(status = UsvmCoverageUpdateStatus.SOURCE_CHANGED) + } else { + guidance?.applyCoverage(artifact) + ?: UsvmCoverageUpdateResult(status = UsvmCoverageUpdateStatus.UNSUPPORTED) + } + if (update.status == UsvmCoverageUpdateStatus.SOURCE_CHANGED) { + invalidated = true + release() + } + update + }, + release = ::release, + ) + } + + private fun invalidatedSourceResult( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + ) = result( + manifest = manifest, + status = UsvmPropertySearchStatus.SOURCE_INVALIDATED, + capability = capability, + additionalDiagnostic = diagnostic( + code = PbtDiagnosticCode.USVM_SESSION_SOURCE_CHANGED, + message = "The original property source changed; the retained analysis cannot continue", + path = "source", + ), + ) + + private fun classifySearchResult( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + analysis: TsMachineAnalysisResult, + observer: UsvmViolationObserver, + projection: () -> UsvmDeclaredDomainProjection, + finished: Boolean, + ): UsvmPropertySearchResult { + val violationState = observer.violationStates.firstOrNull { state -> + state.methodResult is TsMethodResult.Success + } ?: observer.violationStates.firstOrNull() + val candidate = violationState?.let { state -> + violationResult( manifest = manifest, capability = capability, - analysis = analysis, + violationState = state, + projection = projection(), + ) + } + val terminalFailure = classifyTerminalFailure( + manifest = manifest, + capability = capability, + analysis = analysis, + ) + if (!finished) { + val progress = result( + manifest = manifest, + status = UsvmPropertySearchStatus.IN_PROGRESS, + capability = capability, + ).withCandidate(candidate) + return progress.copy( + diagnostics = (progress.diagnostics + terminalFailure?.diagnostics.orEmpty()).distinct(), ) - if (terminalFailure != null) { - return@use terminalFailure.withCandidate(candidate) - } - - candidate - ?: noViolationResult( - manifest = manifest, - capability = capability, - analysis = analysis, - observer = observer, - ) } + if (terminalFailure != null) { + return terminalFailure.withCandidate(candidate) + } + + if (candidate != null) return candidate + return noViolationResult( + manifest = manifest, + capability = capability, + analysis = analysis, + observer = observer, + ) } private fun classifyTerminalFailure(