Skip to content

Commit 5719f00

Browse files
CaelmBleiddLipen
CaelmBleidd
and
Lipen
authored
Division and remainder operator (#290)
--------- Co-authored-by: Konstantin Chukharev <lipen00@gmail.com>
1 parent 90270d3 commit 5719f00

12 files changed

Lines changed: 474 additions & 57 deletions

File tree

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

Lines changed: 18 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,19 @@ fun TsContext.mkTruthyExpr(
9191
fun TsContext.mkNumericExpr(
9292
expr: UExpr<out USort>,
9393
scope: TsStepScope,
94-
): UExpr<KFp64Sort> = scope.calcOnState {
94+
): UExpr<KFp64Sort> {
95+
if (expr.isFakeObject()) {
96+
val type = expr.getFakeType(scope)
97+
return mkIte(
98+
condition = type.fpTypeExpr,
99+
trueBranch = expr.extractFp(scope),
100+
falseBranch = mkIte(
101+
condition = type.boolTypeExpr,
102+
trueBranch = mkNumericExpr(expr.extractBool(scope), scope),
103+
falseBranch = mkNumericExpr(expr.extractRef(scope), scope)
104+
)
105+
)
106+
}
95107

96108
// 7.1.4 ToNumber ( argument )
97109
//
@@ -107,27 +119,27 @@ fun TsContext.mkNumericExpr(
107119
// 10. Return ToNumber(primValue).
108120

109121
if (expr.sort == fp64Sort) {
110-
return@calcOnState expr.asExpr(fp64Sort)
122+
return expr.asExpr(fp64Sort)
111123
}
112124

113125
if (expr == mkUndefinedValue()) {
114-
return@calcOnState mkFp64NaN()
126+
return mkFp64NaN()
115127
}
116128

117129
if (expr == mkTsNullValue()) {
118-
return@calcOnState mkFp64(0.0)
130+
return mkFp64(0.0)
119131
}
120132

121133
if (expr.sort == boolSort) {
122-
return@calcOnState boolToFp(expr.asExpr(boolSort))
134+
return boolToFp(expr.asExpr(boolSort))
123135
}
124136

125137
// TODO: ToPrimitive, then ToNumber again
126138
// TODO: probably we need to implement Object (Ref/Fake) -> Number conversion here directly, without ToPrimitive
127139

128140
// TODO incorrect implementation, returns some number that is not equal to 0 and NaN
129141
// https://github.com/UnitTestBot/usvm/issues/280
130-
return@calcOnState mkIte(
142+
return mkIte(
131143
condition = mkEq(expr.asExpr(addressSort), mkTsNullValue()),
132144
trueBranch = mkFp(0.0, fp64Sort),
133145
falseBranch = mkIte(

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

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -332,13 +332,11 @@ class TsExprResolver(
332332
}
333333

334334
override fun visit(expr: EtsDivExpr): UExpr<out USort>? {
335-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
336-
error("Not supported $expr")
335+
return resolveBinaryOperator(TsBinaryOperator.Div, expr)
337336
}
338337

339338
override fun visit(expr: EtsRemExpr): UExpr<out USort>? {
340-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
341-
error("Not supported $expr")
339+
return resolveBinaryOperator(TsBinaryOperator.Rem, expr)
342340
}
343341

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

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

Lines changed: 99 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1217,7 +1217,7 @@ sealed interface TsBinaryOperator {
12171217
lhs: UBoolExpr,
12181218
rhs: UBoolExpr,
12191219
scope: TsStepScope,
1220-
): UExpr<*> {
1220+
): UExpr<KFp64Sort> {
12211221
val left = mkNumericExpr(lhs, scope)
12221222
val right = mkNumericExpr(rhs, scope)
12231223
return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
@@ -1227,15 +1227,15 @@ sealed interface TsBinaryOperator {
12271227
lhs: UExpr<KFp64Sort>,
12281228
rhs: UExpr<KFp64Sort>,
12291229
scope: TsStepScope,
1230-
): UExpr<*> {
1230+
): UExpr<KFp64Sort> {
12311231
return mkFpMulExpr(fpRoundingModeSortDefaultValue(), lhs, rhs)
12321232
}
12331233

12341234
override fun TsContext.onRef(
12351235
lhs: UHeapRef,
12361236
rhs: UHeapRef,
12371237
scope: TsStepScope,
1238-
): UExpr<*> {
1238+
): UExpr<KFp64Sort> {
12391239
val left = mkNumericExpr(lhs, scope)
12401240
val right = mkNumericExpr(rhs, scope)
12411241
return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
@@ -1245,7 +1245,7 @@ sealed interface TsBinaryOperator {
12451245
lhs: UExpr<*>,
12461246
rhs: UExpr<*>,
12471247
scope: TsStepScope,
1248-
): UExpr<*> {
1248+
): UExpr<KFp64Sort> {
12491249
check(lhs.isFakeObject() || rhs.isFakeObject())
12501250
val left = mkNumericExpr(lhs, scope)
12511251
val right = mkNumericExpr(rhs, scope)
@@ -1256,11 +1256,105 @@ sealed interface TsBinaryOperator {
12561256
lhs: UExpr<*>,
12571257
rhs: UExpr<*>,
12581258
scope: TsStepScope,
1259-
): UExpr<*> {
1259+
): UExpr<KFp64Sort> {
12601260
check(!lhs.isFakeObject() && !rhs.isFakeObject())
12611261
val left = mkNumericExpr(lhs, scope)
12621262
val right = mkNumericExpr(rhs, scope)
12631263
return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
12641264
}
12651265
}
1266+
1267+
data object Div : TsBinaryOperator {
1268+
override fun TsContext.onBool(
1269+
lhs: UBoolExpr,
1270+
rhs: UBoolExpr,
1271+
scope: TsStepScope,
1272+
): UExpr<KFp64Sort> {
1273+
val left = mkNumericExpr(lhs, scope)
1274+
val right = mkNumericExpr(rhs, scope)
1275+
return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
1276+
}
1277+
1278+
override fun TsContext.onFp(
1279+
lhs: UExpr<KFp64Sort>,
1280+
rhs: UExpr<KFp64Sort>,
1281+
scope: TsStepScope,
1282+
): UExpr<KFp64Sort> {
1283+
return mkFpDivExpr(fpRoundingModeSortDefaultValue(), lhs, rhs)
1284+
}
1285+
1286+
override fun TsContext.onRef(
1287+
lhs: UHeapRef,
1288+
rhs: UHeapRef,
1289+
scope: TsStepScope,
1290+
): UExpr<KFp64Sort> {
1291+
val left = mkNumericExpr(lhs, scope)
1292+
val right = mkNumericExpr(rhs, scope)
1293+
return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
1294+
}
1295+
1296+
override fun TsContext.resolveFakeObject(
1297+
lhs: UExpr<*>,
1298+
rhs: UExpr<*>,
1299+
scope: TsStepScope,
1300+
): UExpr<KFp64Sort> {
1301+
val left = mkNumericExpr(lhs, scope)
1302+
val right = mkNumericExpr(rhs, scope)
1303+
return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
1304+
}
1305+
1306+
override fun TsContext.internalResolve(
1307+
lhs: UExpr<*>,
1308+
rhs: UExpr<*>,
1309+
scope: TsStepScope,
1310+
): UExpr<KFp64Sort> {
1311+
val left = mkNumericExpr(lhs, scope)
1312+
val right = mkNumericExpr(rhs, scope)
1313+
return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
1314+
}
1315+
}
1316+
1317+
data object Rem : TsBinaryOperator {
1318+
override fun TsContext.onBool(
1319+
lhs: UBoolExpr,
1320+
rhs: UBoolExpr,
1321+
scope: TsStepScope,
1322+
): UExpr<KFp64Sort> {
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<KFp64Sort> {
1331+
return internalResolve(lhs, rhs, scope)
1332+
}
1333+
1334+
override fun TsContext.onRef(
1335+
lhs: UHeapRef,
1336+
rhs: UHeapRef,
1337+
scope: TsStepScope,
1338+
): UExpr<KFp64Sort> {
1339+
return internalResolve(lhs, rhs, scope)
1340+
}
1341+
1342+
override fun TsContext.resolveFakeObject(
1343+
lhs: UExpr<*>,
1344+
rhs: UExpr<*>,
1345+
scope: TsStepScope,
1346+
): UExpr<KFp64Sort> {
1347+
return internalResolve(lhs, rhs, scope)
1348+
}
1349+
1350+
override fun TsContext.internalResolve(
1351+
lhs: UExpr<*>,
1352+
rhs: UExpr<*>,
1353+
scope: TsStepScope,
1354+
): UExpr<KFp64Sort> {
1355+
val lhsExpr = mkNumericExpr(lhs, scope)
1356+
val rhsExpr = mkNumericExpr(rhs, scope)
1357+
return mkFpRemExpr(lhsExpr, rhsExpr)
1358+
}
1359+
}
12661360
}

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -119,11 +119,12 @@ class InputArrays : TsMethodTestRunner() {
119119
method = method,
120120
{ x, r ->
121121
val value = x.values[0]
122-
value is TsTestValue.TsNumber && value.number == 1.0 && r is TsTestValue.TsNull },
122+
value is TsTestValue.TsNumber && value.number == 1.0 && r is TsTestValue.TsNull
123+
},
123124
{ x, r ->
124125
val value = x.values[0]
125126
value !is TsTestValue.TsNumber || value.number != 1.0 && r == value
126127
},
127128
)
128129
}
129-
}
130+
}

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

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
package org.usvm.samples.operators
2+
3+
import org.jacodb.ets.model.EtsScene
4+
import org.usvm.api.TsTestValue
5+
import org.usvm.util.TsMethodTestRunner
6+
import org.usvm.util.toDouble
7+
import kotlin.test.Test
8+
9+
class Division : TsMethodTestRunner() {
10+
private val className = this::class.simpleName!!
11+
12+
override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
13+
14+
@Test
15+
fun testTwoNumbersDivision() {
16+
val method = getMethod(className, "twoNumbersDivision")
17+
discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber, TsTestValue.TsNumber>(
18+
method = method,
19+
{ a, b, r -> a.number / b.number == 4.0 && r.number == 4.0 },
20+
{ a, b, r -> a.number / b.number == Double.POSITIVE_INFINITY && r.number == Double.POSITIVE_INFINITY },
21+
{ a, b, r -> a.number / b.number == Double.NEGATIVE_INFINITY && r.number == Double.NEGATIVE_INFINITY },
22+
{ a, b, r -> (a.number / b.number).isNaN() && r.number.isNaN() },
23+
{ a, b, r -> a.number / b.number != 4.0 && r.number == a.number / b.number }
24+
)
25+
}
26+
27+
@Test
28+
fun testBooleanDivision() {
29+
val method = getMethod(className, "booleanDivision")
30+
discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
31+
method = method,
32+
{ a, b, r -> a.value.toDouble() / b.value.toDouble() == 0.0 && r.number == 0.0 },
33+
{ a, b, r ->
34+
a.value.toDouble() / b.value.toDouble() != 0.0 && (r.number == (a.value.toDouble() / b.value.toDouble()) || r.number.isNaN())
35+
}
36+
)
37+
}
38+
39+
@Test
40+
fun testMixedDivision() {
41+
val method = getMethod(className, "mixedDivision")
42+
discoverProperties<TsTestValue.TsNumber, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
43+
method = method,
44+
{ a, b, r -> a.number / b.value.toDouble() == 4.0 && r.number == 4.0 },
45+
{ a, b, r -> a.number / b.value.toDouble() == Double.POSITIVE_INFINITY && r.number == Double.POSITIVE_INFINITY },
46+
{ a, b, r -> a.number / b.value.toDouble() == Double.NEGATIVE_INFINITY && r.number == Double.NEGATIVE_INFINITY },
47+
{ a, b, r -> (a.number / b.value.toDouble()).isNaN() && r.number.isNaN() },
48+
{ a, b, r -> a.number / b.value.toDouble() != 4.0 && r.number == a.number / b.value.toDouble() }
49+
)
50+
}
51+
52+
@Test
53+
fun testUnknownDivision() {
54+
val method = getMethod(className, "unknownDivision")
55+
discoverProperties<TsTestValue, TsTestValue, TsTestValue.TsNumber>(
56+
method = method,
57+
{ a, b, r -> (a is TsTestValue.TsUndefined || b is TsTestValue.TsUndefined) && r.number.isNaN() },
58+
{ _, _, r -> r.number == 4.0 },
59+
{ _, _, r -> r.number == Double.POSITIVE_INFINITY },
60+
{ _, _, r -> r.number == Double.NEGATIVE_INFINITY },
61+
{ _, _, r -> r.number.isNaN() },
62+
)
63+
}
64+
}

‎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
)

0 commit comments

Comments
 (0)