From 591073be98300e1c07527af45c7c4ce8dff5bc39 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 12 Sep 2018 14:32:01 +0200 Subject: 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 --- x86/Asm.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'x86/Asm.v') diff --git a/x86/Asm.v b/x86/Asm.v index 7b4a29f4..dfa2a88a 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) @@ -1001,6 +1002,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmovsb | Pmovsw | Pmovw_rm _ _ + | Pnop | Prep_movsl | Psbbl_rr _ _ | Psqrtsd _ _ -- cgit