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

Custom pre/postconditions for llvm_ffi_setup #1953

Open
qsctr opened this issue Oct 6, 2023 · 0 comments
Open

Custom pre/postconditions for llvm_ffi_setup #1953

qsctr opened this issue Oct 6, 2023 · 0 comments
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: feature request Issues requesting a new feature or capability
Milestone

Comments

@qsctr
Copy link
Contributor

qsctr commented Oct 6, 2023

Provide the ability to specify custom pre/postconditions for the LLVM setup generated by llvm_ffi_setup.

Possible approaches are:

  • Have a version of llvm_ffi_setup that outputs as text the setup script that it generates. Then the user can manually edit it to add any extra things they need. However this may result in less maintainable code (like the problem described in Refactor skeleton / boilerplate generation #668). Note: this functionality may be useful in general outside of this use case, just to see what exactly the command is generating. However this is complicated by the fact that currently the command is just directly running the underlying Haskell computations for setting up crucible (that is, the LLVMSetup value that it generates represents just a Haskell computation and not a piece of SAWScript source code), so we would need to generate the SAWScript code separately or abstract it enough that it can do both.
  • Have a way to pass additional arguments to llvm_ffi_setup that specify pre/postconditions.
  • Decompose llvm_ffi_setup into multiple steps which are sequenced together and which allow specifying pre/postconditions in between, similar to the solution in Refactor skeleton / boilerplate generation #668.

Personally I feel like the second and third options are nicer than the first, but we would have to think about how exactly to define the interface.

@qsctr qsctr added type: enhancement Issues describing an improvement to an existing feature or capability type: feature request Issues requesting a new feature or capability labels Oct 6, 2023
@sauclovian-g sauclovian-g added subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm and removed type: enhancement Issues describing an improvement to an existing feature or capability labels Nov 7, 2024
@sauclovian-g sauclovian-g added this to the Someday milestone Nov 7, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: feature request Issues requesting a new feature or capability
Projects
None yet
Development

No branches or pull requests

2 participants