Handling of builtins, continued.

PrintCsyntax, PrintAsm: improve printing of float literals.


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

7 files changed, 57 insertions, 51 deletions

diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml
index 2ad2ac5..57ee8fd 100644
--- a/cfrontend/C2Clight.ml
+++ b/cfrontend/C2Clight.ml
@@ -704,6 +704,7 @@ let convertProgram p =
   Hashtbl.clear decl_atom;
   Hashtbl.clear stringTable;
   Hashtbl.clear stub_function_table;
+  let p = Builtins.declarations() @ p in
   try
     let (funs1, vars1) =
       convertGlobdecls (translEnv Env.empty p) [] [] (cleanupGlobals p) in
@@ -743,3 +744,16 @@ let atom_is_readonly a =
     type_is_readonly env ty
   with Not_found ->
     false
+
+(** ** The builtin environment *)
+
+let builtins = {
+  Builtins.typedefs = [
+    (* keeps GCC-specific headers happy, harmless for others *)
+    "__builtin_va_list", C.TPtr(C.TVoid [], [])
+  ];
+  Builtins.functions = [
+  ]
+}
+
+
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 0388c2e..ebeda7c 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -344,32 +344,21 @@ let print_fundef p (Coq_pair(id, fd)) =
       print_function p id f
 
 let string_of_init id =
-  try
-    let s = String.create (List.length id) in
-    let i = ref 0 in
-    List.iter
-      (function
-        | Init_int8 n ->
-            s.[!i] <- Char.chr(Int32.to_int(camlint_of_coqint n));
-            incr i
-        | _ -> raise Not_found)
-      id;
-    Some s
-  with Not_found -> None
-
-let print_escaped_string p s =
-  fprintf p "\"";
-  for i = 0 to String.length s - 1 do
-    match s.[i] with
-    | ('\"' | '\\') as c -> fprintf p "\\%c" c
-    | '\n' -> fprintf p "\\n"
-    | '\t' -> fprintf p "\\t"
-    | '\r' -> fprintf p "\\r"
-    | c    -> if c >= ' ' && c <= '~'
-              then fprintf p "%c" c
-              else fprintf p "\\x%02x" (Char.code c)
-  done;
-  fprintf p "\""
+  let b = Buffer.create (List.length id) in
+  let add_init = function
+  | Init_int8 n ->
+      let c = Int32.to_int (camlint_of_coqint n) in
+      if c >= 32 && c <= 126 && c <> Char.code '\"' && c <> Char.code '\\'
+      then Buffer.add_char b (Char.chr c)
+      else Buffer.add_string b (Printf.sprintf "\\%03o" c)
+  | _ ->
+      assert false
+  in List.iter add_init id; Buffer.contents b
+
+let chop_last_nul id =
+  match List.rev id with
+  | Init_int8 BinInt.Z0 :: tl -> List.rev tl
+  | _ -> id
 
 let print_init p = function
   | Init_int8 n -> fprintf p "%ld,@ " (camlint_of_coqint n)
@@ -384,6 +373,8 @@ let print_init p = function
       then fprintf p "&%s,@ " (extern_atom symb)
       else fprintf p "(void *)((char *)&%s + %ld),@ " (extern_atom symb) ofs
 
+let re_string_literal = Str.regexp "__stringlit_[0-9]+"
+
 let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) =
   match init with
   | [] ->
@@ -393,10 +384,18 @@ let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) =
       fprintf p "%s;@ @ "
               (name_cdecl (extern_atom id) ty)
   | _ ->
-      fprintf p "@[<hov 2>%s = {@ "
+      fprintf p "@[<hov 2>%s = "
               (name_cdecl (extern_atom id) ty);
-      List.iter (print_init p) init;
-      fprintf p "};@]@ @ "
+      if Str.string_match re_string_literal (extern_atom id) 0
+      && List.for_all (function Init_int8 _ -> true | _ -> false) init
+      then
+        fprintf p "\"%s\"" (string_of_init (chop_last_nul init))
+      else begin
+        fprintf p "{@ ";
+        List.iter (print_init p) init;
+        fprintf p "}"
+      end;
+      fprintf p ";@]@ @ "
 
 (* Collect struct and union types *)
 
diff --git a/cparser/Builtins.ml b/cparser/Builtins.ml
index 020452f..8eb1abf 100644
--- a/cparser/Builtins.ml
+++ b/cparser/Builtins.ml
@@ -20,14 +20,17 @@ open Cutil
 
 let env = ref Env.empty
 let idents = ref []
+let decls = ref []
 
 let environment () = !env
 let identifiers () = !idents
+let declarations () = List.rev !decls
 
 let add_typedef (s, ty) =
   let (id, env') = Env.enter_typedef !env s ty in
   env := env';
-  idents := id :: !idents
+  idents := id :: !idents;
+  decls := {gdesc = Gtypedef(id, ty); gloc = no_loc} :: !decls
 
 let add_function (s, (res, args, va)) =
   let ty =
@@ -36,7 +39,8 @@ let add_function (s, (res, args, va)) =
          va, []) in
   let (id, env') = Env.enter_ident !env s Storage_extern ty in
   env := env';
-  idents := id :: !idents
+  idents := id :: !idents;
+  decls := {gdesc = Gdecl(Storage_extern, id, ty, None); gloc = no_loc} :: !decls
 
 type t = {
   typedefs: (string * C.typ) list;
diff --git a/cparser/Builtins.mli b/cparser/Builtins.mli
index be0d941..7f9d78a 100644
--- a/cparser/Builtins.mli
+++ b/cparser/Builtins.mli
@@ -15,6 +15,7 @@
 
 val environment: unit -> Env.t
 val identifiers: unit -> C.ident list
+val declarations: unit -> C.globdecl list
 
 type t = {
   typedefs: (string * C.typ) list;
diff --git a/cparser/Makefile b/cparser/Makefile
index df1d604..837bda8 100644
--- a/cparser/Makefile
+++ b/cparser/Makefile
@@ -11,9 +11,9 @@ INTFS=C.mli
 
 SRCS=Errors.ml Cabs.ml Cabshelper.ml Parse_aux.ml Parser.ml Lexer.ml \
   Machine.ml \
-  Env.ml Cprint.ml Cutil.ml Ceval.ml Cleanup.ml \
+  Env.ml Cprint.ml Cutil.ml Ceval.ml \
   Builtins.ml GCC.ml \
-  Elab.ml Rename.ml \
+  Cleanup.ml Elab.ml Rename.ml \
   Transform.ml \
   Unblock.ml SimplExpr.ml AddCasts.ml StructByValue.ml StructAssign.ml \
   Bitfields.ml \
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 2d8b026..2cc409f 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -63,7 +63,7 @@ let preprocess ifile ofile =
 let compile_c_file sourcename ifile ofile =
   (* Simplification options *)
   let simplifs =
-    "bec"           (* blocks, impure exprs, implicit casts: mandatory *)
+    "bec" (* blocks, impure exprs, implicit casts: mandatory *)
   ^ (if !option_fstruct_passing then "s" else "")
   ^ (if !option_fstruct_assign then "S" else "")
   ^ (if !option_fbitfields then "f" else "") in
@@ -325,6 +325,7 @@ let cmdline_actions =
 
 let _ =
   Cparser.Machine.config := Cparser.Machine.ilp32ll64;
+  Cparser.Builtins.set C2Clight.builtins;
   CPragmas.initialize();
   parse_cmdline cmdline_actions usage_string;
   if !linker_options <> [] 
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index a1e5afe..d69d0af 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -684,25 +684,12 @@ let print_init oc = function
       fprintf oc "	.long	%a\n" 
                  symbol_offset (symb, camlint_of_coqint ofs)
 
-let print_init_char oc = function
-  | Init_int8 n ->
-      let c = Int32.to_int (camlint_of_coqint n) in
-      if c >= 32 && c <= 126 && c <> Char.code '\"' && c <> Char.code '\\'
-      then output_char oc (Char.chr c)
-      else fprintf oc "\\%03o" c
-  | _ ->
-      assert false
-
-let re_string_literal = Str.regexp "__stringlit_[0-9]+"
-
 let print_init_data oc name id =
-  if Str.string_match re_string_literal (extern_atom name) 0
+  if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
   && List.for_all (function Init_int8 _ -> true | _ -> false) id
-  then begin
-    fprintf oc "	.ascii	\"";
-    List.iter (print_init_char oc) id;
-    fprintf oc "\"\n"
-  end else
+  then
+    fprintf oc "	.ascii	\"%s\"\n" (PrintCsyntax.string_of_init id)
+  else
     List.iter (print_init oc) id
 
 let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =