From 033aa0555a209fa3e825b1eeb8a5fc00ff8163e3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 1 Nov 2009 09:55:35 +0000 Subject: Support Clight initializers of the form "int * x = &y;". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1162 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 9 +++++++++ arm/PrintAsm.ml | 2 ++ cfrontend/Cil2Csyntax.ml | 23 ++++++++++++++++------- cfrontend/PrintCsyntax.ml | 5 +++++ common/AST.v | 1 + common/Mem.v | 4 ++++ powerpc/PrintAsm.ml | 3 +++ test/c/initializers.c | 9 +++++++++ 8 files changed, 49 insertions(+), 7 deletions(-) diff --git a/Changelog b/Changelog index aa5d69f4..f2ed641d 100644 --- a/Changelog +++ b/Changelog @@ -1,3 +1,12 @@ +- Support Clight initializers of the form "int * x = &y;". + +- Fixed spurious compile-time error on Clight initializers of the form + "const enum E x[2] = { E_1, E_2 };". + +- PowerPC code generator: force conversion to single precision before + doing a "store single float" instruction. + + Release 1.5, 2009-08-28 ======================= diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index da0b5d10..9297a694 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -466,6 +466,8 @@ let print_init oc = function | Init_space n -> let n = camlint_of_z n in if n > 0l then fprintf oc " .space %ld\n" n + | Init_addrof(symb, ofs) -> + fprintf oc " .word %a\n" print_symb_ofs (symb, ofs) | Init_pointer id -> let lbl = new_label() in fprintf oc " .word .L%d\n" lbl; diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml index 85380038..b8a88deb 100644 --- a/cfrontend/Cil2Csyntax.ml +++ b/cfrontend/Cil2Csyntax.ml @@ -1003,6 +1003,7 @@ let rec initDataLen accu = function | Init_float32 _ -> 4l | Init_float64 _ -> 8l | Init_space n -> camlint_of_z n + | Init_addrof(_, _) -> 4l | Init_pointer _ -> 4l in initDataLen (Int32.add sz accu) il @@ -1013,16 +1014,21 @@ type init_constant = | ICint of int64 * intsize | ICfloat of float * floatsize | ICstring of string + | ICaddrof of string | ICnone let extract_constant e = - try - match eval_expr e with - | CInt64(n, ikind, _) -> ICint(n, fst (convertIkind ikind)) - | CReal(n, fkind, _) -> ICfloat(n, convertFkind fkind) - | CStr s -> ICstring s - | _ -> ICnone - with NotConst -> ICnone + match e with + | AddrOf(Var v, NoOffset) -> ICaddrof v.vname + | StartOf(Var v, NoOffset) -> ICaddrof v.vname + | _ -> + try + match eval_expr e with + | CInt64(n, ikind, _) -> ICint(n, fst (convertIkind ikind)) + | CReal(n, fkind, _) -> ICfloat(n, convertFkind fkind) + | CStr s -> ICstring s + | _ -> ICnone + with NotConst -> ICnone let init_data_of_string s = let id = ref [] in @@ -1068,6 +1074,9 @@ let convertInit init = | ICfloat(n, F64) -> check_align 8; emit 8 (Init_float64 n) + | ICaddrof id -> + check_align 4; + emit 4 (Init_addrof(intern_string id, coqint_of_camlint 0l)) | ICstring s -> check_align 4; emit 4 (Init_pointer(init_data_of_string s)) diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 88e24eed..fa1d0482 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -378,6 +378,11 @@ let print_init p = function | 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_addrof(symb, ofs) -> + let ofs = camlint_of_coqint ofs in + if ofs = 0l + then fprintf p "&%s,@ " (extern_atom symb) + else fprintf p "(void *)((char *)&%s + %ld),@ " (extern_atom symb) ofs | Init_pointer id -> match string_of_init id with | None -> fprintf p "/* pointer to other init*/,@ " diff --git a/common/AST.v b/common/AST.v index e7b85a98..13e84dd8 100644 --- a/common/AST.v +++ b/common/AST.v @@ -91,6 +91,7 @@ Inductive init_data: Type := | Init_float32: float -> init_data | Init_float64: float -> init_data | Init_space: Z -> init_data + | Init_addrof: ident -> int -> init_data (**r address of symbol + offset *) | Init_pointer: list init_data -> init_data. (** Whole programs consist of: diff --git a/common/Mem.v b/common/Mem.v index 01c1975b..65108288 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -568,6 +568,9 @@ Fixpoint contents_init_data (pos: Z) (id: list init_data) {struct id}: contentma setN 7%nat pos (Vfloat f) (contents_init_data (pos + 1) id') | Init_space n :: id' => contents_init_data (pos + Zmax n 0) id' + | Init_addrof s n :: id' => + (* Not handled properly yet *) + contents_init_data (pos + 4) id' | Init_pointer x :: id' => (* Not handled properly yet *) contents_init_data (pos + 4) id' @@ -581,6 +584,7 @@ Definition size_init_data (id: init_data) : Z := | Init_float32 _ => 4 | Init_float64 _ => 8 | Init_space n => Zmax n 0 + | Init_addrof _ _ => 4 | Init_pointer _ => 4 end. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 335a6cf2..3c8d82bc 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -656,6 +656,9 @@ let print_init oc = function | Init_space n -> let n = camlint_of_z n in if n > 0l then fprintf oc " .space %ld\n" n + | Init_addrof(symb, ofs) -> + fprintf oc " .long %a\n" + symbol_offset (symb, camlint_of_coqint ofs) | Init_pointer id -> let lbl = new_label() in fprintf oc " .long %a\n" label lbl; diff --git a/test/c/initializers.c b/test/c/initializers.c index 2c52d51a..97ce99b0 100644 --- a/test/c/initializers.c +++ b/test/c/initializers.c @@ -31,6 +31,10 @@ typedef enum { AAA , BBB } MyEnum; const MyEnum x13[2] = { AAA, BBB }; +int * x14 = &x2; + +struct { char * y; int * z; float * u; double * v; } x15 = { x4, x5, &x11, &x12 }; + int main(int argc, char ** argv) { int i; @@ -54,6 +58,11 @@ int main(int argc, char ** argv) printf("x11 = %.10f\n", x11); printf("x12 = %.10f\n", x12); printf("x13 = { %d, %d }\n", x13[0], x13[1]); + if (x14 == &x2) printf("x14 ok\n"); else printf("x14 error\n"); + if (x15.y == x4 && x15.z == x5 && x15.u == &x11 && x15.v == &x12) + printf("x15 ok\n"); + else + printf("x15 error\n"); return 0; } -- cgit