Stream: git-wasmtime

Topic: wasmtime / PR #10850 Cranelift: ((x > 0) ? x : -x) => (ia...

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

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

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

bongjunj requested abrown for a review on PR #10850.

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

bongjunj opened PR #10850 from bongjunj:select-to-iabs 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

1. (x (>/>=) 0) ? x : -x ==> (iabs x)
2. (x (</<=) 0) ? -x : x ==> (iabs x)

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

(rule (simplify (select ty
              (icmp cty (IntCC.SignedGreaterThanOrEqual)
                x (iconst tty (u64_from_imm64 (u64_zero))))
              x
              (isub ty
                (iconst ty (u64_from_imm64 (u64_zero)))
              x)))
  (subsume (iabs ty x)))

(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 (isub ty x y)
    (provide (= result (bvsub x y)))
    (require
        (= (widthof x) (widthof y))))
(decl isub (Type Value Value) Value)
(extern extractor isub isub)
(extern constructor isub isub)


(spec (iabs ty x)
    (provide (= result
                (if (bvsge x (conv_to (widthof x) #x0000000000000000))
                    x
                    (bvneg x)))))
(decl iabs (Type Value) Value)
(extern extractor iabs iabs)
(extern constructor iabs iabs)

(spec (select ty c x y)
    (provide (= result (if (= c #x00) y x)))
    (require
        (= (widthof x) (widthof y))))
(decl select (Type Value Value Value) Value)
(extern extractor select select)
(extern constructor select select)

(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 (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 (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 64))  (ret (bv 64))  (canon (bv 64))))
(decl simplify (Value) Value)

</details>

Last updated: Dec 06 2025 at 06:05 UTC