From 6a010b47b216c5a6b6e85abcfbba5339bab15dd6 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 19 Oct 2017 13:08:13 +0200 Subject: New support for inserting ais-annotations. The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call. --- powerpc/AsmToJSON.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'powerpc/AsmToJSON.ml') diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index b542d7a7..a3e57e51 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -367,7 +367,7 @@ let pp_instructions pp ic = | EF_inline_asm _ -> instruction pp "Pinlineasm" [Id]; Cerrors.warning ("",-10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump" - | EF_annot (txt,targs) -> + | EF_annot (kind,txt,targs) -> let annot_string = PrintAsmaux.annot_text preg_annot "r1" (camlstring_of_coqstring txt) args in let len = String.length annot_string in let buf = Buffer.create len in @@ -376,7 +376,11 @@ let pp_instructions pp ic = | _ -> () end; Buffer.add_char buf c) annot_string; let annot_string = Buffer.contents buf in - instruction pp "Pannot" [String annot_string] + let kind = match P.to_int kind with + | 1 -> "normal" + | 2 -> "ais" + | _ -> assert false in + instruction pp "Pannot" [String kind;String annot_string] | EF_annot_val _ | EF_builtin _ | EF_debug _ @@ -423,7 +427,8 @@ let pp_section pp sec = | Section_debug_line _ | Section_debug_loc | Section_debug_ranges - | Section_debug_str -> () (* There should be no info in the debug sections *) + | Section_debug_str + | Section_ais_annotation -> () (* There should be no info in the debug sections *) let pp_int_opt pp = function | None -> fprintf pp "0" -- cgit