-
Notifications
You must be signed in to change notification settings - Fork 25
[TS] Support PtrCall #311
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
base: main
Are you sure you want to change the base?
[TS] Support PtrCall #311
Conversation
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
Dismissed
Show dismissed
Hide dismissed
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Pull Request Overview
This PR introduces basic support for pointer-based lambda calls (PtrCallExpr
) in the TypeScript interpreter and state, along with tests for local lambdas. Key changes include:
- Adding a new test case and sample (
callLocalLambda
) to validate pointer call support for non-capturing lambdas. - Extending
TsState
,TsMethodResult
,TsInterpreter
, andTsExprResolver
to track method references and resolve/call lambdas via pointers. - Consolidating mock call logic into a new
mockMethodCall
helper inorg.usvm.api.TsMock
.
Reviewed Changes
Copilot reviewed 9 out of 9 changed files in this pull request and generated 2 comments.
Show a summary per file
File | Description |
---|---|
usvm-ts/src/test/resources/samples/Call.ts | Add callLocalLambda sample method |
usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt | Add test call local lambda JUnit test |
usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt | Fix lastStmt getter and swap args for RegularCall |
usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt | Introduce method2ref /associatedMethods maps and getMethodRef |
usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt | Change Success from sealed class to interface |
usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | Refactor call handling to use mockMethodCall and doWithState |
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | Implement visit(EtsPtrCallExpr) and enhance field-ref logic |
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsSimpleValueResolver.kt | Resolve anonymous-method locals and register pointer refs |
usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt | Change instance from nullable to non-nullable |
usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt | Add mockMethodCall helper function |
Comments suppressed due to low confidence (2)
usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt:62
- [nitpick] The property name 'method2ref' is ambiguous; consider renaming it to 'methodToRefMap' for clarity.
var method2ref: UPersistentHashMap<EtsMethod, UConcreteHeapRef> = persistentHashMapOf(),
usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt:63
- [nitpick] The property name 'associatedMethods' is not descriptive of its mapping direction; consider renaming it to 'refToMethodMap'.
var associatedMethods: UPersistentHashMap<UConcreteHeapRef, EtsMethod> = persistentHashMapOf(),
This PR adds the support for
PtrCallExpr
.Currently, only local (non-input) lambda calls are supported. In IR, such calls are represented via
PtrCallExpr(ptr)
, whereptr
is a local with%AM
prefix. Local's name corresponds to the anonymous method name, which is auto-generated for each lambda in the source code. We try to resolve this method uniquely, other cases are not yet supported.Note that if the lambda is actually a closure, it should receive all captured variables as arguments (more importantly, those args go before normal args!).
Since the correspondingLexicalEnvType
is not yet supported, we also do not have a proper support for closures, yet.Since more complex cases with PtrCall are inter-connected with closures, this PR also includes some support for closures. Lately, we introduced the support for
LexicalEnvType
andClosureFieldRef
in the model, and now USVM can handle captured locals for closures. Currently, on the call-site, we allocate a "closure object", fill its "fields" with captured locals, and save it inTsState
. In the caller, when resolvingClosureFieldRef
(which is actually a simplifiedInstanceFieldRef
), we just read the necessary fields from the saved object.