From 2cf6f119852cf5fba177ed77759960dd6541b014 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 08:17:58 +0300 Subject: [PATCH 1/5] [TS] Compare string values in equality operators Implement supported string equality cases and preserve explicit unsupported outcomes for unbacked symbolic witnesses. Reuse shared Node replay tests. --- .../ts/calls/CurrentTsCallsSymbolicEngine.kt | 15 +- .../main/kotlin/org/usvm/machine/TsMachine.kt | 27 +- .../usvm/machine/interpreter/TsInterpreter.kt | 13 + .../usvm/machine/operator/TsBinaryOperator.kt | 303 ++++++++++++++++-- .../kotlin/org/usvm/machine/state/TsState.kt | 17 + .../org/usvm/machine/TsStringEqualityTest.kt | 277 ++++++++++++++++ .../call/TsUnknownCallDispatcherTest.kt | 33 ++ .../test/resources/models/StringEquality.ts | 58 ++++ 8 files changed, 707 insertions(+), 36 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt create mode 100644 usvm-ts/src/test/resources/models/StringEquality.ts diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt index b7767ed426..69da1df9d2 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt @@ -149,19 +149,29 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine { MachineResult( states = entryObserver.reachedStates, stopReason = outcome.stopReason, + unsupportedPaths = outcome.unsupportedPaths, ) } val states = analysis.states if (states.isEmpty()) { val status = when (analysis.stopReason) { - TsAnalysisStopReason.EXHAUSTED -> CallsSymbolicStatus.UNREACHED + TsAnalysisStopReason.EXHAUSTED -> { + if (analysis.unsupportedPaths.isEmpty()) { + CallsSymbolicStatus.UNREACHED + } else { + CallsSymbolicStatus.UNSUPPORTED + } + } // The machine options above disable every stop condition except the per-target timeout. - TsAnalysisStopReason.STOPPED -> CallsSymbolicStatus.TIMEOUT + TsAnalysisStopReason.STOPPED -> { + CallsSymbolicStatus.TIMEOUT + } } return result( status = status, startedAt = startedAt, + diagnostic = analysis.unsupportedPaths.joinToString().ifEmpty { null }, ) } @@ -284,6 +294,7 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine { private data class MachineResult( val states: List, val stopReason: TsAnalysisStopReason, + val unsupportedPaths: List, ) } 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 5c5d344b3b..ca75767d69 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -49,6 +49,8 @@ enum class TsAnalysisStopReason { data class TsAnalysisResult( val states: List, val stopReason: TsAnalysisStopReason, + /** Reasons for satisfiable paths excluded by an explicit engine model bound. */ + val unsupportedPaths: List, ) class TsMachine( @@ -101,6 +103,7 @@ class TsMachine( ) private val cfgStatistics = CfgStatisticsImpl(graph) + /** Returns supported states only. Call [analyzeWithOutcome] to inspect excluded unsupported paths. */ fun analyze( methods: List, targets: List = emptyList(), @@ -154,6 +157,7 @@ class TsMachine( val observers = mutableListOf>(coverageStatistics) observers.add(statesCollector) + val unsupportedPaths = mutableSetOf() if (tsOptions.enableVisualization) { observers += TsStateVisualizer() @@ -202,10 +206,25 @@ class TsMachine( ) } + val supportedObserver = CompositeUMachineObserver(observers) + val outcomeObserver = object : UMachineObserver by supportedObserver { + override fun onStateTerminated(state: TsState, stateReachable: Boolean) { + val unsupportedReason = state.unsupportedReason + if (unsupportedReason != null) { + if (stateReachable) { + unsupportedPaths += unsupportedReason + } + return + } + + supportedObserver.onStateTerminated(state, stateReachable) + } + } + run( interpreter, pathSelector, - observer = CompositeUMachineObserver(observers), + observer = outcomeObserver, isStateTerminated = { state -> state.callStack.isEmpty() }, stopStrategy = stopStrategy ) @@ -216,7 +235,11 @@ class TsMachine( TsAnalysisStopReason.STOPPED } - return TsAnalysisResult(states = statesCollector.collectedStates, stopReason = stopReason) + return TsAnalysisResult( + states = statesCollector.collectedStates, + stopReason = stopReason, + unsupportedPaths = unsupportedPaths.toList(), + ) } override fun close() { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index e69a972c17..b15e04d2b1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -151,6 +151,18 @@ class TsInterpreter( } } } + } catch (e: UnsupportedOperationException) { + if (throwExceptionOnStepFailure) { + throw e + } + + val reason = e.message?.takeIf(String::isNotBlank) ?: "Unsupported TypeScript operation" + state.terminateAsUnsupported(reason) + + return StepResult( + forkedStates = scope.stepResult().forkedStates, + originalStateAlive = true, + ) } catch (e: Exception) { if (throwExceptionOnStepFailure) { throw e @@ -826,6 +838,7 @@ class TsInterpreter( val length = state.memory.read(lengthLValue).asExpr(sizeSort) state.pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) state.pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)) + state.boundedStringBackingRefs += ref } val parameterSort = typeToSort(parameterType) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 9e4e1db477..03f28f177a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -4,23 +4,159 @@ import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr import io.ksmt.utils.cast import mu.KotlinLogging +import org.jacodb.ets.model.EtsStringType import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UBoolSort +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.UIteExpr import org.usvm.USort +import org.usvm.api.evalTypeEquals +import org.usvm.isFalse +import org.usvm.isTrue import org.usvm.machine.TsContext +import org.usvm.machine.TsSizeSort import org.usvm.machine.expr.mkNumericExpr import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.ExprWithTypeConstraint import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.util.boolToFp +import org.usvm.util.mkFieldLValue +import org.usvm.util.mkStringBackingElementLValue +import org.usvm.util.mkStringBackingLengthLValue private val logger = KotlinLogging.logger {} +/** Strings are primitive values even though the TS heap stores their UTF-16 contents behind references. */ +private fun TsContext.stringValueEquals( + lhs: UHeapRef, + rhs: UHeapRef, + sameReference: UBoolExpr, + activeGuard: UBoolExpr, + scope: TsStepScope, +): UBoolExpr? { + val lhsConstant = (lhs as? UConcreteHeapRef)?.let(::getStringConstantValue) + val rhsConstant = (rhs as? UConcreteHeapRef)?.let(::getStringConstantValue) + if (lhsConstant != null && rhsConstant != null) { + return if (lhsConstant == rhsConstant) trueExpr else falseExpr + } + + val (lhsIsString, rhsIsString) = scope.calcOnState { + memory.types.evalTypeEquals(lhs, EtsStringType) to memory.types.evalTypeEquals(rhs, EtsStringType) + } + if (lhsIsString.isFalse || rhsIsString.isFalse) return falseExpr + + val bothStrings = mkAnd(lhsIsString, rhsIsString) + val missingBacking = scope.calcOnState { + (lhsConstant == null && lhs !in boundedStringBackingRefs) || + (rhsConstant == null && rhs !in boundedStringBackingRefs) + } + // An alias of a known literal has that literal's value without reading a symbolic backing array. + val knownLiteralAlias = if (lhsConstant != null || rhsConstant != null) sameReference else falseExpr + val notBothStrings = mkNot(bothStrings) + val lhsNullish = mkOr(mkHeapRefEq(lhs, mkTsNullValue()), mkHeapRefEq(lhs, mkUndefinedValue())) + val rhsNullish = mkOr(mkHeapRefEq(rhs, mkTsNullValue()), mkHeapRefEq(rhs, mkUndefinedValue())) + if (missingBacking) { + val supportedWithoutBacking = mkOr( + mkNot(activeGuard), + knownLiteralAlias, + lhsNullish, + rhsNullish, + notBothStrings, + ) + scope.fork(supportedWithoutBacking, blockOnFalseState = { + terminateAsUnsupported(reason = "String equality needs a modeled string backing for dynamic references") + }) ?: return null + return falseExpr + } + + val comparison = scope.calcOnState { + val lhsChars = memory.read(mkFieldLValue(addressSort, lhs, field = "value")) + val rhsChars = memory.read(mkFieldLValue(addressSort, rhs, field = "value")) + val lhsLength = memory.read(mkStringBackingLengthLValue(lhsChars)) + val rhsLength = memory.read(mkStringBackingLengthLValue(rhsChars)) + + StringComparisonData( + lhsChars = lhsChars, + rhsChars = rhsChars, + lhsLength = lhsLength, + rhsLength = rhsLength, + maxLength = maxStringLength, + ) + } + + val zero = mkBv(0) + val maximum = mkBv(comparison.maxLength) + val boundedLengths = mkAnd( + if (lhsConstant == null) { + mkAnd( + mkBvSignedGreaterOrEqualExpr(comparison.lhsLength, zero), + mkBvSignedLessOrEqualExpr(comparison.lhsLength, maximum), + ) + } else { + trueExpr + }, + if (rhsConstant == null) { + mkAnd( + mkBvSignedGreaterOrEqualExpr(comparison.rhsLength, zero), + mkBvSignedLessOrEqualExpr(comparison.rhsLength, maximum), + ) + } else { + trueExpr + }, + ) + val supported = mkOr( + mkNot(activeGuard), + knownLiteralAlias, + lhsNullish, + rhsNullish, + notBothStrings, + boundedLengths, + ) + scope.fork(supported, blockOnFalseState = { + terminateAsUnsupported(reason = "String equality requires symbolic string length in 0..$maxStringLength") + }) ?: return null + + // Known literals supply a tighter comparison bound; all other string lengths are constrained above. + val comparisonLength = lhsConstant?.length ?: rhsConstant?.length ?: comparison.maxLength + val equalCharacters = (0 until comparisonLength).map { index -> + val position = mkBv(index) + val lhsCharacter = scope.calcOnState { + memory.read(mkStringBackingElementLValue(comparison.lhsChars, position)) + } + val rhsCharacter = scope.calcOnState { + memory.read(mkStringBackingElementLValue(comparison.rhsChars, position)) + } + mkImplies(mkBvSignedLessExpr(position, comparison.lhsLength), mkEq(lhsCharacter, rhsCharacter)) + } + + return mkAnd(lhsIsString, rhsIsString, mkEq(comparison.lhsLength, comparison.rhsLength), mkAnd(equalCharacters)) +} + +private data class StringComparisonData( + val lhsChars: UHeapRef, + val rhsChars: UHeapRef, + val lhsLength: UExpr, + val rhsLength: UExpr, + val maxLength: Int, +) + +private fun TsContext.referenceOrStringValueEquals( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + activeGuard: UBoolExpr = trueExpr, +): UBoolExpr? { + val sameReference = mkHeapRefEq(lhs, rhs) + if (sameReference.isTrue) return trueExpr + + val equalStringValues = stringValueEquals(lhs, rhs, sameReference, activeGuard, scope) ?: return null + return mkOr(sameReference, equalStringValues) +} + sealed interface TsBinaryOperator { fun TsContext.onBool( @@ -41,12 +177,26 @@ sealed interface TsBinaryOperator { scope: TsStepScope, ): UExpr<*>? + fun TsContext.onRefWithGuard( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UExpr<*>? = onRef(lhs, rhs, scope) + fun TsContext.resolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, ): UExpr<*>? + fun TsContext.resolveFakeObjectWithGuard( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UExpr<*>? = resolveFakeObject(lhs, rhs, scope) + fun TsContext.internalResolve( lhs: UExpr<*>, rhs: UExpr<*>, @@ -57,10 +207,13 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, + activeGuard: UBoolExpr = trueExpr, ): UExpr<*>? { if (lhs is UIteExpr<*>) { - val trueBranch = resolve(lhs.trueBranch, rhs, scope) ?: return null - val falseBranch = resolve(lhs.falseBranch, rhs, scope) ?: return null + val trueBranchGuard = mkAnd(activeGuard, lhs.condition) + val falseBranchGuard = mkAnd(activeGuard, mkNot(lhs.condition)) + val trueBranch = resolve(lhs.trueBranch, rhs, scope, trueBranchGuard) ?: return null + val falseBranch = resolve(lhs.falseBranch, rhs, scope, falseBranchGuard) ?: return null return lhs.ctx.mkIte( lhs.condition, trueBranch.asExpr(falseBranch.sort), @@ -69,8 +222,10 @@ sealed interface TsBinaryOperator { } if (rhs is UIteExpr<*>) { - val trueBranch = resolve(lhs, rhs.trueBranch, scope) ?: return null - val falseBranch = resolve(lhs, rhs.falseBranch, scope) ?: return null + val trueBranchGuard = mkAnd(activeGuard, rhs.condition) + val falseBranchGuard = mkAnd(activeGuard, mkNot(rhs.condition)) + val trueBranch = resolve(lhs, rhs.trueBranch, scope, trueBranchGuard) ?: return null + val falseBranch = resolve(lhs, rhs.falseBranch, scope, falseBranchGuard) ?: return null return lhs.ctx.mkIte( rhs.condition, trueBranch.asExpr(falseBranch.sort), @@ -82,7 +237,7 @@ sealed interface TsBinaryOperator { val rhsValue = rhs.extractSingleValueFromFakeObjectOrNull(scope) ?: rhs if (lhsValue.isFakeObject() || rhsValue.isFakeObject()) { - return resolveFakeObject(lhsValue, rhsValue, scope) + return resolveFakeObjectWithGuard(lhsValue, rhsValue, scope, activeGuard) } val lhsSort = lhsValue.sort @@ -90,7 +245,12 @@ sealed interface TsBinaryOperator { return when (lhsSort) { boolSort -> onBool(lhsValue.asExpr(boolSort), rhsValue.asExpr(boolSort), scope) fp64Sort -> onFp(lhsValue.asExpr(fp64Sort), rhsValue.asExpr(fp64Sort), scope) - addressSort -> onRef(lhsValue.asExpr(addressSort), rhsValue.asExpr(addressSort), scope) + addressSort -> onRefWithGuard( + lhsValue.asExpr(addressSort), + rhsValue.asExpr(addressSort), + scope, + activeGuard, + ) else -> TODO("Unsupported sort $lhsSort") } } @@ -98,11 +258,13 @@ sealed interface TsBinaryOperator { return internalResolve(lhsValue, rhsValue, scope) } + @Suppress("LongMethod") fun TsContext.commonResolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, resultSort: R, + activeGuard: UBoolExpr = trueExpr, reduce: (List>) -> UExpr, ): UExpr? { check(lhs.isFakeObject() || rhs.isFakeObject()) @@ -180,9 +342,10 @@ sealed interface TsBinaryOperator { ) // fake(ref) + fake(ref) - val refRefExpr = onRef(lhsRef, rhsRef, scope)?.asExpr(resultSort) ?: return null + val refRefGuard = mkAnd(activeGuard, lhsType.refTypeExpr, rhsType.refTypeExpr) + val refRefExpr = onRefWithGuard(lhsRef, rhsRef, scope, refRefGuard)?.asExpr(resultSort) ?: return null conjuncts += ExprWithTypeConstraint( - constraint = mkAnd(lhsType.refTypeExpr, rhsType.refTypeExpr), + constraint = refRefGuard, expr = refRefExpr ) } @@ -259,7 +422,12 @@ sealed interface TsBinaryOperator { ) // fake(ref) + ref - val refRefExpr = onRef(lhsRef, rhsRef, scope)?.asExpr(resultSort) ?: return null + val refRefExpr = onRefWithGuard( + lhsRef, + rhsRef, + scope, + mkAnd(activeGuard, lhsType.refTypeExpr), + )?.asExpr(resultSort) ?: return null conjuncts += ExprWithTypeConstraint( constraint = lhsType.refTypeExpr, expr = refRefExpr @@ -344,7 +512,12 @@ sealed interface TsBinaryOperator { ) // ref + fake(ref) - val refRefExpr = onRef(lhsRef, rhsRef, scope)?.asExpr(resultSort) ?: return null + val refRefExpr = onRefWithGuard( + lhsRef, + rhsRef, + scope, + mkAnd(activeGuard, rhsType.refTypeExpr), + )?.asExpr(resultSort) ?: return null conjuncts += ExprWithTypeConstraint( constraint = rhsType.refTypeExpr, expr = refRefExpr @@ -383,16 +556,24 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UBoolExpr { + ): UBoolExpr? = onRefWithGuard(lhs, rhs, scope, trueExpr) + + override fun TsContext.onRefWithGuard( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UBoolExpr? { // Note: in JavaScript, `null == undefined` val lhsIsNull = mkEq(lhs, mkTsNullValue()) val rhsIsNull = mkEq(rhs, mkTsNullValue()) val lhsIsUndefined = mkEq(lhs, mkUndefinedValue()) val rhsIsUndefined = mkEq(rhs, mkUndefinedValue()) + val referenceEquality = referenceOrStringValueEquals(lhs, rhs, scope, activeGuard) ?: return null return mkOr( mkAnd(lhsIsUndefined, rhsIsNull), mkAnd(lhsIsNull, rhsIsUndefined), - mkHeapRefEq(lhs, rhs) + referenceEquality, ) } @@ -400,21 +581,28 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UBoolExpr { + ): UBoolExpr? = resolveFakeObjectWithGuard(lhs, rhs, scope, trueExpr) + + override fun TsContext.resolveFakeObjectWithGuard( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UBoolExpr? { return commonResolveFakeObject( lhs, rhs, scope, - boolSort + boolSort, + activeGuard, ) { conjuncts -> mkAnd(conjuncts.map { (condition, value) -> mkImplies(condition, value) }) } - ?: error("Should not be null") } override fun TsContext.internalResolve( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UBoolExpr { + ): UBoolExpr? { check(!lhs.isFakeObject() && !rhs.isFakeObject()) // bool == bool @@ -508,29 +696,47 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { return with(Eq) { - onRef(lhs, rhs, scope).not() + onRef(lhs, rhs, scope)?.not() } } + override fun TsContext.onRefWithGuard( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UExpr<*>? = with(Eq) { + onRefWithGuard(lhs, rhs, scope, activeGuard)?.not() + } + override fun TsContext.resolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { return with(Eq) { - resolveFakeObject(lhs, rhs, scope).not() + resolveFakeObject(lhs, rhs, scope)?.not() } } + override fun TsContext.resolveFakeObjectWithGuard( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UExpr<*>? = with(Eq) { + resolveFakeObjectWithGuard(lhs, rhs, scope, activeGuard)?.not() + } + override fun TsContext.internalResolve( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { return with(Eq) { - internalResolve(lhs, rhs, scope).not() + internalResolve(lhs, rhs, scope)?.not() } } } @@ -556,15 +762,27 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UBoolExpr { - return mkHeapRefEq(lhs, rhs) - } + ): UBoolExpr? = onRefWithGuard(lhs, rhs, scope, trueExpr) + + override fun TsContext.onRefWithGuard( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UBoolExpr? = referenceOrStringValueEquals(lhs, rhs, scope, activeGuard) override fun TsContext.resolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UBoolExpr { + ): UBoolExpr? = resolveFakeObjectWithGuard(lhs, rhs, scope, trueExpr) + + override fun TsContext.resolveFakeObjectWithGuard( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UBoolExpr? { check(lhs.isFakeObject() || rhs.isFakeObject()) var lhsValue: UExpr<*> = lhs @@ -643,14 +861,17 @@ sealed interface TsBinaryOperator { if (lhsValue.sort == addressSort && rhsValue.sort == addressSort) { val left = lhsValue.asExpr(addressSort) val right = rhsValue.asExpr(addressSort) + val lhsRefGuard = if (lhs.isFakeObject()) lhs.getFakeType(scope).refTypeExpr else trueExpr + val rhsRefGuard = if (rhs.isFakeObject()) rhs.getFakeType(scope).refTypeExpr else trueExpr + val refComparisonGuard = mkAnd(activeGuard, typeConstraint, lhsRefGuard, rhsRefGuard) return mkAnd( typeConstraint, - mkHeapRefEq(left, right) + onRefWithGuard(left, right, scope, refComparisonGuard) ?: return null ) } val looseEqualityConstraint = with(Eq) { - resolve(lhsValue, rhsValue, scope)?.asExpr(boolSort) ?: error("Should not be encountered") + resolve(lhsValue, rhsValue, scope, activeGuard)?.asExpr(boolSort) ?: return null } return mkAnd(typeConstraint, looseEqualityConstraint) @@ -693,22 +914,40 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UBoolExpr { + ): UBoolExpr? { return with(StrictEq) { - onRef(lhs, rhs, scope).not() + onRef(lhs, rhs, scope)?.not() } } + override fun TsContext.onRefWithGuard( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UBoolExpr? = with(StrictEq) { + onRefWithGuard(lhs, rhs, scope, activeGuard)?.not() + } + override fun TsContext.resolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UBoolExpr { + ): UBoolExpr? { return with(StrictEq) { - resolveFakeObject(lhs, rhs, scope).not() + resolveFakeObject(lhs, rhs, scope)?.not() } } + override fun TsContext.resolveFakeObjectWithGuard( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UBoolExpr? = with(StrictEq) { + resolveFakeObjectWithGuard(lhs, rhs, scope, activeGuard)?.not() + } + override fun TsContext.internalResolve( lhs: UExpr<*>, rhs: UExpr<*>, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 1c753d2e83..4dd9f42851 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -81,6 +81,13 @@ class TsState( * for identical string values. */ var stringConstantAllocatedRefs: UPersistentHashMap = persistentHashMapOf(), + /** + * References whose string backing and length bound have been modeled. + * A new symbolic string producer must register its reference here after creating the backing model. + * String literals are recognized separately through [TsContext.getStringConstantValue]. + */ + var boundedStringBackingRefs: Set = emptySet(), + var unsupportedReason: String? = null, private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( ctx = ctx, @@ -93,6 +100,14 @@ class TsState( forkPoints = forkPoints, targets = targets, ) { + /** Terminates a satisfiable path that the TypeScript model cannot execute soundly. */ + fun terminateAsUnsupported(reason: String) { + require(reason.isNotBlank()) + + unsupportedReason = reason + while (callStack.isNotEmpty()) callStack.pop() + } + fun getSortForLocal(idx: Int): USort? { val localToSort = localToSortStack.last() return localToSort[idx] @@ -308,6 +323,8 @@ class TsState( dfltObject = dfltObject, dfltObjectFieldSorts = dfltObjectFieldSorts, stringConstantAllocatedRefs = stringConstantAllocatedRefs, + boundedStringBackingRefs = boundedStringBackingRefs, + unsupportedReason = unsupportedReason, activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt new file mode 100644 index 0000000000..bf81ad5717 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt @@ -0,0 +1,277 @@ +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.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsTestResolver +import org.usvm.util.TsUnsupportedWitnessException +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.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsStringEqualityTest { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/StringEquality.ts") + private val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + private val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + throwExceptionOnStepFailure = true, + ) + + @Test + fun `string equality and inequality produce replayable witnesses`() { + val expected = mapOf) -> Int>( + "equalsA" to { args -> if (args[0] == "a") 1 else 2 }, + "notEqualsA" to { args -> if (args[0] != "a") 1 else 2 }, + "equalsEmpty" to { args -> if (args[0].isEmpty()) 1 else 2 }, + "equalsUnicode" to { args -> if (args[0] == "\uD83D\uDE00") 1 else 2 }, + "equalsOther" to { args -> if (args[0] == args[1]) 1 else 2 }, + "equalsAtLengthOne" to { args -> + if (args[0].length != 1 || args[1].length != 1) 3 else if (args[0] == args[1]) 1 else 2 + }, + "looselyEqualsOther" to { args -> if (args[0] == args[1]) 1 else 2 }, + "looselyNotEqualsOther" to { args -> if (args[0] != args[1]) 1 else 2 }, + ) + val tests = expected.mapValues { (name, _) -> analyze(name) } + + tests.forEach { (name, generated) -> + val expectedResults = if (name == "equalsAtLengthOne") setOf(1, 2, 3) else setOf(1, 2) + assertEquals(expectedResults, generated.map { resultNumber(it) }.toSet(), name) + generated.forEach { test -> + val inputs = test.before.parameters.map { assertIs(it).value } + assertEquals(expected.getValue(name)(inputs), resultNumber(test), "$name: $test") + } + } + + replay(tests) + } + + @Test + fun `null and undefined strict and loose equality remain distinct`() { + val tests = mapOf("nullAndUndefined" to analyze("nullAndUndefined")) + + assertEquals(setOf(2), tests.getValue("nullAndUndefined").map(::resultNumber).toSet()) + + replay(tests) + } + + @Test + fun `default string bound can compare two symbolic inputs`() { + val tests = analyze("equalsOther", maxStringLength = 1_000) + + assertEquals(setOf(1, 2), tests.map(::resultNumber).toSet()) + + replay(mapOf("equalsOther" to tests)) + } + + @Test + fun `any and unknown string alternatives are explicit unsupported paths`() { + val generated = listOf("equalsAnyStrings", "equalsUnknownStrings").associateWith { name -> + val method = scene.projectClasses.single { it.name == "StringEquality" } + .methods + .single { it.name == name } + val analysis = TsMachine( + scene, + options = options.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), + tsOptions = TsOptions(maxArraySize = 4), + ).use { machine -> + machine.analyzeWithOutcome(listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason, name) + assertTrue(analysis.unsupportedPaths.any { "modeled string backing" in it }, name) + val tests = analysis.states.map { state -> TsTestResolver().resolve(method, state) } + assertTrue(tests.isNotEmpty(), name) + assertTrue(tests.all { resultNumber(it) == 3 }, "$name: $tests") + + tests + } + + replayDynamic(generated) + replayLongMismatch() + + val method = scene.projectClasses.single { it.name == "StringEquality" } + .methods + .single { it.name == "equalsAnyStrings" } + val ordinaryStates = TsMachine( + scene, + options = options, + tsOptions = TsOptions(maxArraySize = 4), + ).use { machine -> + machine.analyze(listOf(method)) + } + val ordinaryTests = ordinaryStates.map { state -> TsTestResolver().resolve(method, state) } + assertTrue(ordinaryTests.none { resultNumber(it) in setOf(1, 2) }) + } + + @Test + fun `two unmodeled string references do not yield equality witnesses`() { + val method = scene.projectClasses.single { it.name == "StringEquality" } + .methods + .single { it.name == "looselyEqualsDynamicStrings" } + val analysis = TsMachine( + scene, + options = options.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), + tsOptions = TsOptions(maxArraySize = 4), + ).use { machine -> + machine.analyzeWithOutcome(listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.any { "modeled string backing" in it }) + val unsupportedWitnesses = mutableListOf() + val tests = analysis.states.mapNotNull { state -> + try { + TsTestResolver().resolve(method, state) + } catch (failure: TsUnsupportedWitnessException) { + unsupportedWitnesses += failure + null + } + } + + assertTrue(unsupportedWitnesses.isNotEmpty(), "Expected an unbacked string witness") + assertTrue(unsupportedWitnesses.all { "missing backing array" in it.message.orEmpty() }) + assertTrue(tests.none { resultNumber(it) in setOf(1, 2) }, "$tests") + } + + @Test + fun `unsupported fork does not consume covered-new slot or stop before supported result`() { + val method = scene.projectClasses.single { it.name == "StringEquality" } + .methods + .single { it.name == "equalsAnyDirect" } + val analysis = TsMachine( + scene, + options = options.copy(collectedStatesLimit = 1), + tsOptions = TsOptions(maxArraySize = 4), + ).use { machine -> + machine.analyzeWithOutcome(listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.any { "modeled string backing" in it }) + val tests = analysis.states.map { state -> TsTestResolver().resolve(method, state) } + val supported = tests.filter { test -> + test.before.parameters[0] !is TsTestValue.TsString && resultNumber(test) == 2 + } + assertTrue(supported.isNotEmpty(), "$tests") + + replayDynamic(mapOf("equalsAnyDirect" to supported)) + } + + private fun analyze(name: String, maxStringLength: Int = 4): List { + val method = scene.projectClasses.single { it.name == "StringEquality" } + .methods + .single { it.name == name } + val analysis = TsMachine( + scene, + options = options, + tsOptions = TsOptions(maxArraySize = maxStringLength), + ).use { machine -> + machine.analyzeWithOutcome(listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason, name) + assertTrue(analysis.states.isNotEmpty(), name) + assertTrue(analysis.states.all { it.methodResult is TsMethodResult.Success }, name) + + return analysis.states.map { state -> TsTestResolver().resolve(method, state) } + } + + private fun resultNumber(test: TsTest): Int = + assertIs(test.returnValue).number.toInt() + + private fun replay(tests: Map>) { + val script = buildString { + appendLine(source.readText()) + tests.forEach { (name, generated) -> + generated.forEachIndexed { index, test -> + val args = test.before.parameters.joinToString { value -> + jsString(assertIs(value).value) + } + val expected = resultNumber(test) + + appendLine("if (new StringEquality().$name($args) !== $expected) {") + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "string-equality", + timeoutMessage = "Node replay timed out", + ) + } + + private fun replayDynamic(tests: Map>) { + val script = buildString { + appendLine(source.readText()) + tests.forEach { (name, generated) -> + generated.forEachIndexed { index, test -> + val left = jsDynamic(test.before.parameters[0]) + val right = jsString(assertIs(test.before.parameters[1]).value) + + appendLine("if (new StringEquality().$name($left, $right) !== ${resultNumber(test)}) {") + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "dynamic-string-equality", + timeoutMessage = "Node replay timed out", + ) + } + + private fun jsDynamic(value: TsTestValue): String = when (value) { + is TsTestValue.TsBoolean -> value.value.toString() + is TsTestValue.TsNumber -> value.number.toString() + TsTestValue.TsNull -> "null" + TsTestValue.TsUndefined -> "undefined" + is TsTestValue.TsClass -> "{}" + is TsTestValue.TsArray<*> -> "[]" + else -> error("Unexpected string alternative: $value") + } + + private fun replayLongMismatch() { + val script = buildString { + appendLine(source.readText()) + appendLine("const left = 'a'.repeat(4) + 'x';") + appendLine("const right = 'a'.repeat(4) + 'y';") + appendLine("if (new StringEquality().equalsAnyStrings(left, right) !== 2) throw Error('long any');") + appendLine("if (new StringEquality().equalsUnknownStrings(left, right) !== 2) throw Error('long unknown');") + } + + assertNodeReplay( + source = script, + directory = directory, + name = "long-string-equality", + timeoutMessage = "Node replay timed out", + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt index 4abb82bb0b..083104b732 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt @@ -28,6 +28,7 @@ import org.usvm.UMachineOptions import org.usvm.api.targets.ReachabilityObserver import org.usvm.api.targets.TsReachabilityTarget import org.usvm.isTrue +import org.usvm.machine.TsAnalysisStopReason import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions @@ -52,6 +53,38 @@ class TsUnknownCallDispatcherTest { ) private val fullScene = EtsScene(listOf(sourceFile)) + @Test + fun `unsupported model exception is reported without a successful state`() { + val method = method(fullScene, "declaredMethodWithoutBodyContinues") + val dispatcher = TsUnknownCallDispatcher { _, _ -> + throw UnsupportedOperationException("The call model is not implemented") + } + + val outcome = TsMachine( + scene = fullScene, + options = allStatesMachineOptions, + tsOptions = TsOptions(), + unknownCallDispatcher = dispatcher, + ).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertEquals(listOf("The call model is not implemented"), outcome.unsupportedPaths) + + assertFailsWith { + TsMachine( + scene = fullScene, + options = allStatesMachineOptions.copy(throwExceptionOnStepFailure = true), + tsOptions = TsOptions(), + unknownCallDispatcher = dispatcher, + ).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + } + } + @Test fun `every model or fallback decision is reported through the interpreter observer`() { val cases = listOf( diff --git a/usvm-ts/src/test/resources/models/StringEquality.ts b/usvm-ts/src/test/resources/models/StringEquality.ts new file mode 100644 index 0000000000..b861925d4f --- /dev/null +++ b/usvm-ts/src/test/resources/models/StringEquality.ts @@ -0,0 +1,58 @@ +class StringEquality { + equalsA(value: string): number { + return value === "a" ? 1 : 2; + } + + notEqualsA(value: string): number { + return value !== "a" ? 1 : 2; + } + + equalsEmpty(value: string): number { + return value === "" ? 1 : 2; + } + + equalsUnicode(value: string): number { + return value === "\uD83D\uDE00" ? 1 : 2; + } + + equalsOther(left: string, right: string): number { + return left === right ? 1 : 2; + } + + equalsAtLengthOne(left: string, right: string): number { + if (left.length !== 1 || right.length !== 1) return 3; + + return left === right ? 1 : 2; + } + + looselyEqualsOther(left: string, right: string): number { + return left == right ? 1 : 2; + } + + looselyNotEqualsOther(left: string, right: string): number { + return left != right ? 1 : 2; + } + + equalsAnyStrings(left: any, right: string): number { + if (typeof left !== "string") return 3; + return left === right ? 1 : 2; + } + + equalsUnknownStrings(left: unknown, right: string): number { + if (typeof left !== "string") return 3; + return left === right ? 1 : 2; + } + + equalsAnyDirect(left: any, right: string): number { + return left === right ? 1 : 2; + } + + looselyEqualsDynamicStrings(left: any, right: any): number { + if (typeof left !== "string" || typeof right !== "string") return 3; + return left == right ? 1 : 2; + } + + nullAndUndefined(): number { + return null === undefined ? 1 : null == undefined ? 2 : 3; + } +} From d04804680a325dcb483f3085681c362a481b1329 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 4 Oct 2026 01:00:47 +0300 Subject: [PATCH 2/5] [TS] Check string equality through discoverProperties --- .../org/usvm/machine/TsStringEqualityTest.kt | 59 ++++++++++++++++--- 1 file changed, 51 insertions(+), 8 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt index bf81ad5717..a559ed3107 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt @@ -12,6 +12,7 @@ import org.usvm.UMachineOptions import org.usvm.api.TsTest import org.usvm.api.TsTestValue import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsMethodTestRunner import org.usvm.util.TsTestResolver import org.usvm.util.TsUnsupportedWitnessException import org.usvm.util.assertNodeReplay @@ -24,13 +25,13 @@ import kotlin.test.assertIs import kotlin.test.assertTrue import kotlin.time.Duration -class TsStringEqualityTest { +class TsStringEqualityTest : TsMethodTestRunner() { @TempDir lateinit var directory: Path private val source = getResourcePath("/models/StringEquality.ts") - private val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) - private val options = UMachineOptions( + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + private val analysisOptions = UMachineOptions( pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), solverType = SolverType.YICES, solverTimeout = Duration.INFINITE, @@ -52,6 +53,36 @@ class TsStringEqualityTest { "looselyEqualsOther" to { args -> if (args[0] == args[1]) 1 else 2 }, "looselyNotEqualsOther" to { args -> if (args[0] != args[1]) 1 else 2 }, ) + + expected.forEach { (name, expectedResult) -> + val method = getMethod(methodName = name, className = "StringEquality") + if (name == "equalsOther" || name == "equalsAtLengthOne" || + name == "looselyEqualsOther" || name == "looselyNotEqualsOther") { + val results = if (name == "equalsAtLengthOne") listOf(1, 2, 3) else listOf(1, 2) + discoverProperties( + method = method, + *results.map { expectedNumber -> + { left: TsTestValue.TsString, right: TsTestValue.TsString, result: TsTestValue.TsNumber -> + result.number == expectedNumber.toDouble() && + result.number == expectedResult(listOf(left.value, right.value)).toDouble() + } + }.toTypedArray(), + invariants = arrayOf({ left, right, result -> + result.number == expectedResult(listOf(left.value, right.value)).toDouble() + }), + ) + } else { + discoverProperties( + method = method, + { input, result -> result.number == 1.0 && expectedResult(listOf(input.value)) == 1 }, + { input, result -> result.number == 2.0 && expectedResult(listOf(input.value)) == 2 }, + invariants = arrayOf({ input, result -> + result.number == expectedResult(listOf(input.value)).toDouble() + }), + ) + } + } + val tests = expected.mapValues { (name, _) -> analyze(name) } tests.forEach { (name, generated) -> @@ -68,6 +99,12 @@ class TsStringEqualityTest { @Test fun `null and undefined strict and loose equality remain distinct`() { + discoverProperties( + method = getMethod(methodName = "nullAndUndefined", className = "StringEquality"), + { result -> result.number == 2.0 }, + invariants = arrayOf({ result -> result.number == 2.0 }), + ) + val tests = mapOf("nullAndUndefined" to analyze("nullAndUndefined")) assertEquals(setOf(2), tests.getValue("nullAndUndefined").map(::resultNumber).toSet()) @@ -77,6 +114,12 @@ class TsStringEqualityTest { @Test fun `default string bound can compare two symbolic inputs`() { + discoverProperties( + method = getMethod(methodName = "equalsOther", className = "StringEquality"), + { left, right, result -> left.value == right.value && result.number == 1.0 }, + { left, right, result -> left.value != right.value && result.number == 2.0 }, + ) + val tests = analyze("equalsOther", maxStringLength = 1_000) assertEquals(setOf(1, 2), tests.map(::resultNumber).toSet()) @@ -92,7 +135,7 @@ class TsStringEqualityTest { .single { it.name == name } val analysis = TsMachine( scene, - options = options.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), + options = analysisOptions.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), tsOptions = TsOptions(maxArraySize = 4), ).use { machine -> machine.analyzeWithOutcome(listOf(method)) @@ -115,7 +158,7 @@ class TsStringEqualityTest { .single { it.name == "equalsAnyStrings" } val ordinaryStates = TsMachine( scene, - options = options, + options = analysisOptions, tsOptions = TsOptions(maxArraySize = 4), ).use { machine -> machine.analyze(listOf(method)) @@ -131,7 +174,7 @@ class TsStringEqualityTest { .single { it.name == "looselyEqualsDynamicStrings" } val analysis = TsMachine( scene, - options = options.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), + options = analysisOptions.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), tsOptions = TsOptions(maxArraySize = 4), ).use { machine -> machine.analyzeWithOutcome(listOf(method)) @@ -161,7 +204,7 @@ class TsStringEqualityTest { .single { it.name == "equalsAnyDirect" } val analysis = TsMachine( scene, - options = options.copy(collectedStatesLimit = 1), + options = analysisOptions.copy(collectedStatesLimit = 1), tsOptions = TsOptions(maxArraySize = 4), ).use { machine -> machine.analyzeWithOutcome(listOf(method)) @@ -184,7 +227,7 @@ class TsStringEqualityTest { .single { it.name == name } val analysis = TsMachine( scene, - options = options, + options = analysisOptions, tsOptions = TsOptions(maxArraySize = maxStringLength), ).use { machine -> machine.analyzeWithOutcome(listOf(method)) From 4c2a89ed3dd15cacb1008a2200eba015ea463449 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 4 Oct 2026 01:31:28 +0300 Subject: [PATCH 3/5] [TS] Format discoverProperties string equality checks --- .../org/usvm/machine/TsStringEqualityTest.kt | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt index a559ed3107..6b65a64be0 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt @@ -54,15 +54,26 @@ class TsStringEqualityTest : TsMethodTestRunner() { "looselyNotEqualsOther" to { args -> if (args[0] != args[1]) 1 else 2 }, ) + val twoParameterMethods = setOf( + "equalsOther", + "equalsAtLengthOne", + "looselyEqualsOther", + "looselyNotEqualsOther", + ) + expected.forEach { (name, expectedResult) -> val method = getMethod(methodName = name, className = "StringEquality") - if (name == "equalsOther" || name == "equalsAtLengthOne" || - name == "looselyEqualsOther" || name == "looselyNotEqualsOther") { + + if (name in twoParameterMethods) { val results = if (name == "equalsAtLengthOne") listOf(1, 2, 3) else listOf(1, 2) discoverProperties( method = method, *results.map { expectedNumber -> - { left: TsTestValue.TsString, right: TsTestValue.TsString, result: TsTestValue.TsNumber -> + { + left: TsTestValue.TsString, + right: TsTestValue.TsString, + result: TsTestValue.TsNumber, + -> result.number == expectedNumber.toDouble() && result.number == expectedResult(listOf(left.value, right.value)).toDouble() } From 9fb0e2d88d587325850d73144c5a0d1e7c51f980 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 4 Oct 2026 01:37:46 +0300 Subject: [PATCH 4/5] [TS] Prepare symbolic string backing after type refinement --- .../usvm/machine/interpreter/TsInterpreter.kt | 18 +-- .../kotlin/org/usvm/machine/state/TsState.kt | 3 + .../org/usvm/machine/state/TsStringBacking.kt | 81 ++++++++++++ .../org/usvm/machine/types/FakeExprUtil.kt | 3 + .../main/kotlin/org/usvm/util/LValueUtil.kt | 3 +- .../org/usvm/machine/TsStringEqualityTest.kt | 115 +++++++++++++++--- .../usvm/samples/lang/SymbolicStringInput.kt | 23 ++++ .../usvm/util/TsStringWitnessResolverTest.kt | 28 +++-- .../test/resources/models/StringEquality.ts | 27 ++++ 9 files changed, 263 insertions(+), 38 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index b15e04d2b1..21a07fdb9a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -69,7 +69,9 @@ import org.usvm.machine.state.lastStmt import org.usvm.machine.state.localsCount import org.usvm.machine.state.newStmt import org.usvm.machine.state.parametersWithThisCount +import org.usvm.machine.state.prepareRefinedStringBackings import org.usvm.machine.state.returnValue +import org.usvm.machine.state.symbolicStringBackingConstraint import org.usvm.machine.types.mkFakeValue import org.usvm.machine.types.toAuxiliaryType import org.usvm.sizeSort @@ -82,7 +84,6 @@ import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.mkRegisterStackLValue -import org.usvm.util.mkStringBackingLengthLValue import org.usvm.util.resolveEtsMethods import org.usvm.util.type import org.usvm.utils.ensureSat @@ -135,6 +136,8 @@ class TsInterpreter( // if no call, visit try { + scope.prepareRefinedStringBackings() ?: return scope.stepResult() + when (stmt) { is TsVirtualMethodCallStmt -> visitVirtualMethodCall(scope, stmt) is TsConcreteMethodCallStmt -> visitConcreteMethodCall(scope, stmt) @@ -826,18 +829,7 @@ class TsInterpreter( state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType) - // String constants store UTF-16 code units in their `value` array. - // Give symbolic inputs the same backing representation and bound its length. - val charsType = EtsArrayType(EtsNumberType, dimensions = 1) - val valueLValue = mkFieldLValue(addressSort, ref, field = "value") - val charsRef = state.memory.read(valueLValue).asExpr(addressSort) - state.pathConstraints += mkNot(mkHeapRefEq(charsRef, mkUndefinedValue())) - state.pathConstraints += state.memory.types.evalTypeEquals(charsRef, charsType) - - val lengthLValue = mkStringBackingLengthLValue(charsRef) - val length = state.memory.read(lengthLValue).asExpr(sizeSort) - state.pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) - state.pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)) + state.pathConstraints += state.symbolicStringBackingConstraint(ref) state.boundedStringBackingRefs += ref } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 4dd9f42851..143b33b358 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -87,6 +87,8 @@ class TsState( * String literals are recognized separately through [TsContext.getStringConstantValue]. */ var boundedStringBackingRefs: Set = emptySet(), + /** Unresolved reference payloads that may acquire string backing after type refinement. */ + var symbolicStringCandidates: Set = emptySet(), var unsupportedReason: String? = null, private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( @@ -324,6 +326,7 @@ class TsState( dfltObjectFieldSorts = dfltObjectFieldSorts, stringConstantAllocatedRefs = stringConstantAllocatedRefs, boundedStringBackingRefs = boundedStringBackingRefs, + symbolicStringCandidates = symbolicStringCandidates, unsupportedReason = unsupportedReason, activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt new file mode 100644 index 0000000000..fee07adb24 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt @@ -0,0 +1,81 @@ +package org.usvm.machine.state + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType +import org.usvm.UBoolExpr +import org.usvm.UHeapRef +import org.usvm.UIteExpr +import org.usvm.UNullRef +import org.usvm.USymbolicHeapRef +import org.usvm.api.evalTypeEquals +import org.usvm.api.typeStreamOf +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.solver.UUnsatResult +import org.usvm.types.singleOrNull +import org.usvm.util.mkFieldLValue +import org.usvm.util.mkStringBackingLengthLValue + +/** Recording a possible string adds no constraints or backing fields. */ +internal fun TsState.trackSymbolicStringCandidate(ref: UHeapRef) { + when (ref) { + is UNullRef -> Unit + is USymbolicHeapRef -> symbolicStringCandidates += ref + is UIteExpr<*> -> { + trackSymbolicStringCandidate(ref.trueBranch.asExpr(ctx.addressSort)) + trackSymbolicStringCandidate(ref.falseBranch.asExpr(ctx.addressSort)) + } + } +} + +/** The same input reference and field are used for typed inputs and later type refinements. */ +internal fun TsState.symbolicStringBackingConstraint(ref: UHeapRef): UBoolExpr = with(ctx) { + val charsRef = memory.read(mkFieldLValue(addressSort, ref, field = "value")) + val charsType = EtsArrayType(EtsNumberType, dimensions = 1) + val length = memory.read(mkStringBackingLengthLValue(charsRef)) + + val definedBacking = mkNot(mkHeapRefEq(charsRef, mkUndefinedValue())) + val backingType = memory.types.evalTypeEquals(charsRef, charsType) + val nonnegativeLength = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + val boundedLength = mkBvSignedLessOrEqualExpr(length, mkBv(maxStringLength)) + + mkAnd(definedBacking, backingType, nonnegativeLength, boundedLength) +} + +/** Prepare only references that are already non-nullish strings on this execution path. */ +internal fun TsStepScope.prepareRefinedStringBackings(): Unit? { + val candidates = calcOnState { + symbolicStringCandidates.filter { ref -> + ref !in boundedStringBackingRefs && memory.typeStreamOf(ref).singleOrNull() == EtsStringType + } + } + for (ref in candidates) { + // A singleton type stream alone does not exclude nullish references. + // Prove the full condition on the path, independently of any one solver model. + val definitelyString = calcOnState { + val alternative = clone() + val stringCondition = with(ctx) { + val stringType = memory.types.evalTypeEquals(ref, EtsStringType) + val nonNull = mkNot(mkHeapRefEq(ref, mkTsNullValue())) + val defined = mkNot(mkHeapRefEq(ref, mkUndefinedValue())) + + mkAnd(stringType, nonNull, defined) + } + alternative.pathConstraints += ctx.mkNot(stringCondition) + + ctx.solver().check(alternative.pathConstraints) is UUnsatResult + } + if (!definitelyString) continue + + val backingConstraint = calcOnState { symbolicStringBackingConstraint(ref) } + assert(backingConstraint) ?: return null + doWithState { + boundedStringBackingRefs += ref + symbolicStringCandidates -= ref + } + } + + return Unit +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt index 0917e2dfc8..412b0f8f44 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt @@ -14,6 +14,7 @@ import org.usvm.machine.IntermediateLValueField import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsState +import org.usvm.machine.state.trackSymbolicStringCandidate import org.usvm.memory.ULValue /** @@ -82,6 +83,8 @@ fun TsState.mkFakeValue( } if (refValue != null) { + trackSymbolicStringCandidate(refValue) + val refLValue = ctx.getIntermediateRefLValue(address) memory.write(refLValue, refValue, guard = ctx.trueExpr) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt index a4e8104319..f1439e6e71 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt @@ -4,6 +4,7 @@ import io.ksmt.sort.KBv16Sort import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsField import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType import org.usvm.UConcreteHeapRef import org.usvm.UExpr @@ -28,7 +29,7 @@ internal fun TsState.arrayStorageType(ref: UHeapRef, staticType: EtsType): EtsTy if (ref !is UConcreteHeapRef && ref !is USymbolicHeapRef) return staticType val memoryType = memory.typeStreamOf(ref).singleOrNull() - return if (memoryType is EtsArrayType || isAllocatedConcreteHeapRef(ref)) { + return if (memoryType is EtsArrayType || memoryType == EtsStringType || isAllocatedConcreteHeapRef(ref)) { memoryType ?: staticType } else { staticType diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt index 6b65a64be0..4f61a3526d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt @@ -1,5 +1,6 @@ package org.usvm.machine +import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.loadEtsFileAutoConvert @@ -11,6 +12,7 @@ import org.usvm.StateCollectionStrategy import org.usvm.UMachineOptions import org.usvm.api.TsTest import org.usvm.api.TsTestValue +import org.usvm.machine.expr.extractDouble import org.usvm.machine.state.TsMethodResult import org.usvm.util.TsMethodTestRunner import org.usvm.util.TsTestResolver @@ -139,11 +141,27 @@ class TsStringEqualityTest : TsMethodTestRunner() { } @Test - fun `any and unknown string alternatives are explicit unsupported paths`() { + fun `refined any and unknown strings produce replayable equality witnesses`() { val generated = listOf("equalsAnyStrings", "equalsUnknownStrings").associateWith { name -> - val method = scene.projectClasses.single { it.name == "StringEquality" } - .methods - .single { it.name == name } + val method = getMethod(methodName = name, className = "StringEquality") + val expectedResult: (TsTestValue, TsTestValue.TsString) -> Int = { left, right -> + if (left is TsTestValue.TsString) { + if (left.value == right.value) 1 else 2 + } else { + 3 + } + } + + discoverProperties( + method = method, + { left, right, result -> result.number == 1.0 && expectedResult(left, right) == 1 }, + { left, right, result -> result.number == 2.0 && expectedResult(left, right) == 2 }, + { left, right, result -> result.number == 3.0 && expectedResult(left, right) == 3 }, + invariants = arrayOf({ left, right, result -> + result.number == expectedResult(left, right).toDouble() + }), + ) + val analysis = TsMachine( scene, options = analysisOptions.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), @@ -153,10 +171,16 @@ class TsStringEqualityTest : TsMethodTestRunner() { } assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason, name) - assertTrue(analysis.unsupportedPaths.any { "modeled string backing" in it }, name) + assertTrue(analysis.unsupportedPaths.isEmpty(), name) val tests = analysis.states.map { state -> TsTestResolver().resolve(method, state) } assertTrue(tests.isNotEmpty(), name) - assertTrue(tests.all { resultNumber(it) == 3 }, "$name: $tests") + assertEquals(setOf(1, 2, 3), tests.map(::resultNumber).toSet(), name) + tests.forEach { test -> + val left = test.before.parameters[0] + val right = assertIs(test.before.parameters[1]) + + assertEquals(expectedResult(left, right), resultNumber(test), "$name: $test") + } tests } @@ -175,11 +199,57 @@ class TsStringEqualityTest : TsMethodTestRunner() { machine.analyze(listOf(method)) } val ordinaryTests = ordinaryStates.map { state -> TsTestResolver().resolve(method, state) } - assertTrue(ordinaryTests.none { resultNumber(it) in setOf(1, 2) }) + assertEquals(setOf(1, 2, 3), ordinaryTests.map(::resultNumber).toSet()) + } + + @Test + fun `refinement prepares backing before length alias reads and unused string results`() { + val expected = mapOf Int>( + "refinedStringLength" to { input -> + if (input is TsTestValue.TsString) { + if (input.value.length == 1) 1 else 2 + } else { + 3 + } + }, + "refinedStringAlias" to { input -> + if (input is TsTestValue.TsString) { + if (input.value.length == 1) 1 else 2 + } else { + 3 + } + }, + "refinedStringUnused" to { input -> if (input is TsTestValue.TsString) 1 else 3 }, + "refinedStringNullish" to { input -> + when (input) { + TsTestValue.TsNull -> 4 + TsTestValue.TsUndefined -> 5 + is TsTestValue.TsString -> if (input.value.length == 1) 1 else 2 + else -> 3 + } + }, + ) + val generated = expected.mapValues { (name, expectedResult) -> + val tests = analyze(name) + val expectedResults = when (name) { + "refinedStringUnused" -> setOf(1, 3) + "refinedStringNullish" -> setOf(1, 2, 3, 4, 5) + else -> setOf(1, 2, 3) + } + + assertEquals(expectedResults, tests.map(::resultNumber).toSet(), name) + tests.forEach { test -> + assertEquals(expectedResult(test.before.parameters[0]), resultNumber(test), "$name: $test") + } + + tests + } + + replayDynamic(generated) } @Test - fun `two unmodeled string references do not yield equality witnesses`() { + fun `two refined dynamic strings produce replayable equality witnesses`() { val method = scene.projectClasses.single { it.name == "StringEquality" } .methods .single { it.name == "looselyEqualsDynamicStrings" } @@ -192,20 +262,37 @@ class TsStringEqualityTest : TsMethodTestRunner() { } assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) - assertTrue(analysis.unsupportedPaths.any { "modeled string backing" in it }) + assertTrue(analysis.unsupportedPaths.isEmpty()) val unsupportedWitnesses = mutableListOf() val tests = analysis.states.mapNotNull { state -> try { TsTestResolver().resolve(method, state) } catch (failure: TsUnsupportedWitnessException) { + // An input left unrefined by the early return may still have no string model. + val result = assertIs(state.methodResult).value + val number = state.models.first().eval(result.asExpr(state.ctx.fp64Sort)).extractDouble() + assertEquals(3.0, number, "A refined string branch must have a replayable witness") + unsupportedWitnesses += failure null } } - assertTrue(unsupportedWitnesses.isNotEmpty(), "Expected an unbacked string witness") assertTrue(unsupportedWitnesses.all { "missing backing array" in it.message.orEmpty() }) - assertTrue(tests.none { resultNumber(it) in setOf(1, 2) }, "$tests") + assertEquals(setOf(1, 2, 3), tests.map(::resultNumber).toSet()) + tests.forEach { test -> + val left = test.before.parameters[0] + val right = test.before.parameters[1] + val expected = if (left is TsTestValue.TsString && right is TsTestValue.TsString) { + if (left.value == right.value) 1 else 2 + } else { + 3 + } + + assertEquals(expected, resultNumber(test), "$test") + } + + replayDynamic(mapOf("looselyEqualsDynamicStrings" to tests)) } @Test @@ -284,10 +371,9 @@ class TsStringEqualityTest : TsMethodTestRunner() { appendLine(source.readText()) tests.forEach { (name, generated) -> generated.forEachIndexed { index, test -> - val left = jsDynamic(test.before.parameters[0]) - val right = jsString(assertIs(test.before.parameters[1]).value) + val args = test.before.parameters.joinToString(transform = ::jsDynamic) - appendLine("if (new StringEquality().$name($left, $right) !== ${resultNumber(test)}) {") + appendLine("if (new StringEquality().$name($args) !== ${resultNumber(test)}) {") appendLine(" throw Error('$name witness $index');") appendLine("}") } @@ -303,6 +389,7 @@ class TsStringEqualityTest : TsMethodTestRunner() { } private fun jsDynamic(value: TsTestValue): String = when (value) { + is TsTestValue.TsString -> jsString(value.value) is TsTestValue.TsBoolean -> value.value.toString() is TsTestValue.TsNumber -> value.number.toString() TsTestValue.TsNull -> "null" diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SymbolicStringInput.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SymbolicStringInput.kt index 5bc75927dc..389dc32a22 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SymbolicStringInput.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SymbolicStringInput.kt @@ -46,6 +46,29 @@ class SymbolicStringInput : TsMethodTestRunner() { ) } + @Test + fun `string inferred from any preserves all length outcomes`() { + val method = getMethod(methodName = "anyStringLength") + + discoverProperties( + method = method, + { input, result -> input !is TsTestValue.TsString && result.number == 0.0 }, + { input, result -> input is TsTestValue.TsString && input.value.length == 1 && result.number == 1.0 }, + { input, result -> input is TsTestValue.TsString && input.value.length != 1 && result.number == 2.0 }, + invariants = arrayOf( + { input, result -> + val expected = when { + input !is TsTestValue.TsString -> 0.0 + input.value.length == 1 -> 1.0 + else -> 2.0 + } + + result.number == expected + }, + ), + ) + } + @Test fun `literal preserves NUL non-ASCII and a surrogate pair`() { val method = getMethod(methodName = "literal") diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsStringWitnessResolverTest.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsStringWitnessResolverTest.kt index 730e70de6a..657f768520 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsStringWitnessResolverTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsStringWitnessResolverTest.kt @@ -11,6 +11,7 @@ import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import java.nio.file.Path import kotlin.io.path.readText +import kotlin.test.assertEquals import kotlin.test.assertIs import kotlin.test.assertTrue import kotlin.time.Duration @@ -24,7 +25,7 @@ class TsStringWitnessResolverTest : TsMethodTestRunner() { override val scene: EtsScene = loadScene(tsPath) @Test - fun `string inferred from any without backing cannot become an empty witness`() { + fun `string inferred from any has replayable length witnesses`() { val method = getMethod(methodName = "anyStringLength", className = "SymbolicStringInput") val machineOptions = UMachineOptions( pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), @@ -40,29 +41,36 @@ class TsStringWitnessResolverTest : TsMethodTestRunner() { ).use { machine -> machine.analyze(methods = listOf(method)) } - val resolutions = states.map { state -> runCatching { TsTestResolver().resolve(method, state) } } + val tests = states.map { state -> TsTestResolver().resolve(method, state) } assertTrue(states.isNotEmpty()) - val unsupported = resolutions.mapNotNull { result -> result.exceptionOrNull() } - assertTrue(unsupported.isNotEmpty(), "Expected an unbacked symbolic string: $resolutions") - unsupported.forEach { failure -> - assertIs(failure) - assertTrue("missing backing array" in failure.message.orEmpty(), failure.toString()) + assertEquals( + setOf(0.0, 1.0, 2.0), + tests.map { test -> assertIs(test.returnValue).number }.toSet(), + ) + tests.forEach { test -> + val input = test.before.parameters.single() + val expected = when { + input !is TsTestValue.TsString -> 0.0 + input.value.length == 1 -> 1.0 + else -> 2.0 + } + + assertEquals(expected, assertIs(test.returnValue).number, message = "$test") } - val supported = resolutions.mapNotNull { result -> result.getOrNull() } - assertTrue(supported.isNotEmpty()) val script = buildString { appendLine(getResourcePath(tsPath).readText()) appendLine("if (new SymbolicStringInput().anyStringLength(\"\") !== 2) throw Error('empty string');") appendLine("if (new SymbolicStringInput().anyStringLength(\"x\") !== 1) throw Error('one-char string');") - supported.forEachIndexed { index, test -> + tests.forEachIndexed { index, test -> val input = when (val value = test.before.parameters.single()) { TsTestValue.TsUndefined -> "undefined" TsTestValue.TsNull -> "null" is TsTestValue.TsBoolean -> value.value.toString() is TsTestValue.TsNumber -> value.number.toString() is TsTestValue.TsString -> jsString(value.value) + is TsTestValue.TsClass -> "{}" else -> error("Unexpected input for anyStringLength: $value") } val expected = assertIs(test.returnValue).number diff --git a/usvm-ts/src/test/resources/models/StringEquality.ts b/usvm-ts/src/test/resources/models/StringEquality.ts index b861925d4f..150607f96c 100644 --- a/usvm-ts/src/test/resources/models/StringEquality.ts +++ b/usvm-ts/src/test/resources/models/StringEquality.ts @@ -52,6 +52,33 @@ class StringEquality { return left == right ? 1 : 2; } + refinedStringLength(left: any): number { + if (typeof left !== "string") return 3; + + return left.length === 1 ? 1 : 2; + } + + refinedStringAlias(left: unknown): number { + const alias = left; + if (typeof left !== "string") return 3; + + return (alias as string).length === 1 ? 1 : 2; + } + + refinedStringUnused(left: any): number { + if (typeof left !== "string") return 3; + + return 1; + } + + refinedStringNullish(left: any): number { + if (left === null) return 4; + if (left === undefined) return 5; + if (typeof left !== "string") return 3; + + return left.length === 1 ? 1 : 2; + } + nullAndUndefined(): number { return null === undefined ? 1 : null == undefined ? 2 : 3; } From 7217c2a1094af74217dc0d2ba03e0c058d0fd4e1 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 4 Oct 2026 22:31:13 +0300 Subject: [PATCH 5/5] [TS] Separate string backing from user property fields --- .../org/usvm/machine/expr/ReadLength.kt | 5 +- .../usvm/machine/operator/TsBinaryOperator.kt | 6 +- .../kotlin/org/usvm/machine/state/TsState.kt | 7 +- .../org/usvm/machine/state/TsStringBacking.kt | 4 +- .../main/kotlin/org/usvm/util/LValueUtil.kt | 7 ++ .../org/usvm/machine/TsStringEqualityTest.kt | 84 ++++++++++++++++++- .../kotlin/org/usvm/util/TsTestResolver.kt | 6 +- .../test/resources/models/StringEquality.ts | 21 +++++ 8 files changed, 124 insertions(+), 16 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt index 61fa030a29..b30f330466 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt @@ -17,7 +17,7 @@ import org.usvm.machine.interpreter.TsStepScope import org.usvm.sizeSort import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayLengthLValue -import org.usvm.util.mkFieldLValue +import org.usvm.util.mkStringBackingLValue import org.usvm.util.mkStringBackingLengthLValue // Handles reading the `length` property. @@ -40,8 +40,7 @@ fun TsContext.readLengthProperty( is EtsStringType -> { val charsRef = scope.calcOnState { - val valueLValue = mkFieldLValue(addressSort, instance, field = "value") - memory.read(valueLValue) + memory.read(mkStringBackingLValue(instance)) } return readArrayLength( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 03f28f177a..3b635c8919 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -24,8 +24,8 @@ import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.ExprWithTypeConstraint import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.util.boolToFp -import org.usvm.util.mkFieldLValue import org.usvm.util.mkStringBackingElementLValue +import org.usvm.util.mkStringBackingLValue import org.usvm.util.mkStringBackingLengthLValue private val logger = KotlinLogging.logger {} @@ -74,8 +74,8 @@ private fun TsContext.stringValueEquals( } val comparison = scope.calcOnState { - val lhsChars = memory.read(mkFieldLValue(addressSort, lhs, field = "value")) - val rhsChars = memory.read(mkFieldLValue(addressSort, rhs, field = "value")) + val lhsChars = memory.read(mkStringBackingLValue(lhs)) + val rhsChars = memory.read(mkStringBackingLValue(rhs)) val lhsLength = memory.read(mkStringBackingLengthLValue(lhsChars)) val rhsLength = memory.read(mkStringBackingLengthLValue(rhsChars)) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 143b33b358..c5b244ee33 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -32,7 +32,7 @@ import org.usvm.memory.UMemory import org.usvm.model.UModelBase import org.usvm.sizeSort import org.usvm.targets.UTargetsSet -import org.usvm.util.mkFieldLValue +import org.usvm.util.mkStringBackingLValue import org.usvm.util.type /** @@ -280,9 +280,8 @@ class TsState( contents = value.asSequence().map { mkBv(it.code, bv16Sort) }, ) - // Write char array to `ref.value` - val valueLValue = mkFieldLValue(addressSort, ref, field = "value") - memory.write(valueLValue, charArray, guard = trueExpr) + val backingLValue = mkStringBackingLValue(ref) + memory.write(backingLValue, charArray, guard = trueExpr) ref } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt index fee07adb24..c55f84de76 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt @@ -15,7 +15,7 @@ import org.usvm.api.typeStreamOf import org.usvm.machine.interpreter.TsStepScope import org.usvm.solver.UUnsatResult import org.usvm.types.singleOrNull -import org.usvm.util.mkFieldLValue +import org.usvm.util.mkStringBackingLValue import org.usvm.util.mkStringBackingLengthLValue /** Recording a possible string adds no constraints or backing fields. */ @@ -32,7 +32,7 @@ internal fun TsState.trackSymbolicStringCandidate(ref: UHeapRef) { /** The same input reference and field are used for typed inputs and later type refinements. */ internal fun TsState.symbolicStringBackingConstraint(ref: UHeapRef): UBoolExpr = with(ctx) { - val charsRef = memory.read(mkFieldLValue(addressSort, ref, field = "value")) + val charsRef = memory.read(mkStringBackingLValue(ref)) val charsType = EtsArrayType(EtsNumberType, dimensions = 1) val length = memory.read(mkStringBackingLengthLValue(charsRef)) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt index f1439e6e71..2dca78e1bd 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt @@ -6,6 +6,7 @@ import org.jacodb.ets.model.EtsField import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType +import org.usvm.UAddressSort import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef @@ -84,6 +85,12 @@ internal fun mkStringBackingLengthLValue( UArrayLengthLValue(ref, stringBackingArrayDescriptor, sizeSort) } +private object StringBackingField + +/** Internal string contents never share a field region with TypeScript properties. */ +internal fun mkStringBackingLValue(ref: UHeapRef): UFieldLValue<*, UAddressSort> = + UFieldLValue(ref.tctx.addressSort, ref, StringBackingField) + internal fun mkStringBackingElementLValue( ref: UHeapRef, index: UExpr, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt index 4f61a3526d..28a45cdf66 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt @@ -248,6 +248,86 @@ class TsStringEqualityTest : TsMethodTestRunner() { replayDynamic(generated) } + @Test + fun `refinement of a value field preserves both branches without unsupported paths`() { + val method = getMethod(methodName = "refinedStringValueFieldUnused", className = "StringEquality") + val defaultOptions = analysisOptions.copy( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = false, + ) + + withOptions(options = defaultOptions) { + discoverProperties( + method = method, + { box, result -> box.properties["value"] is TsTestValue.TsString && result.number == 1.0 }, + { box, result -> box.properties["value"] !is TsTestValue.TsString && result.number == 3.0 }, + invariants = arrayOf({ box, result -> + val expected = if (box.properties["value"] is TsTestValue.TsString) 1.0 else 3.0 + + result.number == expected + }), + ) + } + + val analysis = TsMachine( + scene, + options = defaultOptions, + tsOptions = TsOptions(maxArraySize = 4), + ).use { machine -> + machine.analyzeWithOutcome(listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.isEmpty()) + } + + @Test + fun `refined value fields produce replayable length and equality witnesses`() { + val lengthMethod = getMethod(methodName = "refinedStringValueFieldLength", className = "StringEquality") + val lengthResult: (TsTestValue.TsClass) -> Double = { box -> + val selected = box.properties["value"] + + if (selected is TsTestValue.TsString) { + if (selected.value.length == 1) 1.0 else 2.0 + } else { + 3.0 + } + } + + discoverProperties( + method = lengthMethod, + { box, result -> result.number == 1.0 && lengthResult(box) == 1.0 }, + { box, result -> result.number == 2.0 && lengthResult(box) == 2.0 }, + { box, result -> result.number == 3.0 && lengthResult(box) == 3.0 }, + invariants = arrayOf({ box, result -> result.number == lengthResult(box) }), + ) + + val equalityMethod = getMethod(methodName = "equalsRefinedStringValueField", className = "StringEquality") + val equalityResult: (TsTestValue.TsClass, TsTestValue.TsString) -> Double = { box, other -> + val selected = box.properties["value"] + + if (selected is TsTestValue.TsString) { + if (selected.value == other.value) 1.0 else 2.0 + } else { + 3.0 + } + } + + discoverProperties( + method = equalityMethod, + { box, other, result -> result.number == 1.0 && equalityResult(box, other) == 1.0 }, + { box, other, result -> result.number == 2.0 && equalityResult(box, other) == 2.0 }, + { box, other, result -> result.number == 3.0 && equalityResult(box, other) == 3.0 }, + invariants = arrayOf({ box, other, result -> result.number == equalityResult(box, other) }), + ) + + val generated = listOf("refinedStringValueFieldLength", "equalsRefinedStringValueField") + .associateWith { name -> analyze(name) } + + replayDynamic(generated) + } + @Test fun `two refined dynamic strings produce replayable equality witnesses`() { val method = scene.projectClasses.single { it.name == "StringEquality" } @@ -394,7 +474,9 @@ class TsStringEqualityTest : TsMethodTestRunner() { is TsTestValue.TsNumber -> value.number.toString() TsTestValue.TsNull -> "null" TsTestValue.TsUndefined -> "undefined" - is TsTestValue.TsClass -> "{}" + is TsTestValue.TsClass -> value.properties.entries.joinToString(prefix = "{", postfix = "}") { (name, field) -> + "${jsString(name)}: ${jsDynamic(field)}" + } is TsTestValue.TsArray<*> -> "[]" else -> error("Unexpected string alternative: $value") } diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 1e45549f0e..ef0f1c60d7 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -328,13 +328,13 @@ open class TsTestStateResolver( ): TsTestValue.TsString = with(ctx) { getStringConstantValue(concreteRef)?.let { return TsTestValue.TsString(it) } - // Symbolic strings have no mutable value field in the final state. Resolve + // Symbolic strings have no mutable backing field in the final state. Resolve // their backing array from the model in both before and after snapshots. val allocated = isAllocatedConcreteHeapRef(concreteRef) val stringMemory = if (allocated) finalStateMemory else model val stringRef = if (allocated) heapRef else concreteRef - val valueLValue = mkFieldLValue(addressSort, stringRef, field = "value") - val charsRef = evaluateInModel(stringMemory.read(valueLValue)) as UConcreteHeapRef + val backingLValue = mkStringBackingLValue(stringRef) + val charsRef = evaluateInModel(stringMemory.read(backingLValue)) as UConcreteHeapRef if (charsRef.address == 0) { throw TsUnsupportedWitnessException("Symbolic string is missing backing array: $concreteRef") } diff --git a/usvm-ts/src/test/resources/models/StringEquality.ts b/usvm-ts/src/test/resources/models/StringEquality.ts index 150607f96c..b545014e41 100644 --- a/usvm-ts/src/test/resources/models/StringEquality.ts +++ b/usvm-ts/src/test/resources/models/StringEquality.ts @@ -71,6 +71,27 @@ class StringEquality { return 1; } + refinedStringValueFieldUnused(box: { value: any }): number { + const selected = box.value; + if (typeof selected !== "string") return 3; + + return 1; + } + + refinedStringValueFieldLength(box: { value: any }): number { + const selected = box.value; + if (typeof selected !== "string") return 3; + + return selected.length === 1 ? 1 : 2; + } + + equalsRefinedStringValueField(box: { value: any }, other: string): number { + const selected = box.value; + if (typeof selected !== "string") return 3; + + return selected === other ? 1 : 2; + } + refinedStringNullish(left: any): number { if (left === null) return 4; if (left === undefined) return 5;