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 ++++++++++++++++++++++++++++++++
 backend/Asmexpandaux.mli |  6 +++---
 2 files changed, 35 insertions(+), 3 deletions(-)

(limited to 'backend')

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
diff --git a/backend/Asmexpandaux.mli b/backend/Asmexpandaux.mli
index 797eb10c..d80b4aec 100644
--- a/backend/Asmexpandaux.mli
+++ b/backend/Asmexpandaux.mli
@@ -31,6 +31,6 @@ val set_current_function: coq_function -> unit
   (* Set the current function *)
 val get_current_function: unit -> coq_function
   (* Get the current function *)
-val expand_debug: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit
-  (* Expand builtin debug function. Takes the function id, the register number of the stackpointer, a
-     function to get the dwarf mapping of varibale names  and for the expansion of simple instructions *)
+val expand: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit
+  (* Expand the instruction sequence of a function. Takes the function id, the register number of the stackpointer, a
+     function to get the dwarf mapping of varibale names and for the expansion of simple instructions *)
-- 
cgit