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
Copy Markdown
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
Copy Markdown
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
Copy Markdown
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
Copy Markdown
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
Copy Markdown
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
Copy Markdown
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
Copy Markdown
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
Copy Markdown
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
Copy Markdown
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 referenced this pull request in wellesley-prog-sys/wasmtime Sep 22, 2024
Generate the `SubS` case for `AluRRR` instructions.

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

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

Updates #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
avanhatt referenced this pull request in wellesley-prog-sys/wasmtime Apr 8, 2026
…nce#12779)

If we emit a value label alias for an instruction that isn't lowered,
then that signals that the value has been optimised out. However, since
it is an alias we know that the value also exists in an earlier vreg, so
we should skip the alias and use that instead.

This situation occurs often for memory indexes on AArch64. We translate
memory stores into instructions such as:

    v8 = iconst.i32 42
    v9 = uextend.i64 v6
    v10 = load.i64 notrap aligned readonly can_move checked v0+56
    v11 = iadd v10, v9
    v12 = iconst.i64 20
    v13 = iadd v11, v12  ; v12 = 20
    store little heap v8, v13  ; v8 = 42

Here, v6 is a memory index (which has a label) and v9 is an
extension of the memory index (which has a label alias, added by
cast_index_to_pointer_ty()). This is lowered to:

     40c:       52800540        mov     w0, #0x2a                       // #42
     410:       f9401c41        ldr     x1, [x2, avanhatt#56]
     414:       91005021        add     x1, x1, #0x14
     418:       b8384820        str     w0, [x1, w24, uxtw]

The uextend has been folded into the str, so v9 has been optimised
out. But v6 is still present in w24, so the debuginfo should use that
instead.

This fixes the following tests for AArch64:

    native_debug::lldb::dwarf_cold_block
    native_debug::lldb::dwarf_fib_wasm
    native_debug::lldb::dwarf_fib_wasm_dwarf5
    native_debug::lldb::dwarf_fib_wasm_split4
    native_debug::lldb::dwarf_fission
    native_debug::lldb::dwarf_fraction_norm
    native_debug::lldb::dwarf_imported_memory
    native_debug::lldb::dwarf_shared_memory
    native_debug::lldb::dwarf_simple
    native_debug::lldb::dwarf_spilled_frame_base
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