[PATCH] D140087: [X86] Replace (31/63 -/^ X) with (NOT X) and ignore (32/64 ^ X) when computing shift count

[Roman Lebedev via Phabricator via llvm-commits]

lebedev.ri requested changes to this revision.
lebedev.ri added a comment.
This revision now requires changes to proceed.

Alive2 doesn't deal with assembly/dag, only ir.
I'm asking you to write the proofs for these changes via an IR tests,
explicitly modelling the implicit modulo of the shift amount, which isn't a thing in IR.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D140087/new/

https://reviews.llvm.org/D140087