Skip to content

Commit 6566cf1

Browse files
authored
[TS] Add and refactor ops (#322)
1 parent 9b81489 commit 6566cf1

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

86 files changed

+4127
-1404
lines changed

usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,13 @@ sealed interface TsTestValue {
3333
data object TsException : TsTestValue
3434

3535
data class TsBoolean(val value: Boolean) : TsTestValue
36-
data class TsString(val value: String) : TsTestValue
36+
37+
data class TsString(val value: String) : TsTestValue {
38+
override fun toString(): String {
39+
return "${this::class.simpleName}(value=\"$value\")"
40+
}
41+
}
42+
3743
data class TsBigInt(val value: String) : TsTestValue
3844

3945
sealed interface TsNumber : TsTestValue {

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,11 @@ fun TsExprResolver.tryApproximateInstanceCall(
7272
}
7373
}
7474

75+
// Handle 'Boolean' constructor calls
76+
if (expr.callee.enclosingClass.name == "Boolean" && expr.callee.name == CONSTRUCTOR_NAME) {
77+
return from(handleBooleanConstructor(expr))
78+
}
79+
7580
// Handle `Promise` constructor calls
7681
if (expr.callee.enclosingClass.name == "Promise" && expr.callee.name == CONSTRUCTOR_NAME) {
7782
return from(handlePromiseConstructor(expr))
@@ -194,6 +199,15 @@ private fun TsExprResolver.handleNumberIsNaN(expr: EtsInstanceCallExpr): UBoolEx
194199
}
195200
}
196201

202+
private fun TsExprResolver.handleBooleanConstructor(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) {
203+
check(expr.args.size == 1) {
204+
"Boolean constructor should have exactly one argument, but got ${expr.args.size}"
205+
}
206+
val arg = resolve(expr.args.single()) ?: return null
207+
208+
mkTruthyExpr(arg, scope)
209+
}
210+
197211
private fun TsExprResolver.handlePromiseConstructor(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) {
198212
val instance = resolve(expr.instance) ?: return null
199213
val promise = instance.asExpr(addressSort)

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

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -149,3 +149,36 @@ fun TsContext.mkNumericExpr(
149149
)
150150
)
151151
}
152+
153+
fun TsContext.mkNullishExpr(
154+
expr: UExpr<out USort>,
155+
scope: TsStepScope,
156+
): UBoolExpr {
157+
// Handle fake objects specially
158+
if (expr.isFakeObject()) {
159+
val fakeType = expr.getFakeType(scope)
160+
val ref = expr.extractRef(scope)
161+
// Only check for nullish if the fake object represents a reference type.
162+
// If it represents a primitive type (bool/number), it's never nullish.
163+
return mkIte(
164+
condition = fakeType.refTypeExpr,
165+
trueBranch = mkOr(
166+
mkHeapRefEq(ref, mkTsNullValue()),
167+
mkHeapRefEq(ref, mkUndefinedValue())
168+
),
169+
falseBranch = mkFalse(),
170+
)
171+
}
172+
173+
// Regular reference is nullish if it is either null or undefined
174+
if (expr.sort == addressSort) {
175+
val ref = expr.asExpr(addressSort)
176+
return mkOr(
177+
mkHeapRefEq(ref, mkTsNullValue()),
178+
mkHeapRefEq(ref, mkUndefinedValue())
179+
)
180+
}
181+
182+
// Non-reference types (numbers, booleans, strings) are never nullish
183+
return mkFalse()
184+
}

0 commit comments

Comments
 (0)