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 index 0476738c48..582f0b0146 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt @@ -10,6 +10,8 @@ import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsValue import org.usvm.UConcreteHeapRef @@ -44,10 +46,14 @@ private fun EtsFunctionType.isBuiltinNumberType(): Boolean { private fun EtsFunctionType.isBuiltinArrayType(): Boolean { val parameter = signature.parameters.singleOrNull() ?: return false val arrayType = signature.returnType as? EtsArrayType ?: return false + val lengthTypes = (parameter.type as? EtsUnionType)?.types?.toSet() + val acceptsNumericLength = parameter.type == EtsNumberType || + lengthTypes == setOf(EtsNumberType, EtsUndefinedType) + return signature.enclosingClass == EtsClassSignature.UNKNOWN && signature.name.isEmpty() && arrayType.elementType == EtsAnyType && arrayType.dimensions == 1 && - parameter.type == EtsNumberType && parameter.isOptional && !parameter.isRest + acceptsNumericLength && parameter.isOptional && !parameter.isRest } private fun EtsValue.isLegacyBuiltinGlobal( diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/StrictCollectionOperationsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/StrictCollectionOperationsTest.kt new file mode 100644 index 0000000000..3f25baf0a3 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/StrictCollectionOperationsTest.kt @@ -0,0 +1,66 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.Test + +class StrictCollectionOperationsTest : TsMethodTestRunner() { + override val scene = loadEtsProjectAutoConvert( + getResourcePath("/models/strict-collections"), + useArkAnalyzerTypeInference = null, + ) + override val tsOptions = TsOptions(eraseTypeAssertions = true) + + override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + @TempDir + lateinit var directory: Path + + init { + options = options.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + } + + @Test + fun `Array from accepts the native strict null checks constructor signature`() { + discoverProperties( + method = getMethod(methodName = "nativeFromKeys", className = "StrictCollections"), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } + + @Test + fun `Node confirms strict project collection behavior`() { + val source = getResourcePath("/models/strict-collections/StrictCollections.ts").readText() + + assertNodeReplay( + source = source + "if (StrictCollections.nativeFromKeys() !== 1) throw Error('strict from');", + directory = directory, + name = "native-strict-collection-operations", + timeoutMessage = "Native strict collection regression timed out", + ) + } +} diff --git a/usvm-ts/src/test/resources/models/strict-collections/StrictCollections.ts b/usvm-ts/src/test/resources/models/strict-collections/StrictCollections.ts new file mode 100644 index 0000000000..974125acdd --- /dev/null +++ b/usvm-ts/src/test/resources/models/strict-collections/StrictCollections.ts @@ -0,0 +1,8 @@ +export class StrictCollections { + static nativeFromKeys(): number { + const map = new Map(); + map.set('a', 3).set('b', 5); + const keys = Array.from(map.keys()); + return keys.length === 2 && keys[0] === 'a' && keys[1] === 'b' ? 1 : 0; + } +} diff --git a/usvm-ts/src/test/resources/models/strict-collections/tsconfig.json b/usvm-ts/src/test/resources/models/strict-collections/tsconfig.json new file mode 100644 index 0000000000..7c136e1dde --- /dev/null +++ b/usvm-ts/src/test/resources/models/strict-collections/tsconfig.json @@ -0,0 +1,8 @@ +{ + "compilerOptions": { + "target": "ES2021", + "module": "commonjs", + "strictNullChecks": true + }, + "files": ["StrictCollections.ts"] +}