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 named rules, allowing more sharing for lower.isle #35

Closed
avanhatt opened this issue Jan 16, 2023 · 1 comment
Closed

Support named rules, allowing more sharing for lower.isle #35

avanhatt opened this issue Jan 16, 2023 · 1 comment

Comments

@avanhatt
Copy link
Owner

Cut down on how much we repeat annotations

@avanhatt avanhatt moved this from Todo to Nice to have in Implementation tasks Jan 23, 2023
@avanhatt
Copy link
Owner Author

Fixed in #62

@github-project-automation github-project-automation bot moved this from Nice to have to Done in Implementation tasks Apr 13, 2023
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Sep 22, 2024
Generate the `SubS` case for `AluRRR` instructions.

Updates avanhatt#42 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Sep 22, 2024
Generate the spec for AluRRRR forms from ASLp.

This PR only defines the `MAdd` and `MSub` opcodes which are in use at
the moment.

Updates avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Sep 23, 2024
This PR changes the `isaspec` tool to generate multiple files.

As we extend the use of ASLp, we are generating a lot of spec code. This
is especially true for `BitRR` which we'll be adding soon. Allowing the
tool to generate more than one file will hopefully make them a bit more
manageable.

Updates avanhatt#35 avanhatt#62
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Sep 23, 2024
This PR allows `IsleCompilation` configurations to provide directory
inputs. Directory inputs are expanded to the list of all `.isle` files
contained in them.

Updates avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Sep 23, 2024
Generate ASLp-based spec for the `BitRR` instruction `Cls` opcode.

Updates avanhatt#35 avanhatt#42 avanhatt#62
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Generates the remaining opcodes for `AluRRRR`.

Updates avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Outputs a code generation warning to the top of ISA specs derived from
ASLp.

Updates avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Generate `aslp` test cases for load instructions.

Updates avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Generate spec for the `MInst.Extend` instruction.

Updates avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Support generating ASLp specifications that split based on an enum
`match`.

Update the existing `MInst` specs to use this feature where possible.

Updates avanhatt#48 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Generate specifications from ASLp for AArch64 load operations for a
subset of addressing modes.

Define `loaded_value` and `isa_load` state variables.

Updates avanhatt#49 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Provide a mechanism for generated specs to declare which state fields
they modify, and use it in the generated load specs.

Updates avanhatt#49 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Generate AArch64 load specs for `AMode.RegScaledExtended` and
`AMode.RegExtended` addressing modes.

Updates avanhatt#49 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Change generation of specs split on match cases so the requires uses
`match` also.

The change in avanhatt#101 is actually broken, though it did't trigger any
errors because the specs are unused on the main branch. When working on
avanhatt#99 the error does manifest. Specifically, the error is in the generated
requires clauses:


https://github.com/mmcloughlin/veriisle-wasmtime/blob/432bd4a86635cd82c76857689ff67c77e99cbd4e/cranelift/codegen/src/isa/aarch64/spec/loads.isle#L111-L113

This references the variable `extendop`, which does not exist. It
doesn't exist because it's a field of the enum variant, and we haven't
brought its fields into scope.

This change updates the match case spec generation to use a match in the
requires as well. This is probably a cosmetic regression avanhatt#62. If we care
to we could update this in future to only use a match statement in the
case where the child requires accesses the variable, but it doesn't seem
worth it for now.

Updates avanhatt#35 avanhatt#48
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Change the `isa_load` state to measure load size in bits instead of
bytes.

Updates avanhatt#49 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Generate specs for `AluRRRExtend`.

Updates avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Generate `AluRRImm12` spec from ASLp.

This is the first requiring symbolic opcodes, so there are substantial
changes to support it:

* Updates ASLp dependency to fork containing experimental symbolic
opcode support
mmcloughlin/aslp@e5190a0
* Introduces `Bits` type to `isaspec` for manipulating opcode bitvectors
with symbolic fields.
* Generating ASLp semantics from an opcode template
* Validating an assembly template against the Cranelift assembler
* Updating verification model of `Imm12` to a struct type, and updating
related specs.

Updates avanhatt#36 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Simplify nested extension spec expressions generated by ASLp to spec
conversion.

This pattern comes up a lot in the conversion of `AluRRRShift`
instructions, and is already present in some of the instruction specs.

Updates avanhatt#63 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Generate `AluRRRShift` spec with ASLp.

This is the second example of a spec that relies on symbolic opcodes,
but it's slightly more challenging because the shift amount determines
the size of the symbolic field. Not only that, but the spec cases split
on `shiftop`, which is a struct type. In addition, the `lshl_from_imm64`
spec needed to be fixed.

Updates avanhatt#36 avanhatt#35
Closes bytecodealliance#120
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
Generate conditional select instructions `CSel` and `CSNeg`.

Updates avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 9, 2024
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 18, 2024
)

Generate the `AMode.Unscaled` cases in the load specifications.

Updates avanhatt#49 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 18, 2024
Generate specifications for `Store<N>` instructions. Define `isa_store`
state variable.

Slight refactor to enable sharing the amode case enumeration logic with
loads.

Updates avanhatt#49 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 18, 2024
Generates the flag-setting opcodes for `AluRRImm12`.

Relies on the CSE fix in ASLp added in
mmcloughlin/aslp#5.

Updates avanhatt#36 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 18, 2024
Verify the `iabs` rules.

This did uncover an oddity that the `iabs` 32-bit and lower cases emit
extend
instructions from 32-to-32 bits. This failed at first since our ASLp
generation only generated cases with `from_bits < to_bits`.

Updates avanhatt#34 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 18, 2024
Generate conditional-set and conditional-set-mask instruction specs.

Update avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 18, 2024
Generate conditional compare instruction specs.

Updates avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
Generate spec for `MInst.VecLanes`, required for `popcnt` lowering.

Updates avanhatt#34 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
Generate the `MovToFpu` specs, required for `popcnt`.

Updates avanhatt#34 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
Implement conditional branch joining logic for if/else branches that
assign to distinct targets.

Until now all conditionals in ASLp programs have assigned to the same
targets on both branches. The merging logic or "phi nodes" only
implemented the logic for this simpler case. The `VecMisc` instructions
required for `popcnt` verification include `if` statements without
`else`, and therefore fail in this step. This PR refactors the code to
handle the distinct case.

The change is a no-op on current specs.

Updates avanhatt#35 avanhatt#34
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
Generate `MovFromVec` specification, required for `popcnt`.

Updates avanhatt#34 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
Generate specs for the shift opcodes of `AluRRR` instructions.

These had previously been disabled because of an issue with the bitwidth
of shift amounts. That has since been resolved in bytecodealliance#122 so we can enable
them here without issue.

Updates avanhatt#34 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
Generate spec for `MInst.VecLanes`, required for `popcnt` lowering.

Updates avanhatt#34 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
Generate the `MovToFpu` specs, required for `popcnt`.

Updates avanhatt#34 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
Implement conditional branch joining logic for if/else branches that
assign to distinct targets.

Until now all conditionals in ASLp programs have assigned to the same
targets on both branches. The merging logic or "phi nodes" only
implemented the logic for this simpler case. The `VecMisc` instructions
required for `popcnt` verification include `if` statements without
`else`, and therefore fail in this step. This PR refactors the code to
handle the distinct case.

The change is a no-op on current specs.

Updates avanhatt#35 avanhatt#34
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
Generate `MovFromVec` specification, required for `popcnt`.

Updates avanhatt#34 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
Generate specs for the shift opcodes of `AluRRR` instructions.

These had previously been disabled because of an issue with the bitwidth
of shift amounts. That has since been resolved in bytecodealliance#122 so we can enable
them here without issue.

Updates avanhatt#34 avanhatt#35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this issue Oct 23, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
Development

No branches or pull requests

1 participant