Different fixes (#278)

Author: CaelmBleidd

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

@@ -2,6 +2,7 @@ package org.usvm.machine
 
 import io.ksmt.sort.KFp64Sort
 import io.ksmt.utils.asExpr
+import org.jacodb.ets.model.EtsAliasType
 import org.jacodb.ets.model.EtsAnyType
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBooleanType
@@ -28,8 +29,10 @@ import org.usvm.collection.field.UFieldLValue
 import org.usvm.isTrue
 import org.usvm.machine.expr.TsUndefinedSort
 import org.usvm.machine.expr.TsUnresolvedSort
+import org.usvm.machine.expr.TsVoidSort
+import org.usvm.machine.expr.TsVoidValue
 import org.usvm.machine.interpreter.TsStepScope
-import org.usvm.machine.types.FakeType
+import org.usvm.machine.types.EtsFakeType
 import org.usvm.memory.UReadOnlyMemory
 import org.usvm.types.single
 import org.usvm.util.mkFieldLValue
@@ -46,6 +49,10 @@ class TsContext(
 
     val unresolvedSort: TsUnresolvedSort = TsUnresolvedSort(this)
 
+    val voidSort: TsVoidSort by lazy { TsVoidSort(this) }
+    val voidValue: TsVoidValue by lazy { TsVoidValue(this) }
+
+
     /**
      * In TS we treat undefined value as a null reference in other objects.
      * For real null represented in the language we create another reference.
@@ -66,6 +73,7 @@ class TsContext(
         is EtsRefType -> addressSort
         is EtsAnyType -> unresolvedSort
         is EtsUnknownType -> unresolvedSort
+        is EtsAliasType -> typeToSort(type.originalType)
         else -> TODO("${type::class.simpleName} is not yet supported: $type")
     }
 
@@ -78,12 +86,12 @@ class TsContext(
     //  since we do not rely on array types in any way.
     fun arrayDescriptorOf(type: EtsArrayType): EtsType = EtsUnknownType
 
-    fun UConcreteHeapRef.getFakeType(memory: UReadOnlyMemory<*>): FakeType {
+    fun UConcreteHeapRef.getFakeType(memory: UReadOnlyMemory<*>): EtsFakeType {
         check(isFakeObject())
-        return memory.typeStreamOf(this).single() as FakeType
+        return memory.typeStreamOf(this).single() as EtsFakeType
     }
 
-    fun UConcreteHeapRef.getFakeType(scope: TsStepScope): FakeType =
+    fun UConcreteHeapRef.getFakeType(scope: TsStepScope): EtsFakeType =
         scope.calcOnState { getFakeType(memory) }
 
     @OptIn(ExperimentalContracts::class)
@@ -107,19 +115,19 @@ class TsContext(
                 boolSort -> {
                     val lvalue = getIntermediateBoolLValue(ref.address)
                     memory.write(lvalue, asExpr(boolSort), guard = trueExpr)
-                    memory.types.allocate(ref.address, FakeType.mkBool(this@TsContext))
+                    memory.types.allocate(ref.address, EtsFakeType.mkBool(this@TsContext))
                 }
 
                 fp64Sort -> {
                     val lValue = getIntermediateFpLValue(ref.address)
                     memory.write(lValue, asExpr(fp64Sort), guard = trueExpr)
-                    memory.types.allocate(ref.address, FakeType.mkFp(this@TsContext))
+                    memory.types.allocate(ref.address, EtsFakeType.mkFp(this@TsContext))
                 }
 
                 addressSort -> {
                     val lValue = getIntermediateRefLValue(ref.address)
                     memory.write(lValue, asExpr(addressSort), guard = trueExpr)
-                    memory.types.allocate(ref.address, FakeType.mkRef(this@TsContext))
+                    memory.types.allocate(ref.address, EtsFakeType.mkRef(this@TsContext))
                 }
 
                 else -> TODO("Not yet supported")

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

@@ -10,8 +10,8 @@ import org.usvm.api.makeSymbolicPrimitive
 import org.usvm.isFalse
 import org.usvm.machine.TsContext
 import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.types.EtsFakeType
 import org.usvm.machine.types.ExprWithTypeConstraint
-import org.usvm.machine.types.FakeType
 import org.usvm.types.single
 import org.usvm.util.boolToFp
 
@@ -23,7 +23,7 @@ fun TsContext.mkTruthyExpr(
         val falseBranchGround = makeSymbolicPrimitive(boolSort)
 
         val conjuncts = mutableListOf<ExprWithTypeConstraint<UBoolSort>>()
-        val possibleType = memory.types.getTypeStream(expr.asExpr(addressSort)).single() as FakeType
+        val possibleType = memory.types.getTypeStream(expr.asExpr(addressSort)).single() as EtsFakeType
 
         scope.doWithState {
             pathConstraints += possibleType.mkExactlyOneTypeConstraint(this@mkTruthyExpr)

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

@@ -15,8 +15,6 @@ import org.jacodb.ets.model.EtsBitOrExpr
 import org.jacodb.ets.model.EtsBitXorExpr
 import org.jacodb.ets.model.EtsBooleanConstant
 import org.jacodb.ets.model.EtsCastExpr
-import org.jacodb.ets.model.EtsClassSignature
-import org.jacodb.ets.model.EtsClassType
 import org.jacodb.ets.model.EtsConstant
 import org.jacodb.ets.model.EtsDeleteExpr
 import org.jacodb.ets.model.EtsDivExpr
@@ -99,10 +97,13 @@ import org.usvm.machine.state.TsState
 import org.usvm.machine.state.lastStmt
 import org.usvm.machine.state.localsCount
 import org.usvm.machine.state.newStmt
-import org.usvm.machine.types.AuxiliaryType
+import org.usvm.machine.types.EtsAuxiliaryType
 import org.usvm.machine.types.mkFakeValue
 import org.usvm.memory.ULValue
 import org.usvm.sizeSort
+import org.usvm.util.EtsFieldResolutionResult
+import org.usvm.util.EtsHierarchy
+import org.usvm.util.createFakeField
 import org.usvm.util.isResolved
 import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
@@ -125,7 +126,8 @@ const val ADHOC_STRING__STRING = 2222.0 // 'string'
 class TsExprResolver(
     private val ctx: TsContext,
     private val scope: TsStepScope,
-    private val localToIdx: (EtsMethod, EtsValue) -> Int,
+    private val localToIdx: (EtsMethod, EtsValue) -> Int?,
+    private val hierarchy: EtsHierarchy,
 ) : EtsEntity.Visitor<UExpr<out USort>?> {
 
     val simpleValueResolver: TsSimpleValueResolver =
@@ -630,24 +632,33 @@ class TsExprResolver(
         instance: EtsLocal?,
         instanceRef: UHeapRef,
         field: EtsFieldSignature,
+        hierarchy: EtsHierarchy,
     ): UExpr<out USort>? = with(ctx) {
         val resolvedAddr = if (instanceRef.isFakeObject()) instanceRef.extractRef(scope) else instanceRef
         scope.doWithState {
-            pathConstraints += if (field.enclosingClass != EtsClassSignature.UNKNOWN) {
-                // If we know an enclosing class of the field,
-                // we can add a type constraint about the instance type.
-                // Probably, it's redundant since either both class and field
-                // know exactly their types or none of them.
-                val type = EtsClassType(field.enclosingClass)
-                memory.types.evalIsSubtype(resolvedAddr, type)
-            } else {
-                // Otherwise, we add a type constraint that every type containing such field is fine
-                memory.types.evalIsSubtype(resolvedAddr, AuxiliaryType(setOf(field.name)))
-            }
+            // If we accessed some field, we make an assumption that
+            // this field should present in the object.
+            // That's not true in the common case for TS, but that's the decision we made.
+            val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name))
+            pathConstraints += memory.types.evalIsSubtype(resolvedAddr, auxiliaryType)
         }
 
-        val etsField = resolveEtsField(instance, field)
-        val sort = typeToSort(etsField.type)
+        val etsField = resolveEtsField(instance, field, hierarchy)
+
+        val sort = when (etsField) {
+            is EtsFieldResolutionResult.Empty -> {
+                logger.error("Field $etsField not found, creating fake field")
+                // If we didn't find any real fields, let's create a fake one.
+                // 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.
+                resolvedAddr.createFakeField(field.name, scope)
+                addressSort
+            }
+
+            is EtsFieldResolutionResult.Unique -> typeToSort(etsField.field.type)
+            is EtsFieldResolutionResult.Ambiguous -> unresolvedSort
+        }
 
         if (sort == unresolvedSort) {
             val boolLValue = mkFieldLValue(boolSort, instanceRef, field)
@@ -714,7 +725,7 @@ class TsExprResolver(
             }
         }
 
-        return handleFieldRef(value.instance, instanceRef, value.field)
+        return handleFieldRef(value.instance, instanceRef, value.field, hierarchy)
     }
 
     override fun visit(value: EtsStaticFieldRef): UExpr<out USort>? = with(ctx) {
@@ -747,7 +758,7 @@ class TsExprResolver(
             }
         }
 
-        return handleFieldRef(instance = null, instanceRef, value.field)
+        return handleFieldRef(instance = null, instanceRef, value.field, hierarchy)
     }
 
     // endregion
@@ -811,14 +822,39 @@ class TsExprResolver(
 class TsSimpleValueResolver(
     private val ctx: TsContext,
     private val scope: TsStepScope,
-    private val localToIdx: (EtsMethod, EtsValue) -> Int,
+    private val localToIdx: (EtsMethod, EtsValue) -> Int?,
 ) : EtsValue.Visitor<UExpr<out USort>?> {
 
     private fun resolveLocal(local: EtsValue): ULValue<*, USort> {
         val currentMethod = scope.calcOnState { lastEnteredMethod }
         val entrypoint = scope.calcOnState { entrypoint }
 
         val localIdx = localToIdx(currentMethod, local)
+
+        // If there is no local variable corresponding to the local,
+        // we treat it as a field of some global object with the corresponding name.
+        // It helps us to support global variables that are missed in the IR.
+        if (localIdx == null) {
+            require(local is EtsLocal)
+
+            val globalObject = scope.calcOnState { globalObject }
+
+            val localName = local.name
+            // Check whether this local was already created or not
+            if (localName in scope.calcOnState { addedArtificialLocals }) {
+                return mkFieldLValue(ctx.addressSort, globalObject, local.name)
+            }
+
+            logger.warn { "Cannot resolve local $local" }
+
+            globalObject.createFakeField(localName, scope)
+            scope.doWithState {
+                addedArtificialLocals += localName
+            }
+
+            return mkFieldLValue(ctx.addressSort, globalObject, local.name)
+        }
+
         val sort = scope.calcOnState {
             val type = local.tryGetKnownType(currentMethod)
             getOrPutSortForLocal(localIdx, type)

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

@@ -4,6 +4,7 @@ import io.ksmt.KAst
 import io.ksmt.cache.hash
 import io.ksmt.cache.structurallyEqual
 import io.ksmt.expr.KBitVec32Value
+import io.ksmt.expr.KExpr
 import io.ksmt.expr.KFp64Value
 import io.ksmt.expr.printer.ExpressionPrinter
 import io.ksmt.expr.transformer.KTransformerBase
@@ -49,6 +50,29 @@ class TsUnresolvedSort(ctx: TsContext) : USort(ctx) {
     }
 }
 
+class TsVoidValue(ctx: TsContext) : UExpr<TsVoidSort>(ctx) {
+    override val sort: TsVoidSort
+        get() = tctx.voidSort
+
+    override fun accept(transformer: KTransformerBase): KExpr<TsVoidSort> = this
+
+    override fun print(printer: ExpressionPrinter) {
+        printer.append("void")
+    }
+
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other)
+
+    override fun internHashCode(): Int = hash()
+}
+
+class TsVoidSort(ctx: TsContext) : USort(ctx) {
+    override fun <T> accept(visitor: KSortVisitor<T>): T = error("Should not be called")
+
+    override fun print(builder: StringBuilder) {
+        builder.append("void sort")
+    }
+}
+
 fun UExpr<out USort>.toConcreteBoolValue(): Boolean = when (this) {
     ctx.trueExpr -> true
     ctx.falseExpr -> false