From c19dc1c5b51ce60057f31b65cd746804e5c1e338 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 00:22:19 +0300 Subject: [PATCH 1/3] Support linear RegExp literals in core runtime test and match calls --- .../usvm/machine/expr/CallApproximations.kt | 3 + .../kotlin/org/usvm/machine/expr/ReadField.kt | 3 + .../org/usvm/machine/expr/RegExpCalls.kt | 236 ++++++++++++++++++ .../org/usvm/machine/expr/RegExpMatching.kt | 138 ++++++++++ .../org/usvm/machine/expr/RegExpPattern.kt | 155 ++++++++++++ .../org/usvm/machine/expr/TsExprResolver.kt | 6 +- .../org/usvm/machine/expr/WriteField.kt | 8 + .../kotlin/org/usvm/machine/state/TsState.kt | 3 + .../usvm/machine/expr/RegExpRuntimeTest.kt | 201 +++++++++++++++ .../test/resources/models/RegExpRuntime.ts | 109 ++++++++ .../models/RuntimeLimitationBoundaries.ts | 2 +- 11 files changed, 858 insertions(+), 6 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/RegExpCalls.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/RegExpMatching.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/RegExpPattern.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/expr/RegExpRuntimeTest.kt create mode 100644 usvm-ts/src/test/resources/models/RegExpRuntime.ts 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 870048878a..59788d82b3 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 @@ -153,6 +153,9 @@ internal fun TsExprResolver.tryApproximateInstanceCall( val instance = stmt.instance if (!ensureSupportedObjectMutation(stmt)) return TsExprApproximationResult.ResolveFailure + val regularExpression = tryApproximateRegExpCall(stmt) + if (regularExpression !is TsExprApproximationResult.NoApproximation) return regularExpression + val iterator = tryApproximateBuiltinIteratorCall(stmt) if (iterator !is TsExprApproximationResult.NoApproximation) return iterator 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 052820007b..42e22e1935 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 @@ -128,6 +128,9 @@ internal fun TsContext.resolveField( ): UExpr<*>? { checkNotFake(instance) val receiver = resolveHeapRef(scope, instance) ?: return null + val intrinsicRegExp = receiver is UConcreteHeapRef && scope.calcOnState { receiver in regularExpressions } + if (intrinsicRegExp) return readRegExpField(scope, receiver as UConcreteHeapRef, field.name) + if (isDateModelTimestamp(scope = scope, instance = receiver, field = field)) { val timestamp = dateModelTimestampLValue(receiver) return scope.calcOnState { memory.read(timestamp) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/RegExpCalls.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/RegExpCalls.kt new file mode 100644 index 0000000000..0afa233aa3 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/RegExpCalls.kt @@ -0,0 +1,236 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import io.ksmt.utils.cast +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.USort +import org.usvm.api.initializeArray +import org.usvm.isTrue +import org.usvm.machine.TsContext +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.machine.TsVirtualMethodCallStmt +import org.usvm.machine.call.hasBuiltinGlobalOwner +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsState +import org.usvm.sizeSort +import org.usvm.util.copyStringRange +import org.usvm.util.markDenseArrayOwnSlots +import org.usvm.util.markDenseInputArray +import org.usvm.util.mkFieldLValue +import org.usvm.util.stringLength + +private val regExpMatchArrayType = EtsArrayType(EtsStringType, dimensions = 1) +private val regExpFlagProperties = setOf( + "global", + "ignoreCase", + "multiline", + "dotAll", + "unicode", + "sticky", + "hasIndices", + "unicodeSets", +) +private val regExpReadOnlyProperties = regExpFlagProperties + setOf("source", "flags") + +internal fun TsExprResolver.allocateRegExpLiteral(type: EtsClassType): UConcreteHeapRef = scope.calcOnState { + val reference = memory.allocConcrete(type) + regularExpressions += reference to null + reference +} + +/** Core runtime semantics: available independently of the optional unknown-call model catalog. */ +internal fun TsExprResolver.tryApproximateRegExpCall(stmt: TsVirtualMethodCallStmt): TsExprApproximationResult { + val target = stmt.args.firstOrNull() as? UConcreteHeapRef + val targetsRegExp = target != null && scope.calcOnState { target in regularExpressions } + val reflectiveBuiltin = hasBuiltinGlobalOwner(stmt.call.instance, stmt.call.callee, expectedName = "Object") || + hasBuiltinGlobalOwner(stmt.call.instance, stmt.call.callee, expectedName = "Reflect") + if (targetsRegExp && reflectiveBuiltin) { + return unsupportedRegExp("Reflective operations on intrinsic RegExp objects are unsupported") + } + + val receiver = stmt.instance as? UConcreteHeapRef + val intrinsicRegExp = receiver != null && scope.calcOnState { receiver in regularExpressions } + if (intrinsicRegExp) { + val reference = checkNotNull(receiver) + val method = stmt.call.callee.name + val overridden = scope.calcOnState { (reference to method) in writtenConcreteFields } + if (overridden) return TsExprApproximationResult.NoApproximation + return when (method) { + CONSTRUCTOR_NAME -> initializeRegExpLiteral(reference, stmt) + "test" -> testRegExp(reference, stmt) + else -> unsupportedRegExp("Only intrinsic RegExp.test and String.match are supported") + } + } + + if (stmt.call.callee.name != "match") return TsExprApproximationResult.NoApproximation + val expression = stmt.args.firstOrNull() as? UConcreteHeapRef + val knownExpression = expression != null && scope.calcOnState { expression in regularExpressions } + if (!knownExpression) return TsExprApproximationResult.NoApproximation + val backedReceiver = stmt.instance.sort == ctx.addressSort && scope.calcOnState { + stmt.instance.asExpr(ctx.addressSort) in boundedStringBackingRefs + } + if (!backedReceiver) return TsExprApproximationResult.NoApproximation + + return matchRegExp(checkNotNull(expression), stmt) +} + +private fun TsExprResolver.initializeRegExpLiteral( + reference: UConcreteHeapRef, + stmt: TsVirtualMethodCallStmt, +): TsExprApproximationResult { + if (stmt.args.size != 2) return unsupportedRegExp("RegExp literal requires constant pattern and flags") + val patternRef = stmt.args[0] as? UConcreteHeapRef + val flagsRef = stmt.args[1] as? UConcreteHeapRef + val pattern = patternRef?.let(ctx::getStringConstantValue) + val flags = flagsRef?.let(ctx::getStringConstantValue) + if (pattern == null || flags != "") { + return unsupportedRegExp("Only constant RegExp patterns without flags are supported") + } + if (parseRegExpPattern(pattern) == null) { + return unsupportedRegExp("RegExp pattern requires unsupported syntax or backtracking: $pattern") + } + + scope.doWithState { + regularExpressions += reference to pattern + initializeRegExpField(reference = reference, name = "lastIndex", value = ctx.mkFp64(0.0)) + } + return TsExprApproximationResult.SuccessfulApproximation(reference) +} + +private fun TsExprResolver.testRegExp( + reference: UConcreteHeapRef, + stmt: TsVirtualMethodCallStmt, +): TsExprApproximationResult { + val string = stmt.args.firstOrNull() + val result = computeRegExpMatch(reference, string) ?: return TsExprApproximationResult.ResolveFailure + return TsExprApproximationResult.SuccessfulApproximation(result.success) +} + +private fun TsExprResolver.matchRegExp( + reference: UConcreteHeapRef, + stmt: TsVirtualMethodCallStmt, +): TsExprApproximationResult = with(ctx) { + val result = computeRegExpMatch(reference, stmt.instance) ?: return TsExprApproximationResult.ResolveFailure + val matched = scope.calcOnState { models.first().eval(result.success).isTrue } + val selectedBranch = if (matched) result.success else mkNot(result.success) + scope.fork(selectedBranch) ?: return TsExprApproximationResult.ResolveFailure + if (!matched) return TsExprApproximationResult.SuccessfulApproximation(mkTsNullValue()) + + val string = stmt.instance.asExpr(addressSort) + val array = scope.calcOnState { createRegExpMatchArray(string, result) } + TsExprApproximationResult.SuccessfulApproximation(array) +} + +private fun TsExprResolver.computeRegExpMatch( + reference: UConcreteHeapRef, + value: UExpr<*>?, +): RegExpMatch? = with(ctx) { + val overriddenExec = scope.calcOnState { (reference to "exec") in writtenConcreteFields } + if (overriddenExec) { + unsupportedRegExp("RegExp matching through a custom exec callback is unsupported") + return null + } + + val source = scope.calcOnState { regularExpressions[reference] } + val pattern = source?.let(::parseRegExpPattern) + if (pattern == null) { + unsupportedRegExp("RegExp literal has not been initialized") + return null + } + val string = value?.takeIf { it.sort == ctx.addressSort && !it.isFakeObject() }?.asExpr(ctx.addressSort) + val bound = string?.let { scope.calcOnState { boundedStringBackingRefs[it] } } + if (string == null || bound == null) { + unsupportedRegExp( + "RegExp matching requires a primitive string with modeled UTF-16 backing; coercion is unsupported" + ) + return null + } + + val length = scope.calcOnState { stringLength(string) } + ensureLengthBounds(scope = scope, length = length, maxLength = bound) ?: return null + return scope.calcOnState { RegExpMatcher(state = this, string = string, bound = bound).match(pattern) } +} + +private fun TsState.createRegExpMatchArray(string: UHeapRef, result: RegExpMatch): UConcreteHeapRef = with(ctx) { + val fullMatch = copyStringRange(receiver = string, from = result.start, to = result.end) + val captures = result.captures.toSortedMap().values.map { capture -> + val text = copyStringRange(receiver = string, from = capture.start, to = capture.end) + mkIte(capture.present, text, mkUndefinedValue()) + } + val array = memory.allocConcrete(regExpMatchArrayType) + memory.initializeArray( + arrayHeapRef = array, + type = arrayDescriptorOf(regExpMatchArrayType), + sort = addressSort, + sizeSort = sizeSort, + contents = (listOf(fullMatch) + captures).asSequence(), + ) + markDenseInputArray(array = array, type = regExpMatchArrayType) + markDenseArrayOwnSlots(array = array, length = mkBv(captures.size + 1), capacity = captures.size + 1) + val index = mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), result.start.cast(), signed = true) + initializeRegExpField(reference = array, name = "index", value = index) + initializeRegExpField(reference = array, name = "input", value = string) + initializeRegExpField(reference = array, name = "groups", value = mkUndefinedValue()) + array +} + +private fun TsState.initializeRegExpField( + reference: UConcreteHeapRef, + name: String, + value: UExpr, +) = with(ctx) { + memory.write(mkFieldLValue(value.sort, reference, name), value, guard = trueExpr) + writtenConcreteFields += reference to name + writtenObjectLiteralFieldSorts = writtenObjectLiteralFieldSorts.put(reference to name, value.sort, ownership) +} + +/** Runtime RegExp properties are independent of unavailable structural SDK declarations. */ +internal fun TsContext.readRegExpField(scope: TsStepScope, reference: UConcreteHeapRef, name: String): UExpr<*>? { + val source = scope.calcOnState { regularExpressions[reference] } + if (source == null) return null + + return when (name) { + "source" -> scope.calcOnState { mkInitializedStringConstant(source.ifEmpty { "(?:)" }) } + "flags" -> scope.calcOnState { mkInitializedStringConstant("") } + in regExpFlagProperties -> falseExpr + else -> { + val sort = scope.calcOnState { writtenObjectLiteralFieldSorts[reference to name] } + if (sort == null) { + scope.doWithState { + terminateAsUnsupported(reason = "REGULAR_EXPRESSION_LITERAL: RegExp property $name is unsupported") + } + null + } else { + scope.calcOnState { memory.read(mkFieldLValue(sort, reference, name)) } + } + } + } +} + +internal fun TsContext.writeRegExpField( + scope: TsStepScope, + reference: UConcreteHeapRef, + name: String, + value: UExpr<*>, +): Unit? { + if (name in regExpReadOnlyProperties || name == "__proto__") { + scope.doWithState { + terminateAsUnsupported(reason = "REGULAR_EXPRESSION_LITERAL: RegExp property write $name is unsupported") + } + return null + } + + scope.doWithState { initializeRegExpField(reference = reference, name = name, value = value) } + return Unit +} + +private fun TsExprResolver.unsupportedRegExp(detail: String): TsExprApproximationResult { + stopRuntimeFeatureLimitation(reason = TsRuntimeFeatureLimitationReason.REGULAR_EXPRESSION_LITERAL, detail = detail) + return TsExprApproximationResult.ResolveFailure +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/RegExpMatching.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/RegExpMatching.kt new file mode 100644 index 0000000000..f9926bd742 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/RegExpMatching.kt @@ -0,0 +1,138 @@ +package org.usvm.machine.expr + +import io.ksmt.sort.KBv16Sort +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.machine.TsSizeSort +import org.usvm.machine.state.TsState +import org.usvm.util.mkStringBackingElementLValue +import org.usvm.util.stringCharacters +import org.usvm.util.stringLength + +internal data class RegExpCapture( + val present: UBoolExpr, + val start: UExpr, + val end: UExpr, +) + +internal data class RegExpMatch( + val success: UBoolExpr, + val start: UExpr, + val end: UExpr, + val captures: Map, +) + +/** One bounded scan per greedy run; fixed unanchored patterns use a leftmost-match ITE chain. */ +internal class RegExpMatcher(private val state: TsState, private val string: UHeapRef, private val bound: Int) { + private val ctx = state.ctx + private val length = state.stringLength(string) + private val characters = state.stringCharacters(string) + + fun match(pattern: RegExpPattern): RegExpMatch = with(ctx) { + if (pattern.anchoredStart) return matchAt(pattern, start = 0) + + check(!pattern.hasRepetition) { "Unanchored repetition must be rejected before matching" } + var result = RegExpMatch(falseExpr, mkBv(0), mkBv(0), emptyMap()) + for (start in bound downTo 0) { + val candidate = matchAt(pattern, start) + val captures = candidate.captures.mapValues { (capture, value) -> + val previous = result.captures[capture] ?: RegExpCapture(falseExpr, mkBv(0), mkBv(0)) + RegExpCapture( + present = mkIte(candidate.success, value.present, previous.present), + start = mkIte(candidate.success, value.start, previous.start), + end = mkIte(candidate.success, value.end, previous.end), + ) + } + result = RegExpMatch( + success = mkOr(candidate.success, result.success), + start = mkIte(candidate.success, candidate.start, result.start), + end = mkIte(candidate.success, candidate.end, result.end), + captures = captures, + ) + } + result + } + + private fun matchAt(pattern: RegExpPattern, start: Int): RegExpMatch = with(ctx) { + val result = sequence(pattern.parts, mkBv(start)) + // Without /m, ECMAScript $ requires the absolute end, including after a final newline. + val endMatches = if (pattern.anchoredEnd) mkEq(result.end, length) else trueExpr + val validStart = mkBvSignedLessOrEqualExpr(mkBv(start), length) + result.copy(success = mkAnd(validStart, result.success, endMatches)) + } + + private fun sequence(parts: List, start: UExpr): RegExpMatch = with(ctx) { + var result = RegExpMatch(trueExpr, start, start, emptyMap()) + for (part in parts) { + val next = when (part) { + is RegExpPart.Atom -> atom(part, result.end) + is RegExpPart.Group -> group(part, result.end) + } + result = result.copy( + success = mkAnd(result.success, next.success), + end = next.end, + captures = result.captures + next.captures, + ) + } + result + } + + private fun group(group: RegExpPart.Group, start: UExpr): RegExpMatch = with(ctx) { + var result = sequence(group.parts, start) + val capture = group.capture + if (capture != null) { + result = result.copy(captures = result.captures + (capture to RegExpCapture(trueExpr, start, result.end))) + } + if (!group.optional) return result + + result.copy( + success = trueExpr, + end = mkIte(result.success, result.end, start), + captures = result.captures.mapValues { (_, value) -> + RegExpCapture( + present = mkAnd(result.success, value.present), + start = mkIte(result.success, value.start, start), + end = mkIte(result.success, value.end, start), + ) + }, + ) + } + + private fun atom(atom: RegExpPart.Atom, start: UExpr): RegExpMatch = with(ctx) { + if (!atom.repeated) { + val matches = matchesAt(atom, start) + return RegExpMatch(matches, start, mkBvAddExpr(start, mkBv(1)), emptyMap()) + } + + var active: UBoolExpr = trueExpr + var end = start + for (offset in 0 until bound) { + val index = mkBvAddExpr(start, mkBv(offset)) + active = mkAnd(active, matchesAt(atom, index)) + end = mkIte(active, mkBvAddExpr(index, mkBv(1)), end) + } + RegExpMatch(mkBvSignedGreaterExpr(end, start), start, end, emptyMap()) + } + + private fun matchesAt(atom: RegExpPart.Atom, index: UExpr): UBoolExpr = with(ctx) { + val unit = state.memory.read(mkStringBackingElementLValue(characters, index)) + val withinLength = mkBvSignedLessExpr(index, length) + mkAnd(withinLength, characterMatches(atom, unit)) + } + + private fun characterMatches(atom: RegExpPart.Atom, value: UExpr): UBoolExpr = with(ctx) { + val alternatives = atom.ranges.map { range -> + if (range.first == range.last) { + mkEq(value, mkBv(range.first, bv16Sort)) + } else { + val lowerBound = mkBv(range.first, bv16Sort) + val upperBound = mkBv(range.last, bv16Sort) + val aboveLowerBound = mkBvUnsignedGreaterOrEqualExpr(value, lowerBound) + val belowUpperBound = mkBvUnsignedLessOrEqualExpr(value, upperBound) + mkAnd(aboveLowerBound, belowUpperBound) + } + } + mkOr(alternatives) + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/RegExpPattern.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/RegExpPattern.kt new file mode 100644 index 0000000000..52479fdbeb --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/RegExpPattern.kt @@ -0,0 +1,155 @@ +package org.usvm.machine.expr + +/** Linear UTF-16 patterns whose greedy repetitions never need backtracking. */ +internal data class RegExpPattern( + val parts: List, + val anchoredStart: Boolean, + val anchoredEnd: Boolean, + val captureCount: Int, +) { + val hasRepetition: Boolean get() = parts.atoms().any { it.repeated } +} + +internal sealed interface RegExpPart { + data class Atom(val ranges: List, val repeated: Boolean = false) : RegExpPart + data class Group(val parts: List, val capture: Int?, val optional: Boolean) : RegExpPart +} + +internal fun parseRegExpPattern(source: String): RegExpPattern? = RegExpPatternParser(source).parse() + +private const val MAX_PATTERN_LENGTH = 256 +private const val MAX_PATTERN_ATOMS = 64 + +private class RegExpPatternParser(private val source: String) { + private var index = 0 + private var captureCount = 0 + + fun parse(): RegExpPattern? { + if (source.length > MAX_PATTERN_LENGTH) return null + + val anchoredStart = source.startsWith('^') + if (anchoredStart) index++ + + val parts = sequence() ?: return null + val anchoredEnd = source.getOrNull(index) == '$' + if (anchoredEnd) index++ + if (index != source.length) return null + + val atoms = parts.atoms() + if (atoms.size > MAX_PATTERN_ATOMS) return null + + val needsBacktracking = atoms.zipWithNext().any { (previous, next) -> + previous.repeated && previous.ranges.any { left -> next.ranges.any { right -> left.overlaps(right) } } + } + val hasUnanchoredRepetition = !anchoredStart && atoms.any { it.repeated } + val unsupportedOptionalSuffix = !validOptionalSuffix(parts) + if (needsBacktracking || hasUnanchoredRepetition || unsupportedOptionalSuffix) return null + + return RegExpPattern(parts, anchoredStart, anchoredEnd, captureCount) + } + + private fun sequence(): List? { + val parts = mutableListOf() + while (index < source.length && source[index] != ')' && source[index] != '$') { + val part = if (source[index] == '(') group() else atom() + if (part == null) return null + parts += part + } + return parts + } + + private fun group(): RegExpPart.Group? { + index++ + val capturing = !source.startsWith("?:", startIndex = index) + val capture = if (capturing) captureCount++ else null + if (!capturing) index += 2 + + val parts = sequence() ?: return null + if (source.getOrNull(index) != ')') return null + index++ + + val optional = source.getOrNull(index) == '?' + if (optional) index++ + return RegExpPart.Group(parts, capture, optional) + } + + private fun atom(): RegExpPart.Atom? { + val ranges = if (source[index] == '[') characterClass() else character() + if (ranges == null) return null + + val repeated = source.getOrNull(index) == '+' + if (repeated) index++ + return RegExpPart.Atom(ranges, repeated) + } + + private fun characterClass(): List? { + index++ + if (source.getOrNull(index) == '^') return null + + val ranges = mutableListOf() + while (index < source.length && source[index] != ']') { + val first = character(inClass = true) ?: return null + val hasRange = source.getOrNull(index) == '-' && source.getOrNull(index + 1) != ']' + if (hasRange) { + index++ + val last = character(inClass = true) ?: return null + val start = first.singleOrNull() ?: return null + val end = last.singleOrNull() ?: return null + if (start.first != start.last || end.first != end.last || start.first > end.first) return null + ranges += start.first..end.first + } else { + ranges += first + } + } + if (source.getOrNull(index) != ']' || ranges.isEmpty()) return null + index++ + return ranges + } + + private fun character(inClass: Boolean = false): List? { + val char = source.getOrNull(index) ?: return null + index++ + if (char == '\\') { + val escaped = source.getOrNull(index) ?: return null + index++ + return when (escaped) { + 'd' -> listOf('0'.code..'9'.code) + 'w' -> listOf('0'.code..'9'.code, 'A'.code..'Z'.code, '_'.code..'_'.code, 'a'.code..'z'.code) + 'n' -> listOf('\n'.code..'\n'.code) + 'r' -> listOf('\r'.code..'\r'.code) + 't' -> listOf('\t'.code..'\t'.code) + in "\\/.*+?()[]{}^$|-" -> listOf(escaped.code..escaped.code) + else -> null + } + } + if (!inClass && char in ".*+?()[]{}^$|") return null + return listOf(char.code..char.code) + } +} + +private fun List.atoms(): List = flatMap { part -> + when (part) { + is RegExpPart.Atom -> listOf(part) + is RegExpPart.Group -> part.parts.atoms() + } +} + +private fun IntRange.overlaps(other: IntRange): Boolean = first <= other.last && other.first <= last + +/** An optional fixed suffix cannot force an earlier greedy run to backtrack. */ +private fun validOptionalSuffix(parts: List, suffixAllowed: Boolean = true): Boolean = + parts.withIndex().all { (index, part) -> + when (part) { + is RegExpPart.Atom -> true + is RegExpPart.Group -> { + val lastPart = suffixAllowed && index == parts.lastIndex + if (part.optional) { + val atoms = part.parts.atoms() + lastPart && atoms.isNotEmpty() && atoms.none { it.repeated } && + validOptionalSuffix(part.parts, suffixAllowed = false) + } else { + validOptionalSuffix(part.parts, suffixAllowed = lastPart) + } + } + } + } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index e2a3f7ebab..4483abd36e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -1544,11 +1544,7 @@ class TsExprResolver( ) val intrinsicRegex = hasRegexName && hasIntrinsicOwner if (intrinsicRegex) { - stopRuntimeFeatureLimitation( - reason = TsRuntimeFeatureLimitationReason.REGULAR_EXPRESSION_LITERAL, - detail = "Intrinsic RegExp allocation has no runtime model", - ) - return@with null + return@with allocateRegExpLiteral(checkNotNull(classType)) } // Try to resolve the concrete type if possible. diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index 2e53177a5f..930993b362 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -10,6 +10,7 @@ import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsStaticFieldRef import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort @@ -211,6 +212,13 @@ fun TsContext.assignToInstanceField( ): Unit? { // Unwrap to get non-fake reference. val unwrappedInstance = resolveHeapRef(scope, instance.unwrapRef(scope)) ?: return null + val intrinsicRegExp = unwrappedInstance is UConcreteHeapRef && scope.calcOnState { + unwrappedInstance in regularExpressions + } + if (intrinsicRegExp) { + return writeRegExpField(scope, unwrappedInstance as UConcreteHeapRef, field.name, expr) + } + if (isDateModelTimestamp(scope = scope, instance = unwrappedInstance, field = field)) { val timestamp = dateModelTimestampLValue(unwrappedInstance) return scope.doWithState { 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 0f164cde7f..cc8ef01b10 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 @@ -90,6 +90,8 @@ class TsState( var capturedInstanceCalls: UPersistentHashMap = persistentHashMapOf(), internal var arrayIterators: Map = emptyMap(), internal var stringIterators: Map = emptyMap(), + /** Intrinsic literal allocations; null until their constant constructor arguments are initialized. */ + internal var regularExpressions: Map = emptyMap(), internal var iteratorResults: Map = emptyMap(), internal var knownArrayPropertyPresence: Set = emptySet(), internal var unsupportedIteratorArrays: Set = emptySet(), @@ -379,6 +381,7 @@ class TsState( arrayIterators = arrayIterators, iteratorResults = iteratorResults, stringIterators = stringIterators, + regularExpressions = regularExpressions, initializedArrayIndices = initializedArrayIndices, unsupportedIteratorArrays = unsupportedIteratorArrays, knownArrayPropertyPresence = knownArrayPropertyPresence, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RegExpRuntimeTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RegExpRuntimeTest.kt new file mode 100644 index 0000000000..48b2f4958d --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RegExpRuntimeTest.kt @@ -0,0 +1,201 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.call.TsResidualCallPolicy +import org.usvm.machine.call.TsUnknownCallModelSelection +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import org.usvm.util.jsString +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue + +class RegExpRuntimeTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/RegExpRuntime.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + override val tsOptions = TsOptions( + maxArraySize = 12, + unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet()), + unknownCallFallback = TsResidualCallPolicy.STOP_PATH, + ) + + override val runner: (EtsMethod, UMachineOptions) -> List = { target, machineOptions -> + analyze(target = target, machineOptions = machineOptions, runtimeOptions = tsOptions) + } + + init { + options = options.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + } + + @Test + fun `symbolic DateUtils expression distinguishes failure and optional captures`() { + discoverProperties( + method = method("dateMath"), + { _, result -> result.number == 0.0 }, + { _, result -> result.number == 1.0 }, + { _, result -> result.number == 2.0 }, + invariants = arrayOf({ _, result -> result.number in 0.0..2.0 }), + ) + } + + @Test + fun `symbolic fixed search and anchored runs find matches and failures`() { + for (name in listOf("testLetters", "testRepeated")) { + discoverProperties( + method = method(name), + { _, result -> result.value }, + { _, result -> !result.value }, + ) + } + } + + @Test + fun `anchored greedy run supports the default thousand code unit bound`() { + val tests = analyze( + target = method("testRepeated"), + machineOptions = options, + runtimeOptions = tsOptions.copy(maxArraySize = 1_000), + ) + val values = tests.map { assertIs(it.returnValue).value }.toSet() + + assertEquals(setOf(false, true), values) + } + + @Test + fun `captures metadata UTF16 end anchors and fresh arrays match native semantics`() { + for (name in constantMethods) { + discoverProperties( + method = method(name), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + discoverProperties( + method = method("overriddenTest"), + { result -> !result.value }, + invariants = arrayOf({ result -> !result.value }), + ) + discoverProperties( + method = method("customMatch"), + { result -> result.number == 7.0 }, + invariants = arrayOf({ result -> result.number == 7.0 }), + ) + } + + @Test + fun `core RegExp semantics are the same for all model and fallback profiles`() { + for (selection in listOf(TsUnknownCallModelSelection.All, TsUnknownCallModelSelection.Only(emptySet()))) { + for (fallback in TsResidualCallPolicy.entries) { + val runtimeOptions = tsOptions.copy( + unknownCallModelSelection = selection, + unknownCallFallback = fallback, + ) + val tests = analyze(method("captures"), options, runtimeOptions) + + assertTrue(tests.isNotEmpty()) + assertTrue(tests.all { assertIs(it.returnValue).value }) + } + } + } + + @Test + fun `unsupported syntax flags and coercion remain explicit limitations`() { + val names = listOf( + "unsupportedFlags", + "unsupportedBacktracking", + "unsupportedCoercion", + "unsupportedUnanchoredRun", + "unsupportedExecOverride", + "unsupportedPropertyWrite", + ) + for (name in names) { + TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> + val outcome = machine.analyzeWithOutcome(listOf(method(name))) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty(), name) + assertTrue(outcome.unsupportedPaths.any { "REGULAR_EXPRESSION_LITERAL" in it }, "$name: $outcome") + } + } + } + + @Test + fun `every generated witness replays against Node RegExp`() { + val names = constantMethods + listOf("dateMath", "testLetters", "testRepeated", "overriddenTest", "customMatch") + val script = buildString { + appendLine(source.readText()) + for (name in names) { + val tests = runner(method(name), options) + assertTrue(tests.isNotEmpty(), name) + for (test in tests) { + val args = test.before.parameters.joinToString { jsValue(it) } + val expected = jsValue(test.returnValue) + appendLine("if (RegExpRuntime.$name($args) !== $expected) throw Error('$name');") + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "regexp-runtime", + timeoutMessage = "RegExp runtime replay timed out", + ) + } + + private fun analyze(target: EtsMethod, machineOptions: UMachineOptions, runtimeOptions: TsOptions): List = + TsMachine(scene = scene, options = machineOptions, tsOptions = runtimeOptions).use { machine -> + val outcome = machine.analyzeWithOutcome(listOf(target)) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${target.name}: ${outcome.unsupportedPaths}") + outcome.states.map { state -> TsTestResolver().resolve(target, state) } + } + + private fun method(name: String): EtsMethod = getMethod(methodName = name, className = "RegExpRuntime") + + private fun jsValue(value: TsTestValue): String = when (value) { + is TsTestValue.TsString -> jsString(value.value) + is TsTestValue.TsBoolean -> value.value.toString() + else -> assertIs(value).number.toString() + } + + companion object { + private val constantMethods = listOf( + "captures", + "missingCapture", + "leftmost", + "emptyCapture", + "finalNewlines", + "utf16AndEscapes", + "freshResults", + "lastIndex", + "literalProperties", + ) + } +} diff --git a/usvm-ts/src/test/resources/models/RegExpRuntime.ts b/usvm-ts/src/test/resources/models/RegExpRuntime.ts new file mode 100644 index 0000000000..852e96c27f --- /dev/null +++ b/usvm-ts/src/test/resources/models/RegExpRuntime.ts @@ -0,0 +1,109 @@ +export class RegExpRuntime { + static dateMath(value: string): number { + const match = value.match(/^now([+-])(\d+)([mhdMywQ])(?:\/(\w))?$/); + if (match === null) return 0; + if (match[4] === undefined) return 1; + return 2; + } + + static captures(): boolean { + const match = "now-15m/d".match(/^now([+-])(\d+)([mhdMywQ])(?:\/(\w))?$/); + if (match === null) return false; + return match.length === 5 && match[0] === "now-15m/d" && match[1] === "-" + && match[2] === "15" && match[3] === "m" && match[4] === "d" + && match.index === 0 && match.input === "now-15m/d" && match.groups === undefined; + } + + static missingCapture(): boolean { + const match = "now+1h".match(/^now([+-])(\d+)([mhdMywQ])(?:\/(\w))?$/); + if (match === null) return false; + return match.length === 5 && match[4] === undefined; + } + + static testLetters(value: string): boolean { + if (/[a-zA-Z]/.test(value)) return true; + return false; + } + + static testRepeated(value: string): boolean { + if (/^D+$/.test(value)) return true; + return false; + } + + static leftmost(): boolean { + const match = "zabab".match(/(ab)/); + if (match === null) return false; + return match.index === 1 && match[0] === "ab" && match[1] === "ab" && match.input === "zabab"; + } + + static emptyCapture(): boolean { + const match = "".match(/^()$/); + if (match === null) return false; + return match.length === 2 && match[0] === "" && match[1] === ""; + } + + static finalNewlines(): boolean { + return /^D+$/.test("D") && !/^D+$/.test("D\n") && !/^D+$/.test("D\r") + && !/^D+$/.test("D\r\n") && !/^D+$/.test("D\u2028") && !/^D+$/.test("D\u2029") + && "now+1m\n".match(/^now([+-])(\d+)([mhdMywQ])(?:\/(\w))?$/) === null; + } + + static utf16AndEscapes(): boolean { + const match = "😀".match(/^(😀)$/); + if (match === null) return false; + return match[1] === "😀" && /[😀]/.test("\uD83D") && /[😀]/.test("\uDE00") + && !/\w/.test("é") && /\w/.test("_") && /^a\.b\/c$/.test("a.b/c"); + } + + static freshResults(): boolean { + const expression = /^(a)$/; + const first = "a".match(expression); + const second = "a".match(expression); + if (first === null || second === null) return false; + first[1] = "changed"; + return first !== second && second[1] === "a"; + } + + static lastIndex(): boolean { + const expression = /^D+$/; + expression.lastIndex = 7; + return expression.test("DD") && expression.lastIndex === 7; + } + + static literalProperties(): boolean { + const expression = /^a\.b$/; + return expression.source === "^a\\.b$" && expression.flags === "" && !expression.global + && !expression.ignoreCase && !expression.multiline && !expression.sticky && !expression.unicode; + } + + static overriddenTest(): boolean { + const expression = /^D+$/; + expression.test = (value: string): boolean => false; + return expression.test("D"); + } + + static customMatch(): number { + const custom = { match: (expression: RegExp): number => 7 }; + return custom.match(/x/); + } + + static unsupportedFlags(): boolean { return /x/i.test("X"); } + static unsupportedBacktracking(): boolean { return /^a+ab$/.test("aaab"); } + static unsupportedCoercion(): boolean { + const value: any = 7; + return /7/.test(value); + } + static unsupportedUnanchoredRun(): boolean { return /a+/.test("aa"); } + static unsupportedExecOverride(): boolean { + const expression = /x/; + expression.exec = (value: string): RegExpExecArray | null => null; + return expression.test("x"); + } + + static unsupportedPropertyWrite(): boolean { + const expression: any = /x/; + expression.source = "different"; + return expression.test("x"); + } + +} diff --git a/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts b/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts index 9bd4240338..a30bc7339e 100644 --- a/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts +++ b/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts @@ -1,6 +1,6 @@ export class RuntimeLimitationBoundaries { static regularExpressionLiteral(): boolean { - return /value/.test("value"); + return /value|other/.test("value"); } static unsupportedConversionOrSupportedSibling(flag: boolean, value: { field: number }): string { From 0bfb1ccb3256b648fc4527c472218988580a569d Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 16:50:58 +0300 Subject: [PATCH 2/3] Centralize intrinsic field reads and writes --- .../org/usvm/machine/expr/IntrinsicFields.kt | 74 +++++++++++++++++++ .../kotlin/org/usvm/machine/expr/ReadField.kt | 12 +-- .../org/usvm/machine/expr/WriteField.kt | 16 +--- .../usvm/machine/expr/RegExpRuntimeTest.kt | 2 + .../test/resources/models/RegExpRuntime.ts | 12 +++ 5 files changed, 96 insertions(+), 20 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/IntrinsicFields.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/IntrinsicFields.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/IntrinsicFields.kt new file mode 100644 index 0000000000..26c84ff885 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/IntrinsicFields.kt @@ -0,0 +1,74 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsFieldSignature +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope + +/** A stopped intrinsic operation must never fall through to ordinary object storage. */ +internal sealed interface TsIntrinsicFieldResult { + data object NotApplicable : TsIntrinsicFieldResult + data class Handled(val value: T) : TsIntrinsicFieldResult + data object Stopped : TsIntrinsicFieldResult + + companion object { + fun from(value: T?): TsIntrinsicFieldResult = when (value) { + null -> Stopped + else -> Handled(value) + } + } +} + +internal fun TsContext.tryReadIntrinsicField( + scope: TsStepScope, + instance: UHeapRef, + field: EtsFieldSignature, +): TsIntrinsicFieldResult> { + val regularExpression = intrinsicRegExpReference(scope, instance) + if (regularExpression != null) { + return TsIntrinsicFieldResult.from(readRegExpField(scope, regularExpression, field.name)) + } + + if (isDateModelTimestamp(scope = scope, instance = instance, field = field)) { + val timestamp = dateModelTimestampLValue(instance) + val value = scope.calcOnState { memory.read(timestamp) } + return TsIntrinsicFieldResult.Handled(value) + } + + // Date.constructor implements own-property deletion and inherited lookup itself. + val dateConstructor = readIntrinsicDateConstructor(scope, instance, field.name) + if (dateConstructor != null) return TsIntrinsicFieldResult.Handled(dateConstructor) + + return TsIntrinsicFieldResult.NotApplicable +} + +internal fun TsContext.tryWriteIntrinsicField( + scope: TsStepScope, + instance: UHeapRef, + field: EtsFieldSignature, + value: UExpr<*>, +): TsIntrinsicFieldResult { + val regularExpression = intrinsicRegExpReference(scope, instance) + if (regularExpression != null) { + return TsIntrinsicFieldResult.from(writeRegExpField(scope, regularExpression, field.name, value)) + } + + if (isDateModelTimestamp(scope = scope, instance = instance, field = field)) { + val timestamp = dateModelTimestampLValue(instance) + scope.doWithState { + memory.write(timestamp, value.asExpr(fp64Sort), guard = trueExpr) + } + return TsIntrinsicFieldResult.Handled(Unit) + } + + return TsIntrinsicFieldResult.NotApplicable +} + +private fun TsContext.intrinsicRegExpReference(scope: TsStepScope, instance: UHeapRef): UConcreteHeapRef? { + val reference = instance as? UConcreteHeapRef ?: return null + val isRegExp = scope.calcOnState { reference in regularExpressions } + return if (isRegExp) reference else null +} 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 42e22e1935..0d952dade4 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 @@ -128,12 +128,11 @@ internal fun TsContext.resolveField( ): UExpr<*>? { checkNotFake(instance) val receiver = resolveHeapRef(scope, instance) ?: return null - val intrinsicRegExp = receiver is UConcreteHeapRef && scope.calcOnState { receiver in regularExpressions } - if (intrinsicRegExp) return readRegExpField(scope, receiver as UConcreteHeapRef, field.name) - if (isDateModelTimestamp(scope = scope, instance = receiver, field = field)) { - val timestamp = dateModelTimestampLValue(receiver) - return scope.calcOnState { memory.read(timestamp) } + when (val intrinsic = tryReadIntrinsicField(scope, receiver, field)) { + is TsIntrinsicFieldResult.Handled -> return intrinsic.value + TsIntrinsicFieldResult.Stopped -> return null + TsIntrinsicFieldResult.NotApplicable -> {} } // Input fields have symbolic initial presence. Allocations use their declaration and later writes. @@ -151,9 +150,6 @@ private fun TsContext.resolveDeclaredField( field: EtsFieldSignature, hierarchy: EtsHierarchy, ): UExpr<*>? { - val dateConstructor = readIntrinsicDateConstructor(scope, instance, field.name) - if (dateConstructor != null) return dateConstructor - val deleted = scope.calcOnState { memory.read(deletedFieldLValue(instance, field)) } if (deleted.isTrue) return mkUndefinedValue() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index 930993b362..f1e29d64aa 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -10,7 +10,6 @@ import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsStaticFieldRef import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType -import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort @@ -212,18 +211,11 @@ fun TsContext.assignToInstanceField( ): Unit? { // Unwrap to get non-fake reference. val unwrappedInstance = resolveHeapRef(scope, instance.unwrapRef(scope)) ?: return null - val intrinsicRegExp = unwrappedInstance is UConcreteHeapRef && scope.calcOnState { - unwrappedInstance in regularExpressions - } - if (intrinsicRegExp) { - return writeRegExpField(scope, unwrappedInstance as UConcreteHeapRef, field.name, expr) - } - if (isDateModelTimestamp(scope = scope, instance = unwrappedInstance, field = field)) { - val timestamp = dateModelTimestampLValue(unwrappedInstance) - return scope.doWithState { - memory.write(timestamp, expr.asExpr(fp64Sort), guard = trueExpr) - } + when (val intrinsic = tryWriteIntrinsicField(scope, unwrappedInstance, field, expr)) { + is TsIntrinsicFieldResult.Handled -> return intrinsic.value + TsIntrinsicFieldResult.Stopped -> return null + TsIntrinsicFieldResult.NotApplicable -> {} } if (!isAllocatedConcreteHeapRef(unwrappedInstance) && instanceLocal.type !is EtsArrayType) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RegExpRuntimeTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RegExpRuntimeTest.kt index 48b2f4958d..815a2ccbb7 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RegExpRuntimeTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RegExpRuntimeTest.kt @@ -132,6 +132,7 @@ class RegExpRuntimeTest : TsMethodTestRunner() { "unsupportedUnanchoredRun", "unsupportedExecOverride", "unsupportedPropertyWrite", + "unsupportedPropertyRead", ) for (name in names) { TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> @@ -196,6 +197,7 @@ class RegExpRuntimeTest : TsMethodTestRunner() { "freshResults", "lastIndex", "literalProperties", + "bracketProperties", ) } } diff --git a/usvm-ts/src/test/resources/models/RegExpRuntime.ts b/usvm-ts/src/test/resources/models/RegExpRuntime.ts index 852e96c27f..078ef9282d 100644 --- a/usvm-ts/src/test/resources/models/RegExpRuntime.ts +++ b/usvm-ts/src/test/resources/models/RegExpRuntime.ts @@ -76,6 +76,13 @@ export class RegExpRuntime { && !expression.ignoreCase && !expression.multiline && !expression.sticky && !expression.unicode; } + static bracketProperties(): boolean { + const expression = /^D+$/; + expression["lastIndex"] = 7; + return expression["lastIndex"] === 7 && expression["source"] === "^D+$" + && expression["flags"] === "" && expression.test("DD"); + } + static overriddenTest(): boolean { const expression = /^D+$/; expression.test = (value: string): boolean => false; @@ -106,4 +113,9 @@ export class RegExpRuntime { return expression.test("x"); } + static unsupportedPropertyRead(): boolean { + const expression: any = /x/; + return expression.unknownProperty === undefined; + } + } From 8a584dc807a2b1eb61cccb0937641c39ea9be46e Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 18:28:32 +0300 Subject: [PATCH 3/3] Match intrinsic field result filename to its declaration --- .../expr/{IntrinsicFields.kt => TsIntrinsicFieldResult.kt} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename usvm-ts/src/main/kotlin/org/usvm/machine/expr/{IntrinsicFields.kt => TsIntrinsicFieldResult.kt} (100%) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/IntrinsicFields.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsIntrinsicFieldResult.kt similarity index 100% rename from usvm-ts/src/main/kotlin/org/usvm/machine/expr/IntrinsicFields.kt rename to usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsIntrinsicFieldResult.kt