Skip to content

[TS] Adopt literal types #324

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Lipen merged 1 commit into from
Aug 20, 2025
Merged

[TS] Adopt literal types #324

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/Dependencies.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ object Versions {
const val clikt = "5.0.0"
const val detekt = "1.23.7"
const val ini4j = "0.5.4"
const val jacodb = "213f9a1aee"
const val jacodb = "f3655cbc5d"
const val juliet = "1.3.2"
const val junit = "5.9.3"
const val kotlin = "2.1.0"
Expand Down
39 changes: 19 additions & 20 deletions usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ import org.jacodb.ets.dto.VoidTypeDto
import org.jacodb.ets.model.EtsAliasType
import org.jacodb.ets.model.EtsAnyType
import org.jacodb.ets.model.EtsArrayType
import org.jacodb.ets.model.EtsBooleanLiteralType
import org.jacodb.ets.model.EtsBooleanType
import org.jacodb.ets.model.EtsClassType
import org.jacodb.ets.model.EtsEnumValueType
Expand All @@ -53,8 +54,10 @@ import org.jacodb.ets.model.EtsLexicalEnvType
import org.jacodb.ets.model.EtsLiteralType
import org.jacodb.ets.model.EtsNeverType
import org.jacodb.ets.model.EtsNullType
import org.jacodb.ets.model.EtsNumberLiteralType
import org.jacodb.ets.model.EtsNumberType
import org.jacodb.ets.model.EtsRawType
import org.jacodb.ets.model.EtsStringLiteralType
import org.jacodb.ets.model.EtsStringType
import org.jacodb.ets.model.EtsTupleType
import org.jacodb.ets.model.EtsType
Expand Down Expand Up @@ -149,26 +152,22 @@ private object EtsTypeToDto : EtsType.Visitor<TypeDto> {
return NeverTypeDto
}

override fun visit(type: EtsLiteralType): TypeDto {
val literal = when {
type.literalTypeName.equals("true", ignoreCase = true) -> {
PrimitiveLiteralDto.BooleanLiteral(true)
}

type.literalTypeName.equals("false", ignoreCase = true) -> {
PrimitiveLiteralDto.BooleanLiteral(false)
}

else -> {
val x = type.literalTypeName.toDoubleOrNull()
if (x != null) {
PrimitiveLiteralDto.NumberLiteral(x)
} else {
PrimitiveLiteralDto.StringLiteral(type.literalTypeName)
}
}
}
return LiteralTypeDto(literal = literal)
override fun visit(type: EtsStringLiteralType): TypeDto {
return LiteralTypeDto(
literal = PrimitiveLiteralDto.StringLiteral(type.value)
)
}

override fun visit(type: EtsNumberLiteralType): TypeDto {
return LiteralTypeDto(
literal = PrimitiveLiteralDto.NumberLiteral(type.value)
)
}

override fun visit(type: EtsBooleanLiteralType): TypeDto {
return LiteralTypeDto(
literal = PrimitiveLiteralDto.BooleanLiteral(type.value)
)
}

override fun visit(type: EtsClassType): TypeDto {
Expand Down
30 changes: 19 additions & 11 deletions usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,20 @@
import org.jacodb.ets.model.EtsAliasType
import org.jacodb.ets.model.EtsAnyType
import org.jacodb.ets.model.EtsArrayType
import org.jacodb.ets.model.EtsBooleanLiteralType
import org.jacodb.ets.model.EtsBooleanType
import org.jacodb.ets.model.EtsClassType
import org.jacodb.ets.model.EtsFunctionType
import org.jacodb.ets.model.EtsIntersectionType
import org.jacodb.ets.model.EtsLiteralType
import org.jacodb.ets.model.EtsNeverType
import org.jacodb.ets.model.EtsNullType
import org.jacodb.ets.model.EtsNumberLiteralType
import org.jacodb.ets.model.EtsNumberType
import org.jacodb.ets.model.EtsPrimitiveType
import org.jacodb.ets.model.EtsRefType
import org.jacodb.ets.model.EtsScene
import org.jacodb.ets.model.EtsStringLiteralType
import org.jacodb.ets.model.EtsStringType
import org.jacodb.ets.model.EtsTupleType
import org.jacodb.ets.model.EtsType
Expand Down Expand Up @@ -91,11 +94,10 @@
if (unwrappedSupertype is EtsPrimitiveType && unwrappedType is EtsPrimitiveType) {
if (unwrappedType is EtsLiteralType) {
// Literal types are subtypes of their base primitive (e.g., 'foo' <: string).
return when (unwrappedType.literalTypeName) {
"String" -> unwrappedSupertype is EtsStringType
"Number" -> unwrappedSupertype is EtsNumberType
"Boolean" -> unwrappedSupertype is EtsBooleanType
else -> error("Unexpected literal type name ${unwrappedType.literalTypeName}")
return when (unwrappedType) {
is EtsStringLiteralType -> unwrappedSupertype is EtsStringType
is EtsNumberLiteralType -> unwrappedSupertype is EtsNumberType
is EtsBooleanLiteralType -> unwrappedSupertype is EtsBooleanType
}
}

Expand Down Expand Up @@ -224,7 +226,8 @@
is EtsUnionType -> true // unions can always drop a branch
is EtsIntersectionType -> true // intersections can always add a constraint
is EtsAnyType,
is EtsUnknownType -> true // top types can always have subtypes
is EtsUnknownType,
-> true // top types can always have subtypes

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (16) (should be 12)

Check warning

Code scanning / detekt

Reports multiple space usages Warning

Unnecessary long whitespace
else -> false
}
}
Expand All @@ -239,7 +242,8 @@
is EtsNumberType,
is EtsStringType,
is EtsBooleanType,
is EtsLiteralType -> true // primitives/literals always final
is EtsLiteralType,
-> true // primitives/literals always final

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (16) (should be 12)

Check warning

Code scanning / detekt

Reports multiple space usages Warning

Unnecessary long whitespace
is EtsClassType -> false
else -> false // others can always be specialized
}
Expand All @@ -250,11 +254,13 @@
return when (t) {
is EtsNeverType -> false // no runtime value
is EtsAnyType,
is EtsUnknownType -> true // may represent some value
is EtsUnknownType,
-> true // may represent some value

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (16) (should be 12)

Check warning

Code scanning / detekt

Reports multiple space usages Warning

Unnecessary long whitespace
is EtsLiteralType,
is EtsNullType,
is EtsUndefinedType,
is EtsPrimitiveType -> true // literals/primitives have values
is EtsPrimitiveType,
-> true // literals/primitives have values

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (16) (should be 12)

Check warning

Code scanning / detekt

Reports multiple space usages Warning

Unnecessary long whitespace
is EtsUnionType -> t.types.any { isInstantiable(it) } // union has some branch value
is EtsIntersectionType -> t.types.all { isInstantiable(it) } // intersection if all parts have values
is EtsArrayType -> isInstantiable(t.elementType) // array if elements instantiable
Expand All @@ -270,7 +276,8 @@
return when (t) {
is EtsPrimitiveType -> emptySequence()
is EtsAnyType,
is EtsUnknownType ->
is EtsUnknownType,
->

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (16) (should be 12)
scene.projectAndSdkClasses
.asSequence()
.map { it.type }
Expand All @@ -296,7 +303,8 @@
}

is EtsUnclearRefType,
is EtsClassType ->
is EtsClassType,
->

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (16) (should be 12)
Comment thread
Lipen marked this conversation as resolved.
if ((t as? EtsClassType)?.signature == EtsHierarchy.OBJECT_CLASS.signature) { // TODO change it
scene.projectAndSdkClasses.asSequence().map { it.type } + EtsStringType + EtsAnyType
} else {
Expand Down