Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"

This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing
changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.

1 files changed, 2 insertions, 74 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index b423b4fc..b67c3cc5 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -212,42 +212,7 @@ 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 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)
-  | 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)
-  | Pmovq_mr  (a: addrmode) (rs: freg)
-  | Pmovsb
-  | Pmovsw
-  | Pmovw_rm (rs: 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).
+  | Pannot(ef: external_function)(args: list (annot_arg preg)).
 
 Definition code := list instruction.
 Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
@@ -783,44 +748,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pbuiltin ef args res =>
       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 _ _
-  | Pbswap _
-  | Pbsfl _ _
-  | Pbslr _ _
-  | Pcfi_adjust _
-  | Pfmadd132 _ _ _
-  | Pfmadd213 _ _ _
-  | Pfmadd231 _ _ _
-  | Pfmsub132 _ _ _
-  | Pfmsub213 _ _ _
-  | Pfmsub231 _ _ _
-  | Pfnmadd132 _ _ _
-  | Pfnmadd213 _ _ _
-  | Pfnmadd231 _ _ _
-  | Pfnmsub132 _ _ _
-  | Pfnmsub213 _ _ _
-  | Pfnmsub231 _ _ _
-  | Pmaxsd _ _
-  | Pminsd _ _
-  | Pmovb_rm _ _
-  | Pmovq_rm _ _
-  | Pmovq_mr _ _   
-  | Pmovsb
-  | Pmovsw
-  | Pmovw_rm _ _ 
-  | Prep_movsl
-  | Prolw_8 _
-  | Psbbl _ _
-  | Psqrtsd _ _
-  | Psubl_ri _ _
-  | Pxchg _ _ => Stuck 
+      Stuck                             (**r treated specially below *)
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers