diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 44ac1c78a4..870048878a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -455,8 +455,8 @@ private fun TsExprResolver.handleBooleanConstructor(expr: EtsInstanceCallExpr): } val arg = resolve(expr.args.single()) ?: return null - val truthy = mkTruthyExpr(arg, scope) scope.ensureTruthinessSupported(arg) ?: return null + val truthy = mkTruthyExpr(arg, scope) truthy } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStaticApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStaticApproximations.kt index c8161576f4..224bcb11ff 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStaticApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStaticApproximations.kt @@ -68,8 +68,8 @@ private fun TsExprResolver.handleBooleanConverter(expr: EtsStaticCallExpr): UExp } val arg = resolve(expr.args.single()) ?: return null - val truthy = mkTruthyExpr(arg, scope) scope.ensureTruthinessSupported(arg) ?: return null + val truthy = mkTruthyExpr(arg, scope) return truthy } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt index 3833b98440..c69bd9c328 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt @@ -24,6 +24,7 @@ import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState +import org.usvm.machine.state.prepareStringBacking import org.usvm.machine.types.EtsFakeType import org.usvm.machine.types.ExprWithTypeConstraint import org.usvm.types.single @@ -162,6 +163,7 @@ private fun TsState.unsupportedTruthinessCondition(expr: UExpr): UBoo /** Validate the execution path separately from constructing its boolean expression. */ fun TsStepScope.ensureTruthinessSupported(expr: UExpr): Unit? { + prepareTruthinessStringBacking(expr) ?: return null val unsupportedString = calcOnState { unsupportedTruthinessCondition(expr) } if (unsupportedString.isFalse) return Unit @@ -171,6 +173,41 @@ fun TsStepScope.ensureTruthinessSupported(expr: UExpr): Unit? { }) } +private fun TsStepScope.prepareTruthinessStringBacking( + expr: UExpr, + activeGuard: UBoolExpr = calcOnState { ctx.trueExpr }, +): Unit? { + val context = calcOnState { ctx } + val hasFakeBranches = with(context) { + expr.sort == addressSort && expr.asExpr(addressSort).hasFakeValueBranch() + } + if (expr is UIteExpr<*> && hasFakeBranches) { + val trueGuard = context.mkAnd(activeGuard, expr.condition) + val falseGuard = context.mkAnd(activeGuard, context.mkNot(expr.condition)) + prepareTruthinessStringBacking(expr.trueBranch, trueGuard) ?: return null + return prepareTruthinessStringBacking(expr.falseBranch, falseGuard) + } + + val isFake = with(context) { expr.isFakeObject() } + if (isFake) { + val fakeValue = expr as UConcreteHeapRef + val (reference, referenceGuard) = calcOnState { + with(ctx) { + val type = fakeValue.getFakeType(memory) + val guard = mkAnd(activeGuard, type.refTypeExpr) + + memory.read(getIntermediateRefLValue(fakeValue.address)) to guard + } + } + return prepareStringBacking(reference, referenceGuard) + } + if (expr.sort == context.addressSort) { + return prepareStringBacking(expr.asExpr(context.addressSort), activeGuard) + } + + return Unit +} + /** Construct a condition; call [ensureTruthinessSupported] before executing with it. */ fun TsContext.mkTruthyExpr( expr: UExpr, 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 10f4a9ed6d..81aa89a000 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 @@ -542,14 +542,14 @@ class TsInterpreter( val expr = exprResolver.resolve(stmt.condition) ?: return + scope.ensureTruthinessSupported(expr) ?: return + val boolExpr = if (expr.sort == ctx.boolSort) { expr.asExpr(ctx.boolSort) } else { ctx.mkTruthyExpr(expr, scope) } - scope.ensureTruthinessSupported(expr) ?: return - observer?.onIfStatementWithResolvedCondition(simpleValueResolver, stmt, boolExpr, scope) val successors = graph.successors(stmt).take(2).toList() 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 5e73b1dee6..375221e027 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 @@ -20,10 +20,12 @@ import org.usvm.machine.TsContext import org.usvm.machine.TsSizeSort import org.usvm.machine.expr.ensureTruthinessSupported import org.usvm.machine.expr.mkIsNullOrUndefined +import org.usvm.machine.expr.mkNotNullOrUndefined import org.usvm.machine.expr.mkNumericExpr import org.usvm.machine.expr.mkNumericExprWithGuard import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.prepareStringBacking import org.usvm.machine.types.ExprWithTypeConstraint import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.util.boolToFp @@ -260,6 +262,12 @@ private fun TsContext.stringValueEquals( if (lhsIsString.isFalse || rhsIsString.isFalse) return falseExpr val bothStrings = mkAnd(lhsIsString, rhsIsString) + val lhsNonNullish = mkNotNullOrUndefined(lhs) + val rhsNonNullish = mkNotNullOrUndefined(rhs) + val stringComparisonGuard = mkAnd(activeGuard, bothStrings, lhsNonNullish, rhsNonNullish) + scope.prepareStringBacking(lhs, stringComparisonGuard) ?: return null + scope.prepareStringBacking(rhs, stringComparisonGuard) ?: return null + val missingBacking = scope.calcOnState { (lhsConstant == null && lhs !in boundedStringBackingRefs) || (rhsConstant == null && rhs !in boundedStringBackingRefs) @@ -379,6 +387,9 @@ private fun TsContext.referenceOrStringValueEquals( val sameReference = mkHeapRefEq(lhs, rhs) if (sameReference.isTrue) return trueExpr + val comparesNullishConstant = mkIsNullOrUndefined(lhs).isTrue || mkIsNullOrUndefined(rhs).isTrue + if (comparesNullishConstant) return sameReference + val equalStringValues = stringValueEquals(lhs, rhs, sameReference, activeGuard, scope) ?: return null return mkOr(sameReference, equalStringValues) } @@ -1445,8 +1456,8 @@ sealed interface TsBinaryOperator { ): UExpr<*>? { check(lhs.isFakeObject() || rhs.isFakeObject()) - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) scope.ensureTruthinessSupported(lhs) ?: return null + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) return scope.calcOnState { iteWriteIntoFakeObject(scope, lhsTruthyExpr, rhs, lhs) @@ -1460,8 +1471,8 @@ sealed interface TsBinaryOperator { ): UExpr<*>? { check(!lhs.isFakeObject() && !rhs.isFakeObject()) - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) scope.ensureTruthinessSupported(lhs) ?: return null + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) return scope.calcOnState { iteWriteIntoFakeObject(scope, lhsTruthyExpr, rhs, lhs) @@ -1501,8 +1512,8 @@ sealed interface TsBinaryOperator { ): UExpr<*>? { check(lhs.isFakeObject() || rhs.isFakeObject()) - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) scope.ensureTruthinessSupported(lhs) ?: return null + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) return iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs) } @@ -1514,8 +1525,8 @@ sealed interface TsBinaryOperator { ): UExpr<*>? { check(!lhs.isFakeObject() && !rhs.isFakeObject()) - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) scope.ensureTruthinessSupported(lhs) ?: return null + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) return iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsUnaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsUnaryOperator.kt index 4c54e04bba..ef2fcf4f4c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsUnaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsUnaryOperator.kt @@ -70,8 +70,8 @@ sealed interface TsUnaryOperator { arg: UExpr, scope: TsStepScope, ): UBoolExpr? { - val truthy = mkTruthyExpr(arg, scope) scope.ensureTruthinessSupported(arg) ?: return null + val truthy = mkTruthyExpr(arg, scope) return mkNot(truthy) } @@ -80,8 +80,8 @@ sealed interface TsUnaryOperator { arg: UConcreteHeapRef, scope: TsStepScope, ): UBoolExpr? { - val truthy = mkTruthyExpr(arg, scope) scope.ensureTruthinessSupported(arg) ?: return null + val truthy = mkTruthyExpr(arg, scope) return mkNot(truthy) } 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 91b181f1b4..e2734a08b7 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 @@ -12,6 +12,8 @@ import org.usvm.UNullRef import org.usvm.USymbolicHeapRef import org.usvm.api.evalTypeEquals import org.usvm.api.typeStreamOf +import org.usvm.isFalse +import org.usvm.isTrue import org.usvm.machine.expr.mkNotNullOrUndefined import org.usvm.machine.interpreter.TsStepScope import org.usvm.solver.UUnsatResult @@ -45,6 +47,40 @@ internal fun TsState.symbolicStringBackingConstraint(ref: UHeapRef): UBoolExpr = mkAnd(definedBacking, backingType, nonnegativeLength, boundedLength) } +/** Split the runtime string alternative before reading contents; other values retain their original state. */ +internal fun TsStepScope.prepareStringBacking(ref: UHeapRef, activeGuard: UBoolExpr): Unit? { + val context = calcOnState { ctx } + if (ref is UIteExpr<*>) { + val trueGuard = context.mkAnd(activeGuard, ref.condition) + val falseGuard = context.mkAnd(activeGuard, context.mkNot(ref.condition)) + prepareStringBacking(ref.trueBranch.asExpr(context.addressSort), trueGuard) ?: return null + return prepareStringBacking(ref.falseBranch.asExpr(context.addressSort), falseGuard) + } + val needsBacking = calcOnState { ref is USymbolicHeapRef && ref !in boundedStringBackingRefs } + if (!needsBacking) return Unit + + val stringCondition = calcOnState { + val stringType = memory.types.evalTypeEquals(ref, EtsStringType) + val nonNullish = ctx.mkNotNullOrUndefined(ref) + ctx.mkAnd(activeGuard, stringType, nonNullish) + } + if (stringCondition.isFalse) return Unit + + val takeString = calcOnState { models.first().eval(stringCondition).isTrue } + val selectedCondition = if (takeString) stringCondition else context.mkNot(stringCondition) + fork(selectedCondition) ?: return null + if (!takeString) return Unit + + val backingConstraint = calcOnState { symbolicStringBackingConstraint(ref) } + assert(backingConstraint) ?: return null + doWithState { + boundedStringBackingRefs += ref to maxStringLength + symbolicStringCandidates -= ref + } + + return Unit +} + /** Prepare only references that are already non-nullish strings on this execution path. */ internal fun TsStepScope.prepareRefinedStringBackings(): Unit? { val candidates = calcOnState { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsDynamicTruthinessTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsDynamicTruthinessTest.kt index 7e0054f6df..7633de49fd 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsDynamicTruthinessTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsDynamicTruthinessTest.kt @@ -13,7 +13,6 @@ import org.usvm.api.TsTest import org.usvm.api.TsTestValue import org.usvm.util.TsMethodTestRunner 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 @@ -25,14 +24,11 @@ import kotlin.test.assertTrue import kotlin.time.Duration private const val TRUTHINESS_REPLAY_FAILURE_CONTEXT_LIMIT = 1000 -private const val UNBACKED_STRING_REASON = "Truthiness needs a modeled string backing for dynamic references" -private const val MISSING_STRING_BACKING_PREFIX = "Symbolic string is missing backing array:" class TsDynamicTruthinessTest : TsMethodTestRunner() { private data class AnalysisWitnesses( val analysis: TsAnalysisResult, val witnesses: List, - val unsupportedWitnesses: List, ) @TempDir @@ -42,14 +38,23 @@ class TsDynamicTruthinessTest : TsMethodTestRunner() { override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) @Test - fun `unbacked any strings are unsupported in truthiness without losing object paths`() { + fun `dynamic truthiness prepares string backing without losing object paths`() { discoverProperties( method = getMethod(methodName = "objectTruthy", className = "SymbolicStringInput"), { _, result -> result.number == 1.0 }, invariants = arrayOf({ _, result -> result.number == 1.0 }), ) - val names = setOf("anyTruthy", "anyNegated", "anyAnd", "anyOr", "anyObjectTruthy", "objectTruthy") + val names = setOf( + "anyTruthy", + "anyNegated", + "anyAnd", + "anyOr", + "anyObjectTruthy", + "objectTruthy", + "truthinessBeforeKind", + "equalsObjectBeforeKind", + ) val methods = scene.projectClasses.single { it.name == "SymbolicStringInput" }.methods .filter { it.name in names } .associateBy { it.name } @@ -59,6 +64,7 @@ class TsDynamicTruthinessTest : TsMethodTestRunner() { solverTimeout = Duration.INFINITE, typeOperationsTimeout = Duration.INFINITE, stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, ) val results = TsMachine( @@ -68,38 +74,18 @@ class TsDynamicTruthinessTest : TsMethodTestRunner() { ).use { machine -> methods.mapValues { (_, method) -> val analysis = machine.analyzeWithOutcome(listOf(method)) - val unsupportedWitnesses = mutableListOf() - val witnesses = analysis.states.mapNotNull { state -> - try { - TsTestResolver().resolve(method, state) - } catch (e: TsUnsupportedWitnessException) { - if (method.name != "anyObjectTruthy" || - e.message?.startsWith(MISSING_STRING_BACKING_PREFIX) != true - ) { - throw e - } - - unsupportedWitnesses += e.message.orEmpty() - null - } - } + val witnesses = analysis.states.map { state -> TsTestResolver().resolve(method, state) } - AnalysisWitnesses(analysis, witnesses, unsupportedWitnesses) + AnalysisWitnesses(analysis, witnesses) } } assertEquals(names, methods.keys) results.forEach { (name, result) -> - val (analysis, witnesses, unsupportedWitnesses) = result + val (analysis, witnesses) = result assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) - if (name == "objectTruthy") { - assertTrue(analysis.unsupportedPaths.isEmpty(), "$name: ${analysis.unsupportedPaths}") - } else if (name == "anyObjectTruthy") { - assertTrue(analysis.unsupportedPaths.isEmpty(), "$name: ${analysis.unsupportedPaths}") - assertTrue( - unsupportedWitnesses.isEmpty(), - "$name regressed a string witness prepared after type refinement: $unsupportedWitnesses", - ) + assertTrue(analysis.unsupportedPaths.isEmpty(), "$name: ${analysis.unsupportedPaths}") + if (name == "anyObjectTruthy") { assertTrue( witnesses.any { witness -> witness.before.parameters.single() is TsTestValue.TsClass && @@ -107,8 +93,6 @@ class TsDynamicTruthinessTest : TsMethodTestRunner() { }, "$name lost its object path", ) - } else { - assertTrue(UNBACKED_STRING_REASON in analysis.unsupportedPaths, "$name: ${analysis.unsupportedPaths}") } assertTrue(witnesses.isNotEmpty(), "$name produced no supported witnesses") } @@ -143,4 +127,32 @@ class TsDynamicTruthinessTest : TsMethodTestRunner() { failureContext = script.take(TRUTHINESS_REPLAY_FAILURE_CONTEXT_LIMIT), ) } + + @Test + fun `truthiness before type refinement retains empty strings null and undefined`() { + discoverProperties( + method = getMethod(methodName = "truthinessBeforeKind", className = "SymbolicStringInput"), + { input, result -> input is TsTestValue.TsString && input.value.isEmpty() && result.number == 10.0 }, + { input, result -> input is TsTestValue.TsString && input.value.isNotEmpty() && result.number == 21.0 }, + { input, result -> input == TsTestValue.TsNull && result.number == 30.0 }, + { input, result -> input == TsTestValue.TsUndefined && result.number == 40.0 }, + ) + } + + @Test + fun `object equality before type refinement retains all runtime kinds`() { + discoverProperties( + method = getMethod(methodName = "equalsObjectBeforeKind", className = "SymbolicStringInput"), + { input, result -> input is TsTestValue.TsString && result.number == 10.0 }, + { input, result -> input == TsTestValue.TsNull && result.number == 20.0 }, + { input, result -> input == TsTestValue.TsUndefined && result.number == 30.0 }, + { input, result -> + val otherKind = input !is TsTestValue.TsString && + input != TsTestValue.TsNull && input != TsTestValue.TsUndefined + + otherKind && result.number == 40.0 + }, + invariants = arrayOf({ _, result -> result.number < 100.0 }), + ) + } } 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 d69f4f9849..726c01e356 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt @@ -39,6 +39,7 @@ class TsStringEqualityTest : TsMethodTestRunner() { solverTimeout = Duration.INFINITE, typeOperationsTimeout = Duration.INFINITE, throwExceptionOnStepFailure = true, + stopOnCoverage = 0, ) @Test @@ -444,27 +445,37 @@ class TsStringEqualityTest : TsMethodTestRunner() { } @Test - fun `unsupported fork does not consume covered-new slot or stop before supported result`() { + fun `unrefined equality retains equal and unequal string and non string inputs`() { val method = scene.projectClasses.single { it.name == "StringEquality" } .methods .single { it.name == "equalsAnyDirect" } val analysis = TsMachine( scene, - options = analysisOptions.copy(collectedStatesLimit = 1), + options = analysisOptions.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 }) + assertTrue(analysis.unsupportedPaths.isEmpty(), analysis.unsupportedPaths.toString()) val tests = analysis.states.map { state -> TsTestResolver().resolve(method, state) } - val supported = tests.filter { test -> + val nonString = tests.filter { test -> test.before.parameters[0] !is TsTestValue.TsString && resultNumber(test) == 2 } - assertTrue(supported.isNotEmpty(), "$tests") + assertTrue(nonString.isNotEmpty(), "$tests") + assertTrue( + tests.any { test -> + test.before.parameters[0] is TsTestValue.TsString && resultNumber(test) == 1 + }, + ) + assertTrue( + tests.any { test -> + test.before.parameters[0] is TsTestValue.TsString && resultNumber(test) == 2 + }, + ) - replayDynamic(mapOf("equalsAnyDirect" to supported)) + replayDynamic(mapOf("equalsAnyDirect" to tests)) } private fun analyze(name: String, maxStringLength: Int = 4): List { diff --git a/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts b/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts index 5e9e214fd3..2e984edc4e 100644 --- a/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts +++ b/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts @@ -125,6 +125,27 @@ class SymbolicStringInput { return 0; } + truthinessBeforeKind(value: any): number { + const truthy = value ? 1 : 0; + if (typeof value === "string") { + return truthy + (value.length === 0 ? 10 : 20); + } + if (value === null) return truthy + 30; + if (value === undefined) return truthy + 40; + + return truthy + 50; + } + + equalsObjectBeforeKind(value: any): number { + const object = { marker: 1 }; + const equal = value === object ? 100 : 0; + if (typeof value === "string") return equal + 10; + if (value === null) return equal + 20; + if (value === undefined) return equal + 30; + + return equal + 40; + } + anyAnd(value: any): number { if (value && true) return 1; return 0;