summaryrefslogtreecommitdiff
path: root/ia32
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-09-10 11:26:03 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-09-10 11:26:03 +0000
commitf7cc6f0b16f475480ddafe1fb1690c509e545de0 (patch)
tree9d33de92f340fd2aecdafb817a242133b5ed1c9f /ia32
parent637334181f54154f6c5598073c60f3f2c3ab5e87 (diff)
Comments
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1508 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32')
-rw-r--r--ia32/Asm.v18
1 files changed, 10 insertions, 8 deletions
diff --git a/ia32/Asm.v b/ia32/Asm.v
index 9c23d9d..0f70912 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -48,7 +48,8 @@ Proof. decide equality. Defined.
Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}.
Proof. decide equality. Defined.
-(** Condition bits *)
+(** Bits of the flags register. [SOF] is a pseudo-bit representing
+ the "xor" of the [OF] and [SF] bits. *)
Inductive crbit: Type :=
| ZF | CF | PF | SOF.
@@ -60,7 +61,7 @@ Inductive preg: Type :=
| IR: ireg -> preg (**r integer register *)
| FR: freg -> preg (**r XMM register *)
| ST0: preg (**r top of FP stack *)
- | CR: crbit -> preg (**r bit of the condition register *)
+ | CR: crbit -> preg (**r bit of the flags register *)
| RA: preg. (**r pseudo-reg representing return address *)
Coercion IR: ireg >-> preg.
@@ -90,7 +91,8 @@ Inductive testcond: Type :=
(** Instructions. IA32 instructions accept many combinations of
registers, memory references and immediate constants as arguments.
- Here, we list the combinations that we actually use.
+ Here, we list only the combinations that we actually use.
+
Naming conventions:
- [r]: integer register operand
- [f]: XMM register operand
@@ -98,9 +100,9 @@ Inductive testcond: Type :=
- [i]: immediate integer operand
- [s]: immediate symbol operand
- [l]: immediate label operand
-- [st0]: top of floating-point stack
- [cl]: the [CL] register
-- For two-operand instructions, the first suffix describes the result
+
+ For two-operand instructions, the first suffix describes the result
(and first argument), the second suffix describes the second argument.
*)
@@ -433,12 +435,12 @@ Definition exec_store (chunk: memory_chunk) (m: mem)
(** Execution of a single instruction [i] in initial state
[rs] and [m]. Return updated state. For instructions
- that correspond to actual PowerPC instructions, the cases are
+ that correspond to actual IA32 instructions, the cases are
straightforward transliterations of the informal descriptions
- given in the PowerPC reference manuals. For pseudo-instructions,
+ given in the IA32 reference manuals. For pseudo-instructions,
refer to the informal descriptions given above. Note that
we set to [Vundef] the registers used as temporaries by the
- expansions of the pseudo-instructions, so that the PPC code
+ expansions of the pseudo-instructions, so that the IA32 code
we generate cannot use those registers to hold values that
must survive the execution of the pseudo-instruction.
*)