[TS] Some fixes to read/write, fake objects, calls

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
+}

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

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) }
+}

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)
+}

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") }
     )
 }