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

This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.

3 files changed, 7 insertions, 1 deletions

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