diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/EtsTypeFact.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/EtsTypeFact.kt index 2951f9905a..897d0c21ec 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/EtsTypeFact.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/EtsTypeFact.kt @@ -209,59 +209,102 @@ sealed interface EtsTypeFact { ) : EtsTypeFact companion object { - internal val allStringProperties = listOf( - "length", - "constructor", - "anchor", - "at", - "big", - "blink", - "bold", - "charAt", - "charCodeAt", - "codePointAt", - "concat", - "endsWith", - "fontcolor", - "fontsize", - "fixed", - "includes", - "indexOf", - "isWellFormed", - "italics", - "lastIndexOf", - "link", - "localeCompare", - "match", - "matchAll", - "normalize", - "padEnd", - "padStart", - "repeat", - "replace", - "replaceAll", - "search", - "slice", - "small", - "split", - "strike", - "sub", - "substr", - "substring", - "sup", - "startsWith", - "toString", - "toWellFormed", - "trim", - "trimStart", - "trimLeft", - "trimEnd", - "trimRight", - "toLocaleLowerCase", - "toLocaleUpperCase", - "toLowerCase", - "toUpperCase", - "valueOf", + internal val allStringProperties = mapOf( + "length" to NumberEtsTypeFact, + "constructor" to FunctionEtsTypeFact, + "anchor" to FunctionEtsTypeFact, + "at" to FunctionEtsTypeFact, + "big" to FunctionEtsTypeFact, + "blink" to FunctionEtsTypeFact, + "bold" to FunctionEtsTypeFact, + "charAt" to FunctionEtsTypeFact, + "charCodeAt" to FunctionEtsTypeFact, + "codePointAt" to FunctionEtsTypeFact, + "concat" to FunctionEtsTypeFact, + "endsWith" to FunctionEtsTypeFact, + "fixed" to FunctionEtsTypeFact, + "fontcolor" to FunctionEtsTypeFact, + "fontsize" to FunctionEtsTypeFact, + "includes" to FunctionEtsTypeFact, + "indexOf" to FunctionEtsTypeFact, + "isWellFormed" to FunctionEtsTypeFact, + "italics" to FunctionEtsTypeFact, + "lastIndexOf" to FunctionEtsTypeFact, + "link" to FunctionEtsTypeFact, + "localeCompare" to FunctionEtsTypeFact, + "match" to FunctionEtsTypeFact, + "matchAll" to FunctionEtsTypeFact, + "normalize" to FunctionEtsTypeFact, + "padEnd" to FunctionEtsTypeFact, + "padStart" to FunctionEtsTypeFact, + "repeat" to FunctionEtsTypeFact, + "replace" to FunctionEtsTypeFact, + "replaceAll" to FunctionEtsTypeFact, + "search" to FunctionEtsTypeFact, + "slice" to FunctionEtsTypeFact, + "small" to FunctionEtsTypeFact, + "split" to FunctionEtsTypeFact, + "strike" to FunctionEtsTypeFact, + "sub" to FunctionEtsTypeFact, + "substr" to FunctionEtsTypeFact, + "substring" to FunctionEtsTypeFact, + "sup" to FunctionEtsTypeFact, + "startsWith" to FunctionEtsTypeFact, + "toString" to FunctionEtsTypeFact, + "toWellFormed" to FunctionEtsTypeFact, + "trim" to FunctionEtsTypeFact, + "trimStart" to FunctionEtsTypeFact, + "trimLeft" to FunctionEtsTypeFact, + "trimEnd" to FunctionEtsTypeFact, + "trimRight" to FunctionEtsTypeFact, + "toLocaleLowerCase" to FunctionEtsTypeFact, + "toLocaleUpperCase" to FunctionEtsTypeFact, + "toLowerCase" to FunctionEtsTypeFact, + "toUpperCase" to FunctionEtsTypeFact, + "valueOf" to FunctionEtsTypeFact, + ) + + internal val allArrayProperties = mapOf( + "constructor" to FunctionEtsTypeFact, + "length" to NumberEtsTypeFact, + "at" to FunctionEtsTypeFact, + "concat" to FunctionEtsTypeFact, + "copyWithin" to FunctionEtsTypeFact, + "entries" to FunctionEtsTypeFact, + "every" to FunctionEtsTypeFact, + "fill" to FunctionEtsTypeFact, + "filter" to FunctionEtsTypeFact, + "find" to FunctionEtsTypeFact, + "findIndex" to FunctionEtsTypeFact, + "findLast" to FunctionEtsTypeFact, + "findLastIndex" to FunctionEtsTypeFact, + "flat" to FunctionEtsTypeFact, + "flatMap" to FunctionEtsTypeFact, + "forEach" to FunctionEtsTypeFact, + "includes" to FunctionEtsTypeFact, + "indexOf" to FunctionEtsTypeFact, + "join" to FunctionEtsTypeFact, + "keys" to FunctionEtsTypeFact, + "lastIndexOf" to FunctionEtsTypeFact, + "map" to FunctionEtsTypeFact, + "pop" to FunctionEtsTypeFact, + "push" to FunctionEtsTypeFact, + "reduce" to FunctionEtsTypeFact, + "reduceRight" to FunctionEtsTypeFact, + "reverse" to FunctionEtsTypeFact, + "shift" to FunctionEtsTypeFact, + "slice" to FunctionEtsTypeFact, + "some" to FunctionEtsTypeFact, + "sort" to FunctionEtsTypeFact, + "splice" to FunctionEtsTypeFact, + "toLocaleString" to FunctionEtsTypeFact, + "toReversed" to FunctionEtsTypeFact, + "toSorted" to FunctionEtsTypeFact, + "toSpliced" to FunctionEtsTypeFact, + "toString" to FunctionEtsTypeFact, + "unshift" to FunctionEtsTypeFact, + "values" to FunctionEtsTypeFact, + "with" to FunctionEtsTypeFact, ) fun mkUnionType(vararg types: EtsTypeFact): EtsTypeFact = mkUnionType(types.toHashSet()) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeFactProcessor.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeFactProcessor.kt index 12af9a763b..ddbd041b98 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeFactProcessor.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeFactProcessor.kt @@ -24,6 +24,8 @@ import org.jacodb.ets.model.EtsType import org.usvm.dataflow.ts.infer.EtsTypeFact.AnyEtsTypeFact import org.usvm.dataflow.ts.infer.EtsTypeFact.ArrayEtsTypeFact import org.usvm.dataflow.ts.infer.EtsTypeFact.BooleanEtsTypeFact +import org.usvm.dataflow.ts.infer.EtsTypeFact.Companion.allArrayProperties +import org.usvm.dataflow.ts.infer.EtsTypeFact.Companion.allStringProperties import org.usvm.dataflow.ts.infer.EtsTypeFact.Companion.mkIntersectionType import org.usvm.dataflow.ts.infer.EtsTypeFact.Companion.mkUnionType import org.usvm.dataflow.ts.infer.EtsTypeFact.FunctionEtsTypeFact @@ -76,7 +78,16 @@ class TypeFactProcessor( is AnyEtsTypeFact -> type - is StringEtsTypeFact, + is StringEtsTypeFact -> { + when (other) { + is ObjectEtsTypeFact -> intersect(other, type) + is UnionEtsTypeFact -> intersect(other, type) + is IntersectionEtsTypeFact -> intersect(other, type) + is GuardedTypeFact -> intersect(other, type) + else -> null + } + } + is NumberEtsTypeFact, is BooleanEtsTypeFact, is NullEtsTypeFact, @@ -113,12 +124,15 @@ class TypeFactProcessor( } } + is ObjectEtsTypeFact -> intersect(other, type) + else -> null } is ObjectEtsTypeFact -> when (other) { is ObjectEtsTypeFact -> intersect(type, other) is StringEtsTypeFact -> intersect(type, other) + is ArrayEtsTypeFact -> intersect(type, other) is FunctionEtsTypeFact -> mkIntersectionType(type, other) is UnionEtsTypeFact -> intersect(other, type) is IntersectionEtsTypeFact -> intersect(other, type) @@ -192,16 +206,43 @@ class TypeFactProcessor( if (obj.cls == EtsStringType) return string if (obj.cls != null) return null + // Check intersection is string + val intersectionIsString = obj.properties.all { (name, type) -> + val stringPropertyType = allStringProperties[name] ?: return@all false + intersect(stringPropertyType, type) == stringPropertyType + } + if (intersectionIsString) { + return StringEtsTypeFact + } + val intersectionProperties = obj.properties - .filter { it.key in EtsTypeFact.allStringProperties } - .mapValues { (_, type) -> - // TODO: intersect with the corresponding type of String's property - type + .mapValues { (name, type) -> + val stringPropertyType = allStringProperties[name] ?: return@mapValues type + intersect(stringPropertyType, type) ?: return null } return ObjectEtsTypeFact(null, intersectionProperties) } + private fun intersect(obj: ObjectEtsTypeFact, array: ArrayEtsTypeFact): EtsTypeFact? { + // Check intersection is array + val intersectionIsArray = obj.properties.all { (name, type) -> + val arrayPropertyType = allArrayProperties[name] ?: return@all false + intersect(arrayPropertyType, type) == arrayPropertyType + } + if (intersectionIsArray) { + return array + } + + val intersectionProperties = obj.properties + .mapValues { (name, type) -> + val arrayPropertyType = allArrayProperties[name] ?: return@mapValues type + intersect(arrayPropertyType, type) ?: return null + } + + return ObjectEtsTypeFact(obj.cls, intersectionProperties) + } + private fun union(unionType: UnionEtsTypeFact, other: EtsTypeFact): EtsTypeFact { val result = hashSetOf() for (type in unionType.types) { @@ -261,7 +302,7 @@ class TypeFactProcessor( if (obj.cls != null) return mkUnionType(obj, string) for (p in obj.properties.keys) { - if (p !in EtsTypeFact.allStringProperties) { + if (p !in allStringProperties) { return mkUnionType(obj, string) } } diff --git a/usvm-ts-dataflow/src/test/resources/ts/testcases.ts b/usvm-ts-dataflow/src/test/resources/ts/testcases.ts index 1731296432..9927bf0c74 100644 --- a/usvm-ts-dataflow/src/test/resources/ts/testcases.ts +++ b/usvm-ts-dataflow/src/test/resources/ts/testcases.ts @@ -215,6 +215,36 @@ class CaseAssignLocalToArrayElementNumber { // ---------------------------------------- +// Case `y := x.length, x: any[]` +class CaseAssignLocalToArrayLength { + entrypoint(x: any[]) { + let y = x.length; // y: number + x[0] = y; // x: Array + this.infer(x); + } + + infer(a: any) { + const EXPECTED_ARG_0 = "Array"; + } +} + +// ---------------------------------------- + +// Case `y := x.length, x: string` +class CaseAssignLocalToStringLength { + entrypoint(x: any) { + x = "abacaba"; // x: string + let y = x.length; // y: number + this.infer(x); + } + + infer(a: any) { + const EXPECTED_ARG_0 = "string"; + } +} + +// ---------------------------------------- + interface ICustom { a: number; b: string;