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/TargetPrinter.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'x86/TargetPrinter.ml') 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 -- cgit