From e3c3c6b6dd15c0256e4d936f05666bffd0f9a82e Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 2 Oct 2026 22:07:55 +0300 Subject: [PATCH 1/7] Support modeled TypeScript Number exponentiation (#428) --- .../org/usvm/machine/expr/TsExprResolver.kt | 49 ++++- .../usvm/samples/operators/Exponentiation.kt | 176 ++++++++++++++++++ .../samples/operators/Exponentiation.ts | 59 ++++++ 3 files changed, 282 insertions(+), 2 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt create mode 100644 usvm-ts/src/test/resources/samples/operators/Exponentiation.ts 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 65a7a3d5d8..956625f683 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 @@ -140,6 +140,8 @@ private const val ECMASCRIPT_BITWISE_INTEGER_SIZE = 32 */ private const val ECMASCRIPT_BITWISE_SHIFT_MASK = 0b11111 +private const val SQUARE_ROOT_EXPONENT = 0.5 + private enum class UpdateOperator { INCREMENT, DECREMENT, @@ -638,8 +640,51 @@ class TsExprResolver( } override fun visit(expr: EtsExpExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + return resolveAfterResolved(expr.left, expr.right) { left, right -> + with(ctx) { + for (operand in listOf(left, right)) { + val supportedPrimitive = operand.sort == fp64Sort || operand.sort == boolSort || + operand == mkTsNullValue() || operand == mkUndefinedValue() + if (!supportedPrimitive) { + throw UnsupportedOperationException( + "Exponentiation operand outside the supported Number conversion model: $operand" + ) + } + } + + val base = mkNumericExpr(left, scope) + val exponent = mkNumericExpr(right, scope) + + if (base is KFp64Value && exponent is KFp64Value) { + return@with mkFp64(value = Math.pow(base.value, exponent.value)) + } + + val concreteExponent = (exponent as? KFp64Value)?.value + ?: throw UnsupportedOperationException("Symbolic exponentiation exponent is not supported: $expr") + + when (concreteExponent) { + 0.0 -> mkFp64(value = 1.0) + 1.0 -> base + 2.0 -> mkFpMulExpr(fpRoundingModeSortDefaultValue(), base, base) + -1.0 -> mkFpDivExpr(fpRoundingModeSortDefaultValue(), mkFp64(value = 1.0), base) + SQUARE_ROOT_EXPONENT -> { + // Number::exponentiate maps either signed zero to +0 for a non-integral exponent. + val positiveZero = mkFp64(value = 0.0) + val isZero = mkFpEqualExpr(base, positiveZero) + val squareRoot = mkFpSqrtExpr(fpRoundingModeSortDefaultValue(), base) + + mkIte( + condition = isZero, + trueBranch = positiveZero, + falseBranch = squareRoot, + ) + } + else -> throw UnsupportedOperationException( + "Symbolic exponentiation with exponent $concreteExponent is not supported: $expr" + ) + } + } + } } override fun visit(expr: EtsBitAndExpr): UExpr? = with(ctx) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt new file mode 100644 index 0000000000..1e0258efeb --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt @@ -0,0 +1,176 @@ +package org.usvm.samples.operators + +import org.jacodb.ets.model.EtsScene +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.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import java.nio.file.Path +import java.util.concurrent.TimeUnit +import kotlin.io.path.readText +import kotlin.io.path.writeText +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class Exponentiation : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val resource = "/samples/operators/Exponentiation.ts" + + override val scene: EtsScene = loadScene(resource) + + @Test + fun `supported symbolic powers replay in Node`() { + for (methodName in listOf("square", "reciprocal", "squareRoot")) { + val tests = analyze(methodName) + + assertTrue(tests.isNotEmpty(), "No results for $methodName") + if (methodName == "square") { + assertTrue(tests.any { test -> + val input = assertIs(test.before.parameters.single()).number + val result = assertIs(test.returnValue).number + input == 3.0 && result == 9.0 + }, "The generated square(3) witness is missing") + } + if (methodName == "reciprocal" || methodName == "squareRoot") { + assertTrue(tests.any { test -> + val input = assertIs(test.before.parameters.single()).number + val result = assertIs(test.returnValue).number + input.toRawBits() == (-0.0).toRawBits() && + (methodName == "reciprocal" && result == Double.NEGATIVE_INFINITY || + methodName == "squareRoot" && result.toRawBits() == 0.0.toRawBits()) + }, "The generated signed-zero witness is missing for $methodName") + } + + replay(methodName, tests) + } + } + + @Test + fun `constant fractional power is evaluated`() { + val tests = analyze("constantFractional") + + assertTrue(tests.isNotEmpty()) + tests.forEach { test -> + val result = assertIs(test.returnValue).number + assertEquals(3.0, result) + } + replay("constantFractional", tests) + } + + @Test + fun `concrete Number edge cases replay in Node`() { + val cases = mapOf( + "nanToZero" to 1.0, + "negativeZeroToMinusOne" to Double.NEGATIVE_INFINITY, + "negativeInfinitySquared" to Double.POSITIVE_INFINITY, + "negativeOneInfinite" to Double.NaN, + "negativeFractional" to Double.NaN, + ) + + for ((methodName, expected) in cases) { + val tests = analyze(methodName) + + assertTrue(tests.isNotEmpty(), "No result for $methodName") + tests.forEach { test -> + val actual = assertIs(test.returnValue).number + assertTrue( + actual.toRawBits() == expected.toRawBits() || (actual.isNaN() && expected.isNaN()), + "$methodName returned $actual rather than $expected", + ) + } + replay(methodName, tests) + } + } + + @Test + fun `unsupported symbolic powers are explicit`() { + for (methodName in listOf("symbolicExponent", "unsupportedFractional")) { + val failure = assertFailsWith { analyze(methodName) } + + assertTrue(failure.message.orEmpty().contains("Symbolic exponentiation")) + } + } + + @Test + fun `unsupported string conversion is explicit`() { + val failure = assertFailsWith { analyze("stringBase") } + + assertTrue(failure.message.orEmpty().contains("outside the supported Number conversion model")) + } + + private fun analyze(methodName: String): List { + val method = getMethod(methodName) + + return TsMachine(scene = scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> + machine.analyze(methods = listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + private fun replay(methodName: String, tests: List) { + val source = javaClass.getResourceAsStream(resource)?.bufferedReader()?.use { it.readText() } + ?: error("Missing $resource") + val script = directory.resolve("$methodName.ts") + val output = directory.resolve("$methodName.out") + script.writeText(buildString { + appendLine(source) + tests.forEachIndexed { index, test -> + val args = test.before.parameters.map { value -> + val number = assertIs(value).number + jsNumber(number) + }.joinToString() + val expected = assertIs(test.returnValue).number + appendLine( + "if (!Object.is(new Exponentiation().$methodName($args), ${jsNumber(expected)})) " + + "throw Error('Replay mismatch at result $index');" + ) + } + }) + + val process = ProcessBuilder("node", "--experimental-strip-types", script.toString()) + .redirectErrorStream(true) + .redirectOutput(output.toFile()) + .start() + + try { + assertTrue(process.waitFor(10, TimeUnit.SECONDS), "Node replay timed out") + assertEquals(0, process.exitValue(), output.readText()) + } finally { + if (process.isAlive) process.destroyForcibly() + } + } + + private fun jsNumber(value: Double): String = when { + value.isNaN() -> "NaN" + value == Double.POSITIVE_INFINITY -> "Infinity" + value == Double.NEGATIVE_INFINITY -> "-Infinity" + value == 0.0 && value.toRawBits() == (-0.0).toRawBits() -> "-0" + else -> value.toString() + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts b/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts new file mode 100644 index 0000000000..3688f7468a --- /dev/null +++ b/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts @@ -0,0 +1,59 @@ +class Exponentiation { + square(value: number): number { + if (value === 3) return value ** 2; + if (value === -3) return value ** 2; + if (value === Infinity) return value ** 2; + if (value === -Infinity) return value ** 2; + if (value !== value) return value ** 2; + return value ** 2; + } + + reciprocal(value: number): number { + if (1 / value === -Infinity) return value ** -1; + if (value === 0) return value ** -1; + return value ** -1; + } + + squareRoot(value: number): number { + if (1 / value === -Infinity) return value ** 0.5; + if (value === 9) return value ** 0.5; + if (value === -1) return value ** 0.5; + return value ** 0.5; + } + + constantFractional(): number { + return 9 ** 0.5; + } + + nanToZero(): number { + return (0 / 0) ** 0; + } + + negativeZeroToMinusOne(): number { + return (-0) ** -1; + } + + negativeInfinitySquared(): number { + return (-1 / 0) ** 2; + } + + negativeOneInfinite(): number { + return (-1) ** (1 / 0); + } + + negativeFractional(): number { + return (-9) ** 0.5; + } + + symbolicExponent(value: number, exponent: number): number { + return value ** exponent; + } + + unsupportedFractional(value: number): number { + return value ** 1.5; + } + + stringBase(): number { + return "3" ** 2; + } +} From 5c7e538f2136090789d2ce869b91350347319505 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 2 Oct 2026 22:41:18 +0300 Subject: [PATCH 2/7] Correct symbolic Number exponentiation boundaries (#428) --- .../org/usvm/machine/expr/TsExprResolver.kt | 12 ++++--- .../usvm/samples/operators/Exponentiation.kt | 34 ++++++++++++++++--- .../samples/operators/Exponentiation.ts | 2 ++ 3 files changed, 38 insertions(+), 10 deletions(-) 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 956625f683..18267d1149 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 @@ -662,21 +662,23 @@ class TsExprResolver( val concreteExponent = (exponent as? KFp64Value)?.value ?: throw UnsupportedOperationException("Symbolic exponentiation exponent is not supported: $expr") + // More powers cannot be expanded to FP arithmetic: x ** -1 can differ from 1 / x. when (concreteExponent) { 0.0 -> mkFp64(value = 1.0) 1.0 -> base 2.0 -> mkFpMulExpr(fpRoundingModeSortDefaultValue(), base, base) - -1.0 -> mkFpDivExpr(fpRoundingModeSortDefaultValue(), mkFp64(value = 1.0), base) SQUARE_ROOT_EXPONENT -> { - // Number::exponentiate maps either signed zero to +0 for a non-integral exponent. + // Number::exponentiate maps either signed zero and -Infinity to positive results here. val positiveZero = mkFp64(value = 0.0) val isZero = mkFpEqualExpr(base, positiveZero) + val isNegativeInfinity = mkFpEqualExpr(base, mkFp64(value = Double.NEGATIVE_INFINITY)) val squareRoot = mkFpSqrtExpr(fpRoundingModeSortDefaultValue(), base) + val ordinaryResult = mkIte(isZero, positiveZero, squareRoot) mkIte( - condition = isZero, - trueBranch = positiveZero, - falseBranch = squareRoot, + condition = isNegativeInfinity, + trueBranch = mkFp64(value = Double.POSITIVE_INFINITY), + falseBranch = ordinaryResult, ) } else -> throw UnsupportedOperationException( diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt index 1e0258efeb..bfd94782b3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt @@ -33,7 +33,7 @@ class Exponentiation : TsMethodTestRunner() { @Test fun `supported symbolic powers replay in Node`() { - for (methodName in listOf("square", "reciprocal", "squareRoot")) { + for (methodName in listOf("square", "squareRoot")) { val tests = analyze(methodName) assertTrue(tests.isNotEmpty(), "No results for $methodName") @@ -44,14 +44,17 @@ class Exponentiation : TsMethodTestRunner() { input == 3.0 && result == 9.0 }, "The generated square(3) witness is missing") } - if (methodName == "reciprocal" || methodName == "squareRoot") { + if (methodName == "squareRoot") { assertTrue(tests.any { test -> val input = assertIs(test.before.parameters.single()).number val result = assertIs(test.returnValue).number - input.toRawBits() == (-0.0).toRawBits() && - (methodName == "reciprocal" && result == Double.NEGATIVE_INFINITY || - methodName == "squareRoot" && result.toRawBits() == 0.0.toRawBits()) + input.toRawBits() == (-0.0).toRawBits() && result.toRawBits() == 0.0.toRawBits() }, "The generated signed-zero witness is missing for $methodName") + assertTrue(tests.any { test -> + val input = assertIs(test.before.parameters.single()).number + val result = assertIs(test.returnValue).number + input == Double.NEGATIVE_INFINITY && result == Double.POSITIVE_INFINITY + }, "The generated negative-infinity witness is missing for $methodName") } replay(methodName, tests) @@ -104,6 +107,27 @@ class Exponentiation : TsMethodTestRunner() { } } + @Test + fun `symbolic reciprocal stays unsupported when division differs in Node`() { + val output = directory.resolve("reciprocal-divergence.out") + val script = "const x = 518.3984755809512; Object.is(x ** -1, 1 / x)" + val process = ProcessBuilder("node", "-p", script) + .redirectErrorStream(true) + .redirectOutput(output.toFile()) + .start() + + try { + assertTrue(process.waitFor(10, TimeUnit.SECONDS), "Node reciprocal probe timed out") + assertEquals(0, process.exitValue(), output.readText()) + assertEquals("false", output.readText().trim()) + } finally { + if (process.isAlive) process.destroyForcibly() + } + + val failure = assertFailsWith { analyze("reciprocal") } + assertTrue(failure.message.orEmpty().contains("exponent -1.0")) + } + @Test fun `unsupported string conversion is explicit`() { val failure = assertFailsWith { analyze("stringBase") } diff --git a/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts b/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts index 3688f7468a..37817995cc 100644 --- a/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts +++ b/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts @@ -9,12 +9,14 @@ class Exponentiation { } reciprocal(value: number): number { + if (value === 518.3984755809512) return value ** -1; if (1 / value === -Infinity) return value ** -1; if (value === 0) return value ** -1; return value ** -1; } squareRoot(value: number): number { + if (value === -Infinity) return value ** 0.5; if (1 / value === -Infinity) return value ** 0.5; if (value === 9) return value ** 0.5; if (value === -1) return value ** 0.5; From 49fa6c70356c5ff83f5565b3307a77ae13c14514 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 2 Oct 2026 22:54:40 +0300 Subject: [PATCH 3/7] Avoid Node-version-specific reciprocal assertion (#428) --- .../usvm/samples/operators/Exponentiation.kt | 18 ++---------------- .../samples/operators/Exponentiation.ts | 3 --- 2 files changed, 2 insertions(+), 19 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt index bfd94782b3..4d2497b4ca 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt @@ -108,23 +108,9 @@ class Exponentiation : TsMethodTestRunner() { } @Test - fun `symbolic reciprocal stays unsupported when division differs in Node`() { - val output = directory.resolve("reciprocal-divergence.out") - val script = "const x = 518.3984755809512; Object.is(x ** -1, 1 / x)" - val process = ProcessBuilder("node", "-p", script) - .redirectErrorStream(true) - .redirectOutput(output.toFile()) - .start() - - try { - assertTrue(process.waitFor(10, TimeUnit.SECONDS), "Node reciprocal probe timed out") - assertEquals(0, process.exitValue(), output.readText()) - assertEquals("false", output.readText().trim()) - } finally { - if (process.isAlive) process.destroyForcibly() - } - + fun `symbolic reciprocal is explicitly unsupported`() { val failure = assertFailsWith { analyze("reciprocal") } + assertTrue(failure.message.orEmpty().contains("exponent -1.0")) } diff --git a/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts b/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts index 37817995cc..24eebb3ec1 100644 --- a/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts +++ b/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts @@ -9,9 +9,6 @@ class Exponentiation { } reciprocal(value: number): number { - if (value === 518.3984755809512) return value ** -1; - if (1 / value === -Infinity) return value ** -1; - if (value === 0) return value ** -1; return value ** -1; } From 0db0f339a77c19bd14a779c71e785cb3f23fc639 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 01:20:52 +0300 Subject: [PATCH 4/7] Report unsupported exponentiation in normal analysis (#428) --- .../usvm/samples/operators/Exponentiation.kt | 38 ++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt index 4d2497b4ca..6a92d87136 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt @@ -8,6 +8,8 @@ import org.usvm.StateCollectionStrategy import org.usvm.UMachineOptions import org.usvm.api.TsTest import org.usvm.api.TsTestValue +import org.usvm.machine.TsAnalysisResult +import org.usvm.machine.TsAnalysisStopReason import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.TsMethodTestRunner @@ -34,8 +36,12 @@ class Exponentiation : TsMethodTestRunner() { @Test fun `supported symbolic powers replay in Node`() { for (methodName in listOf("square", "squareRoot")) { - val tests = analyze(methodName) + val outcome = analyzeWithDefaultFailureHandling(methodName) + val method = getMethod(methodName) + val tests = outcome.states.map { state -> TsTestResolver().resolve(method, state) } + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") assertTrue(tests.isNotEmpty(), "No results for $methodName") if (methodName == "square") { assertTrue(tests.any { test -> @@ -114,6 +120,27 @@ class Exponentiation : TsMethodTestRunner() { assertTrue(failure.message.orEmpty().contains("exponent -1.0")) } + @Test + fun `unsupported powers remain visible in ordinary analysis outcome`() { + val cases = mapOf( + "symbolicExponent" to "Symbolic exponentiation exponent", + "unsupportedFractional" to "Symbolic exponentiation with exponent 1.5", + "reciprocal" to "Symbolic exponentiation with exponent -1.0", + "stringBase" to "outside the supported Number conversion model", + ) + + for ((methodName, expectedReason) in cases) { + val outcome = analyzeWithDefaultFailureHandling(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), "$methodName yielded a completed state") + assertTrue( + outcome.unsupportedPaths.any { reason -> expectedReason in reason }, + "$methodName: ${outcome.unsupportedPaths}", + ) + } + } + @Test fun `unsupported string conversion is explicit`() { val failure = assertFailsWith { analyze("stringBase") } @@ -129,6 +156,15 @@ class Exponentiation : TsMethodTestRunner() { } } + private fun analyzeWithDefaultFailureHandling(methodName: String): TsAnalysisResult { + val method = getMethod(methodName) + val options = machineOptions.copy(throwExceptionOnStepFailure = false) + + return TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + } + private fun replay(methodName: String, tests: List) { val source = javaClass.getResourceAsStream(resource)?.bufferedReader()?.use { it.readText() } ?: error("Missing $resource") From bdabc1569142a4310edaab4d31f2822fa28ba85a Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 01:55:08 +0300 Subject: [PATCH 5/7] Constrain concrete TypeScript exponentiation to exact cases (#428) --- .../org/usvm/machine/expr/TsExprResolver.kt | 14 ++++++- .../usvm/samples/operators/Exponentiation.kt | 40 +++++++++++++++---- .../samples/operators/Exponentiation.ts | 12 ++++++ 3 files changed, 57 insertions(+), 9 deletions(-) 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 18267d1149..e6f0f3728a 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 @@ -656,7 +656,17 @@ class TsExprResolver( val exponent = mkNumericExpr(right, scope) if (base is KFp64Value && exponent is KFp64Value) { - return@with mkFp64(value = Math.pow(base.value, exponent.value)) + // JVM Math.pow and JavaScript ** can differ by one ULP for ordinary finite powers. + // Only these discrete edge cases have runtime-independent Number results. + if (base.value == 0.0 && exponent.value == -1.0) { + val isNegativeZero = base.value.toRawBits() < 0 + val result = if (isNegativeZero) Double.NEGATIVE_INFINITY else Double.POSITIVE_INFINITY + return@with mkFp64(value = result) + } + + if (base.value == -1.0 && exponent.value.isInfinite()) { + return@with mkFp64NaN() + } } val concreteExponent = (exponent as? KFp64Value)?.value @@ -682,7 +692,7 @@ class TsExprResolver( ) } else -> throw UnsupportedOperationException( - "Symbolic exponentiation with exponent $concreteExponent is not supported: $expr" + "Number exponentiation with exponent $concreteExponent is not modeled: $expr" ) } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt index 6a92d87136..d58bbcef2c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt @@ -79,13 +79,33 @@ class Exponentiation : TsMethodTestRunner() { replay("constantFractional", tests) } + @Test + fun `unmodeled concrete fractional power is unsupported and runs in Node`() { + val outcome = analyzeWithDefaultFailureHandling("unmodeledConcreteFractional") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.unsupportedPaths.any { "exponent 0.7" in it }) + + val source = javaClass.getResourceAsStream(resource)?.bufferedReader()?.use { it.readText() } + ?: error("Missing $resource") + val script = buildString { + appendLine(source) + appendLine("const actual = new Exponentiation().unmodeledConcreteFractional();") + appendLine("if (!Object.is(actual, 0.1 ** 0.7)) throw Error('Node replay mismatch');") + } + runNode("unmodeledConcreteFractional.ts", script) + } + @Test fun `concrete Number edge cases replay in Node`() { val cases = mapOf( "nanToZero" to 1.0, "negativeZeroToMinusOne" to Double.NEGATIVE_INFINITY, + "positiveZeroToMinusOne" to Double.POSITIVE_INFINITY, "negativeInfinitySquared" to Double.POSITIVE_INFINITY, "negativeOneInfinite" to Double.NaN, + "negativeOneNegativeInfinite" to Double.NaN, "negativeFractional" to Double.NaN, ) @@ -109,7 +129,7 @@ class Exponentiation : TsMethodTestRunner() { for (methodName in listOf("symbolicExponent", "unsupportedFractional")) { val failure = assertFailsWith { analyze(methodName) } - assertTrue(failure.message.orEmpty().contains("Symbolic exponentiation")) + assertTrue(failure.message.orEmpty().contains("exponentiation")) } } @@ -124,8 +144,8 @@ class Exponentiation : TsMethodTestRunner() { fun `unsupported powers remain visible in ordinary analysis outcome`() { val cases = mapOf( "symbolicExponent" to "Symbolic exponentiation exponent", - "unsupportedFractional" to "Symbolic exponentiation with exponent 1.5", - "reciprocal" to "Symbolic exponentiation with exponent -1.0", + "unsupportedFractional" to "Number exponentiation with exponent 1.5", + "reciprocal" to "Number exponentiation with exponent -1.0", "stringBase" to "outside the supported Number conversion model", ) @@ -168,9 +188,7 @@ class Exponentiation : TsMethodTestRunner() { private fun replay(methodName: String, tests: List) { val source = javaClass.getResourceAsStream(resource)?.bufferedReader()?.use { it.readText() } ?: error("Missing $resource") - val script = directory.resolve("$methodName.ts") - val output = directory.resolve("$methodName.out") - script.writeText(buildString { + val script = buildString { appendLine(source) tests.forEachIndexed { index, test -> val args = test.before.parameters.map { value -> @@ -183,7 +201,15 @@ class Exponentiation : TsMethodTestRunner() { "throw Error('Replay mismatch at result $index');" ) } - }) + } + + runNode("$methodName.ts", script) + } + + private fun runNode(scriptName: String, source: String) { + val script = directory.resolve(scriptName) + val output = directory.resolve("$scriptName.out") + script.writeText(source) val process = ProcessBuilder("node", "--experimental-strip-types", script.toString()) .redirectErrorStream(true) diff --git a/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts b/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts index 24eebb3ec1..ef7e22c69f 100644 --- a/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts +++ b/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts @@ -24,6 +24,10 @@ class Exponentiation { return 9 ** 0.5; } + unmodeledConcreteFractional(): number { + return 0.1 ** 0.7; + } + nanToZero(): number { return (0 / 0) ** 0; } @@ -32,6 +36,10 @@ class Exponentiation { return (-0) ** -1; } + positiveZeroToMinusOne(): number { + return 0 ** -1; + } + negativeInfinitySquared(): number { return (-1 / 0) ** 2; } @@ -40,6 +48,10 @@ class Exponentiation { return (-1) ** (1 / 0); } + negativeOneNegativeInfinite(): number { + return (-1) ** (-1 / 0); + } + negativeFractional(): number { return (-9) ** 0.5; } From 0e7262ff2e5dfe66ee5d2ed2f98a225a3b33d6af Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 08:50:08 +0300 Subject: [PATCH 6/7] [TS] Reuse Node replay helper in exponentiation tests Remove duplicate Node process handling from #428 regressions while preserving witness assertions. --- .../usvm/samples/operators/Exponentiation.kt | 36 +++++++------------ 1 file changed, 13 insertions(+), 23 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt index d58bbcef2c..ab46574c1c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt @@ -14,10 +14,8 @@ 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 java.nio.file.Path -import java.util.concurrent.TimeUnit -import kotlin.io.path.readText -import kotlin.io.path.writeText import kotlin.test.Test import kotlin.test.assertEquals import kotlin.test.assertFailsWith @@ -94,7 +92,12 @@ class Exponentiation : TsMethodTestRunner() { appendLine("const actual = new Exponentiation().unmodeledConcreteFractional();") appendLine("if (!Object.is(actual, 0.1 ** 0.7)) throw Error('Node replay mismatch');") } - runNode("unmodeledConcreteFractional.ts", script) + assertNodeReplay( + source = script, + directory = directory, + name = "unmodeledConcreteFractional", + timeoutMessage = "Node replay timed out", + ) } @Test @@ -203,25 +206,12 @@ class Exponentiation : TsMethodTestRunner() { } } - runNode("$methodName.ts", script) - } - - private fun runNode(scriptName: String, source: String) { - val script = directory.resolve(scriptName) - val output = directory.resolve("$scriptName.out") - script.writeText(source) - - val process = ProcessBuilder("node", "--experimental-strip-types", script.toString()) - .redirectErrorStream(true) - .redirectOutput(output.toFile()) - .start() - - try { - assertTrue(process.waitFor(10, TimeUnit.SECONDS), "Node replay timed out") - assertEquals(0, process.exitValue(), output.readText()) - } finally { - if (process.isAlive) process.destroyForcibly() - } + assertNodeReplay( + source = script, + directory = directory, + name = methodName, + timeoutMessage = "Node replay timed out", + ) } private fun jsNumber(value: Double): String = when { From 615bcb7ab786567d0d5faf39911574a6dd1e71f1 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 4 Oct 2026 00:51:43 +0300 Subject: [PATCH 7/7] [TS] Check exponentiation results through discoverProperties --- .../usvm/samples/operators/Exponentiation.kt | 38 ++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt index ab46574c1c..63420ac5b9 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt @@ -34,8 +34,27 @@ class Exponentiation : TsMethodTestRunner() { @Test fun `supported symbolic powers replay in Node`() { for (methodName in listOf("square", "squareRoot")) { - val outcome = analyzeWithDefaultFailureHandling(methodName) val method = getMethod(methodName) + + if (methodName == "square") { + discoverProperties( + method = method, + { input, result -> input.number == 3.0 && result.number == 9.0 }, + ) + } else { + discoverProperties( + method = method, + { input, result -> + input.number.toRawBits() == (-0.0).toRawBits() && + result.number.toRawBits() == 0.0.toRawBits() + }, + { input, result -> + input.number == Double.NEGATIVE_INFINITY && result.number == Double.POSITIVE_INFINITY + }, + ) + } + + val outcome = analyzeWithDefaultFailureHandling(methodName) val tests = outcome.states.map { state -> TsTestResolver().resolve(method, state) } assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) @@ -67,6 +86,13 @@ class Exponentiation : TsMethodTestRunner() { @Test fun `constant fractional power is evaluated`() { + val method = getMethod("constantFractional") + discoverProperties( + method = method, + { result -> result.number == 3.0 }, + invariants = arrayOf({ result -> result.number == 3.0 }), + ) + val tests = analyze("constantFractional") assertTrue(tests.isNotEmpty()) @@ -113,6 +139,16 @@ class Exponentiation : TsMethodTestRunner() { ) for ((methodName, expected) in cases) { + val method = getMethod(methodName) + val matchesExpected: (TsTestValue.TsNumber) -> Boolean = { result -> + result.number.toRawBits() == expected.toRawBits() || (result.number.isNaN() && expected.isNaN()) + } + discoverProperties( + method = method, + matchesExpected, + invariants = arrayOf(matchesExpected), + ) + val tests = analyze(methodName) assertTrue(tests.isNotEmpty(), "No result for $methodName")