Stream: git-wasmtime

Topic: wasmtime / PR #10979 Cranelift: `or(x, C) + (-C) --> an...

Wasmtime GitHub notifications bot (Jun 08 2025 at 08:17):

bongjunj opened PR #10979 from bongjunj:add-or-to-and to bytecodealliance:main:

<!--
Please make sure you include the following information:

• If this work has been discussed elsewhere, please include a link to that
  conversation. If it was discussed in an issue, just mention "issue #...".

• Explain why this change is needed. If the details are in an issue already,
  this can be brief.

Our development process is documented in the Wasmtime book:
https://docs.wasmtime.dev/contributing-development-process.html

Please ensure all communication follows the code of conduct:
https://github.com/bytecodealliance/wasmtime/blob/main/CODE_OF_CONDUCT.md
-->

This add or(x, C) + (-C) --> and(x, ~C)

<details>
<summary>proof.isle</summary>

(rule
  (simplify (iadd ty
              (bor ty x (iconst_s ty n))
              (iconst_s ty m)))
  (if-let m (i64_neg n))
  (band ty x (iconst ty (imm64_masked ty (i64_as_u64 (i64_not n))))))

(form
  bv_unary_8_to_64
  ((args (bv  8)) (ret (bv  8)) (canon (bv  8)))
  ((args (bv 16)) (ret (bv 16)) (canon (bv 16)))
  ((args (bv 32)) (ret (bv 32)) (canon (bv 32)))
  ((args (bv 64)) (ret (bv 64)) (canon (bv 64)))
)

(form
  bv_binary_8_to_64
  ((args (bv  8) (bv  8)) (ret (bv  8)) (canon (bv  8)))
  ((args (bv 16) (bv 16)) (ret (bv 16)) (canon (bv 16)))
  ((args (bv 32) (bv 32)) (ret (bv 32)) (canon (bv 32)))
  ((args (bv 64) (bv 64)) (ret (bv 64)) (canon (bv 64)))
)

(form
  bv_ternary_8_to_64
  ((args (bv  8) (bv  8) (bv  8)) (ret (bv  8)) (canon (bv  8)))
  ((args (bv 16) (bv 16) (bv 16)) (ret (bv 16)) (canon (bv 16)))
  ((args (bv 32) (bv 32) (bv 32)) (ret (bv 32)) (canon (bv 32)))
  ((args (bv 64) (bv 64) (bv 64)) (ret (bv 64)) (canon (bv 64)))
)


(form
  bv_ty_unary_8_to_64
  ((args Int (bv  8)) (ret (bv  8)) (canon (bv  8)))
  ((args Int (bv 16)) (ret (bv 16)) (canon (bv 16)))
  ((args Int (bv 32)) (ret (bv 32)) (canon (bv 32)))
  ((args Int (bv 64)) (ret (bv 64)) (canon (bv 64)))
)

(form
  bv_ty_binary_8_to_64
  ((args Int (bv  8) (bv  8)) (ret (bv  8)) (canon (bv  8)))
  ((args Int (bv 16) (bv 16)) (ret (bv 16)) (canon (bv 16)))
  ((args Int (bv 32) (bv 32)) (ret (bv 32)) (canon (bv 32)))
  ((args Int (bv 64) (bv 64)) (ret (bv 64)) (canon (bv 64)))
)

(form
  bv_ty_ternary_8_to_64
  ((args Int (bv  8) (bv  8) (bv  8)) (ret (bv  8)) (canon (bv  8)))
  ((args Int (bv 16) (bv 16) (bv 16)) (ret (bv 16)) (canon (bv 16)))
  ((args Int (bv 32) (bv 32) (bv 32)) (ret (bv 32)) (canon (bv 32)))
  ((args Int (bv 64) (bv 64) (bv 64)) (ret (bv 64)) (canon (bv 64)))
)

(type Type (primitive Type))
(type Value (primitive Value))
(type Imm64 (primitive Imm64))
(type Inst (primitive Inst))
(type SkeletonInstSimplification (primitive SkeletonInstSimplification))
(type IntCC extern
    (enum
        Equal
        NotEqual
        SignedGreaterThan
        SignedGreaterThanOrEqual
        SignedLessThan
        SignedLessThanOrEqual
        UnsignedGreaterThan
        UnsignedGreaterThanOrEqual
        UnsignedLessThan
        UnsignedLessThanOrEqual))

(model IntCC (enum
    (Equal #x00)
    (NotEqual #x01)
    (SignedGreaterThan #x02)
    (SignedGreaterThanOrEqual #x03)
    (SignedLessThan #x04)
    (SignedLessThanOrEqual #x05)
    (UnsignedGreaterThan #x06)
    (UnsignedGreaterThanOrEqual #x07)
    (UnsignedLessThan #x08)
    (UnsignedLessThanOrEqual #x09)))


(spec (bor ty x y)
    (provide (= (bvor x y) result))
    (require
        (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))
        (= ty (widthof x)) (= ty (widthof y))))
(decl bor (Type Value Value) Value)
(extern extractor bor bor)
(extern constructor bor bor)
(instantiate bor bv_ty_binary_8_to_64)

(spec (band ty x y)
    (provide (= (bvand x y) result))
    (require
        (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))
        (= ty (widthof x)) (= ty (widthof y))))
(decl band (Type Value Value) Value)
(extern extractor band band)
(extern constructor band band)
(instantiate band bv_ty_binary_8_to_64)

(spec (bxor ty x y)
    (provide (= (bvxor x y) result))
    (require
        (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))
        (= ty (widthof x)) (= ty (widthof y))))
(decl bxor (Type Value Value) Value)
(extern extractor bxor bxor)
(extern constructor bxor bxor)
(instantiate bxor bv_ty_binary_8_to_64)

(spec (sshr ty x y)
    (provide
        (= result
           (bvashr x
                  (bvand (conv_to (widthof y) (bvsub (int2bv 64 (widthof y))
                                                     #x0000000000000001))
                         y))))
    (require
        (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))
        (= ty (widthof x)) (= ty (widthof y))))
(decl sshr (Type Value Value) Value)
(extern extractor sshr sshr)
(extern constructor sshr sshr)
(instantiate sshr bv_ty_binary_8_to_64)

(spec (ushr ty x y)
    (provide
        (= result
           (bvlshr x
                  (bvand (conv_to (widthof y) (bvsub (int2bv 64 (widthof y))
                                                     #x0000000000000001))
                         y))))
    (require
        (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))
        (= ty (widthof x)) (= ty (widthof y))))
(decl ushr (Type Value Value) Value)
(extern extractor ushr ushr)
(extern constructor ushr ushr)
(instantiate ushr bv_ty_binary_8_to_64)

(spec (iadd ty x y)
    (provide (= result (bvadd x y)))
    (require
        (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))
        (= ty (widthof x)) (= ty (widthof y))))
(decl iadd (Type Value Value) Value)
(extern extractor iadd iadd)
(extern constructor iadd iadd)
(instantiate iadd bv_ty_binary_8_to_64)

(spec (isub ty x y)
    (provide (= result (bvsub x y)))
    (require
        (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))
        (= ty (widthof x)) (= ty (widthof y))))
(decl isub (Type Value Value) Value)
(extern extractor isub isub)
(extern constructor isub isub)
(instantiate isub bv_ty_binary_8_to_64)

(spec (imul ty x y)
    (provide (= result (bvmul x y)))
    (require
        (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))
        (= ty (widthof x)) (= ty (widthof y))))
(decl imul (Type Value Value) Value)
(extern extractor imul imul)
(extern constructor imul imul)
(instantiate imul bv_ty_binary_8_to_64)

(spec (iabs ty x)
    (provide (= result
                (if (bvsge x (conv_to (widthof x) #x0000000000000000))
                    x
                    (bvneg x))))
    (require
        (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))
        (= ty (widthof x))))
(decl iabs (Type Value) Value)
(extern extractor iabs iabs)
(extern constructor iabs iabs)
(instantiate iabs bv_ty_unary_8_to_64)


; s &:= y \pmod B,
; a &:= x \cdot 2^s \pmod{2^B}.
(spec (ishl ty x y)
    (provide
        (= result
           (bvshl x
                  (bvand (conv_to (widthof y) (bvsub (int2bv 64 (widthof y))
                                                     #x0000000000000001))
                         y))))
    (require
        (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))
        (= ty (widthof x)) (= ty (widthof y))))
(decl ishl (Type Value Value) Value)
(extern extractor ishl ishl)
(extern constructor ishl ishl)
(instantiate ishl bv_ty_binary_8_to_64)

(spec (select ty c x y)
    (provide (= result (if (= c #x00) y x)))
    (require
        (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))
        (= ty (widthof x)) (= ty (widthof y))))
(decl select (Type Value Value Value) Value)
(extern extractor select select)
(extern constructor select select)
(instantiate select bv_ty_ternary_8_to_64)

(spec (icmp ty cc x y)
    (provide
        (= result
            (switch cc
                ((IntCC.Equal)                        (if (= x y)       #x01 #x00))
                ((IntCC.NotEqual)                     (if (not (= x y)) #x01 #x00))
                ((IntCC.SignedGreaterThan)            (if (bvsgt x y)   #x01 #x00))
                ((IntCC.SignedGreaterThanOrEqual)     (if (bvsge x y)   #x01 #x00))
                ((IntCC.SignedLessThan)               (if (bvslt x y)   #x01 #x00))
                ((IntCC.SignedLessThanOrEqual)        (if (bvsle x y)   #x01 #x00))
                ((IntCC.UnsignedGreaterThan)          (if (bvugt x y)   #x01 #x00))
                ((IntCC.UnsignedGreaterThanOrEqual)   (if (bvuge x y)   #x01 #x00))
                ((IntCC.UnsignedLessThan)             (if (bvult x y)   #x01 #x00))
                ((IntCC.UnsignedLessThanOrEqual)      (if (bvule x y)   #x01 #x00)))))
    (require
        (= ty 8)
        (or (= 8 (widthof x)) (= 16 (widthof x)) (= 32 (widthof x)) (= 64 (widthof x)))
        (or
            (= cc (IntCC.Equal))
            (= cc (IntCC.NotEqual))
            (= cc (IntCC.UnsignedGreaterThanOrEqual))
            (= cc (IntCC.UnsignedGreaterThan))
            (= cc (IntCC.UnsignedLessThanOrEqual))
            (= cc (IntCC.UnsignedLessThan))
            (= cc (IntCC.SignedGreaterThanOrEqual))
            (= cc (IntCC.SignedGreaterThan))
            (= cc (IntCC.SignedLessThanOrEqual))
            (= cc (IntCC.SignedLessThan)))))

(decl icmp (Type IntCC Value Value) Value)
(extern extractor icmp icmp)
(extern constructor icmp icmp)
(instantiate icmp
  ((args Int (bv 8) (bv 8) (bv 8)) (ret (bv 8)) (canon (bv 8)))
  ((args Int (bv 8) (bv 16) (bv 16)) (ret (bv 8)) (canon (bv 16)))
  ((args Int (bv 8) (bv 32) (bv 32)) (ret (bv 8)) (canon (bv 32)))
  ((args Int (bv 8) (bv 64) (bv 64)) (ret (bv 8)) (canon (bv 64)))
)

(spec (iconst ty arg)
    (provide (= arg (zero_ext ty result)))
    (require (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))))
(decl iconst (Type Imm64) Value)
(extern constructor iconst iconst)
(extern extractor iconst ic
[message truncated]

Wasmtime GitHub notifications bot (Jun 08 2025 at 08:17):

bongjunj requested fitzgen for a review on PR #10979.

Wasmtime GitHub notifications bot (Jun 08 2025 at 08:17):

bongjunj requested wasmtime-compiler-reviewers for a review on PR #10979.

Wasmtime GitHub notifications bot (Jun 08 2025 at 09:45):

github-actions[bot] commented on PR #10979:

Subscribe to Label Action

cc @cfallin, @fitzgen

<details>
This issue or pull request has been labeled: "cranelift", "isle"

Thus the following users have been cc'd because of the following labels:

• cfallin: isle
• fitzgen: isle

To subscribe or unsubscribe from this label, edit the <code>.github/subscribe-to-label.json</code> configuration file.

Learn more.
</details>

Wasmtime GitHub notifications bot (Jun 09 2025 at 17:35):

fitzgen submitted PR review:

Thanks! Just a couple minor nitpicks below.

Out of curiosity, did you find this code pattern in the wild? Synthesize it? Something else?

Wasmtime GitHub notifications bot (Jun 09 2025 at 17:35):

fitzgen created PR review comment:

Can you add this summary comment to the ISLE rule? Thanks!

Wasmtime GitHub notifications bot (Jun 09 2025 at 17:35):

fitzgen created PR review comment:

With this change, the rhs is slightly simpler and we don't need to introduce the new i64_not constructor

  (band ty x (iconst ty (imm64_masked ty (u64_not n)))))

Wasmtime GitHub notifications bot (Jun 09 2025 at 17:38):

fitzgen commented on PR #10979:

https://github.com/bytecodealliance/wasmtime/actions/runs/15516516108/job/43684140159?pr=10979#step:19:865

Looks like this optimization applied to one of our existing test cases in CI, changing its golden output.

You can update the output via

$ CRANELIFT_TEST_BLESS=1 cargo run -p cranelift-tools -- test filetests/filetests/isa/x64/stack_switch.clif

And then commit that test expectation update and include it in this PR.

Wasmtime GitHub notifications bot (Jun 09 2025 at 17:40):

fitzgen edited PR review comment.

Wasmtime GitHub notifications bot (Jun 10 2025 at 01:43):

bongjunj updated PR #10979.

Wasmtime GitHub notifications bot (Jun 10 2025 at 01:46):

bongjunj commented on PR #10979:

Hi, thanks for the comment.

1. I added the summary to the ISLE rule,
2. and updated the expected output as you mentioned.

Actually I'm collecting these code patterns from LLVM using some kind of synthesizer.

Wasmtime GitHub notifications bot (Jun 10 2025 at 17:33):

fitzgen submitted PR review:

Thanks!

Wasmtime GitHub notifications bot (Jun 10 2025 at 17:51):

fitzgen commented on PR #10979:

Actually I'm collecting these code patterns from LLVM using some kind of synthesizer.

Nice! I'd love to hear a little more about this. Are you harvesting LHSes via LLVM and then synthesizing RHSes directly for ISLE? Or synthesizing RHSes for LLVM and porting them to ISLE? Are you using Souper or a different synthesizer?

---

FWIW, we have some Souper-synthesized rules that we haven't completed landing (mostly because I don't have time) over in https://github.com/bytecodealliance/wasmtime/issues/5783

And we also have some infrastructure for harvesting Souper LHSes from CLIF input. The following command will harvest LHSes from the path/to/input.clif file and write each of them into the path/to/left-hand-sides directory:

$ cargo run -p cranelift-tools -- souper-harvest path/to/input.clif \
    -o path/to/left-hand-sides

And then we also have a helper script to run Souper. This will take those harvested LHSes from the previous step and run Souper on each of them. For each RHS that it finds, it will write a $LHS.result file next to the $LHS file:

$ ./cranelift/run-souper.sh path/to/souper-check path/to/left-hand-sides

As far as getting the initial CLIF input goes for the above commands, Wasmtime has a --emit-clif option you can use. The following will write a .clif file into path/to/output/dir for each function inside the Wasm module:

$ wasmtime compile path/to/module.wasm --emit-clif path/to/output/dir

Wasmtime GitHub notifications bot (Jun 10 2025 at 17:53):

fitzgen merged PR #10979.

Wasmtime GitHub notifications bot (Jun 13 2025 at 09:57):

bongjunj commented on PR #10979:

My synthesizer construct the LHS and RHS from the input and the output programs of LLVM optimizers. Most of the job is done by deterministic mapping from LLVM opcode to Cranelift ones. But the remaining part of synthesizing relationships among constants is the problem Im solving.

Thanks for the idea using souper. I will take a look into that.

Last updated: Dec 06 2025 at 06:05 UTC