[acl2/acl2] 5af9bb: Extend other ADD/ADC/etc. variants to 32-bit mode.

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: 5af9bb2e432919ebf1fccf142f8ba5fd7b6be1f2
https://github.com/acl2/acl2/commit/5af9bb2e432919ebf1fccf142f8ba5fd7b6be1f2
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2018-04-17 (Tue, 17 Apr 2018)

Changed paths:
M books/projects/x86isa/machine/decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/wordCount/wc.lisp

Log Message:
-----------
Extend other ADD/ADC/etc. variants to 32-bit mode.

These are the (Eb Ib), (Ev Iv), and (Ev Ib) variants of the instructions ADD,
ADC, SUB, SBB, OR, AND, XOR, and CMP.

The same semantic function that has just been extended also implements the Eb
and Ev variants of the TEST instruction, which will be enabled at the top level
soon.

Prior to these extensions, the semantic function was generating #UD when the
LOCK prefix is used and the instruction is CMP. I relaxed the test for the CMP
instruction to include the TEST instruction as well, because that one also
generates #UD with the LOCK prefix. The new function also generates #UD when the
LOCK prefix is used but the destination operand is a register and not memory.

[GitHub]

Branch: refs/heads/master