Remove `__builtin_nop` for some architectures. (#208)

The `__builtin_nop` function is documented only for PowerPC.
It was added to the other architectures by copy paste, but has no
known uses.  So, remove `__builtin_nop` from all architectures
but PowerPC.

14 files changed, 3 insertions, 33 deletions

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 47cd3051..87fcae8e 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -298,7 +298,6 @@ Inductive instruction: Type :=
   | Pbtbl (r1: ireg) (tbl: list label)                                (**r N-way branch through a jump table *)
   | Pbuiltin (ef: external_function)
              (args: list (builtin_arg preg)) (res: builtin_res preg)  (**r built-in function (pseudo) *)
-  | Pnop                                                              (**r no operation *)
   | Pcfi_adjust (ofs: int)                                            (**r .cfi_adjust debug directive *)
   | Pcfi_rel_offset (ofs: int)                                        (**r .cfi_rel_offset debug directive *)
 .
@@ -1112,8 +1111,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfmsub _ _ _ _ _
   | Pfnmadd _ _ _ _ _
   | Pfnmsub _ _ _ _ _
-  | Pnop
-  | Pcfi_adjust _ 
+  | Pcfi_adjust _
   | Pcfi_rel_offset _ =>
       Stuck
   end.
diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml
index 471ad501..cbe1cf2f 100644
--- a/aarch64/Asmexpand.ml
+++ b/aarch64/Asmexpand.ml
@@ -327,8 +327,6 @@ let expand_builtin_inline name args res =
   (* Synchronization *)
   | "__builtin_membar", [], _ ->
      ()
-  | "__builtin_nop", [], _ ->
-     emit Pnop
   (* Byte swap *)
   | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
      emit (Prev(W, res, a1))
diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index e54673dd..f64083c4 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -473,9 +473,6 @@ module Target : TARGET =
     (* Floating-point conditional select *)
     | Pfsel(rd, r1, r2, c) ->
         fprintf oc "	fcsel	%a, %a, %a, %s\n" dreg rd dreg r1 dreg r2 (condition_name c)
-    (* No-op *)
-    | Pnop ->
-        fprintf oc "	nop\n"
     (* Pseudo-instructions expanded in Asmexpand *)
     | Pallocframe(sz, linkofs) -> assert false
     | Pfreeframe(sz, linkofs) -> assert false
diff --git a/arm/Asm.v b/arm/Asm.v
index 194074ac..7f447c76 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -232,7 +232,6 @@ Inductive instruction : Type :=
   | Prev16: ireg -> ireg -> 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 *)
-  | Pnop : instruction                                (**r nop instruction *)
   (* 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 *)
@@ -815,7 +814,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfsqrt _ _
   | Prsc _ _ _
   | Psbc _ _ _
-  | Pnop
   | Padds _ _ _
   | Psubs _ _ _
   | Prsbs _ _ _
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index e850fed6..599d3d7b 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -34,7 +34,7 @@ let mnemonic_names = StringSet.of_list
       "Pfuitos"; "Pinlineasm"; "Pisb"; "Plabel"; "Pldr"; "Ploadsymbol_lbl";
       "Pldr_p"; "Pldrb"; "Pldrb_p"; "Pldrh"; "Pldrh_p"; "Pldrsb"; "Pldrsh";
       "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite"; "Pfmovite"; "Pmovt"; "Pmovw";
-      "Pmul"; "Pmvn";  "Ploadsymbol_imm"; "Pnop"; "Porr"; "Ppush"; "Prev";
+      "Pmul"; "Pmvn";  "Ploadsymbol_imm"; "Porr"; "Ppush"; "Prev";
       "Prev16"; "Prsb"; "Prsbs"; "Prsc"; "Psbc"; "Psbfx"; "Psdiv"; "Psmull";
       "Pstr"; "Pstr_p"; "Pstrb"; "Pstrb_p"; "Pstrh"; "Pstrh_p"; "Psub"; "Psubs";
       "Pudiv";"Pumull" ]
@@ -268,7 +268,6 @@ let pp_instructions pp ic =
     | Pmovw(r1, n) -> instruction pp "Pmovw" [Ireg r1; Long n]
     | Pmul(r1, r2, r3) -> instruction pp "Pmul" [Ireg r1; Ireg r2; Ireg r3]
     | Pmvn(r1, so) -> instruction pp "Pmvn" [Ireg r1; Shift so]
-    | Pnop -> instruction pp "Pnop" []
     | Porr(r1, r2, so) -> instruction pp "Porr" [Ireg r1; Ireg r2; Shift so]
     | Ppush(rl) -> instruction pp "Ppush" (List.map (fun r -> Ireg r) rl)
     | Prev(r1, r2) -> instruction pp "Prev" [Ireg r1; Ireg r2]
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 89aab5c7..5c7e5ad4 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -409,8 +409,6 @@ let expand_builtin_inline name args res =
   (* Vararg stuff *)
   | "__builtin_va_start", [BA(IR a)], _ ->
      expand_builtin_va_start a
-  | "__builtin_nop", [], _ ->
-     emit Pnop
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 03e06a65..c19f36b0 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -306,8 +306,6 @@ struct
       fprintf oc "	vsqrt.f64 %a, %a\n" freg f1 freg f2
     | Psbc (r1,r2,sa) ->
       fprintf oc "	sbc	%a, %a, %a\n" ireg r1 ireg r2 shift_op sa
-    | Pnop ->
-      fprintf oc "	nop\n"
     | Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) ->
       fprintf oc "	str	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa
     | Pstrb(r1, r2, sa) ->
diff --git a/riscV/Asm.v b/riscV/Asm.v
index dc410a3b..50caab12 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -344,8 +344,7 @@ Inductive instruction : Type :=
   | Ploadsi (rd: freg) (f: float32)                 (**r load an immediate single *)
   | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *)
   | Pbuiltin: external_function -> list (builtin_arg preg)
-              -> builtin_res preg -> instruction    (**r built-in function (pseudo) *)
-  | Pnop : instruction.                             (**r nop instruction *)
+              -> builtin_res preg -> instruction.   (**r built-in function (pseudo) *)
 
 
 (** The pseudo-instructions are the following:
@@ -986,7 +985,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfmsubd _ _ _ _
   | Pfnmaddd _ _ _ _
   | Pfnmsubd _ _ _ _
-  | Pnop
     => Stuck
   end.
 
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 3e734747..3c1ef39f 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -468,8 +468,6 @@ let expand_builtin_inline name args res =
                         (fun rl ->
                           emit (Pmulw (rl, X a, X b));
                           emit (Pmulhuw (rh, X a, X b)))
-  | "__builtin_nop", [], _ ->
-     emit Pnop
   (* Catch-all *)
   | _ ->
      raise (Error ("unrecognized builtin " ^ name))
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 64bcea4c..9cd8236c 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -564,8 +564,6 @@ module Target : TARGET =
          fprintf oc "	jr	x5\n";
          jumptables := (lbl, tbl) :: !jumptables;
          fprintf oc "%s end pseudoinstr btbl\n" comment
-      | Pnop ->
-        fprintf oc "	nop\n"
       | Pbuiltin(ef, args, res) ->
          begin match ef with
            | EF_annot(kind,txt, targs) ->
diff --git a/x86/Asm.v b/x86/Asm.v
index 58e28c40..bbed28cb 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -284,7 +284,6 @@ Inductive instruction: Type :=
   | Pmovsb
   | Pmovsw
   | Pmovw_rm (rd: ireg) (ad: addrmode)
-  | Pnop
   | Prep_movsl
   | Psbbl_rr (rd: ireg) (r2: ireg)
   | Psqrtsd (rd: freg) (r1: freg)
@@ -1003,7 +1002,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pmovsb
   | Pmovsw
   | Pmovw_rm _ _
-  | Pnop
   | Prep_movsl
   | Psbbl_rr _ _
   | Psqrtsd _ _
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index 16426ce3..5cf52b5e 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -473,9 +473,6 @@ let expand_builtin_inline name args res =
   (* Synchronization *)
   | "__builtin_membar", [], _ ->
      ()
-  (* no operation *)
-  | "__builtin_nop", [], _ ->
-     emit Pnop
   (* Catch-all *)
   | _ ->
      raise (Error ("unrecognized builtin " ^ name))
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index f4f40a31..e7f714c7 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -73,9 +73,6 @@ let builtins = {
       (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
     "__builtin_write32_reversed",
       (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
-    (* no operation *)
-    "__builtin_nop",
-      (TVoid [], [], false);
   ]
 }
 
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 6159437e..30468fac 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -797,8 +797,6 @@ module Target(System: SYSTEM):TARGET =
 	 fprintf oc "	movsw\n";
       | Pmovw_rm (rd, a) ->
           fprintf oc "	movw	%a, %a\n" addressing a ireg16 rd
-      | Pnop ->
-          fprintf oc "	nop\n"
       | Prep_movsl ->
 	 fprintf oc "	rep	movsl\n"
       | Psbbl_rr (res,a1) ->