Handle Number.isNaN (#266)

Author: Lipen

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

@@ -13,18 +13,22 @@ import org.jacodb.ets.base.EtsUnionType
 import org.jacodb.ets.base.EtsUnknownType
 import org.jacodb.ets.model.EtsScene
 import org.usvm.UAddressSort
+import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
 import org.usvm.UBv32Sort
 import org.usvm.UConcreteHeapRef
 import org.usvm.UContext
 import org.usvm.UExpr
+import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.api.typeStreamOf
 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.interpreter.TsStepScope
 import org.usvm.machine.types.FakeType
+import org.usvm.types.UTypeStream
 import org.usvm.types.single
 import org.usvm.util.mkFieldLValue
 import kotlin.contracts.ExperimentalContracts
@@ -44,8 +48,11 @@ class TsContext(
      * In TS we treat undefined value as a null reference in other objects.
      * For real null represented in the language we create another reference.
      */
-    private val undefinedValue: UExpr<UAddressSort>
-        get() = mkNullRef()
+    private val undefinedValue: UExpr<UAddressSort> = mkNullRef()
+    fun mkUndefinedValue(): UExpr<UAddressSort> = undefinedValue
+
+    private val nullValue: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())
+    fun mkTsNullValue(): UConcreteHeapRef = nullValue
 
     fun typeToSort(type: EtsType): USort = when (type) {
         is EtsBooleanType -> boolSort
@@ -59,6 +66,14 @@ class TsContext(
         else -> TODO("Support all JacoDB types, encountered $type")
     }
 
+    fun UHeapRef.getTypeStream(scope: TsStepScope): UTypeStream<EtsType> =
+        scope.calcOnState {
+            memory.typeStreamOf(this@getTypeStream)
+        }
+
+    fun UConcreteHeapRef.getFakeType(scope: TsStepScope): FakeType =
+        getTypeStream(scope).single() as FakeType
+
     @OptIn(ExperimentalContracts::class)
     fun UExpr<out USort>.isFakeObject(): Boolean {
         contract {
@@ -136,22 +151,35 @@ class TsContext(
         return mkConcreteHeapRef(address)
     }
 
-    fun mkUndefinedValue(): UExpr<UAddressSort> = undefinedValue
-
-    fun mkTsNullValue(): UConcreteHeapRef = nullValue
-    private val nullValue: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())
-
     fun getIntermediateBoolLValue(addr: Int): UFieldLValue<IntermediateLValueField, UBoolSort> {
+        require(addr > MAGIC_OFFSET)
         return mkFieldLValue(boolSort, mkConcreteHeapRef(addr), IntermediateLValueField.BOOL)
     }
 
     fun getIntermediateFpLValue(addr: Int): UFieldLValue<IntermediateLValueField, KFp64Sort> {
+        require(addr > MAGIC_OFFSET)
         return mkFieldLValue(fp64Sort, mkConcreteHeapRef(addr), IntermediateLValueField.FP)
     }
 
     fun getIntermediateRefLValue(addr: Int): UFieldLValue<IntermediateLValueField, UAddressSort> {
+        require(addr > MAGIC_OFFSET)
         return mkFieldLValue(addressSort, mkConcreteHeapRef(addr), IntermediateLValueField.REF)
     }
+
+    fun UConcreteHeapRef.extractBool(scope: TsStepScope): UBoolExpr {
+        val lValue = getIntermediateBoolLValue(address)
+        return scope.calcOnState { memory.read(lValue) }
+    }
+
+    fun UConcreteHeapRef.extractFp(scope: TsStepScope): UExpr<KFp64Sort> {
+        val lValue = getIntermediateFpLValue(address)
+        return scope.calcOnState { memory.read(lValue) }
+    }
+
+    fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef {
+        val lValue = getIntermediateRefLValue(address)
+        return scope.calcOnState { memory.read(lValue) }
+    }
 }
 
 const val MAGIC_OFFSET = 1000000

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

@@ -77,6 +77,7 @@ import org.jacodb.ets.model.EtsFieldSignature
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsMethodSignature
 import org.usvm.UAddressSort
+import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
 import org.usvm.UExpr
 import org.usvm.UHeapRef
@@ -404,25 +405,34 @@ class TsExprResolver(
 
     // region CALL
 
+    private fun handleNumberIsNaN(arg: UExpr<out USort>): UBoolExpr? = with(ctx) {
+        // 21.1.2.4 Number.isNaN ( number )
+        // 1. If number is not a Number, return false.
+        // 2. If number is NaN, return true.
+        // 3. Otherwise, return false.
+
+        if (arg.isFakeObject()) {
+            val fakeType = arg.getFakeType(scope)
+            val value = arg.extractFp(scope)
+            return mkIte(
+                condition = fakeType.fpTypeExpr,
+                trueBranch = mkFpIsNaNExpr(value),
+                falseBranch = mkFalse(),
+            )
+        }
+
+        if (arg.sort == fp64Sort) {
+            mkFpIsNaNExpr(arg.asExpr(fp64Sort))
+        } else {
+            mkFalse()
+        }
+    }
+
     override fun visit(expr: EtsInstanceCallExpr): UExpr<out USort>? = with(ctx) {
         if (expr.instance.name == "Number") {
             if (expr.method.name == "isNaN") {
-                val arg = resolve(expr.args.single()) ?: return null
-                if (arg.sort == fp64Sort) {
-                    return mkFpIsNaNExpr(arg.asExpr(fp64Sort))
-                }
-                if (arg.isFakeObject()) {
-                    val fakeType = scope.calcOnState {
-                        memory.types.getTypeStream(arg).single() as FakeType
-                    }
-                    scope.calcOnState {
-                        if (fakeType.fpTypeExpr.isTrue) {
-                            val lValue = getIntermediateFpLValue(arg.address)
-                            val value = memory.read(lValue).asExpr(fp64Sort)
-                            return@calcOnState mkFpIsNaNExpr(value)
-                        }
-                        null
-                    }?.let { return it }
+                return resolveAfterResolved(expr.args.single()) { arg ->
+                    handleNumberIsNaN(arg)
                 }
             }
         }