MAYCHANGE prediate doesn't discharge well when YMM registers are involved

[aqjune-aws]

This doesn't work:

g `MAYCHANGE [YMM1;YMM2] s0 s1 ==> MAYCHANGE [YMM2;YMM1] s0 s1`;;

e STRIP_TAC;;
e MONOTONE_MAYCHANGE_TAC;;

But this works:

g `MAYCHANGE [RAX;RBX] s0 s1 ==> MAYCHANGE [RBX;RAX] s0 s1`;;

e STRIP_TAC;;
e MONOTONE_MAYCHANGE_TAC;;

[aqjune-aws]

Pasting John's answer here:

I think the reason the machinery fails is that the YMM registers are defined as sub-parts of the ZMM registers such that assignments to the YMM registers zero the top halves on write as per usual VEX-encoded behaviour. The MAYCHANGE concept is defined in terms like "the change from the initial to final state can be expressed as a sequence of assignments to these states", so it's affected by the write behavior specifically. It might be simplest for now just to use ZMM registers throughout in the MAYCHANGE list; this will fit the way MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI is defined for the final statement, though needless to say the Windows version is more complicated.

[jakemas]

+1 Also hitting this!