SMT model pretty-printing #34

avanhatt · 2023-01-16T19:43:08Z

Parse variable names back to something that looks like more the input ISLE, have options to show everything as hex, binary, or both.

avanhatt · 2023-03-01T15:25:29Z

Added in #52

Quick implementation of `bitselect`, `bnot` basically worked out-of-the-box! Updates avanhatt#34

Specify and verify `ineg` on AArch64. Updates avanhatt#34

Some of the CLIF term specs had incomplete type instantiations. This PR populates more complete lists. For unclear reasons this triggers some of the verification solver calls to take a long time on 16-bit instantiations. This would need more investigation. For now, this PR drops the solver timeout to 10 seconds so the timeouts don't take as long. Updates avanhatt#34

Verify `load_i64` expansions involving `MovWide` instructions. We added `MovWide` ASLp specs in bytecodealliance#127. This PR provides additional specs to utilize them. Updates avanhatt#49 avanhatt#34

Expand verification coverage of load rules. Includes the 8/16/32-bit cases. Builds on bytecodealliance#132 to verify `AMode.Unscaled` cases. Port over specs for `{s,u}extend` to cover `load` expansions involving extensions. Updates avanhatt#49 avanhatt#34

Provide specs for store rules and verify a subset of expansions. Updates avanhatt#34

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

Verify `imul`, `smulhi` and `umulhi` rules. Updates avanhatt#34

Verify rules involving `bxor`. Updates avanhatt#34

Model the `Reg` type on AArch64 as unknown bitvector width. Reverses bytecodealliance#108. The motivation for this is the need to model vector intructions, where `Reg` is also used to represent ARM `Z` 128-bit registers. The type inference problems that necessitated the 64-bit type before have now been fixed by a combination of bytecodealliance#167 and bytecodealliance#171. Updates avanhatt#46 avanhatt#34

Generate spec for `MInst.VecLanes`, required for `popcnt` lowering. Updates avanhatt#34 avanhatt#35

Generate the `MovToFpu` specs, required for `popcnt`. Updates avanhatt#34 avanhatt#35

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

Generate `VecMisc` count opcode spec, required for popcount verification. Updates avanhatt#34

Verify a subset of CLIF `icmp` lowerings. Updates avanhatt#34

Verifies the `iadd_extend_*` rules. The main challenge here was specifying the `extended_value_from_value` extractor which is polymorphic on its input and output widths. Updates avanhatt#34

Generate `MovFromVec` specification, required for `popcnt`. Updates avanhatt#34 avanhatt#35

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

Generate the `VecRRR` `Addp` spec case. Updates avanhatt#34 avanhatt#35

Adds verification for `ishl` lowerings. Updates avanhatt#34