Skip to content
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

Support llvm_extract, llvm_compositional_extract, jvm_extract, etc. in the Python bindings #2092

Open
RyanGlScott opened this issue Aug 16, 2024 · 0 comments
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm subsystem: saw-python Related to the Python bindings for the RPC SAW server subsystem: saw-remote-api Issues related to the SAW server and its RPC bindings type: feature request Issues requesting a new feature or capability
Milestone

Comments

@RyanGlScott
Copy link
Contributor

RyanGlScott commented Aug 16, 2024

Currently, the llvm_extract family of SAWScript commands do not have counterparts in the SAW Python bindings. I would like to ensure feature parity between SAWScript and Python when adding support for MIR versions of these commands (see #2085), and this issue is a prerequisite for that.

In the spirit of the existing design of the Python bindings, I propose that we add extract and compositional_extract Python functions, which choose the appropriate language backend under the hood (e.g., llvm_extract for LLVM or jvm_extract for JVM). Not all language backends would be supported at this time—for instance, there is currently no jvm_compositional_extract function (see #1039), so calling the Python compositional_extract function with JVM verification would be an error.

@RyanGlScott RyanGlScott added subsystem: crucible-jvm Issues related to Java verification with crucible-jvm subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm subsystem: saw-remote-api Issues related to the SAW server and its RPC bindings type: feature request Issues requesting a new feature or capability labels Aug 16, 2024
@sauclovian-g sauclovian-g added the subsystem: saw-python Related to the Python bindings for the RPC SAW server label Nov 8, 2024
@sauclovian-g sauclovian-g added this to the 2025T1 milestone Nov 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm subsystem: saw-python Related to the Python bindings for the RPC SAW server subsystem: saw-remote-api Issues related to the SAW server and its RPC bindings type: feature request Issues requesting a new feature or capability
Projects
None yet
Development

No branches or pull requests

2 participants