Adding __builtin_annotation

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 39 insertions, 9 deletions

diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index f23515f5..9df9cc0a 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -389,6 +389,33 @@ let print_builtin_function oc s =
   end;
   fprintf oc "%s end builtin function %s\n" comment (extern_atom s)
 
+let re_builtin_annotation = Str.regexp "__builtin_annotation_\"\\(.*\\)\"$"
+
+let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
+
+let print_annotation oc txt args res =
+  fprintf oc "%s annotation: " comment;
+  let print_fragment = function
+  | Str.Text s ->
+      output_string oc s
+  | Str.Delim "%%" ->
+      output_char oc '%'
+  | Str.Delim s ->
+      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
+      try
+        preg oc (List.nth args (n-1))
+      with Failure _ ->
+        fprintf oc "<bad parameter %s>" s in
+  List.iter print_fragment (Str.full_split re_annot_param txt);
+  fprintf oc "\n";
+  match args, res with
+  | [], _ -> ()
+  | IR src :: _, IR dst ->
+      if dst <> src then fprintf oc "	mr	%a, %a\n" ireg dst ireg src 
+  | FR src :: _, FR dst ->
+      if dst <> src then fprintf oc "	fmr	%a, %a\n" freg dst freg src 
+  | _, _ -> assert false
+
 (* Printing of instructions *)
 
 module Labelset = Set.Make(struct type t = label let compare = compare end)
@@ -667,7 +694,10 @@ let print_instruction oc labels = function
       if Labelset.mem lbl labels then
         fprintf oc "%a:\n" label (transl_label lbl)
   | Pbuiltin(ef, args, res) ->
-      print_builtin_inlined oc (extern_atom ef.ef_id) args res
+      let name = extern_atom ef.ef_id in
+      if Str.string_match re_builtin_annotation name 0
+      then print_annotation oc (Str.matched_group 1 name) args res
+      else print_builtin_inlined oc name args res
 
 let print_literal oc (lbl, n) =
   let nlo = Int64.to_int32 n
diff --git a/powerpc/eabi/CPragmas.ml b/powerpc/eabi/CPragmas.ml
index 7dbc2157..817584ae 100644
--- a/powerpc/eabi/CPragmas.ml
+++ b/powerpc/eabi/CPragmas.ml
@@ -35,20 +35,20 @@ let process_section_pragma classname istring ustring addrmode accmode =
 
 let process_use_section_pragma classname id =
   if not (Sections.use_section_for (intern_string id) classname)
-  then C2Clight.error (sprintf "unknown section name `%s'" classname)
+  then C2C.error (sprintf "unknown section name `%s'" classname)
 
 (* #pragma reserve_register *)
 
 let process_reserve_register_pragma name =
   match Machregsaux.register_by_name name with
   | None ->
-      C2Clight.error "unknown register in `reserve_register' pragma"
+      C2C.error "unknown register in `reserve_register' pragma"
   | Some r ->
       if Machregsaux.can_reserve_register r then
         Coloringaux.reserved_registers :=
           r :: !Coloringaux.reserved_registers
       else
-        C2Clight.error "cannot reserve this register (not a callee-save)"
+        C2C.error "cannot reserve this register (not a callee-save)"
 
 (* Parsing of pragmas using regexps *)
 
@@ -87,22 +87,22 @@ let process_pragma name =
       (Str.matched_group 5 name); (* accmode *)
     true
   end else if Str.string_match re_start_pragma_section name 0 then
-    (C2Clight.error "ill-formed `section' pragma"; true)
+    (C2C.error "ill-formed `section' pragma"; true)
  else if Str.string_match re_pragma_use_section name 0 then begin
     let classname = Str.matched_group 1 name
     and idents = Str.matched_group 2 name in
     let identlist = Str.split re_split_idents idents in
-    if identlist = [] then C2Clight.warning "vacuous `use_section' pragma";
+    if identlist = [] then C2C.warning "vacuous `use_section' pragma";
     List.iter (process_use_section_pragma classname) identlist;
     true
   end else if Str.string_match re_start_pragma_use_section name 0 then begin
-    C2Clight.error "ill-formed `use_section' pragma"; true
+    C2C.error "ill-formed `use_section' pragma"; true
   end else if Str.string_match re_pragma_reserve_register name 0 then begin
     process_reserve_register_pragma (Str.matched_group 1 name); true
   end else if Str.string_match re_start_pragma_reserve_register name 0 then begin
-    C2Clight.error "ill-formed `reserve_register' pragma"; true
+    C2C.error "ill-formed `reserve_register' pragma"; true
   end else
     false
 
 let initialize () =
-  C2Clight.process_pragma_hook := process_pragma
+  C2C.process_pragma_hook := process_pragma