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 c651b676ca..f46523dc73 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 @@ -1,6 +1,7 @@ package org.usvm.machine.expr import io.ksmt.expr.KFpRoundingMode +import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.model.EtsArrayType @@ -10,10 +11,12 @@ import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.USort import org.usvm.api.allocateConcreteRef import org.usvm.api.initializeArray +import org.usvm.api.initializeArrayLength import org.usvm.api.makeSymbolicPrimitive import org.usvm.api.memcpy import org.usvm.api.typeStreamOf @@ -28,6 +31,7 @@ import org.usvm.types.first import org.usvm.types.firstOrNull import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.boolToFp import org.usvm.util.resolveEtsMethods private val logger = KotlinLogging.logger {} @@ -58,6 +62,17 @@ internal fun TsExprResolver.tryApproximateInstanceCall( if (expr.callee.name == "isNaN") { return from(handleNumberIsNaN(expr)) } + if (expr.callee.name == "isInteger" || expr.callee.name == "isSafeInteger") { + return from(handleNumberIsInteger(expr)) + } + if (expr.callee.name == "isFinite") { + return from(handleNumberIsFinite(expr)) + } + } + + // `console.*` is side-effect-free for the analysis, like `Logger` + if (expr.instance.name == "console") { + return from(mkUndefinedValue()) } // Handle 'Boolean' constructor calls @@ -79,8 +94,15 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `Math` method calls if (expr.instance.name == "Math") { - if (expr.callee.name == "floor") { - return from(handleMathFloor(expr)) + when (expr.callee.name) { + "floor" -> return from(handleMathRounding(expr, KFpRoundingMode.RoundTowardNegative)) + "ceil" -> return from(handleMathRounding(expr, KFpRoundingMode.RoundTowardPositive)) + "trunc" -> return from(handleMathRounding(expr, KFpRoundingMode.RoundTowardZero)) + "round" -> return from(handleMathRound(expr)) + "abs" -> return from(handleMathAbs(expr)) + "sqrt" -> return from(handleMathSqrt(expr)) + "min" -> return from(handleMathMinMax(expr, isMin = true)) + "max" -> return from(handleMathMinMax(expr, isMin = false)) } } @@ -100,6 +122,11 @@ internal fun TsExprResolver.tryApproximateInstanceCall( .takeIf { it !is TsUnresolvedSort } ?: addressSort + // Handle the `Array` constructor: `new Array()` / `new Array(n)` + if (expr.callee.name == CONSTRUCTOR_NAME) { + return from(handleArrayConstructor(expr, instanceType)) + } + // Handle 'Array.push()' method calls if (expr.callee.name == "push") { return from(handleArrayPush(expr, instanceType, elementSort)) @@ -263,27 +290,152 @@ private fun TsExprResolver.handlePromiseResolveReject(expr: EtsInstanceCallExpr) promise } -private fun TsExprResolver.handleMathFloor(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { +/** Resolve the single argument of a Math function as an fp64 value, when possible. */ +private fun TsExprResolver.resolveSingleFpArg(expr: EtsInstanceCallExpr): UExpr? = with(ctx) { check(expr.args.size == 1) { - "Math.floor() should have exactly one argument, but got ${expr.args.size}" + "Math.${expr.callee.name}() should have exactly one argument, but got ${expr.args.size}" } val arg = resolve(expr.args.single()) ?: return null + when { + arg.isFakeObject() -> { + // Constrain the fake object to its numeric alternative: precise Math + // semantics for non-number arguments (ToNumber coercions) is future work. + scope.assert(arg.getFakeType(scope).fpTypeExpr) ?: return null + arg.extractFp(scope) + } - when (arg.sort) { - fp64Sort -> mkFpRoundToIntegralExpr( - roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardNegative), - value = arg.asExpr(fp64Sort), - ) + arg.sort == fp64Sort -> arg.asExpr(fp64Sort) - sizeSort -> arg.asExpr(sizeSort) + arg.sort == boolSort -> boolToFp(arg.asExpr(boolSort)) else -> { - logger.warn { "Unsupported argument sort for Math.floor(): ${arg.sort}" } + logger.warn { "Unsupported argument sort for Math.${expr.callee.name}(): ${arg.sort}" } null } } } +/** `Math.floor` / `Math.ceil` / `Math.trunc`: fp round-to-integral in the corresponding mode. */ +private fun TsExprResolver.handleMathRounding( + expr: EtsInstanceCallExpr, + mode: KFpRoundingMode, +): UExpr<*>? = with(ctx) { + val value = resolveSingleFpArg(expr) ?: return null + mkFpRoundToIntegralExpr(mkFpRoundingModeExpr(mode), value) +} + +/** + * `Math.round(x)` in JS is `floor(x + 0.5)` (halfway cases round towards +Infinity), + * which differs from the IEEE round-to-nearest-even mode. + * (The sign of a `-0` result is not preserved by this encoding.) + */ +private fun TsExprResolver.handleMathRound(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + val value = resolveSingleFpArg(expr) ?: return null + val plusHalf = mkFpAddExpr( + mkFpRoundingModeExpr(KFpRoundingMode.RoundNearestTiesToEven), + value, + mkFp64(0.5), + ) + mkFpRoundToIntegralExpr(mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardNegative), plusHalf) +} + +private fun TsExprResolver.handleMathAbs(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + val value = resolveSingleFpArg(expr) ?: return null + mkFpAbsExpr(value) +} + +private fun TsExprResolver.handleMathSqrt(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + val value = resolveSingleFpArg(expr) ?: return null + mkFpSqrtExpr(mkFpRoundingModeExpr(KFpRoundingMode.RoundNearestTiesToEven), value) +} + +/** + * `Math.min` / `Math.max`. Unlike the IEEE minNum/maxNum operations (which prefer + * the non-NaN operand), JS returns NaN if *any* argument is NaN. + */ +private fun TsExprResolver.handleMathMinMax(expr: EtsInstanceCallExpr, isMin: Boolean): UExpr<*>? = with(ctx) { + val args = expr.args.map { arg -> + val resolved = resolve(arg) ?: return null + when { + resolved.isFakeObject() -> { + scope.assert(resolved.getFakeType(scope).fpTypeExpr) ?: return null + resolved.extractFp(scope) + } + + resolved.sort == fp64Sort -> resolved.asExpr(fp64Sort) + resolved.sort == boolSort -> boolToFp(resolved.asExpr(boolSort)) + else -> { + logger.warn { "Unsupported argument sort for Math.min/max: ${resolved.sort}" } + return null + } + } + } + if (args.isEmpty()) { + // Math.min() == +Infinity, Math.max() == -Infinity + return mkFp64(if (isMin) Double.POSITIVE_INFINITY else Double.NEGATIVE_INFINITY) + } + val anyNaN = args.map { mkFpIsNaNExpr(it) }.reduce { a, b -> mkOr(a, b) } + val pure = args.reduce { a, b -> if (isMin) mkFpMinExpr(a, b) else mkFpMaxExpr(a, b) } + mkIte(anyNaN, mkFp64(Double.NaN), pure) +} + +/** + * 21.1.2.3 `Number.isInteger ( number )`: false for non-numbers, NaN and infinities; + * true iff the value equals its integral rounding. `isSafeInteger` is approximated + * the same way (the 2^53 bound is not modeled). + */ +private fun TsExprResolver.handleNumberIsInteger(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + check(expr.args.size == 1) { "Number.isInteger should have one argument" } + val arg = resolve(expr.args.single()) ?: return null + + fun isIntegral(value: UExpr): UBoolExpr { + val rounded = mkFpRoundToIntegralExpr(mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardZero), value) + return mkAnd( + mkNot(mkFpIsInfiniteExpr(value)), + mkFpEqualExpr(rounded, value), // false for NaN by IEEE equality + ) + } + + if (arg.isFakeObject()) { + val fakeType = arg.getFakeType(scope) + return mkIte( + condition = fakeType.fpTypeExpr, + trueBranch = isIntegral(arg.extractFp(scope)), + falseBranch = mkFalse(), + ) + } + + if (arg.sort == fp64Sort) { + isIntegral(arg.asExpr(fp64Sort)) + } else { + mkFalse() + } +} + +/** 21.1.2.2 `Number.isFinite ( number )`: false for non-numbers, NaN and infinities. */ +private fun TsExprResolver.handleNumberIsFinite(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + check(expr.args.size == 1) { "Number.isFinite should have one argument" } + val arg = resolve(expr.args.single()) ?: return null + + fun isFinite(value: UExpr): UBoolExpr = + mkAnd(mkNot(mkFpIsNaNExpr(value)), mkNot(mkFpIsInfiniteExpr(value))) + + if (arg.isFakeObject()) { + val fakeType = arg.getFakeType(scope) + return mkIte( + condition = fakeType.fpTypeExpr, + trueBranch = isFinite(arg.extractFp(scope)), + falseBranch = mkFalse(), + ) + } + + if (arg.sort == fp64Sort) { + isFinite(arg.asExpr(fp64Sort)) + } else { + mkFalse() + } +} + /** * Handles the `Array.push(...items)` method call. * Appends the specified `items` to the end of the array. @@ -429,6 +581,66 @@ private fun TsExprResolver.handleArrayPop( * * https://tc39.es/ecma262/multipage/indexed-collections.html#sec-array.prototype.fill */ +/** + * The `Array` constructor. `new Array()` keeps the zero length set at allocation; + * `new Array(n)` sets the length to `n`, forking on the validity of the size + * (a non-integral or out-of-range `n` throws a RangeError in JS). + * The multi-argument literal form `new Array(a, b, ...)` is not approximated. + */ +private fun TsExprResolver.handleArrayConstructor( + expr: EtsInstanceCallExpr, + arrayType: EtsArrayType, +): UExpr<*>? = with(ctx) { + val resolved = resolve(expr.instance)?.asExpr(addressSort) ?: return null + val array = resolved as? UConcreteHeapRef ?: run { + logger.warn { "Array constructor on a non-concrete instance is not approximated" } + return null + } + + when (expr.args.size) { + 0 -> array + + 1 -> { + val size = resolve(expr.args.single()) ?: return null + if (size.sort != fp64Sort) { + logger.warn { "Unsupported sort for the Array constructor size: ${size.sort}" } + return null + } + val bvSize = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = size.asExpr(fp64Sort), + bvSize = 32, + isSigned = true, + ) + val isValidSize = mkAnd( + mkEq( + mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = bvSize, + signed = true, + ), + size.asExpr(fp64Sort), + ), + mkBvSignedLessOrEqualExpr(mkBv(0), bvSize.asExpr(bv32Sort)), + ) + scope.fork( + isValidSize, + blockOnFalseState = { throwException("Invalid array length: ${size.asExpr(fp64Sort)}") }, + ) ?: return null + scope.doWithState { + memory.initializeArrayLength(array, arrayType, sizeSort, bvSize.asExpr(sizeSort)) + } + array + } + + else -> { + logger.warn { "The literal form of the Array constructor is not approximated: ${expr.args.size} args" } + null + } + } +} + private fun TsExprResolver.handleArrayFill( expr: EtsInstanceCallExpr, arrayType: EtsArrayType, 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 b283ae66cc..541f7cb1b1 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 @@ -77,6 +77,7 @@ import org.jacodb.ets.model.EtsYieldExpr import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.getDeclaredLocals +import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.UIteExpr import org.usvm.USort @@ -248,24 +249,32 @@ class TsExprResolver( return mkNumericExpr(arg, scope) } - override fun visit(expr: EtsPostIncExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + // NOTE on inc/dec: front ends lower the *side effect* of `x++`/`--x` into an + // explicit assignment (`%t := x; x := ++x`), and the jacodb DTO conversion maps + // both `++` and `--` to the Pre* classes only. Therefore the expressions below + // are pure value computations: Pre* yield ToNumber(arg) +- 1, Post* (which never + // come from the converter, but are part of the model) yield the old value. + + override fun visit(expr: EtsPostIncExpr): UExpr? = with(ctx) { + val arg = resolve(expr.arg) ?: return null + return mkNumericExpr(arg, scope) } - override fun visit(expr: EtsPostDecExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsPostDecExpr): UExpr? = with(ctx) { + val arg = resolve(expr.arg) ?: return null + return mkNumericExpr(arg, scope) } - override fun visit(expr: EtsPreIncExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsPreIncExpr): UExpr? = with(ctx) { + val arg = resolve(expr.arg) ?: return null + val numeric = mkNumericExpr(arg, scope).asExpr(fp64Sort) + return mkFpAddExpr(fpRoundingModeSortDefaultValue(), numeric, mkFp64(1.0)) } - override fun visit(expr: EtsPreDecExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsPreDecExpr): UExpr? = with(ctx) { + val arg = resolve(expr.arg) ?: return null + val numeric = mkNumericExpr(arg, scope).asExpr(fp64Sort) + return mkFpSubExpr(fpRoundingModeSortDefaultValue(), numeric, mkFp64(1.0)) } override fun visit(expr: EtsBitNotExpr): UExpr? = with(ctx) { @@ -782,9 +791,35 @@ class TsExprResolver( } override fun visit(expr: EtsNotEqExpr): UExpr? { + truthinessIdiomOrNull(expr.left, expr.right)?.let { truthy -> + return truthy + } return resolveBinaryOperator(TsBinaryOperator.Neq, expr) } + /** + * Front ends lower the truthiness test `if (x)` into the compare idiom + * `x != 0` (ArkAnalyzer) / `x != false` (ts-frontend) — byte-identical to a + * genuine loose comparison in the IR. The numeric reading diverges from + * ToBoolean on both axes: `undefined != 0` evaluates to + * ToNumber(undefined) = NaN != 0 = true although `undefined` is falsy, and + * `NaN != 0` is true although `NaN` is falsy. Follow the idiom contract: + * `!=` against literal zero/false is ToBoolean for ALL operand kinds + * (bool/fp/ref/fake), matching the concrete ArkIR interpreter of the + * hybrid pipeline. Note the idiom only ever uses `!=` (negated tests swap + * the branch successors instead), so `==` keeps the literal semantics. + * + * @return the truthiness expression, or null when the idiom does not apply. + */ + private fun truthinessIdiomOrNull(left: EtsEntity, right: EtsEntity): UBoolExpr? = with(ctx) { + val isZeroOrFalse = (right is EtsNumberConstant && right.value == 0.0) || + (right is EtsBooleanConstant && !right.value) + if (!isZeroOrFalse) return null + + val lhs = resolve(left) ?: return null + mkTruthyExpr(lhs, scope) + } + override fun visit(expr: EtsStrictEqExpr): UExpr? { return resolveBinaryOperator(TsBinaryOperator.StrictEq, expr) } @@ -965,6 +1000,18 @@ class TsExprResolver( expr.type } + if (expr.type.typeName == "Array") { + // `new Array(...)`: allocate a genuine array object so that the array + // approximations apply; the length is set by the constructor call + // that immediately follows the allocation. + val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + return@with scope.calcOnState { + val address = memory.allocConcrete(arrayType) + memory.initializeArrayLength(address, arrayType, sizeSort, mkBv(0).asExpr(sizeSort)) + address + } + } + if (expr.type.typeName == "Boolean") { val clazz = scene.sdkClasses.filter { it.name == "Boolean" }.maxByOrNull { it.methods.size } ?: error("No Boolean class found in SDK") diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 850f97e9de..2933befcac 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -183,7 +183,12 @@ class TsInterpreter( } return } - scope.assert(falseExpr) + // Approximate a call on an unresolved class with a mock instead of + // killing the state: otherwise a single unmodeled call (e.g. an SDK + // function) makes everything after it unreachable. + logger.warn { "Mocking a call on an unresolved class: ${stmt.callee} (over-approximation)" } + mockMethodCall(scope, stmt.callee) + scope.doWithState { newStmt(stmt.returnSite) } return } if (classes.size > 1) { @@ -203,7 +208,10 @@ class TsInterpreter( logger.warn { "Could not resolve method: ${stmt.callee} on type: $type" } - scope.assert(falseExpr) + // Mock instead of killing the state (see the comment above). + logger.warn { "Mocking an unresolved call: ${stmt.callee} (over-approximation)" } + mockMethodCall(scope, stmt.callee) + scope.doWithState { newStmt(stmt.returnSite) } return } } else { @@ -212,7 +220,10 @@ class TsInterpreter( if (stmt.callee.name !in listOf("then")) { logger.warn { "Could not resolve method: ${stmt.callee}" } } - scope.assert(falseExpr) + // Mock instead of killing the state (see the comment above). + logger.warn { "Mocking an unresolved call: ${stmt.callee} (over-approximation)" } + mockMethodCall(scope, stmt.callee) + scope.doWithState { newStmt(stmt.returnSite) } return } concreteMethods += methods diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/IncDecExprTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/IncDecExprTest.kt new file mode 100644 index 0000000000..d1ef32f653 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/IncDecExprTest.kt @@ -0,0 +1,122 @@ +package org.usvm.machine + +import org.jacodb.ets.model.BasicBlock +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsBlockCfg +import org.jacodb.ets.model.EtsClassImpl +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethodImpl +import org.jacodb.ets.model.EtsMethodParameter +import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsPostDecExpr +import org.jacodb.ets.model.EtsPostIncExpr +import org.jacodb.ets.model.EtsPreDecExpr +import org.jacodb.ets.model.EtsPreIncExpr +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmtLocation +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Test +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.util.TsTestResolver +import kotlin.time.Duration.Companion.seconds + +/** + * Direct tests for the inc/dec expression resolution. + * + * The IR is built programmatically: ArkAnalyzer never emits `++`/`--` unary + * expressions (it expands them into `x := x + 1`), while the native ts-frontend + * does emit them (as the value part, with an explicit write-back assignment), + * so sample-based tests cannot exercise these visits. + */ +class IncDecExprTest { + + private fun buildMethod(name: String, makeExpr: (EtsEntity) -> EtsEntity): Pair { + val fileSig = EtsFileSignature(projectName = "test", fileName = "IncDec.ts") + val classSig = EtsClassSignature(name = "T", file = fileSig) + val method = EtsMethodImpl( + signature = EtsMethodSignature( + enclosingClass = classSig, + name = name, + parameters = listOf(EtsMethodParameter(0, "a", EtsNumberType)), + returnType = EtsNumberType, + ), + ) + + fun loc(i: Int) = EtsStmtLocation(method, i) + val a = EtsLocal("a", EtsNumberType) + val res = EtsLocal("res", EtsNumberType) + val stmts = listOf( + EtsAssignStmt(loc(0), a, EtsParameterRef(0, EtsNumberType)), + EtsAssignStmt(loc(1), res, makeExpr(a)), + EtsReturnStmt(loc(2), res), + ) + method.body.cfg = EtsBlockCfg( + blocks = listOf(BasicBlock(0, stmts)), + successors = mapOf(0 to emptyList()), + ) + method.body.locals = listOf(a, res) + + val cls = EtsClassImpl(signature = classSig, fields = emptyList(), methods = listOf(method)) + val file = EtsFile(signature = fileSig, classes = listOf(cls), namespaces = emptyList()) + return EtsScene(listOf(file)) to method + } + + private fun run(name: String, makeExpr: (EtsEntity) -> EtsEntity): List> { + val (scene, method) = buildMethod(name, makeExpr) + val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + exceptionsPropagation = true, + timeout = 20.seconds, + solverType = SolverType.YICES, + ) + val states = TsMachine(scene, options, TsOptions()).use { machine -> + machine.analyze(listOf(method)) + } + assertTrue(states.isNotEmpty()) { "no states collected for $name" } + return states.mapNotNull { state -> + val test = TsTestResolver().resolve(method, state) + val input = (test.before.parameters.firstOrNull() as? TsTestValue.TsNumber)?.number + val result = (test.returnValue as? TsTestValue.TsNumber)?.number + if (input != null && result != null) input to result else null + }.also { assertTrue(it.isNotEmpty()) { "no numeric executions for $name" } } + } + + @Test + fun `pre-increment yields arg plus one`() { + for ((input, result) in run("preInc") { EtsPreIncExpr(it, EtsNumberType) }) { + if (input.isNaN()) assertTrue(result.isNaN()) + else assertEquals(input + 1, result, 0.0) { "++($input)" } + } + } + + @Test + fun `pre-decrement yields arg minus one`() { + for ((input, result) in run("preDec") { EtsPreDecExpr(it, EtsNumberType) }) { + if (input.isNaN()) assertTrue(result.isNaN()) + else assertEquals(input - 1, result, 0.0) { "--($input)" } + } + } + + @Test + fun `post-increment and post-decrement yield the old value`() { + for ((input, result) in run("postInc") { EtsPostIncExpr(it, EtsNumberType) }) { + if (input.isNaN()) assertTrue(result.isNaN()) + else assertEquals(input, result, 0.0) { "($input)++" } + } + for ((input, result) in run("postDec") { EtsPostDecExpr(it, EtsNumberType) }) { + if (input.isNaN()) assertTrue(result.isNaN()) + else assertEquals(input, result, 0.0) { "($input)--" } + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/IncDec.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/IncDec.kt new file mode 100644 index 0000000000..91ef1bdb6c --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/IncDec.kt @@ -0,0 +1,60 @@ +package org.usvm.samples.operators + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.eq +import org.usvm.util.isNaN + +class IncDec : TsMethodTestRunner() { + private val tsPath = "/samples/operators/IncDec.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `test preIncrement`() { + val method = getMethod("preIncrement") + discoverProperties( + method = method, + { a, r -> a.isNaN() && r.isNaN() }, + { a, r -> !a.isNaN() && (r.number eq a.number + 1) }, + invariants = arrayOf( + { a, r -> + if (a.isNaN()) r.isNaN() else r.number eq a.number + 1 + }, + ) + ) + } + + @Test + fun `test preDecrement`() { + val method = getMethod("preDecrement") + discoverProperties( + method = method, + { a, r -> a.isNaN() && r.isNaN() }, + { a, r -> !a.isNaN() && (r.number eq a.number - 1) }, + invariants = arrayOf( + { a, r -> + if (a.isNaN()) r.isNaN() else r.number eq a.number - 1 + }, + ) + ) + } + + @Test + fun `test decrementLoop`() { + val method = getMethod("decrementLoop") + discoverProperties( + method = method, + // Classify by the observed depth, not by n: non-integral inputs + // (e.g. n = 2.5) legitimately reach depth ceil(n). + { n, r -> (n.number <= 0 || n.isNaN()) && (r eq 0) }, + { n, r -> r eq 3 }, + { n, r -> r.number > 0 && r.number < 3 }, + invariants = arrayOf( + { _, r -> r.number >= 0 && r.number <= 3 }, + ), + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/operators/IncDec.ts b/usvm-ts/src/test/resources/samples/operators/IncDec.ts new file mode 100644 index 0000000000..5dfa95d54d --- /dev/null +++ b/usvm-ts/src/test/resources/samples/operators/IncDec.ts @@ -0,0 +1,42 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class IncDec { + preIncrement(a: number): number { + let x = a; + ++x; + if (Number.isNaN(a)) return x; // NaN + 1 == NaN + if (a == 0) return x; // ++0 == 1 + if (a > 0) return x; + if (a < 0) return x; + // unreachable + } + + // NOTE: a `const old = x++` case is deliberately absent: ArkAnalyzer + // (neo/2025-09-03) lowers it as `x := x + 1; old := x`, i.e. `old` receives + // the *new* value — a frontend lowering bug that no engine semantics can fix. + + preDecrement(a: number): number { + let x = a; + --x; + if (Number.isNaN(a)) return x; // NaN - 1 == NaN + if (a == 0) return x; // --0 == -1 + if (a > 0) return x; + if (a < 0) return x; + // unreachable + } + + decrementLoop(n: number): number { + let count = 0; + let x = n; + while (x > 0 && count < 3) { + x--; + count++; + } + // Each loop depth is a distinct branch so that full coverage requires + // the engine to actually unroll the decrementing loop. + if (count == 0) return count; + if (count == 3) return count; + return count; // 1 or 2 iterations + } +}