Skip to content

More fixes for real applications #283

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

Draft
wants to merge 16 commits into
base: main
Choose a base branch
from
Draft

More fixes for real applications #283

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
89ed53e
Hacks
CaelmBleidd May 29, 2025
069cb78
More hacks
CaelmBleidd May 29, 2025
f85ef55
Some more fixes
CaelmBleidd May 30, 2025
51f5b9f
Tmp commit
CaelmBleidd May 30, 2025
545887c
Input arrays support
CaelmBleidd Jun 6, 2025
f6c17c4
Format
Lipen Jun 9, 2025
db952f6
Operators implementation
CaelmBleidd Jun 10, 2025
911e8ca
Some hacks
CaelmBleidd Jun 10, 2025
a07c653
Fix a class signature lookup
CaelmBleidd Jun 11, 2025
201e5f4
Support simple casts
CaelmBleidd Jun 11, 2025
f8fd3fa
Clear logs
CaelmBleidd Jun 11, 2025
59393c2
Add todo
CaelmBleidd Jun 11, 2025
0f18a8c
Rebase fix
CaelmBleidd Jun 18, 2025
bb4df1f
Tmp changes
CaelmBleidd Jun 19, 2025
7b1bcd8
Some fixes
CaelmBleidd Jun 20, 2025
c3e5fe0
Fix mocker return value
CaelmBleidd Jun 20, 2025
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
Prev Previous commit
Next Next commit
Support simple casts
  • Loading branch information
@CaelmBleidd
CaelmBleidd committed Jun 18, 2025
commit 201e5f4d0243019a933ca31f219cbdb3df0f37b9
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 = "4ff7243d3a"
const val jacodb = "77b83e4127"
const val juliet = "1.3.2"
const val junit = "5.9.3"
const val kotlin = "2.1.0"
Expand Down
9 changes: 3 additions & 6 deletions usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,10 @@ import org.jacodb.ets.model.EtsAliasType
import org.jacodb.ets.model.EtsAnyType
import org.jacodb.ets.model.EtsArrayType
import org.jacodb.ets.model.EtsBooleanType
import org.jacodb.ets.model.EtsEnumValueType
import org.jacodb.ets.model.EtsGenericType
import org.jacodb.ets.model.EtsNullType
import org.jacodb.ets.model.EtsNumberType
import org.jacodb.ets.model.EtsRawType
import org.jacodb.ets.model.EtsRefType
import org.jacodb.ets.model.EtsScene
import org.jacodb.ets.model.EtsStringType
Expand Down Expand Up @@ -82,12 +82,9 @@ class TsContext(
TODO("Not yet implemented")
}
}
is EtsEnumValueType -> unresolvedSort
else -> {
if (type is EtsRawType && type.kind == "EnumValueType") {
unresolvedSort
} else {
TODO("${type::class.simpleName} is not yet supported: $type")
}
TODO("${type::class.simpleName} is not yet supported: $type")
}
}

Expand Down
30 changes: 28 additions & 2 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@ import org.jacodb.ets.model.EtsPreDecExpr
import org.jacodb.ets.model.EtsPreIncExpr
import org.jacodb.ets.model.EtsPtrCallExpr
import org.jacodb.ets.model.EtsRawType
import org.jacodb.ets.model.EtsRefType
import org.jacodb.ets.model.EtsRemExpr
import org.jacodb.ets.model.EtsRightShiftExpr
import org.jacodb.ets.model.EtsStaticCallExpr
Expand Down Expand Up @@ -270,8 +271,33 @@ class TsExprResolver(
}

override fun visit(expr: EtsCastExpr): UExpr<*>? = with(ctx) {
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
error("Not supported $expr")
val resolvedExpr = resolve(expr.arg) ?: return@with null
return when (resolvedExpr.sort) {
fp64Sort -> {
TODO()
}

boolSort -> {
TODO()
}

addressSort -> {
scope.calcOnState {
val instance = resolvedExpr.asExpr(addressSort)

if (expr.type !is EtsRefType) {
TODO("Not supported yet")
}

pathConstraints += memory.types.evalIsSubtype(instance, expr.type)
instance
}
}

else -> {
error("Unsupported cast from ${expr.arg} to ${expr.type}")
}
}
}

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