From f8ffa8cb23df6b09c7dc6668174558dd773abe2a Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 26 Feb 2025 21:09:23 +0300
Subject: [PATCH] Intercept array length for arrays inside fake objects

---
 .../org/usvm/machine/expr/TsExprResolver.kt   | 28 +++++++++++++++----
 .../usvm/machine/interpreter/TsInterpreter.kt |  4 ++-
 .../kotlin/org/usvm/samples/FieldAccess.kt    |  1 -
 3 files changed, 26 insertions(+), 7 deletions(-)

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 56657ecea..b25dc732e 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
@@ -42,6 +42,7 @@ import org.jacodb.ets.base.EtsNotExpr
 import org.jacodb.ets.base.EtsNullConstant
 import org.jacodb.ets.base.EtsNullishCoalescingExpr
 import org.jacodb.ets.base.EtsNumberConstant
+import org.jacodb.ets.base.EtsNumberType
 import org.jacodb.ets.base.EtsOrExpr
 import org.jacodb.ets.base.EtsParameterRef
 import org.jacodb.ets.base.EtsPostDecExpr
@@ -66,6 +67,7 @@ import org.jacodb.ets.base.EtsUnaryExpr
 import org.jacodb.ets.base.EtsUnaryPlusExpr
 import org.jacodb.ets.base.EtsUnclearRefType
 import org.jacodb.ets.base.EtsUndefinedConstant
+import org.jacodb.ets.base.EtsUnknownType
 import org.jacodb.ets.base.EtsUnsignedRightShiftExpr
 import org.jacodb.ets.base.EtsValue
 import org.jacodb.ets.base.EtsVoidExpr
@@ -644,12 +646,28 @@ class TsExprResolver(
 
         // TODO It is a hack for array's length
         if (value.instance.type is EtsArrayType && value.field.name == "length") {
-            val lValue = mkArrayLengthLValue(instanceRef, value.instance.type as EtsArrayType)
-            val expr = scope.calcOnState { memory.read(lValue) }
-
-            check(expr.sort == ctx.sizeSort)
+            val lengthLValue = mkArrayLengthLValue(instanceRef, value.instance.type as EtsArrayType)
+            val length = scope.calcOnState { memory.read(lengthLValue) }
+            return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), length.asExpr(sizeSort), signed = true)
+        }
 
-            return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), expr.asExpr(sizeSort), signed = true)
+        // TODO: handle "length" property for arrays inside fake objects
+        if (value.field.name == "length" && instanceRef.isFakeObject()) {
+            val fakeType = scope.calcOnState {
+                memory.types.getTypeStream(instanceRef).single() as FakeType
+            }
+            if (fakeType.refTypeExpr.isTrue) {
+                val refLValue = getIntermediateRefLValue(instanceRef.address)
+                val obj = scope.calcOnState { memory.read(refLValue) }
+                // TODO: fix array type. It should be the same as the type used when "writing" the length.
+                //  However, current value.instance typically has 'unknown' type, and the best we can do here is
+                //  to pretend that this is an array-like object (with "array length", not just "length" field),
+                //  and "cast" instance to "unknown[]". The same could be done for any length writes, making
+                //  the array type (for length) consistent (unknown everywhere), but less precise.
+                val lengthLValue = mkArrayLengthLValue(obj, EtsArrayType(EtsUnknownType, 1))
+                val length = scope.calcOnState { memory.read(lengthLValue) }
+                return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), length.asExpr(sizeSort), signed = true)
+            }
         }
 
         val field = resolveInstanceField(value.instance, value.field)
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 c1dacd8c1..5abd99d04 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
@@ -156,8 +156,10 @@ class TsInterpreter(
                         isSigned = true
                     ).asExpr(sizeSort)
 
+                    // TODO: handle the case when `lhv.array.type` is NOT an array.
+                    //  In this case, it could be created manually: `EtsArrayType(EtsUnknownType, 1)`.
                     val lengthLValue = mkArrayLengthLValue(instance, lhv.array.type as EtsArrayType)
-                    val currentLength = memory.read(lengthLValue).asExpr(sizeSort)
+                    val currentLength = memory.read(lengthLValue)
 
                     val condition = mkBvSignedGreaterOrEqualExpr(bvIndex, currentLength)
                     val newLength = mkIte(condition, mkBvAddExpr(bvIndex, mkBv(1)), currentLength)
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt
index 87e11310a..124022170 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt
@@ -113,7 +113,6 @@ class FieldAccess : TsMethodTestRunner() {
         )
     }
 
-    @Disabled("Need to handle .length property specifically")
     @Test
     fun `test circularTypeChanges`() {
         val method = getMethod(className, "circularTypeChanges")