From c24a652789e15b33153c1d90c6869eb6e6e28040 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 7 Mar 2010 17:49:18 +0000 Subject: 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 --- cfrontend/C2Clight.ml | 14 ++++++++++++ cfrontend/PrintCsyntax.ml | 57 +++++++++++++++++++++++------------------------ cparser/Builtins.ml | 8 +++++-- cparser/Builtins.mli | 1 + cparser/Makefile | 4 ++-- driver/Driver.ml | 3 ++- powerpc/PrintAsm.ml | 21 ++++------------- 7 files changed, 57 insertions(+), 51 deletions(-) diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml index 2ad2ac5e..57ee8fd5 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 0388c2eb..ebeda7cc 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 "@[%s = {@ " + fprintf p "@[%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 020452f9..8eb1abfd 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 be0d941f..7f9d78a9 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 df1d6047..837bda87 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 2d8b0266..2cc409f5 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 a1e5afe3..d69d0aff 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), _)) = -- cgit