summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-09-01 08:36:03 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-09-01 08:36:03 +0000
commit99f47c7a99b11c9cc3429fc0e5d0e21ae3707518 (patch)
treef452a9d6f8ec4c4573a7ca55581a0060d315f510
parent1b8e228a2c5d8f63ffa28c1fcef68f64a0408900 (diff)
Adding __builtin_annotation
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--arm/PrintAsm.ml34
-rw-r--r--cfrontend/C2C.ml46
-rw-r--r--cfrontend/Csyntax.v67
-rw-r--r--cparser/Elab.ml11
-rw-r--r--powerpc/PrintAsm.ml32
-rw-r--r--powerpc/eabi/CPragmas.ml16
-rw-r--r--test/regression/Makefile2
-rw-r--r--test/regression/annot1.c23
8 files changed, 219 insertions, 12 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index c2fc8a9..9e1cae7 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 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
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index b3e375c..2ae7c7e 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 f23515f..9df9cc0 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 7dbc215..817584a 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 44e1718..55b07f5 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 0000000..42ab826
--- /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;
+}
+