Skip to content

Commit 69484a8

Browse files
CaelmBleiddCaelmBleidd
committed
Division operator
1 parent c5cc31c commit 69484a8

File tree

5 files changed

+209
-2
lines changed

5 files changed

+209
-2
lines changed

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

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

96110
// 7.1.4 ToNumber ( argument )
97111
//

‎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
@@ -359,8 +359,7 @@ class TsExprResolver(
359359
}
360360

361361
override fun visit(expr: EtsDivExpr): UExpr<out USort>? {
362-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
363-
error("Not supported $expr")
362+
return resolveBinaryOperator(TsBinaryOperator.Div, expr)
364363
}
365364

366365
override fun visit(expr: EtsRemExpr): UExpr<out USort>? {

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

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1263,4 +1263,55 @@ sealed interface TsBinaryOperator {
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<*>? {
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<*>? {
1283+
return mkFpDivExpr(fpRoundingModeSortDefaultValue(), lhs, rhs)
1284+
}
1285+
1286+
override fun TsContext.onRef(
1287+
lhs: UHeapRef,
1288+
rhs: UHeapRef,
1289+
scope: TsStepScope
1290+
): UExpr<*>? {
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<*>? {
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<*>? {
1311+
val left = mkNumericExpr(lhs, scope)
1312+
val right = mkNumericExpr(rhs, scope)
1313+
return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
1314+
}
1315+
1316+
}
12661317
}

‎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/resources/samples/operators/Division.ts

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

0 commit comments

Comments
 (0)