From 5c0f812e5304a017ece0d9269d68e7574bb971ad Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 8 Oct 2026 00:36:47 +0300 Subject: [PATCH] Model numeric builtins with verified global ownership --- usvm-ts-calls/build.gradle.kts | 7 +- .../org/usvm/ts/calls/CallsExperiment.kt | 11 +- .../ts/calls/CurrentTsCallsSymbolicEngine.kt | 37 +- .../calls/CurrentTsCallsSymbolicEngineTest.kt | 33 ++ .../usvm/machine/call/TsBuiltinGlobalType.kt | 43 +++ .../TsNumericIntrinsicModelFamily.kt | 351 ++++++++++++++++++ .../usvm/machine/expr/CallApproximations.kt | 54 ++- .../machine/call/BuiltinOwnerBoundaryTest.kt | 60 +++ .../call/TsNumericIntrinsicModelsTest.kt | 276 ++++++++++++++ .../call/TsUnknownCallModelCatalogTest.kt | 22 +- .../resources/models/BuiltinOwnerBoundary.ts | 25 ++ .../models/NumericIntrinsicModels.ts | 208 +++++++++++ 12 files changed, 1106 insertions(+), 21 deletions(-) create mode 100644 usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumericIntrinsicModelFamily.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/BuiltinOwnerBoundaryTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsNumericIntrinsicModelsTest.kt create mode 100644 usvm-ts/src/test/resources/models/BuiltinOwnerBoundary.ts create mode 100644 usvm-ts/src/test/resources/models/NumericIntrinsicModels.ts diff --git a/usvm-ts-calls/build.gradle.kts b/usvm-ts-calls/build.gradle.kts index bcc0ba431b..3d7f8f67dd 100644 --- a/usvm-ts-calls/build.gradle.kts +++ b/usvm-ts-calls/build.gradle.kts @@ -30,6 +30,7 @@ val toolStatus = providers.exec { val generateBuildMetadata = tasks.register("generateBuildMetadata") { inputs.property("toolRevision", toolRevision) inputs.property("toolStatus", toolStatus) + inputs.property("jacodbVersion", Versions.jacodb) outputs.dir(generatedBuildMetadataDirectory) doLast { @@ -39,7 +40,11 @@ val generateBuildMetadata = tasks.register("generateBuildMetadata") { .file("org/usvm/ts/calls/build.properties") .asFile metadataFile.parentFile.mkdirs() - metadataFile.writeText("tool.revision=$buildIdentity\n", Charsets.UTF_8) + metadataFile.writeText( + "tool.revision=$buildIdentity\n" + + "native.frontend.revision=bundled:${Versions.jacodb}\n", + Charsets.UTF_8, + ) } } diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt index 3746582ff3..606dab1886 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt @@ -244,16 +244,25 @@ internal object CallsExperimentJson { } internal object CallsBuildIdentity { - val toolRevision: String by lazy { + private val properties: Properties by lazy { val properties = Properties() val resource = checkNotNull(javaClass.getResourceAsStream("/org/usvm/ts/calls/build.properties")) { "Missing calls build identity" } resource.use(properties::load) + properties + } + + val toolRevision: String by lazy { checkNotNull(properties.getProperty("tool.revision")).takeIf(String::isNotBlank) ?: error("Missing tool revision in calls build identity") } + + val nativeFrontendRevision: String by lazy { + checkNotNull(properties.getProperty("native.frontend.revision")).takeIf(String::isNotBlank) + ?: error("Missing native frontend revision in calls build identity") + } } internal class CallsExperimentRunner( diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt index 69da1df9d2..5cb013e8e3 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt @@ -30,9 +30,12 @@ import org.usvm.util.mkRegisterStackLValue import java.nio.file.Path import kotlin.time.TimeSource -internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine { +internal class CurrentTsCallsSymbolicEngine( + private val environment: (String) -> String? = System::getenv, + private val bundledNativeFrontendRevision: String = CallsBuildIdentity.nativeFrontendRevision, +) : CallsSymbolicEngine { private val verifiedProjects = mutableMapOf() - private var verifiedNativeFrontend: Pair? = null + private var verifiedNativeFrontendIdentity: String? = null override fun search(request: CallsSymbolicSearchRequest): CallsSymbolicSearchResult { val startedAt = TimeSource.Monotonic.markNow() @@ -248,22 +251,34 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine { diagnostic = diagnostic, ) - private fun verifyNativeFrontendOnce(expectedRevision: String) { - require(System.getenv("ETS_FRONTEND_SCRIPT") == null) { + internal fun verifyNativeFrontendOnce(expectedRevision: String) { + val configuredScript = environment("ETS_FRONTEND_SCRIPT") + require(configuredScript == null) { "ETS_FRONTEND_SCRIPT must be unset so the frozen native frontend runtime is used" } - val configuredFrontend = requireNotNull(System.getenv("ETS_FRONTEND_DIR")) { + if (expectedRevision.startsWith(BUNDLED_FRONTEND_PREFIX)) { + require(environment("ETS_FRONTEND_DIR") == null) { + "ETS_FRONTEND_DIR must be unset when the bundled native frontend is selected" + } + require(expectedRevision == bundledNativeFrontendRevision) { + "Bundled native frontend revision $expectedRevision does not match running build " + + bundledNativeFrontendRevision + } + verifiedNativeFrontendIdentity = expectedRevision + return + } + + val configuredFrontend = requireNotNull(environment("ETS_FRONTEND_DIR")) { "ETS_FRONTEND_DIR is required to verify the frozen native frontend revision" } val frontendDirectory = Path.of(configuredFrontend).toRealPath() - val cached = verifiedNativeFrontend - val expectedIdentity = expectedRevision - if (cached == Pair(frontendDirectory, expectedIdentity)) { + val expectedIdentity = "$frontendDirectory@$expectedRevision" + if (verifiedNativeFrontendIdentity == expectedIdentity) { return } verifyCallsGitCheckout(frontendDirectory, expectedRevision) - verifiedNativeFrontend = frontendDirectory to expectedIdentity + verifiedNativeFrontendIdentity = expectedIdentity } private fun verifyGitCheckoutOnce( @@ -296,6 +311,10 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine { val stopReason: TsAnalysisStopReason, val unsupportedPaths: List, ) + + private companion object { + const val BUNDLED_FRONTEND_PREFIX: String = "bundled:" + } } internal data class SourceStatementEntry( diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt new file mode 100644 index 0000000000..b8923279e3 --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt @@ -0,0 +1,33 @@ +package org.usvm.ts.calls + +import kotlin.test.Test +import kotlin.test.assertFailsWith + +class CurrentTsCallsSymbolicEngineTest { + @Test + fun `bundled frontend accepts only the revision baked into the running build`() { + val engine = CurrentTsCallsSymbolicEngine( + environment = emptyMap()::get, + bundledNativeFrontendRevision = "bundled:published-jacodb", + ) + + engine.verifyNativeFrontendOnce(expectedRevision = "bundled:published-jacodb") + + assertFailsWith { + engine.verifyNativeFrontendOnce(expectedRevision = "bundled:different-jacodb") + } + } + + @Test + fun `bundled frontend rejects native frontend environment overrides`() { + val environment = mapOf("ETS_FRONTEND_DIR" to "/unused/frontend") + val engine = CurrentTsCallsSymbolicEngine( + environment = environment::get, + bundledNativeFrontendRevision = "bundled:published-jacodb", + ) + + assertFailsWith { + engine.verifyNativeFrontendOnce(expectedRevision = "bundled:published-jacodb") + } + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt new file mode 100644 index 0000000000..288fc23f13 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt @@ -0,0 +1,43 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsUnknownType +import org.jacodb.ets.model.EtsValue + +internal fun hasBuiltinGlobalOwner( + owner: EtsValue, + callee: EtsMethodSignature, + expectedName: String, +): Boolean = owner.type.isBuiltinGlobalType(expectedName) || + owner.isLegacyBuiltinGlobal(expectedName = expectedName, callee = callee) + +internal fun EtsType.isBuiltinGlobalType(expectedName: String): Boolean = when (expectedName) { + "Math" -> this is EtsUnclearRefType && name == expectedName + "Number" -> this is EtsFunctionType && isBuiltinNumberType() + else -> false +} + +private fun EtsFunctionType.isBuiltinNumberType(): Boolean { + val parameter = signature.parameters.singleOrNull() ?: return false + return signature.enclosingClass == EtsClassSignature.UNKNOWN && + signature.name.isEmpty() && + signature.returnType == EtsNumberType && + parameter.type == EtsAnyType && + parameter.isOptional && + !parameter.isRest +} + +private fun EtsValue.isLegacyBuiltinGlobal( + expectedName: String, + callee: EtsMethodSignature, +): Boolean = this is EtsLocal && + name == expectedName && + type == EtsUnknownType && + callee.enclosingClass == EtsClassSignature.UNKNOWN.copy(name = expectedName) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumericIntrinsicModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumericIntrinsicModelFamily.kt new file mode 100644 index 0000000000..948493f52d --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumericIntrinsicModelFamily.kt @@ -0,0 +1,351 @@ +package org.usvm.machine.call.intrinsic + +import io.ksmt.expr.KFpRoundingMode +import io.ksmt.sort.KFp64Sort +import io.ksmt.utils.asExpr +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModel +import org.usvm.machine.call.TsUnknownCallModelCompletion +import org.usvm.machine.call.TsUnknownCallModelExecution +import org.usvm.machine.call.TsUnknownCallModelSuccessor +import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.call.hasBuiltinGlobalOwner +import org.usvm.machine.state.TsState + +internal object TsNumericIntrinsicModelFamily : TsBuiltInUnknownCallModelFamily { + const val MATH_ABS_ID: String = "ts.math.abs" + const val MATH_CEIL_ID: String = "ts.math.ceil" + const val MATH_FLOOR_ID: String = "ts.math.floor" + const val MATH_MAX_ID: String = "ts.math.max" + const val MATH_MIN_ID: String = "ts.math.min" + const val MATH_ROUND_ID: String = "ts.math.round" + const val MATH_SQRT_ID: String = "ts.math.sqrt" + const val MATH_TRUNC_ID: String = "ts.math.trunc" + const val NUMBER_IS_FINITE_ID: String = "ts.number.isFinite" + const val NUMBER_IS_INTEGER_ID: String = "ts.number.isInteger" + const val NUMBER_IS_NAN_ID: String = "ts.number.isNaN" + const val NUMBER_IS_SAFE_INTEGER_ID: String = "ts.number.isSafeInteger" + + private val mathAbsModel = NumericIntrinsicModel( + id = MATH_ABS_ID, + methodName = "abs", + implementation = { state, call -> + unaryMathCall(state, call) { value -> state.ctx.mkFpAbsExpr(value) } + }, + ) + private val mathCeilModel = NumericIntrinsicModel( + id = MATH_CEIL_ID, + methodName = "ceil", + implementation = { state, call -> + unaryMathCall(state, call) { value -> + with(state.ctx) { + mkFpRoundToIntegralExpr( + roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardPositive), + value = value, + ) + } + } + }, + ) + private val mathFloorModel = NumericIntrinsicModel( + id = MATH_FLOOR_ID, + methodName = "floor", + implementation = roundingMathCall(roundingMode = KFpRoundingMode.RoundTowardNegative), + ) + private val mathMaxModel = NumericIntrinsicModel( + id = MATH_MAX_ID, + methodName = "max", + implementation = { state, call -> + variadicMathCall( + state = state, + call = call, + identity = Double.NEGATIVE_INFINITY, + combine = state::mathMax, + ) + }, + ) + private val mathMinModel = NumericIntrinsicModel( + id = MATH_MIN_ID, + methodName = "min", + implementation = { state, call -> + variadicMathCall( + state = state, + call = call, + identity = Double.POSITIVE_INFINITY, + combine = state::mathMin, + ) + }, + ) + private val mathRoundModel = NumericIntrinsicModel( + id = MATH_ROUND_ID, + methodName = "round", + implementation = { state, call -> unaryMathCall(state, call, state::mathRound) }, + ) + private val mathSqrtModel = NumericIntrinsicModel( + id = MATH_SQRT_ID, + methodName = "sqrt", + implementation = { state, call -> + unaryMathCall(state, call) { value -> + state.ctx.mkFpSqrtExpr(state.ctx.fpRoundingModeSortDefaultValue(), value) + } + }, + ) + private val mathTruncModel = NumericIntrinsicModel( + id = MATH_TRUNC_ID, + methodName = "trunc", + implementation = roundingMathCall(roundingMode = KFpRoundingMode.RoundTowardZero), + ) + private val numberIsFiniteModel = NumericIntrinsicModel( + id = NUMBER_IS_FINITE_ID, + methodName = "isFinite", + implementation = { state, call -> + numberPredicate(state, call) { value -> + with(state.ctx) { + val isNotNaN = mkFpIsNaNExpr(value).not() + val isNotInfinite = mkFpIsInfiniteExpr(value).not() + + mkAnd(isNotNaN, isNotInfinite) + } + } + }, + ) + private val numberIsIntegerModel = NumericIntrinsicModel( + id = NUMBER_IS_INTEGER_ID, + methodName = "isInteger", + implementation = { state, call -> numberPredicate(state, call, state::isInteger) }, + ) + private val numberIsNaNModel = NumericIntrinsicModel( + id = NUMBER_IS_NAN_ID, + methodName = "isNaN", + implementation = { state, call -> + numberPredicate(state, call) { value -> state.ctx.mkFpIsNaNExpr(value) } + }, + ) + private val numberIsSafeIntegerModel = NumericIntrinsicModel( + id = NUMBER_IS_SAFE_INTEGER_ID, + methodName = "isSafeInteger", + implementation = { state, call -> numberPredicate(state, call, state::isSafeInteger) }, + ) + + override val models: List = listOf( + mathAbsModel, + mathCeilModel, + mathFloorModel, + mathMaxModel, + mathMinModel, + mathRoundModel, + mathSqrtModel, + mathTruncModel, + numberIsFiniteModel, + numberIsIntegerModel, + numberIsNaNModel, + numberIsSafeIntegerModel, + ) +} + +private class NumericIntrinsicModel( + override val id: String, + methodName: String, + private val implementation: (TsState, TsUnknownCall) -> TsUnknownCallModelExecution?, +) : TsUnknownCallModel { + override val target = numericTarget(methodName) + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? = + implementation(state, call) +} + +private fun numberPredicate( + state: TsState, + call: TsUnknownCall, + predicate: (UExpr) -> UBoolExpr, +): TsUnknownCallModelExecution? { + if (!call.hasGlobalOwner("Number")) { + return null + } + val value = call.arguments.firstOrNull()?.resolved + ?: return state.normalExecution(state.ctx.falseExpr) + val result = with(state.ctx) { + if (value.isFakeObject()) { + val type = value.getFakeType(state.memory) + mkAnd(type.fpTypeExpr, predicate(value.extractFp(state.memory))) + } else if (value.sort == fp64Sort) { + predicate(value.asExpr(fp64Sort)) + } else { + falseExpr + } + } + + return state.normalExecution(result) +} + +private fun roundingMathCall( + roundingMode: KFpRoundingMode, +): (TsState, TsUnknownCall) -> TsUnknownCallModelExecution? = { state, call -> + unaryMathCall(state, call) { value -> + with(state.ctx) { + mkFpRoundToIntegralExpr( + roundingMode = mkFpRoundingModeExpr(roundingMode), + value = value, + ) + } + } +} + +private fun numericTarget(methodName: String) = TsUnknownCallTarget( + methodName = methodName, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, +) + +private fun unaryMathCall( + state: TsState, + call: TsUnknownCall, + operation: (UExpr) -> UExpr, +): TsUnknownCallModelExecution? { + if (!call.hasGlobalOwner("Math")) { + return null + } + val argument = call.arguments.firstOrNull()?.resolved + ?: return state.normalExecution(state.ctx.mkFp(Double.NaN, state.ctx.fp64Sort)) + if (argument.sort != state.ctx.fp64Sort) { + return null + } + + val result = operation(argument.asExpr(state.ctx.fp64Sort)) + return state.normalExecution(result) +} + +private fun variadicMathCall( + state: TsState, + call: TsUnknownCall, + identity: Double, + combine: (UExpr, UExpr) -> UExpr, +): TsUnknownCallModelExecution? { + if (!call.hasGlobalOwner("Math")) { + return null + } + val arguments = call.arguments.map { argument -> + val value = argument.resolved ?: return null + if (value.sort != state.ctx.fp64Sort) { + return null + } + + value.asExpr(state.ctx.fp64Sort) + } + val result = arguments.fold(state.ctx.mkFp(identity, state.ctx.fp64Sort), combine) + + return state.normalExecution(result) +} + +private fun TsUnknownCall.hasGlobalOwner(expectedName: String): Boolean { + val owner = receiver?.source ?: return false + return hasBuiltinGlobalOwner(owner = owner, callee = callee, expectedName = expectedName) +} + +private fun TsState.normalExecution(result: UExpr<*>): TsUnknownCallModelExecution = with(ctx) { + val successor = TsUnknownCallModelSuccessor( + guard = trueExpr, + completion = TsUnknownCallModelCompletion.Normal { result }, + ) + + TsUnknownCallModelExecution(successors = listOf(successor)) +} + +private fun TsState.isInteger(value: UExpr) = with(ctx) { + val truncated = mkFpRoundToIntegralExpr( + roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardZero), + value = value, + ) + + mkAnd( + mkFpIsNaNExpr(value).not(), + mkFpIsInfiniteExpr(value).not(), + mkFpEqualExpr(value, truncated), + ) +} + +private fun TsState.isSafeInteger(value: UExpr) = with(ctx) { + val absoluteValue = mkFpAbsExpr(value) + val maxSafeInteger = mkFp(MAX_SAFE_INTEGER, fp64Sort) + val isInSafeRange = mkFpLessOrEqualExpr(absoluteValue, maxSafeInteger) + + mkAnd( + isInteger(value), + isInSafeRange, + ) +} + +private fun TsState.mathMin( + left: UExpr, + right: UExpr, +): UExpr = with(ctx) { + val zero = mkFp(0.0, fp64Sort) + val negativeZero = mkFp(NEGATIVE_ZERO, fp64Sort) + val leftIsNegative = mkFpIsNegativeExpr(left) + val rightIsNegative = mkFpIsNegativeExpr(right) + val eitherNegative = mkOr(leftIsNegative, rightIsNegative) + val signedZero = mkIte(eitherNegative, negativeZero, zero) + val leftIsZero = mkFpIsZeroExpr(left) + val rightIsZero = mkFpIsZeroExpr(right) + val bothZero = mkAnd(leftIsZero, rightIsZero) + val equalResult = mkIte(bothZero, signedZero, left) + val rightLessResult = mkIte(mkFpLessExpr(right, left), right, equalResult) + val leftLessResult = mkIte(mkFpLessExpr(left, right), left, rightLessResult) + val rightNaNResult = mkIte(mkFpIsNaNExpr(right), right, leftLessResult) + + mkIte(mkFpIsNaNExpr(left), left, rightNaNResult) +} + +private fun TsState.mathMax( + left: UExpr, + right: UExpr, +): UExpr = with(ctx) { + val zero = mkFp(0.0, fp64Sort) + val negativeZero = mkFp(NEGATIVE_ZERO, fp64Sort) + val leftIsPositive = mkFpIsPositiveExpr(left) + val rightIsPositive = mkFpIsPositiveExpr(right) + val eitherPositive = mkOr(leftIsPositive, rightIsPositive) + val signedZero = mkIte(eitherPositive, zero, negativeZero) + val leftIsZero = mkFpIsZeroExpr(left) + val rightIsZero = mkFpIsZeroExpr(right) + val bothZero = mkAnd(leftIsZero, rightIsZero) + val equalResult = mkIte(bothZero, signedZero, left) + val rightGreaterResult = mkIte(mkFpGreaterExpr(right, left), right, equalResult) + val leftGreaterResult = mkIte(mkFpGreaterExpr(left, right), left, rightGreaterResult) + val rightNaNResult = mkIte(mkFpIsNaNExpr(right), right, leftGreaterResult) + + mkIte(mkFpIsNaNExpr(left), left, rightNaNResult) +} + +private fun TsState.mathRound(value: UExpr): UExpr = with(ctx) { + val roundingMode = fpRoundingModeSortDefaultValue() + val floor = mkFpRoundToIntegralExpr( + roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardNegative), + value = value, + ) + val fraction = mkFpSubExpr(roundingMode, value, floor) + val half = mkFp(ROUNDING_THRESHOLD, fp64Sort) + val useFloor = mkFpLessExpr(fraction, half) + val increment = mkFp(ROUNDING_INCREMENT, fp64Sort) + val incrementedFloor = mkFpAddExpr(roundingMode, floor, increment) + val rounded = mkIte(useFloor, floor, incrementedFloor) + val isNegative = mkFpIsNegativeExpr(value) + val roundedIsZero = mkFpIsZeroExpr(rounded) + val returnsNegativeZero = mkAnd(isNegative, roundedIsZero) + val negativeZero = mkFp(NEGATIVE_ZERO, fp64Sort) + val signedRounded = mkIte(returnsNegativeZero, negativeZero, rounded) + val preserveInput = mkOr( + mkFpIsNaNExpr(value), + mkFpIsInfiniteExpr(value), + mkFpIsZeroExpr(value), + ) + + mkIte(preserveInput, value, signedRounded) +} + +private const val MAX_SAFE_INTEGER: Double = 9_007_199_254_740_991.0 +private const val NEGATIVE_ZERO: Double = -0.0 +private const val ROUNDING_THRESHOLD: Double = 0.5 +private const val ROUNDING_INCREMENT: Double = 1.0 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 385cd38679..ec72f82efb 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 @@ -25,11 +25,13 @@ import org.usvm.machine.TsVirtualMethodCallStmt import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallModelDispatcher import org.usvm.machine.call.dispatch +import org.usvm.machine.call.hasBuiltinGlobalOwner import org.usvm.machine.expr.TsExprApproximationResult.Companion.from import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.markResolved import org.usvm.machine.interpreter.setResolvedValue import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.lastStmt import org.usvm.machine.state.newStmt import org.usvm.machine.types.TsUnresolvedArrayKind import org.usvm.machine.types.mkFakeValue @@ -53,10 +55,16 @@ internal fun TsExprResolver.tryApproximateGlobalInstanceCall( return from(mkUndefinedValue()) } - // Handle `Number.isNaN()` calls - if (expr.instance.name == "Number") { - if (expr.callee.name == "isNaN") { - return from(handleNumberIsNaN(expr)) + // Handle `Number` calls. + if (hasBuiltinGlobalOwner(owner = expr.instance, callee = expr.callee, expectedName = "Number")) { + when (expr.callee.name) { + "isFinite", "isInteger", "isSafeInteger" -> { + return tryDispatchNumericBuiltin(expr) + ?: TsExprApproximationResult.NoApproximation + } + + "isNaN" -> return tryDispatchNumericBuiltin(expr) + ?: from(handleNumberIsNaN(expr)) } } @@ -77,16 +85,46 @@ internal fun TsExprResolver.tryApproximateGlobalInstanceCall( } } - // Handle `Math` method calls - if (expr.instance.name == "Math") { - if (expr.callee.name == "floor") { - return from(handleMathFloor(expr)) + // Handle `Math` method calls. + if (hasBuiltinGlobalOwner(owner = expr.instance, callee = expr.callee, expectedName = "Math")) { + when (expr.callee.name) { + "abs", "ceil", "max", "min", "round", "sqrt", "trunc" -> { + return tryDispatchNumericBuiltin(expr) + ?: TsExprApproximationResult.NoApproximation + } + + "floor" -> return tryDispatchNumericBuiltin(expr) + ?: from(handleMathFloor(expr)) } } return TsExprApproximationResult.NoApproximation } +private fun TsExprResolver.tryDispatchNumericBuiltin( + expr: EtsInstanceCallExpr, +): TsExprApproximationResult? { + val dispatcher = unknownCallDispatcher + if (dispatcher !is TsUnknownCallModelDispatcher) { + return null + } + val resolvedArguments = buildList { + for (argument in expr.args) { + add(resolve(argument) ?: return TsExprApproximationResult.ResolveFailure) + } + } + + dispatcher.dispatch( + scope = scope, + call = expr, + callSite = scope.calcOnState { lastStmt }, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + resolvedArguments = resolvedArguments, + ) + + return TsExprApproximationResult.ResolveFailure +} + internal fun TsExprResolver.tryApproximateInstanceCall( stmt: TsVirtualMethodCallStmt, ): TsExprApproximationResult = with(ctx) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/BuiltinOwnerBoundaryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/BuiltinOwnerBoundaryTest.kt new file mode 100644 index 0000000000..eed868523c --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/BuiltinOwnerBoundaryTest.kt @@ -0,0 +1,60 @@ +package org.usvm.machine.call + +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.Test +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.getResourcePath + +class BuiltinOwnerBoundaryTest : TsMethodTestRunner() { + override val scene = EtsScene( + listOf( + loadEtsFileAutoConvert( + getResourcePath("/models/BuiltinOwnerBoundary.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + + override val runner: (EtsMethod, UMachineOptions) -> List = { method, options -> + TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + @Test + fun `local objects named Math and Number retain their own methods`() { + discoverProperties( + method = getMethod(methodName = "shadowedMath", className = "BuiltinOwnerBoundary"), + { result -> result.number == 77.0 }, + invariants = arrayOf({ result -> result.number == 77.0 }), + ) + discoverProperties( + method = getMethod(methodName = "shadowedNumber", className = "BuiltinOwnerBoundary"), + { result -> !result.value }, + invariants = arrayOf({ result -> !result.value }), + ) + } + + @Test + fun `aliases retain genuine numeric builtin semantics`() { + discoverProperties( + method = getMethod(methodName = "aliasedMath", className = "BuiltinOwnerBoundary"), + { result -> result.number == 2.0 }, + invariants = arrayOf({ result -> result.number == 2.0 }), + ) + discoverProperties( + method = getMethod(methodName = "aliasedNumber", className = "BuiltinOwnerBoundary"), + { result -> !result.value }, + invariants = arrayOf({ result -> !result.value }), + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsNumericIntrinsicModelsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsNumericIntrinsicModelsTest.kt new file mode 100644 index 0000000000..e56aee2623 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsNumericIntrinsicModelsTest.kt @@ -0,0 +1,276 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.call.intrinsic.TsNumericIntrinsicModelFamily +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsNumericIntrinsicModelsTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/NumericIntrinsicModels.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(projectFiles = listOf(sourceFile)) + + @Test + fun `primary Math models preserve binary64 special values and signed zero`() { + val expected = linkedMapOf( + "absNegativeZero" to numberToken(0.0), + "absNaN" to NAN, + "absNegativeInfinity" to numberToken(Double.POSITIVE_INFINITY), + "minSignedZero" to numberToken(-0.0), + "minNaN" to NAN, + "minNoArguments" to numberToken(Double.POSITIVE_INFINITY), + "maxSignedZero" to numberToken(0.0), + "maxInfinity" to numberToken(Double.POSITIVE_INFINITY), + "maxNoArguments" to numberToken(Double.NEGATIVE_INFINITY), + "roundNegativeHalf" to numberToken(-0.0), + "roundPositiveHalf" to numberToken(1.0), + "roundNegativeOneHalf" to numberToken(-1.0), + "roundNaN" to NAN, + "ceilNegativeFraction" to numberToken(-0.0), + "ceilInfinity" to numberToken(Double.POSITIVE_INFINITY), + "absNoArguments" to NAN, + "absExtraArgument" to numberToken(2.0), + ) + + val result = analyze(expected.keys.toList()) + + expected.forEach { (methodName, expectedToken) -> + val actual = assertIs(result.values.getValue(methodName).single()).number + + assertEquals(expectedToken, numberToken(actual), methodName) + } + assertEquals(expected.size, result.events.size) + assertTrue(result.events.all { event -> event.outcome == TsUnknownCallOutcome.MODEL_APPLIED }) + } + + @Test + fun `Number isInteger handles finite boundaries and non numbers`() { + val expected = linkedMapOf( + "integerPositiveZero" to true, + "integerNegativeZero" to true, + "integerFraction" to false, + "integerNaN" to false, + "integerInfinity" to false, + "integerLargeBinary64" to true, + "integerBoolean" to false, + "integerNoArguments" to false, + "integerExtraArgument" to true, + ) + + val result = analyze(expected.keys.toList()) + + expected.forEach { (methodName, expectedValue) -> + val actual = assertIs(result.values.getValue(methodName).single()).value + + assertEquals(expectedValue, actual, methodName) + } + assertEquals( + List(expected.size) { TsNumericIntrinsicModelFamily.NUMBER_IS_INTEGER_ID }, + result.modelIds, + ) + } + + @Test + fun `symbolic numeric calls use intrinsic models`() { + val methodNames = listOf("symbolicAbs", "symbolicInteger") + + val result = analyze(methodNames) + + val absValues = result.values.getValue("symbolicAbs") + .map { value -> assertIs(value).number } + val integerValues = result.values.getValue("symbolicInteger") + .map { value -> assertIs(value).number } + + assertEquals(setOf(1.0), absValues.toSet()) + assertEquals(setOf(0.0, 1.0), integerValues.toSet()) + assertEquals( + setOf( + TsNumericIntrinsicModelFamily.MATH_ABS_ID, + TsNumericIntrinsicModelFamily.NUMBER_IS_INTEGER_ID, + ), + result.modelIds.toSet(), + ) + assertTrue(result.events.all { event -> event.outcome == TsUnknownCallOutcome.MODEL_APPLIED }) + } + + @Test + fun `unsupported Math domain uses residual fallback`() { + val methodNames = listOf("unsupportedAbsDomain") + + val result = analyze(methodNames) + + assertTrue(result.values.values.all { values -> values.isEmpty() }) + assertTrue(result.modelIds.isEmpty()) + assertEquals( + List(methodNames.size) { TsUnknownCallOutcome.PATH_STOPPED }, + result.events.map { event -> event.outcome }, + ) + } + + @Test + fun `disabled numeric model uses configured fallback`() { + val result = analyze( + methodNames = listOf("absNegativeZero"), + tsOptions = TsOptions( + unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet()), + unknownCallFallback = TsResidualCallPolicy.STOP_PATH, + ), + ) + + assertTrue(result.values.getValue("absNegativeZero").isEmpty()) + assertTrue(result.modelIds.isEmpty()) + assertEquals(listOf(TsUnknownCallOutcome.PATH_STOPPED), result.events.map { event -> event.outcome }) + } + + @Test + fun `adjacent Math models preserve special values`() { + val expected = linkedMapOf( + "floorNegativeFraction" to numberToken(-2.0), + "floorNegativeZero" to numberToken(-0.0), + "floorInfinity" to numberToken(Double.POSITIVE_INFINITY), + "truncNegativeFraction" to numberToken(-1.0), + "truncNegativeSmall" to numberToken(-0.0), + "truncNaN" to NAN, + "sqrtFour" to numberToken(2.0), + "sqrtNegative" to NAN, + "sqrtNegativeZero" to numberToken(-0.0), + "sqrtInfinity" to numberToken(Double.POSITIVE_INFINITY), + ) + + val result = analyze(expected.keys.toList()) + + expected.forEach { (methodName, expectedToken) -> + val actual = assertIs(result.values.getValue(methodName).single()).number + + assertEquals(expectedToken, numberToken(actual), methodName) + } + assertEquals( + setOf( + TsNumericIntrinsicModelFamily.MATH_FLOOR_ID, + TsNumericIntrinsicModelFamily.MATH_TRUNC_ID, + TsNumericIntrinsicModelFamily.MATH_SQRT_ID, + ), + result.modelIds.toSet(), + ) + } + + @Test + fun `adjacent Number predicates handle special and non number values`() { + val expected = linkedMapOf( + "finiteNumber" to true, + "finiteNaN" to false, + "finiteInfinity" to false, + "finiteBoolean" to false, + "nanNaN" to true, + "nanNumber" to false, + "nanBoolean" to false, + "safeIntegerMaximum" to true, + "safeIntegerAboveMaximum" to false, + "safeIntegerFraction" to false, + "safeIntegerInfinity" to false, + "safeIntegerBoolean" to false, + ) + + val result = analyze(expected.keys.toList()) + + expected.forEach { (methodName, expectedValue) -> + val actual = assertIs(result.values.getValue(methodName).single()).value + + assertEquals(expectedValue, actual, methodName) + } + assertEquals( + setOf( + TsNumericIntrinsicModelFamily.NUMBER_IS_FINITE_ID, + TsNumericIntrinsicModelFamily.NUMBER_IS_NAN_ID, + TsNumericIntrinsicModelFamily.NUMBER_IS_SAFE_INTEGER_ID, + ), + result.modelIds.toSet(), + ) + } + + private fun analyze( + methodNames: List, + tsOptions: TsOptions = TsOptions(), + ): AnalysisResult { + val methods = methodNames.associateWith(::method) + val observer = RecordingUnknownCallObserver() + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + observer = observer, + ).use { machine -> + val states = machine.analyze(methods.values.toList()) + val values = methods.mapValues { (_, method) -> + states.filter { state -> state.entrypoint === method } + .map { state -> TsTestResolver().resolve(method, state).returnValue } + } + + AnalysisResult( + values = values, + events = observer.events.toList(), + ) + } + } + + private fun method(name: String): EtsMethod = scene.projectClasses + .single { clazz -> clazz.name == DEFAULT_ARK_CLASS_NAME && clazz.declaringFile === sourceFile } + .methods + .single { method -> method.name == name } + + private class RecordingUnknownCallObserver : TsInterpreterObserver { + val events = mutableListOf() + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + private data class AnalysisResult( + val values: Map>, + val events: List, + ) { + val modelIds: List = events.mapNotNull { event -> + (event.decision as? TsUnknownCallDecision.ModelApplied)?.modelId + } + } + + private companion object { + const val NAN: String = "nan" + + fun numberToken(value: Double): String = + if (value.isNaN()) NAN else value.toRawBits().toULong().toString(radix = 16).padStart(16, '0') + + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt index e0083ed8ea..77d8018b3a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -12,6 +12,7 @@ import org.usvm.UMachineOptions import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel +import org.usvm.machine.call.intrinsic.TsNumericIntrinsicModelFamily import org.usvm.machine.state.TsState import kotlin.test.Test import kotlin.test.assertEquals @@ -150,11 +151,28 @@ class TsUnknownCallModelCatalogTest { fun `built in models are discovered once and an explicit empty selection disables all`() { val catalog = TsBuiltInUnknownCallModels.catalog() - assertEquals(listOf("ts.array.pop", TsArrayShiftIntrinsicModel.MODEL_ID), catalog.modelIds) + val expectedModelIds = listOf( + "ts.array.pop", + TsArrayShiftIntrinsicModel.MODEL_ID, + TsNumericIntrinsicModelFamily.MATH_ABS_ID, + TsNumericIntrinsicModelFamily.MATH_CEIL_ID, + TsNumericIntrinsicModelFamily.MATH_FLOOR_ID, + TsNumericIntrinsicModelFamily.MATH_MAX_ID, + TsNumericIntrinsicModelFamily.MATH_MIN_ID, + TsNumericIntrinsicModelFamily.MATH_ROUND_ID, + TsNumericIntrinsicModelFamily.MATH_SQRT_ID, + TsNumericIntrinsicModelFamily.MATH_TRUNC_ID, + TsNumericIntrinsicModelFamily.NUMBER_IS_FINITE_ID, + TsNumericIntrinsicModelFamily.NUMBER_IS_INTEGER_ID, + TsNumericIntrinsicModelFamily.NUMBER_IS_NAN_ID, + TsNumericIntrinsicModelFamily.NUMBER_IS_SAFE_INTEGER_ID, + ) + + assertEquals(expectedModelIds, catalog.modelIds) assertSame(catalog, TsBuiltInUnknownCallModels.catalog()) assertFailsWith { (catalog.modelIds as MutableList).clear() } assertEquals( - listOf("ts.array.pop", TsArrayShiftIntrinsicModel.MODEL_ID), + expectedModelIds, TsBuiltInUnknownCallModels.catalog().modelIds, ) assertTrue(TsBuiltInUnknownCallModels.catalog(TsUnknownCallModelSelection.Only(emptySet())).modelIds.isEmpty()) diff --git a/usvm-ts/src/test/resources/models/BuiltinOwnerBoundary.ts b/usvm-ts/src/test/resources/models/BuiltinOwnerBoundary.ts new file mode 100644 index 0000000000..67af2e6f3e --- /dev/null +++ b/usvm-ts/src/test/resources/models/BuiltinOwnerBoundary.ts @@ -0,0 +1,25 @@ +export class BuiltinOwnerBoundary { + shadowedMath(): number { + const Math = { abs(value: number): number { return value + 79; } }; + + return Math.abs(-2); + } + + shadowedNumber(): boolean { + const Number = { isInteger(_value: number): boolean { return false; } }; + + return Number.isInteger(2); + } + + aliasedMath(): number { + const numeric = Math; + + return numeric.abs(-2); + } + + aliasedNumber(): boolean { + const numeric = Number; + + return numeric.isInteger(1.5); + } +} diff --git a/usvm-ts/src/test/resources/models/NumericIntrinsicModels.ts b/usvm-ts/src/test/resources/models/NumericIntrinsicModels.ts new file mode 100644 index 0000000000..a87c3beed7 --- /dev/null +++ b/usvm-ts/src/test/resources/models/NumericIntrinsicModels.ts @@ -0,0 +1,208 @@ +export function absNegativeZero(): number { + return Math.abs(-0); +} + +export function absNaN(): number { + return Math.abs(0 / 0); +} + +export function absNegativeInfinity(): number { + return Math.abs(-1 / 0); +} + +export function minSignedZero(): number { + return Math.min(0, -0); +} + +export function minNaN(): number { + return Math.min(1, 0 / 0, 2); +} + +export function minNoArguments(): number { + return Math.min(); +} + +export function maxSignedZero(): number { + return Math.max(-0, 0); +} + +export function maxInfinity(): number { + return Math.max(-1 / 0, 1 / 0, 42); +} + +export function maxNoArguments(): number { + return Math.max(); +} + +export function roundNegativeHalf(): number { + return Math.round(-0.5); +} + +export function roundPositiveHalf(): number { + return Math.round(0.5); +} + +export function roundNegativeOneHalf(): number { + return Math.round(-1.5); +} + +export function roundNaN(): number { + return Math.round(0 / 0); +} + +export function ceilNegativeFraction(): number { + return Math.ceil(-0.25); +} + +export function ceilInfinity(): number { + return Math.ceil(1 / 0); +} + +export function absNoArguments(): number { + // @ts-expect-error Arity test deliberately omits the first argument. + return Math.abs(); +} + +export function absExtraArgument(): number { + // @ts-expect-error Arity test deliberately supplies an extra argument. + return Math.abs(-2, true); +} + +export function integerPositiveZero(): boolean { + return Number.isInteger(0); +} + +export function integerNegativeZero(): boolean { + return Number.isInteger(-0); +} + +export function integerFraction(): boolean { + return Number.isInteger(1.5); +} + +export function integerNaN(): boolean { + return Number.isInteger(0 / 0); +} + +export function integerInfinity(): boolean { + return Number.isInteger(1 / 0); +} + +export function integerLargeBinary64(): boolean { + return Number.isInteger(9007199254740992); +} + +export function integerBoolean(): boolean { + return Number.isInteger(true); +} + +export function integerNoArguments(): boolean { + // @ts-expect-error Arity test deliberately omits the first argument. + return Number.isInteger(); +} + +export function integerExtraArgument(): boolean { + // @ts-expect-error Arity test deliberately supplies an extra argument. + return Number.isInteger(2, true); +} + +export function symbolicAbs(value: number): number { + return Math.abs(value) < 0 ? 0 : 1; +} + +export function symbolicInteger(value: number): number { + return Number.isInteger(value) ? 1 : 0; +} + +export function unsupportedAbsDomain(): number { + // @ts-expect-error Domain fallback deliberately supplies a non-number. + return Math.abs(true); +} + +export function floorNegativeFraction(): number { + return Math.floor(-1.25); +} + +export function floorNegativeZero(): number { + return Math.floor(-0); +} + +export function floorInfinity(): number { + return Math.floor(1 / 0); +} + +export function truncNegativeFraction(): number { + return Math.trunc(-1.75); +} + +export function truncNegativeSmall(): number { + return Math.trunc(-0.25); +} + +export function truncNaN(): number { + return Math.trunc(0 / 0); +} + +export function sqrtFour(): number { + return Math.sqrt(4); +} + +export function sqrtNegative(): number { + return Math.sqrt(-1); +} + +export function sqrtNegativeZero(): number { + return Math.sqrt(-0); +} + +export function sqrtInfinity(): number { + return Math.sqrt(1 / 0); +} + +export function finiteNumber(): boolean { + return Number.isFinite(42); +} + +export function finiteNaN(): boolean { + return Number.isFinite(0 / 0); +} + +export function finiteInfinity(): boolean { + return Number.isFinite(1 / 0); +} + +export function finiteBoolean(): boolean { + return Number.isFinite(true); +} + +export function nanNaN(): boolean { + return Number.isNaN(0 / 0); +} + +export function nanNumber(): boolean { + return Number.isNaN(42); +} + +export function nanBoolean(): boolean { + return Number.isNaN(true); +} + +export function safeIntegerMaximum(): boolean { + return Number.isSafeInteger(9007199254740991); +} + +export function safeIntegerAboveMaximum(): boolean { + return Number.isSafeInteger(9007199254740992); +} + +export function safeIntegerFraction(): boolean { + return Number.isSafeInteger(1.5); +} + +export function safeIntegerInfinity(): boolean { + return Number.isSafeInteger(1 / 0); +} + +export function safeIntegerBoolean(): boolean { + return Number.isSafeInteger(true); +}