Generate a nop instruction after some ais annotations (#137)

* Generate a nop instruction after ais annotations.

In order to prevent the merging of ais annotations with following
Labels a nop instruction is inserted, but only if the annotation
is followed immediately by a label.

The insertion of nop instructions is performed during the
expansion of builtin and pseudo assembler instructions and is
processor independent, by inserting a __builtin_nop built-in.

* Add Pnop instruction to ARM, RISC-V, and x86

ARM as well as RISC-V don't have nop instructions that can
be easily encoded by for example add with zero instructions.
For x86 we used to use `mov X0, X0` for nop but this may
not be as efficient as the true nop instruction.

* Implement __builtin_nop on all supported target architectures.

This builtin is not yet made available on the C side for all architectures.

Bug 24067

1 files changed, 2 insertions, 0 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 07dea756..e6d1b4fc 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -231,6 +231,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 *)
@@ -805,6 +806,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfsqrt _ _
   | Prsc _ _ _
   | Psbc _ _ _
+  | Pnop
   | Padds _ _ _
   | Psubs _ _ _
   | Prsbs _ _ _