diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 34faf3df14..0802421971 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -148,6 +148,11 @@ jobs: echo "ARKANALYZER_DIR=$(realpath $DEST_DIR)" >> $GITHUB_ENV cd $DEST_DIR + # ArkAnalyzer's bundled TypeScript 4.9 cannot parse syntax from the + # latest floating @types/node, so pin a compatible major before the + # single install. A second install would prune the postinstall-only + # ohos-typescript package because it is absent from package.json. + npm pkg set 'devDependencies.@types/node=18' npm install npm run build diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index fe81c5630b..9e465a8ecc 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "b17013382a" + const val jacodb = "9ea33879c9" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" diff --git a/settings.gradle.kts b/settings.gradle.kts index 428d679fce..a408cda64d 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -55,18 +55,23 @@ findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons" // Actually, relative path is enough, but there is a bug in IDEA when the path is a symlink. // As a workaround, we convert it to a real absolute path. // See IDEA bug: https://youtrack.jetbrains.com/issue/IDEA-329756 -// val jacodbPath = file("jacodb").takeIf { it.exists() } -// ?: file("../jacodb").takeIf { it.exists() } -// ?: error("Local JacoDB directory not found") -// includeBuild(jacodbPath.toPath().toRealPath().toAbsolutePath()) { -// dependencySubstitution { -// all { -// val requested = requested -// if (requested is ModuleComponentSelector && requested.group == "com.github.UnitTestBot.jacodb") { -// val targetProject = ":${requested.module}" -// useTarget(project(targetProject)) -// logger.info("Substituting ${requested.group}:${requested.module} with $targetProject") -// } -// } -// } -// } +// Opt-in local JacoDB substitution: -PuseLocalJacodb[=] (default: ./jacodb or ../jacodb) +if (extra.has("useLocalJacodb")) { + val prop = extra.get("useLocalJacodb")?.toString() + val jacodbPath = prop?.takeIf { it.isNotBlank() && it != "true" }?.let { file(it) } + ?: file("jacodb").takeIf { it.exists() } + ?: file("../jacodb").takeIf { it.exists() } + ?: error("Local JacoDB directory not found") + includeBuild(jacodbPath.toPath().toRealPath().toAbsolutePath()) { + dependencySubstitution { + all { + val requested = requested + if (requested is ModuleComponentSelector && requested.group == "com.github.UnitTestBot.jacodb") { + val targetProject = ":${requested.module}" + useTarget(project(targetProject)) + logger.info("Substituting ${requested.group}:${requested.module} with $targetProject") + } + } + } + } +} diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt index a9cd0ec33a..25f38ddec9 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt @@ -67,7 +67,6 @@ import kotlin.io.path.toPath import kotlin.test.assertContains import kotlin.test.assertEquals import kotlin.test.assertIs -import kotlin.test.assertNotEquals import kotlin.test.assertTrue private val logger = KotlinLogging.logger {} @@ -304,7 +303,7 @@ class EtsTypeInferenceTest { } @Test - fun `test if guesser does anything`() { + fun `type guesser reaches a fixed point after one pass`() { val name = "testcases" val file = load("/ts/$name.ts") val project = EtsScene(listOf(file)) @@ -322,8 +321,9 @@ class EtsTypeInferenceTest { val manager = TypeInferenceManager(EtsTraits(), graph) val resultWithoutGuessed = manager.analyze(entrypoints) val resultWithGuessed = resultWithoutGuessed.withGuessedTypes(guesser) + val resultWithGuessedTwice = resultWithGuessed.withGuessedTypes(guesser) - assertNotEquals(resultWithoutGuessed.inferredTypes, resultWithGuessed.inferredTypes) + assertEquals(resultWithGuessed, resultWithGuessedTwice) println("=".repeat(42)) println("Inferred types WITHOUT guesser: ") diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 39370250cb..9ae27cb06e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -5,16 +5,20 @@ import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsAliasType import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanLiteralType import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsEnumValueType import org.jacodb.ets.model.EtsGenericType import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsLexicalEnvType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsNumberLiteralType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStringLiteralType import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsThis import org.jacodb.ets.model.EtsType @@ -134,13 +138,17 @@ class TsContext( } fun typeToSort(type: EtsType): USort = when (type) { + is EtsBooleanLiteralType -> boolSort is EtsBooleanType -> boolSort + is EtsNumberLiteralType -> fp64Sort is EtsNumberType -> fp64Sort + is EtsStringLiteralType -> addressSort is EtsStringType -> addressSort is EtsNullType -> addressSort is EtsUndefinedType -> addressSort is EtsUnionType -> unresolvedSort is EtsRefType -> addressSort + is EtsLexicalEnvType -> addressSort is EtsAnyType -> unresolvedSort is EtsUnknownType -> unresolvedSort is EtsAliasType -> typeToSort(type.originalType) 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..4aecbb62eb 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 @@ -485,18 +485,20 @@ private fun TsExprResolver.handleArrayFill( } scope.calcOnState { + val descriptor = arrayDescriptorOf(arrayType) + // Calculate the length of the range to fill val fillLength = mkBvSubExpr(endBv, startBv) // TODO: check that `fillLength` is less than `ARRAY_FILL_MAX_SIZE` // Allocate a temporary array to hold the filled values - val tempArray = memory.allocConcrete(arrayType) + val tempArray = memory.allocConcrete(descriptor) // Fill the temporary array with the specified `value` memory.initializeArray( tempArray, - arrayType, + descriptor, elementSort, sizeSort, (0 until ARRAY_FILL_MAX_SIZE).asSequence().map { value.asExpr(elementSort) } @@ -506,7 +508,7 @@ private fun TsExprResolver.handleArrayFill( memory.memcpy( srcRef = tempArray, dstRef = array, - type = arrayType, + type = descriptor, elementSort = elementSort, fromSrc = mkBv(0), fromDst = startBv, @@ -777,17 +779,19 @@ private fun TsExprResolver.handleArraySlice( } scope.calcOnState { + val descriptor = arrayDescriptorOf(arrayType) + // Calculate the new length of the sliced array val newLength = mkBvSubExpr(endBv, startBv) // Allocate a new array for the slice - val slicedArray = memory.allocConcrete(arrayType) + val slicedArray = memory.allocConcrete(descriptor) // Copy the specified range from the original array to the new array memory.memcpy( srcRef = array, dstRef = slicedArray, - type = arrayType, + type = descriptor, elementSort = elementSort, fromSrc = startBv, fromDst = mkBv(0), @@ -830,8 +834,10 @@ private fun TsExprResolver.handleArrayConcat( val args = expr.args.map { resolve(it) ?: return null } scope.calcOnState { + val descriptor = arrayDescriptorOf(arrayType) + // Allocate a new array for the concatenated result - val resultArray = memory.allocConcrete(arrayType) + val resultArray = memory.allocConcrete(descriptor) // Read the length of the original array val originalLengthLValue = mkArrayLengthLValue(array, arrayType) @@ -841,7 +847,7 @@ private fun TsExprResolver.handleArrayConcat( memory.memcpy( srcRef = array, dstRef = resultArray, - type = arrayType, + type = descriptor, elementSort = elementSort, fromSrc = mkBv(0), fromDst = mkBv(0), @@ -863,7 +869,7 @@ private fun TsExprResolver.handleArrayConcat( memory.memcpy( srcRef = arg.asExpr(addressSort), dstRef = resultArray, - type = arrayType, + type = descriptor, elementSort = elementSort, fromSrc = mkBv(0), fromDst = totalLength, @@ -1037,8 +1043,10 @@ private fun TsExprResolver.handleArrayReverse( } scope.calcOnState { + val descriptor = arrayDescriptorOf(arrayType) + // Allocate a new array to represent the reversed result - val reversedArray = memory.allocConcrete(arrayType) + val reversedArray = memory.allocConcrete(descriptor) // Read the length of the original array val lengthLValue = mkArrayLengthLValue(array, arrayType) @@ -1047,7 +1055,7 @@ private fun TsExprResolver.handleArrayReverse( // Initialize the reversed array with symbolic elements memory.initializeArray( reversedArray, - arrayType, + descriptor, elementSort, sizeSort, (0 until ARRAY_REVERSE_MAX_SIZE).asSequence().map { index -> @@ -1073,7 +1081,7 @@ private fun TsExprResolver.handleArrayReverse( memory.memcpy( srcRef = reversedArray, dstRef = array, - type = arrayType, + type = descriptor, elementSort = elementSort, fromSrc = mkBv(0), fromDst = mkBv(0), diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt index f7ca10ca7e..4f53b8bea8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt @@ -16,6 +16,7 @@ import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.lastStmt import org.usvm.machine.state.newStmt import org.usvm.util.TsResolutionResult +import org.usvm.util.canonicalizeExecutableOverloads private val logger = KotlinLogging.logger {} @@ -70,14 +71,18 @@ private fun TsExprResolver.resolveStaticMethod( if (method.enclosingClass.name != UNKNOWN_CLASS_NAME) { val classes = hierarchy.classesForType(EtsClassType(method.enclosingClass)) if (classes.size > 1) { - val methods = classes.map { it.methods.single { it.name == method.name } } + val methods = classes + .flatMap { clazz -> clazz.methods.filter { it.name == method.name } } + .canonicalizeExecutableOverloads() return TsResolutionResult.create(methods) } if (classes.isEmpty()) return TsResolutionResult.Empty val clazz = classes.single() - val methods = clazz.methods.filter { it.name == method.name } + val methods = clazz.methods + .filter { it.name == method.name } + .canonicalizeExecutableOverloads() return TsResolutionResult.create(methods) } @@ -85,6 +90,7 @@ private fun TsExprResolver.resolveStaticMethod( val methods = ctx.scene.projectAndSdkClasses .flatMap { it.methods } .filter { it.name == method.name } + .canonicalizeExecutableOverloads() return TsResolutionResult.create(methods) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStaticApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStaticApproximations.kt index 5aeb93a092..16cb646287 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStaticApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStaticApproximations.kt @@ -1,6 +1,7 @@ package org.usvm.machine.expr import org.jacodb.ets.model.EtsStaticCallExpr +import org.jacodb.ets.model.EtsValue import org.usvm.UExpr import org.usvm.machine.expr.TsExprApproximationResult.Companion.from @@ -14,7 +15,7 @@ internal fun TsExprResolver.tryApproximateStaticCall( // Handle `Number(...)` calls if (expr.callee.name == "Number") { - return from(handleNumberConverter(expr)) + return from(handleNumberConverter(expr.args)) } // Handle `Boolean(...)` calls @@ -33,11 +34,14 @@ private fun TsExprResolver.handleR(): UExpr<*> = with(ctx) { mockSymbol } -private fun TsExprResolver.handleNumberConverter(expr: EtsStaticCallExpr): UExpr<*>? = with(ctx) { - check(expr.args.size == 1) { - "Number() should have exactly one argument, but got ${expr.args.size}" +internal fun TsExprResolver.handleNumberConverter(args: List): UExpr<*>? = with(ctx) { + if (args.isEmpty()) { + return mkFp64(0.0) } - val arg = resolve(expr.args.single()) ?: return null + check(args.size == 1) { + "Number() should have exactly one argument, but got ${args.size}" + } + val arg = resolve(args.single()) ?: return null return mkNumericExpr(arg, scope) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/EcmaScriptNumberToString.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/EcmaScriptNumberToString.kt new file mode 100644 index 0000000000..c7f0f31ba4 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/EcmaScriptNumberToString.kt @@ -0,0 +1,85 @@ +package org.usvm.machine.expr + +import java.math.BigDecimal +import java.math.BigInteger +import java.math.MathContext +import java.math.RoundingMode +import kotlin.math.absoluteValue + +private const val MAX_SIGNIFICANT_DIGITS = 17 +private const val MAX_PLAIN_DECIMAL_POINT = 21 +private const val MIN_PLAIN_DECIMAL_POINT = -5 +private const val ROUNDING_NEIGHBORHOOD = 2 + +/** Formats a concrete IEEE-754 value according to ECMAScript Number::toString. */ +internal fun Double.toEcmaScriptString(): String = when { + isNaN() -> { + "NaN" + } + + this == Double.POSITIVE_INFINITY -> { + "Infinity" + } + + this == Double.NEGATIVE_INFINITY -> { + "-Infinity" + } + + this == 0.0 -> { + "0" + } + + else -> { + val negative = this < 0.0 + val decimal = absoluteValue.shortestRoundTripDecimal().stripTrailingZeros() + val digits = decimal.unscaledValue().abs().toString() + val decimalPoint = digits.length - decimal.scale() + val unsigned = when { + decimalPoint in 1..MAX_PLAIN_DECIMAL_POINT -> { + if (decimalPoint >= digits.length) { + digits + "0".repeat(decimalPoint - digits.length) + } else { + digits.substring(0, decimalPoint) + "." + digits.substring(decimalPoint) + } + } + + decimalPoint in MIN_PLAIN_DECIMAL_POINT..0 -> { + "0." + "0".repeat(-decimalPoint) + digits + } + + else -> { + val mantissa = if (digits.length == 1) { + digits + } else { + digits.substring(0, 1) + "." + digits.substring(1) + } + val exponent = decimalPoint - 1 + mantissa + "e" + (if (exponent >= 0) "+" else "") + exponent + } + } + if (negative) "-$unsigned" else unsigned + } +} + +private fun Double.shortestRoundTripDecimal(): BigDecimal { + // This constructor intentionally retains the exact binary value. At the first + // precision that round-trips, ECMAScript selects the closest decimal (ties to even). + val exact = BigDecimal(this) + for (precision in 1..MAX_SIGNIFICANT_DIGITS) { + val rounded = exact.round(MathContext(precision, RoundingMode.HALF_EVEN)) + val unit = rounded.ulp() + val candidates = (-ROUNDING_NEIGHBORHOOD..ROUNDING_NEIGHBORHOOD) + .asSequence() + .map { offset -> rounded + unit * offset.toBigDecimal() } + .filter { candidate -> candidate.signum() > 0 && candidate.toDouble() == this } + .toList() + if (candidates.isNotEmpty()) { + return candidates.minWith( + compareBy { candidate -> candidate.subtract(exact).abs() } + .thenBy { candidate -> candidate.unscaledValue().abs().and(BigInteger.ONE).toInt() } + .thenBy { candidate -> candidate }, + ) + } + } + error("Could not format finite double: $this") +} 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..58fa7eca6b 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 @@ -1,10 +1,12 @@ package org.usvm.machine.expr +import io.ksmt.expr.KFp64Value import io.ksmt.utils.asExpr import io.ksmt.utils.cast import mu.KotlinLogging import org.jacodb.ets.model.EtsAddExpr import org.jacodb.ets.model.EtsAndExpr +import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsAwaitExpr @@ -47,6 +49,7 @@ import org.jacodb.ets.model.EtsNotExpr import org.jacodb.ets.model.EtsNullConstant import org.jacodb.ets.model.EtsNullishCoalescingExpr import org.jacodb.ets.model.EtsNumberConstant +import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsOrExpr import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsPostDecExpr @@ -77,7 +80,9 @@ 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.UConcreteHeapRef import org.usvm.UExpr +import org.usvm.UHeapRef import org.usvm.UIteExpr import org.usvm.USort import org.usvm.api.allocateConcreteRef @@ -104,6 +109,7 @@ import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.lastStmt import org.usvm.machine.state.localsCount import org.usvm.machine.state.newStmt +import org.usvm.machine.types.EtsNominalType import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.sizeSort import org.usvm.util.EtsHierarchy @@ -131,6 +137,11 @@ private const val ECMASCRIPT_BITWISE_INTEGER_SIZE = 32 */ private const val ECMASCRIPT_BITWISE_SHIFT_MASK = 0b11111 +private enum class UpdateOperator { + INCREMENT, + DECREMENT, +} + class TsExprResolver( internal val ctx: TsContext, internal val scope: TsStepScope, @@ -249,23 +260,43 @@ class TsExprResolver( } override fun visit(expr: EtsPostIncExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + return resolveUpdateExpression(expr.arg, UpdateOperator.INCREMENT, returnOldValue = true) } override fun visit(expr: EtsPostDecExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + return resolveUpdateExpression(expr.arg, UpdateOperator.DECREMENT, returnOldValue = true) } override fun visit(expr: EtsPreIncExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + return resolveUpdateExpression(expr.arg, UpdateOperator.INCREMENT, returnOldValue = false) } override fun visit(expr: EtsPreDecExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + return resolveUpdateExpression(expr.arg, UpdateOperator.DECREMENT, returnOldValue = false) + } + + private fun resolveUpdateExpression( + target: EtsEntity, + operator: UpdateOperator, + returnOldValue: Boolean, + ): UExpr? = with(ctx) { + val oldValue = resolve(target) ?: return null + val oldNumericValue = mkNumericExpr(oldValue, scope) + val one = mkFp64(1.0) + val updatedValue = when (operator) { + UpdateOperator.INCREMENT -> mkFpAddExpr(fpRoundingModeSortDefaultValue(), oldNumericValue, one) + UpdateOperator.DECREMENT -> mkFpSubExpr(fpRoundingModeSortDefaultValue(), oldNumericValue, one) + } + + when (target) { + is EtsLocal -> handleAssignToLocal(target, updatedValue) + is EtsArrayAccess -> handleAssignToArrayIndex(target, updatedValue) + is EtsInstanceFieldRef -> handleAssignToInstanceField(target, updatedValue) + is EtsStaticFieldRef -> handleAssignToStaticField(target, updatedValue) + else -> error("Increment and decrement require an assignable target, got: $target") + } ?: return null + + if (returnOldValue) oldNumericValue else updatedValue } override fun visit(expr: EtsBitNotExpr): UExpr? = with(ctx) { @@ -543,9 +574,30 @@ class TsExprResolver( // region BINARY override fun visit(expr: EtsAddExpr): UExpr? { + if (expr.type == EtsStringType) { + return resolveAfterResolved(expr.left, expr.right) { lhs, rhs -> + val lhsString = concreteStringValue(lhs) + ?: error("Symbolic string concatenation is not supported for left operand: $lhs") + val rhsString = concreteStringValue(rhs) + ?: error("Symbolic string concatenation is not supported for right operand: $rhs") + ctx.mkStringConstant(lhsString + rhsString, scope) + } + } return resolveBinaryOperator(TsBinaryOperator.Add, expr) } + private fun concreteStringValue(value: UExpr<*>): String? = with(ctx) { + when { + value == trueExpr -> "true" + value == falseExpr -> "false" + value == mkTsNullValue() -> "null" + value == mkUndefinedValue() -> "undefined" + value is KFp64Value -> value.value.toEcmaScriptString() + value is UConcreteHeapRef -> getStringConstantValue(value) + else -> null + } + } + override fun visit(expr: EtsSubExpr): UExpr? { return resolveBinaryOperator(TsBinaryOperator.Sub, expr) } @@ -834,8 +886,10 @@ class TsExprResolver( override fun visit(expr: EtsInstanceOfExpr): UExpr? = with(ctx) { val arg = resolve(expr.arg)?.asExpr(addressSort) ?: return null + val checkType = expr.checkType as? EtsRefType ?: return falseExpr + scope.calcOnState { - memory.types.evalIsSubtype(arg, expr.checkType) + memory.types.evalIsSubtype(arg, EtsNominalType(checkType)) } } @@ -848,6 +902,10 @@ class TsExprResolver( override fun visit(expr: EtsStaticCallExpr): UExpr<*>? = handleStaticCall(expr) override fun visit(expr: EtsPtrCallExpr): UExpr? = with(ctx) { + if (expr.isBuiltInNumberConverter()) { + return handleNumberConverter(expr.args) + } + when (val result = scope.calcOnState { methodResult }) { is TsMethodResult.Success -> { scope.doWithState { methodResult = TsMethodResult.NoCall } @@ -897,7 +955,10 @@ class TsExprResolver( val callee = scope.calcOnState { associatedFunction[ptr] ?: error("No associated methods for ptr: $ptr") } - val resolvedArgs = expr.args.map { resolve(it) ?: return null } + val resolvedArgs = buildList { + callee.closure?.let(::add) + expr.args.mapTo(this) { resolve(it) ?: return null } + } val concreteCall = TsConcreteMethodCallStmt( callee = callee.method, instance = callee.thisInstance ?: ctx.mkUndefinedValue(), @@ -914,6 +975,24 @@ class TsExprResolver( } } + private fun EtsPtrCallExpr.isBuiltInNumberConverter(): Boolean { + val hasBuiltInCallSite = callee.name == "Number" && + callee.enclosingClass == EtsClassSignature.UNKNOWN && + ptr.name == "Number" + if (!hasBuiltInCallSite) { + return false + } + + val signature = (ptr.type as? EtsFunctionType)?.signature ?: return false + 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 + } + // endregion // region ACCESS @@ -1026,8 +1105,9 @@ class TsExprResolver( TODO("Multidimensional arrays are not supported yet, https://github.com/UnitTestBot/usvm/issues/287") } - val address = memory.allocConcrete(arrayType) - memory.initializeArrayLength(address, arrayType, sizeSort, bvSize) + val descriptor = arrayDescriptorOf(arrayType) + val address = memory.allocConcrete(descriptor) + memory.initializeArrayLength(address, descriptor, sizeSort, bvSize) address } @@ -1046,17 +1126,22 @@ class TsSimpleValueResolver( "Expected EtsLocal, EtsThis, or EtsParameterRef, but got ${local::class.java}: $local" } + val currentMethod = scope.calcOnState { lastEnteredMethod } + // Handle closures if (local is EtsLocal && local.name.startsWith("%closures")) { - // TODO: add comments - val existingClosures = scope.calcOnState { closureObject[local.name] } - if (existingClosures != null) { - return existingClosures + val idx = getLocalIdx(local, currentMethod) + if (idx != null) { + val initializedSort = scope.calcOnState { getSortForLocal(idx) } + if (initializedSort != null) { + val lValue = mkRegisterStackLValue(initializedSort, idx) + return scope.calcOnState { memory.read(lValue) } + } } + val type = local.type check(type is EtsLexicalEnvType) val obj = allocateConcreteRef() - // TODO: consider 'types.allocate' for (captured in type.closures) { val resolvedCaptured = resolveLocal(captured) ?: return null val lValue = mkFieldLValue(resolvedCaptured.sort, obj, captured.name) @@ -1064,14 +1149,9 @@ class TsSimpleValueResolver( memory.write(lValue, resolvedCaptured.cast(), guard = trueExpr) } } - scope.doWithState { - setClosureObject(local.name, obj) - } return obj } - val currentMethod = scope.calcOnState { lastEnteredMethod } - // Locals in %dflt method are a little bit *special*... if (currentMethod.name == DEFAULT_ARK_METHOD_NAME) { val file = currentMethod.enclosingClass!!.declaringFile!! @@ -1179,7 +1259,17 @@ class TsSimpleValueResolver( return null } val method = methods.single() - val ref = scope.calcOnState { getMethodRef(method) } + val closureParameter = method.parameters + .firstOrNull() + ?.takeIf { it.type is EtsLexicalEnvType } + val closure: UHeapRef? = if (closureParameter != null) { + val closureLocal = EtsLocal(closureParameter.name, closureParameter.type) + val resolved = resolveLocal(closureLocal) ?: return null + resolved.asExpr(ctx.addressSort) + } else { + null + } + val ref = scope.calcOnState { getMethodRef(method, closure = closure) } return ref } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index 3740f4634d..c553668414 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -12,6 +12,7 @@ import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.interpreter.ensureStaticsInitialized import org.usvm.machine.types.EtsAuxiliaryType import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult @@ -134,11 +135,11 @@ fun TsContext.assignToStaticField( it.signature == field.enclosingClass } ?: return null - val instance = scope.calcOnState { getStaticInstance(clazz) } + // Static initialization precedes the first read or write. In particular, + // a module initializer must not overwrite a value written by the caller. + ensureStaticsInitialized(scope, clazz) ?: return null - // TODO: initialize the static field first - // Note: Since we are assigning to a static field, we can omit its initialization, - // if it does not have any side effects. + val instance = scope.calcOnState { getStaticInstance(clazz) } val sort = run { val fields = clazz.fields.filter { it.name == field.name } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsFunction.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsFunction.kt index 928ffccbfa..ffa7141120 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsFunction.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsFunction.kt @@ -6,4 +6,5 @@ import org.usvm.UHeapRef class TsFunction( val method: EtsMethod, val thisInstance: UHeapRef?, + val closure: UHeapRef?, ) 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..c17dbfc5d2 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 @@ -74,6 +74,7 @@ import org.usvm.targets.UTargetsSet import org.usvm.types.TypesResult import org.usvm.types.first import org.usvm.types.single +import org.usvm.util.executableOverloadImplementation import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue @@ -313,28 +314,30 @@ class TsInterpreter( // TODO: observer - if (stmt.callee.signature.enclosingClass.name == "Log") { - mockMethodCall(scope, stmt.callee.signature) + val callee = stmt.callee.executableOverloadImplementation() + + if (callee.signature.enclosingClass.name == "Log") { + mockMethodCall(scope, callee.signature) scope.doWithState { newStmt(stmt.returnSite) } return } - val entryPoint = graph.entryPoints(stmt.callee).singleOrNull() + val entryPoint = graph.entryPoints(callee).singleOrNull() if (entryPoint == null) { - // logger.warn { "No entry point for method: ${stmt.callee}, mocking the call" } + // logger.warn { "No entry point for method: $callee, mocking the call" } // If the method doesn't have entry points, // we go through it, we just mock the call - mockMethodCall(scope, stmt.callee.signature) + mockMethodCall(scope, callee.signature) scope.doWithState { newStmt(stmt.returnSite) } return } scope.doWithState { - registerCallee(stmt.returnSite, stmt.callee.cfg) + registerCallee(stmt.returnSite, callee.cfg) val args = mutableListOf>() val numActual = stmt.args.size - val numFormal = stmt.callee.parameters.size + val numFormal = callee.parameters.size args += stmt.instance @@ -352,7 +355,7 @@ class TsInterpreter( // g() -> g(undefined, undefined) // g(1, 2, 3) -> g(1, 2) - if (stmt.callee.parameters.isNotEmpty() && stmt.callee.parameters.last().isRest) { + if (callee.parameters.isNotEmpty() && callee.parameters.last().isRest) { // vararg call // first n-1 args are normal @@ -402,8 +405,8 @@ class TsInterpreter( // TODO: re-check push sorts for arguments pushSortsForActualArguments(args) - callStack.push(stmt.callee, stmt.returnSite) - memory.stack.push(args.toTypedArray(), stmt.callee.localsCount) + callStack.push(callee, stmt.returnSite) + memory.stack.push(args.toTypedArray(), callee.localsCount) newStmt(entryPoint) } } @@ -575,6 +578,10 @@ class TsInterpreter( } } + is EtsStaticFieldRef -> { + exprResolver.handleAssignToStaticField(lhv, expr) + } + else -> { error("LHV of type ${lhv::class.java} is not supported in %dflt::%dflt: $lhv") } @@ -690,7 +697,12 @@ class TsInterpreter( } private fun visitNopStmt(scope: TsStepScope, stmt: EtsNopStmt) { - // Do nothing + val successors = graph.successors(stmt).toList() + when (successors.size) { + 0 -> scope.doWithState { returnValue(ctx.mkUndefinedValue()) } + 1 -> scope.doWithState { newStmt(successors.single()) } + else -> error("A NOP statement must not have multiple successors") + } } private fun exprResolverWithScope(scope: TsStepScope): TsExprResolver = diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt index 269a95aea2..65218fc1b0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt @@ -4,6 +4,8 @@ import mu.KotlinLogging import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME import org.usvm.UBoolSort import org.usvm.UHeapRef @@ -52,6 +54,9 @@ internal fun TsContext.ensureStaticsInitialized( clazz: EtsClass, ): Unit? = scope.calcOnState { val initializer = clazz.methods.singleOrNull { it.name == STATIC_INIT_METHOD_NAME } + ?: clazz.takeIf { it.name == DEFAULT_ARK_CLASS_NAME } + ?.methods + ?.singleOrNull { it.name == DEFAULT_ARK_METHOD_NAME } if (initializer == null) { return@calcOnState Unit } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 37034ea083..172da63294 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -65,7 +65,6 @@ class TsState( var promiseExecutor: UPersistentHashMap = persistentHashMapOf(), var methodToRef: UPersistentHashMap = persistentHashMapOf(), var associatedFunction: UPersistentHashMap = persistentHashMapOf(), - var closureObject: UPersistentHashMap = persistentHashMapOf(), var boundThis: UPersistentHashMap = persistentHashMapOf(), var dfltObject: UPersistentHashMap = persistentHashMapOf(), @@ -176,20 +175,19 @@ class TsState( fun getMethodRef( method: EtsMethod, thisInstance: UHeapRef? = null, + closure: UHeapRef? = null, ): UConcreteHeapRef { - val (updated, result) = methodToRef.getOrPut(method, ownership) { ctx.allocateConcreteRef() } - associatedFunction = associatedFunction.put(result, TsFunction(method, thisInstance), ownership) - methodToRef = updated + val result = if (closure == null) { + val (updated, methodRef) = methodToRef.getOrPut(method, ownership) { ctx.allocateConcreteRef() } + methodToRef = updated + methodRef + } else { + ctx.allocateConcreteRef() + } + associatedFunction = associatedFunction.put(result, TsFunction(method, thisInstance, closure), ownership) return result } - fun setClosureObject( - name: String, - closure: UConcreteHeapRef, - ) { - closureObject = closureObject.put(name, closure, ownership) - } - fun setBoundThis( instance: UConcreteHeapRef, thisRef: UHeapRef, @@ -292,7 +290,6 @@ class TsState( promiseExecutor = promiseExecutor, methodToRef = methodToRef, associatedFunction = associatedFunction, - closureObject = closureObject, boundThis = boundThis, dfltObject = dfltObject, dfltObjectFieldSorts = dfltObjectFieldSorts, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsNominalType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsNominalType.kt new file mode 100644 index 0000000000..22505c64b7 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsNominalType.kt @@ -0,0 +1,13 @@ +package org.usvm.machine.types + +import org.jacodb.ets.model.EtsRefType +import org.jacodb.ets.model.EtsType + +internal data class EtsNominalType(val type: EtsRefType) : EtsType { + override val typeName: String + get() = "NominalType $type" + + override fun accept(visitor: EtsType.Visitor): R { + error("Should not be called") + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index c29c149dd9..b887fd4719 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -127,6 +127,17 @@ class TsTypeSystem( return unwrappedType.types.all { isSupertype(unwrappedSupertype, it) } } + // Runtime checks such as `instanceof` use the nominal class hierarchy, + // independently of TypeScript's structural assignability rules. + if (unwrappedSupertype is EtsNominalType) { + val nominalType = when (unwrappedType) { + is EtsNominalType -> unwrappedType.type + is EtsRefType -> unwrappedType + else -> return false + } + return isNominalSupertype(unwrappedSupertype.type, nominalType) + } + // Function types if (unwrappedSupertype is EtsFunctionType && unwrappedType is EtsFunctionType) { @@ -196,17 +207,7 @@ class TsTypeSystem( if (unwrappedSupertype is EtsClassType || unwrappedSupertype is EtsUnclearRefType) { if (unwrappedType is EtsClassType || unwrappedType is EtsUnclearRefType) { - val classes = hierarchy.classesForType(unwrappedType) - val superClasses = hierarchy.classesForType(unwrappedSupertype) - - if (classes.isEmpty() || superClasses.isEmpty()) return false // TODO log - - return classes.any { cls -> - val ancestors = hierarchy.getAncestors(cls) - superClasses.any { superClass -> - superClass in ancestors - } - } + return isNominalSupertype(unwrappedSupertype, unwrappedType) } } @@ -216,6 +217,7 @@ class TsTypeSystem( override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean { val t = unwrapAlias(type) return when (t) { + is EtsNominalType -> true is EtsAuxiliaryType -> true // structural types can always be refined is EtsPrimitiveType -> types.isEmpty() // primitive has no subtypes, so only when no other constraints is EtsClassType -> true // classes can always have subclasses @@ -321,6 +323,20 @@ class TsTypeSystem( } override fun topTypeStream(): UTypeStream = topTypeStream + + private fun isNominalSupertype(supertype: EtsRefType, type: EtsRefType): Boolean { + val classes = hierarchy.classesForType(type) + val superClasses = hierarchy.classesForType(supertype) + + if (classes.isEmpty() || superClasses.isEmpty()) return false // TODO log + + return classes.any { cls -> + val ancestors = hierarchy.getAncestors(cls) + superClasses.any { superClass -> + superClass in ancestors + } + } + } } // TODO support unclear ref type diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsMethodOverloads.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsMethodOverloads.kt new file mode 100644 index 0000000000..f1e4a4d1df --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsMethodOverloads.kt @@ -0,0 +1,20 @@ +package org.usvm.util + +import org.jacodb.ets.model.EtsMethod + +internal fun EtsMethod.executableOverloadImplementation(): EtsMethod { + if (cfg.stmts.isNotEmpty()) return this + + return enclosingClass + ?.methods + ?.filter { candidate -> + candidate.name == name && + candidate.isStatic == isStatic && + candidate.cfg.stmts.isNotEmpty() + } + ?.singleOrNull() + ?: this +} + +internal fun Iterable.canonicalizeExecutableOverloads(): List = + map { it.executableOverloadImplementation() }.distinct() diff --git a/usvm-ts/src/test/kotlin/org/usvm/frontend/NativeTsFrontendDefaultTest.kt b/usvm-ts/src/test/kotlin/org/usvm/frontend/NativeTsFrontendDefaultTest.kt new file mode 100644 index 0000000000..ab306647b3 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/frontend/NativeTsFrontendDefaultTest.kt @@ -0,0 +1,20 @@ +package org.usvm.frontend + +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.util.getResourcePath +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +class NativeTsFrontendDefaultTest { + @Test + fun `loads TypeScript without an external frontend`() { + val file = loadEtsFileAutoConvert( + getResourcePath("/samples/lang/Numeric.ts"), + useArkAnalyzerTypeInference = null, + ) + + val numericClass = assertNotNull(file.classes.singleOrNull { it.name == "Numeric" }) + assertTrue(numericClass.methods.any { it.name == "numberToNumber" }) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextTest.kt new file mode 100644 index 0000000000..35e523467f --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextTest.kt @@ -0,0 +1,20 @@ +package org.usvm.machine + +import io.mockk.mockk +import org.jacodb.ets.model.EtsBooleanLiteralType +import org.jacodb.ets.model.EtsNumberLiteralType +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStringLiteralType +import org.junit.jupiter.api.Test +import kotlin.test.assertSame + +class TsContextTest { + @Test + fun `literal types use their base type sorts`() { + TsContext(EtsScene(emptyList()), mockk()).use { context -> + assertSame(context.boolSort, context.typeToSort(EtsBooleanLiteralType(true))) + assertSame(context.fp64Sort, context.typeToSort(EtsNumberLiteralType(1.0))) + assertSame(context.addressSort, context.typeToSort(EtsStringLiteralType("value"))) + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt new file mode 100644 index 0000000000..2e699edffc --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt @@ -0,0 +1,37 @@ +package org.usvm.machine.types + +import org.jacodb.ets.model.EtsClassImpl +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFieldImpl +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.usvm.util.EtsHierarchy +import org.usvm.util.type +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class TsTypeSystemTest { + @Test + fun `auxiliary type is a subtype of a class containing its properties`() { + val fileSignature = EtsFileSignature(projectName = "test", fileName = "types.ts") + val classSignature = EtsClassSignature(name = "WithTwoFields", file = fileSignature) + val clazz = EtsClassImpl( + signature = classSignature, + fields = listOf( + EtsFieldImpl(EtsFieldSignature(classSignature, "a", EtsNumberType)), + EtsFieldImpl(EtsFieldSignature(classSignature, "b", EtsNumberType)), + ), + methods = emptyList(), + ) + val file = EtsFile(fileSignature, classes = listOf(clazz), namespaces = emptyList()) + val scene = EtsScene(projectFiles = listOf(file)) + val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, EtsHierarchy(scene)) + val auxiliaryType = EtsAuxiliaryType(properties = setOf("a")) + + assertTrue(typeSystem.isSupertype(clazz.type, auxiliaryType)) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Numeric.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Numeric.kt index 4c4477653b..ef7c5ae761 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Numeric.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Numeric.kt @@ -13,6 +13,24 @@ class Numeric : TsMethodTestRunner() { override val scene: EtsScene = loadScene(tsPath) + @Test + fun `test Number without arguments`() { + val method = getMethod("emptyNumber") + discoverProperties( + method = method, + { r -> r eq 0 }, + ) + } + + @Test + fun `test custom Number is not handled as built-in converter`() { + val method = getMethod("customNumber") + discoverProperties( + method = method, + { r -> r eq 42 }, + ) + } + @Test fun `test numberToNumber`() { val method = getMethod("numberToNumber") diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StaticOverloads.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StaticOverloads.kt new file mode 100644 index 0000000000..3255d41d5f --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StaticOverloads.kt @@ -0,0 +1,44 @@ +package org.usvm.samples.lang + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.usvm.api.TsTestValue +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsState +import org.usvm.statistics.UMachineObserver +import org.usvm.test.util.checkers.eq as exactly +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.eq +import kotlin.test.assertEquals + +class StaticOverloads : TsMethodTestRunner() { + override val scene: EtsScene = loadScene("/samples/lang/StaticOverloads.ts") + + @Test + fun `test static overload group executes once`() { + val method = getMethod("callOverloaded") + checkMatches( + method = method, + analysisResultNumberMatches = exactly(1), + { result -> result eq 42 }, + ) + } + + @Test + fun `test static overload group does not fork equivalent states`() { + var forkedStates = 0 + val observer = object : UMachineObserver { + override fun onState(parent: TsState, forks: Sequence) { + forkedStates += forks.count() + } + } + val method = getMethod("callOverloaded") + + TsMachine(scene, options, TsOptions(), machineObserver = observer).use { machine -> + machine.analyze(listOf(method)) + } + + assertEquals(0, forkedStates) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt index 9fb0f6a59f..f9394d0e7f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt @@ -15,6 +15,26 @@ class Add : TsMethodTestRunner() { override val scene: EtsScene = loadScene(tsPath) + @Test + fun `string + number constants`() { + val method = getMethod("addStringAndNumberConstants") + discoverProperties( + method = method, + { r -> r.value == "timeout:5000ms" }, + ) + } + + @Test + fun `string + fractional number constant`() { + val method = getMethod("addStringAndFractionalNumberConstant") + val expected = "values:1.5,1e-7,0.000001," + + "100000000000000000000,1e+21,5e-324" + discoverProperties( + method = method, + { r -> r.value == expected }, + ) + } + @Test fun `bool + bool`() { val method = getMethod("addBoolAndBool") diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Increment.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Increment.kt new file mode 100644 index 0000000000..5568756c5d --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Increment.kt @@ -0,0 +1,43 @@ +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 + +class Increment : TsMethodTestRunner() { + override val scene: EtsScene = loadScene("/samples/operators/Increment.ts") + + @Test + fun `pre increment returns and stores the incremented value`() { + discoverProperties( + method = getMethod("preIncrement"), + { result -> result eq 22 }, + ) + } + + @Test + fun `post increment returns the old value and stores the incremented value`() { + discoverProperties( + method = getMethod("postIncrement"), + { result -> result eq 12 }, + ) + } + + @Test + fun `pre decrement returns and stores the decremented value`() { + discoverProperties( + method = getMethod("preDecrement"), + { result -> result eq 0 }, + ) + } + + @Test + fun `post decrement returns the old value and stores the decremented value`() { + discoverProperties( + method = getMethod("postDecrement"), + { result -> result eq 10 }, + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/lang/Numeric.ts b/usvm-ts/src/test/resources/samples/lang/Numeric.ts index 0d252487e7..1eb2ca4602 100644 --- a/usvm-ts/src/test/resources/samples/lang/Numeric.ts +++ b/usvm-ts/src/test/resources/samples/lang/Numeric.ts @@ -2,6 +2,15 @@ // noinspection JSUnusedGlobalSymbols class Numeric { + emptyNumber(): number { + return Number(); + } + + customNumber(): number { + const Number = (value: number): number => value + 10; + return Number(32); + } + numberToNumber(x: number): number { if (x != x) return Number(x); // NaN if (x == 0) return Number(x); // 0 diff --git a/usvm-ts/src/test/resources/samples/lang/StaticOverloads.ts b/usvm-ts/src/test/resources/samples/lang/StaticOverloads.ts new file mode 100644 index 0000000000..8cec979a1d --- /dev/null +++ b/usvm-ts/src/test/resources/samples/lang/StaticOverloads.ts @@ -0,0 +1,14 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +function overloaded(value: number): number; +function overloaded(value: string): string; +function overloaded(value: number | string): number | string { + return typeof value === "number" ? value + 1 : value; +} + +class StaticOverloads { + callOverloaded(): number { + return overloaded(41); + } +} diff --git a/usvm-ts/src/test/resources/samples/operators/Add.ts b/usvm-ts/src/test/resources/samples/operators/Add.ts index b438e648cf..4aeed953f9 100644 --- a/usvm-ts/src/test/resources/samples/operators/Add.ts +++ b/usvm-ts/src/test/resources/samples/operators/Add.ts @@ -2,6 +2,15 @@ // noinspection JSUnusedGlobalSymbols class Add { + addStringAndNumberConstants(): string { + return "timeout:" + 5000 + "ms"; + } + + addStringAndFractionalNumberConstant(): string { + return "values:" + 1.5 + "," + 1e-7 + "," + 1e-6 + "," + + 1e20 + "," + 1e21 + "," + 5e-324; + } + addBoolAndBool(a: boolean, b: boolean): number { let res = a + b; diff --git a/usvm-ts/src/test/resources/samples/operators/Increment.ts b/usvm-ts/src/test/resources/samples/operators/Increment.ts new file mode 100644 index 0000000000..433b45ebb6 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/operators/Increment.ts @@ -0,0 +1,28 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class Increment { + preIncrement(): number { + let value = 1; + const result = ++value; + return result * 10 + value; + } + + postIncrement(): number { + let value = 1; + const result = value++; + return result * 10 + value; + } + + preDecrement(): number { + let value = 1; + const result = --value; + return result * 10 + value; + } + + postDecrement(): number { + let value = 1; + const result = value--; + return result * 10 + value; + } +}