Closed
Conversation
Derive type constraints for struct types. This now allows an `instantiate` directive for example to contain a struct field. This arises in avanhatt#99 when specifying the type instantiations of a `load`, which takes `MemFlags`. Updates avanhatt#49
…iance#111) Introduces specification for CLIF load instructions, and verifies a limited subset of the `I64` load lowerings. Verifying these lowerings is a clear example of rule chaining at work. We tag the `amode*` intermediate terms with the `chain` tag. As a result the total number of expansions increases substantially to 9000+. There are a 200+ expansions of the `load_i64` rule. In order to make this work it was necessary to exclude a lot of terms for the time being with a `TODO` tag, as well as model some types as unspecified. We will need to return to these and specify them, or decide they are out of scope. Updates avanhatt#49
Upload verification results as artifacts. This could be useful for backtesting and comparison of results over time.
Generate specs for `AluRRRExtend`. Updates #35
Make `isaspec` output line length configurable, and increase it to 120. Updates avanhatt#62
Support opcode templates the the ASLp client. This uses the format implemented in mmcloughlin/aslp#4. The change is safe to land now since in the common fixed 32-bit case, the formats are the same. Updates #36
Adds library functions for manipulating opcode templates. Updates #36
Error if there are two specs on the same term. Closes avanhatt#56
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 #36 #35
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 #35
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 #36 #35 Closes bytecodealliance#120
Simplify the `should_verify` logic. Log when expansions are skipped.
Specify and verify `ineg` on AArch64. Updates #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 #34
Generate conditional select instructions `CSel` and `CSNeg`. Updates #35
Implement `Constraint::Variant` binding constraint. This implementation is not ideal: 1. Will not handle cases where we have decided to model an ISLE enum as some other type. The binding the constraint applies to is assumed to have enum value type. 2. Does not confirm that the enum type matches the enum type of the binding constraint. The prior layers should have confirmed this won't happen. Updates avanhatt#48
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 #34
) Generate the `AMode.Unscaled` cases in the load specifications. Updates avanhatt#49 #35
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 #34
Adds macro support to the spec language. Syntax for definitions: ``` (macro (bvone n) (zero_ext n #b1)) ``` Expansion: ``` (bvone! 64) ``` This PR also adds a couple of macros to a new `prelude_spec.isle`. Closes avanhatt#39
Updates the `int2bv` operator so its width can be an expression. The current behavior was problematic in bytecodealliance#135, where it prevents the use of `int2bv` in a macro expansion. This PR brings `int2bv` in line with other operators taking an integer width, such as zero extension.
Add a `low_bits_mask!` macro and use it to simplify the `move_wide_const_...` specs a little. Updates bytecodealliance#134
Migrate the logic in the `veri` binary into a `Runner` class. This is intended to make testing a little easier by providing a library entry point into the verifier. Updates avanhatt#79
Improves readability of verifier output by printing the term name of a chosen type instantiation.
Provides basic support for file-based tests, with a single examples of passing and broken test cases. Updates avanhatt#79
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 #35
Output SMT2 log files to an output log directory structure.
Support solver selection on a per-expansion basis. The runner now supports "solver rules" consisting of an expansion predicate and a solver backend. These can be provided on the command line with e.g. `--solver-rule z3=tag:float`. It also sets up default selection rules with an explicit tag, so `solver_z3` and `solver_cvc5`. Updates bytecodealliance#275
Rust macro for ISA spec configuration that simplifies the common cases.
…e#340) Move ISA instruction definitions to separate file.
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
4 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.
No description provided.