From f2a22c368c515e3591c8f5f0fd02a1be19eedf23 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 5 Oct 2026 15:54:45 +0300 Subject: [PATCH 1/3] [TS] Model string truthiness and typed field values --- .../kotlin/org/usvm/machine/expr/ExprUtil.kt | 106 +++- .../kotlin/org/usvm/machine/expr/ReadField.kt | 97 +++- .../usvm/machine/interpreter/TsInterpreter.kt | 2 +- .../usvm/machine/operator/TsBinaryOperator.kt | 24 +- .../usvm/machine/operator/TsUnaryOperator.kt | 25 +- .../usvm/machine/TsDynamicTruthinessTest.kt | 146 ++++++ .../machine/TsStringTruthinessReplayTest.kt | 473 ++++++++++++++++++ .../samples/lang/SymbolicStringInput.ts | 115 +++++ 8 files changed, 945 insertions(+), 43 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsDynamicTruthinessTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsStringTruthinessReplayTest.kt 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 0d913621ee..b885770b4d 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 @@ -2,14 +2,21 @@ package org.usvm.machine.expr import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsStringLiteralType import org.jacodb.ets.model.EtsStringType 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.USymbolicHeapRef +import org.usvm.api.allocateConcreteRef +import org.usvm.api.evalTypeEquals import org.usvm.api.makeSymbolicPrimitive import org.usvm.isFalse +import org.usvm.isTrue import org.usvm.machine.TsContext import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope @@ -18,7 +25,10 @@ import org.usvm.machine.state.TsState import org.usvm.machine.types.EtsFakeType import org.usvm.machine.types.ExprWithTypeConstraint import org.usvm.types.single +import org.usvm.types.singleOrNull import org.usvm.util.boolToFp +import org.usvm.util.mkStringBackingLValue +import org.usvm.util.mkStringBackingLengthLValue fun TsContext.checkNotFake(expr: UExpr<*>) { require(!expr.isFakeObject()) { @@ -29,7 +39,82 @@ fun TsContext.checkNotFake(expr: UExpr<*>) { fun TsContext.mkTruthyExpr( expr: UExpr, scope: TsStepScope, -): UBoolExpr = scope.calcOnState { +): UBoolExpr? = scope.calcOnState { + // `any` is assignable both to and from string, so a type-relation query cannot identify + // a materialized string. Inspect the concrete type stream before reading its backing array. + fun stringTypeCondition(ref: UHeapRef): UBoolExpr = when (ref) { + is UConcreteHeapRef, is USymbolicHeapRef -> { + val type = memory.types.getTypeStream(ref).singleOrNull() + if (type is EtsStringType || type is EtsStringLiteralType) { + mkTrue() + } else { + memory.types.evalTypeEquals(ref, EtsStringType) + } + } + + is UIteExpr<*> -> { + val trueRef = ref.trueBranch.asExpr(addressSort) + val falseRef = ref.falseBranch.asExpr(addressSort) + val trueIsString = stringTypeCondition(trueRef) + val falseIsString = stringTypeCondition(falseRef) + + mkIte(ref.condition, trueIsString, falseIsString) + } + + else -> mkFalse() + } + + fun hasStringBacking(ref: UHeapRef): UBoolExpr = when (ref) { + is UConcreteHeapRef -> { + if (getStringConstantValue(ref) != null || ref in boundedStringBackingRefs) mkTrue() else mkFalse() + } + + is USymbolicHeapRef -> { + if (ref in boundedStringBackingRefs) mkTrue() else mkFalse() + } + + is UIteExpr<*> -> { + val trueRef = ref.trueBranch.asExpr(addressSort) + val falseRef = ref.falseBranch.asExpr(addressSort) + + mkIte(ref.condition, hasStringBacking(trueRef), hasStringBacking(falseRef)) + } + + else -> mkFalse() + } + + fun referenceTruthy(ref: UHeapRef, activeGuard: UBoolExpr): UBoolExpr? { + val nonNullish = mkAnd( + mkHeapRefEq(ref, mkTsNullValue()).not(), + mkHeapRefEq(ref, mkUndefinedValue()).not(), + ) + if (nonNullish.isFalse) return mkFalse() + + val isString = stringTypeCondition(ref) + if (isString.isFalse) return nonNullish + + val backedString = hasStringBacking(ref) + val unsupportedString = mkAnd(activeGuard, nonNullish, isString, mkNot(backedString)) + if (!unsupportedString.isFalse) { + scope.fork(mkNot(unsupportedString), blockOnFalseState = { + terminateAsUnsupported(reason = "Truthiness needs a modeled string backing for dynamic references") + }) ?: return null + } + if (backedString.isFalse) return nonNullish + + val charsRef = memory.read(mkStringBackingLValue(ref)) + val readableCharsRef = if (isString.isTrue) { + charsRef + } else { + // Other objects need no backing array. Keep the array-region read away from their null field value. + mkIte(isString, charsRef, allocateConcreteRef()) + } + val length = memory.read(mkStringBackingLengthLValue(readableCharsRef)) + val stringIsNonEmpty = mkNot(mkEq(length, mkBv(0))) + + return mkAnd(nonNullish, mkImplies(isString, stringIsNonEmpty)) + } + if (expr.isFakeObject()) { val falseBranchGround = makeSymbolicPrimitive(boolSort) @@ -61,12 +146,11 @@ fun TsContext.mkTruthyExpr( if (!possibleType.refTypeExpr.isFalse) { val value = memory.read(getIntermediateRefLValue(expr.address)) + val refTruthy = referenceTruthy(value, activeGuard = possibleType.refTypeExpr) + ?: return@calcOnState null conjuncts += ExprWithTypeConstraint( constraint = possibleType.refTypeExpr, - expr = mkAnd( - mkHeapRefEq(value, mkTsNullValue()).not(), - mkHeapRefEq(value, mkUndefinedValue()).not(), - ) + expr = refTruthy ) } @@ -74,12 +158,7 @@ fun TsContext.mkTruthyExpr( mkIte(condition, value, acc) } } else { - // TODO: simply convert `expr` to bool by implementing ToBoolean(arg): - // if arg is Boolean : return arg - // if arg is undefined | null | +0f | -0f | NaN | 0 | "" : return false - // else return true // non-negative numbers, any living objects, non-empty strings, etc - // (https://tc39.es/ecma262/#sec-toboolean) - // This conversion might be useful in other places as well, not just for truthy in ifs. + // ECMAScript ToBoolean (https://tc39.es/ecma262/#sec-toboolean). when (expr.sort) { boolSort -> expr.asExpr(boolSort) @@ -89,10 +168,7 @@ fun TsContext.mkTruthyExpr( mkFpIsNaNExpr(expr.asExpr(fp64Sort)).not() ) - addressSort -> mkAnd( - mkHeapRefEq(expr.asExpr(addressSort), mkTsNullValue()).not(), - mkHeapRefEq(expr.asExpr(addressSort), mkUndefinedValue()).not(), - ) + addressSort -> referenceTruthy(expr.asExpr(addressSort), activeGuard = trueExpr) else -> TODO("Unsupported sort: ${expr.sort}") } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index fd27d6f2c5..9cca305474 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -2,12 +2,20 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr import mu.KotlinLogging +import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsInstanceFieldRef import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStaticFieldRef +import org.jacodb.ets.model.EtsStringLiteralType +import org.jacodb.ets.model.EtsStringType +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.USymbolicHeapRef +import org.usvm.api.evalTypeEquals +import org.usvm.api.makeSymbolicRefUntyped import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.interpreter.ensureStaticsInitialized @@ -17,6 +25,9 @@ import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult import org.usvm.util.createFakeField import org.usvm.util.mkFieldLValue +import org.usvm.util.mkStringBackingElementLValue +import org.usvm.util.mkStringBackingLValue +import org.usvm.util.mkStringBackingLengthLValue import org.usvm.util.resolveEtsField private val logger = KotlinLogging.logger {} @@ -62,10 +73,11 @@ fun TsContext.readField( instance: UHeapRef, field: EtsFieldSignature, hierarchy: EtsHierarchy, -): UExpr<*> { +): UExpr<*>? { checkNotFake(instance) - val sort = when (val etsField = resolveEtsField(instanceLocal, field, hierarchy)) { + val resolvedField = resolveEtsField(instanceLocal, field, hierarchy) + val sort = when (resolvedField) { is TsResolutionResult.Empty -> { if (field.name !in listOf("i", "LogLevel")) { logger.warn { "Field $field not found, creating fake field" } @@ -78,7 +90,7 @@ fun TsContext.readField( addressSort } - is TsResolutionResult.Unique -> typeToSort(etsField.property.type) + is TsResolutionResult.Unique -> typeToSort(resolvedField.property.type) is TsResolutionResult.Ambiguous -> unresolvedSort } @@ -95,7 +107,27 @@ fun TsContext.readField( // If the field type is known, we can read it directly. if (sort !is TsUnresolvedSort) { val lValue = mkFieldLValue(sort, instance, field) - return scope.calcOnState { memory.read(lValue) } + val value = scope.calcOnState { memory.read(lValue) } + if (resolvedField is TsResolutionResult.Unique) { + when (val fieldType = resolvedField.property.type) { + is EtsStringLiteralType -> { + val maxStringLength = scope.calcOnState { maxStringLength } + return materializeTypedStringField( + scope = scope, + value = value.asExpr(addressSort), + literal = fieldType.value, + maxStringLength = maxStringLength, + ) + } + + is EtsStringType -> { + val maxStringLength = scope.calcOnState { maxStringLength } + return materializeTypedStringField(scope, value.asExpr(addressSort), maxStringLength) + } + } + } + + return value } // If the field type is unknown, we create a fake object. @@ -121,6 +153,63 @@ fun TsContext.readField( } } +private fun TsContext.materializeTypedStringField( + scope: TsStepScope, + value: UHeapRef, + maxStringLength: Int, + literal: String? = null, +): UHeapRef? { + // A prior write may have supplied an allocated literal or an already materialized string. + // Keep its original reference so its existing backing array remains authoritative. + if (value == mkTsNullValue() || value == mkUndefinedValue() || value is UConcreteHeapRef) { + return value + } + if (value is USymbolicHeapRef && scope.calcOnState { value in boundedStringBackingRefs }) { + return value + } + if (literal != null && literal.length > maxStringLength) { + scope.doWithState { + terminateAsUnsupported(reason = "Literal string field exceeds configured string length $maxStringLength") + } + return null + } + + val stringRef = scope.calcOnState { makeSymbolicRefUntyped() } + scope.assert(mkHeapRefEq(stringRef, value)) ?: return null + scope.assert(mkNot(mkHeapRefEq(stringRef, mkTsNullValue()))) ?: return null + scope.assert(mkNot(mkHeapRefEq(stringRef, mkUndefinedValue()))) ?: return null + scope.assert(scope.calcOnState { memory.types.evalTypeEquals(stringRef, EtsStringType) }) ?: return null + + val charsRef = scope.calcOnState { + val valueLValue = mkStringBackingLValue(stringRef) + memory.read(valueLValue) + } + val charsType = EtsArrayType(EtsNumberType, dimensions = 1) + scope.assert(mkNot(mkHeapRefEq(charsRef, mkTsNullValue()))) ?: return null + scope.assert(mkNot(mkHeapRefEq(charsRef, mkUndefinedValue()))) ?: return null + scope.assert(scope.calcOnState { memory.types.evalTypeEquals(charsRef, charsType) }) ?: return null + + val length = scope.calcOnState { memory.read(mkStringBackingLengthLValue(charsRef)) } + if (literal == null) { + val lengthIsNonNegative = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + val lengthIsWithinLimit = mkBvSignedLessOrEqualExpr(length, mkBv(maxStringLength)) + scope.assert(mkAnd(lengthIsNonNegative, lengthIsWithinLimit)) ?: return null + } else { + // A literal type fixes both the UTF-16 length and every code unit. + scope.assert(mkEq(length, mkBv(literal.length))) ?: return null + for ((index, character) in literal.withIndex()) { + val element = scope.calcOnState { + memory.read(mkStringBackingElementLValue(charsRef, mkBv(index))) + } + scope.assert(mkEq(element, mkBv(character.code, bv16Sort))) ?: return null + } + } + + scope.doWithState { boundedStringBackingRefs += stringRef } + + return stringRef +} + internal fun TsExprResolver.handleStaticFieldRef( value: EtsStaticFieldRef, ): UExpr<*>? = with(ctx) { 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 21a07fdb9a..2b94125e0f 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 @@ -464,7 +464,7 @@ class TsInterpreter( expr.asExpr(ctx.boolSort) } else { ctx.mkTruthyExpr(expr, scope) - } + } ?: return observer?.onIfStatementWithResolvedCondition(simpleValueResolver, stmt, boolExpr, scope) 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 3b635c8919..4890a87333 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 @@ -1098,7 +1098,7 @@ sealed interface TsBinaryOperator { lhs: UExpr, rhs: UExpr, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { return internalResolve(lhs, rhs, scope) } @@ -1106,7 +1106,7 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { return internalResolve(lhs, rhs, scope) } @@ -1114,11 +1114,11 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { check(lhs.isFakeObject() || rhs.isFakeObject()) + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) ?: return null return scope.calcOnState { - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) iteWriteIntoFakeObject(scope, lhsTruthyExpr, rhs, lhs) } } @@ -1127,10 +1127,10 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { check(!lhs.isFakeObject() && !rhs.isFakeObject()) - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) ?: return null return scope.calcOnState { iteWriteIntoFakeObject(scope, lhsTruthyExpr, rhs, lhs) } @@ -1150,7 +1150,7 @@ sealed interface TsBinaryOperator { lhs: UExpr, rhs: UExpr, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { return internalResolve(lhs, rhs, scope) } @@ -1158,7 +1158,7 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { return internalResolve(lhs, rhs, scope) } @@ -1166,10 +1166,10 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { check(lhs.isFakeObject() || rhs.isFakeObject()) - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) ?: return null return iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs) } @@ -1177,10 +1177,10 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { check(!lhs.isFakeObject() && !rhs.isFakeObject()) - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) ?: return null 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 ee7af60c16..81c1ad4cd0 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 @@ -17,27 +17,27 @@ sealed interface TsUnaryOperator { fun TsContext.resolveBool( arg: UBoolExpr, scope: TsStepScope, - ): UExpr + ): UExpr? fun TsContext.resolveFp( arg: UExpr, scope: TsStepScope, - ): UExpr + ): UExpr? fun TsContext.resolveRef( arg: UExpr, scope: TsStepScope, - ): UExpr + ): UExpr? fun TsContext.resolveFake( arg: UConcreteHeapRef, scope: TsStepScope, - ): UExpr + ): UExpr? fun TsContext.resolve( arg: UExpr, scope: TsStepScope, - ): UExpr { + ): UExpr? { if (arg.isFakeObject()) { return resolveFake(arg, scope) } @@ -60,22 +60,25 @@ sealed interface TsUnaryOperator { override fun TsContext.resolveFp( arg: UExpr, scope: TsStepScope, - ): UBoolExpr { - return mkNot(mkTruthyExpr(arg, scope)) + ): UBoolExpr? { + val truthy = mkTruthyExpr(arg, scope) ?: return null + return mkNot(truthy) } override fun TsContext.resolveRef( arg: UExpr, scope: TsStepScope, - ): UBoolExpr { - return mkNot(mkTruthyExpr(arg, scope)) + ): UBoolExpr? { + val truthy = mkTruthyExpr(arg, scope) ?: return null + return mkNot(truthy) } override fun TsContext.resolveFake( arg: UConcreteHeapRef, scope: TsStepScope, - ): UBoolExpr { - return mkNot(mkTruthyExpr(arg, scope)) + ): UBoolExpr? { + val truthy = mkTruthyExpr(arg, scope) ?: return null + return mkNot(truthy) } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsDynamicTruthinessTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsDynamicTruthinessTest.kt new file mode 100644 index 0000000000..130d9e5b87 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsDynamicTruthinessTest.kt @@ -0,0 +1,146 @@ +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.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 +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 + +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 + lateinit var directory: Path + + private val source = getResourcePath("/samples/lang/SymbolicStringInput.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + + @Test + fun `unbacked any strings are unsupported in truthiness 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", "anyObjectTruthy", "objectTruthy") + val methods = scene.projectClasses.single { it.name == "SymbolicStringInput" }.methods + .filter { it.name in names } + .associateBy { it.name } + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + stateCollectionStrategy = StateCollectionStrategy.ALL, + ) + + val results = TsMachine( + scene, + options = machineOptions, + tsOptions = TsOptions(maxArraySize = 2), + ).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 + } + } + + AnalysisWitnesses(analysis, witnesses, unsupportedWitnesses) + } + } + + assertEquals(names, methods.keys) + results.forEach { (name, result) -> + val (analysis, witnesses, unsupportedWitnesses) = 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( + witnesses.any { witness -> + witness.before.parameters.single() is TsTestValue.TsClass && + assertIs(witness.returnValue).number == 1.0 + }, + "$name lost its object path", + ) + } else { + assertTrue(UNBACKED_STRING_REASON in analysis.unsupportedPaths, "$name: ${analysis.unsupportedPaths}") + } + assertTrue(witnesses.isNotEmpty(), "$name produced no supported witnesses") + } + + val script = buildString { + appendLine(source.readText()) + results.forEach { (name, result) -> + result.witnesses.forEachIndexed { index, witness -> + val input = when (val value = witness.before.parameters.single()) { + is TsTestValue.TsBoolean -> value.value.toString() + is TsTestValue.TsNumber -> value.number.toString() + is TsTestValue.TsString -> jsString(value.value) + is TsTestValue.TsClass -> "{}" + is TsTestValue.TsArray<*> -> "[]" + TsTestValue.TsNull -> "null" + TsTestValue.TsUndefined -> "undefined" + else -> error("Unexpected truthiness input: $value") + } + val expected = assertIs(witness.returnValue).number + + appendLine("if (new SymbolicStringInput().$name($input) !== $expected) {") + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } + } + } + assertNodeReplay( + source = script, + directory = directory, + name = "any-truthiness", + timeoutMessage = "any-truthiness replay timed out", + failureContext = script.take(TRUTHINESS_REPLAY_FAILURE_CONTEXT_LIMIT), + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringTruthinessReplayTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringTruthinessReplayTest.kt new file mode 100644 index 0000000000..c3dc883772 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringTruthinessReplayTest.kt @@ -0,0 +1,473 @@ +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.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import org.usvm.util.jsString +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +private const val REPLAY_FAILURE_CONTEXT_LIMIT = 1000 + +class TsStringTruthinessReplayTest : TsMethodTestRunner() { + private data class FieldWitness(val value: TsTestValue, val result: Double) + + @TempDir + lateinit var directory: Path + + override val scene: EtsScene = loadScene("/samples/lang/SymbolicStringInput.ts") + + private val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + @Test + fun `symbolic strings have both truthiness outcomes`() { + discoverProperties( + method = getMethod(methodName = "conditional", className = "SymbolicStringInput"), + { input, result -> input.value.isEmpty() && result.number == 0.0 }, + { input, result -> input.value.isNotEmpty() && result.number == 1.0 }, + invariants = arrayOf({ input, result -> result.number == if (input.value.isEmpty()) 0.0 else 1.0 }), + ) + } + + @Test + fun `string field conditions and equality preserve both outcomes`() { + for (name in listOf("fieldConditional", "fieldNegation", "fieldAnd", "fieldOr", "fieldEqualsEmpty")) { + discoverProperties( + method = getMethod(methodName = name, className = "SymbolicStringInput"), + { _, result -> result.number == 0.0 }, + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ input, result -> + val value = assertIs(input.properties.getValue("value")).value + val expected = if (name == "fieldEqualsEmpty") value.isEmpty() else value.isNotEmpty() + + result.number == if (expected) 1.0 else 0.0 + }), + ) + } + } + + @Test + fun `literal string fields preserve exact input contents`() { + for ((name, expected) in mapOf("emptyLiteralField" to "", "nonemptyLiteralField" to "A\u0000\uD83D\uDE00")) { + discoverProperties( + method = getMethod(methodName = name, className = "SymbolicStringInput"), + { input, result -> + val value = assertIs(input.properties.getValue("value")).value + + value == expected && result.number == if (expected.isEmpty()) 0.0 else 1.0 + }, + ) + } + } + + @Test + fun `writes determine subsequent field truthiness`() { + for ((name, expected) in mapOf("writtenNonEmptyField" to 1.0, "writtenEmptyField" to 0.0)) { + discoverProperties( + method = getMethod(methodName = name, className = "SymbolicStringInput"), + { _, result -> result.number == expected }, + invariants = arrayOf({ _, result -> result.number == expected }), + ) + } + } + + @Test + fun `conditional write preserves untouched empty and nonempty fields`() { + options = options.copy(stateCollectionStrategy = StateCollectionStrategy.ALL, stopOnCoverage = 0) + + discoverProperties( + method = getMethod(methodName = "conditionallyWrittenField", className = "SymbolicStringInput"), + { _, overwrite, result -> overwrite.value && result.number == 0.0 }, + { _, overwrite, result -> !overwrite.value && result.number == 0.0 }, + { _, overwrite, result -> !overwrite.value && result.number == 1.0 }, + invariants = arrayOf({ input, overwrite, result -> + val truthy = !overwrite.value && + assertIs(input.properties.getValue("value")).value.isNotEmpty() + + result.number == if (truthy) 1.0 else 0.0 + }), + ) + } + + @Test + fun `symbolic and literal string truthiness replays in Node`() { + val source = getResourcePath("/samples/lang/SymbolicStringInput.ts") + val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + val names = setOf( + "truthy", + "conditional", + "emptyLiteralIsFalsy", + "nullCodeUnitIsTruthy", + "surrogatePairIsTruthy", + ) + val methods = scene.projectClasses.single { it.name == "SymbolicStringInput" }.methods + .filter { it.name in names } + .associateBy { it.name } + assertEquals(names, methods.keys) + + val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions(maxArraySize = 2)).use { machine -> + methods.mapValues { (_, method) -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + for (name in listOf("truthy", "conditional")) { + val generated = tests.getValue(name) + assertTrue(generated.isNotEmpty(), "$name produced no witnesses") + val outcomes = generated.map { test -> + val input = assertIs(test.before.parameters.single()).value + val result = when (val value = test.returnValue) { + is TsTestValue.TsBoolean -> value.value + is TsTestValue.TsNumber -> value.number == 1.0 + else -> error("Unexpected result for $name: $value") + } + + assertEquals(input.isNotEmpty(), result, message = test.toString()) + result + }.toSet() + if (name == "conditional") { + assertEquals(setOf(false, true), outcomes) + } + } + + for ((name, expected) in listOf( + "emptyLiteralIsFalsy" to false, + "nullCodeUnitIsTruthy" to true, + "surrogatePairIsTruthy" to true, + )) { + val generated = tests.getValue(name) + assertTrue(generated.isNotEmpty(), "$name produced no witnesses") + generated.forEach { test -> + assertEquals(expected, assertIs(test.returnValue).value) + } + } + + 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 = when (val result = test.returnValue) { + is TsTestValue.TsBoolean -> result.value.toString() + is TsTestValue.TsNumber -> result.number.toString() + else -> error("Unexpected result for $name: $result") + } + + appendLine("if (new SymbolicStringInput().$name($args) !== $expected) {") + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } + } + } + assertNodeReplay( + source = script, + directory = directory, + name = "string-truthiness", + timeoutMessage = "string-truthiness replay timed out", + failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), + ) + } + + @Test + fun `typed string field truthiness replays in Node`() { + val source = getResourcePath("/samples/lang/SymbolicStringInput.ts") + val names = setOf("fieldConditional", "fieldNegation", "fieldAnd", "fieldOr") + val tests = analyzeFieldMethods( + source = source, + names = names, + tsOptions = TsOptions(maxArraySize = 2), + requireComplete = false, + ) + + tests.forEach { (name, generated) -> + assertTrue(generated.isNotEmpty(), "$name produced no witnesses") + val outcomes = generated.map { test -> + val witness = fieldWitness(test) + val value = assertIs(witness.value).value + val result = witness.result + + assertEquals(if (value.isEmpty()) 0.0 else 1.0, result, message = test.toString()) + result + }.toSet() + assertEquals(setOf(0.0, 1.0), outcomes, message = name) + } + + val script = buildString { + appendLine(source.readText()) + tests.forEach { (name, generated) -> + generated.forEachIndexed { index, test -> + appendFieldWitness(name = name, index = index, witness = fieldWitness(test)) + } + } + } + assertNodeReplay( + source = script, + directory = directory, + name = "string-field-truthiness", + timeoutMessage = "string-field-truthiness replay timed out", + failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), + ) + } + + @Test + fun `typed string fields have no unsupported truthiness or equality paths`() { + val source = getResourcePath("/samples/lang/SymbolicStringInput.ts") + val names = setOf("fieldConditional", "fieldEqualsEmpty") + val generated = analyzeFieldMethods( + source = source, + names = names, + tsOptions = TsOptions(maxArraySize = 2), + requireComplete = true, + ) + + val script = buildString { + appendLine(source.readText()) + generated.forEach { (name, tests) -> + assertTrue(tests.isNotEmpty(), "$name produced no witnesses") + val outcomes = tests.mapIndexed { index, test -> + val witness = fieldWitness(test) + val value = assertIs(witness.value).value + val result = witness.result + val expected = if (name == "fieldEqualsEmpty") value.isEmpty() else value.isNotEmpty() + assertEquals(if (expected) 1.0 else 0.0, result, message = test.toString()) + + appendFieldWitness(name = name, index = index, witness = witness) + result + }.toSet() + assertEquals(setOf(0.0, 1.0), outcomes, name) + } + } + assertNodeReplay( + source = script, + directory = directory, + name = "string-field-truthiness-and-equality", + timeoutMessage = "string-field-truthiness-and-equality replay timed out", + failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), + ) + } + + @Test + fun `literal typed string fields retain exact contents and truthiness`() { + val source = getResourcePath("/samples/lang/SymbolicStringInput.ts") + val expected = mapOf( + "emptyLiteralField" to ("" to 0.0), + "nonemptyLiteralField" to ("A\u0000\uD83D\uDE00" to 1.0), + ) + val generated = analyzeFieldMethods( + source = source, + names = expected.keys, + tsOptions = TsOptions(maxArraySize = 4), + requireComplete = true, + ) + + val script = buildString { + appendLine(source.readText()) + generated.forEach { (name, tests) -> + assertTrue(tests.isNotEmpty(), "$name produced no witnesses") + val (expectedValue, expectedResult) = expected.getValue(name) + tests.forEachIndexed { index, test -> + val witness = fieldWitness(test) + val value = assertIs(witness.value).value + val result = witness.result + assertEquals(expectedValue, value, message = test.toString()) + assertEquals(expectedResult, result, message = test.toString()) + + appendFieldWitness(name = name, index = index, witness = witness) + } + } + } + assertNodeReplay( + source = script, + directory = directory, + name = "literal-string-field-truthiness", + timeoutMessage = "literal-string-field-truthiness replay timed out", + failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), + ) + } + + @Test + fun `literal field beyond configured bound is explicitly unsupported`() { + val source = getResourcePath("/samples/lang/SymbolicStringInput.ts") + val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + val method = scene.projectClasses.single { it.name == "SymbolicStringInput" }.methods + .single { it.name == "longLiteralField" } + + val analysis = TsMachine( + scene, + options = machineOptions.copy(throwExceptionOnStepFailure = true), + tsOptions = TsOptions(maxArraySize = 4), + ).use { machine -> machine.analyzeWithOutcome(listOf(method)) } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.states.isEmpty()) + assertEquals( + listOf("Literal string field exceeds configured string length 4"), + analysis.unsupportedPaths, + ) + } + + @Test + fun `written string field keeps literal truthiness`() { + val source = getResourcePath("/samples/lang/SymbolicStringInput.ts") + val expectedResults = mapOf("writtenNonEmptyField" to 1.0, "writtenEmptyField" to 0.0) + val tests = analyzeFieldMethods( + source = source, + names = expectedResults.keys, + tsOptions = TsOptions(maxArraySize = 2), + requireComplete = false, + ) + + val script = buildString { + appendLine(source.readText()) + tests.forEach { (name, generated) -> + assertTrue(generated.isNotEmpty(), "$name produced no witnesses") + generated.forEachIndexed { index, test -> + val witness = fieldWitness(test) + assertEquals(expectedResults.getValue(name), witness.result, message = test.toString()) + + appendFieldWitness(name = name, index = index, witness = witness) + } + } + } + assertNodeReplay( + source = script, + directory = directory, + name = "written-string-field-truthiness", + timeoutMessage = "written-string-field-truthiness replay timed out", + failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), + ) + } + + @Test + fun `conditional string field write preserves both paths`() { + val source = getResourcePath("/samples/lang/SymbolicStringInput.ts") + val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + val clazz = scene.projectClasses.single { it.name == "SymbolicStringInput" } + val method = clazz.methods.single { it.name == "conditionallyWrittenField" } + + val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions(maxArraySize = 2)).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + + assertTrue(tests.isNotEmpty()) + val outcomes = tests.map { test -> + val input = assertIs(test.before.parameters[0]) + val overwrite = assertIs(test.before.parameters[1]).value + val field = input.properties.getValue("value") + val result = assertIs(test.returnValue).number + val isTruthy = !overwrite && assertIs(field).value.isNotEmpty() + val expected = if (isTruthy) 1.0 else 0.0 + + assertEquals(expected, result, message = test.toString()) + result + }.toSet() + assertEquals(setOf(0.0, 1.0), outcomes) + + val script = buildString { + appendLine(source.readText()) + tests.forEachIndexed { index, test -> + val input = assertIs(test.before.parameters[0]) + val overwrite = assertIs(test.before.parameters[1]).value + val value = when (val field = input.properties.getValue("value")) { + is TsTestValue.TsString -> jsString(field.value) + is TsTestValue.TsUndefined -> "undefined" + else -> error("Unexpected field value: $field") + } + val expected = assertIs(test.returnValue).number + + val call = "new SymbolicStringInput().conditionallyWrittenField({ value: $value }, $overwrite)" + appendLine("if ($call !== $expected) {") + appendLine(" throw Error('conditional field witness $index');") + appendLine("}") + } + } + assertNodeReplay( + source = script, + directory = directory, + name = "conditional-string-field-truthiness", + timeoutMessage = "conditional-string-field-truthiness replay timed out", + failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), + ) + } + + private fun analyzeFieldMethods( + source: Path, + names: Set, + tsOptions: TsOptions, + requireComplete: Boolean, + ): Map> { + val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + val methods = scene.projectClasses.single { it.name == "SymbolicStringInput" }.methods + .filter { it.name in names } + .associateBy { it.name } + assertEquals(names, methods.keys) + + val options = if (requireComplete) { + machineOptions.copy( + stateCollectionStrategy = StateCollectionStrategy.ALL, + throwExceptionOnStepFailure = true, + ) + } else { + machineOptions + } + + return TsMachine(scene, options = options, tsOptions = tsOptions).use { machine -> + methods.mapValues { (_, method) -> + val states = if (requireComplete) { + val analysis = machine.analyzeWithOutcome(listOf(method)) + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.isEmpty(), "$method: ${analysis.unsupportedPaths}") + analysis.states + } else { + machine.analyze(listOf(method)) + } + + states.map { state -> TsTestResolver().resolve(method, state) } + } + } + } + + private fun fieldWitness(test: TsTest): FieldWitness { + val input = assertIs(test.before.parameters.single()) + val value = input.properties.getValue("value") + val result = assertIs(test.returnValue).number + + return FieldWitness(value = value, result = result) + } + + private fun StringBuilder.appendFieldWitness(name: String, index: Int, witness: FieldWitness) { + val encodedValue = when (val value = witness.value) { + is TsTestValue.TsString -> jsString(value.value) + is TsTestValue.TsUndefined -> "undefined" + is TsTestValue.TsNull -> "null" + else -> error("Unexpected field value: $value") + } + + appendLine("if (new SymbolicStringInput().$name({ value: $encodedValue }) !== ${witness.result}) {") + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } +} diff --git a/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts b/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts index 5802ee7e31..fc6001bd4b 100644 --- a/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts +++ b/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts @@ -1,3 +1,19 @@ +class SymbolicStringFieldInput { + value: string = ""; +} + +class EmptyLiteralStringFieldInput { + value: "" = ""; +} + +class NonemptyLiteralStringFieldInput { + value: "A\u0000\uD83D\uDE00" = "A\u0000\uD83D\uDE00"; +} + +class LongLiteralStringFieldInput { + value: "abcde" = "abcde"; +} + class SymbolicStringInput { identity(value: string): string { return value; @@ -26,4 +42,103 @@ class SymbolicStringInput { return value.length === 1 ? 1 : 2; } + + truthy(value: string): boolean { + return !!value; + } + + conditional(value: string): number { + if (value) return 1; + return 0; + } + + emptyLiteralIsFalsy(): boolean { + return !!""; + } + + nullCodeUnitIsTruthy(): boolean { + return !!"\u0000"; + } + + surrogatePairIsTruthy(): boolean { + return !!"\uD83D\uDE00"; + } + + fieldConditional(input: SymbolicStringFieldInput): number { + if (input.value) return 1; + return 0; + } + + fieldNegation(input: SymbolicStringFieldInput): number { + if (!input.value) return 0; + return 1; + } + + fieldAnd(input: SymbolicStringFieldInput): number { + if (input.value && true) return 1; + return 0; + } + + fieldOr(input: SymbolicStringFieldInput): number { + if (input.value || false) return 1; + return 0; + } + + fieldEqualsEmpty(input: SymbolicStringFieldInput): number { + return input.value === "" ? 1 : 0; + } + + emptyLiteralField(input: EmptyLiteralStringFieldInput): number { + if (input.value) return 1; + return 0; + } + + nonemptyLiteralField(input: NonemptyLiteralStringFieldInput): number { + if (input.value && input.value === "A\u0000\uD83D\uDE00") return 1; + return 0; + } + + longLiteralField(input: LongLiteralStringFieldInput): number { + return input.value ? 1 : 0; + } + + writtenNonEmptyField(input: SymbolicStringFieldInput): number { + input.value = "x"; + if (input.value) return 1; + return 0; + } + + writtenEmptyField(input: SymbolicStringFieldInput): number { + input.value = ""; + if (input.value) return 1; + return 0; + } + + conditionallyWrittenField(input: SymbolicStringFieldInput, overwrite: boolean): number { + if (overwrite) input.value = ""; + if (input.value) return 1; + return 0; + } + + anyTruthy(value: any): number { + if (value) return 1; + return 0; + } + + anyNegated(value: any): number { + if (!value) return 1; + return 0; + } + + anyObjectTruthy(value: any): number { + if (typeof value === "object" && value !== null) { + if (value) return 1; + } + return 0; + } + + objectTruthy(value: { x: number }): number { + if (value) return 1; + return 0; + } } From a1df4f6584640b721a6ac36ea739efb439e438cc Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 9 Oct 2026 12:58:27 +0300 Subject: [PATCH 2/3] [TS] Address string truthiness review feedback --- .../usvm/machine/expr/CallApproximations.kt | 5 +- .../machine/expr/CallStaticApproximations.kt | 6 +- .../kotlin/org/usvm/machine/expr/ExprUtil.kt | 130 ++++++++++-------- .../kotlin/org/usvm/machine/expr/ReadField.kt | 116 ++++++++-------- .../usvm/machine/interpreter/TsInterpreter.kt | 19 +-- .../usvm/machine/operator/TsBinaryOperator.kt | 22 ++- .../usvm/machine/operator/TsUnaryOperator.kt | 13 +- .../org/usvm/machine/state/TsStringBacking.kt | 6 +- .../usvm/machine/TsDynamicTruthinessTest.kt | 2 +- .../samples/lang/SymbolicStringInput.ts | 10 ++ 10 files changed, 192 insertions(+), 137 deletions(-) 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 385cd38679..9d6b68c402 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 @@ -255,7 +255,10 @@ private fun TsExprResolver.handleBooleanConstructor(expr: EtsInstanceCallExpr): } val arg = resolve(expr.args.single()) ?: return null - mkTruthyExpr(arg, scope) + val truthy = mkTruthyExpr(arg, scope) + scope.ensureTruthinessSupported(arg) ?: return null + + truthy } private fun TsExprResolver.handlePromiseConstructor(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { 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 16cb646287..d67aff4c38 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 @@ -50,5 +50,9 @@ private fun TsExprResolver.handleBooleanConverter(expr: EtsStaticCallExpr): UExp "Boolean() should have exactly one argument, but got ${expr.args.size}" } val arg = resolve(expr.args.single()) ?: return null - return mkTruthyExpr(arg, scope) + + val truthy = mkTruthyExpr(arg, scope) + scope.ensureTruthinessSupported(arg) ?: return null + + 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 b885770b4d..d164d1fda5 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 @@ -36,13 +36,10 @@ fun TsContext.checkNotFake(expr: UExpr<*>) { } } -fun TsContext.mkTruthyExpr( - expr: UExpr, - scope: TsStepScope, -): UBoolExpr? = scope.calcOnState { - // `any` is assignable both to and from string, so a type-relation query cannot identify - // a materialized string. Inspect the concrete type stream before reading its backing array. - fun stringTypeCondition(ref: UHeapRef): UBoolExpr = when (ref) { +// `any` is assignable both to and from string, so a type-relation query cannot identify +// a materialized string. Inspect the concrete type stream before reading its backing array. +private fun TsState.stringTypeCondition(ref: UHeapRef): UBoolExpr = with(ctx) { + when (ref) { is UConcreteHeapRef, is USymbolicHeapRef -> { val type = memory.types.getTypeStream(ref).singleOrNull() if (type is EtsStringType || type is EtsStringLiteralType) { @@ -63,8 +60,10 @@ fun TsContext.mkTruthyExpr( else -> mkFalse() } +} - fun hasStringBacking(ref: UHeapRef): UBoolExpr = when (ref) { +private fun TsState.hasStringBacking(ref: UHeapRef): UBoolExpr = with(ctx) { + when (ref) { is UConcreteHeapRef -> { if (getStringConstantValue(ref) != null || ref in boundedStringBackingRefs) mkTrue() else mkFalse() } @@ -82,39 +81,62 @@ fun TsContext.mkTruthyExpr( else -> mkFalse() } +} - fun referenceTruthy(ref: UHeapRef, activeGuard: UBoolExpr): UBoolExpr? { - val nonNullish = mkAnd( - mkHeapRefEq(ref, mkTsNullValue()).not(), - mkHeapRefEq(ref, mkUndefinedValue()).not(), - ) - if (nonNullish.isFalse) return mkFalse() +private fun TsState.referenceTruthy(ref: UHeapRef): UBoolExpr = with(ctx) { + val nonNullish = mkNotNullOrUndefined(ref) + if (nonNullish.isFalse) return@with mkFalse() - val isString = stringTypeCondition(ref) - if (isString.isFalse) return nonNullish + val isString = stringTypeCondition(ref) + if (isString.isFalse) return@with nonNullish - val backedString = hasStringBacking(ref) - val unsupportedString = mkAnd(activeGuard, nonNullish, isString, mkNot(backedString)) - if (!unsupportedString.isFalse) { - scope.fork(mkNot(unsupportedString), blockOnFalseState = { - terminateAsUnsupported(reason = "Truthiness needs a modeled string backing for dynamic references") - }) ?: return null - } - if (backedString.isFalse) return nonNullish - - val charsRef = memory.read(mkStringBackingLValue(ref)) - val readableCharsRef = if (isString.isTrue) { - charsRef - } else { - // Other objects need no backing array. Keep the array-region read away from their null field value. - mkIte(isString, charsRef, allocateConcreteRef()) - } - val length = memory.read(mkStringBackingLengthLValue(readableCharsRef)) - val stringIsNonEmpty = mkNot(mkEq(length, mkBv(0))) + val backedString = hasStringBacking(ref) + if (backedString.isFalse) return@with nonNullish + + val charsRef = memory.read(mkStringBackingLValue(ref)) + val readableBacking = mkAnd(isString, backedString) + val readableCharsRef = if (readableBacking.isTrue) { + charsRef + } else { + // Other objects need no backing array. Keep the array-region read away from their null field value. + mkIte(readableBacking, charsRef, allocateConcreteRef()) + } + val length = memory.read(mkStringBackingLengthLValue(readableCharsRef)) + val stringIsNonEmpty = mkNot(mkEq(length, mkBv(0))) + + mkAnd(nonNullish, mkImplies(isString, stringIsNonEmpty)) +} + +/** Validate the execution path separately from constructing its boolean expression. */ +fun TsStepScope.ensureTruthinessSupported(expr: UExpr): Unit? { + val unsupportedString = calcOnState { + with(ctx) { + val (ref, activeGuard) = when { + expr.isFakeObject() -> { + val type = expr.getFakeType(memory) + memory.read(getIntermediateRefLValue(expr.address)) to type.refTypeExpr + } + + expr.sort == addressSort -> expr.asExpr(addressSort) to trueExpr + else -> return@calcOnState falseExpr + } - return mkAnd(nonNullish, mkImplies(isString, stringIsNonEmpty)) + mkAnd(activeGuard, mkNotNullOrUndefined(ref), stringTypeCondition(ref), mkNot(hasStringBacking(ref))) + } } + if (unsupportedString.isFalse) return Unit + + val supported = calcOnState { ctx.mkNot(unsupportedString) } + return fork(supported, blockOnFalseState = { + terminateAsUnsupported(reason = "Truthiness needs a modeled string backing for dynamic references") + }) +} +/** Construct a condition; call [ensureTruthinessSupported] before executing with it. */ +fun TsContext.mkTruthyExpr( + expr: UExpr, + scope: TsStepScope, +): UBoolExpr = scope.calcOnState { if (expr.isFakeObject()) { val falseBranchGround = makeSymbolicPrimitive(boolSort) @@ -146,8 +168,7 @@ fun TsContext.mkTruthyExpr( if (!possibleType.refTypeExpr.isFalse) { val value = memory.read(getIntermediateRefLValue(expr.address)) - val refTruthy = referenceTruthy(value, activeGuard = possibleType.refTypeExpr) - ?: return@calcOnState null + val refTruthy = referenceTruthy(value) conjuncts += ExprWithTypeConstraint( constraint = possibleType.refTypeExpr, expr = refTruthy @@ -168,7 +189,7 @@ fun TsContext.mkTruthyExpr( mkFpIsNaNExpr(expr.asExpr(fp64Sort)).not() ) - addressSort -> referenceTruthy(expr.asExpr(addressSort), activeGuard = trueExpr) + addressSort -> referenceTruthy(expr.asExpr(addressSort)) else -> TODO("Unsupported sort: ${expr.sort}") } @@ -249,10 +270,7 @@ fun TsContext.mkNullishExpr( // If it represents a primitive type (bool/number), it's never nullish. return mkIte( condition = fakeType.refTypeExpr, - trueBranch = mkOr( - mkHeapRefEq(ref, mkTsNullValue()), - mkHeapRefEq(ref, mkUndefinedValue()) - ), + trueBranch = mkIsNullOrUndefined(ref), falseBranch = mkFalse(), ) } @@ -260,10 +278,7 @@ fun TsContext.mkNullishExpr( // Regular reference is nullish if it is either null or undefined if (expr.sort == addressSort) { val ref = expr.asExpr(addressSort) - return mkOr( - mkHeapRefEq(ref, mkTsNullValue()), - mkHeapRefEq(ref, mkUndefinedValue()) - ) + return mkIsNullOrUndefined(ref) } // Non-reference types (numbers, booleans, strings) are never nullish @@ -275,16 +290,21 @@ fun TsState.throwException(reason: String) { methodResult = TsMethodResult.TsException(ref, EtsStringType) } +fun TsContext.mkIsNullOrUndefined(ref: UHeapRef): UBoolExpr { + checkNotFake(ref) + + val isNull = mkHeapRefEq(ref, mkTsNullValue()) + val isUndefined = mkHeapRefEq(ref, mkUndefinedValue()) + return mkOr(isNull, isUndefined) +} + fun TsContext.mkNotNullOrUndefined(ref: UHeapRef): UBoolExpr { - require(!ref.isFakeObject()) { - "Fake object handling should be done outside of this function" - } - return mkNot( - mkOr( - mkHeapRefEq(ref, mkTsNullValue()), - mkHeapRefEq(ref, mkUndefinedValue()) - ) - ) + checkNotFake(ref) + + val isNull = mkHeapRefEq(ref, mkTsNullValue()) + val isUndefined = mkHeapRefEq(ref, mkUndefinedValue()) + // Preserve the explicit disequalities when this expression is composed into path guards. + return mkAnd(mkNot(isNull), mkNot(isUndefined)) } fun TsContext.checkUndefinedOrNullPropertyRead( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index 9cca305474..7cc1a9b381 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -13,6 +13,7 @@ import org.jacodb.ets.model.EtsStringType import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.USort import org.usvm.USymbolicHeapRef import org.usvm.api.evalTypeEquals import org.usvm.api.makeSymbolicRefUntyped @@ -64,10 +65,10 @@ internal fun TsExprResolver.handleInstanceFieldRef( } // Read the field. - return readField(scope, instanceLocal, instance, value.field, hierarchy) + return resolveField(scope, instanceLocal, instance, value.field, hierarchy) } -fun TsContext.readField( +private fun TsContext.resolveField( scope: TsStepScope, instanceLocal: EtsLocal?, instance: UHeapRef, @@ -95,39 +96,40 @@ fun TsContext.readField( is TsResolutionResult.Ambiguous -> unresolvedSort } - scope.doWithState { - // If we accessed some field, we make an assumption that - // this field should present in the object. - // That's not true in the common case for TS, but that's the decision we made. + val fieldExists = scope.calcOnState { + // We assume a field accessed by the program is present, even though TS permits absent fields. val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name)) - // assert is required to update models - scope.assert(memory.types.evalIsSubtype(instance, auxiliaryType)) + memory.types.evalIsSubtype(instance, auxiliaryType) } + scope.assert(fieldExists) ?: return null + + val value = readField(scope, instance, field, sort) + if (resolvedField !is TsResolutionResult.Unique || sort is TsUnresolvedSort) return value + + val maxStringLength = scope.calcOnState { maxStringLength } + return when (val fieldType = resolvedField.property.type) { + is EtsStringLiteralType -> materializeTypedStringField( + scope = scope, + value = value.asExpr(addressSort), + literal = fieldType.value, + maxStringLength = maxStringLength, + ) + + is EtsStringType -> materializeTypedStringField(scope, value.asExpr(addressSort), maxStringLength) + else -> value + } +} - // If the field type is known, we can read it directly. +/** Reading a field always produces a value; path validation belongs to [resolveField]. */ +private fun TsContext.readField( + scope: TsStepScope, + instance: UHeapRef, + field: EtsFieldSignature, + sort: USort, +): UExpr<*> { if (sort !is TsUnresolvedSort) { val lValue = mkFieldLValue(sort, instance, field) - val value = scope.calcOnState { memory.read(lValue) } - if (resolvedField is TsResolutionResult.Unique) { - when (val fieldType = resolvedField.property.type) { - is EtsStringLiteralType -> { - val maxStringLength = scope.calcOnState { maxStringLength } - return materializeTypedStringField( - scope = scope, - value = value.asExpr(addressSort), - literal = fieldType.value, - maxStringLength = maxStringLength, - ) - } - - is EtsStringType -> { - val maxStringLength = scope.calcOnState { maxStringLength } - return materializeTypedStringField(scope, value.asExpr(addressSort), maxStringLength) - } - } - } - - return value + return scope.calcOnState { memory.read(lValue) } } // If the field type is unknown, we create a fake object. @@ -175,35 +177,35 @@ private fun TsContext.materializeTypedStringField( } val stringRef = scope.calcOnState { makeSymbolicRefUntyped() } - scope.assert(mkHeapRefEq(stringRef, value)) ?: return null - scope.assert(mkNot(mkHeapRefEq(stringRef, mkTsNullValue()))) ?: return null - scope.assert(mkNot(mkHeapRefEq(stringRef, mkUndefinedValue()))) ?: return null - scope.assert(scope.calcOnState { memory.types.evalTypeEquals(stringRef, EtsStringType) }) ?: return null - - val charsRef = scope.calcOnState { - val valueLValue = mkStringBackingLValue(stringRef) - memory.read(valueLValue) - } - val charsType = EtsArrayType(EtsNumberType, dimensions = 1) - scope.assert(mkNot(mkHeapRefEq(charsRef, mkTsNullValue()))) ?: return null - scope.assert(mkNot(mkHeapRefEq(charsRef, mkUndefinedValue()))) ?: return null - scope.assert(scope.calcOnState { memory.types.evalTypeEquals(charsRef, charsType) }) ?: return null - - val length = scope.calcOnState { memory.read(mkStringBackingLengthLValue(charsRef)) } - if (literal == null) { - val lengthIsNonNegative = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) - val lengthIsWithinLimit = mkBvSignedLessOrEqualExpr(length, mkBv(maxStringLength)) - scope.assert(mkAnd(lengthIsNonNegative, lengthIsWithinLimit)) ?: return null - } else { - // A literal type fixes both the UTF-16 length and every code unit. - scope.assert(mkEq(length, mkBv(literal.length))) ?: return null - for ((index, character) in literal.withIndex()) { - val element = scope.calcOnState { - memory.read(mkStringBackingElementLValue(charsRef, mkBv(index))) + val constraints = scope.calcOnState { + val charsRef = memory.read(mkStringBackingLValue(stringRef)) + val charsType = EtsArrayType(EtsNumberType, dimensions = 1) + val length = memory.read(mkStringBackingLengthLValue(charsRef)) + val stringType = memory.types.evalTypeEquals(stringRef, EtsStringType) + val backingType = memory.types.evalTypeEquals(charsRef, charsType) + val contents = if (literal == null) { + val nonnegativeLength = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + val boundedLength = mkBvSignedLessOrEqualExpr(length, mkBv(maxStringLength)) + mkAnd(nonnegativeLength, boundedLength) + } else { + // A literal type fixes both the UTF-16 length and every code unit. + val characters = literal.mapIndexed { index, character -> + val element = memory.read(mkStringBackingElementLValue(charsRef, mkBv(index))) + mkEq(element, mkBv(character.code, bv16Sort)) } - scope.assert(mkEq(element, mkBv(character.code, bv16Sort))) ?: return null + mkAnd(mkEq(length, mkBv(literal.length)), mkAnd(characters)) } + + mkAnd( + mkHeapRefEq(stringRef, value), + mkNotNullOrUndefined(stringRef), + stringType, + mkNotNullOrUndefined(charsRef), + backingType, + contents, + ) } + scope.assert(constraints) ?: return null scope.doWithState { boundedStringBackingRefs += stringRef } @@ -233,5 +235,5 @@ fun TsContext.readStaticField( val instance = scope.calcOnState { getStaticInstance(clazz) } // Read the field. - return readField(scope, null, instance, field, hierarchy) + return resolveField(scope, null, instance, field, hierarchy) } 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 2b94125e0f..9d42276687 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 @@ -55,10 +55,12 @@ import org.usvm.machine.expr.TsExprApproximationResult import org.usvm.machine.expr.TsExprResolver import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.expr.checkUndefinedOrNullPropertyRead +import org.usvm.machine.expr.ensureTruthinessSupported import org.usvm.machine.expr.handleAssignToArrayIndex import org.usvm.machine.expr.handleAssignToInstanceField import org.usvm.machine.expr.handleAssignToLocal import org.usvm.machine.expr.handleAssignToStaticField +import org.usvm.machine.expr.mkNotNullOrUndefined import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.expr.readGlobal import org.usvm.machine.expr.tryApproximateInstanceCall @@ -464,7 +466,9 @@ class TsInterpreter( expr.asExpr(ctx.boolSort) } else { ctx.mkTruthyExpr(expr, scope) - } ?: return + } + + scope.ensureTruthinessSupported(expr) ?: return observer?.onIfStatementWithResolvedCondition(simpleValueResolver, stmt, boolExpr, scope) @@ -774,8 +778,7 @@ class TsInterpreter( val thisInstanceRef = mkRegisterStackLValue(addressSort, thisIdx) val thisRef = state.memory.read(thisInstanceRef).asExpr(addressSort) - state.pathConstraints += mkNot(mkHeapRefEq(thisRef, mkTsNullValue())) - state.pathConstraints += mkNot(mkHeapRefEq(thisRef, mkUndefinedValue())) + state.pathConstraints += mkNotNullOrUndefined(thisRef) // TODO not equal but subtype for abstract/interfaces state.pathConstraints += state.memory.types.evalTypeEquals(thisRef, method.enclosingClass!!.type) @@ -789,9 +792,10 @@ class TsInterpreter( } val parameterType = param.type - if (parameterType is EtsRefType) run { - state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue())) - state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue())) + run { + if (parameterType !is EtsRefType) return@run + + state.pathConstraints += mkNotNullOrUndefined(ref) if (parameterType is EtsArrayType) { state.pathConstraints += state.memory.types.evalIsSubtype(ref, parameterType) @@ -824,8 +828,7 @@ class TsInterpreter( state.pathConstraints += mkHeapRefEq(ref, mkUndefinedValue()) } if (parameterType == EtsStringType) { - state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue())) - state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue())) + state.pathConstraints += mkNotNullOrUndefined(ref) state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType) 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 4890a87333..1d7ac99326 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 @@ -18,6 +18,8 @@ import org.usvm.isFalse import org.usvm.isTrue 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.mkNumericExpr import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.interpreter.TsStepScope @@ -57,8 +59,8 @@ private fun TsContext.stringValueEquals( // 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())) + val lhsNullish = mkIsNullOrUndefined(lhs) + val rhsNullish = mkIsNullOrUndefined(rhs) if (missingBacking) { val supportedWithoutBacking = mkOr( mkNot(activeGuard), @@ -1117,7 +1119,9 @@ sealed interface TsBinaryOperator { ): UExpr<*>? { check(lhs.isFakeObject() || rhs.isFakeObject()) - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) ?: return null + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) + scope.ensureTruthinessSupported(lhs) ?: return null + return scope.calcOnState { iteWriteIntoFakeObject(scope, lhsTruthyExpr, rhs, lhs) } @@ -1130,7 +1134,9 @@ sealed interface TsBinaryOperator { ): UExpr<*>? { check(!lhs.isFakeObject() && !rhs.isFakeObject()) - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) ?: return null + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) + scope.ensureTruthinessSupported(lhs) ?: return null + return scope.calcOnState { iteWriteIntoFakeObject(scope, lhsTruthyExpr, rhs, lhs) } @@ -1169,7 +1175,9 @@ sealed interface TsBinaryOperator { ): UExpr<*>? { check(lhs.isFakeObject() || rhs.isFakeObject()) - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) ?: return null + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) + scope.ensureTruthinessSupported(lhs) ?: return null + return iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs) } @@ -1180,7 +1188,9 @@ sealed interface TsBinaryOperator { ): UExpr<*>? { check(!lhs.isFakeObject() && !rhs.isFakeObject()) - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) ?: return null + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) + scope.ensureTruthinessSupported(lhs) ?: return null + 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 81c1ad4cd0..4c54e04bba 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 @@ -8,6 +8,7 @@ import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.USort import org.usvm.machine.TsContext +import org.usvm.machine.expr.ensureTruthinessSupported import org.usvm.machine.expr.mkNumericExpr import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.interpreter.TsStepScope @@ -60,8 +61,8 @@ sealed interface TsUnaryOperator { override fun TsContext.resolveFp( arg: UExpr, scope: TsStepScope, - ): UBoolExpr? { - val truthy = mkTruthyExpr(arg, scope) ?: return null + ): UBoolExpr { + val truthy = mkTruthyExpr(arg, scope) return mkNot(truthy) } @@ -69,7 +70,9 @@ sealed interface TsUnaryOperator { arg: UExpr, scope: TsStepScope, ): UBoolExpr? { - val truthy = mkTruthyExpr(arg, scope) ?: return null + val truthy = mkTruthyExpr(arg, scope) + scope.ensureTruthinessSupported(arg) ?: return null + return mkNot(truthy) } @@ -77,7 +80,9 @@ sealed interface TsUnaryOperator { arg: UConcreteHeapRef, scope: TsStepScope, ): UBoolExpr? { - val truthy = mkTruthyExpr(arg, scope) ?: return null + val truthy = mkTruthyExpr(arg, scope) + scope.ensureTruthinessSupported(arg) ?: return null + 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 c55f84de76..55a87920ed 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,7 @@ import org.usvm.UNullRef import org.usvm.USymbolicHeapRef import org.usvm.api.evalTypeEquals import org.usvm.api.typeStreamOf +import org.usvm.machine.expr.mkNotNullOrUndefined import org.usvm.machine.interpreter.TsStepScope import org.usvm.solver.UUnsatResult import org.usvm.types.singleOrNull @@ -58,10 +59,7 @@ internal fun TsStepScope.prepareRefinedStringBackings(): Unit? { 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) + mkAnd(stringType, mkNotNullOrUndefined(ref)) } alternative.pathConstraints += ctx.mkNot(stringCondition) 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 130d9e5b87..7e0054f6df 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsDynamicTruthinessTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsDynamicTruthinessTest.kt @@ -49,7 +49,7 @@ class TsDynamicTruthinessTest : TsMethodTestRunner() { invariants = arrayOf({ _, result -> result.number == 1.0 }), ) - val names = setOf("anyTruthy", "anyNegated", "anyObjectTruthy", "objectTruthy") + val names = setOf("anyTruthy", "anyNegated", "anyAnd", "anyOr", "anyObjectTruthy", "objectTruthy") val methods = scene.projectClasses.single { it.name == "SymbolicStringInput" }.methods .filter { it.name in names } .associateBy { it.name } diff --git a/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts b/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts index fc6001bd4b..5e9e214fd3 100644 --- a/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts +++ b/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts @@ -125,6 +125,16 @@ class SymbolicStringInput { return 0; } + anyAnd(value: any): number { + if (value && true) return 1; + return 0; + } + + anyOr(value: any): number { + if (value || false) return 1; + return 0; + } + anyNegated(value: any): number { if (!value) return 1; return 0; From f5f28249e64f02ce197e08a078fe6a0fee25034e Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 9 Oct 2026 13:11:33 +0300 Subject: [PATCH 3/3] [TS] Reuse nullish predicate in non-nullish checks --- .../src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) 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 d164d1fda5..de1a7869a8 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 @@ -10,6 +10,7 @@ import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.UIteExpr +import org.usvm.UOrExpr import org.usvm.USort import org.usvm.USymbolicHeapRef import org.usvm.api.allocateConcreteRef @@ -299,12 +300,13 @@ fun TsContext.mkIsNullOrUndefined(ref: UHeapRef): UBoolExpr { } fun TsContext.mkNotNullOrUndefined(ref: UHeapRef): UBoolExpr { - checkNotFake(ref) + val isNullOrUndefined = mkIsNullOrUndefined(ref) - val isNull = mkHeapRefEq(ref, mkTsNullValue()) - val isUndefined = mkHeapRefEq(ref, mkUndefinedValue()) // Preserve the explicit disequalities when this expression is composed into path guards. - return mkAnd(mkNot(isNull), mkNot(isUndefined)) + return when (isNullOrUndefined) { + is UOrExpr -> mkAnd(isNullOrUndefined.args.map(::mkNot)) + else -> mkNot(isNullOrUndefined) + } } fun TsContext.checkUndefinedOrNullPropertyRead(