Problemes d'alignement des variables globales et a l'interieur de leurs initialiseurs

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@444 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 65 insertions, 51 deletions

diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml
index 0e168414..fd3ad496 100644
--- a/caml/Cil2Csyntax.ml
+++ b/caml/Cil2Csyntax.ml
@@ -796,50 +796,67 @@ let init_data_of_string s =
   done;
   !id
 
-let rec convertInit init k =
-  match init with
-  | SingleInit e ->
-      begin match extract_constant(Cil.constFold true e) with
-      | ICint(n, I8) ->
-          CList.Coq_cons(Init_int8 (coqint_of_camlint (Int64.to_int32 n)), k)
-      | ICint(n, I16) ->
-          CList.Coq_cons(Init_int16 (coqint_of_camlint (Int64.to_int32 n)), k)
-      | ICint(n, I32) ->
-          CList.Coq_cons(Init_int32 (coqint_of_camlint (Int64.to_int32 n)), k)
-      | ICfloat(n, F32) ->
-          CList.Coq_cons(Init_float32 n, k)
-      | ICfloat(n, F64) ->
-          CList.Coq_cons(Init_float64 n, k)
-      | ICstring s ->
-          CList.Coq_cons(Init_pointer(init_data_of_string s), k)
-      | ICnone ->
-          unsupported "this kind of expression is not supported in global initializers"
-    end
-  | CompoundInit(ty, data) ->
-      begin match Cil.unrollType ty with
-      | TComp _ ->
-          let init =
-            Cil.foldLeftCompoundAll
-              ~doinit: (fun ofs init ty k -> convertInit init k)
-              ~ct: ty
-              ~initl: data
-              ~acc: CList.Coq_nil in
-          let act_len = initDataLen 0l init in
-          let exp_len = camlint_of_z (Csyntax.sizeof (convertTyp ty)) in
-          assert (act_len <= exp_len);
-          let init' = 
-            if act_len < exp_len
-            then let spc = z_of_camlint (Int32.sub exp_len act_len) in
-                 CList.Coq_cons(Init_space spc, init)
-            else init in
-          CList.app init' k
-      | _ ->
-          Cil.foldLeftCompoundAll
-            ~doinit: (fun ofs init ty k -> convertInit init k)
-            ~ct: ty
-            ~initl: data
-            ~acc: k
+let convertInit init =
+  let k = ref Coq_nil
+  and pos = ref 0 in
+  let emit size datum =
+    k := Coq_cons(datum, !k);
+    pos := !pos + size in
+  let emit_space size =
+    emit size (Init_space (z_of_camlint (Int32.of_int size))) in
+  let check_align size =
+    assert (!pos land (size - 1) = 0) in
+  let align size =
+    let n = !pos land (size - 1) in
+    if n > 0 then emit_space (size - n) in
+
+  let rec cvtInit init =
+    match init with
+    | SingleInit e ->
+        begin match extract_constant(Cil.constFold true e) with
+        | ICint(n, I8) ->
+            let n' = coqint_of_camlint (Int64.to_int32 n) in
+            emit 1 (Init_int8 n')
+        | ICint(n, I16) ->
+            check_align 2;
+            let n' = coqint_of_camlint (Int64.to_int32 n) in
+            emit 2 (Init_int16 n')
+        | ICint(n, I32) ->
+            check_align 4;
+            let n' = coqint_of_camlint (Int64.to_int32 n) in
+            emit 4 (Init_int32 n')
+        | ICfloat(n, F32) ->
+            check_align 4;
+            emit 4 (Init_float32 n)
+        | ICfloat(n, F64) ->
+            check_align 8;
+            emit 8 (Init_float64 n)
+        | ICstring s ->
+            check_align 4;
+            emit 4 (Init_pointer(init_data_of_string s))
+        | ICnone ->
+            unsupported "this kind of expression is not supported in global initializers"
       end
+  | CompoundInit(ty, data) ->
+      let ty' = convertTyp ty in
+      let sz = Int32.to_int (camlint_of_z (Csyntax.sizeof ty')) in
+      let pos0 = !pos in
+      Cil.foldLeftCompoundAll
+          ~doinit: cvtCompoundInit
+          ~ct: ty
+          ~initl: data
+          ~acc: ();
+      let pos1 = !pos in
+      assert (pos1 <= pos0 + sz);
+      if pos1 < pos0 + sz then emit_space (pos0 + sz - pos1)
+
+  and cvtCompoundInit ofs init ty () =
+    let ty' = convertTyp ty in
+    let al = Int32.to_int (camlint_of_z (Csyntax.alignof ty')) in
+    align al;
+    cvtInit init
+
+  in cvtInit init; CList.rev !k
 
 (** Convert a [Cil.initinfo] into a list of [AST.init_data] *)
 
@@ -848,7 +865,7 @@ let convertInitInfo ty info =
   | None -> 
       CList.Coq_cons(Init_space(Csyntax.sizeof (convertTyp ty)), CList.Coq_nil)
   | Some init ->
-      CList.rev (convertInit init CList.Coq_nil)
+      convertInit init
 
 (** Convert a [Cil.GVar] into a global variable definition *)
 
diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml
index 59c42d3b..4eff1c68 100644
--- a/caml/PrintCsyntax.ml
+++ b/caml/PrintCsyntax.ml
@@ -352,7 +352,7 @@ let print_init p = function
   | Init_int32 n -> fprintf p "%ld,@ " (camlint_of_coqint n)
   | Init_float32 n -> fprintf p "%F,@ " n
   | Init_float64 n -> fprintf p "%F,@ " n
-  | Init_space n -> fprintf p "/* skip %ld*/@ " (camlint_of_coqint n)
+  | Init_space n -> fprintf p "/* skip %ld, */@ " (camlint_of_coqint n)
   | Init_pointer id ->
       match string_of_init id with
       | None -> fprintf p "/* pointer to other init*/,@ "
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml
index bf7b2cc7..97082b9b 100644
--- a/caml/PrintPPC.ml
+++ b/caml/PrintPPC.ml
@@ -54,14 +54,10 @@ let print_symb_ofs oc (symb, ofs) =
 let print_constant oc = function
   | Cint n ->
       fprintf oc "%ld" (camlint_of_coqint n)
-  | Csymbol_low_signed(s, n) ->
+  | Csymbol_low(s, n) ->
       fprintf oc "lo16(%a)" print_symb_ofs (s, camlint_of_coqint n)
-  | Csymbol_high_signed(s, n) ->
+  | Csymbol_high(s, n) ->
       fprintf oc "ha16(%a)" print_symb_ofs (s, camlint_of_coqint n)
-  | Csymbol_low_unsigned(s, n) ->
-      fprintf oc "lo16(%a)" print_symb_ofs (s, camlint_of_coqint n)
-  | Csymbol_high_unsigned(s, n) ->
-      fprintf oc "hi16(%a)" print_symb_ofs (s, camlint_of_coqint n)
 
 let num_crbit = function
   | CRbit_0 -> 0
@@ -499,6 +495,7 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
   | Coq_nil -> ()
   | _  ->
       fprintf oc "	.data\n";
+      fprintf oc "	.align	3\n";
       fprintf oc "	.globl	%a\n" print_symb name;
       fprintf oc "%a:\n" print_symb name;
       print_init_data oc init_data