From 7077c2ea9e86f001e805d7a2a5e7fcdfd0a8ece8 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 2 Jan 2020 14:58:37 +0100
Subject: Revert "Remove `__builtin_nop` for some architectures. (#208)"

This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
---
 aarch64/Asm.v            | 4 +++-
 aarch64/Asmexpand.ml     | 2 ++
 aarch64/TargetPrinter.ml | 3 +++
 3 files changed, 8 insertions(+), 1 deletion(-)

(limited to 'aarch64')

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
-- 
cgit