[TS] Add checks to forbid fake objects (#335)

Author: Lipen

usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt

@@ -344,6 +344,8 @@ private fun TsExprResolver.handleArrayPop(
         "Array.pop() should have no arguments, but got ${expr.args.size}"
     }
 
+    checkNotFake(array)
+
     scope.calcOnState {
         // Read the length of the array
         val lengthLValue = mkArrayLengthLValue(array, arrayType)

usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt

@@ -20,6 +20,12 @@ import org.usvm.machine.types.ExprWithTypeConstraint
 import org.usvm.types.single
 import org.usvm.util.boolToFp
 
+fun TsContext.checkNotFake(expr: UExpr<*>) {
+    require(!expr.isFakeObject()) {
+        "Fake object handling should be done outside of this function"
+    }
+}
+
 fun TsContext.mkTruthyExpr(
     expr: UExpr<out USort>,
     scope: TsStepScope,

usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt

@@ -68,6 +68,8 @@ fun TsContext.readArray(
     index: UExpr<TsSizeSort>,
     arrayType: EtsArrayType,
 ): UExpr<*>? {
+    checkNotFake(array)
+
     // Read the array length.
     val length = scope.calcOnState {
         val lengthLValue = mkArrayLengthLValue(array, arrayType)

usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt

@@ -63,9 +63,7 @@ fun TsContext.readField(
     field: EtsFieldSignature,
     hierarchy: EtsHierarchy,
 ): UExpr<*> {
-    require(!instance.isFakeObject()) {
-        "Fake object handling should be done outside of this function"
-    }
+    checkNotFake(instance)
 
     val sort = when (val etsField = resolveEtsField(instanceLocal, field, hierarchy)) {
         is TsResolutionResult.Empty -> {

usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt

@@ -42,6 +42,8 @@ fun TsContext.readArrayLength(
     array: UHeapRef,
     arrayType: EtsArrayType,
 ): UExpr<KFp64Sort> {
+    checkNotFake(array)
+
     // Read the length of the array.
     val length = scope.calcOnState {
         val lengthLValue = mkArrayLengthLValue(array, arrayType)

usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt

@@ -66,6 +66,8 @@ fun TsContext.assignToArrayIndex(
     expr: UExpr<*>,
     arrayType: EtsArrayType,
 ): Unit? {
+    checkNotFake(array)
+
     // Read the array length.
     val length = scope.calcOnState {
         val lengthLValue = mkArrayLengthLValue(array, arrayType)