diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 18bedd4f5..7f6256035 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -127,13 +127,11 @@ module Printer(Target:TARGET) = symbol_offset (symb, ofs) - let print_init_data oc name id = - if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0 - && List.for_all (function Init_int8 _ -> true | _ -> false) id - then - fprintf oc " .ascii \"%s\"\n" (PrintCsyntax.string_of_init id) + let print_init_data oc name il = + if C2C.atom_literal name = C2C.String_literal then + fprintf oc " .ascii \"%s\"\n" (PrintCsyntax.string_of_init il) else - List.iter (print_init oc) id + List.iter (print_init oc) il let print_var oc name v = match v.gvar_init with diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 3586c714d..70f7273fb 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -32,6 +32,11 @@ type inline_status = | Noinline (* The atom is declared with the noinline attribute *) | Inline (* The atom is declared inline *) +type literal_status = + | No_literal + | String_literal + | Wide_string_literal + type atom_info = { a_storage: C.storage; (* storage class *) a_defined: bool; (* defined in the current comp. unit? *) @@ -41,6 +46,7 @@ type atom_info = (* 1 section for data, 3 sections (code/lit/jumptbl) for functions *) a_access: Sections.access_mode; (* access mode, e.g. small data area *) a_inline: inline_status; (* function declared inline? *) + a_literal: literal_status; (* is this a string literal? *) a_loc: location (* source location *) } @@ -138,6 +144,12 @@ let atom_location a = with Not_found -> Cutil.no_loc +let atom_literal a = + try + (Hashtbl.find decl_atom a).a_literal + with Not_found -> + No_literal + (** The current environment of composite definitions *) let comp_env : composite_env ref = ref Maps.PTree.empty @@ -594,6 +606,14 @@ let is_int64 env ty = (** String literals *) let stringNum = ref 0 (* number of next global for string literals *) + +let rec gensym_string_literal () = + incr stringNum; + let name = Printf.sprintf "__stringlit_%d" !stringNum in + if Hashtbl.mem atom_of_string name + then gensym_string_literal () + else name + let stringTable : (string, AST.ident) Hashtbl.t = Hashtbl.create 47 let wstringTable : (int64 list * ikind, AST.ident) Hashtbl.t = Hashtbl.create 47 @@ -603,8 +623,7 @@ let name_for_string_literal s = try Hashtbl.find stringTable s with Not_found -> - incr stringNum; - let name = Printf.sprintf "__stringlit_%d" !stringNum in + let name = gensym_string_literal () in let id = intern_string name in let mergeable = if is_C_string s then 1 else 0 in Hashtbl.add decl_atom id @@ -615,6 +634,7 @@ let name_for_string_literal s = a_sections = [Sections.for_stringlit mergeable]; a_access = Sections.Access_default; a_inline = No_specifier; + a_literal = String_literal; a_loc = Cutil.no_loc }; Hashtbl.add stringTable s id; id @@ -638,8 +658,7 @@ let name_for_wide_string_literal s ik = try Hashtbl.find wstringTable (s, ik) with Not_found -> - incr stringNum; - let name = Printf.sprintf "__stringlit_%d" !stringNum in + let name = gensym_string_literal () in let id = intern_string name in let wchar_size = Cutil.sizeof_ikind ik in let mergeable = if is_C_wide_string s then wchar_size else 0 in @@ -652,6 +671,7 @@ let name_for_wide_string_literal s ik = a_sections = [Sections.for_stringlit mergeable]; a_access = Sections.Access_default; a_inline = No_specifier; + a_literal = Wide_string_literal; a_loc = Cutil.no_loc }; Hashtbl.add wstringTable (s, ik) id; id @@ -1185,6 +1205,7 @@ let convertFundef loc env fd = a_sections = Sections.for_function env loc id' fd.fd_attrib; a_access = Sections.Access_default; a_inline = inline; + a_literal = No_literal; a_loc = loc }; (id', AST.Gfun(Ctypes.Internal {fn_return = ret; @@ -1276,6 +1297,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) = a_sections = [section]; a_access = access; a_inline = No_specifier; + a_literal = No_literal; a_loc = loc }; let volatile = List.mem C.AVolatile attr in let readonly = List.mem C.AConst attr && not volatile in diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 14d833c95..ec7bb6f12 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -451,6 +451,7 @@ let string_of_init id = let add_init = function | Init_int8 n -> let c = Int32.to_int (camlint_of_coqint n) in + assert (c >= 0 && c < 256); 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) @@ -486,8 +487,6 @@ let print_composite_init p il = il; fprintf p "}" -let re_string_literal = Str.regexp "__stringlit_[0-9]+" - let print_globvar p id v = let name1 = extern_atom id in let name2 = if v.gvar_readonly then "const " ^ name1 else name1 in @@ -506,8 +505,7 @@ let print_globvar p id v = [i1] -> print_init p i1 | _, il -> - if Str.string_match re_string_literal (extern_atom id) 0 - && List.for_all (function Init_int8 _ -> true | _ -> false) il + if C2C.atom_literal id = C2C.String_literal then fprintf p "\"%s\"" (string_of_init (chop_last_nul il)) else print_composite_init p il end; diff --git a/test b/test index ddb2ea33a..081175df3 160000 --- a/test +++ b/test @@ -1 +1 @@ -Subproject commit ddb2ea33a776bb576edb79a4476b06280087fb84 +Subproject commit 081175df374260304a5cd78dd3dfaded93dceb41