From 99f47c7a99b11c9cc3429fc0e5d0e21ae3707518 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 1 Sep 2010 08:36:03 +0000 Subject: Adding __builtin_annotation git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/PrintAsm.ml | 34 +++++++++++++++++++++++- cfrontend/C2C.ml | 46 ++++++++++++++++++++++++++++++++- cfrontend/Csyntax.v | 67 ++++++++++++++++++++++++++++++++++++++++++++++++ cparser/Elab.ml | 11 ++++++++ powerpc/PrintAsm.ml | 32 ++++++++++++++++++++++- powerpc/eabi/CPragmas.ml | 16 ++++++------ test/regression/Makefile | 2 +- test/regression/annot1.c | 23 +++++++++++++++++ 8 files changed, 219 insertions(+), 12 deletions(-) create mode 100644 test/regression/annot1.c 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 "" 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 "" 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 + +/* 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; +} + -- cgit