Stream: git-wasmtime

Topic: wasmtime / PR #7450 Cranelift: Reassociate constants out ...

Wasmtime GitHub notifications bot (Nov 01 2023 at 21:52):

fitzgen opened PR #7450 from fitzgen:reassociate-constants-in-nested-shifts to bytecodealliance:main:

This allows for more constant propagation.

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

Wasmtime GitHub notifications bot (Nov 01 2023 at 21:52):

fitzgen requested elliottt for a review on PR #7450.

Wasmtime GitHub notifications bot (Nov 01 2023 at 21:52):

fitzgen requested wasmtime-compiler-reviewers for a review on PR #7450.

Wasmtime GitHub notifications bot (Nov 01 2023 at 22:03):

afonso360 submitted PR review.

Wasmtime GitHub notifications bot (Nov 01 2023 at 22:03):

afonso360 created PR review comment:

I think this doesn't hold if (c + b) >= ty_bits right? Either way I'm going to run fuzzgen on this for a while to doublecheck.

Wasmtime GitHub notifications bot (Nov 01 2023 at 22:31):

fitzgen submitted PR review.

Wasmtime GitHub notifications bot (Nov 01 2023 at 22:31):

fitzgen created PR review comment:

Ah yeah unfortunately I think you are right:

(declare-const a (_ BitVec 32))
(declare-const b (_ BitVec 32))
(declare-const c (_ BitVec 32))

(define-fun shl ((x (_ BitVec 32)) (y (_ BitVec 32))) (_ BitVec 32)
  (let ((z (bvurem y #x00000020)))
    (bvshl x z)))


(assert (not (= (shl (shl a b) c)
                (shl a (bvadd b c)))))

(check-sat)
(get-model)

Produces

sat
(
  (define-fun b () (_ BitVec 32)
    #x00000010)
  (define-fun a () (_ BitVec 32)
    #xf879c486)
  (define-fun c () (_ BitVec 32)
    #x00000010)
)

and then

fn shl(a: u32, b: u32) -> u32 {
    a << (b % 32)
}

fn foo(a: u32, b: u32, c: u32) -> u32 {
    shl(shl(a, b), c)
}

fn bar(a: u32, b: u32, c: u32) -> u32 {
    shl(a, b.wrapping_add(c))
}

fn main() {
    let a = 0xf879c486;
    dbg!(a);

    let b = 0x00000010;
    dbg!(b);

    let c = 0x00000010;
    dbg!(c);

    dbg!(foo(a, b, c));
    dbg!(bar(a, b, c));
}

produces

[src/main.rs:15] a = 4168729734
[src/main.rs:18] b = 16
[src/main.rs:21] c = 16
[src/main.rs:23] foo(a, b, c) = 0
[src/main.rs:24] bar(a, b, c) = 4168729734

Wasmtime GitHub notifications bot (Nov 01 2023 at 22:40):

fitzgen updated PR #7450.

Wasmtime GitHub notifications bot (Nov 01 2023 at 22:40):

fitzgen submitted PR review.

Wasmtime GitHub notifications bot (Nov 01 2023 at 22:40):

fitzgen created PR review comment:

Removed the rules that depended on this buggy identity.

Wasmtime GitHub notifications bot (Nov 01 2023 at 23:00):

afonso360 submitted PR review:

:+1: LGTM!

Coincidentally I've been working on a similar set of rules at egraphs-shifts-2. I'll submit those as a PR tomorrow!

Wasmtime GitHub notifications bot (Nov 01 2023 at 23:01):

afonso360 submitted PR review:

:+1: LGTM!

Coincidentally I've been working on a similar set of rules. I'll submit those as a PR tomorrow!

Wasmtime GitHub notifications bot (Nov 01 2023 at 23:49):

fitzgen merged PR #7450.

Last updated: Nov 22 2024 at 17:03 UTC