Skip to content

Cranelift: (udiv (select c A B)) => (ushr (select c log2(A) log2(B)) #10978

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Jun 9, 2025
Merged

Cranelift: (udiv (select c A B)) => (ushr (select c log2(A) log2(B)) #10978

merged 1 commit into from
Jun 9, 2025

Conversation

bongjunj
Copy link
Contributor

@bongjunj bongjunj commented Jun 8, 2025 •
edited
Loading

This adds the following optimization:

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

proof.isle 
(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))))
(decl iconst (Type Imm64) Value)
(extern constructor iconst iconst)
(extern extractor iconst iconst)
(instantiate iconst bv_ty_unary_8_to_64)

(spec (u64_zero) (provide (= #x0000000000000000 result)))
(decl u64_zero () u64)
(extern extractor u64_zero u64_zero)

(spec (u64_nonzero arg) (provide (= result arg)) (require (bvsgt arg #x0000000000000000)))
(decl u64_nonzero (u64) u64)
(extern extractor u64_nonzero u64_nonzero)

(spec (u64_from_imm64 arg) (provide (= arg result)))
(decl u64_from_imm64 (u64) Imm64)
(extern extractor u64_from_imm64 u64_from_imm64)

(spec (nonzero_u64_from_imm64 arg) (provide (= arg result)) (require (bvsgt arg #x0000000000000000)))
(decl nonzero_u64_from_imm64 (u64) Imm64)
(extern extractor nonzero_u64_from_imm64 nonzero_u64_from_imm64)
                    
(spec (u64_not arg) (provide (= (bvnot arg) result)))
(decl pure u64_not (u64) u64)
(extern constructor u64_not u64_not)

(spec (u64_add x y) (provide (= (bvadd x y) result)))
(decl pure u64_add (u64 u64) u64)
(extern constructor u64_add u64_add)

(spec (u64_and x y) (provide (= (bvand x y) result)))
(decl pure u64_and (u64 u64) u64)
(extern constructor u64_and u64_and)

(spec (u64_or x y) (provide (= (bvor x y) result)))
(decl pure u64_or (u64 u64) u64)
(extern constructor u64_or u64_or)
                    
(spec (u64_sub x y) (provide (= (bvsub x y) result)))
(decl pure u64_sub (u64 u64) u64)
(extern constructor u64_sub u64_sub)

(spec (u64_xor x y) (provide (= (bvxor x y) result)))
(decl pure u64_xor (u64 u64) u64)
(extern constructor u64_xor u64_xor)

(spec (u64_udiv x y)
    (provide (= result (bvudiv x y))))
(decl pure partial u64_udiv (u64 u64) u64)
(extern constructor u64_udiv u64_udiv)

(spec (u64_eq x y)
      (provide (= result (if (= x y) true false))))
(decl pure u64_eq (u64 u64) bool)
(extern constructor u64_eq u64_eq)

(spec (u64_le x y)
      (provide (= result (if (bvule x y) true false))))
(decl pure u64_le (u64 u64) bool)
(extern constructor u64_le u64_le)

(spec (u64_lt x y)
      (provide (= result (if (bvult x y) true false))))
(decl pure u64_lt (u64 u64) bool)
(extern constructor u64_lt u64_lt)

(spec (u64_shl x y)
      (provide (= result (bvshl x y))))
(decl pure u64_shl (u64 u64) u64)
(extern constructor u64_shl u64_shl)

(spec (u64_rem x y)
      (provide (= result (bvurem x y)))
      (require
        (not (= y (zero_ext (widthof y) #b0)))))
(decl pure partial u64_rem (u64 u64) u64)
(extern constructor u64_rem u64_rem)

(spec (u64_is_odd x)
      (provide (= result (if (= (bvand x #x0000000000000001) #x0000000000000001) true false))))
(decl pure u64_is_odd (u64) bool)
(extern constructor u64_is_odd u64_is_odd)

(spec (imm64 x) (provide (= x result)))
(decl imm64 (u64) Imm64)
(extern constructor imm64 imm64)
                    
(spec (imm64_masked ty x) (provide (= (conv_to ty x) result)))
(decl imm64_masked (Type u64) Imm64)
(extern constructor imm64_masked imm64_masked)

(spec (imm64_power_of_two x)
  (provide (= result (bvshl #x0000000000000001 x)))
  (require
    (bvsgt x #x0000000000000000)
    (bvule x #x000000000000003e)
    (= (bvand x (bvsub x #x0000000000000001)) #x0000000000000000)))
(decl imm64_power_of_two (u64) Imm64)
(extern extractor imm64_power_of_two imm64_power_of_two)

(spec (fits_in_64 ty)
    (provide (= result ty))
    (require (<= ty 64)))
(decl fits_in_64 (Type) Type)
(extern extractor fits_in_64 fits_in_64)

(spec (ty_bits_u64 ty)
    (provide (= result (int2bv 64 ty))))
(decl pure ty_bits_u64 (Type) u64)
(extern constructor ty_bits_u64 ty_bits_u64)


(spec (udiv x y)
    (provide (= result (bvudiv x y)))
    (require (not (= y (zero_ext (widthof y) #b0)))))
(decl udiv (Value Value) Inst)
(extern extractor udiv udiv)
(instantiate udiv bv_binary_8_to_64)

(spec (sdiv x y)
    (provide (= result (bvsdiv x y)))
    (require (not (= y (zero_ext (widthof y) #b0)))))
(decl sdiv (Value Value) Inst)
(extern extractor sdiv sdiv)
(extern constructor sdiv sdiv)
(instantiate sdiv bv_binary_8_to_64)

(spec (urem x y)
    (provide (= result (bvurem x y)))
    (require (not (= y (zero_ext (widthof y) #b0)))))
(decl urem (Value Value) Inst)
(extern extractor urem urem)
(extern constructor urem urem)
(instantiate urem bv_binary_8_to_64)

(spec (srem x y)
    (provide (= result (bvsrem x y)))
    (require (not (= y (zero_ext (widthof y) #b0)))))
(decl srem (Value Value) Inst)
(extern extractor srem srem)
(extern constructor srem srem)
(instantiate srem bv_binary_8_to_64)

(spec (subsume x) (provide (= result x)))
(decl subsume (Value) Value)
(extern constructor subsume subsume)


(spec (iconst_u ty arg)
    (provide (= arg (zero_ext 64 result))))
(decl iconst_u (Type u64) Value)
(extern extractor iconst_u iconst_u)
(instantiate iconst_u
    ((args (bv 64)) (ret (bv 8)) (canon (bv 8)))
    ((args (bv 64)) (ret (bv 16)) (canon (bv 16)))
    ((args (bv 64)) (ret (bv 32)) (canon (bv 32)))
    ((args (bv 64)) (ret (bv 64)) (canon (bv 64))))

(spec (iconst_s ty arg)
    (provide (= arg (sign_ext 64 result))))
(decl iconst_s (Type u64) Value)
(extern extractor iconst_s iconst_s)
(instantiate iconst_s
    ((args (bv 64)) (ret (bv 8)) (canon (bv 8)))
    ((args (bv 64)) (ret (bv 16)) (canon (bv 16)))
    ((args (bv 64)) (ret (bv 32)) (canon (bv 32)))
    ((args (bv 64)) (ret (bv 64)) (canon (bv 64))))(spec (simplify_skeleton x) (provide (= x result)))
(instantiate simplify_skeleton
    ((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)))
)
(decl simplify_skeleton (Inst) Value)

@bongjunj bongjunj requested a review from a team as a code owner June 8, 2025 06:03
@bongjunj bongjunj requested review from alexcrichton and removed request for a team June 8, 2025 06:03
@github-actions github-actions bot added cranelift Issues related to the Cranelift code generator isle Related to the ISLE domain-specific language labels Jun 8, 2025
@github-actions GitHub Actions
Copy link

github-actions bot commented Jun 8, 2025

Subscribe to Label Action

cc @cfallin, @fitzgen

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 .github/subscribe-to-label.json configuration file.

Learn more.

alexcrichton
alexcrichton approved these changes Jun 9, 2025
View reviewed changes
Copy link
Member

@alexcrichton alexcrichton left a comment

Choose a reason for hiding this comment

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

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.

@alexcrichton alexcrichton added this pull request to the merge queue Jun 9, 2025
Merged via the queue into bytecodealliance:main with commit 0e7fc1c Jun 9, 2025
41 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alexcrichton alexcrichton alexcrichton approved these changes

Assignees
No one assigned
Labels
cranelift Issues related to the Cranelift code generator isle Related to the ISLE domain-specific language
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@bongjunj @alexcrichton