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.
---
 x86/Asm.v            | 2 ++
 x86/Asmexpand.ml     | 3 +++
 x86/CBuiltins.ml     | 3 +++
 x86/TargetPrinter.ml | 2 ++
 4 files changed, 10 insertions(+)

(limited to 'x86')

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