Merge branch 'master' into 'new-builtins'

1 files changed, 42 insertions, 43 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 6e21ec63..96a49005 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -212,41 +212,41 @@ Inductive instruction: Type :=
   | Pallocframe(sz: Z)(ofs_ra ofs_link: int)
   | Pfreeframe(sz: Z)(ofs_ra ofs_link: int)
   | Pbuiltin(ef: external_function)(args: list (builtin_arg preg))(res: builtin_res 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 }.
@@ -790,16 +790,17 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       end
   | Pbuiltin ef args res =>
       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 _ _ _
@@ -822,11 +823,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