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..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 @@ -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,63 @@ 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) { + // 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 + ?: 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) + SQUARE_ROOT_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 = isNegativeInfinity, + trueBranch = mkFp64(value = Double.POSITIVE_INFINITY), + falseBranch = ordinaryResult, + ) + } + else -> throw UnsupportedOperationException( + "Number exponentiation with exponent $concreteExponent is not modeled: $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..63420ac5b9 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Exponentiation.kt @@ -0,0 +1,274 @@ +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.TsAnalysisResult +import org.usvm.machine.TsAnalysisStopReason +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 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", "squareRoot")) { + 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) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") + 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 == "squareRoot") { + assertTrue(tests.any { test -> + val input = assertIs(test.before.parameters.single()).number + val result = assertIs(test.returnValue).number + 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) + } + } + + @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()) + tests.forEach { test -> + val result = assertIs(test.returnValue).number + assertEquals(3.0, result) + } + 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');") + } + assertNodeReplay( + source = script, + directory = directory, + name = "unmodeledConcreteFractional", + timeoutMessage = "Node replay timed out", + ) + } + + @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, + ) + + 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") + 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("exponentiation")) + } + } + + @Test + fun `symbolic reciprocal is explicitly unsupported`() { + val failure = assertFailsWith { analyze("reciprocal") } + + 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 "Number exponentiation with exponent 1.5", + "reciprocal" to "Number 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") } + + 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 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") + val script = 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');" + ) + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = methodName, + timeoutMessage = "Node replay timed out", + ) + } + + 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..ef7e22c69f --- /dev/null +++ b/usvm-ts/src/test/resources/samples/operators/Exponentiation.ts @@ -0,0 +1,70 @@ +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 { + 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; + return value ** 0.5; + } + + constantFractional(): number { + return 9 ** 0.5; + } + + unmodeledConcreteFractional(): number { + return 0.1 ** 0.7; + } + + nanToZero(): number { + return (0 / 0) ** 0; + } + + negativeZeroToMinusOne(): number { + return (-0) ** -1; + } + + positiveZeroToMinusOne(): number { + return 0 ** -1; + } + + negativeInfinitySquared(): number { + return (-1 / 0) ** 2; + } + + negativeOneInfinite(): number { + return (-1) ** (1 / 0); + } + + negativeOneNegativeInfinite(): 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; + } +}