From 0a9e21307d3abd1612bc95f9552dc2fe110742b5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 23 Mar 2013 10:17:10 +0000 Subject: Watch out for behaviors exponential in the nesting of struct/union types. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/C2C.ml | 61 ++++++++++++++++++++++++++++++++++--------- cfrontend/Initializers.v | 6 +++-- cfrontend/Initializersproof.v | 16 +++++------- cfrontend/PrintClight.ml | 31 +++------------------- cfrontend/PrintCsyntax.ml | 28 +++++++++----------- 5 files changed, 76 insertions(+), 66 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index f80b379..44d07e6 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -204,6 +204,20 @@ let convertInt n = coqint_of_camlint(Int64.to_int32 n) let convertAttr a = List.mem AVolatile a +let mergeAttr a1 a2 = a1 || a2 + +let mergeTypAttr ty a2 = + match ty with + | Tvoid -> ty + | Tint(sz, sg, a1) -> Tint(sz, sg, mergeAttr a1 a2) + | Tfloat(sz, a1) -> Tfloat(sz, mergeAttr a1 a2) + | Tpointer(ty', a1) -> Tpointer(ty', mergeAttr a1 a2) + | Tarray(ty', sz, a1) -> Tarray(ty', sz, mergeAttr a1 a2) + | Tfunction(targs, tres) -> ty + | Tstruct(id, fld, a1) -> Tstruct(id, fld, mergeAttr a1 a2) + | Tunion(id, fld, a1) -> Tunion(id, fld, mergeAttr a1 a2) + | Tcomp_ptr(id, a1) -> Tcomp_ptr(id, mergeAttr a1 a2) + (** Types *) let convertIkind = function @@ -237,6 +251,10 @@ let int64_struct a = else Fcons(intern_string "lo", ty, Fcons(intern_string "hi", ty, Fnil))), a) +(** A cache for structs and unions already converted *) + +let compositeCache : (C.ident, coq_type) Hashtbl.t = Hashtbl.create 77 + let convertTyp env t = let rec convertTyp seen t = @@ -276,19 +294,29 @@ let convertTyp env t = | C.TNamed _ -> assert false | C.TStruct(id, a) -> - let flds = - try - convertFields (id :: seen) (Env.find_struct env id) - with Env.Error e -> - error (Env.error_message e); Fnil in - Tstruct(intern_string("struct " ^ id.name), flds, convertAttr a) + let a' = convertAttr a in + begin try + mergeTypAttr (Hashtbl.find compositeCache id) a' + with Not_found -> + let flds = + try + convertFields (id :: seen) (Env.find_struct env id) + with Env.Error e -> + error (Env.error_message e); Fnil in + Tstruct(intern_string("struct " ^ id.name), flds, a') + end | C.TUnion(id, a) -> - let flds = - try - convertFields (id :: seen) (Env.find_union env id) - with Env.Error e -> - error (Env.error_message e); Fnil in - Tunion(intern_string("union " ^ id.name), flds, convertAttr a) + let a' = convertAttr a in + begin try + mergeTypAttr (Hashtbl.find compositeCache id) a' + with Not_found -> + let flds = + try + convertFields (id :: seen) (Env.find_union env id) + with Env.Error e -> + error (Env.error_message e); Fnil in + Tunion(intern_string("union " ^ id.name), flds, a') + end | C.TEnum(id, a) -> let (sg, sz) = convertIkind Cutil.enum_ikind in Tint(sz, sg, convertAttr a) @@ -313,6 +341,12 @@ let rec convertTypList env = function | [] -> Tnil | t1 :: tl -> Tcons(convertTyp env t1, convertTypList env tl) +let cacheCompositeDef env su id attr flds = + (* we currently ignore attributes on structs and unions *) + let ty = + match su with C.Struct -> C.TStruct(id, []) | C.Union -> C.TUnion(id, []) in + Hashtbl.add compositeCache id (convertTyp env ty) + let rec projFunType env ty = match Cutil.unroll env ty with | TFun(res, args, vararg, attr) -> Some(res, vararg) @@ -854,6 +888,8 @@ let rec convertGlobdecls env res gl = | C.Gcompositedef(su, id, attr, flds) -> (* sanity checks on fields *) checkComposite env su id attr flds; + (* convert it to a CompCert C type and cache this type *) + cacheCompositeDef env su id attr flds; convertGlobdecls env res gl' | C.Gpragma s -> if not (!process_pragma_hook s) then @@ -937,6 +973,7 @@ let convertProgram p = stringNum := 0; Hashtbl.clear decl_atom; Hashtbl.clear stringTable; + Hashtbl.clear compositeCache; Hashtbl.clear special_externals_table; let p = Builtins.declarations() @ p in try diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 8757ba2..7711ade 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -151,10 +151,12 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data := | Vint n, Tint I16 sg _ => OK(Init_int16 n) | Vint n, Tint I32 sg _ => OK(Init_int32 n) | Vint n, Tpointer _ _ => OK(Init_int32 n) + | Vint n, Tcomp_ptr _ _ => OK(Init_int32 n) | Vfloat f, Tfloat F32 _ => OK(Init_float32 f) | Vfloat f, Tfloat F64 _ => OK(Init_float64 f) | Vptr (Zpos id) ofs, Tint I32 sg _ => OK(Init_addrof id ofs) | Vptr (Zpos id) ofs, Tpointer _ _ => OK(Init_addrof id ofs) + | Vptr (Zpos id) ofs, Tcomp_ptr _ _ => OK(Init_addrof id ofs) | Vundef, _ => Error(msg "undefined operation in initializer") | _, _ => Error (msg "type mismatch in initializer") end. @@ -208,7 +210,7 @@ with transl_init_struct (id: ident) (ty: type) OK (padding pos (sizeof ty)) | Init_cons i1 il', Fcons _ ty1 fl' => let pos1 := align pos (alignof ty1) in - do d1 <- transl_init (unroll_composite id ty ty1) i1; + do d1 <- transl_init ty1 i1; do d2 <- transl_init_struct id ty fl' il' (pos1 + sizeof ty1); OK (padding pos pos1 ++ d1 ++ d2) | _, _ => @@ -221,7 +223,7 @@ with transl_init_union (id: ident) (ty ty1: type) (il: initializer_list) | Init_nil => Error (msg "empty union initializer") | Init_cons i1 _ => - do d <- transl_init (unroll_composite id ty ty1) i1; + do d <- transl_init ty1 i1; OK (d ++ padding (sizeof ty1) (sizeof ty)) end. diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index b0884ac..75b73ff 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -605,7 +605,8 @@ Proof. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. (* pointer *) assert (data = Init_addrof id ofs0 /\ chunk = Mint32). - destruct ty; inv EQ2; inv H2. destruct i; inv H5. intuition congruence. auto. + destruct ty; inv EQ2; inv H2. + destruct i; inv H5. intuition congruence. auto. destruct H4; subst. rewrite H. assumption. (* undef *) discriminate. @@ -754,13 +755,13 @@ Proof. repeat rewrite idlsize_app. simpl in H0. rewrite padding_size. - rewrite (transl_init_size _ _ _ EQ). rewrite sizeof_unroll_composite. + rewrite (transl_init_size _ _ _ EQ). rewrite <- (B _ _ _ _ _ EQ1). omega. auto. apply align_le. apply alignof_pos. (* unions *) intros. simpl in H. monadInv H. rewrite idlsize_app. - rewrite (transl_init_size _ _ _ EQ). rewrite sizeof_unroll_composite. + rewrite (transl_init_size _ _ _ EQ). rewrite padding_size. omega. auto. Qed. @@ -772,8 +773,7 @@ Fixpoint fields_of_struct (id: ident) (ty: type) (fl: fieldlist) (pos: Z) : list match fl with | Fnil => nil | Fcons id1 ty1 fl' => - (align pos (alignof ty1), unroll_composite id ty ty1) - :: fields_of_struct id ty fl' (align pos (alignof ty1) + sizeof ty1) + (align pos (alignof ty1), ty1) :: fields_of_struct id ty fl' (align pos (alignof ty1) + sizeof ty1) end. Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := @@ -791,7 +791,7 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := exec_init_list m b ofs (fields_of_struct id (Tstruct id fl a) fl 0) il m' -> exec_init m b ofs (Tstruct id fl a) (Init_compound il) m' | exec_init_compound_union: forall m b ofs id id1 ty1 fl a i m', - exec_init m b ofs (unroll_composite id (Tunion id (Fcons id1 ty1 fl) a) ty1) i m' -> + exec_init m b ofs ty1 i m' -> exec_init m b ofs (Tunion id (Fcons id1 ty1 fl) a) (Init_compound (Init_cons i Init_nil)) m' with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem -> Prop := @@ -893,9 +893,7 @@ Proof. eapply store_init_data_list_app. eauto. rewrite (transl_init_size _ _ _ EQ). - rewrite <- Zplus_assoc. eapply H2. - rewrite sizeof_unroll_composite. eauto. - rewrite sizeof_unroll_composite. eauto. + rewrite <- Zplus_assoc. eapply H2. eauto. eauto. apply align_le. apply alignof_pos. Qed. diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 7653f0c..d61afa3 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -26,18 +26,6 @@ open Cop open PrintCsyntax open Clight -(* Collecting the names and fields of structs and unions *) - -module StructUnionSet = Set.Make(struct - type t = string * fieldlist - let compare (n1, _ : t) (n2, _ : t) = compare n1 n2 -end) - -let struct_unions = ref StructUnionSet.empty - -let register_struct_union id fld = - struct_unions := StructUnionSet.add (extern_atom id, fld) !struct_unions - (* Naming temporaries *) let temp_name (id: ident) = "$" ^ Z.to_string (Z.Zpos id) @@ -320,25 +308,12 @@ let collect_globdef (id, gd) = let collect_program p = List.iter collect_globdef p.prog_defs -let declare_struct_or_union p (name, fld) = - fprintf p "%s;@ @ " name - -let print_struct_or_union p (name, fld) = - fprintf p "@[%s {" name; - let rec print_fields = function - | Fnil -> () - | Fcons(id, ty, rem) -> - fprintf p "@ %s;" (name_cdecl (extern_atom id) ty); - print_fields rem in - print_fields fld; - fprintf p "@;<0 -2>};@]@ @ " - let print_program p prog = - struct_unions := StructUnionSet.empty; + struct_unions := StructUnion.empty; collect_program prog; fprintf p "@["; - StructUnionSet.iter (declare_struct_or_union p) !struct_unions; - StructUnionSet.iter (print_struct_or_union p) !struct_unions; + StructUnion.iter (declare_struct_or_union p) !struct_unions; + StructUnion.iter (print_struct_or_union p) !struct_unions; List.iter (print_globdef p) prog.prog_defs; fprintf p "@]@." diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 67efd1b..b1ee234 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -66,15 +66,9 @@ let name_floattype sz = (* Collecting the names and fields of structs and unions *) -module StructUnionSet = Set.Make(struct - type t = string * fieldlist - let compare (n1, _ : t) (n2, _ : t) = compare n1 n2 -end) +module StructUnion = Map.Make(String) -let struct_unions = ref StructUnionSet.empty - -let register_struct_union id fld = - struct_unions := StructUnionSet.add (extern_atom id, fld) !struct_unions +let struct_unions = ref StructUnion.empty (* Declarator (identifier + type) *) @@ -453,8 +447,12 @@ let rec collect_type = function | Tpointer(t, _) -> collect_type t | Tarray(t, _, _) -> collect_type t | Tfunction(args, res) -> collect_type_list args; collect_type res - | Tstruct(id, fld, _) -> register_struct_union id fld; collect_fields fld - | Tunion(id, fld, _) -> register_struct_union id fld; collect_fields fld + | Tstruct(id, fld, _) | Tunion(id, fld, _) -> + let s = extern_atom id in + if not (StructUnion.mem s !struct_unions) then begin + struct_unions := StructUnion.add s fld !struct_unions; + collect_fields fld + end | Tcomp_ptr _ -> () and collect_type_list = function @@ -533,10 +531,10 @@ let collect_globdef (id, gd) = let collect_program p = List.iter collect_globdef p.prog_defs -let declare_struct_or_union p (name, fld) = +let declare_struct_or_union p name fld = fprintf p "%s;@ @ " name -let print_struct_or_union p (name, fld) = +let print_struct_or_union p name fld = fprintf p "@[%s {" name; let rec print_fields = function | Fnil -> () @@ -547,11 +545,11 @@ let print_struct_or_union p (name, fld) = fprintf p "@;<0 -2>};@]@ @ " let print_program p prog = - struct_unions := StructUnionSet.empty; + struct_unions := StructUnion.empty; collect_program prog; fprintf p "@["; - StructUnionSet.iter (declare_struct_or_union p) !struct_unions; - StructUnionSet.iter (print_struct_or_union p) !struct_unions; + StructUnion.iter (declare_struct_or_union p) !struct_unions; + StructUnion.iter (print_struct_or_union p) !struct_unions; List.iter (print_globdef p) prog.prog_defs; fprintf p "@]@." -- cgit v1.2.3