Skip to content

Commit 201e5f4

Browse files
committed
Support simple casts
1 parent a07c653 commit 201e5f4

File tree

3 files changed

+32
-9
lines changed

3 files changed

+32
-9
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 = "4ff7243d3a"
9+
const val jacodb = "77b83e4127"
1010
const val juliet = "1.3.2"
1111
const val junit = "5.9.3"
1212
const val kotlin = "2.1.0"

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,10 @@ import org.jacodb.ets.model.EtsAliasType
66
import org.jacodb.ets.model.EtsAnyType
77
import org.jacodb.ets.model.EtsArrayType
88
import org.jacodb.ets.model.EtsBooleanType
9+
import org.jacodb.ets.model.EtsEnumValueType
910
import org.jacodb.ets.model.EtsGenericType
1011
import org.jacodb.ets.model.EtsNullType
1112
import org.jacodb.ets.model.EtsNumberType
12-
import org.jacodb.ets.model.EtsRawType
1313
import org.jacodb.ets.model.EtsRefType
1414
import org.jacodb.ets.model.EtsScene
1515
import org.jacodb.ets.model.EtsStringType
@@ -82,12 +82,9 @@ class TsContext(
8282
TODO("Not yet implemented")
8383
}
8484
}
85+
is EtsEnumValueType -> unresolvedSort
8586
else -> {
86-
if (type is EtsRawType && type.kind == "EnumValueType") {
87-
unresolvedSort
88-
} else {
89-
TODO("${type::class.simpleName} is not yet supported: $type")
90-
}
87+
TODO("${type::class.simpleName} is not yet supported: $type")
9188
}
9289
}
9390

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

Lines changed: 28 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ import org.jacodb.ets.model.EtsPreDecExpr
5555
import org.jacodb.ets.model.EtsPreIncExpr
5656
import org.jacodb.ets.model.EtsPtrCallExpr
5757
import org.jacodb.ets.model.EtsRawType
58+
import org.jacodb.ets.model.EtsRefType
5859
import org.jacodb.ets.model.EtsRemExpr
5960
import org.jacodb.ets.model.EtsRightShiftExpr
6061
import org.jacodb.ets.model.EtsStaticCallExpr
@@ -270,8 +271,33 @@ class TsExprResolver(
270271
}
271272

272273
override fun visit(expr: EtsCastExpr): UExpr<*>? = with(ctx) {
273-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
274-
error("Not supported $expr")
274+
val resolvedExpr = resolve(expr.arg) ?: return@with null
275+
return when (resolvedExpr.sort) {
276+
fp64Sort -> {
277+
TODO()
278+
}
279+
280+
boolSort -> {
281+
TODO()
282+
}
283+
284+
addressSort -> {
285+
scope.calcOnState {
286+
val instance = resolvedExpr.asExpr(addressSort)
287+
288+
if (expr.type !is EtsRefType) {
289+
TODO("Not supported yet")
290+
}
291+
292+
pathConstraints += memory.types.evalIsSubtype(instance, expr.type)
293+
instance
294+
}
295+
}
296+
297+
else -> {
298+
error("Unsupported cast from ${expr.arg} to ${expr.type}")
299+
}
300+
}
275301
}
276302

277303
override fun visit(expr: EtsTypeOfExpr): UExpr<out USort>? = with(ctx) {

0 commit comments

Comments
 (0)