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

This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.

14 files changed, 33 insertions, 3 deletions

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 87fcae8e..47cd3051 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -298,6 +298,7 @@ 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 *)
 .
@@ -1111,7 +1112,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfmsub _ _ _ _ _
   | Pfnmadd _ _ _ _ _
   | Pfnmsub _ _ _ _ _
-  | Pcfi_adjust _
+  | Pnop
+  | Pcfi_adjust _ 
   | Pcfi_rel_offset _ =>
       Stuck
   end.
diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml
index cbe1cf2f..471ad501 100644
--- a/aarch64/Asmexpand.ml
+++ b/aarch64/Asmexpand.ml
@@ -327,6 +327,8 @@ 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 f64083c4..e54673dd 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -473,6 +473,9 @@ 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 7f447c76..194074ac 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -232,6 +232,7 @@ 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 *)
@@ -814,6 +815,7 @@ 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 599d3d7b..e850fed6 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"; "Porr"; "Ppush"; "Prev";
+      "Pmul"; "Pmvn";  "Ploadsymbol_imm"; "Pnop"; "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,6 +268,7 @@ 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 5c7e5ad4..89aab5c7 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -409,6 +409,8 @@ 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 c19f36b0..03e06a65 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -306,6 +306,8 @@ 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 50caab12..dc410a3b 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -344,7 +344,8 @@ 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) *)
+              -> builtin_res preg -> instruction    (**r built-in function (pseudo) *)
+  | Pnop : instruction.                             (**r nop instruction *)
 
 
 (** The pseudo-instructions are the following:
@@ -985,6 +986,7 @@ 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 3c1ef39f..3e734747 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -468,6 +468,8 @@ 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 9cd8236c..64bcea4c 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -564,6 +564,8 @@ 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 bbed28cb..58e28c40 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -284,6 +284,7 @@ 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)
@@ -1002,6 +1003,7 @@ 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 5cf52b5e..16426ce3 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -473,6 +473,9 @@ 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 e7f714c7..f4f40a31 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -73,6 +73,9 @@ 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 30468fac..6159437e 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -797,6 +797,8 @@ 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) ->