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

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

1 files changed, 1 insertions, 38 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index dd434c02..2a120dd4 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -148,7 +148,6 @@ Inductive instruction : Type :=
   | Pmul: ireg -> ireg -> ireg -> instruction      (**r integer multiplication *)
   | Pmvn: ireg -> shift_op -> instruction          (**r integer complement *)
   | Porr: ireg -> ireg -> shift_op -> instruction  (**r bitwise or *)
-  | Ppush: list ireg -> instruction (** push registers on the stack instruction *)
   | Prsb: ireg -> ireg -> shift_op -> instruction  (**r integer reverse subtraction *)
   | Psbfx: ireg -> ireg -> int -> int -> instruction (**r signed bitfield extract *)
   | Pstr: ireg -> ireg -> shift_op -> instruction (**r int32 store *)
@@ -205,24 +204,7 @@ Inductive instruction : Type :=
   | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *)
   | Pbtbl: ireg -> list label -> instruction       (**r N-way branch through a jump table *)
   | Pbuiltin: external_function -> list preg -> list preg -> instruction  (**r built-in function *)
-  | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement *)
-  | Padc: ireg -> ireg -> shift_op -> instruction   (**r add with carry *)
-  | Pcfi_adjust: int -> instruction                 (**r .cfi_adjust debug directive *)
-  | Pclz: preg -> preg -> instruction               (**r count leading zeros. *)
-  | Pfsqrt: freg -> freg -> instruction             (**r floating-point square root. *)
-  | Prev: preg -> preg -> instruction               (**r reverse bytes and reverse bits. *)
-  | Prev16: preg -> preg -> instruction             (**r reverse bytes and reverse bits. *)
-  | Prsc: ireg -> ireg -> shift_op -> instruction (**r reverse subtract without carry. *)
-  | Psbc: ireg -> ireg -> shift_op -> instruction   (**r add with carry *)
-  (* Add, sub, rsb versions with s suffix *)
-  | Padds: ireg -> ireg -> shift_op -> instruction  (**r integer addition with update of condition flags *)
-  | Psubs: ireg -> ireg -> shift_op -> instruction  (**r integer subtraction with update of condition flags *)
-  | Prsbs: ireg -> ireg -> shift_op -> instruction  (**r integer reverse subtraction with update of condition flags *)
-  | Pdmb: instruction                               (**r data memory barrier *)
-  | Pdsb: instruction                               (**r data synchronization barrier *)
-  | Pisb: instruction                               (**r instruction synchronization barrier *)
-  | Pbne: label -> instruction.                     (**r branch if negative macro *)
-
+  | Pannot: external_function -> list (annot_arg preg) -> instruction. (**r annotation statement *)
 
 (** The pseudo-instructions are the following:
 
@@ -741,25 +723,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       end
   | 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. *)
-  | Ppush _
-  | Padc _ _ _
-  | Pcfi_adjust _
-  | Pclz _ _
-  | Prev _ _
-  | Prev16 _ _
-  | Pfsqrt _ _
-  | Prsc _ _ _
-  | Psbc _ _ _
-  | Padds _ _ _
-  | Psubs _ _ _
-  | Prsbs _ _ _
-  | Pdmb
-  | Pdsb
-  | Pisb
-  | Pbne _ =>
-    Stuck
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers