From 9174523f4791e2263f13866b1df1f5adc0cc3ec4 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 21 Aug 2015 10:51:08 +0200
Subject: Consistent naming of "P" instructions and consistent ordering of
 arguments according to Intel convention (instr destination, argument).

---
 ia32/Asm.v | 85 +++++++++++++++++++++++++++++++-------------------------------
 1 file changed, 42 insertions(+), 43 deletions(-)

(limited to 'ia32/Asm.v')

diff --git a/ia32/Asm.v b/ia32/Asm.v
index b423b4fc..9e763f60 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -213,41 +213,41 @@ Inductive instruction: Type :=
   | Pfreeframe(sz: Z)(ofs_ra ofs_link: int)
   | Pbuiltin(ef: external_function)(args: list preg)(res: list preg)
   | Pannot(ef: external_function)(args: list (annot_arg preg))
-  | Padcl_ir (n: int) (r: ireg)
-  | Padcl_rr (r1: ireg) (r2: ireg)
-  | Paddl (r1: ireg) (r2: ireg)
-  | Paddl_mi (a: addrmode) (n: int)
-  | Paddl_ri (r1: ireg) (n: int)
-  | Pbsfl (r1: ireg) (r2: ireg)
-  | Pbslr (r1: ireg) (r2: ireg)
-  | Pbswap (r: ireg)
+  (** Instructions not generated by [Asmgen] *)
+  | Padc_ri (rd: ireg) (n: int)
+  | Padc_rr (rd: ireg) (r2: ireg)
+  | Padd_mi (a: addrmode) (n: int)
+  | Padd_ri (rd: ireg) (n: int)
+  | Padd_rr (rd: ireg) (r2: ireg)
+  | Pbsf (rd: ireg) (r1: ireg)
+  | Pbsr (rd: ireg) (r1: ireg)
+  | Pbswap (rd: ireg)
+  | Pbswap16 (rd: ireg)
   | Pcfi_adjust (n: int)
-  | Pfmadd132 (r1: freg) (r2: freg) (r3: freg)
-  | Pfmadd213 (r1: freg) (r2: freg) (r3: freg)
-  | Pfmadd231 (r1: freg) (r2: freg) (r3: freg)
-  | Pfmsub132 (r1: freg) (r2: freg) (r3: freg)
-  | Pfmsub213 (r1: freg) (r2: freg) (r3: freg)
-  | Pfmsub231 (r1: freg) (r2: freg) (r3: freg)
-  | Pfnmadd132 (r1: freg) (r2: freg) (r3: freg)
-  | Pfnmadd213 (r1: freg) (r2: freg) (r3: freg)
-  | Pfnmadd231 (r1: freg) (r2: freg) (r3: freg)
-  | Pfnmsub132 (r1: freg) (r2: freg) (r3: freg)
-  | Pfnmsub213 (r1: freg) (r2: freg) (r3: freg)
-  | Pfnmsub231 (r1: freg) (r2: freg) (r3: freg)
-  | Pmaxsd (r1: freg) (r2: freg)
-  | Pminsd (r1: freg) (r2: freg)
-  | Pmovb_rm (rs: ireg) (a: addrmode)
-  | Pmovq_rm (rs: freg) (a: addrmode)
+  | Pfmadd132 (rd: freg) (r2: freg) (r3: freg)
+  | Pfmadd213 (rd: freg) (r2: freg) (r3: freg)
+  | Pfmadd231 (rd: freg) (r2: freg) (r3: freg)
+  | Pfmsub132 (rd: freg) (r2: freg) (r3: freg)
+  | Pfmsub213 (rd: freg) (r2: freg) (r3: freg)
+  | Pfmsub231 (rd: freg) (r2: freg) (r3: freg)
+  | Pfnmadd132 (rd: freg) (r2: freg) (r3: freg)
+  | Pfnmadd213 (rd: freg) (r2: freg) (r3: freg)
+  | Pfnmadd231 (rd: freg) (r2: freg) (r3: freg)
+  | Pfnmsub132 (rd: freg) (r2: freg) (r3: freg)
+  | Pfnmsub213 (rd: freg) (r2: freg) (r3: freg)
+  | Pfnmsub231 (rd: freg) (r2: freg) (r3: freg)
+  | Pmaxsd (rd: freg) (r2: freg)
+  | Pminsd (rd: freg) (r2: freg)
+  | Pmovb_rm (rd: ireg) (a: addrmode)
   | Pmovq_mr  (a: addrmode) (rs: freg)
+  | Pmovq_rm (rd: freg) (a: addrmode)
   | Pmovsb
   | Pmovsw
-  | Pmovw_rm (rs: ireg) (ad: addrmode)
+  | Pmovw_rm (rd: ireg) (ad: addrmode)
   | Prep_movsl
-  | Prolw_8 (r: ireg)
-  | Psbbl (r1: ireg) (r2: ireg)
-  | Psqrtsd (r1: freg) (r2: freg)
-  | Psubl_ri (r1: ireg) (n: int)
-  | Pxchg (r1: ireg) (r2: ireg).
+  | Psbb_rr (rd: ireg) (r2: ireg)
+  | Psqrtsd (rd: freg) (r1: freg)
+  | Psub_ri (rd: ireg) (n: int).
 
 Definition code := list instruction.
 Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
@@ -784,16 +784,17 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Stuck                             (**r treated specially below *)
   | Pannot ef args =>
     Stuck                             (**r treated specially below *)
-  (** The following instructions and directives are not generated directly by Asmgen,
-      so we do not model them. *)
-  | Padcl_ir _ _
-  | Padcl_rr _ _
-  | Paddl _ _
-  | Paddl_mi _ _
-  | Paddl_ri _ _
+  (** The following instructions and directives are not generated
+      directly by [Asmgen], so we do not model them. *)
+  | Padc_ri _ _
+  | Padc_rr _ _
+  | Padd_mi _ _
+  | Padd_ri _ _
+  | Padd_rr _ _
+  | Pbsf _ _
+  | Pbsr _ _
   | Pbswap _
-  | Pbsfl _ _
-  | Pbslr _ _
+  | Pbswap16 _
   | Pcfi_adjust _
   | Pfmadd132 _ _ _
   | Pfmadd213 _ _ _
@@ -816,11 +817,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pmovsw
   | Pmovw_rm _ _ 
   | Prep_movsl
-  | Prolw_8 _
-  | Psbbl _ _
+  | Psbb_rr _ _
   | Psqrtsd _ _
-  | Psubl_ri _ _
-  | Pxchg _ _ => Stuck 
+  | Psub_ri _ _ => Stuck 
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
-- 
cgit