diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt
new file mode 100644
index 0000000000..152faf7ad7
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt
@@ -0,0 +1,91 @@
+package org.usvm.machine.expr
+
+import io.ksmt.utils.asExpr
+import mu.KotlinLogging
+import org.jacodb.ets.model.EtsInstanceCallExpr
+import org.jacodb.ets.model.EtsMethodSignature
+import org.usvm.UExpr
+import org.usvm.machine.TsContext
+import org.usvm.machine.TsVirtualMethodCallStmt
+import org.usvm.machine.expr.TsExprApproximationResult.NoApproximation
+import org.usvm.machine.expr.TsExprApproximationResult.ResolveFailure
+import org.usvm.machine.expr.TsExprApproximationResult.SuccessfulApproximation
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.state.TsMethodResult
+import org.usvm.machine.state.lastStmt
+import org.usvm.machine.state.newStmt
+
+private val logger = KotlinLogging.logger {}
+
+internal fun TsExprResolver.handleInstanceCall(
+    expr: EtsInstanceCallExpr,
+): UExpr<*>? = with(ctx) {
+    // Check if the method was already called and returned a value.
+    when (val result = scope.calcOnState { methodResult }) {
+        is TsMethodResult.Success -> {
+            scope.doWithState { methodResult = TsMethodResult.NoCall }
+            return result.value
+        }
+
+        is TsMethodResult.TsException -> {
+            error("Exception should be handled earlier")
+        }
+
+        is TsMethodResult.NoCall -> {} // proceed to call
+    }
+
+    // Try to approximate the call.
+    when (val result = tryApproximateInstanceCall(expr)) {
+        is SuccessfulApproximation -> return result.expr
+        is ResolveFailure -> return null
+        is NoApproximation -> {}
+    }
+
+    // Resolve the instance.
+    val instance = run {
+        val resolved = resolve(expr.instance) ?: return null
+        if (resolved.isFakeObject()) {
+            val fakeType = resolved.getFakeType(scope)
+            scope.assert(fakeType.refTypeExpr) ?: run {
+                logger.warn { "Calls on non-ref (fake) instance is not supported: $expr" }
+                return null
+            }
+            resolved.extractRef(scope)
+        } else {
+            if (resolved.sort != addressSort) {
+                logger.warn { "Calling method on non-ref instance is not yet supported: $expr" }
+                scope.assert(falseExpr)
+                return null
+            }
+            resolved.asExpr(addressSort)
+        }
+    }
+
+    // Check for undefined or null property access.
+    checkUndefinedOrNullPropertyRead(scope, instance, expr.callee.name) ?: return null
+
+    // Resolve arguments.
+    val args = expr.args.map { resolve(it) ?: return null }
+
+    // Call.
+    callInstanceMethod(scope, expr.callee, instance, args)
+}
+
+fun TsContext.callInstanceMethod(
+    scope: TsStepScope,
+    callee: EtsMethodSignature,
+    instance: UExpr<*>,
+    args: List<UExpr<*>>,
+): UExpr<*>? {
+    // Create the virtual call statement.
+    val virtualCall = TsVirtualMethodCallStmt(
+        callee = callee,
+        instance = instance,
+        args = args,
+        returnSite = scope.calcOnState { lastStmt },
+    )
+    scope.doWithState { newStmt(virtualCall) }
+
+    // Return null to indicate that we are waiting for the call to be executed.
+    return null
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt
index f85a10ff73..428267ef50 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt
@@ -31,20 +31,7 @@ import org.usvm.util.resolveEtsMethods
 
 private val logger = KotlinLogging.logger {}
 
-sealed interface TsExprApproximationResult {
-    data class SuccessfulApproximation(val expr: UExpr<*>) : TsExprApproximationResult
-    data object ResolveFailure : TsExprApproximationResult
-    data object NoApproximation : TsExprApproximationResult
-
-    companion object {
-        fun from(expr: UExpr<*>?): TsExprApproximationResult = when {
-            expr != null -> SuccessfulApproximation(expr)
-            else -> ResolveFailure
-        }
-    }
-}
-
-fun TsExprResolver.tryApproximateInstanceCall(
+internal fun TsExprResolver.tryApproximateInstanceCall(
     expr: EtsInstanceCallExpr,
 ): TsExprApproximationResult = with(ctx) {
     // Mock all calls to `Logger` methods
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt
new file mode 100644
index 0000000000..f7ca10ca7e
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt
@@ -0,0 +1,131 @@
+package org.usvm.machine.expr
+
+import mu.KotlinLogging
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.model.EtsStaticCallExpr
+import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME
+import org.usvm.UExpr
+import org.usvm.machine.Constants
+import org.usvm.machine.TsConcreteMethodCallStmt
+import org.usvm.machine.expr.TsExprApproximationResult.NoApproximation
+import org.usvm.machine.expr.TsExprApproximationResult.ResolveFailure
+import org.usvm.machine.expr.TsExprApproximationResult.SuccessfulApproximation
+import org.usvm.machine.state.TsMethodResult
+import org.usvm.machine.state.lastStmt
+import org.usvm.machine.state.newStmt
+import org.usvm.util.TsResolutionResult
+
+private val logger = KotlinLogging.logger {}
+
+internal fun TsExprResolver.handleStaticCall(
+    expr: EtsStaticCallExpr,
+): UExpr<*>? = with(ctx) {
+    // Check if the method was already called and returned a value.
+    when (val result = scope.calcOnState { methodResult }) {
+        is TsMethodResult.Success -> {
+            scope.doWithState { methodResult = TsMethodResult.NoCall }
+            return result.value
+        }
+
+        is TsMethodResult.TsException -> {
+            error("Exception should be handled earlier")
+        }
+
+        is TsMethodResult.NoCall -> {} // proceed to call
+    }
+
+    // Try to approximate the call.
+    when (val result = tryApproximateStaticCall(expr)) {
+        is SuccessfulApproximation -> return result.expr
+        is ResolveFailure -> return null
+        is NoApproximation -> {}
+    }
+
+    // Resolve the static method.
+    when (val resolved = resolveStaticMethod(expr.callee)) {
+        is TsResolutionResult.Empty -> {
+            logger.error { "Could not resolve static call: ${expr.callee}" }
+            scope.assert(falseExpr) ?: return null
+        }
+
+        is TsResolutionResult.Ambiguous -> {
+            processAmbiguousStaticMethod(resolved, expr)
+        }
+
+        is TsResolutionResult.Unique -> {
+            processUniqueStaticMethod(resolved, expr)
+        }
+    }
+
+    // Return null to indicate that we are awaiting the call to be executed.
+    null
+}
+
+private fun TsExprResolver.resolveStaticMethod(
+    method: EtsMethodSignature,
+): TsResolutionResult<EtsMethod> {
+    // Perfect signature:
+    if (method.enclosingClass.name != UNKNOWN_CLASS_NAME) {
+        val classes = hierarchy.classesForType(EtsClassType(method.enclosingClass))
+        if (classes.size > 1) {
+            val methods = classes.map { it.methods.single { it.name == method.name } }
+            return TsResolutionResult.create(methods)
+        }
+
+        if (classes.isEmpty()) return TsResolutionResult.Empty
+
+        val clazz = classes.single()
+        val methods = clazz.methods.filter { it.name == method.name }
+        return TsResolutionResult.create(methods)
+    }
+
+    // Unknown signature:
+    val methods = ctx.scene.projectAndSdkClasses
+        .flatMap { it.methods }
+        .filter { it.name == method.name }
+
+    return TsResolutionResult.create(methods)
+}
+
+private fun TsExprResolver.processAmbiguousStaticMethod(
+    resolved: TsResolutionResult.Ambiguous<EtsMethod>,
+    expr: EtsStaticCallExpr,
+) {
+    val args = expr.args.map { resolve(it) ?: return }
+    val staticProperties = resolved.properties.take(Constants.STATIC_METHODS_FORK_LIMIT)
+    val staticInstances = scope.calcOnState {
+        staticProperties.map { getStaticInstance(it.enclosingClass!!) }
+    }
+    val concreteCalls = staticProperties.mapIndexed { index, value ->
+        TsConcreteMethodCallStmt(
+            callee = value,
+            instance = staticInstances[index],
+            args = args,
+            returnSite = scope.calcOnState { lastStmt }
+        )
+    }
+    scope.forkMulti(
+        concreteCalls.map { stmt ->
+            ctx.mkTrue() to { newStmt(stmt) }
+        }
+    )
+}
+
+private fun TsExprResolver.processUniqueStaticMethod(
+    resolved: TsResolutionResult.Unique<EtsMethod>,
+    expr: EtsStaticCallExpr,
+) {
+    val instance = scope.calcOnState {
+        getStaticInstance(resolved.property.enclosingClass!!)
+    }
+    val args = expr.args.map { resolve(it) ?: return }
+    val concreteCall = TsConcreteMethodCallStmt(
+        callee = resolved.property,
+        instance = instance,
+        args = args,
+        returnSite = scope.calcOnState { lastStmt },
+    )
+    scope.doWithState { newStmt(concreteCall) }
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStaticApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStaticApproximations.kt
new file mode 100644
index 0000000000..5aeb93a092
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStaticApproximations.kt
@@ -0,0 +1,50 @@
+package org.usvm.machine.expr
+
+import org.jacodb.ets.model.EtsStaticCallExpr
+import org.usvm.UExpr
+import org.usvm.machine.expr.TsExprApproximationResult.Companion.from
+
+internal fun TsExprResolver.tryApproximateStaticCall(
+    expr: EtsStaticCallExpr,
+): TsExprApproximationResult {
+    // Mock `$r` calls
+    if (expr.callee.name == "\$r") {
+        return from(handleR())
+    }
+
+    // Handle `Number(...)` calls
+    if (expr.callee.name == "Number") {
+        return from(handleNumberConverter(expr))
+    }
+
+    // Handle `Boolean(...)` calls
+    if (expr.callee.name == "Boolean") {
+        return from(handleBooleanConverter(expr))
+    }
+
+    return TsExprApproximationResult.NoApproximation
+}
+
+private fun TsExprResolver.handleR(): UExpr<*> = with(ctx) {
+    val mockSymbol = scope.calcOnState {
+        memory.mocker.createMockSymbol(trackedLiteral = null, addressSort, ownership)
+    }
+    scope.assert(mkNot(mkEq(mockSymbol, mkTsNullValue())))
+    mockSymbol
+}
+
+private fun TsExprResolver.handleNumberConverter(expr: EtsStaticCallExpr): UExpr<*>? = with(ctx) {
+    check(expr.args.size == 1) {
+        "Number() should have exactly one argument, but got ${expr.args.size}"
+    }
+    val arg = resolve(expr.args.single()) ?: return null
+    return mkNumericExpr(arg, scope)
+}
+
+private fun TsExprResolver.handleBooleanConverter(expr: EtsStaticCallExpr): UExpr<*>? = with(ctx) {
+    check(expr.args.size == 1) {
+        "Boolean() should have exactly one argument, but got ${expr.args.size}"
+    }
+    val arg = resolve(expr.args.single()) ?: return null
+    return mkTruthyExpr(arg, scope)
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt
index d61e9a4ad8..64a764f4bb 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt
@@ -193,19 +193,30 @@ fun TsState.throwException(reason: String) {
     methodResult = TsMethodResult.TsException(ref, EtsStringType)
 }
 
+fun TsContext.mkNotNullOrUndefined(ref: UHeapRef): UBoolExpr {
+    require(!ref.isFakeObject()) {
+        "Fake object handling should be done outside of this function"
+    }
+    return mkNot(
+        mkOr(
+            mkHeapRefEq(ref, mkTsNullValue()),
+            mkHeapRefEq(ref, mkUndefinedValue())
+        )
+    )
+}
+
 fun TsContext.checkUndefinedOrNullPropertyRead(
     scope: TsStepScope,
     instance: UHeapRef,
     propertyName: String,
 ): Unit? {
-    val ref = instance.unwrapRef(scope)
-    val condition = mkAnd(
-        mkNot(mkHeapRefEq(ref, mkUndefinedValue())),
-        mkNot(mkHeapRefEq(ref, mkTsNullValue())),
-    )
+    require(!instance.isFakeObject()) {
+        "Fake object handling should be done outside of this function"
+    }
+    val condition = mkNotNullOrUndefined(instance)
     return scope.fork(
         condition,
-        blockOnFalseState = { throwException("Undefined or null property access: $propertyName of $ref") }
+        blockOnFalseState = { throwException("Undefined or null property access: $propertyName of $instance") }
     )
 }
 
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt
index 435c7cb402..b2272f28e2 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt
@@ -2,7 +2,6 @@ package org.usvm.machine.expr
 
 import io.ksmt.utils.asExpr
 import mu.KotlinLogging
-import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsFieldSignature
 import org.jacodb.ets.model.EtsInstanceFieldRef
 import org.jacodb.ets.model.EtsLocal
@@ -28,40 +27,45 @@ internal fun TsExprResolver.handleInstanceFieldRef(
     val instanceLocal = value.instance
 
     // Resolve the instance.
-    val instance = resolve(instanceLocal) ?: return null
-    check(instance.sort == addressSort) {
-        "Expected address sort for instance, got: ${instance.sort}"
+    val instance: UHeapRef = run {
+        val resolved = resolve(instanceLocal) ?: return null
+        if (resolved.isFakeObject()) {
+            scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: run {
+                logger.warn { "UNSAT after ensuring fake object is ref-typed" }
+                return null
+            }
+            resolved.extractRef(scope)
+        } else {
+            check(resolved.sort == addressSort) {
+                "Expected address sort for instance, got: ${resolved.sort}"
+            }
+            resolved.asExpr(addressSort)
+        }
     }
-    val instanceRef = instance.asExpr(addressSort)
 
     // TODO: consider moving this to 'readField'
     // Check for undefined or null property access.
-    checkUndefinedOrNullPropertyRead(scope, instanceRef, value.field.name) ?: return null
+    checkUndefinedOrNullPropertyRead(scope, instance, propertyName = value.field.name) ?: return null
 
-    // Handle reading "length" property for arrays.
-    if (value.field.name == "length" && instanceLocal.type is EtsArrayType) {
-        return readLengthArray(scope, instanceLocal, instanceRef)
-    }
-
-    // Handle reading "length" property for fake objects.
-    // TODO: handle "length" property for arrays inside fake objects
-    if (value.field.name == "length" && instanceRef.isFakeObject()) {
-        return readLengthFake(scope, instanceLocal, instanceRef)
+    // Handle reading "length" property.
+    if (value.field.name == "length") {
+        return readLengthProperty(scope, instanceLocal, instance)
     }
 
     // Read the field.
-    return readField(scope, instanceLocal, instanceRef, value.field, hierarchy)
+    return readField(scope, instanceLocal, instance, value.field, hierarchy)
 }
 
-internal fun TsContext.readField(
+fun TsContext.readField(
     scope: TsStepScope,
     instanceLocal: EtsLocal?,
     instance: UHeapRef,
     field: EtsFieldSignature,
     hierarchy: EtsHierarchy,
 ): UExpr<*> {
-    // Unwrap to get non-fake reference.
-    val unwrappedInstance = instance.unwrapRef(scope)
+    require(!instance.isFakeObject()) {
+        "Fake object handling should be done outside of this function"
+    }
 
     val sort = when (val etsField = resolveEtsField(instanceLocal, field, hierarchy)) {
         is TsResolutionResult.Empty -> {
@@ -72,7 +76,7 @@ internal fun TsContext.readField(
             // It is possible due to mistakes in the IR or if the field was added explicitly
             // in the code.
             // Probably, the right behaviour here is to fork the state.
-            unwrappedInstance.createFakeField(scope, field.name)
+            instance.createFakeField(scope, field.name)
             addressSort
         }
 
@@ -87,12 +91,12 @@ internal fun TsContext.readField(
         // That's not true in the common case for TS, but that's the decision we made.
         val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name))
         // assert is required to update models
-        scope.assert(memory.types.evalIsSubtype(unwrappedInstance, auxiliaryType))
+        scope.assert(memory.types.evalIsSubtype(instance, auxiliaryType))
     }
 
     // If the field type is known, we can read it directly.
     if (sort !is TsUnresolvedSort) {
-        val lValue = mkFieldLValue(sort, unwrappedInstance, field)
+        val lValue = mkFieldLValue(sort, instance, field)
         return scope.calcOnState { memory.read(lValue) }
     }
 
@@ -125,7 +129,7 @@ internal fun TsExprResolver.handleStaticFieldRef(
     return readStaticField(scope, value.field, hierarchy)
 }
 
-internal fun TsContext.readStaticField(
+fun TsContext.readStaticField(
     scope: TsStepScope,
     field: EtsFieldSignature,
     hierarchy: EtsHierarchy,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadGlobal.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadGlobal.kt
index 6db88b9726..ea37d294c5 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadGlobal.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadGlobal.kt
@@ -10,7 +10,7 @@ import org.usvm.util.mkFieldLValue
 
 private val logger = KotlinLogging.logger {}
 
-internal fun TsContext.readGlobal(
+fun TsContext.readGlobal(
     scope: TsStepScope,
     file: EtsFile,
     name: String,
@@ -18,9 +18,6 @@ internal fun TsContext.readGlobal(
     // Initialize globals in `file` if necessary
     ensureGlobalsInitialized(scope, file) ?: return@calcOnState null
 
-    // Get the globals container object
-    val dfltObject = getDfltObject(file)
-
     // Restore the sort of the requested global variable
     val savedSort = getSortForDfltObjectField(file, name)
     if (savedSort == null) {
@@ -30,6 +27,9 @@ internal fun TsContext.readGlobal(
         return@calcOnState null
     }
 
+    // Get the globals container object
+    val dfltObject = getDfltObject(file)
+
     // Read the global variable as a field of the globals container object
     val lValue = mkFieldLValue(savedSort, dfltObject, name)
     memory.read(lValue)
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt
index d407cff825..9490a370f4 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt
@@ -13,44 +13,19 @@ import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.sizeSort
 import org.usvm.util.mkArrayLengthLValue
 
-// Handles reading the `length` property of an array.
-internal fun TsContext.readLengthArray(
+// Handles reading the `length` property.
+fun TsContext.readLengthProperty(
     scope: TsStepScope,
     instanceLocal: EtsLocal,
-    instance: UHeapRef, // array
+    instance: UHeapRef,
 ): UExpr<*> {
-    // Assume that instance is always an array.
-    val arrayType = instanceLocal.type as EtsArrayType
-
-    // Read the length of the array.
-    return readArrayLength(scope, instance, arrayType)
-}
-
-// Handles reading the `length` property of a fake object.
-internal fun TsContext.readLengthFake(
-    scope: TsStepScope,
-    instanceLocal: EtsLocal,
-    instance: UHeapRef, // fake object
-): UExpr<*> {
-    require(instance.isFakeObject())
-
-    // If we want to get length from a fake object,
-    // we assume that it is an array (has address sort).
-    scope.doWithState {
-        val fakeType = instance.getFakeType(scope)
-        pathConstraints += fakeType.refTypeExpr
-    }
-
-    // Unwrap to get non-fake reference.
-    val unwrappedInstance = instance.unwrapRef(scope)
-
     // Determine the array type.
-    val arrayType = when (val type = instanceLocal.type) {
+    val arrayType: EtsArrayType = when (val type = instanceLocal.type) {
         is EtsArrayType -> type
 
         is EtsAnyType, is EtsUnknownType -> {
-            // If the type is not an array, we assume it is a fake object with
-            // a length property that behaves like an array.
+            // If the type is not an array, and explicitly unknown,
+            // we represent it is an array with unknown element type.
             EtsArrayType(EtsUnknownType, dimensions = 1)
         }
 
@@ -58,11 +33,11 @@ internal fun TsContext.readLengthFake(
     }
 
     // Read the length of the array.
-    return readArrayLength(scope, unwrappedInstance, arrayType)
+    return readArrayLength(scope, instance, arrayType)
 }
 
 // Reads the length of the array and returns it as a fp64 expression.
-internal fun TsContext.readArrayLength(
+fun TsContext.readArrayLength(
     scope: TsStepScope,
     array: UHeapRef,
     arrayType: EtsArrayType,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsApproximations.kt
new file mode 100644
index 0000000000..ad1a5c37b7
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsApproximations.kt
@@ -0,0 +1,16 @@
+package org.usvm.machine.expr
+
+import org.usvm.UExpr
+
+sealed interface TsExprApproximationResult {
+    data class SuccessfulApproximation(val expr: UExpr<*>) : TsExprApproximationResult
+    data object ResolveFailure : TsExprApproximationResult
+    data object NoApproximation : TsExprApproximationResult
+
+    companion object {
+        fun from(expr: UExpr<*>?): TsExprApproximationResult = when {
+            expr != null -> SuccessfulApproximation(expr)
+            else -> ResolveFailure
+        }
+    }
+}
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 bfea1c8634..386f3380c8 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
@@ -17,7 +17,6 @@ import org.jacodb.ets.model.EtsBooleanConstant
 import org.jacodb.ets.model.EtsCastExpr
 import org.jacodb.ets.model.EtsCaughtExceptionRef
 import org.jacodb.ets.model.EtsClassSignature
-import org.jacodb.ets.model.EtsClassType
 import org.jacodb.ets.model.EtsClosureFieldRef
 import org.jacodb.ets.model.EtsConstant
 import org.jacodb.ets.model.EtsDeleteExpr
@@ -38,7 +37,6 @@ import org.jacodb.ets.model.EtsLexicalEnvType
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsLtEqExpr
 import org.jacodb.ets.model.EtsLtExpr
-import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsMethodSignature
 import org.jacodb.ets.model.EtsMulExpr
 import org.jacodb.ets.model.EtsNegExpr
@@ -78,9 +76,7 @@ import org.jacodb.ets.model.EtsVoidExpr
 import org.jacodb.ets.model.EtsYieldExpr
 import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX
 import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME
-import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME
 import org.jacodb.ets.utils.getDeclaredLocals
-import org.usvm.UBoolExpr
 import org.usvm.UExpr
 import org.usvm.UIteExpr
 import org.usvm.USort
@@ -92,10 +88,8 @@ import org.usvm.api.mockMethodCall
 import org.usvm.dataflow.ts.infer.tryGetKnownType
 import org.usvm.dataflow.ts.util.type
 import org.usvm.isAllocatedConcreteHeapRef
-import org.usvm.machine.Constants
 import org.usvm.machine.TsConcreteMethodCallStmt
 import org.usvm.machine.TsContext
-import org.usvm.machine.TsVirtualMethodCallStmt
 import org.usvm.machine.interpreter.PromiseState
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.interpreter.getGlobals
@@ -106,7 +100,6 @@ import org.usvm.machine.interpreter.setResolvedValue
 import org.usvm.machine.operator.TsBinaryOperator
 import org.usvm.machine.operator.TsUnaryOperator
 import org.usvm.machine.state.TsMethodResult
-import org.usvm.machine.state.TsState
 import org.usvm.machine.state.lastStmt
 import org.usvm.machine.state.localsCount
 import org.usvm.machine.state.newStmt
@@ -114,7 +107,6 @@ import org.usvm.machine.types.iteWriteIntoFakeObject
 import org.usvm.sizeSort
 import org.usvm.util.EtsHierarchy
 import org.usvm.util.SymbolResolutionResult
-import org.usvm.util.TsResolutionResult
 import org.usvm.util.isResolved
 import org.usvm.util.mkFieldLValue
 import org.usvm.util.mkRegisterStackLValue
@@ -849,187 +841,9 @@ class TsExprResolver(
 
     // region CALL
 
-    override fun visit(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) {
-        when (val result = tryApproximateInstanceCall(expr)) {
-            is TsExprApproximationResult.SuccessfulApproximation -> return result.expr
-            is TsExprApproximationResult.ResolveFailure -> return null
-            is TsExprApproximationResult.NoApproximation -> {}
-        }
-
-        val result = scope.calcOnState { methodResult }
-
-        if (result is TsMethodResult.Success) {
-            scope.doWithState { methodResult = TsMethodResult.NoCall }
-            return result.value
-        }
-
-        if (result is TsMethodResult.TsException) {
-            error("Exception should be handled earlier")
-        }
-
-        check(result is TsMethodResult.NoCall)
-
-        val instance = run {
-            val resolved = resolve(expr.instance) ?: return null
-
-            if (resolved.sort != addressSort) {
-                logger.warn { "Calling method on non-ref instance is not yet supported: $expr" }
-                scope.assert(falseExpr)
-                return null
-            }
-
-            resolved.asExpr(addressSort)
-        }
-
-        checkUndefinedOrNullPropertyRead(scope, instance, expr.callee.name) ?: return null
-
-        val resolvedArgs = expr.args.map { resolve(it) ?: return null }
-
-        val virtualCall = TsVirtualMethodCallStmt(
-            callee = expr.callee,
-            instance = instance,
-            args = resolvedArgs,
-            returnSite = scope.calcOnState { lastStmt },
-        )
-        scope.doWithState { newStmt(virtualCall) }
-
-        null
-    }
-
-    private fun handleR(): UExpr<*>? = with(ctx) {
-        val mockSymbol = scope.calcOnState {
-            memory.mocker.createMockSymbol(trackedLiteral = null, addressSort, ownership)
-        }
-        scope.assert(mkNot(mkEq(mockSymbol, mkTsNullValue())))
-        mockSymbol
-    }
-
-    private fun handleNumberConverter(expr: EtsStaticCallExpr): UExpr<*>? = with(ctx) {
-        check(expr.args.size == 1) {
-            "Number() should have exactly one argument, but got ${expr.args.size}"
-        }
-        val arg = resolve(expr.args.single()) ?: return null
-        return mkNumericExpr(arg, scope)
-    }
-
-    private fun handleBooleanConverter(expr: EtsStaticCallExpr): UExpr<*>? = with(ctx) {
-        check(expr.args.size == 1) {
-            "Boolean() should have exactly one argument, but got ${expr.args.size}"
-        }
-        val arg = resolve(expr.args.single()) ?: return null
-        return mkTruthyExpr(arg, scope)
-    }
-
-    override fun visit(expr: EtsStaticCallExpr): UExpr<*>? = with(ctx) {
-        // Mock `$r` calls
-        if (expr.callee.name == "\$r") {
-            return handleR()
-        }
-
-        // Handle `Number(...)` calls
-        if (expr.callee.name == "Number") {
-            return handleNumberConverter(expr)
-        }
-
-        // Handle `Boolean(...)` calls
-        if (expr.callee.name == "Boolean") {
-            return handleBooleanConverter(expr)
-        }
-
-        val result = scope.calcOnState { methodResult }
-
-        if (result is TsMethodResult.Success) {
-            scope.doWithState { methodResult = TsMethodResult.NoCall }
-            return result.value
-        }
-
-        if (result is TsMethodResult.TsException) {
-            error("Exception should be handled earlier")
-        }
-
-        check(result is TsMethodResult.NoCall)
-
-        when (val resolved = resolveStaticMethod(expr.callee)) {
-            is TsResolutionResult.Empty -> {
-                logger.error { "Could not resolve static call: ${expr.callee}" }
-                scope.assert(falseExpr)
-            }
+    override fun visit(expr: EtsInstanceCallExpr): UExpr<*>? = handleInstanceCall(expr)
 
-            is TsResolutionResult.Ambiguous -> {
-                processAmbiguousStaticMethod(resolved, expr)
-            }
-
-            is TsResolutionResult.Unique -> {
-                processUniqueStaticMethod(resolved, expr)
-            }
-        }
-
-        null
-    }
-
-    private fun resolveStaticMethod(method: EtsMethodSignature): TsResolutionResult<EtsMethod> {
-        // Perfect signature:
-        if (method.enclosingClass.name != UNKNOWN_CLASS_NAME) {
-            val classes = hierarchy.classesForType(EtsClassType(method.enclosingClass))
-            if (classes.size > 1) {
-                val methods = classes.map { it.methods.single { it.name == method.name } }
-                return TsResolutionResult.create(methods)
-            }
-
-            if (classes.isEmpty()) return TsResolutionResult.Empty
-
-            val clazz = classes.single()
-            val methods = clazz.methods.filter { it.name == method.name }
-            return TsResolutionResult.create(methods)
-        }
-
-        // Unknown signature:
-        val methods = ctx.scene.projectAndSdkClasses
-            .flatMap { it.methods }
-            .filter { it.name == method.name }
-
-        return TsResolutionResult.create(methods)
-    }
-
-    private fun processAmbiguousStaticMethod(
-        resolved: TsResolutionResult.Ambiguous<EtsMethod>,
-        expr: EtsStaticCallExpr,
-    ) {
-        val resolvedArgs = expr.args.map { resolve(it) ?: return }
-        val staticProperties = resolved.properties.take(Constants.STATIC_METHODS_FORK_LIMIT)
-        val staticInstances = scope.calcOnState {
-            staticProperties.map { getStaticInstance(it.enclosingClass!!) }
-        }
-        val concreteCalls = staticProperties.mapIndexed { index, value ->
-            TsConcreteMethodCallStmt(
-                callee = value,
-                instance = staticInstances[index],
-                args = resolvedArgs,
-                returnSite = scope.calcOnState { lastStmt }
-            )
-        }
-        val blocks: List<Pair<UBoolExpr, TsState.() -> Unit>> = concreteCalls.map { stmt ->
-            ctx.mkTrue() to { newStmt(stmt) }
-        }
-        scope.forkMulti(blocks)
-    }
-
-    private fun processUniqueStaticMethod(
-        resolved: TsResolutionResult.Unique<EtsMethod>,
-        expr: EtsStaticCallExpr,
-    ) {
-        val instance = scope.calcOnState {
-            getStaticInstance(resolved.property.enclosingClass!!)
-        }
-        val args = expr.args.map { resolve(it) ?: return }
-        val concreteCall = TsConcreteMethodCallStmt(
-            callee = resolved.property,
-            instance = instance,
-            args = args,
-            returnSite = scope.calcOnState { lastStmt },
-        )
-        scope.doWithState { newStmt(concreteCall) }
-    }
+    override fun visit(expr: EtsStaticCallExpr): UExpr<*>? = handleStaticCall(expr)
 
     override fun visit(expr: EtsPtrCallExpr): UExpr<out USort>? = with(ctx) {
         when (val result = scope.calcOnState { methodResult }) {
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt
index 60790925f1..aa52d2c21b 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt
@@ -59,7 +59,7 @@ internal fun TsExprResolver.handleAssignToArrayIndex(
     return assignToArrayIndex(scope, array, bvIndex, expr, arrayType)
 }
 
-internal fun TsContext.assignToArrayIndex(
+fun TsContext.assignToArrayIndex(
     scope: TsStepScope,
     array: UHeapRef,
     index: UExpr<TsSizeSort>,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt
index dd15548291..3740f4634d 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt
@@ -1,6 +1,7 @@
 package org.usvm.machine.expr
 
 import io.ksmt.utils.asExpr
+import mu.KotlinLogging
 import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsFieldSignature
 import org.jacodb.ets.model.EtsInstanceFieldRef
@@ -17,6 +18,8 @@ import org.usvm.util.TsResolutionResult
 import org.usvm.util.mkFieldLValue
 import org.usvm.util.resolveEtsField
 
+private val logger = KotlinLogging.logger {}
+
 internal fun TsExprResolver.handleAssignToInstanceField(
     lhv: EtsInstanceFieldRef,
     expr: UExpr<*>,
@@ -25,20 +28,30 @@ internal fun TsExprResolver.handleAssignToInstanceField(
     val field = lhv.field
 
     // Resolve the instance.
-    val instance = resolve(instanceLocal) ?: return null
-    check(instance.sort == addressSort) {
-        "Expected address sort for instance, got: ${instance.sort}"
+    val instance: UHeapRef = run {
+        val resolved = resolve(instanceLocal) ?: return null
+        if (resolved.isFakeObject()) {
+            scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: run {
+                logger.warn { "UNSAT after ensuring fake object is ref-typed" }
+                return null
+            }
+            resolved.extractRef(scope)
+        } else {
+            check(resolved.sort == addressSort) {
+                "Expected address sort for instance, got: ${resolved.sort}"
+            }
+            resolved.asExpr(addressSort)
+        }
     }
-    val instanceRef = instance.asExpr(addressSort)
 
     // Check for undefined or null field access.
-    checkUndefinedOrNullPropertyRead(scope, instanceRef, field.name) ?: return null
+    checkUndefinedOrNullPropertyRead(scope, instance, field.name) ?: return null
 
     // Assign to the field.
-    assignToInstanceField(scope, instanceLocal, instanceRef, field, expr, hierarchy)
+    assignToInstanceField(scope, instanceLocal, instance, field, expr, hierarchy)
 }
 
-internal fun TsContext.assignToInstanceField(
+fun TsContext.assignToInstanceField(
     scope: TsStepScope,
     instanceLocal: EtsLocal,
     instance: UHeapRef,
@@ -112,7 +125,7 @@ internal fun TsExprResolver.handleAssignToStaticField(
     assignToStaticField(scope, lhv.field, expr)
 }
 
-internal fun TsContext.assignToStaticField(
+fun TsContext.assignToStaticField(
     scope: TsStepScope,
     field: EtsFieldSignature,
     expr: UExpr<*>,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteGlobal.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteGlobal.kt
index 327c9eba73..4a97d68828 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteGlobal.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteGlobal.kt
@@ -8,7 +8,7 @@ import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.interpreter.ensureGlobalsInitialized
 import org.usvm.util.mkFieldLValue
 
-internal fun TsContext.writeGlobal(
+fun TsContext.writeGlobal(
     scope: TsStepScope,
     file: EtsFile,
     name: String,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteLocal.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteLocal.kt
index f5802e7735..6b07e6fca8 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteLocal.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteLocal.kt
@@ -17,7 +17,7 @@ internal fun TsExprResolver.handleAssignToLocal(
     return assignToLocal(scope, local, expr)
 }
 
-internal fun TsContext.assignToLocal(
+fun TsContext.assignToLocal(
     scope: TsStepScope,
     local: EtsLocal,
     expr: UExpr<*>,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt
index cba36ca32a..269a95aea2 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt
@@ -6,7 +6,6 @@ import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
 import org.usvm.UBoolSort
-import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.collection.field.UFieldLValue
 import org.usvm.isTrue
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/FieldAccess.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/FieldAccess.kt
index ce2d9a0ec4..08e880185a 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/FieldAccess.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/FieldAccess.kt
@@ -130,4 +130,23 @@ class FieldAccess : TsMethodTestRunner() {
             { r -> r eq 1 },
         )
     }
+
+    @Test
+    fun `test readFromAny`() {
+        val method = getMethod("readFromAny")
+        discoverProperties<TsTestValue, TsTestValue.TsNumber>(
+            method = method,
+            { _, r -> r eq 1 },
+            { _, r -> r eq 2 },
+        )
+    }
+
+    @Test
+    fun `test writeToAny`() {
+        val method = getMethod("writeToAny")
+        discoverProperties<TsTestValue, TsTestValue.TsNumber>(
+            method = method,
+            { _, r -> r eq 50 },
+        )
+    }
 }
diff --git a/usvm-ts/src/test/resources/samples/lang/FieldAccess.ts b/usvm-ts/src/test/resources/samples/lang/FieldAccess.ts
index 1b4b9f008d..efe25dff32 100644
--- a/usvm-ts/src/test/resources/samples/lang/FieldAccess.ts
+++ b/usvm-ts/src/test/resources/samples/lang/FieldAccess.ts
@@ -80,6 +80,21 @@ class FieldAccess {
     private createObject(): { x: number } {
         return { x: 42 };
     }
+
+    readFromAny(x: any): number {
+        if (x === undefined) return 0;
+        if (x === null) return 0;
+        if (x.a === 10) return 1;
+        return 2;
+    }
+
+    writeToAny(x: any): number {
+        if (x === undefined) return 0;
+        if (x === null) return 0;
+        x.a = 20;
+        x.b = 30;
+        return x.a + x.b;
+    }
 }
 
 class SimpleClass {