8 karma · joined October 25, 2024
There is even an instruction where AMD got this wrong! VPERMQ requires VEX.W=1, but some AMD CPUs also happily execute it when VEX.W=0 even though that is supposed to raise an exception.
The CPU also doesn't care if you use prefixes that aren't valid for a specific instruction, for example a REP on a non-repeatable instruction. The LOCK prefix is the only prefix that makes the sane choice to reject invalid combinations, rather than silently accept them.
Also, the (E)VEX prefix doesn't behave like the other prefixes: it must be placed last, and can therefore only appear once. All other prefixes can be repeated.
Fun (but useless) fact: This being x86, of course there are at least three different ways [1] to encode this instruction: the way it was shown, with an address size override prefix (giving `lea eax, [edi+esi]`), or with both a REX prefix and an address size override prefix (giving `lea rax, [edi+esi]`).
And if you have a segment with base=0 around you can also add in a segment for fun: `lea rax, cs:[edi+esi]`
[1]: not counting redundant prefixes and different ModRMs
From Table 7 you can get an idea of how many instruction variants we cover (~1500 covered, ~700 enumerated but not synthesized, 744 out of enumeration scope). Instruction variants correspond much more closely with the mnemonics listed in the reference manuals, and this is typically the number reported by related work.
Documentation is definitely not one of x86's strengths. Other architectures do much better. For example, ARM provides formal models of their CPUs, and RISC-V is so simple you could implement all its semantics in a few thousand lines of code.
There are quite a few instructions with undefined behavior, but it is not that much of an issue if you can choose to avoid it -- for example in a compiler. Almost all UB is found in flags or when using invalid instruction prefixes. And although there is some unexpected UB, like `imul`'s zero flag being UB instead of being set according to the result of the multiplication [1], reading the manual and sticking to the parts that are clearly not UB gets you most of the way.
However, it becomes an issue if you need to analyze a binary that uses UB. Then you can't choose which instructions to use, so you need to have a complete model of all UB. That's much more difficult, and for example most decompilers currently fail at this. We have an example of this in Figure 1 of our paper.
I'm happy to answer questions if there are any.