Stream: git-wasmtime

Topic: wasmtime / issue #7450 Cranelift: Reassociate constants o...

view this post on Zulip Wasmtime GitHub notifications bot (Nov 01 2023 at 22:42):

fitzgen commented on issue #7450:

The remaining rule is correct according to Z3:

(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 (shl a c) b))))

(check-sat)
(get-model)

produces unsat, meaning there is no counterexample.

view this post on Zulip Wasmtime GitHub notifications bot (Nov 01 2023 at 22:44):

github-actions[bot] commented on issue #7450:

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:

To subscribe or unsubscribe from this label, edit the <code>.github/subscribe-to-label.json</code> configuration file.

Learn more.
</details>

Last updated: Nov 22 2024 at 17:03 UTC