Division and remainder operator

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

@@ -91,7 +91,19 @@ fun TsContext.mkTruthyExpr(
 fun TsContext.mkNumericExpr(
     expr: UExpr<out USort>,
     scope: TsStepScope,
-): UExpr<KFp64Sort> = scope.calcOnState {
+): UExpr<KFp64Sort> {
+    if (expr.isFakeObject()) {
+        val type = expr.getFakeType(scope)
+        return mkIte(
+            condition = type.fpTypeExpr,
+            trueBranch = expr.extractFp(scope),
+            falseBranch = mkIte(
+                condition = type.boolTypeExpr,
+                trueBranch = mkNumericExpr(expr.extractBool(scope), scope),
+                falseBranch = mkNumericExpr(expr.extractRef(scope), scope)
+            )
+        )
+    }
 
     // 7.1.4 ToNumber ( argument )
     //
@@ -107,27 +119,27 @@ fun TsContext.mkNumericExpr(
     // 10. Return ToNumber(primValue).
 
     if (expr.sort == fp64Sort) {
-        return@calcOnState expr.asExpr(fp64Sort)
+        return expr.asExpr(fp64Sort)
     }
 
     if (expr == mkUndefinedValue()) {
-        return@calcOnState mkFp64NaN()
+        return mkFp64NaN()
     }
 
     if (expr == mkTsNullValue()) {
-        return@calcOnState mkFp64(0.0)
+        return mkFp64(0.0)
     }
 
     if (expr.sort == boolSort) {
-        return@calcOnState boolToFp(expr.asExpr(boolSort))
+        return boolToFp(expr.asExpr(boolSort))
     }
 
     // TODO: ToPrimitive, then ToNumber again
     // TODO: probably we need to implement Object (Ref/Fake) -> Number conversion here directly, without ToPrimitive
 
     // TODO incorrect implementation, returns some number that is not equal to 0 and NaN
     //      https://github.com/UnitTestBot/usvm/issues/280
-    return@calcOnState mkIte(
+    return mkIte(
         condition = mkEq(expr.asExpr(addressSort), mkTsNullValue()),
         trueBranch = mkFp(0.0, fp64Sort),
         falseBranch = mkIte(

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

@@ -332,13 +332,11 @@ class TsExprResolver(
     }
 
     override fun visit(expr: EtsDivExpr): UExpr<out USort>? {
-        logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
+        return resolveBinaryOperator(TsBinaryOperator.Div, expr)
     }
 
     override fun visit(expr: EtsRemExpr): UExpr<out USort>? {
-        logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
+        return resolveBinaryOperator(TsBinaryOperator.Rem, expr)
     }
 
     override fun visit(expr: EtsExpExpr): UExpr<out USort>? {

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

@@ -1217,7 +1217,7 @@ sealed interface TsBinaryOperator {
             lhs: UBoolExpr,
             rhs: UBoolExpr,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<KFp64Sort> {
             val left = mkNumericExpr(lhs, scope)
             val right = mkNumericExpr(rhs, scope)
             return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
@@ -1227,15 +1227,15 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<KFp64Sort>,
             rhs: UExpr<KFp64Sort>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<KFp64Sort> {
             return mkFpMulExpr(fpRoundingModeSortDefaultValue(), lhs, rhs)
         }
 
         override fun TsContext.onRef(
             lhs: UHeapRef,
             rhs: UHeapRef,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<KFp64Sort> {
             val left = mkNumericExpr(lhs, scope)
             val right = mkNumericExpr(rhs, scope)
             return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
@@ -1245,7 +1245,7 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<KFp64Sort> {
             check(lhs.isFakeObject() || rhs.isFakeObject())
             val left = mkNumericExpr(lhs, scope)
             val right = mkNumericExpr(rhs, scope)
@@ -1256,11 +1256,105 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<KFp64Sort> {
             check(!lhs.isFakeObject() && !rhs.isFakeObject())
             val left = mkNumericExpr(lhs, scope)
             val right = mkNumericExpr(rhs, scope)
             return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
         }
     }
+
+    data object Div : TsBinaryOperator {
+        override fun TsContext.onBool(
+            lhs: UBoolExpr,
+            rhs: UBoolExpr,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            val left = mkNumericExpr(lhs, scope)
+            val right = mkNumericExpr(rhs, scope)
+            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
+        }
+
+        override fun TsContext.onFp(
+            lhs: UExpr<KFp64Sort>,
+            rhs: UExpr<KFp64Sort>,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), lhs, rhs)
+        }
+
+        override fun TsContext.onRef(
+            lhs: UHeapRef,
+            rhs: UHeapRef,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            val left = mkNumericExpr(lhs, scope)
+            val right = mkNumericExpr(rhs, scope)
+            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
+        }
+
+        override fun TsContext.resolveFakeObject(
+            lhs: UExpr<*>,
+            rhs: UExpr<*>,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            val left = mkNumericExpr(lhs, scope)
+            val right = mkNumericExpr(rhs, scope)
+            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
+        }
+
+        override fun TsContext.internalResolve(
+            lhs: UExpr<*>,
+            rhs: UExpr<*>,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            val left = mkNumericExpr(lhs, scope)
+            val right = mkNumericExpr(rhs, scope)
+            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
+        }
+    }
+
+    data object Rem : TsBinaryOperator {
+        override fun TsContext.onBool(
+            lhs: UBoolExpr,
+            rhs: UBoolExpr,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            return internalResolve(lhs, rhs, scope)
+        }
+
+        override fun TsContext.onFp(
+            lhs: UExpr<KFp64Sort>,
+            rhs: UExpr<KFp64Sort>,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            return internalResolve(lhs, rhs, scope)
+        }
+
+        override fun TsContext.onRef(
+            lhs: UHeapRef,
+            rhs: UHeapRef,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            return internalResolve(lhs, rhs, scope)
+        }
+
+        override fun TsContext.resolveFakeObject(
+            lhs: UExpr<*>,
+            rhs: UExpr<*>,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            return internalResolve(lhs, rhs, scope)
+        }
+
+        override fun TsContext.internalResolve(
+            lhs: UExpr<*>,
+            rhs: UExpr<*>,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            val lhsExpr = mkNumericExpr(lhs, scope)
+            val rhsExpr = mkNumericExpr(rhs, scope)
+            return mkFpRemExpr(lhsExpr, rhsExpr)
+        }
+    }
 }

usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt

@@ -119,11 +119,12 @@ class InputArrays : TsMethodTestRunner() {
             method = method,
             { x, r ->
                 val value = x.values[0]
-                value is TsTestValue.TsNumber && value.number == 1.0 && r is TsTestValue.TsNull },
+                value is TsTestValue.TsNumber && value.number == 1.0 && r is TsTestValue.TsNull
+            },
             { x, r ->
                 val value = x.values[0]
                 value !is TsTestValue.TsNumber || value.number != 1.0 && r == value
             },
         )
     }
-}
+}

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

@@ -0,0 +1,64 @@
+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 Division : TsMethodTestRunner() {
+    private val className = this::class.simpleName!!
+
+    override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
+
+    @Test
+    fun testTwoNumbersDivision() {
+        val method = getMethod(className, "twoNumbersDivision")
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> a.number / b.number == 4.0 && r.number == 4.0 },
+            { a, b, r -> a.number / b.number == Double.POSITIVE_INFINITY && r.number == Double.POSITIVE_INFINITY },
+            { a, b, r -> a.number / b.number == Double.NEGATIVE_INFINITY && r.number == Double.NEGATIVE_INFINITY },
+            { a, b, r -> (a.number / b.number).isNaN() && r.number.isNaN() },
+            { a, b, r -> a.number / b.number != 4.0 && r.number == a.number / b.number }
+        )
+    }
+
+    @Test
+    fun testBooleanDivision() {
+        val method = getMethod(className, "booleanDivision")
+        discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> a.value.toDouble() / b.value.toDouble() == 0.0 && r.number == 0.0 },
+            { a, b, r ->
+                a.value.toDouble() / b.value.toDouble() != 0.0 && (r.number == (a.value.toDouble() / b.value.toDouble()) || r.number.isNaN())
+            }
+        )
+    }
+
+    @Test
+    fun testMixedDivision() {
+        val method = getMethod(className, "mixedDivision")
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> a.number / b.value.toDouble() == 4.0 && r.number == 4.0 },
+            { a, b, r -> a.number / b.value.toDouble() == Double.POSITIVE_INFINITY && r.number == Double.POSITIVE_INFINITY },
+            { a, b, r -> a.number / b.value.toDouble() == Double.NEGATIVE_INFINITY && r.number == Double.NEGATIVE_INFINITY },
+            { a, b, r -> (a.number / b.value.toDouble()).isNaN() && r.number.isNaN() },
+            { a, b, r -> a.number / b.value.toDouble() != 4.0 && r.number == a.number / b.value.toDouble() }
+        )
+    }
+
+    @Test
+    fun testUnknownDivision() {
+        val method = getMethod(className, "unknownDivision")
+        discoverProperties<TsTestValue, TsTestValue, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> (a is TsTestValue.TsUndefined || b is TsTestValue.TsUndefined) && r.number.isNaN() },
+            { _, _, r -> r.number == 4.0 },
+            { _, _, r -> r.number == Double.POSITIVE_INFINITY },
+            { _, _, r -> r.number == Double.NEGATIVE_INFINITY },
+            { _, _, r -> r.number.isNaN() },
+        )
+    }
+}

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

@@ -0,0 +1,80 @@
+package org.usvm.samples.operators
+
+import org.junit.jupiter.api.Disabled
+import org.junit.jupiter.api.Test
+import org.usvm.api.TsTestValue
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.toDouble
+
+class Remainder : TsMethodTestRunner() {
+    private val className = this::class.simpleName!!
+
+    override val scene = loadSampleScene(className, folderPrefix = "operators")
+
+    @Test
+    @Disabled("Never ends")
+    fun testTwoNumbersRemainder() {
+        val method = getMethod(className, "twoNumbersRemainder")
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r ->
+                val res = a.number % b.number
+                res != res && (a.number.isNaN() || b.number.isNaN())
+            },
+            { a, b, r ->
+                val res = a.number % b.number
+                res != res && (a.number == Double.POSITIVE_INFINITY || a.number == Double.NEGATIVE_INFINITY)
+            },
+            { a, b, r -> a.number == 0.0 && b.number == 0.0 && r.number.isNaN() },
+            { a, b, r ->
+                b.number == 0.0 && a.number != 0.0 && r.number.isNaN()
+            },
+            { a, b, r ->
+                (b.number == Double.POSITIVE_INFINITY || b.number == Double.NEGATIVE_INFINITY) && r.number == a.number
+            },
+            { a, b, r -> a.number == 0.0 && r.number == a.number },
+            { a, b, r -> a.number % b.number == 4.0 && r.number == 4.0 },
+            { a, b, r ->
+                val res = a.number % b.number
+                !res.isNaN() && res != 4.0 && r.number == res
+            },
+        )
+    }
+
+    @Test
+    fun testBooleanRemainder() {
+        val method = getMethod(className, "booleanRemainder")
+        discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> a.value.toDouble() % b.value.toDouble() == 0.0 && r.number == 0.0 },
+            { a, b, r ->
+                a.value.toDouble() % b.value.toDouble() != 0.0 && (r.number == (a.value.toDouble() % b.value.toDouble()) || r.number.isNaN())
+            }
+        )
+    }
+
+    @Test
+    @Disabled("Wrong result")
+    fun testMixedRemainder() {
+        val method = getMethod(className, "mixedRemainder")
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> a.number % b.value.toDouble() == 4.0 && r.number == 4.0 },
+            { a, b, r -> (a.number % b.value.toDouble()).isNaN() && r.number.isNaN() },
+            { a, b, r -> a.number % b.value.toDouble() != 4.0 && r.number == a.number % b.value.toDouble() }
+        )
+    }
+
+    @Test
+    @Disabled("Never ends")
+    fun testUnknownRemainder() {
+        val method = getMethod(className, "unknownRemainder")
+        discoverProperties<TsTestValue, TsTestValue, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> (a is TsTestValue.TsUndefined || b is TsTestValue.TsUndefined) && r.number.isNaN() },
+            { _, _, r -> r.number == 4.0 },
+            { _, _, r -> r.number.isNaN() },
+            { _, _, r -> !r.number.isNaN() && r.number != 4.0 }
+        )
+    }
+}

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

@@ -18,6 +18,7 @@ import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.junit.jupiter.api.TestInstance
 import org.junit.jupiter.api.TestInstance.Lifecycle.PER_CLASS
 import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
 import org.usvm.UMachineOptions
 import org.usvm.api.NoCoverage
 import org.usvm.api.TsMethodCoverage
@@ -343,6 +344,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
         exceptionsPropagation = true,
         timeout = Duration.INFINITE,
         stepsFromLastCovered = 3500L,
+        solverType = SolverType.YICES,
         solverTimeout = Duration.INFINITE, // we do not need the timeout for a solver in tests
         typeOperationsTimeout = Duration.INFINITE, // we do not need the timeout for type operations in tests
     )