Skip to content

Commit 3f8f361

Browse files
LipenLipen
authored
Rename TsValue (#253)
1 parent 90b4122 commit 3f8f361

File tree

21 files changed

+163
-171
lines changed

21 files changed

+163
-171
lines changed

‎usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt‎

Lines changed: 28 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -9,62 +9,53 @@ data class TsTest(
99
val method: EtsMethod,
1010
val before: TsParametersState,
1111
val after: TsParametersState,
12-
val returnValue: TsObject,
12+
val returnValue: TsValue,
1313
val trace: List<EtsStmt>? = null,
1414
)
1515

1616
data class TsParametersState(
17-
val thisInstance: TsObject?,
18-
val parameters: List<TsObject>,
17+
val thisInstance: TsValue?,
18+
val parameters: List<TsValue>,
1919
val globals: Map<EtsClass, List<GlobalFieldValue>>,
2020
)
2121

22-
data class GlobalFieldValue(val field: EtsField, val value: TsObject) // TODO is it right?????
22+
data class GlobalFieldValue(val field: EtsField, val value: TsValue) // TODO is it right?????
2323

2424
open class TsMethodCoverage
2525

2626
object NoCoverage : TsMethodCoverage()
2727

28-
sealed interface TsObject {
29-
sealed interface TsNumber : org.usvm.api.TsObject {
30-
data class Integer(val value: Int) : TsNumber
28+
sealed interface TsValue {
29+
data object TsAny : TsValue
30+
data object TsUnknown : TsValue
31+
data object TsNull : TsValue
32+
data object TsUndefined : TsValue
33+
data object TsException : TsValue
3134

32-
data class Double(val value: kotlin.Double) : TsNumber
35+
data class TsBoolean(val value: Boolean) : TsValue
36+
data class TsString(val value: String) : TsValue
37+
data class TsBigInt(val value: String) : TsValue
3338

34-
val number: kotlin.Double
35-
get() = when (this) {
36-
is Integer -> value.toDouble()
37-
is Double -> value
38-
}
39-
40-
val truthyValue: Boolean
41-
get() = number != 0.0 && !number.isNaN()
42-
}
39+
sealed interface TsNumber : TsValue {
40+
data class TsInteger(val value: Int) : TsNumber
4341

44-
data class TsString(val value: String) : org.usvm.api.TsObject
42+
data class TsDouble(val value: Double) : TsNumber
4543

46-
data class TsBoolean(val value: Boolean) : org.usvm.api.TsObject {
4744
val number: Double
48-
get() = if (value) 1.0 else 0.0
45+
get() = when (this) {
46+
is TsInteger -> value.toDouble()
47+
is TsDouble -> value
48+
}
4949
}
5050

51-
data class TsBigInt(val value: String) : org.usvm.api.TsObject
52-
53-
data class TsClass(val name: String, val properties: Map<String, org.usvm.api.TsObject>) :
54-
org.usvm.api.TsObject
55-
56-
data object TsAny : org.usvm.api.TsObject
57-
58-
data object TsUndefinedObject : org.usvm.api.TsObject
59-
60-
data class TsArray(val values: List<org.usvm.api.TsObject>) :
61-
org.usvm.api.TsObject
62-
63-
data class TsObject(val addr: Int) : org.usvm.api.TsObject
64-
65-
data object TsUnknown : org.usvm.api.TsObject
51+
data class TsObject(val addr: Int) : TsValue
6652

67-
data object TsNull : org.usvm.api.TsObject
53+
data class TsClass(
54+
val name: String,
55+
val properties: Map<String, TsValue>,
56+
) : TsValue
6857

69-
data object TsException : org.usvm.api.TsObject
58+
data class TsArray(
59+
val values: List<TsValue>,
60+
) : TsValue
7061
}

‎usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,12 +13,12 @@ import org.usvm.api.targets.TsTarget
1313
import org.usvm.collections.immutable.getOrPut
1414
import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
1515
import org.usvm.collections.immutable.internal.MutabilityOwnership
16+
import org.usvm.collections.immutable.persistentHashMapOf
1617
import org.usvm.constraints.UPathConstraints
1718
import org.usvm.machine.TsContext
1819
import org.usvm.memory.UMemory
1920
import org.usvm.model.UModelBase
2021
import org.usvm.targets.UTargetsSet
21-
import org.usvm.collections.immutable.persistentHashMapOf
2222

2323
class TsState(
2424
ctx: TsContext,

‎usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ import org.usvm.machine.state.TsState
1515
fun TsContext.boolToFp(expr: UExpr<UBoolSort>): UExpr<KFp64Sort> =
1616
mkIte(expr, mkFp64(1.0), mkFp64(0.0))
1717

18-
1918
// TODO probably this should be written differently
2019
fun EtsScene.fieldLookUp(field: EtsFieldSignature) = projectAndSdkClasses
2120
.first { it.signature == field.enclosingClass }

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

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ import org.jacodb.ets.utils.getLocals
3535
import org.jacodb.ets.utils.loadEtsFileAutoConvert
3636
import org.junit.jupiter.api.Disabled
3737
import org.junit.jupiter.api.Test
38-
import org.usvm.api.TsObject
38+
import org.usvm.api.TsValue
3939
import org.usvm.util.TsMethodTestRunner
4040
import org.usvm.util.getResourcePath
4141
import org.usvm.util.isTruthy
@@ -59,7 +59,7 @@ class And : TsMethodTestRunner() {
5959
@Test
6060
fun `test andOfBooleanAndBoolean`() {
6161
val method = getMethod("And", "andOfBooleanAndBoolean")
62-
discoverProperties<TsObject.TsBoolean, TsObject.TsBoolean, TsObject.TsNumber>(
62+
discoverProperties<TsValue.TsBoolean, TsValue.TsBoolean, TsValue.TsNumber>(
6363
method = method,
6464
{ a, b, r -> a.value && b.value && r.number == 1.0 },
6565
{ a, b, r -> a.value && !b.value && r.number == 2.0 },
@@ -107,7 +107,7 @@ class And : TsMethodTestRunner() {
107107
method._cfg = etsCfg
108108
locals += method.getLocals()
109109

110-
discoverProperties<TsObject.TsBoolean, TsObject.TsBoolean, TsObject.TsNumber>(
110+
discoverProperties<TsValue.TsBoolean, TsValue.TsBoolean, TsValue.TsNumber>(
111111
method = method,
112112
{ a, b, r -> a.value && b.value && r.number == 1.0 },
113113
{ a, b, r -> a.value && !b.value && r.number == 2.0 },
@@ -232,7 +232,7 @@ class And : TsMethodTestRunner() {
232232
method._cfg = EtsCfg(statements, successorMap)
233233
locals += method.getLocals()
234234

235-
discoverProperties<TsObject.TsNumber, TsObject.TsNumber, TsObject.TsNumber>(
235+
discoverProperties<TsValue.TsNumber, TsValue.TsNumber, TsValue.TsNumber>(
236236
method = method,
237237
{ a, b, r -> isTruthy(a) && isTruthy(b) && r.number == 1.0 },
238238
{ a, b, r -> isTruthy(a) && b.number.isNaN() && r.number == 2.0 },
@@ -335,7 +335,7 @@ class And : TsMethodTestRunner() {
335335
method._cfg = EtsCfg(statements, successorMap)
336336
locals += method.getLocals()
337337

338-
discoverProperties<TsObject.TsBoolean, TsObject.TsNumber, TsObject.TsNumber>(
338+
discoverProperties<TsValue.TsBoolean, TsValue.TsNumber, TsValue.TsNumber>(
339339
method = method,
340340
{ a, b, r -> a.value && isTruthy(b) && r.number == 1.0 },
341341
{ a, b, r -> a.value && b.number.isNaN() && r.number == 2.0 },
@@ -435,7 +435,7 @@ class And : TsMethodTestRunner() {
435435
method._cfg = EtsCfg(statements, successorMap)
436436
locals += method.getLocals()
437437

438-
discoverProperties<TsObject.TsNumber, TsObject.TsBoolean, TsObject.TsNumber>(
438+
discoverProperties<TsValue.TsNumber, TsValue.TsBoolean, TsValue.TsNumber>(
439439
method = method,
440440
{ a, b, r -> isTruthy(a) && b.value && r.number == 1.0 },
441441
{ a, b, r -> isTruthy(a) && !b.value && r.number == 2.0 },
@@ -450,7 +450,7 @@ class And : TsMethodTestRunner() {
450450
@Disabled("Does not work because objects cannot be null")
451451
fun `test andOfObjectAndObject`() {
452452
val method = getMethod("And", "andOfObjectAndObject")
453-
discoverProperties<TsObject.TsClass, TsObject.TsClass, TsObject.TsNumber>(
453+
discoverProperties<TsValue.TsClass, TsValue.TsClass, TsValue.TsNumber>(
454454
method = method,
455455
{ a, b, r -> isTruthy(a) && isTruthy(b) && r.number == 1.0 },
456456
{ a, b, r -> isTruthy(a) && !isTruthy(b) && r.number == 2.0 },
@@ -462,25 +462,25 @@ class And : TsMethodTestRunner() {
462462
@Test
463463
fun `test andOfUnknown`() {
464464
val method = getMethod("And", "andOfUnknown")
465-
discoverProperties<TsObject, TsObject, TsObject.TsNumber>(
465+
discoverProperties<TsValue, TsValue, TsValue.TsNumber>(
466466
method = method,
467467
{ a, b, r ->
468-
if (a is TsObject.TsBoolean && b is TsObject.TsBoolean) {
468+
if (a is TsValue.TsBoolean && b is TsValue.TsBoolean) {
469469
a.value && b.value && r.number == 1.0
470470
} else true
471471
},
472472
{ a, b, r ->
473-
if (a is TsObject.TsBoolean && b is TsObject.TsBoolean) {
473+
if (a is TsValue.TsBoolean && b is TsValue.TsBoolean) {
474474
a.value && !b.value && r.number == 2.0
475475
} else true
476476
},
477477
{ a, b, r ->
478-
if (a is TsObject.TsBoolean && b is TsObject.TsBoolean) {
478+
if (a is TsValue.TsBoolean && b is TsValue.TsBoolean) {
479479
!a.value && b.value && r.number == 3.0
480480
} else true
481481
},
482482
{ a, b, r ->
483-
if (a is TsObject.TsBoolean && b is TsObject.TsBoolean) {
483+
if (a is TsValue.TsBoolean && b is TsValue.TsBoolean) {
484484
!a.value && !b.value && r.number == 4.0
485485
} else true
486486
},
@@ -490,20 +490,20 @@ class And : TsMethodTestRunner() {
490490
@Test
491491
fun `test truthyUnknown`() {
492492
val method = getMethod("And", "truthyUnknown")
493-
discoverProperties<TsObject, TsObject, TsObject.TsNumber>(
493+
discoverProperties<TsValue, TsValue, TsValue.TsNumber>(
494494
method = method,
495495
{ a, b, r ->
496-
if (a is TsObject.TsBoolean && b is TsObject.TsBoolean) {
496+
if (a is TsValue.TsBoolean && b is TsValue.TsBoolean) {
497497
a.value && !b.value && r.number == 1.0
498498
} else true
499499
},
500500
{ a, b, r ->
501-
if (a is TsObject.TsBoolean && b is TsObject.TsBoolean) {
501+
if (a is TsValue.TsBoolean && b is TsValue.TsBoolean) {
502502
!a.value && b.value && r.number == 2.0
503503
} else true
504504
},
505505
{ a, b, r ->
506-
if (a is TsObject.TsBoolean && b is TsObject.TsBoolean) {
506+
if (a is TsValue.TsBoolean && b is TsValue.TsBoolean) {
507507
!a.value && !b.value && r.number == 99.0
508508
} else true
509509
},

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ package org.usvm.samples
33
import org.jacodb.ets.model.EtsScene
44
import org.jacodb.ets.utils.loadEtsFileAutoConvert
55
import org.junit.jupiter.api.Disabled
6-
import org.usvm.api.TsObject
6+
import org.usvm.api.TsValue
77
import org.usvm.util.TsMethodTestRunner
88
import org.usvm.util.getResourcePath
99
import kotlin.test.Test
@@ -20,7 +20,7 @@ class Arguments : TsMethodTestRunner() {
2020
@Test
2121
fun testNoArgs() {
2222
val method = getMethod("SimpleClass", "noArguments")
23-
discoverProperties<TsObject.TsNumber>(
23+
discoverProperties<TsValue.TsNumber>(
2424
method,
2525
{ r -> r.number == 42.0 },
2626
)
@@ -29,7 +29,7 @@ class Arguments : TsMethodTestRunner() {
2929
@Test
3030
fun testSingleArg() {
3131
val method = getMethod("SimpleClass", "singleArgument")
32-
discoverProperties<TsObject.TsNumber, TsObject.TsNumber>(
32+
discoverProperties<TsValue.TsNumber, TsValue.TsNumber>(
3333
method,
3434
{ a, r -> a == r },
3535
)
@@ -38,7 +38,7 @@ class Arguments : TsMethodTestRunner() {
3838
@Test
3939
fun testManyArgs() {
4040
val method = getMethod("SimpleClass", "manyArguments")
41-
discoverProperties<TsObject.TsNumber, TsObject.TsNumber, TsObject.TsNumber, TsObject.TsNumber>(
41+
discoverProperties<TsValue.TsNumber, TsValue.TsNumber, TsValue.TsNumber, TsValue.TsNumber>(
4242
method,
4343
{ a, _, _, r -> a.number == 1.0 && r == a },
4444
{ _, b, _, r -> b.number == 2.0 && r == b },
@@ -53,7 +53,7 @@ class Arguments : TsMethodTestRunner() {
5353
@Disabled
5454
fun testThisArg() {
5555
val method = getMethod("SimpleClass", "thisArgument")
56-
discoverProperties<TsObject.TsNumber>(
56+
discoverProperties<TsValue.TsNumber>(
5757
method,
5858
)
5959
}

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ package org.usvm.samples
33
import org.jacodb.ets.model.EtsScene
44
import org.jacodb.ets.utils.loadEtsFileAutoConvert
55
import org.junit.jupiter.api.Test
6-
import org.usvm.api.TsObject
6+
import org.usvm.api.TsValue
77
import org.usvm.util.TsMethodTestRunner
88
import org.usvm.util.getResourcePath
99

@@ -19,7 +19,7 @@ class Call : TsMethodTestRunner() {
1919
@Test
2020
fun `test simpleCall`() {
2121
val method = getMethod("Call", "simpleCall")
22-
discoverProperties<TsObject.TsNumber>(
22+
discoverProperties<TsValue.TsNumber>(
2323
method = method,
2424
{ r -> r.number == 42.0 },
2525
)
@@ -28,7 +28,7 @@ class Call : TsMethodTestRunner() {
2828
@Test
2929
fun `test fib`() {
3030
val method = getMethod("Call", "fib")
31-
discoverProperties<TsObject.TsNumber, TsObject.TsNumber>(
31+
discoverProperties<TsValue.TsNumber, TsValue.TsNumber>(
3232
method = method,
3333
{ n, r -> n.number < 0.0 && r.number == -1.0 },
3434
{ n, r -> n.number > 10.0 && r.number == -2.0 },

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

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ import org.jacodb.ets.model.EtsScene
44
import org.jacodb.ets.utils.loadEtsFileAutoConvert
55
import org.junit.jupiter.api.Disabled
66
import org.junit.jupiter.api.Test
7-
import org.usvm.api.TsObject
7+
import org.usvm.api.TsValue
88
import org.usvm.util.TsMethodTestRunner
99
import org.usvm.util.getResourcePath
1010

@@ -20,15 +20,15 @@ class Equality : TsMethodTestRunner() {
2020
@Disabled("Unsupported array new")
2121
fun testTruthyTypes() {
2222
val method = getMethod("Equality", "truthyTypes")
23-
discoverProperties<TsObject.TsNumber>(
23+
discoverProperties<TsValue.TsNumber>(
2424
method,
2525
)
2626
}
2727

2828
@Test
2929
fun testEqBoolWithBool() {
3030
val method = getMethod("Equality", "eqBoolWithBool")
31-
discoverProperties<TsObject.TsBoolean, TsObject.TsNumber>(
31+
discoverProperties<TsValue.TsBoolean, TsValue.TsNumber>(
3232
method,
3333
{ a, r -> a.value && r.number == 1.0 },
3434
{ a, r -> !a.value && r.number == -1.0 },
@@ -38,7 +38,7 @@ class Equality : TsMethodTestRunner() {
3838
@Test
3939
fun testEqNumberWithNumber() {
4040
val method = getMethod("Equality", "eqNumberWithNumber")
41-
discoverProperties<TsObject.TsNumber, TsObject.TsNumber>(
41+
discoverProperties<TsValue.TsNumber, TsValue.TsNumber>(
4242
method,
4343
{ a, r -> a.number == 1.1 && r.number == 1.0 },
4444
{ a, r -> a.number.isNaN() && r.number == 2.0 },
@@ -50,7 +50,7 @@ class Equality : TsMethodTestRunner() {
5050
@Disabled("Unsupported string")
5151
fun testEqStringWithString() {
5252
val method = getMethod("Equality", "eqStringWithString")
53-
discoverProperties<TsObject.TsString, TsObject.TsNumber>(
53+
discoverProperties<TsValue.TsString, TsValue.TsNumber>(
5454
method,
5555
{ a, r -> a.value == "123" && r.number == 1.0 },
5656
{ a, r -> a.value != "123" && r.number == 2.0 },
@@ -61,7 +61,7 @@ class Equality : TsMethodTestRunner() {
6161
@Disabled("Unsupported bigint")
6262
fun testEqBigintWithBigint() {
6363
val method = getMethod("Equality", "eqBigintWithBigint")
64-
discoverProperties<TsObject.TsBigInt, TsObject.TsNumber>(
64+
discoverProperties<TsValue.TsBigInt, TsValue.TsNumber>(
6565
method,
6666
{ a, r -> a.value == "42" && r.number == 1.0 },
6767
{ a, r -> a.value == "9999999999999999999999999999999999999" && r.number == 2.0 },
@@ -73,7 +73,7 @@ class Equality : TsMethodTestRunner() {
7373
@Disabled("Unsupported new construction")
7474
fun testEqObjectWithObject() {
7575
val method = getMethod("Equality", "eqObjectWithObject")
76-
discoverProperties<TsObject.TsClass, TsObject.TsNumber>(
76+
discoverProperties<TsValue.TsClass, TsValue.TsNumber>(
7777
method,
7878
{ a, r -> r.number == 1.0 },
7979
invariants = arrayOf(
@@ -86,10 +86,10 @@ class Equality : TsMethodTestRunner() {
8686
@Test
8787
fun testEqWithItself() {
8888
val method = getMethod("Equality", "eqWithItself")
89-
discoverProperties<TsObject.TsNumber, TsObject.TsNumber>(
89+
discoverProperties<TsValue.TsNumber, TsValue.TsNumber>(
9090
method,
9191
{ a, r -> a.number.isNaN() && r.number == 1.0 },
9292
{ a, r -> !a.number.isNaN() && r.number == 2.0 },
9393
)
9494
}
95-
}
95+
}

0 commit comments

Comments
 (0)