Support exact literal and bounded decimal numeric conversion

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<KFp64Sort>)
+
+/** 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<TsSizeSort> = mkBv(-1)
+    var firstCharacter: UExpr<KBv16Sort> = 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<UBoolExpr>()
+    var integer: UExpr<KBvSort> = 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)
+}

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()
+}

usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt

@@ -302,13 +302,20 @@ private fun TsState.numericConversionSupported(expr: UExpr<out USort>): 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)

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<KBv16Sort>): UBoolExpr {
     val matches = ecmaScriptWhitespace.map { character ->

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<TsTest> = { 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<TsTestValue.TsNumber>(
+            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<TsTestValue.TsString, TsTestValue.TsNumber>(
+            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<TsTestValue.TsString, TsTestValue.TsNumber>(
+            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")
+}