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

14 files changed, 64 insertions, 28 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 _ _ _
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index 276ceecc..3874e141 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -30,7 +30,7 @@ let mnemonic_names = [ "Padc"; "Padd"; "Padds"; "Pand";"Pannot"; "Pasr"; "Pb"; "
                        "Pftouizs"; "Pfuitod"; "Pfuitos"; "Pinlineasm"; "Pisb"; "Plabel"; "Pldr";
                        "Ploadsymbol_lbl"; "Pldr_p"; "Pldrb"; "Pldrb_p"; "Pldrh"; "Pldrh_p"; "Pldrsb";
                        "Pldrsh"; "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite";
-                       "Pmovt"; "Pmovw"; "Pmul"; "Pmvn";  "Ploadsymbol_imm"; "Porr";
+                       "Pmovt"; "Pmovw"; "Pmul"; "Pmvn";  "Ploadsymbol_imm"; "Pnop"; "Porr";
                        "Ppush"; "Prev"; "Prev16"; "Prsb"; "Prsbs"; "Prsc"; "Psbc"; "Psbfx"; "Psdiv"; "Psmull";
                        "Pstr"; "Pstr_p"; "Pstrb"; "Pstrb_p"; "Pstrh"; "Pstrh_p"; "Psub"; "Psubs"; "Pudiv";
                        "Pumull" ]
@@ -263,6 +263,7 @@ let pp_instructions pp ic =
     | Pmovw(r1, n) -> instruction pp "Pmovw" [Ireg r1; Long n]
     | Pmul(r1, r2, r3) -> instruction pp "Pmul" [Ireg r1; Ireg r2; Ireg r3]
     | Pmvn(r1, so) -> instruction pp "Pmvn" [Ireg r1; Shift so]
+    | Pnop -> instruction pp "Pnop" []
     | Porr(r1, r2, so) -> instruction pp "Porr" [Ireg r1; Ireg r2; Shift so]
     | Ppush(rl) -> instruction pp "Ppush" (List.map (fun r -> Ireg r) rl)
     | Prev(r1, r2) -> instruction pp "Prev" [Ireg r1; Ireg r2]
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 7c18be6b..d9424d11 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -404,6 +404,8 @@ let expand_builtin_inline name args res =
   (* Vararg stuff *)
   | "__builtin_va_start", [BA(IR a)], _ ->
      expand_builtin_va_start a
+  | "__builtin_nop", [], _ ->
+     emit Pnop
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
@@ -665,10 +667,7 @@ let expand_function id fn =
   try
     set_current_function fn;
     fixup_arguments Incoming fn.fn_sig;
-    if !Clflags.option_g then
-      expand_debug id 13 preg_to_dwarf expand_instruction fn.fn_code
-    else
-      List.iter expand_instruction fn.fn_code;
+    expand id 13 preg_to_dwarf expand_instruction fn.fn_code;
     let fn = get_current_function () in
     let fn = Constantexpand.expand_constants fn in
     Errors.OK fn
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 52d2ada6..bf37b0e4 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -306,6 +306,8 @@ struct
       fprintf oc "	vsqrt.f64 %a, %a\n" freg f1 freg f2
     | Psbc (r1,r2,sa) ->
       fprintf oc "	sbc	%a, %a, %a\n" ireg r1 ireg r2 shift_op sa
+    | Pnop ->
+      fprintf oc "	nop\n"
     | Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) ->
       fprintf oc "	str	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa
     | Pstrb(r1, r2, sa) ->
@@ -463,7 +465,7 @@ struct
               | 1 -> let annot = annot_text preg_annot "sp" (camlstring_of_coqstring txt) args in
                 fprintf oc "%s annotation: %S\n" comment annot
               | 2 -> let lbl = new_label () in
-                fprintf oc "%a: " label lbl;
+                fprintf oc "%a:\n" label lbl;
                 AisAnnot.add_ais_annot lbl preg_annot "r13" (camlstring_of_coqstring txt) args
               | _ -> assert false
             end
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 *)
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index a17be2ee..5a2df8d3 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -891,7 +891,7 @@ let expand_instruction instr =
           expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
       | EF_annot_val(kind,txt, targ) ->
           expand_annot_val kind txt targ args res
-       | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
+      | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
           emit instr
       | _ ->
           assert false
@@ -932,10 +932,7 @@ let preg_to_dwarf = function
 let expand_function id fn =
   try
     set_current_function fn;
-    if !Clflags.option_g then
-      expand_debug id 1 preg_to_dwarf expand_instruction fn.fn_code
-    else
-      List.iter expand_instruction fn.fn_code;
+    expand id 1 preg_to_dwarf expand_instruction fn.fn_code;
     Errors.OK (get_current_function ())
   with Error s ->
     Errors.Error (Errors.msg (coqstring_of_camlstring s))
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 3e11406c..d8b0ee4b 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -844,7 +844,7 @@ module Target (System : SYSTEM):TARGET =
                 fprintf oc "%s annotation: %S\n" comment annot
 
               | 2 -> let lbl = new_label () in
-                fprintf oc "%a: " label lbl;
+                fprintf oc "%a:\n" label lbl;
                 add_ais_annot lbl preg_annot "r1" (camlstring_of_coqstring txt) args
               | _ -> assert false
               end
diff --git a/riscV/Asm.v b/riscV/Asm.v
index 6d223c1d..1d8fda11 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 0a7f8a8a..3e734747 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -468,7 +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))
@@ -598,10 +599,7 @@ let preg_to_dwarf = function
 let expand_function id fn =
   try
     set_current_function fn;
-    if !Clflags.option_g then
-      expand_debug id (* sp= *) 2 preg_to_dwarf expand_instruction fn.fn_code
-    else
-      List.iter expand_instruction fn.fn_code;
+    expand id (* sp= *) 2 preg_to_dwarf expand_instruction fn.fn_code;
     Errors.OK (get_current_function ())
   with Error s ->
     Errors.Error (Errors.msg (coqstring_of_camlstring s))
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index e3fbfe36..19704bad 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) ->
@@ -571,7 +573,7 @@ module Target : TARGET =
                | 1 -> let annot = annot_text preg_annot "x2" (camlstring_of_coqstring txt) args  in
                  fprintf oc "%s annotation: %S\n" comment annot
                | 2 -> let lbl = new_label () in
-                 fprintf oc "%a: " label lbl;
+                 fprintf oc "%a:\n" label lbl;
                  add_ais_annot lbl preg_annot "x2" (camlstring_of_coqstring txt) args
                | _ -> assert false
              end
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 _ _
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index 99666920..16426ce3 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -475,7 +475,7 @@ let expand_builtin_inline name args res =
      ()
   (* no operation *)
   | "__builtin_nop", [], _ ->
-     emit (Pmov_rr (RAX,RAX))
+     emit Pnop
   (* Catch-all *)
   | _ ->
      raise (Error ("unrecognized builtin " ^ name))
@@ -632,10 +632,7 @@ let preg_to_dwarf = function
 let expand_function id fn =
   try
     set_current_function fn;
-    if !Clflags.option_g then
-      expand_debug id (int_reg_to_dwarf RSP) preg_to_dwarf expand_instruction fn.fn_code
-    else
-      List.iter expand_instruction fn.fn_code;
+    expand id (int_reg_to_dwarf RSP) preg_to_dwarf expand_instruction fn.fn_code;
     Errors.OK (get_current_function ())
   with Error s ->
     Errors.Error (Errors.msg (coqstring_of_camlstring s))
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 1bb8c226..3ac2f36e 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -791,6 +791,8 @@ module Target(System: SYSTEM):TARGET =
 	 fprintf oc "	movsw\n";
       | Pmovw_rm (rd, a) ->
           fprintf oc "	movw	%a, %a\n" addressing a ireg16 rd
+      | Pnop ->
+          fprintf oc "	nop\n"
       | Prep_movsl ->
 	 fprintf oc "	rep	movsl\n"
       | Psbbl_rr (res,a1) ->
@@ -814,7 +816,7 @@ module Target(System: SYSTEM):TARGET =
                   | 1 ->  let annot = annot_text preg_annot "esp" (camlstring_of_coqstring txt) args in
                     fprintf oc "%s annotation: %S\n" comment annot
                   | 2 -> let lbl = new_label () in
-                    fprintf oc "%a: \n" label lbl;
+                    fprintf oc "%a:\n" label lbl;
                     let sp = if Archi.ptr64 then "rsp" else "esp" in
                     add_ais_annot lbl preg_ais_annot sp (camlstring_of_coqstring txt) args
                   | _ -> assert false