Stream: git-wasmtime

Topic: wasmtime / PR #11359 [Cranelift] `(x + y) - (x | y) --> x...

Wasmtime GitHub notifications bot (Jul 31 2025 at 06:05):

bongjunj opened PR #11359 from bongjunj:main 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 adds a new optimization (x + y) - (x | y) --> x & y

<details>
<summary>proof</summary>

(rule (simplify (isub ty (iadd ty x y) (bor ty x y))) (band ty x y))

(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 Imm64 (type (bv 64)))

(model Type (type Int))
(model Value (type (bv)))

(model u8 (type (bv 8)))
(model u16 (type (bv 16)))
(model u32 (type (bv 32)))
(model u64 (type (bv 64)))
(model usize (type (bv)))

(model i8 (type (bv 8)))
(model i16 (type (bv 16)))
(model i32 (type (bv 32)))
(model i64 (type (bv 64)))
(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 (bnot ty x)
    (provide (= (bvnot x) result))
    (require
        (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))
        (= ty (widthof x))))
(decl bnot (Type Value) Value)
(extern extractor bnot bnot)
(extern constructor bnot bnot)
(instantiate bnot bv_ty_unary_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 eq (Type Value Value) Value)
(extern extractor eq eq)
(extern constructor eq eq)
(spec (eq ty x y)
    (provide (= result (if (= x y) #x01
[message truncated]

Wasmtime GitHub notifications bot (Jul 31 2025 at 06:05):

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

Wasmtime GitHub notifications bot (Jul 31 2025 at 06:05):

bongjunj requested cfallin for a review on PR #11359.

Wasmtime GitHub notifications bot (Jul 31 2025 at 08:50):

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

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 (Jul 31 2025 at 15:58):

fitzgen submitted PR review:

Awesome, thanks!

Wasmtime GitHub notifications bot (Jul 31 2025 at 16:22):

fitzgen merged PR #11359.

Last updated: Dec 06 2025 at 06:05 UTC