Add special objects handlers to type processor (#279)

---------

Co-authored-by: Alexey Menshutin <alex.menshutin99@gmail.com>

Author: MForest7

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())

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<EtsTypeFact>()
         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)
             }
         }

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<any>
+        this.infer(x);
+    }
+
+    infer(a: any) {
+        const EXPECTED_ARG_0 = "Array<any>";
+    }
+}
+
+// ----------------------------------------
+
+// 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;