Intercept array length for arrays inside fake objects

UnitTestBot · Feb 26, 2025 · f8ffa8c · f8ffa8c
1 parent 34a1d18
commit f8ffa8c
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 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
@@ -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
@@ -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
@@ -113,7 +113,6 @@ class FieldAccess : TsMethodTestRunner() {
         )
     }
 
-    @Disabled("Need to handle .length property specifically")
     @Test
     fun `test circularTypeChanges`() {
         val method = getMethod(className, "circularTypeChanges")
-Original file line number
+Diff line change
@@ Expand Up / @@ -113,7 +113,6 @@ class FieldAccess : TsMethodTestRunner() { @@
             )
         }
-        @Disabled("Need to handle .length property specifically")
         @Test
         fun `test circularTypeChanges`() {
             val method = getMethod(className, "circularTypeChanges")
@@ Expand Down @@