Support IBI variation in Ocaml offline backend - #149
Merged
Conversation
agle
approved these changes
May 28, 2026
agle
left a comment
agle
left a comment
There was a problem hiding this comment.
very cool, a completely normal and expectable set of changes. lmk if you want me to handle pushing the opam package when you're done
|
|
||
| let write_epilogue use_pc fid st = | ||
| let conv_pc = "let pc = (mkBits (Z.of_int 64) (Z.of_int pc)) in" in | ||
| let conv_pc = "let pc = (I.mkBits (I.bigint_of_int 64) (I.bigint_of_int pc)) in" in |
There was a problem hiding this comment.
This is the only reason to for constraining Asl_ibi.bitvector = Primops.bitvector right? Could just shove the conversion in the IBI too, or take a bv and make the caller do it.
Member
Author
There was a problem hiding this comment.
I changed it so this function is only generated in the ASL instantiation of the IBI. I can rename it to make it more obvious.
extract ibi names dynamically fix offline_coverage reference and make asli optional dependency use offlineASL_runner module directly add stateful reset_ir and get_ir functions
Member
Author
|
Oh yeah if you can do the opam stuff that would be really good, thanks |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Uses first-class modules in all the instruction class lifting functions. The generated files now look something like this:
This allows for parametrisation without module functors, as described in https://ocaml.org/manual/5.4/firstclassmodules.html#p:fst-mod-advexamples
The implementation is what you'd expect, with a bunch of work to define the IBI and distinguish IBI functions from instruction class functions. This is because we have to use
I.f_functionnamewhen calling IBI functions and we have to propagate the(module I)when calling instruction class functions (though, maybe this could be avoided with anopen....)In doing so, we are able to make ASLp an optional dependency of the offline lifter package - it's only needed if you want to use the ASL IBI, otherwise you can BYO.