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 https://github.com/GaloisInc/saw-script/issues/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 https://github.com/GaloisInc/saw-script/issues/1039), so calling the Python compositional_extract function with JVM verification would be an error.
Currently, the
llvm_extractfamily 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 https://github.com/GaloisInc/saw-script/issues/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
extractandcompositional_extractPython functions, which choose the appropriate language backend under the hood (e.g.,llvm_extractfor LLVM orjvm_extractfor JVM). Not all language backends would be supported at this time—for instance, there is currently nojvm_compositional_extractfunction (see https://github.com/GaloisInc/saw-script/issues/1039), so calling the Pythoncompositional_extractfunction with JVM verification would be an error.