Skip to content

Verify sdiv#39

Merged
avanhatt merged 14 commits intoverify-mainfrom
sdiv
Mar 21, 2023
Merged

Verify sdiv#39
avanhatt merged 14 commits intoverify-mainfrom
sdiv

Conversation

@mpardesh
Copy link
Collaborator

  • the sdiv example fails the "query width used" check, but all the terms seem to explicitly want 64 bit bvs
  • the tests are a lil slow but I promise if you kill and rerun enough times they pass within a few seconds

}
if !query_width_used {
panic!("Query width unused, check rule!");
//panic!("Query width unused, check rule!");
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wouldn't land like this, but I'm not sure what the right annotations for examples/sdiv/sdiv.isle would be otherwise

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks like x should be able to be something like 32 here though, no?

rule 1 (lower (has_type (fits_in_64 ty) (sdiv x (iconst (safe_divisor_from_imm64 y)))))
       (a64_sdiv $I64 (put_in_reg_sext64 x) (imm ty (ImmExtend.Sign) y)))

@avanhatt avanhatt merged commit 37236bb into verify-main Mar 21, 2023
@avanhatt avanhatt deleted the sdiv branch March 27, 2023 14:21
avanhatt pushed a commit that referenced this pull request May 26, 2023
Many users won't need these, because they'll just grab one default clock
handle and reuse it for the rest of the program. But it should still be
possible to close a clock handle.

Also, add a simple test for the clock APIs.
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 18, 2024
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

Development

Successfully merging this pull request may close these issues.

2 participants