Skip to content

[TS] Add and refactor ops #322

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.

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
merged 16 commits into from
Aug 13, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
8 changes: 7 additions & 1 deletion usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,13 @@ sealed interface TsTestValue {
data object TsException : TsTestValue

data class TsBoolean(val value: Boolean) : TsTestValue
data class TsString(val value: String) : TsTestValue

data class TsString(val value: String) : TsTestValue {
override fun toString(): String {
return "${this::class.simpleName}(value=\"$value\")"
}
}

data class TsBigInt(val value: String) : TsTestValue

sealed interface TsNumber : TsTestValue {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,11 @@ fun TsExprResolver.tryApproximateInstanceCall(
}
}

// Handle 'Boolean' constructor calls
if (expr.callee.enclosingClass.name == "Boolean" && expr.callee.name == CONSTRUCTOR_NAME) {
return from(handleBooleanConstructor(expr))
}

// Handle `Promise` constructor calls
if (expr.callee.enclosingClass.name == "Promise" && expr.callee.name == CONSTRUCTOR_NAME) {
return from(handlePromiseConstructor(expr))
Expand Down Expand Up @@ -194,6 +199,15 @@ private fun TsExprResolver.handleNumberIsNaN(expr: EtsInstanceCallExpr): UBoolEx
}
}

private fun TsExprResolver.handleBooleanConstructor(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) {
check(expr.args.size == 1) {
"Boolean constructor should have exactly one argument, but got ${expr.args.size}"
}
val arg = resolve(expr.args.single()) ?: return null

mkTruthyExpr(arg, scope)
}

private fun TsExprResolver.handlePromiseConstructor(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) {
val instance = resolve(expr.instance) ?: return null
val promise = instance.asExpr(addressSort)
Expand Down
33 changes: 33 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt
Original file line number Diff line number Diff line change
Expand Up @@ -149,3 +149,36 @@ fun TsContext.mkNumericExpr(
)
)
}

fun TsContext.mkNullishExpr(
expr: UExpr<out USort>,
scope: TsStepScope,
): UBoolExpr {
// Handle fake objects specially
if (expr.isFakeObject()) {
val fakeType = expr.getFakeType(scope)
val ref = expr.extractRef(scope)
// Only check for nullish if the fake object represents a reference type.
// If it represents a primitive type (bool/number), it's never nullish.
return mkIte(
condition = fakeType.refTypeExpr,
trueBranch = mkOr(
mkHeapRefEq(ref, mkTsNullValue()),
mkHeapRefEq(ref, mkUndefinedValue())
),
falseBranch = mkFalse(),
)
}

// Regular reference is nullish if it is either null or undefined
if (expr.sort == addressSort) {
val ref = expr.asExpr(addressSort)
return mkOr(
mkHeapRefEq(ref, mkTsNullValue()),
mkHeapRefEq(ref, mkUndefinedValue())
)
}

// Non-reference types (numbers, booleans, strings) are never nullish
return mkFalse()
}
Loading