Adding __builtin_annotation

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

8 files changed, 219 insertions, 12 deletions

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index c2fc8a9e..9e1cae75 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -284,6 +284,35 @@ let print_builtin_function oc s =
   fprintf oc "%s end %s\n" comment (extern_atom s);
   n
 
+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";
+  begin 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
+  end;
+  0
+
 (* Printing of instructions *)
 
 let shift_op oc = function
@@ -482,7 +511,10 @@ let print_instruction oc labels = function
         tbl;
       2 + List.length tbl
   | 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 no_fallthrough = function
   | Pb _ -> true
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index feac4f0c..6649a2c8 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -107,6 +107,11 @@ let builtins_generic = {
            [TPtr(TVoid [], []); 
             TPtr(TVoid [AConst], []); 
             TInt(Cutil.size_t_ikind, [])],
+          false);
+    (* Annotations *)
+    "__builtin_annotation",
+        (TVoid [],                      (* overriden during elaboration *)
+          [TPtr(TInt(IChar, [AConst]), [])],
           false)
   ]
 }
@@ -194,6 +199,30 @@ let declare_stub_functions k =
   Hashtbl.fold (fun n i k -> declare_stub_function n i :: k)
                stub_function_table k
 
+(** ** Handling of annotations *)
+
+let annot_function_list = ref []
+let annot_function_next = ref 0
+
+let register_annotation_function txt targs tres =
+  incr annot_function_next;
+  let fun_name =
+    intern_string
+      (Printf.sprintf "__builtin_annotation_%d" !annot_function_next)
+  and ext_ident =
+    intern_string
+      (Printf.sprintf "__builtin_annotation_\"%s\"" txt) in
+  annot_function_list :=
+      Datatypes.Coq_pair(fun_name,
+        External({ ef_id = ext_ident;
+                   ef_sig = signature_of_type targs tres;
+                   ef_inline = true },
+                 targs, tres)) :: !annot_function_list;
+  Evalof(Evar(fun_name, Tfunction(targs, tres)), Tfunction(targs, tres))
+
+let declare_annotation_functions k =
+  List.rev_append !annot_function_list k
+
 (** ** Translation functions *)
 
 (** Constants *)
@@ -455,6 +484,20 @@ let rec convertExpr env e =
       Econdition(convertExpr env e1, convertExpr env e2, convertExpr env e3, ty)
   | C.ECast(ty1, e1) ->
       Ecast(convertExpr env e1, convertTyp env ty1)
+
+  | C.ECall({edesc = C.EVar {name = "__builtin_annotation"}}, args) ->
+      begin match args with
+      | {edesc = C.EConst(CStr txt)} :: args1 ->
+          if List.length args1 > 2 then
+            error "too many arguments to __builtin_annotation";
+          let targs1 = convertTypList env (List.map (fun e -> e.etyp) args1) in
+          let fn' = register_annotation_function txt targs1 ty in
+          Ecall(fn', convertExprList env args1, ty)
+      | _ ->
+          error "ill-formed __builtin_annotation (first argument must be string literal)";
+          ezero
+      end          
+
   | C.ECall(fn, args) ->
       match projFunType env fn.etyp with
       | None ->
@@ -893,10 +936,11 @@ let convertProgram p =
     let (funs1, vars1) =
       convertGlobdecls (translEnv Env.empty p) [] [] (cleanupGlobals p) in
     let funs2 = declare_stub_functions funs1 in
+    let funs3 = declare_annotation_functions funs2 in
     let vars2 = globals_for_strings vars1 in
     if !numErrors > 0
     then None
-    else Some { AST.prog_funct = funs2;
+    else Some { AST.prog_funct = funs3;
                 AST.prog_vars = vars2;
                 AST.prog_main = intern_string "main" }
   with Env.Error msg ->
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 6e9a860a..8560d5e6 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -665,6 +665,73 @@ Definition access_mode (ty: type) : mode :=
   | Tcomp_ptr _ => By_value Mint32
 end.
 
+(** Unroll the type of a structure or union field, substituting
+    [Tcomp_ptr] by a pointer to the structure. *)
+
+Section UNROLL_COMPOSITE.
+
+Variable cid: ident.
+Variable comp: type.
+
+Fixpoint unroll_composite (ty: type) : type :=
+  match ty with
+  | Tvoid => ty
+  | Tint _ _ => ty
+  | Tfloat _ => ty
+  | Tpointer t1 => Tpointer (unroll_composite t1)
+  | Tarray t1 sz => Tarray (unroll_composite t1) sz
+  | Tfunction t1 t2 => Tfunction (unroll_composite_list t1) (unroll_composite t2)
+  | Tstruct id fld => if ident_eq id cid then ty else Tstruct id (unroll_composite_fields fld)
+  | Tunion id fld => if ident_eq id cid then ty else Tunion id (unroll_composite_fields fld)
+  | Tcomp_ptr id => if ident_eq id cid then Tpointer comp else ty
+  end
+
+with unroll_composite_list (tl: typelist) : typelist :=
+  match tl with
+  | Tnil => Tnil
+  | Tcons t1 tl' => Tcons (unroll_composite t1) (unroll_composite_list tl')
+  end
+
+with unroll_composite_fields (fld: fieldlist) : fieldlist :=
+  match fld with
+  | Fnil => Fnil
+  | Fcons id ty fld' => Fcons id (unroll_composite ty) (unroll_composite_fields fld')
+  end.
+
+Lemma alignof_unroll_composite:
+  forall ty, alignof (unroll_composite ty) = alignof ty.
+Proof.
+  apply (type_ind2 (fun ty => alignof (unroll_composite ty) = alignof ty)
+                   (fun fld => alignof_fields (unroll_composite_fields fld) = alignof_fields fld));
+  simpl; intros; auto.
+  destruct (ident_eq i cid); auto. 
+  destruct (ident_eq i cid); auto. 
+  destruct (ident_eq i cid); auto.
+  decEq; auto.
+Qed.
+
+Lemma sizeof_unroll_composite:
+  forall ty, sizeof (unroll_composite ty) = sizeof ty.
+Proof.
+Opaque alignof.
+  apply (type_ind2 (fun ty => sizeof (unroll_composite ty) = sizeof ty)
+                   (fun fld => 
+                      sizeof_union (unroll_composite_fields fld) = sizeof_union fld
+                   /\ forall pos,
+                      sizeof_struct (unroll_composite_fields fld) pos = sizeof_struct fld pos));
+  simpl; intros; auto.
+  congruence.
+  destruct H. rewrite <- (alignof_unroll_composite (Tstruct i f)).
+  simpl. destruct (ident_eq i cid); simpl. auto. rewrite H0; auto.
+  destruct H. rewrite <- (alignof_unroll_composite (Tunion i f)).
+  simpl. destruct (ident_eq i cid); simpl. auto. rewrite H; auto.
+  destruct (ident_eq i cid); auto.
+  destruct H0. split. congruence.
+  intros. rewrite alignof_unroll_composite. rewrite H1. rewrite H. auto.
+Qed.
+
+End UNROLL_COMPOSITE.
+
 (** Classification of arithmetic operations and comparisons.
   The following [classify_] functions take as arguments the types
   of the arguments of an operation.  They return enough information
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index b3e375cd..2ae7c7e9 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -778,6 +778,17 @@ let elab_expr loc env a =
       let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in
       { edesc = ECall(b1, [b2; b3]); etyp = ty }
 
+(* Hack to treat __builtin_annotation the CompCert way.
+   Arguments are treated as per the prototype (const char *, ...).
+   Result type is type of second argument, or void if only one argument. *)
+  | CALL((VARIABLE "__builtin_annotation" as a1), al) ->
+      let b1 = elab a1 in
+      let bl = List.map elab al in
+      let bl' = elab_arguments 1 bl [Env.fresh_ident "",
+                                     TPtr(TInt(IChar, [AConst]),[])] true in
+      let tyres = match bl' with _ :: b2 :: _ -> b2.etyp | _ -> TVoid[] in
+      { edesc = ECall(b1, bl'); etyp = tyres }
+
   | CALL(a1, al) ->
       let b1 =
         (* Catch the old-style usage of calling a function without
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
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 44e1718e..55b07f56 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -13,7 +13,7 @@ TESTS=bitfields1 bitfields2 bitfields3 bitfields4 \
   funct3 expr5 struct7 struct8 casts1 casts2
 
 # Other tests: should compile to .s without errors (but expect warnings)
-EXTRAS=commaprec expr2 expr3 expr4 extern1 funct2 funptr1 init1 \
+EXTRAS=annot1 commaprec expr2 expr3 expr4 extern1 funct2 funptr1 init1 \
   init2 init3 init4 pragmas ptrs1 ptrs2 sizeof1 struct1 struct2 struct3 \
   struct4 struct5 struct6 types1 volatile1
 
diff --git a/test/regression/annot1.c b/test/regression/annot1.c
new file mode 100644
index 00000000..42ab826f
--- /dev/null
+++ b/test/regression/annot1.c
@@ -0,0 +1,23 @@
+#include <stdio.h>
+
+/* Annotations */
+
+int f(int x, int y)
+{
+  return __builtin_annotation("f(%1,%2)", x, y);
+}
+
+double g(double x)
+{
+  return __builtin_annotation("g(%1 + 1.0)", x + 1.0);
+}
+
+int main()
+{
+  __builtin_annotation("calling f");
+  printf("f returns %d\n", f(12, 34));
+  __builtin_annotation("calling g");
+  printf("f returns %.2f\n", g(3.14));
+  return 0;
+}
+