Skip to content

Commit 96aa98e

Browse files
CaelmBleiddLipen
CaelmBleidd
and
Lipen
authored
Add operator for USVM TS (#277)
--------- Co-authored-by: Konstantin Chukharev <lipen00@gmail.com>
1 parent 3a42692 commit 96aa98e

16 files changed

Lines changed: 496 additions & 55 deletions

File tree

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

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -125,5 +125,15 @@ fun TsContext.mkNumericExpr(
125125
// TODO: ToPrimitive, then ToNumber again
126126
// TODO: probably we need to implement Object (Ref/Fake) -> Number conversion here directly, without ToPrimitive
127127

128-
error("Unsupported sort: ${expr.sort}")
128+
// TODO incorrect implementation, returns some number that is not equal to 0 and NaN
129+
// https://github.com/UnitTestBot/usvm/issues/280
130+
return@calcOnState mkIte(
131+
condition = mkEq(expr.asExpr(addressSort), mkTsNullValue()),
132+
trueBranch = mkFp(0.0, fp64Sort),
133+
falseBranch = mkIte(
134+
mkEq(expr.asExpr(addressSort), mkUndefinedValue()),
135+
mkFp64NaN(),
136+
mkFp64NaN()
137+
)
138+
)
129139
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ class TsUnresolvedSort(ctx: TsContext) : USort(ctx) {
4949
}
5050
}
5151

52-
fun UExpr<out USort>.extractBool(): Boolean = when (this) {
52+
fun UExpr<out USort>.toConcreteBoolValue(): Boolean = when (this) {
5353
ctx.trueExpr -> true
5454
ctx.falseExpr -> false
5555
else -> error("Cannot extract boolean from $this")

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

Lines changed: 302 additions & 41 deletions
Large diffs are not rendered by default.

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -77,8 +77,8 @@ class FieldAccess : TsMethodTestRunner() {
7777
x.number == 1.1 && r.number == 14.0
7878
},
7979
{ a, r ->
80-
val x = a.properties["x"] as TsTestValue.TsNumber
81-
x.number != 1.1 && r.number == 10.0
80+
val x = a.properties["x"] as? TsTestValue.TsNumber
81+
x?.number != 1.1 && r.number == 10.0
8282
},
8383
)
8484
}

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

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
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 Add : TsMethodTestRunner() {
10+
private val className = this::class.simpleName!!
11+
12+
override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
13+
14+
@Test
15+
fun `bool + bool`() {
16+
val method = getMethod(className, "addBoolAndBool")
17+
discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
18+
method = method,
19+
{ a, b, r -> r.number == 1.0 && !a.value && !b.value },
20+
{ a, b, r -> r.number == 2.0 && !a.value && b.value },
21+
{ a, b, r -> r.number == 3.0 && a.value && !b.value },
22+
{ a, b, r -> r.number == 4.0 && a.value && b.value },
23+
invariants = arrayOf(
24+
{ _, _, r -> r.number != -1.0 }
25+
)
26+
)
27+
}
28+
29+
@Test
30+
fun `bool + number`() {
31+
val method = getMethod(className, "addBoolAndNumber")
32+
discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsNumber, TsTestValue.TsNumber>(
33+
method = method,
34+
{ a, b, r -> r.number == 1.0 && a.value && b.number == -1.0 },
35+
{ a, b, r -> r.number == 2.0 && !a.value && b.number == 0.0 },
36+
{ a, b, r -> r.number == 3.0 && a.value && b.number == 5.0 },
37+
{ _, b, r -> r.number.isNaN() && b.number.isNaN() },
38+
{ a, b, r ->
39+
val result = a.value.toDouble() + b.number
40+
r.number == 4.0 && result != 2.2 && !result.isNaN()
41+
}
42+
)
43+
}
44+
45+
@Test
46+
fun `number + number`() {
47+
val method = getMethod(className, "addNumberAndNumber")
48+
discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber, TsTestValue.TsNumber>(
49+
method = method,
50+
{ a, b, r -> a.number.isNaN() && r.number.isNaN() },
51+
{ a, b, r -> !a.number.isNaN() && b.number.isNaN() && r.number.isNaN() },
52+
{ a, b, r -> a.number + b.number == r.number },
53+
{ a, b, r -> !a.number.isNaN() && !b.number.isNaN() && r.number == 0.0 },
54+
)
55+
}
56+
57+
@Test
58+
fun `number + undefined`() {
59+
val method = getMethod(className, "addNumberAndUndefined")
60+
discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
61+
method = method,
62+
invariants = arrayOf(
63+
{ a, r -> r.number != -1.0 },
64+
)
65+
)
66+
}
67+
68+
@Test
69+
fun `number + null`() {
70+
val method = getMethod(className, "addNumberAndNull")
71+
discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
72+
method = method,
73+
{ a, r -> a.number.isNaN() && r.number.isNaN() },
74+
{ a, r -> !a.number.isNaN() && r.number == a.number },
75+
)
76+
}
77+
78+
@Test
79+
fun `add unknown values`() {
80+
val method = getMethod(className, "addUnknownValues")
81+
discoverProperties<TsTestValue, TsTestValue, TsTestValue.TsNumber>(
82+
method = method,
83+
{ a, b, r -> a is TsTestValue.TsUndefined || b is TsTestValue.TsUndefined && r.number.isNaN() },
84+
{ a, b, r ->
85+
(a is TsTestValue.TsClass
86+
|| b is TsTestValue.TsClass
87+
|| (a as? TsTestValue.TsNumber)?.number?.isNaN() == true
88+
|| (b as? TsTestValue.TsNumber)?.number?.isNaN() == true)
89+
&& r.number.isNaN()
90+
},
91+
{ a, b, r -> r.number == 7.0 },
92+
{ a, b, r -> a is TsTestValue.TsNull && b is TsTestValue.TsNull && r.number == 0.0 },
93+
{ a, b, r -> r.number == 42.0 }
94+
)
95+
}
96+
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package org.usvm.samples
1+
package org.usvm.samples.operators
22

33
import org.jacodb.ets.dsl.and
44
import org.jacodb.ets.dsl.const
@@ -28,7 +28,7 @@ class And : TsMethodTestRunner() {
2828

2929
private val className = this::class.simpleName!!
3030

31-
override val scene: EtsScene = loadSampleScene(className)
31+
override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
3232

3333
private val classSignature: EtsClassSignature =
3434
scene.projectFiles[0].classes.single { it.name != DEFAULT_ARK_CLASS_NAME }.signature

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package org.usvm.samples
1+
package org.usvm.samples.operators
22

33
import org.jacodb.ets.model.EtsScene
44
import org.junit.jupiter.api.Disabled
@@ -10,7 +10,7 @@ class Equality : TsMethodTestRunner() {
1010

1111
private val className = this::class.simpleName!!
1212

13-
override val scene: EtsScene = loadSampleScene(className)
13+
override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
1414

1515
@Test
1616
fun `test eqBoolWithBool`() {

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package org.usvm.samples
1+
package org.usvm.samples.operators
22

33
import org.jacodb.ets.model.EtsScene
44
import org.junit.jupiter.api.Test
@@ -9,7 +9,7 @@ class Neg : TsMethodTestRunner() {
99

1010
private val className = this::class.simpleName!!
1111

12-
override val scene: EtsScene = loadSampleScene(className)
12+
override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
1313

1414
@Test
1515
fun `test negateNumber`() {

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package org.usvm.samples
1+
package org.usvm.samples.operators
22

33
import org.jacodb.ets.dsl.const
44
import org.jacodb.ets.dsl.eq
@@ -26,7 +26,7 @@ class Or : TsMethodTestRunner() {
2626

2727
private val className = this::class.simpleName!!
2828

29-
override val scene: EtsScene = loadSampleScene(className)
29+
override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
3030

3131
private val classSignature: EtsClassSignature =
3232
scene.projectFiles[0].classes.single { it.name != DEFAULT_ARK_CLASS_NAME }.signature

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,8 +34,8 @@ import org.usvm.api.typeStreamOf
3434
import org.usvm.isTrue
3535
import org.usvm.machine.TsContext
3636
import org.usvm.machine.expr.TsUnresolvedSort
37-
import org.usvm.machine.expr.extractBool
3837
import org.usvm.machine.expr.extractDouble
38+
import org.usvm.machine.expr.toConcreteBoolValue
3939
import org.usvm.machine.state.TsMethodResult
4040
import org.usvm.machine.state.TsState
4141
import org.usvm.memory.ULValue
@@ -306,7 +306,7 @@ open class TsTestStateResolver(
306306
}
307307
}
308308

309-
EtsBooleanType -> TsTestValue.TsBoolean(evaluateInModel(expr).extractBool())
309+
EtsBooleanType -> TsTestValue.TsBoolean(evaluateInModel(expr).toConcreteBoolValue())
310310
EtsUndefinedType -> TsTestValue.TsUndefined
311311
is EtsLiteralType -> TODO()
312312
EtsNullType -> TODO()

0 commit comments

Comments
 (0)