From 591073be98300e1c07527af45c7c4ce8dff5bc39 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bschommer@users.noreply.github.com>
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
---
 backend/Asmexpandaux.ml | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

(limited to 'backend/Asmexpandaux.ml')

diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 07e33efa..1b250457 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -95,6 +95,16 @@ let translate_annot sp preg_to_dwarf annot =
   | [] -> None
   | a::_ -> aux a)
 
+let builtin_nop =
+  let signature ={sig_args = []; sig_res = None; sig_cc = cc_default} in
+  let name = coqstring_of_camlstring "__builtin_nop" in
+  Pbuiltin(EF_builtin(name,signature),[],BR_none)
+
+let rec lbl_follows = function
+  | Pbuiltin (EF_debug _, _, _):: rest ->
+    lbl_follows rest
+  | Plabel _ :: _ -> true
+  | _ -> false
 
 let expand_debug id sp preg simple l =
   let get_lbl = function
@@ -142,6 +152,11 @@ let expand_debug id sp preg simple l =
           | _ ->
               aux None scopes rest
         end
+    | (Pbuiltin(EF_annot (kind, _, _),_,_) as annot)::rest ->
+      if P.to_int kind = 2 && lbl_follows rest then begin
+        simple annot; simple builtin_nop; aux None scopes rest
+      end else
+        simple annot; aux None scopes rest
     | (Plabel lbl)::rest -> simple (Plabel lbl); aux (Some lbl) scopes rest
     | i::rest -> simple i; aux None scopes rest in
   (* We need to move all closing debug annotations before the last real statement *)
@@ -155,3 +170,20 @@ let expand_debug id sp preg simple l =
     | b::rest -> List.rev ((List.rev (b::bcc)@List.rev acc)@rest) (* We found the first non debug location *)
     | [] -> List.rev acc (* This actually can never happen *) in
   aux None [] (move_debug [] [] (List.rev l))
+
+let expand_simple simple l =
+  let rec aux = function
+   | (Pbuiltin(EF_annot (kind, _, _),_,_) as annot)::rest ->
+      if P.to_int kind = 2 && lbl_follows rest then begin
+        simple annot; simple builtin_nop; aux rest
+      end else
+        simple annot; aux rest
+   | i::rest -> simple i; aux rest
+   | [] -> () in
+  aux l
+
+let expand id sp preg simple l =
+  if !Clflags.option_g then
+    expand_debug id sp preg simple l
+  else
+    expand_simple simple l
-- 
cgit