Adding __builtin_annotation

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

2 files changed, 112 insertions, 1 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index feac4f0..6649a2c 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 6e9a860..8560d5e 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