[acl2/acl2] 87fc2f: Extend 'PUSH register' instruction to 32-bit mode.

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: 87fc2fe8b37b91ed760faf7fe8aed44411be62ca
https://github.com/acl2/acl2/commit/87fc2fe8b37b91ed760faf7fe8aed44411be62ca
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2018-01-04 (Thu, 04 Jan 2018)

Changed paths:
M books/projects/x86isa/machine/decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/x86.lisp

Log Message:
-----------
Extend 'PUSH register' instruction to 32-bit mode.

This is the instruction to push GPRs (general-purpose registers) onto the stack.

This commit completes the extension of this instruction to 64-bit mode,
initiated by some previous commits. We use the newly introduced functions
READ-*SP, ADD-TO-*SP, and WRITE-*SP to manipulate the stack pointer, and the
newly introduced function WRITE-*IP to save the final instruction pointer. We
also extend the determination of the operand size to take CS.D into account in
32-bit mode, as well as the override prefix. The resuling semantic function
should be an accurate formalization of the instruction in both 64-bit and 32-bit
mode. The top-level dispatch function has been changed to always call this
semantic function, not just in 64-bit mode; that is, this instruction is no
longer "unimplemented" in 32-bit mode.

Also added theorems saying that READ-*SP and the other functions mentioned above
reduce to the previous "direct" manipulations in 64-bit mode. These theorems
keep all the proofs working, which are currently for 64-bit mode.

Also updated slightly the documentation, and added a comment about not capturing
the 8086 behavior of PUSH SP.

[GitHub]

Branch: refs/heads/master