Skip to content

Shifts: ishr, sshr, ushr#49

Closed
avanhatt wants to merge 13 commits intoverify-mainfrom
shifts-rebase
Closed

Shifts: ishr, sshr, ushr#49
avanhatt wants to merge 13 commits intoverify-mainfrom
shifts-rebase

Conversation

@avanhatt
Copy link
Owner

@avanhatt avanhatt commented Jan 24, 2023

Currently, two rules with immediate are still failing with infeasible assumptions. Working on it.

@avanhatt avanhatt changed the title Shifts rebase Shifts: ishr, sshr, ushr Jan 24, 2023
@avanhatt avanhatt closed this Mar 17, 2023
avanhatt pushed a commit that referenced this pull request May 26, 2023
@sunfishcode
Minor cleanups (#49)
3a49d68 
* Use `use` imports consistently.

* Rename `flags_from_descriptor_flags` to `descriptor_flags_from_flags`.

* Rename `black_box` to `obscure`.

* Make some comments be doc comments.

* Use a hyphen for compound adjectives.

* Delete an unused variable.

* Update the name of `change-file-permissions-at`.

* Use generated typedefs instead of hard-coding u64.

* Use core::hint::black_box now that it's stabilized.
avanhatt pushed a commit that referenced this pull request May 26, 2023
@sunfishcode
Minor cleanups (#49)
44eebc5 
* Use `use` imports consistently.

* Rename `flags_from_descriptor_flags` to `descriptor_flags_from_flags`.

* Rename `black_box` to `obscure`.

* Make some comments be doc comments.

* Use a hyphen for compound adjectives.

* Delete an unused variable.

* Update the name of `change-file-permissions-at`.

* Use generated typedefs instead of hard-coding u64.

* Use core::hint::black_box now that it's stabilized.
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 9, 2024
@mmcloughlin
isle: unify provide/require spec parsing (avanhatt#89)
f08d035 
This PR makes a minor tweak to the ISLE `spec` parsing to unify how
`provide` and `require` fields are parsed.

The intention is to make it slightly cleaner to parse additional fields,
such as to support state modeling avanhatt#49. Doing this in a separate PR just
to verify this change is valid.
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 9, 2024
@mmcloughlin
verifier: state variables (avanhatt#91)
313127d 
Add global state variables accessible from specs.

State variables may declare a `default`. Specs may also declare which
state variables they modify. If no specs in an expansion modify a state
variable, the default is applied.

Updates avanhatt#49
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 9, 2024
@mmcloughlin
isaspec: generate aarch64 loads (avanhatt#92)
8e69949 
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 #35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 9, 2024
@mmcloughlin
isaspec: declare modified state (avanhatt#93)
314f8ea 
Provide a mechanism for generated specs to declare which state fields
they modify, and use it in the generated load specs.

Updates avanhatt#49 #35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 9, 2024
@mmcloughlin
isaspec: generate loads with extended addressing modes (avanhatt#101)
3cc5151 
Generate AArch64 load specs for `AMode.RegScaledExtended` and
`AMode.RegExtended` addressing modes.

Updates avanhatt#49 #35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 9, 2024
@mmcloughlin
isaspec: record load size in bits (bytecodealliance#104)
a478856 
Change the `isa_load` state to measure load size in bits instead of
bytes.

Updates avanhatt#49 #35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 9, 2024
@mmcloughlin
spec: unspecified type (bytecodealliance#107)
84e2364 
Introduces an explicit unspecified type in the spec language.

This is motivated by work to model memory operations avanhatt#99, and in
particular the use of the `AMode` enum and its many variants. Some of
the variants are unused at the moment. The unspecified type is intended
to allow us to define _some_ model for them, and therefore satisfy type
inference. However, unspecified type is not allowed to be used for
anything non-trivial, so we would be alerted in future if we need to
revise the model to a correct type.

Updates avanhatt#48 avanhatt#49
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 9, 2024
@mmcloughlin
verifier: type constraints for structs (bytecodealliance#109)
c5f1787 
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
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 9, 2024
@mmcloughlin
aarch64: verify limited subset of 64-bit load expansions (bytecodeall…
9a29952 
…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
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 18, 2024
@mmcloughlin
aarch: verify loads using MovWide (bytecodealliance#131)
000bfa5 
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
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 18, 2024
@mmcloughlin
isaspec: generate load specs with AMode.Unscaled (bytecodealliance#132
33d5850 
)

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

Updates avanhatt#49 #35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 18, 2024
@mmcloughlin
aarch64: verify more load expansions (bytecodealliance#133)
0ebc5a2 
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
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 18, 2024
@mmcloughlin
isaspec: generate Store<N> specs (bytecodealliance#140)
20c2281 
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
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 23, 2024
@mmcloughlin
isaspec: generate memory operations with AMode.UnsignedOffset (byte…
c98e98e 
…codealliance#168)

Generate load/store specs using `AMode.UnsignedOffset`.

Updates #36 avanhatt#49 #35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 23, 2024
@mmcloughlin @avanhatt
isaspec: generate memory operations with AMode.UnsignedOffset (byte…
ec771c1 
…codealliance#168)

Generate load/store specs using `AMode.UnsignedOffset`.

Updates #36 avanhatt#49 #35
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Apr 9, 2025
@mmcloughlin
aarch64: verify udiv (bytecodealliance#221)
dcb32f6 
Verify `udiv` rules.

This approach improves on the prior verificaiton of divide instructions,
since we can now use state to model traps. We do so by introducing two
flags: one for an expected trap in CLIF, and a second for a trap on the
execution side. The post-condition for `lower` is updated to require
that a trap must happen on both sides or neither.

Updates #34 avanhatt#49
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Apr 9, 2025
@mmcloughlin
veri: print state in counter-example models (bytecodealliance#231)
81ec1bc 
Include state variables in counter-example printing.

Updates avanhatt#49
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Apr 9, 2025
@mmcloughlin
veri: conditional state modification (bytecodealliance#232)
1224545 
Extend state modification clauses to optionally specify a condition
variable.

The default spec for a state will only apply when none of its condition
variables hold.

Updates avanhatt#49
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Apr 9, 2025
@mmcloughlin
aarch64: specs for verification of broken sdiv lowering (bytecodeal…
448703f 
…liance#233)

Attempt verification of the `sdiv` rule, which is relatively complex
given:

* Two conditions under which it can trap: divide by zero, and the
unrepresentable signed case `(-2^{N-1})/(-1)`.
* A delicate sequence of instructions to perform the checks, depending
on flags behavior.
* Multiple instructions in an expansion modifying the same state,
therefore the first use of conditional state modification bytecodealliance#232.

This PR adds specs required to verify this rule, and has uncovered an
apparent bug! The overflow check used to detect the unrepresentable case
only works in the 32/64-bit cases, and breaks in 8/16. The bug is filed
as bytecodealliance#9537.

In order to land the specs and proceed the rule has been marked with the
`broken` tag, and `broken` cases excluded from the CI verification run.

Updates #34 avanhatt#49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@avanhatt