Skip to content

imm12 add#42

Merged
avanhatt merged 5 commits intoverify-mainfrom
imm12new
Jan 24, 2023
Merged

imm12 add#42
avanhatt merged 5 commits intoverify-mainfrom
imm12new

Conversation

@mpardesh
Copy link
Collaborator

Works, but since type inference prioritizes known bit widths, it thinks the args to iadd have whatever width imm12 has. This is causing "query width unused."

@mpardesh mpardesh changed the title imm12 with 13 bits imm12 add Jan 19, 2023
;;@ (= (extract 2 0 (arg)) (0i3:bv))
;;@ )),
;;@ (= (arg) (ret))
;;@ ))
Copy link
Owner

Choose a reason for hiding this comment

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

To get around the "query width unused", we need more complicated logic for (= (arg) (ret)): Imm12 can be a different width from Value.

On option would be something like:
(= (arg) (conv_to (widthof (arg)) (ret))

Copy link
Owner

@avanhatt avanhatt left a comment

Choose a reason for hiding this comment

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

Looks good to me!

A weird subset of tests are actually failing, but I don't see why from this PR.

@mpardesh
Copy link
Collaborator Author

Looks good to me!

A weird subset of tests are actually failing, but I don't see why from this PR.

Should I wait to merge? Do you think it might be due to the iconst changes or the extraction bug?

@avanhatt
Copy link
Owner

Let me try to run locally first, will report back in a few.

(
"Imm12".to_owned(),
annotation_ir::Type::BitVectorWithWidth(12),
annotation_ir::Type::BitVectorWithWidth(24),
Copy link
Owner

Choose a reason for hiding this comment

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

Looks like this change is making the failing tests fail locally, too. Doing a quick pass to see if I can update them.

@avanhatt
Copy link
Owner

No tests failing, but these two failed to terminate after 3 hours in CI:

test test_iadd_from_file 
test test_udiv 

@mpardesh
Copy link
Collaborator Author

No tests failing, but these two failed to terminate after 3 hours in CI:

test test_iadd_from_file 
test test_udiv 

I've definitely run all the iadd examples and they've passed. I think this is due to hanging solver. The same might be true for udiv though I'm less sure about that. In any case, this hanging solver is making it hard to tell which tests are really broken and which just look broken.

@avanhatt
Copy link
Owner

Things now work locally, so force merging

@avanhatt avanhatt merged commit 6e8fb32 into verify-main Jan 24, 2023
avanhatt pushed a commit that referenced this pull request May 26, 2023
This gets us another step closer to running the Wasmtime tests.
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Sep 22, 2024
Generate the `SubS` case for `AluRRR` instructions.

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

Updates #35 avanhatt#42 avanhatt#62
avanhatt added a commit to wellesley-prog-sys/wasmtime that referenced this pull request Apr 9, 2025
Implement the encoded spec ops `clz` and `rev`. Use them to verify the
`clz` and `ctz` lowerings.

Updates avanhatt#42 #34

Co-authored-by: Vaishu Chintam <jc103@wellesley.edu>
avanhatt pushed a commit that referenced this pull request Jan 11, 2026
Allow to map host directory as arbitary guest path
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