From c3c6a63420f592721b48b263e62752542c9740f1 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 17 Oct 2026 00:34:30 +0300 Subject: [PATCH] Support exact literal and bounded decimal numeric conversion --- .../machine/expr/BoundedStringToNumber.kt | 89 ++++++++++++ .../machine/expr/EcmaScriptStringToNumber.kt | 39 +++++ .../kotlin/org/usvm/machine/expr/ExprUtil.kt | 20 ++- .../machine/expr/StringCodeUnitConversion.kt | 2 + .../machine/expr/BoundedStringToNumberTest.kt | 133 ++++++++++++++++++ .../expr/ExprUtilConditionalValueTest.kt | 49 ++++--- .../expr/RuntimeLimitationBoundariesTest.kt | 4 +- .../resources/models/BoundedStringToNumber.ts | 38 +++++ .../models/RuntimeLimitationBoundaries.ts | 8 +- 9 files changed, 358 insertions(+), 24 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/BoundedStringToNumber.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/EcmaScriptStringToNumber.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/expr/BoundedStringToNumberTest.kt create mode 100644 usvm-ts/src/test/resources/models/BoundedStringToNumber.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/BoundedStringToNumber.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/BoundedStringToNumber.kt new file mode 100644 index 0000000000..e6c63611cf --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/BoundedStringToNumber.kt @@ -0,0 +1,89 @@ +package org.usvm.machine.expr + +import io.ksmt.sort.KBv16Sort +import io.ksmt.sort.KBvSort +import io.ksmt.sort.KFp64Sort +import io.ksmt.utils.cast +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.machine.TsSizeSort +import org.usvm.machine.state.TsState +import org.usvm.util.mkStringBackingElementLValue +import org.usvm.util.stringCharacters +import org.usvm.util.stringLength + +private const val MAX_STRING_NUMBER_CODE_UNITS = 32 +private const val MAX_EXACT_DECIMAL_DIGITS = 15 +private const val DECIMAL_RADIX = 10 +private const val MAX_DECIMAL_DIGIT = 9 + +internal data class TsStringNumberConversion(val supported: UBoolExpr, val value: UExpr) + +/** Exact signed decimal integers, trimmed with ECMAScript whitespace, under the existing string bound. */ +internal fun TsState.boundedIntegerStringToNumber(string: UHeapRef): TsStringNumberConversion? = with(ctx) { + val lengthBound = boundedStringBackingRefs[string] ?: return null + val capacity = minOf(lengthBound, MAX_STRING_NUMBER_CODE_UNITS) + val length = stringLength(string) + val backing = stringCharacters(string) + val characters = (0 until capacity).map { index -> + memory.read(mkStringBackingElementLValue(backing, mkBv(index))) + } + + var firstIndex = length + var lastIndex: UExpr = mkBv(-1) + var firstCharacter: UExpr = mkBv(0, bv16Sort) + for ((index, character) in characters.withIndex()) { + val position = mkBv(index) + val live = mkBvSignedLessExpr(position, length) + val nonWhitespace = mkAnd(live, mkNot(mkEcmaScriptWhitespace(character))) + val firstNonWhitespace = mkAnd(nonWhitespace, mkEq(firstIndex, length)) + firstCharacter = mkIte(firstNonWhitespace, character, firstCharacter) + firstIndex = mkIte(firstNonWhitespace, position, firstIndex) + lastIndex = mkIte(nonWhitespace, position, lastIndex) + } + + val plus = mkEq(firstCharacter, mkBv('+'.code, bv16Sort)) + val minus = mkEq(firstCharacter, mkBv('-'.code, bv16Sort)) + val hasSign = mkOr(plus, minus) + val firstDigitIndex = mkIte(hasSign, mkBvAddExpr(firstIndex, mkBv(1)), firstIndex) + val digitCount = mkBvAddExpr(mkBvSubExpr(lastIndex, firstDigitIndex), mkBv(1)) + val empty = mkEq(firstIndex, length) + val signOnly = mkAnd(hasSign, mkEq(digitCount, mkBv(0))) + val digitConditions = mutableListOf() + var integer: UExpr = mkBv(0, bv64Sort) + val digitWidthExtension = (bv64Sort.sizeBits - bv16Sort.sizeBits).toInt() + for ((index, character) in characters.withIndex()) { + val position = mkBv(index) + val inDigits = mkAnd( + mkBvSignedGreaterOrEqualExpr(position, firstDigitIndex), + mkBvSignedLessOrEqualExpr(position, lastIndex), + ) + val digit = mkBvSubExpr(character, mkBv('0'.code, bv16Sort)) + val isDigit = mkBvUnsignedLessOrEqualExpr(digit, mkBv(MAX_DECIMAL_DIGIT, bv16Sort)) + digitConditions += mkOr(mkNot(inDigits), isDigit) + + val wideDigit = mkBvZeroExtensionExpr(digitWidthExtension, digit) + val nextInteger = mkBvAddExpr(mkBvMulExpr(integer, mkBv(DECIMAL_RADIX, bv64Sort)), wideDigit) + integer = mkIte(inDigits, nextInteger, integer) + } + + val nonnegativeLength = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + val lengthFitsCapacity = mkBvSignedLessOrEqualExpr(length, mkBv(capacity)) + val withinLength = mkAnd(nonnegativeLength, lengthFitsCapacity) + val positiveDigitCount = mkBvSignedGreaterExpr(digitCount, mkBv(0)) + val digitCountFitsPrecision = mkBvSignedLessOrEqualExpr(digitCount, mkBv(MAX_EXACT_DECIMAL_DIGITS)) + val allDigits = mkAnd(digitConditions) + val exactDigits = mkAnd(positiveDigitCount, digitCountFitsPrecision, allDigits) + val supported = mkAnd(withinLength, mkOr(empty, signOnly, exactDigits)) + val positive = mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = integer.cast(), + signed = false, + ) + val signed = mkIte(minus, mkFpNegationExpr(positive), positive) + val number = mkIte(empty, mkFp64(0.0), mkIte(signOnly, mkFp64NaN(), signed)) + + TsStringNumberConversion(supported = supported, value = number) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/EcmaScriptStringToNumber.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/EcmaScriptStringToNumber.kt new file mode 100644 index 0000000000..3b63e1f1a9 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/EcmaScriptStringToNumber.kt @@ -0,0 +1,39 @@ +package org.usvm.machine.expr + +import java.math.BigInteger + +private val decimalStringNumber = Regex("[+-]?(?:[0-9]+(?:\\.[0-9]*)?|\\.[0-9]+)(?:[eE][+-]?[0-9]+)?") +private const val ASCII_RADIX_DIGITS = "0123456789abcdef" +private const val HEXADECIMAL_RADIX = 16 +private const val OCTAL_RADIX = 8 + +/** StringNumericLiteral, excluding Java-only suffixes, hexadecimal floats and extra whitespace. */ +internal fun ecmaScriptStringToNumber(value: String): Double { + val text = value.trim(::isEcmaScriptWhitespace) + if (text.isEmpty()) return 0.0 + when (text) { + "Infinity", "+Infinity" -> return Double.POSITIVE_INFINITY + "-Infinity" -> return Double.NEGATIVE_INFINITY + } + + val radix = if (text.length >= 2 && text[0] == '0') { + when (text[1]) { + 'x', 'X' -> HEXADECIMAL_RADIX + 'o', 'O' -> OCTAL_RADIX + 'b', 'B' -> 2 + else -> null + } + } else { + null + } + if (radix != null) { + val digits = text.substring(startIndex = 2) + val validDigits = digits.isNotEmpty() && digits.all { character -> + ASCII_RADIX_DIGITS.indexOf(character.lowercaseChar()) in 0 until radix + } + return if (validDigits) BigInteger(digits, radix).toDouble() else Double.NaN + } + + if (!decimalStringNumber.matches(text)) return Double.NaN + return text.toDouble() +} 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 c69bd9c328..f2c6a90ed2 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 @@ -302,13 +302,20 @@ private fun TsState.numericConversionSupported(expr: UExpr): UBoolExp } val reference = expr.asExpr(addressSort) + val literalString = (reference as? UConcreteHeapRef)?.let(::getStringConstantValue) + if (literalString != null) return@with trueExpr + val lengthBound = boundedStringBackingRefs[reference] val hasModeledStringConversion = lengthBound != null && lengthBound in 0..1 if (hasModeledStringConversion) { return@with trueExpr } - mkIsNullOrUndefined(reference) + val integerString = boundedIntegerStringToNumber(reference) + val nullish = mkIsNullOrUndefined(reference) + if (integerString == null) return@with nullish + + mkOr(nullish, integerString.supported) } /** Converts modeled primitives and bounded strings, retaining unmodeled alternatives as unsupported paths. */ @@ -407,14 +414,23 @@ private fun TsContext.mkNumericExprUnchecked( return mkIte(expr.condition, trueNumber, falseNumber) } + val reference = expr.asExpr(addressSort) + val literalString = (reference as? UConcreteHeapRef)?.let(::getStringConstantValue) + if (literalString != null) return mkFp64(ecmaScriptStringToNumber(literalString)) + val codeUnitNumber = singleCodeUnitToNumber(scope = scope, string = expr.asExpr(addressSort)) if (codeUnitNumber != null) { return codeUnitNumber } + val integerString = scope.calcOnState { boundedIntegerStringToNumber(reference) } + if (integerString != null) { + val nullishNumber = mkIte(mkHeapRefEq(reference, mkTsNullValue()), mkFp64(0.0), mkFp64NaN()) + return mkIte(mkIsNullOrUndefined(reference), nullishNumber, integerString.value) + } + // TODO: Model general StringToNumber and ToPrimitive conversion (https://github.com/UnitTestBot/usvm/issues/280). // The public support guard excludes unmodeled reference alternatives from the selected result. - val reference = expr.asExpr(addressSort) val nullValue = mkTsNullValue() val isNull = mkEq(reference, nullValue) val zero = mkFp(0.0, fp64Sort) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringCodeUnitConversion.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringCodeUnitConversion.kt index 0761bd4694..758278ce48 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringCodeUnitConversion.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringCodeUnitConversion.kt @@ -17,6 +17,8 @@ private val ecmaScriptWhitespace = listOf( '\u2028', '\u2029', '\u202f', '\u205f', '\u3000', '\ufeff', ) + ('\u2000'..'\u200a') +internal fun isEcmaScriptWhitespace(character: Char): Boolean = character in ecmaScriptWhitespace + /** ECMAScript WhiteSpace and LineTerminator, kept as one predicate rather than execution branches. */ internal fun TsContext.mkEcmaScriptWhitespace(codeUnit: UExpr): UBoolExpr { val matches = ecmaScriptWhitespace.map { character -> diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/BoundedStringToNumberTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/BoundedStringToNumberTest.kt new file mode 100644 index 0000000000..91cbc81edc --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/BoundedStringToNumberTest.kt @@ -0,0 +1,133 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsMethod +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.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class BoundedStringToNumberTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + override val scene = loadScene("/models/BoundedStringToNumber.ts") + override val tsOptions = TsOptions(maxArraySize = 16) + override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + machine.analyze(methods = listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + init { + options = options.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + } + + @Test + fun `literal string numeric syntax follows ECMAScript rather than Java parsing extensions`() { + discoverProperties( + method = method(name = "literalForms"), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } + + @Test + fun `bounded symbolic decimal integers preserve trimming negative zero NaN and exact fifteen digits`() { + discoverProperties( + method = method(name = "selectedIntegers"), + { value, result -> value.value == "12" && result.number == 12.0 }, + { value, result -> value.value == " -0 " && result.number == Double.NEGATIVE_INFINITY }, + { value, result -> value.value == "+" && result.number.isNaN() }, + { value, result -> value.value == "999999999999999" && result.number == 999_999_999_999_999.0 }, + invariants = arrayOf({ value, result -> + when (value.value) { + "12" -> result.number == 12.0 + " -0 " -> result.number == Double.NEGATIVE_INFINITY + "+" -> result.number.isNaN() + "999999999999999" -> result.number == 999_999_999_999_999.0 + else -> result.number == 0.0 + } + }), + ) + } + + @Test + fun `unary plus uses the same bounded integer conversion`() { + discoverProperties( + method = method(name = "unaryInteger"), + { value, result -> value.value == "-12" && result.number == -12.0 }, + invariants = arrayOf({ value, result -> result.number == if (value.value == "-12") -12.0 else 0.0 }), + ) + } + + @Test + fun `unmodeled symbolic formats retain unsupported prefixes and ordinary siblings`() { + for (name in listOf("unsupportedFraction", "unsupportedPrecision")) { + val method = method(name = name) + val machineOptions = options.copy(throwExceptionOnStepFailure = false) + val outcome = TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + machine.analyzeWithMetadata(methods = listOf(method)) + } + val tests = outcome.states.map { TsTestResolver().resolve(method, it) } + + assertTrue(outcome.unsupportedPaths.any { "Numeric conversion" in it }, name) + assertFalse(outcome.engineFailed, name) + assertTrue(tests.isNotEmpty(), name) + assertTrue(tests.all { (it.returnValue as TsTestValue.TsNumber).number == 0.0 }, name) + } + } + + @Test + fun `native JavaScript confirms literal and selected symbolic values`() { + val source = getResourcePath("/models/BoundedStringToNumber.ts").readText() + val checks = """ + if (BoundedStringToNumber.literalForms() !== 1) throw Error("literal syntax"); + for (const value of ["12", " -0 ", "+", "999999999999999", "", "else"]) { + const expected = ["12", " -0 ", "+", "999999999999999"].includes(value) + ? (value === " -0 " ? 1 / Number(value) : Number(value)) : 0; + if (!Object.is(BoundedStringToNumber.selectedIntegers(value), expected)) throw Error(value); + } + if (BoundedStringToNumber.unaryInteger("-12") !== -12) throw Error("unary plus"); + if (BoundedStringToNumber.unsupportedFraction("1.5") !== 1.5) throw Error("fraction boundary"); + if (BoundedStringToNumber.unsupportedPrecision("9007199254740993") !== 9007199254740992) { + throw Error("precision boundary"); + } + """.trimIndent() + + assertNodeReplay( + source = source + checks, + directory = directory, + name = "bounded-string-to-number", + timeoutMessage = "Bounded string conversion replay timed out", + ) + } + + @Test + fun `literal parser rounds decimal and radix values at binary64 precision`() { + assertEquals(9_007_199_254_740_992.0, ecmaScriptStringToNumber("9007199254740993")) + assertEquals(9_007_199_254_740_992.0, ecmaScriptStringToNumber("0x20000000000001")) + assertEquals((-0.0).toRawBits(), ecmaScriptStringToNumber("-0").toRawBits()) + assertTrue(ecmaScriptStringToNumber("\u180e1").isNaN()) + } + + private fun method(name: String) = getMethod(methodName = name, className = "BoundedStringToNumber") +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ExprUtilConditionalValueTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ExprUtilConditionalValueTest.kt index 0df9909110..b9175b94a7 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ExprUtilConditionalValueTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ExprUtilConditionalValueTest.kt @@ -1,6 +1,7 @@ package org.usvm.machine.expr import io.mockk.mockk +import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsType @@ -169,11 +170,11 @@ class ExprUtilConditionalValueTest { @Test fun `inactive unmodeled reference payload does not reject a numeric wrapper`() = with(ctx) { val number = mkFp64(7.0) - val unmodeledString = state.mkInitializedStringConstant(value = "42") + val unmodeledObject = state.memory.allocConcrete(EtsAnyType) val wrapper = state.mkFakeValue( scope = null, fpValue = number, - refValue = unmodeledString, + refValue = unmodeledObject, valueType = EtsFakeType.mkFp(ctx), ) @@ -188,14 +189,14 @@ class ExprUtilConditionalValueTest { fun `numeric conversion retains a supported conditional wrapper and records its unsupported sibling`() = with(ctx) { val selected = mkRegisterReading(idx = 0, sort = boolSort) val number = mkFp64(7.0) - val unmodeledString = state.mkInitializedStringConstant(value = "42") + val unmodeledObject = state.memory.allocConcrete(EtsAnyType) val numberWrapper = state.mkFakeValue(scope = null, fpValue = number, valueType = EtsFakeType.mkFp(ctx)) - val stringWrapper = state.mkFakeValue( + val referenceWrapper = state.mkFakeValue( scope = null, - refValue = unmodeledString, + refValue = unmodeledObject, valueType = EtsFakeType.mkRef(ctx), ) - val conditional = mkIte(selected, numberWrapper, stringWrapper) + val conditional = mkIte(selected, numberWrapper, referenceWrapper) assertIs>(conditional) val numeric = mkNumericExpr(conditional, scope) @@ -209,11 +210,27 @@ class ExprUtilConditionalValueTest { ) } + @Test + fun `literal string and numeric conditional wrappers both retain exact conversion`() = with(ctx) { + val selected = mkRegisterReading(idx = 0, sort = boolSort) + val number = mkFp64(7.0) + val string = state.mkInitializedStringConstant(value = "42") + val numberWrapper = state.mkFakeValue(scope = null, fpValue = number, valueType = EtsFakeType.mkFp(ctx)) + val stringWrapper = state.mkFakeValue(scope = null, refValue = string, valueType = EtsFakeType.mkRef(ctx)) + val conditional = mkIte(selected, numberWrapper, stringWrapper) + + val numeric = mkNumericExpr(conditional, scope) + + assertEquals(mkIte(selected, number, mkFp64(42.0)), numeric) + assertNull(state.unsupportedReason) + assertEquals(emptyList(), scope.stepResult().forkedStates.toList()) + } + @Test fun `binary arithmetic retains the numeric result of joined operator wrappers`() = with(ctx) { val selected = mkRegisterReading(idx = 0, sort = boolSort) - val unmodeledString = state.mkInitializedStringConstant(value = "42") - val joined = with(TsBinaryOperator.Or) { ctx.resolve(boolToFp(selected), unmodeledString, scope) } + val unmodeledObject = state.memory.allocConcrete(EtsAnyType) + val joined = with(TsBinaryOperator.Or) { ctx.resolve(boolToFp(selected), unmodeledObject, scope) } val conditional = assertNotNull(joined) assertIs>(conditional) @@ -232,8 +249,8 @@ class ExprUtilConditionalValueTest { @Test fun `binary arithmetic retains a numeric conditional right operand`() = with(ctx) { val selected = mkRegisterReading(idx = 0, sort = boolSort) - val unmodeledString = state.mkInitializedStringConstant(value = "42") - val joined = with(TsBinaryOperator.Or) { ctx.resolve(boolToFp(selected), unmodeledString, scope) } + val unmodeledObject = state.memory.allocConcrete(EtsAnyType) + val joined = with(TsBinaryOperator.Or) { ctx.resolve(boolToFp(selected), unmodeledObject, scope) } val conditional = assertNotNull(joined) assertIs>(conditional) @@ -252,7 +269,7 @@ class ExprUtilConditionalValueTest { @Test fun `numeric binary operators ignore inactive populated reference payloads on either side`() = with(ctx) { val selected = mkRegisterReading(idx = 0, sort = boolSort) - val unmodeledString = state.mkInitializedStringConstant(value = "42") + val unmodeledObject = state.memory.allocConcrete(EtsAnyType) val kinds = EtsFakeType( boolTypeExpr = selected, fpTypeExpr = mkNot(selected), @@ -262,7 +279,7 @@ class ExprUtilConditionalValueTest { scope = null, boolValue = trueExpr, fpValue = mkFp64(7.0), - refValue = unmodeledString, + refValue = unmodeledObject, valueType = kinds, ) val operators = listOf(TsBinaryOperator.Add, TsBinaryOperator.Lt, TsBinaryOperator.Gt) @@ -311,7 +328,7 @@ class ExprUtilConditionalValueTest { @Test fun `addition retains symbolic numeric kinds while rejecting the selected reference kind`() = with(ctx) { val selected = mkRegisterReading(idx = 0, sort = boolSort) - val unmodeledString = state.mkInitializedStringConstant(value = "42") + val string = state.mkInitializedStringConstant(value = "42") val kinds = EtsFakeType( boolTypeExpr = falseExpr, fpTypeExpr = selected, @@ -320,7 +337,7 @@ class ExprUtilConditionalValueTest { val wrapper = state.mkFakeValue( scope = null, fpValue = mkFp64(7.0), - refValue = unmodeledString, + refValue = string, valueType = kinds, ) @@ -372,10 +389,10 @@ class ExprUtilConditionalValueTest { @Test fun `numeric binary support failures stay under the enclosing active guard`() = with(ctx) { val selected = mkRegisterReading(idx = 0, sort = boolSort) - val unmodeledString = state.mkInitializedStringConstant(value = "42") + val unmodeledObject = state.memory.allocConcrete(EtsAnyType) val resolved = with(TsBinaryOperator.Sub) { - ctx.resolve(unmodeledString, mkFp64(1.0), scope, activeGuard = selected) + ctx.resolve(unmodeledObject, mkFp64(1.0), scope, activeGuard = selected) } val result = assertNotNull(resolved) val unsupported = scope.stepResult().forkedStates.single() diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt index 5eb1b0366e..909143140b 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt @@ -195,10 +195,10 @@ class RuntimeLimitationBoundariesTest : TsMethodTestRunner() { assertTrue(unsupportedReason in outcome.unsupportedPaths) assertTrue(witnesses.isNotEmpty()) witnesses.forEach { witness -> - val useString = witness.before.parameters.single() as TsTestValue.TsBoolean + val unsupportedBranch = witness.before.parameters.single() as TsTestValue.TsBoolean val result = witness.returnValue as TsTestValue.TsNumber - assertTrue(!useString.value) + assertTrue(!unsupportedBranch.value) assertEquals(expected, result.number) } } diff --git a/usvm-ts/src/test/resources/models/BoundedStringToNumber.ts b/usvm-ts/src/test/resources/models/BoundedStringToNumber.ts new file mode 100644 index 0000000000..48a4ecc955 --- /dev/null +++ b/usvm-ts/src/test/resources/models/BoundedStringToNumber.ts @@ -0,0 +1,38 @@ +export class BoundedStringToNumber { + static literalForms(): number { + if (Number("42") !== 42 || Number(" -12.5e1 ") !== -125) return 0; + if (Number("0xff") !== 255 || Number("0o17") !== 15 || Number("0b101") !== 5) return 0; + if (Number("\ufeff\u00a0") !== 0 || Number(".5") !== 0.5 || Number("1.") !== 1) return 0; + if (Number("1e309") !== 1 / 0 || Number("-Infinity") !== -1 / 0) return 0; + if (1 / Number("-0") !== -1 / 0) return 0; + const invalid = ["0x1p0", "1d", "+0x1", "0b2", "1_0", "\u0085", "0xＦＦ"]; + for (const value of invalid) { + const converted = Number(value); + if (converted === converted) return 0; + } + return 1; + } + + static selectedIntegers(value: string): number { + if (value === "12") return Number(value); + if (value === " -0 ") return 1 / Number(value); + if (value === "+") return Number(value); + if (value === "999999999999999") return Number(value); + return 0; + } + + static unaryInteger(value: string): number { + if (value !== "-12") return 0; + return +value; + } + + static unsupportedFraction(value: string): number { + if (value !== "1.5") return 0; + return Number(value); + } + + static unsupportedPrecision(value: string): number { + if (value !== "9007199254740993") return 0; + return Number(value); + } +} diff --git a/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts b/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts index a30bc7339e..8f01a02b10 100644 --- a/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts +++ b/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts @@ -18,9 +18,9 @@ export class RuntimeLimitationBoundaries { return record.length; } - static unsupportedNumericConversionOrSupportedSibling(useString: boolean): number { + static unsupportedNumericConversionOrSupportedSibling(useObject: boolean): number { const values: unknown[] = [7]; - if (useString) values[0] = "42"; + if (useObject) values[0] = { value: 42 }; return +values[0]; } @@ -39,9 +39,9 @@ export class RuntimeLimitationBoundaries { && Number.isNaN(+"x"); } - static unsupportedNumericBinaryConversionOrSupportedSibling(useString: boolean): number { + static unsupportedNumericBinaryConversionOrSupportedSibling(useObject: boolean): number { const values: unknown[] = [7]; - if (useString) values[0] = "42"; + if (useObject) values[0] = { value: 42 }; return values[0] - 1; }