Update isla-sail for current Sail, add missing isla-lib primops for RISC-V#1
Open
jahanzebkhalid-10Xe wants to merge 1 commit into
Open
Update isla-sail for current Sail, add missing isla-lib primops for RISC-V#1jahanzebkhalid-10Xe wants to merge 1 commit into
jahanzebkhalid-10Xe wants to merge 1 commit into
Conversation
…ISC-V isla-sail: fix Jib.funtype's bool->variant change, CT_bit removal, Bindings module scoping, dead opt_magic_hash reference, and the rewrite-pass list drift (vector_string_pats_to_bit_list removed, remove_vector_subrange_pats/remove_numeral_pats added and reordered) needed to compile against a current Sail against the real, unmodified sail-riscv model. isla-lib: add cancel_reservation/valid_reservation/match_reservation/ load_reservation stubs, count_trailing_zeros (+ BV::trailing_zeros), vector_init (aliases undefined_vector), and sys_enable_experimental_extensions - primops sail-riscv calls that isla-lib never implemented. Also fix check_concrete_overlap in memory.rs to use the address's own solver-tracked width instead of a hardcoded 64 bits, for non-64-bit-address targets. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
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
1 participant
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.
isla-sail: fix Jib.funtype's bool->variant change, CT_bit removal, Bindings module scoping, dead opt_magic_hash reference, and the rewrite-pass list drift (vector_string_pats_to_bit_list removed, remove_vector_subrange_pats/remove_numeral_pats added and reordered) needed to compile against a current Sail against the real, unmodified sail-riscv model.
isla-lib: add cancel_reservation/valid_reservation/match_reservation/load_reservation stubs, count_trailing_zeros (+ BV::trailing_zeros), vector_init (aliases undefined_vector), and sys_enable_experimental_extensions - primops sail-riscv calls that isla-lib never implemented. Also fixes check_concrete_overlap in memory.rs to use the address's own solver-tracked width instead of a hardcoded 64 bits, for non-64-bit-address targets.
Part of the RISC-V target-support work in 10x-Engineers/isla-testgen#1.