Cranelift: `or(x, C) + (-C) --> and(x, ~C)` #10979

bongjunj · 2025-06-08T08:17:27Z

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

proof.isle

(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 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 (i64_as_u64 arg) (provide (= arg result)))
(decl pure i64_as_u64 (i64) u64)
(extern constructor i64_as_u64 i64_as_u64)

(spec (i64_neg x) (provide (= result (bvneg x))))
(decl pure i64_neg (i64) i64)
(extern constructor i64_neg i64_neg)

(spec (i64_not arg) (provide (= (bvnot arg) result)))
(decl pure i64_not (i64) i64)
(extern constructor i64_not i64_not)

(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 i64) 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))))(decl simplify (Value) Value)
(spec (simplify x) (provide (= x result)))
(instantiate simplify
    ((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))))

github-actions · 2025-06-08T09:45:37Z

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.

fitzgen

Thanks! Just a couple minor nitpicks below.

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

cranelift/codegen/src/opts/arithmetic.isle

fitzgen · 2025-06-09T17:34:50Z

cranelift/filetests/filetests/egraph/arithmetic.clif

@@ -366,3 +366,17 @@ block0(v0: i16, v1: i16, v2: i16):
 ; check: v12 = iadd v0, v1
 ; check: v15 = iadd v12, v2
 ; check: return v15
+
+;; or(x, C) + (-C)  -->  and(x, ~C)


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

fitzgen · 2025-06-09T17:38:02Z

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.

bongjunj · 2025-06-10T01:46:53Z

Hi, thanks for the comment.

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

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

fitzgen

Thanks!

fitzgen · 2025-06-10T17:51:11Z

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 #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

bongjunj · 2025-06-13T09:57:19Z

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.

bongjunj added 3 commits June 8, 2025 08:08

add helper

1a7d9dd

add rule and test

d5bab31

update rule

4c0e7ad

bongjunj requested a review from a team as a code owner June 8, 2025 08:17

bongjunj requested review from fitzgen and removed request for a team June 8, 2025 08:17

github-actions bot added cranelift Issues related to the Cranelift code generator isle Related to the ISLE domain-specific language labels Jun 8, 2025

fitzgen reviewed Jun 9, 2025

View reviewed changes

bongjunj added 2 commits June 10, 2025 01:42

add rule summary

27c5c4e

update expectation test

3ee5f1b

fitzgen approved these changes Jun 10, 2025

View reviewed changes

fitzgen added this pull request to the merge queue Jun 10, 2025

Merged via the queue into bytecodealliance:main with commit 9447700 Jun 10, 2025
41 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Cranelift: `or(x, C) + (-C) --> and(x, ~C)` #10979

Cranelift: `or(x, C) + (-C) --> and(x, ~C)` #10979

Uh oh!

bongjunj commented Jun 8, 2025

Uh oh!

github-actions bot commented Jun 8, 2025

Uh oh!

fitzgen left a comment

Uh oh!

Uh oh!

fitzgen Jun 9, 2025

Uh oh!

fitzgen commented Jun 9, 2025

Uh oh!

bongjunj commented Jun 10, 2025

Uh oh!

fitzgen left a comment

Uh oh!

fitzgen commented Jun 10, 2025

Uh oh!

Uh oh!

bongjunj commented Jun 13, 2025

Uh oh!

Uh oh!

Cranelift: or(x, C) + (-C) --> and(x, ~C) #10979

Cranelift: or(x, C) + (-C) --> and(x, ~C) #10979

Uh oh!

Conversation

bongjunj commented Jun 8, 2025

Uh oh!

github-actions bot commented Jun 8, 2025

Subscribe to Label Action

Uh oh!

fitzgen left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

fitzgen Jun 9, 2025

Choose a reason for hiding this comment

Uh oh!

fitzgen commented Jun 9, 2025

Uh oh!

bongjunj commented Jun 10, 2025

Uh oh!

fitzgen left a comment

Choose a reason for hiding this comment

Uh oh!

fitzgen commented Jun 10, 2025

Uh oh!

Uh oh!

bongjunj commented Jun 13, 2025

Uh oh!

Uh oh!

Cranelift: `or(x, C) + (-C) --> and(x, ~C)` #10979

Cranelift: `or(x, C) + (-C) --> and(x, ~C)` #10979