Skip to content

Commit 3f9bd62

Browse files
LipenLipen
authored
Adopt literal types (#324)
1 parent 6566cf1 commit 3f9bd62

File tree

3 files changed

+39
-32
lines changed

3 files changed

+39
-32
lines changed

‎buildSrc/src/main/kotlin/Dependencies.kt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ object Versions {
66
const val clikt = "5.0.0"
77
const val detekt = "1.23.7"
88
const val ini4j = "0.5.4"
9-
const val jacodb = "213f9a1aee"
9+
const val jacodb = "f3655cbc5d"
1010
const val juliet = "1.3.2"
1111
const val junit = "5.9.3"
1212
const val kotlin = "2.1.0"

‎usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt‎

Lines changed: 19 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,7 @@ import org.jacodb.ets.dto.VoidTypeDto
4343
import org.jacodb.ets.model.EtsAliasType
4444
import org.jacodb.ets.model.EtsAnyType
4545
import org.jacodb.ets.model.EtsArrayType
46+
import org.jacodb.ets.model.EtsBooleanLiteralType
4647
import org.jacodb.ets.model.EtsBooleanType
4748
import org.jacodb.ets.model.EtsClassType
4849
import org.jacodb.ets.model.EtsEnumValueType
@@ -53,8 +54,10 @@ import org.jacodb.ets.model.EtsLexicalEnvType
5354
import org.jacodb.ets.model.EtsLiteralType
5455
import org.jacodb.ets.model.EtsNeverType
5556
import org.jacodb.ets.model.EtsNullType
57+
import org.jacodb.ets.model.EtsNumberLiteralType
5658
import org.jacodb.ets.model.EtsNumberType
5759
import org.jacodb.ets.model.EtsRawType
60+
import org.jacodb.ets.model.EtsStringLiteralType
5861
import org.jacodb.ets.model.EtsStringType
5962
import org.jacodb.ets.model.EtsTupleType
6063
import org.jacodb.ets.model.EtsType
@@ -149,26 +152,22 @@ private object EtsTypeToDto : EtsType.Visitor<TypeDto> {
149152
return NeverTypeDto
150153
}
151154

152-
override fun visit(type: EtsLiteralType): TypeDto {
153-
val literal = when {
154-
type.literalTypeName.equals("true", ignoreCase = true) -> {
155-
PrimitiveLiteralDto.BooleanLiteral(true)
156-
}
157-
158-
type.literalTypeName.equals("false", ignoreCase = true) -> {
159-
PrimitiveLiteralDto.BooleanLiteral(false)
160-
}
161-
162-
else -> {
163-
val x = type.literalTypeName.toDoubleOrNull()
164-
if (x != null) {
165-
PrimitiveLiteralDto.NumberLiteral(x)
166-
} else {
167-
PrimitiveLiteralDto.StringLiteral(type.literalTypeName)
168-
}
169-
}
170-
}
171-
return LiteralTypeDto(literal = literal)
155+
override fun visit(type: EtsStringLiteralType): TypeDto {
156+
return LiteralTypeDto(
157+
literal = PrimitiveLiteralDto.StringLiteral(type.value)
158+
)
159+
}
160+
161+
override fun visit(type: EtsNumberLiteralType): TypeDto {
162+
return LiteralTypeDto(
163+
literal = PrimitiveLiteralDto.NumberLiteral(type.value)
164+
)
165+
}
166+
167+
override fun visit(type: EtsBooleanLiteralType): TypeDto {
168+
return LiteralTypeDto(
169+
literal = PrimitiveLiteralDto.BooleanLiteral(type.value)
170+
)
172171
}
173172

174173
override fun visit(type: EtsClassType): TypeDto {

‎usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt‎

Lines changed: 19 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -3,17 +3,20 @@ package org.usvm.machine.types
33
import org.jacodb.ets.model.EtsAliasType
44
import org.jacodb.ets.model.EtsAnyType
55
import org.jacodb.ets.model.EtsArrayType
6+
import org.jacodb.ets.model.EtsBooleanLiteralType
67
import org.jacodb.ets.model.EtsBooleanType
78
import org.jacodb.ets.model.EtsClassType
89
import org.jacodb.ets.model.EtsFunctionType
910
import org.jacodb.ets.model.EtsIntersectionType
1011
import org.jacodb.ets.model.EtsLiteralType
1112
import org.jacodb.ets.model.EtsNeverType
1213
import org.jacodb.ets.model.EtsNullType
14+
import org.jacodb.ets.model.EtsNumberLiteralType
1315
import org.jacodb.ets.model.EtsNumberType
1416
import org.jacodb.ets.model.EtsPrimitiveType
1517
import org.jacodb.ets.model.EtsRefType
1618
import org.jacodb.ets.model.EtsScene
19+
import org.jacodb.ets.model.EtsStringLiteralType
1720
import org.jacodb.ets.model.EtsStringType
1821
import org.jacodb.ets.model.EtsTupleType
1922
import org.jacodb.ets.model.EtsType
@@ -91,11 +94,10 @@ class TsTypeSystem(
9194
if (unwrappedSupertype is EtsPrimitiveType && unwrappedType is EtsPrimitiveType) {
9295
if (unwrappedType is EtsLiteralType) {
9396
// Literal types are subtypes of their base primitive (e.g., 'foo' <: string).
94-
return when (unwrappedType.literalTypeName) {
95-
"String" -> unwrappedSupertype is EtsStringType
96-
"Number" -> unwrappedSupertype is EtsNumberType
97-
"Boolean" -> unwrappedSupertype is EtsBooleanType
98-
else -> error("Unexpected literal type name ${unwrappedType.literalTypeName}")
97+
return when (unwrappedType) {
98+
is EtsStringLiteralType -> unwrappedSupertype is EtsStringType
99+
is EtsNumberLiteralType -> unwrappedSupertype is EtsNumberType
100+
is EtsBooleanLiteralType -> unwrappedSupertype is EtsBooleanType
99101
}
100102
}
101103

@@ -224,7 +226,8 @@ class TsTypeSystem(
224226
is EtsUnionType -> true // unions can always drop a branch
225227
is EtsIntersectionType -> true // intersections can always add a constraint
226228
is EtsAnyType,
227-
is EtsUnknownType -> true // top types can always have subtypes
229+
is EtsUnknownType,
230+
-> true // top types can always have subtypes
228231
else -> false
229232
}
230233
}
@@ -239,7 +242,8 @@ class TsTypeSystem(
239242
is EtsNumberType,
240243
is EtsStringType,
241244
is EtsBooleanType,
242-
is EtsLiteralType -> true // primitives/literals always final
245+
is EtsLiteralType,
246+
-> true // primitives/literals always final
243247
is EtsClassType -> false
244248
else -> false // others can always be specialized
245249
}
@@ -250,11 +254,13 @@ class TsTypeSystem(
250254
return when (t) {
251255
is EtsNeverType -> false // no runtime value
252256
is EtsAnyType,
253-
is EtsUnknownType -> true // may represent some value
257+
is EtsUnknownType,
258+
-> true // may represent some value
254259
is EtsLiteralType,
255260
is EtsNullType,
256261
is EtsUndefinedType,
257-
is EtsPrimitiveType -> true // literals/primitives have values
262+
is EtsPrimitiveType,
263+
-> true // literals/primitives have values
258264
is EtsUnionType -> t.types.any { isInstantiable(it) } // union has some branch value
259265
is EtsIntersectionType -> t.types.all { isInstantiable(it) } // intersection if all parts have values
260266
is EtsArrayType -> isInstantiable(t.elementType) // array if elements instantiable
@@ -270,7 +276,8 @@ class TsTypeSystem(
270276
return when (t) {
271277
is EtsPrimitiveType -> emptySequence()
272278
is EtsAnyType,
273-
is EtsUnknownType ->
279+
is EtsUnknownType,
280+
->
274281
scene.projectAndSdkClasses
275282
.asSequence()
276283
.map { it.type }
@@ -296,7 +303,8 @@ class TsTypeSystem(
296303
}
297304

298305
is EtsUnclearRefType,
299-
is EtsClassType ->
306+
is EtsClassType,
307+
->
300308
if ((t as? EtsClassType)?.signature == EtsHierarchy.OBJECT_CLASS.signature) { // TODO change it
301309
scene.projectAndSdkClasses.asSequence().map { it.type } + EtsStringType + EtsAnyType
302310
} else {

0 commit comments

Comments
 (0)