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

5 files changed, 76 insertions, 66 deletions

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 "@[<v 2>%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 "@[<v 0>";
-  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 "@[<v 2>%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 "@[<v 0>";
-  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 "@]@."