Stream: git-wasmtime

Topic: wasmtime / PR #10978 Cranelift: `(udiv (select c A B)) =>...


view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2025 at 06:03):

bongjunj opened PR #10978 from bongjunj:udiv-select to bytecodealliance:main:

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

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 the following optimization:

(udiv (select c A B)) => (ushr (select c log2(A) log2(B))

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

(rule
  (simplify_skeleton (udiv y
                       (select ty
                         x
                         (iconst ty (imm64_power_of_two n))
                         (iconst ty (imm64_power_of_two m)))))
  (ushr ty y (select ty x (iconst ty (imm64 n)) (iconst ty (imm64 m)))))

(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)))
    (
[message truncated]

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2025 at 06:03):

bongjunj requested alexcrichton for a review on PR #10978.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2025 at 06:03):

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

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2025 at 07:44):

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

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:

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

Learn more.
</details>

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2025 at 08:17):

bongjunj edited PR #10978:

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

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 the following optimization:

(udiv (select c A B)) => (ushr (select c log2(A) log2(B))

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

(rule
  (simplify_skeleton (udiv y
                       (select ty
                         x
                         (iconst ty (imm64_power_of_two n))
                         (iconst ty (imm64_power_of_two m)))))
  (ushr ty y (select ty x (iconst ty (imm64 n)) (iconst ty (imm64 m)))))

(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))
[message truncated]

view this post on Zulip Wasmtime GitHub notifications bot (Jun 09 2025 at 14:39):

alexcrichton submitted PR review:

Thanks! It looks like we don't currently have rules for divide-by-power-of-two-constant which, if you're interested, might be a good rule to add as well as a follow-up.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 09 2025 at 15:01):

alexcrichton merged PR #10978.


Last updated: Dec 06 2025 at 06:05 UTC