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 --- cfrontend/C2C.ml | 46 +++++++++++++++++++++++++++++++++++- cfrontend/Csyntax.v | 67 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 112 insertions(+), 1 deletion(-) (limited to 'cfrontend') 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 -- cgit