[TS] Construct project instances from runtime constructor values

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

@@ -80,7 +80,13 @@ fun TsContext.readField(
 
         is TsResolutionResult.Unique -> typeToSort(etsField.property.type)
 
-        is TsResolutionResult.Ambiguous -> unresolvedSort
+        is TsResolutionResult.Ambiguous -> resolveAmbiguousFieldSort(
+            scope = scope,
+            instanceLocal = instanceLocal,
+            instance = instance,
+            fields = etsField.properties,
+            hierarchy = hierarchy,
+        )
     }
 
     scope.doWithState {

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

@@ -0,0 +1,37 @@
+package org.usvm.machine.expr
+
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsField
+import org.jacodb.ets.model.EtsLocal
+import org.jacodb.ets.model.EtsUnionType
+import org.usvm.UHeapRef
+import org.usvm.USort
+import org.usvm.api.typeStreamOf
+import org.usvm.isAllocatedConcreteHeapRef
+import org.usvm.machine.TsContext
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.types.singleOrNull
+import org.usvm.util.EtsHierarchy
+
+internal fun TsContext.resolveAmbiguousFieldSort(
+    scope: TsStepScope,
+    instanceLocal: EtsLocal?,
+    instance: UHeapRef,
+    fields: List<EtsField>,
+    hierarchy: EtsHierarchy,
+): USort {
+    // A dynamic constructor leaves the local union-typed after allocating one concrete class.
+    // Keep the existing representation for other ambiguous and any-typed fields.
+    if (instanceLocal?.type !is EtsUnionType || !isAllocatedConcreteHeapRef(instance)) {
+        return unresolvedSort
+    }
+
+    val runtimeType = scope.calcOnState { memory.typeStreamOf(instance).singleOrNull() }
+    val runtimeClass = (runtimeType as? EtsClassType)?.let { type ->
+        scene.projectAndSdkClasses.singleOrNull { it.signature == type.signature }
+    } ?: return unresolvedSort
+
+    val ancestors = hierarchy.getAncestors(runtimeClass)
+    val runtimeField = fields.singleOrNull { it.declaringClass in ancestors } ?: return unresolvedSort
+    return typeToSort(runtimeField.type)
+}

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

@@ -958,16 +958,16 @@ class TsExprResolver(
 
     private fun resolveInstanceofConstructor(checkValue: EtsEntity): EtsClassType? = with(ctx) {
         val constructor = resolve(checkValue) ?: return null
-        if (constructor.sort == fp64Sort || constructor.sort == boolSort) return throwInstanceofTypeError()
-        if (constructor == mkTsNullValue() || constructor == mkUndefinedValue()) return throwInstanceofTypeError()
+        if (constructor.sort == fp64Sort || constructor.sort == boolSort) return throwTypeError()
+        if (constructor == mkTsNullValue() || constructor == mkUndefinedValue()) return throwTypeError()
 
         if (constructor.sort != addressSort || constructor.isFakeObject()) {
             throw UnsupportedOperationException("Unresolved instanceof RHS callability is not modeled")
         }
 
         val constructorRef = constructor as? UConcreteHeapRef
             ?: throw UnsupportedOperationException("Symbolic instanceof constructor identity is not modeled")
-        if (getStringConstantValue(constructorRef) != null) return throwInstanceofTypeError()
+        if (getStringConstantValue(constructorRef) != null) return throwTypeError()
 
         val signature = classConstructorSignature(constructorRef)
             ?: return resolveNonConstructorInstanceofRight(constructorRef)
@@ -994,7 +994,7 @@ class TsExprResolver(
             null
         }
         val objectType = (objectTypes as? TypesResult.SuccessfulTypesResult)?.types?.singleOrNull()
-        if (objectType == EtsStringType) return throwInstanceofTypeError()
+        if (objectType == EtsStringType) return throwTypeError()
 
         val objectClass = (objectType as? EtsClassType)?.let { type ->
             scene.projectClasses.singleOrNull { it.signature == type.signature }
@@ -1009,13 +1009,13 @@ class TsExprResolver(
             }
             val isFunction = scope.calcOnState { associatedFunction[ref] != null }
 
-            if (ordinaryObject && !hasComputedMember && !isFunction) return throwInstanceofTypeError()
+            if (ordinaryObject && !hasComputedMember && !isFunction) return throwTypeError()
         }
 
         throw UnsupportedOperationException("Unknown instanceof constructor value: $ref")
     }
 
-    private fun throwInstanceofTypeError(): Nothing? {
+    private fun throwTypeError(): Nothing? {
         scope.doWithState {
             val exception = memory.allocConcrete(TS_TYPE_ERROR_TYPE)
             methodResult = TsMethodResult.TsException(exception, TS_TYPE_ERROR_TYPE)
@@ -1181,6 +1181,8 @@ class TsExprResolver(
     // region OTHER
 
     override fun visit(expr: EtsNewExpr): UExpr<out USort>? = with(ctx) {
+        expr.constructorValue?.let { return@with constructRuntimeClass(it) }
+
         // Try to resolve the concrete type if possible.
         // Otherwise, create an object with UnclearRefType
         val resolvedType = if (expr.type.isResolved()) {
@@ -1206,6 +1208,45 @@ class TsExprResolver(
         scope.calcOnState { memory.allocConcrete(resolvedType) }
     }
 
+    private fun constructRuntimeClass(constructorValue: EtsValue): UExpr<out USort>? = with(ctx) {
+        val constructor = resolve(constructorValue) ?: return@with null
+        if (constructor.sort == fp64Sort || constructor.sort == boolSort) return@with throwTypeError()
+        if (constructor == mkTsNullValue() || constructor == mkUndefinedValue()) return@with throwTypeError()
+
+        if (constructor.sort != addressSort || constructor.isFakeObject()) {
+            throw UnsupportedOperationException("Unresolved new constructor callability is not modeled")
+        }
+
+        val constructorRef = constructor as? UConcreteHeapRef
+            ?: throw UnsupportedOperationException("Symbolic new constructor identity is not modeled")
+        if (getStringConstantValue(constructorRef) != null) return@with throwTypeError()
+
+        val signature = classConstructorSignature(constructorRef)
+            ?: return@with resolveNonConstructorNew(constructorRef)
+        val clazz = scene.projectClasses.singleOrNull { it.signature == signature }
+            ?: throw UnsupportedOperationException("Unknown new project class: $signature")
+
+        scope.calcOnState { memory.allocConcrete(clazz.type) }
+    }
+
+    private fun resolveNonConstructorNew(ref: UConcreteHeapRef): Nothing? = with(ctx) {
+        val objectTypes = if (isAllocatedConcreteHeapRef(ref)) {
+            scope.calcOnState { memory.typeStreamOf(ref).take(n = 2) }
+        } else {
+            null
+        }
+        val objectType = (objectTypes as? TypesResult.SuccessfulTypesResult)?.types?.singleOrNull()
+        val objectClass = (objectType as? EtsClassType)?.let { type ->
+            scene.projectClasses.singleOrNull { it.signature == type.signature }
+        }
+        val isOrdinaryInstance = objectClass?.category == EtsClassCategory.CLASS ||
+            objectClass?.category == EtsClassCategory.OBJECT
+        val isFunction = scope.calcOnState { associatedFunction[ref] != null }
+        if (isOrdinaryInstance && !isFunction) return@with throwTypeError()
+
+        throw UnsupportedOperationException("Unknown new constructor value: $ref")
+    }
+
     override fun visit(expr: EtsNewArrayExpr): UExpr<out USort>? = with(ctx) {
         val arrayType = expr.type
 

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

@@ -3,11 +3,9 @@ package org.usvm.machine.expr
 import io.ksmt.utils.asExpr
 import mu.KotlinLogging
 import org.jacodb.ets.model.EtsArrayType
-import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsFieldSignature
 import org.jacodb.ets.model.EtsInstanceFieldRef
 import org.jacodb.ets.model.EtsLocal
-import org.jacodb.ets.model.EtsNumberType
 import org.jacodb.ets.model.EtsStaticFieldRef
 import org.usvm.UExpr
 import org.usvm.UHeapRef
@@ -153,7 +151,34 @@ fun TsContext.assignToInstanceField(
     val sort = when (etsField) {
         is TsResolutionResult.Empty -> unresolvedSort
         is TsResolutionResult.Unique -> typeToSort(etsField.property.type)
-        is TsResolutionResult.Ambiguous -> unresolvedSort
+        is TsResolutionResult.Ambiguous -> resolveAmbiguousFieldSort(
+            scope = scope,
+            instanceLocal = instanceLocal,
+            instance = unwrappedInstance,
+            fields = etsField.properties,
+            hierarchy = hierarchy,
+        )
+    }
+
+    if (sort !is TsUnresolvedSort && expr.isFakeObject()) {
+        val fakeType = scope.calcOnState { expr.getFakeType(scope) }
+        val compatibleType = when (sort) {
+            boolSort -> fakeType.boolTypeExpr
+            fp64Sort -> fakeType.fpTypeExpr
+            addressSort -> fakeType.refTypeExpr
+            else -> error("Unsupported field sort: $sort")
+        }
+
+        scope.fork(
+            compatibleType,
+            blockOnFalseState = {
+                terminateAsUnsupported(reason = "Assignment changes runtime sort of field '${field.name}'")
+            },
+        ) ?: return
+    }
+
+    if (sort !is TsUnresolvedSort && expr.sort != sort && !expr.isFakeObject()) {
+        throw UnsupportedOperationException("Assignment changes runtime sort of field '${field.name}'")
     }
 
     // If the field type is unknown, we create a fake object for the expr and assign it.
@@ -167,28 +192,14 @@ fun TsContext.assignToInstanceField(
         } else {
             val lValue = mkFieldLValue(sort, unwrappedInstance, field)
             if (lValue.sort != expr.sort) {
-                if (expr.isFakeObject()) {
-                    val lhvType = instanceLocal.type
-                    val value = when (lhvType) {
-                        is EtsBooleanType -> {
-                            pathConstraints += expr.getFakeType(scope).boolTypeExpr
-                            expr.extractBool(scope)
-                        }
-
-                        is EtsNumberType -> {
-                            pathConstraints += expr.getFakeType(scope).fpTypeExpr
-                            expr.extractFp(scope)
-                        }
-
-                        else -> {
-                            pathConstraints += expr.getFakeType(scope).refTypeExpr
-                            expr.extractRef(scope)
-                        }
-                    }
-                    memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr)
-                } else {
-                    TODO("Support enums fields")
+                check(expr.isFakeObject())
+                val value = when (sort) {
+                    boolSort -> expr.extractBool(scope)
+                    fp64Sort -> expr.extractFp(scope)
+                    addressSort -> expr.extractRef(scope)
+                    else -> error("Unsupported field sort: $sort")
                 }
+                memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr)
             } else {
                 memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
             }