More prudent handling of static names for string literals (#579)

- Make sure the names are fresh and not already used.
- Mark the names specially so that the special printing of initializers as strings applies only to those names.

Author: xavierleroy

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

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,15 @@ 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
+  (* Make sure the name is not already used in the source program *)
+  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 +624,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 +635,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 +659,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 +672,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 +1206,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 +1298,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

cfrontend/PrintCsyntax.ml

@@ -450,7 +450,9 @@ let string_of_init id =
   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
+      let n = camlint_of_coqint n in
+      assert (n >= 0l && n < 256l);
+      let c = Int32.to_int 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)
@@ -486,8 +488,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 +506,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;