Undefined and null values support (#248)

---------

Co-authored-by: Konstantin Chukharev <[email protected]>

usvm-ts/src/main/kotlin/org/usvm/api/TSTest.kt

@@ -50,4 +50,8 @@ sealed interface TSObject {
     data class TSObject(val addr: Int) : org.usvm.api.TSObject
 
     data object TSUnknown : org.usvm.api.TSObject
+
+    data object TSNull : org.usvm.api.TSObject
+
+    data object TSException : org.usvm.api.TSObject
 }

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

@@ -2,9 +2,11 @@ package org.usvm.machine
 
 import io.ksmt.sort.KFp64Sort
 import org.jacodb.ets.base.EtsBooleanType
+import org.jacodb.ets.base.EtsNullType
 import org.jacodb.ets.base.EtsNumberType
 import org.jacodb.ets.base.EtsRefType
 import org.jacodb.ets.base.EtsType
+import org.jacodb.ets.base.EtsUndefinedType
 import org.jacodb.ets.base.EtsUnknownType
 import org.jacodb.ets.model.EtsScene
 import org.usvm.UAddressSort
@@ -41,6 +43,8 @@ class TSContext(
         is EtsBooleanType -> boolSort
         is EtsNumberType -> fp64Sort
         is EtsRefType -> addressSort
+        is EtsNullType -> addressSort
+        is EtsUndefinedType -> addressSort
         is EtsUnknownType -> unresolvedSort
         else -> TODO("Support all JacoDB types, encountered $type")
     }
@@ -61,6 +65,9 @@ class TSContext(
 
     fun mkUndefinedValue(): UExpr<UAddressSort> = undefinedValue
 
+    fun mkTSNullValue(): UConcreteHeapRef = nullValue
+    private val nullValue: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())
+
     fun getIntermediateBoolLValue(addr: Int): UFieldLValue<IntermediateLValueField, UBoolSort> {
         return UFieldLValue(boolSort, mkConcreteHeapRef(addr), IntermediateLValueField.BOOL)
     }

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

@@ -38,6 +38,7 @@ import org.jacodb.ets.base.EtsNewExpr
 import org.jacodb.ets.base.EtsNotEqExpr
 import org.jacodb.ets.base.EtsNotExpr
 import org.jacodb.ets.base.EtsNullConstant
+import org.jacodb.ets.base.EtsNullType
 import org.jacodb.ets.base.EtsNullishCoalescingExpr
 import org.jacodb.ets.base.EtsNumberConstant
 import org.jacodb.ets.base.EtsNumberType
@@ -55,6 +56,7 @@ import org.jacodb.ets.base.EtsStaticFieldRef
 import org.jacodb.ets.base.EtsStrictEqExpr
 import org.jacodb.ets.base.EtsStrictNotEqExpr
 import org.jacodb.ets.base.EtsStringConstant
+import org.jacodb.ets.base.EtsStringType
 import org.jacodb.ets.base.EtsSubExpr
 import org.jacodb.ets.base.EtsTernaryExpr
 import org.jacodb.ets.base.EtsThis
@@ -72,6 +74,7 @@ import org.jacodb.ets.model.EtsMethodSignature
 import org.usvm.UAddressSort
 import org.usvm.UBoolSort
 import org.usvm.UExpr
+import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.api.makeSymbolicPrimitive
 import org.usvm.collection.field.UFieldLValue
@@ -80,13 +83,15 @@ import org.usvm.machine.interpreter.TSStepScope
 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.localsCount
 import org.usvm.machine.state.newStmt
 import org.usvm.machine.types.FakeType
 import org.usvm.machine.types.mkFakeValue
 import org.usvm.memory.ULValue
 import org.usvm.memory.URegisterStackLValue
 import org.usvm.util.fieldLookUp
+import org.usvm.util.throwExceptionWithoutStackFrameDrop
 
 private val logger = KotlinLogging.logger {}
 
@@ -354,8 +359,7 @@ class TSExprResolver(
     }
 
     override fun visit(expr: EtsStrictEqExpr): UExpr<out USort>? {
-        logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
+        return resolveBinaryOperator(TSBinaryOperator.StrictEq, expr)
     }
 
     override fun visit(expr: EtsStrictNotEqExpr): UExpr<out USort>? {
@@ -499,8 +503,28 @@ class TSExprResolver(
         error("Not supported $value")
     }
 
+    private fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
+        val neqNull = mkAnd(
+            mkHeapRefEq(instance, ctx.mkUndefinedValue()).not(),
+            mkHeapRefEq(instance, ctx.mkTSNullValue()).not()
+        )
+
+        scope.fork(
+            neqNull,
+            blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
+        )
+    }
+
+    private fun allocateException(type: EtsType): (TSState) -> Unit = { state ->
+        val address = state.memory.allocConcrete(type)
+        state.throwExceptionWithoutStackFrameDrop(address, type)
+    }
+
     override fun visit(value: EtsInstanceFieldRef): UExpr<out USort>? = with(ctx) {
         val instanceRef = resolve(value.instance)?.asExpr(addressSort) ?: return null
+
+        checkUndefinedOrNullPropertyRead(instanceRef) ?: return null
+
         // TODO: checkNullPointer(instanceRef)
         val fieldType = scene.fieldLookUp(value.field).type
         val sort = typeToSort(fieldType)
@@ -639,13 +663,11 @@ class TSSimpleValueResolver(
     }
 
     override fun visit(value: EtsNullConstant): UExpr<out USort> = with(ctx) {
-        // TODO: replace with `ctx.nullConstant` (!= nullRef)
-        nullRef
+        mkTSNullValue()
     }
 
     override fun visit(value: EtsUndefinedConstant): UExpr<out USort> = with(ctx) {
-        // TODO: replace with `ctx.nullRef` or `ctx.undefinedConstant` (== nullRef)
-        nullRef
+        mkUndefinedValue()
     }
 
     override fun visit(value: EtsArrayAccess): UExpr<out USort> = with(ctx) {

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt

@@ -8,6 +8,7 @@ import org.jacodb.ets.base.EtsGotoStmt
 import org.jacodb.ets.base.EtsIfStmt
 import org.jacodb.ets.base.EtsLocal
 import org.jacodb.ets.base.EtsNopStmt
+import org.jacodb.ets.base.EtsNullType
 import org.jacodb.ets.base.EtsParameterRef
 import org.jacodb.ets.base.EtsReturnStmt
 import org.jacodb.ets.base.EtsStmt
@@ -208,6 +209,8 @@ class TSInterpreter(
         state.memory.stack.push(method.parametersWithThisCount, method.localsCount)
         state.newStmt(method.cfg.instructions.first())
 
+        state.memory.types.allocate(ctx.mkTSNullValue().address, EtsNullType)
+
         return state
     }
 

usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt

@@ -186,6 +186,7 @@ sealed interface TSBinaryOperator {
                                     )
                                 )
 
+                                scope.assert(lhsType.fpTypeExpr or lhsType.boolTypeExpr)
                                 // TODO: support objects
                             }
 
@@ -206,6 +207,7 @@ sealed interface TSBinaryOperator {
                                     )
                                 )
 
+                                scope.assert(lhsType.fpTypeExpr or lhsType.boolTypeExpr)
                                 // TODO: support objects
                             }
 
@@ -218,6 +220,7 @@ sealed interface TSBinaryOperator {
                                     )
                                 )
 
+                                scope.assert(lhsType.refTypeExpr)
                                 // TODO: support objects
                             }
 
@@ -250,6 +253,7 @@ sealed interface TSBinaryOperator {
                                     )
                                 )
 
+                                scope.assert(rhsType.fpTypeExpr or rhsType.boolTypeExpr)
                                 // TODO: support objects
                             }
 
@@ -270,6 +274,7 @@ sealed interface TSBinaryOperator {
                                     )
                                 )
 
+                                scope.assert(rhsType.fpTypeExpr or rhsType.boolTypeExpr)
                                 // TODO: support objects
                             }
 
@@ -282,6 +287,7 @@ sealed interface TSBinaryOperator {
                                     )
                                 )
 
+                                scope.assert(rhsType.refTypeExpr)
                                 // TODO: support objects
 
                             }
@@ -330,7 +336,6 @@ sealed interface TSBinaryOperator {
 
             TODO("Unsupported String and bigint comparison")
         }
-
     }
 
     data object Neq : TSBinaryOperator {
@@ -385,6 +390,52 @@ sealed interface TSBinaryOperator {
         }
     }
 
+    data object StrictEq : TSBinaryOperator {
+        override fun TSContext.onBool(
+            lhs: UExpr<UBoolSort>,
+            rhs: UExpr<UBoolSort>,
+            scope: TSStepScope,
+        ): UExpr<out USort> {
+            return mkEq(lhs, rhs)
+        }
+
+        override fun TSContext.onFp(
+            lhs: UExpr<KFp64Sort>,
+            rhs: UExpr<KFp64Sort>,
+            scope: TSStepScope,
+        ): UExpr<out USort> {
+            return mkFpEqualExpr(lhs, rhs)
+        }
+
+        override fun TSContext.onRef(
+            lhs: UExpr<UAddressSort>,
+            rhs: UExpr<UAddressSort>,
+            scope: TSStepScope,
+        ): UExpr<out USort> {
+            TODO("Not yet implemented")
+        }
+
+        override fun TSContext.resolveFakeObject(
+            lhs: UExpr<out USort>,
+            rhs: UExpr<out USort>,
+            scope: TSStepScope,
+        ): UExpr<out USort> {
+            check(lhs.isFakeObject() || rhs.isFakeObject())
+            // TODO: delegating to '==' is not correct in general case
+            return with(Eq) {
+                resolveFakeObject(lhs, rhs, scope)
+            }
+        }
+
+        override fun TSContext.internalResolve(
+            lhs: UExpr<out USort>,
+            rhs: UExpr<out USort>,
+            scope: TSStepScope,
+        ): UExpr<out USort> {
+            TODO("Not yet implemented")
+        }
+    }
+
     data object Add : TSBinaryOperator {
         override fun TSContext.onBool(
             lhs: UExpr<UBoolSort>,

usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt

@@ -1,11 +1,15 @@
 package org.usvm.util
 
 import io.ksmt.sort.KFp64Sort
+import org.jacodb.ets.base.EtsType
 import org.jacodb.ets.model.EtsFieldSignature
 import org.jacodb.ets.model.EtsScene
 import org.usvm.UBoolSort
 import org.usvm.UExpr
+import org.usvm.UHeapRef
 import org.usvm.machine.TSContext
+import org.usvm.machine.state.TSMethodResult
+import org.usvm.machine.state.TSState
 
 // Built-in KContext.bvToBool has identical implementation.
 fun TSContext.boolToFp(expr: UExpr<UBoolSort>): UExpr<KFp64Sort> =
@@ -16,4 +20,8 @@ fun TSContext.boolToFp(expr: UExpr<UBoolSort>): UExpr<KFp64Sort> =
 fun EtsScene.fieldLookUp(field: EtsFieldSignature) = projectAndSdkClasses
     .first { it.signature == field.enclosingClass }
     .fields
-    .single { it.name == field.name }
+    .single { it.name == field.name }
+
+fun TSState.throwExceptionWithoutStackFrameDrop(address: UHeapRef, type: EtsType) {
+    methodResult = TSMethodResult.TSException(address, type)
+}

usvm-ts/src/test/kotlin/org/usvm/samples/InstanceFields.kt

@@ -19,46 +19,65 @@ class InstanceFields : TSMethodTestRunner() {
     @Test
     fun testReturnSingleField() {
         val method = getMethod("InstanceFields", "returnSingleField")
-        discoverProperties<TSObject.TSClass, TSObject.TSNumber>(
+        discoverProperties<TSObject, TSObject>(
             method,
             { x, r ->
                 // Note: this is an attempt to represent `r == x["a"]`
+                if (x !is TSObject.TSClass || r !is TSObject.TSNumber) return@discoverProperties false
+
                 val xa = x.properties["a"] as TSObject.TSNumber
                 xa.number == r.number || (xa.number.isNaN() && r.number.isNaN())
             },
+            { x, r ->
+                (x is TSObject.TSUndefinedObject || x is TSObject.TSNull) && r is TSObject.TSException
+            }
         )
     }
 
     @Test
     fun testDispatchOverField() {
         val method = getMethod("InstanceFields", "dispatchOverField")
-        discoverProperties<TSObject.TSClass, TSObject.TSNumber>(
+        discoverProperties<TSObject, TSObject>(
             method,
             { x, r ->
+                if (x !is TSObject.TSClass || r !is TSObject.TSNumber) return@discoverProperties false
+
                 val xa = x.properties["a"] as TSObject.TSNumber
                 xa.number == 1.0 && r.number == 1.0
             },
             { x, r ->
+                if (x !is TSObject.TSClass || r !is TSObject.TSNumber) return@discoverProperties false
+
                 val xa = x.properties["a"] as TSObject.TSNumber
                 xa.number == 2.0 && r.number == 2.0
             },
             { x, r ->
+                if (x !is TSObject.TSClass || r !is TSObject.TSNumber) return@discoverProperties false
+
                 val xa = x.properties["a"] as TSObject.TSNumber
                 xa.number != 1.0 && xa.number != 2.0 && r.number == 100.0
             },
+            { x, r ->
+                (x is TSObject.TSUndefinedObject || x is TSObject.TSNull) && r is TSObject.TSException
+            }
         )
     }
 
     @Test
     fun testReturnSumOfTwoFields() {
         val method = getMethod("InstanceFields", "returnSumOfTwoFields")
-        discoverProperties<TSObject.TSClass, TSObject.TSNumber>(
+        discoverProperties<TSObject, TSObject>(
             method,
             { x, r ->
+                if (x !is TSObject.TSClass || r !is TSObject.TSNumber) return@discoverProperties false
+
                 val xa = x.properties["a"] as TSObject.TSNumber
                 val xb = x.properties["b"] as TSObject.TSNumber
                 xa.number + xb.number == r.number
             },
+            { x, r ->
+                (x is TSObject.TSUndefinedObject || x is TSObject.TSNull) && r is TSObject.TSException
+            }
         )
     }
 }

usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt

@@ -0,0 +1,28 @@
+package org.usvm.samples
+
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.junit.jupiter.api.RepeatedTest
+import org.usvm.api.TSObject
+import org.usvm.util.TSMethodTestRunner
+import org.usvm.util.getResourcePath
+
+class Null : TSMethodTestRunner() {
+
+    override val scene = run {
+        val name = "Null.ts"
+        val path = getResourcePath("/samples/$name")
+        val file = loadEtsFileAutoConvert(path)
+        EtsScene(listOf(file))
+    }
+
+    @RepeatedTest(20)
+    fun testIsNull() {
+        val method = getMethod("Null", "isNull")
+        discoverProperties<TSObject, TSObject.TSNumber>(
+            method,
+            { a, r -> a is TSObject.TSNull && r.number == 1.0 },
+            { a, r -> a !is TSObject.TSNull && r.number == 2.0 },
+        )
+    }
+}