Add operator

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

@@ -125,5 +125,15 @@ fun TsContext.mkNumericExpr(
     // TODO: ToPrimitive, then ToNumber again
     // TODO: probably we need to implement Object (Ref/Fake) -> Number conversion here directly, without ToPrimitive
 
-    error("Unsupported sort: ${expr.sort}")
+    // TODO incorrect implementation, returns some number that is not equal to 0 and NaN
+    //      https://github.com/UnitTestBot/usvm/issues/280
+    return@calcOnState mkIte(
+        condition = mkEq(expr.asExpr(addressSort), mkTsNullValue()),
+        trueBranch = mkFp(0.0, fp64Sort),
+        falseBranch = mkIte(
+            mkEq(expr.asExpr(addressSort), mkUndefinedValue()),
+            mkFp64NaN(),
+            mkFp64NaN()
+        )
+    )
 }

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

@@ -49,7 +49,7 @@ class TsUnresolvedSort(ctx: TsContext) : USort(ctx) {
     }
 }
 
-fun UExpr<out USort>.extractBool(): Boolean = when (this) {
+fun UExpr<out USort>.toConcreteBoolValue(): Boolean = when (this) {
     ctx.trueExpr -> true
     ctx.falseExpr -> false
     else -> error("Cannot extract boolean from $this")

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

@@ -77,8 +77,8 @@ class FieldAccess : TsMethodTestRunner() {
                 x.number == 1.1 && r.number == 14.0
             },
             { a, r ->
-                val x = a.properties["x"] as TsTestValue.TsNumber
-                x.number != 1.1 && r.number == 10.0
+                val x = a.properties["x"] as? TsTestValue.TsNumber
+                x?.number != 1.1 && r.number == 10.0
             },
         )
     }

usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt

@@ -0,0 +1,96 @@
+package org.usvm.samples.operators
+
+import org.jacodb.ets.model.EtsScene
+import org.usvm.api.TsTestValue
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.toDouble
+import kotlin.test.Test
+
+class Add : TsMethodTestRunner() {
+    private val className = this::class.simpleName!!
+
+    override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
+
+    @Test
+    fun `bool + bool`() {
+        val method = getMethod(className, "addBoolAndBool")
+        discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> r.number == 1.0 && !a.value && !b.value },
+            { a, b, r -> r.number == 2.0 && !a.value && b.value },
+            { a, b, r -> r.number == 3.0 && a.value && !b.value },
+            { a, b, r -> r.number == 4.0 && a.value && b.value },
+            invariants = arrayOf(
+                { _, _, r -> r.number != -1.0 }
+            )
+        )
+    }
+
+    @Test
+    fun `bool + number`() {
+        val method = getMethod(className, "addBoolAndNumber")
+        discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> r.number == 1.0 && a.value && b.number == -1.0 },
+            { a, b, r -> r.number == 2.0 && !a.value && b.number == 0.0 },
+            { a, b, r -> r.number == 3.0 && a.value && b.number == 5.0 },
+            { _, b, r -> r.number.isNaN() && b.number.isNaN() },
+            { a, b, r ->
+                val result = a.value.toDouble() + b.number
+                r.number == 4.0 && result != 2.2 && !result.isNaN()
+            }
+        )
+    }
+
+    @Test
+    fun `number + number`() {
+        val method = getMethod(className, "addNumberAndNumber")
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> a.number.isNaN() && r.number.isNaN() },
+            { a, b, r -> !a.number.isNaN() && b.number.isNaN() && r.number.isNaN() },
+            { a, b, r -> a.number + b.number == r.number },
+            { a, b, r -> !a.number.isNaN() && !b.number.isNaN() && r.number == 0.0 },
+        )
+    }
+
+    @Test
+    fun `number + undefined`() {
+        val method = getMethod(className, "addNumberAndUndefined")
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = method,
+            invariants = arrayOf(
+                { a, r -> r.number != -1.0 },
+            )
+        )
+    }
+
+    @Test
+    fun `number + null`() {
+        val method = getMethod(className, "addNumberAndNull")
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = method,
+            { a, r -> a.number.isNaN() && r.number.isNaN() },
+            { a, r -> !a.number.isNaN() && r.number == a.number },
+        )
+    }
+
+    @Test
+    fun `add unknown values`() {
+        val method = getMethod(className, "addUnknownValues")
+        discoverProperties<TsTestValue, TsTestValue, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> a is TsTestValue.TsUndefined || b is TsTestValue.TsUndefined && r.number.isNaN() },
+            { a, b, r ->
+                (a is TsTestValue.TsClass
+                    || b is TsTestValue.TsClass
+                    || (a as? TsTestValue.TsNumber)?.number?.isNaN() == true
+                    || (b as? TsTestValue.TsNumber)?.number?.isNaN() == true)
+                    && r.number.isNaN()
+            },
+            { a, b, r -> r.number == 7.0 },
+            { a, b, r -> a is TsTestValue.TsNull && b is TsTestValue.TsNull && r.number == 0.0 },
+            { a, b, r -> r.number == 42.0 }
+        )
+    }
+}

usvm-ts/src/test/kotlin/org/usvm/samples/And.kt → usvm-ts/src/test/kotlin/org/usvm/samples/operators/And.kt

@@ -1,4 +1,4 @@
-package org.usvm.samples
+package org.usvm.samples.operators
 
 import org.jacodb.ets.dsl.and
 import org.jacodb.ets.dsl.const
@@ -28,7 +28,7 @@ class And : TsMethodTestRunner() {
 
     private val className = this::class.simpleName!!
 
-    override val scene: EtsScene = loadSampleScene(className)
+    override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
 
     private val classSignature: EtsClassSignature =
         scene.projectFiles[0].classes.single { it.name != DEFAULT_ARK_CLASS_NAME }.signature

usvm-ts/src/test/kotlin/org/usvm/samples/Equality.kt → usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt

@@ -1,4 +1,4 @@
-package org.usvm.samples
+package org.usvm.samples.operators
 
 import org.jacodb.ets.model.EtsScene
 import org.junit.jupiter.api.Disabled
@@ -10,7 +10,7 @@ class Equality : TsMethodTestRunner() {
 
     private val className = this::class.simpleName!!
 
-    override val scene: EtsScene = loadSampleScene(className)
+    override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
 
     @Test
     fun `test eqBoolWithBool`() {

usvm-ts/src/test/kotlin/org/usvm/samples/Neg.kt → usvm-ts/src/test/kotlin/org/usvm/samples/operators/Neg.kt

@@ -1,4 +1,4 @@
-package org.usvm.samples
+package org.usvm.samples.operators
 
 import org.jacodb.ets.model.EtsScene
 import org.junit.jupiter.api.Test
@@ -9,7 +9,7 @@ class Neg : TsMethodTestRunner() {
 
     private val className = this::class.simpleName!!
 
-    override val scene: EtsScene = loadSampleScene(className)
+    override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
 
     @Test
     fun `test negateNumber`() {

usvm-ts/src/test/kotlin/org/usvm/samples/Or.kt → usvm-ts/src/test/kotlin/org/usvm/samples/operators/Or.kt

@@ -1,4 +1,4 @@
-package org.usvm.samples
+package org.usvm.samples.operators
 
 import org.jacodb.ets.dsl.const
 import org.jacodb.ets.dsl.eq
@@ -26,7 +26,7 @@ class Or : TsMethodTestRunner() {
 
     private val className = this::class.simpleName!!
 
-    override val scene: EtsScene = loadSampleScene(className)
+    override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
 
     private val classSignature: EtsClassSignature =
         scene.projectFiles[0].classes.single { it.name != DEFAULT_ARK_CLASS_NAME }.signature

usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt

@@ -34,8 +34,8 @@ import org.usvm.api.typeStreamOf
 import org.usvm.isTrue
 import org.usvm.machine.TsContext
 import org.usvm.machine.expr.TsUnresolvedSort
-import org.usvm.machine.expr.extractBool
 import org.usvm.machine.expr.extractDouble
+import org.usvm.machine.expr.toConcreteBoolValue
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
 import org.usvm.memory.ULValue
@@ -306,7 +306,7 @@ open class TsTestStateResolver(
                 }
             }
 
-            EtsBooleanType -> TsTestValue.TsBoolean(evaluateInModel(expr).extractBool())
+            EtsBooleanType -> TsTestValue.TsBoolean(evaluateInModel(expr).toConcreteBoolValue())
             EtsUndefinedType -> TsTestValue.TsUndefined
             is EtsLiteralType -> TODO()
             EtsNullType -> TODO()

usvm-ts/src/test/kotlin/org/usvm/util/Util.kt

@@ -0,0 +1,3 @@
+package org.usvm.util
+
+fun Boolean.toDouble() = if (this) 1.0 else 0.0

usvm-ts/src/test/resources/samples/operators/Add.ts

@@ -0,0 +1,71 @@
+class Add {
+    addBoolAndBool(a: boolean, b: boolean): number {
+        res = a + b;
+
+        if (res == 0 && (a || b)) return -1 // unreachable
+        if (res < 0 || res > 2) return -1 // unreachable
+        if (res == 1 && a && b) return -1 // unreachable
+        if (res == 2 && !(a && b)) return -1 // unreachable
+
+        if (res == 0) return 1 // false false
+        if (res == 1 && !a) return 2 // false true
+        if (res == 1 && !b) return 3 // true false
+        if (res == 2) return 4 // true true
+
+        return -1 // unreachable
+    }
+
+    addBoolAndNumber(a: boolean, b: number): number {
+        res = a + b;
+
+        if (res == 0 && a) return 1 // true -1
+        if (res == 0 && !a) return 2 // false 0
+
+        if (res == 6 && a) return 3
+
+        if (b != b) return res // _ NaN
+
+        return 4
+    }
+
+    addNumberAndNumber(a: number, b: number): number {
+        res = a + b;
+
+        if (a != a) return res
+        if (b != b) return res
+
+        if (res == 1.1) return res
+
+        return 0
+    }
+
+    addNumberAndUndefined(a: number): number {
+        res = a + undefined;
+
+        if (res == 0) return -1 // unreachable
+
+        return res
+    }
+
+    addNumberAndNull(a: number): number {
+        res = a + null;
+
+        if (res != a) return res
+
+        return res
+    }
+
+    addUnknownValues(a, b) {
+        res = a + b;
+
+        if (a === undefined || b === undefined) return res
+
+        if (res != res) return res
+
+        if (res == 7) return res
+
+        if (a === null && b === null) return res
+
+        return 42
+    }
+}