Stream: git-wasmtime

Topic: wasmtime / PR #10849 Cranelift: `(eq/ne (xor x y) y)` => ...

Wasmtime GitHub notifications bot (May 28 2025 at 07:26):

bongjunj opened PR #10849 from bongjunj:icmp-xor 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 new rules to the mid-end optimizer.
Rules are verified with crocus.

crocus -i proof.isle -t simplify --noprelude --codegen <codegen-dir>

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

(rule (simplify (icmp cty (IntCC.NotEqual) x (bxor bty x y))) (subsume (icmp cty (IntCC.NotEqual) y (iconst_u bty 0))))
; (rule (simplify (icmp cty (IntCC.NotEqual) x (bxor bty x y))) (subsume (icmp cty (IntCC.NotEqual) y (iconst_u bty 0))))
(type Type (primitive Type))
(type Value (primitive Value))
(type Imm64 (primitive Imm64))
(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 (bxor ty x y)
    (provide (= (bvxor x y) result))
    (require
        (= ty (widthof x))
        (= (widthof x) (widthof y))))
(decl bxor (Type Value Value) Value)
(extern extractor bxor bxor)
(extern constructor bxor bxor)

(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)
        (= (widthof x) (widthof y))
        (= (widthof x) 64)
        (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)

(spec (iconst ty arg)
    (provide (= arg (zero_ext 64 result)))
    (require (= ty (widthof arg))))
(decl iconst (Type Imm64) Value)
(extern constructor iconst iconst)
(extern extractor iconst iconst)

(spec (imm64 x) (provide (= x result)))
(decl imm64 (u64) Imm64)
(extern constructor imm64 imm64)

(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 constructor iconst_u iconst_u)

(spec (simplify x) (provide (= x result)))
(instantiate simplify
    ((args (bv 8))  (ret (bv 8))  (canon (bv 8))))
(decl simplify (Value) Value)

</details>

Wasmtime GitHub notifications bot (May 28 2025 at 07:26):

bongjunj requested cfallin for a review on PR #10849.

Wasmtime GitHub notifications bot (May 28 2025 at 07:26):

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

Wasmtime GitHub notifications bot (May 28 2025 at 09:46):

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

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 (May 28 2025 at 17:32):

cfallin submitted PR review:

LGTM, and thanks for the formal verification as well!

Wasmtime GitHub notifications bot (May 28 2025 at 17:52):

cfallin merged PR #10849.

Last updated: Dec 06 2025 at 06:05 UTC