Skip to content

Commit 97614f7

Browse files
CaelmBleiddCaelmBleidd
committed
Remainder operator
1 parent 69484a8 commit 97614f7

File tree

5 files changed

+198
-2
lines changed

5 files changed

+198
-2
lines changed

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -363,8 +363,7 @@ class TsExprResolver(
363363
}
364364

365365
override fun visit(expr: EtsRemExpr): UExpr<out USort>? {
366-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
367-
error("Not supported $expr")
366+
return resolveBinaryOperator(TsBinaryOperator.Rem, expr)
368367
}
369368

370369
override fun visit(expr: EtsExpExpr): UExpr<out USort>? {

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

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1312,6 +1312,49 @@ sealed interface TsBinaryOperator {
13121312
val right = mkNumericExpr(rhs, scope)
13131313
return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
13141314
}
1315+
}
1316+
1317+
data object Rem : TsBinaryOperator {
1318+
override fun TsContext.onBool(
1319+
lhs: UBoolExpr,
1320+
rhs: UBoolExpr,
1321+
scope: TsStepScope
1322+
): UExpr<*>? {
1323+
return internalResolve(lhs, rhs, scope)
1324+
}
1325+
1326+
override fun TsContext.onFp(
1327+
lhs: UExpr<KFp64Sort>,
1328+
rhs: UExpr<KFp64Sort>,
1329+
scope: TsStepScope
1330+
): UExpr<*>? {
1331+
return internalResolve(lhs, rhs, scope)
1332+
}
13151333

1334+
override fun TsContext.onRef(
1335+
lhs: UHeapRef,
1336+
rhs: UHeapRef,
1337+
scope: TsStepScope
1338+
): UExpr<*>? {
1339+
return internalResolve(lhs, rhs, scope)
1340+
}
1341+
1342+
override fun TsContext.resolveFakeObject(
1343+
lhs: UExpr<*>,
1344+
rhs: UExpr<*>,
1345+
scope: TsStepScope
1346+
): UExpr<*>? {
1347+
return internalResolve(lhs, rhs, scope)
1348+
}
1349+
1350+
override fun TsContext.internalResolve(
1351+
lhs: UExpr<*>,
1352+
rhs: UExpr<*>,
1353+
scope: TsStepScope
1354+
): UExpr<*>? {
1355+
val lhsExpr = mkNumericExpr(lhs, scope)
1356+
val rhsExpr = mkNumericExpr(rhs, scope)
1357+
return mkFpRemExpr(lhsExpr, rhsExpr)
1358+
}
13161359
}
13171360
}

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

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
package org.usvm.samples.operators
2+
3+
import org.junit.jupiter.api.Disabled
4+
import org.junit.jupiter.api.Test
5+
import org.usvm.api.TsTestValue
6+
import org.usvm.util.TsMethodTestRunner
7+
import org.usvm.util.toDouble
8+
9+
class Remainder : TsMethodTestRunner() {
10+
private val className = this::class.simpleName!!
11+
12+
override val scene = loadSampleScene(className, folderPrefix = "operators")
13+
14+
@Test
15+
@Disabled("Never ends")
16+
fun testTwoNumbersRemainder() {
17+
val method = getMethod(className, "twoNumbersRemainder")
18+
discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber, TsTestValue.TsNumber>(
19+
method = method,
20+
{ a, b, r ->
21+
val res = a.number % b.number
22+
res != res && (a.number.isNaN() || b.number.isNaN())
23+
},
24+
{ a, b, r ->
25+
val res = a.number % b.number
26+
res != res && (a.number == Double.POSITIVE_INFINITY || a.number == Double.NEGATIVE_INFINITY)
27+
},
28+
{ a, b, r -> a.number == 0.0 && b.number == 0.0 && r.number.isNaN() },
29+
{ a, b, r ->
30+
b.number == 0.0 && a.number != 0.0 && r.number.isNaN()
31+
},
32+
{ a, b, r ->
33+
(b.number == Double.POSITIVE_INFINITY || b.number == Double.NEGATIVE_INFINITY) && r.number == a.number
34+
},
35+
{ a, b, r -> a.number == 0.0 && r.number == a.number },
36+
{ a, b, r -> a.number % b.number == 4.0 && r.number == 4.0 },
37+
{ a, b, r ->
38+
val res = a.number % b.number
39+
!res.isNaN() && res != 4.0 && r.number == res
40+
},
41+
)
42+
}
43+
44+
@Test
45+
fun testBooleanRemainder() {
46+
val method = getMethod(className, "booleanRemainder")
47+
discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
48+
method = method,
49+
{ a, b, r -> a.value.toDouble() % b.value.toDouble() == 0.0 && r.number == 0.0 },
50+
{ a, b, r ->
51+
a.value.toDouble() % b.value.toDouble() != 0.0 && (r.number == (a.value.toDouble() % b.value.toDouble()) || r.number.isNaN())
52+
}
53+
)
54+
}
55+
56+
@Test
57+
@Disabled("Wrong result")
58+
fun testMixedRemainder() {
59+
val method = getMethod(className, "mixedRemainder")
60+
discoverProperties<TsTestValue.TsNumber, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
61+
method = method,
62+
{ a, b, r -> a.number % b.value.toDouble() == 4.0 && r.number == 4.0 },
63+
{ a, b, r -> (a.number % b.value.toDouble()).isNaN() && r.number.isNaN() },
64+
{ a, b, r -> a.number % b.value.toDouble() != 4.0 && r.number == a.number % b.value.toDouble() }
65+
)
66+
}
67+
68+
@Test
69+
@Disabled("Never ends")
70+
fun testUnknownRemainder() {
71+
val method = getMethod(className, "unknownRemainder")
72+
discoverProperties<TsTestValue, TsTestValue, TsTestValue.TsNumber>(
73+
method = method,
74+
{ a, b, r -> (a is TsTestValue.TsUndefined || b is TsTestValue.TsUndefined) && r.number.isNaN() },
75+
{ _, _, r -> r.number == 4.0 },
76+
{ _, _, r -> r.number.isNaN() },
77+
{ _, _, r -> !r.number.isNaN() && r.number != 4.0 }
78+
)
79+
}
80+
}

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ import org.jacodb.ets.utils.loadEtsFileAutoConvert
1818
import org.junit.jupiter.api.TestInstance
1919
import org.junit.jupiter.api.TestInstance.Lifecycle.PER_CLASS
2020
import org.usvm.PathSelectionStrategy
21+
import org.usvm.SolverType
2122
import org.usvm.UMachineOptions
2223
import org.usvm.api.NoCoverage
2324
import org.usvm.api.TsMethodCoverage
@@ -343,6 +344,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
343344
exceptionsPropagation = true,
344345
timeout = Duration.INFINITE,
345346
stepsFromLastCovered = 3500L,
347+
solverType = SolverType.YICES,
346348
solverTimeout = Duration.INFINITE, // we do not need the timeout for a solver in tests
347349
typeOperationsTimeout = Duration.INFINITE, // we do not need the timeout for type operations in tests
348350
)

‎usvm-ts/src/test/resources/samples/operators/Remainder.ts

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
class Remainder {
2+
twoNumbersRemainder(a: number, b: number): number {
3+
res = a % b;
4+
5+
if (a != a || b != b) {
6+
return res // NaN
7+
}
8+
9+
if (a == Infinity || a == -Infinity) {
10+
return res // NaN
11+
}
12+
13+
if (a == 0 && b == 0) {
14+
return res // NaN
15+
}
16+
17+
if (b == 0) {
18+
return res // NaN
19+
}
20+
21+
if (b == Infinity || b == -Infinity) {
22+
return res // a
23+
}
24+
25+
if (a == 0) {
26+
return res // a
27+
}
28+
29+
if (res == 4) {
30+
return res
31+
}
32+
33+
return res
34+
}
35+
36+
booleanRemainder(a: boolean, b: boolean): number {
37+
res = a % b;
38+
39+
if (res == 0) {
40+
return res
41+
}
42+
43+
return res
44+
}
45+
46+
mixedRemainder(a: number, b: boolean): number {
47+
res = a % b;
48+
if (res == 4) {
49+
return res
50+
}
51+
52+
if (res != res) {
53+
return res
54+
}
55+
56+
return res
57+
}
58+
59+
unknownRemainder(a, b): number {
60+
res = a % b;
61+
62+
if (res == 4) {
63+
return res;
64+
}
65+
66+
if (res != res) {
67+
return res;
68+
}
69+
70+
return res;
71+
}
72+
}

0 commit comments

Comments
 (0)