[TS] Support await#303
Conversation
Currently fail
There was a problem hiding this comment.
Pull Request Overview
Adds full support for await expressions in the TypeScript machine by tracking promise state, wiring executors, and extending the interpreter and state. It also introduces two comprehensive test samples (Async.ts and Async2.ts) covering a variety of async/await and promise patterns.
- Introduce
promiseStatesandpromiseExecutorsinTsStatefor tracking. - Implement
EtsAwaitExprhandling and staticPromise.resolve/rejectinTsExprResolver. - Add extensive async/await test suites under
src/test/resources/samples.
Reviewed Changes
Copilot reviewed 16 out of 16 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| usvm-ts/src/test/resources/samples/Async2.ts | New test cases for chaining, error handling, Promise.all/race, nested awaits, etc. |
| usvm-ts/src/test/resources/samples/Async.ts | New test cases for basic promise creation, awaiting rejections, and top-level await cases. |
| usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | Handle EtsAwaitExpr, Promise constructor, and static resolve/reject calls. |
| usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsPromise.kt | Core promise utilities (isResolved, markResolved, etc.). |
| usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt | Added persistent maps promiseStates and promiseExecutors and their accessors. |
Comments suppressed due to low confidence (3)
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt:783
- [nitpick] The logic for handling static
Promise.resolve/rejectand memberresolve/rejectis nearly identical. Extract into a shared helper to reduce duplication.
if (expr.callee.name == "resolve" || expr.callee.name == "reject") {
usvm-ts/src/test/resources/samples/Async2.ts:6
- This method uses
awaitbut isn't declaredasync. Addasyncto its signature (e.g.async chainPromises(): Promise<number>).
chainPromises(): number {
usvm-ts/src/test/resources/samples/Async.ts:5
- This method uses
awaitwithout being markedasync. Change toasync createAndAwaitPromise(): Promise<number>.
createAndAwaitPromise(): number {
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| override fun visit(expr: EtsAwaitExpr): UExpr<out USort>? { | ||
| logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } | ||
| error("Not supported $expr") | ||
| override fun visit(expr: EtsAwaitExpr): UExpr<out USort>? = with(ctx) { |
Check warning
Code scanning / detekt
Excessive nesting leads to hidden complexity. Prefer extracting code to make it easier to understand. Warning
| // - `reject`, if present in parameters | ||
| // - `promise` == "this", should be the last | ||
| check(executor.parameters.size <= 2) { | ||
| "Executor should have at most 2 parameters (resolve and reject), but it has ${executor.parameters.size} for $executor" |
Check warning
Code scanning / detekt
Reports lines with exceeded length Warning
| // - `reject`, if present in parameters | ||
| // - `promise` == "this", should be the last | ||
| check(executor.parameters.size <= 2) { | ||
| "Executor should have at most 2 parameters (resolve and reject), but it has ${executor.parameters.size} for $executor" |
Check warning
Code scanning / detekt
Line detected, which is longer than the defined maximum line length in the code style. Warning
| promise | ||
| } | ||
|
|
||
| override fun visit(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { |
Check warning
Code scanning / detekt
Excessive nesting leads to hidden complexity. Prefer extracting code to make it easier to understand. Warning
| // TODO wrong order, ancestors are unordered | ||
| .map { graph.hierarchy.getAncestors(it) } | ||
| .map { it.first { it.methods.any { it.name == stmt.callee.name } } } | ||
| .mapNotNull { it.firstOrNull { it.methods.any { it.name == stmt.callee.name } } } |
Check warning
Code scanning / detekt
Disallow shadowing variable declarations. Warning
This PR adds support for AwaitExpr in TS machine.
Currently, only the basic case with concrete promises (created in the same execution path) is supported, i.e. "input" promises are not yet supported.
Notes