Naming of compiler-generated temporaries

clightgen now gives semi-readable and relatively stable names of the form _t'1, _t'2, _t'3, etc, to compiler-generated temporaries, instead of the unreadable and unstable NNN%positive notation generated previously.

1 files changed, 76 insertions, 32 deletions

diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 96c7398f..5d4ab88b 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -60,10 +60,7 @@ let sanitize s =
   done;
   s'
 
-module StringSet = Set.Make(String)
-
 let temp_names : (ident, string) Hashtbl.t = Hashtbl.create 17
-let all_temp_names : StringSet.t ref = ref StringSet.empty
 
 let ident p id =
   try
@@ -76,41 +73,35 @@ let ident p id =
   with Not_found ->
     fprintf p "%ld%%positive" (P.to_int32 id)
 
+let iter_hashtbl_sorted (h: ('a, string) Hashtbl.t) (f: 'a * string -> unit) =
+  List.iter f
+    (List.fast_sort (fun (k1, d1) (k2, d2) -> String.compare d1 d2)
+      (Hashtbl.fold (fun k d accu -> (k, d) :: accu) h []))
+
 let define_idents p =
-  Hashtbl.iter
-    (fun id name ->
+  iter_hashtbl_sorted 
+    string_of_atom
+    (fun (id, name) ->
       try
         fprintf p "Definition _%s : ident := %ld%%positive.@ "
                   (sanitize name) (P.to_int32 id)
       with Not_an_identifier ->
-        ())
-    string_of_atom;
-  Hashtbl.iter
-    (fun id name ->
+        ());
+  iter_hashtbl_sorted
+    temp_names
+    (fun (id, name) ->
       fprintf p "Definition %s : ident := %ld%%positive.@ "
-                name (P.to_int32 id))
-    temp_names;
+                name (P.to_int32 id));
   fprintf p "@ "
 
-let rec find_temp_name name counter =
-  let name' =
-    if counter = 0 then name ^ "'" else sprintf "%s'%d" name counter in
-  if StringSet.mem name' !all_temp_names
-  then find_temp_name name (counter + 1)
-  else name'
-
-let name_temporary t v =
-  (* Try to give "t" a name that is the name of "v" with a prime
-     plus a number to disambiguate if needed. *)
-  if not (Hashtbl.mem string_of_atom t || Hashtbl.mem temp_names t) then begin
-    try
-      let vname = "_" ^ sanitize (Hashtbl.find string_of_atom v) in
-      let tname = find_temp_name vname 0 in
-      Hashtbl.add temp_names t tname;
-      all_temp_names := StringSet.add tname !all_temp_names
-    with Not_found | Not_an_identifier ->
-      ()
-  end
+let name_temporary t =
+  let t1 = P.to_int t and t0 = P.to_int (first_unused_ident ()) in
+  if t1 >= t0 && not (Hashtbl.mem temp_names t)
+  then Hashtbl.add temp_names t (sprintf "_t'%d" (t1 - t0 + 1))
+
+let name_opt_temporary = function
+  | None -> ()
+  | Some id -> name_temporary id
 
 (* Numbers *)
 
@@ -489,13 +480,66 @@ Local Open Scope Z_scope.
 
 "
 
+(* Naming the compiler-generated temporaries occurring in the program *)
+
+let rec name_expr = function
+  | Evar(id, t) -> ()
+  | Etempvar(id, t) -> name_temporary id
+  | Ederef(a1, t) -> name_expr a1
+  | Efield(a1, f, t) -> name_expr a1
+  | Econst_int(n, t) -> ()
+  | Econst_float(n, t) -> ()
+  | Econst_long(n, t) -> ()
+  | Econst_single(n, t) -> ()
+  | Eunop(op, a1, t) -> name_expr a1
+  | Eaddrof(a1, t) -> name_expr a1
+  | Ebinop(op, a1, a2, t) -> name_expr a1; name_expr a2
+  | Ecast(a1, t) -> name_expr a1
+  | Esizeof(t1, t) -> ()
+  | Ealignof(t1, t) -> ()
+
+let rec name_stmt = function
+  | Sskip -> ()
+  | Sassign(e1, e2) -> name_expr e1; name_expr e2
+  | Sset(id, e2) -> name_temporary id; name_expr e2
+  | Scall(optid, e1, el) ->
+      name_opt_temporary optid; name_expr e1; List.iter name_expr el
+  | Sbuiltin(optid, ef, tyl, el) ->
+      name_opt_temporary optid; List.iter name_expr el
+  | Ssequence(s1, s2) -> name_stmt s1; name_stmt s2
+  | Sifthenelse(e, s1, s2) -> name_expr e; name_stmt s1; name_stmt s2
+  | Sloop(s1, s2) -> name_stmt s1; name_stmt s2
+  | Sbreak -> ()
+  | Scontinue -> ()
+  | Sswitch(e, cases) -> name_expr e; name_lblstmts cases
+  | Sreturn (Some e) -> name_expr e
+  | Sreturn None -> ()
+  | Slabel(lbl, s1) -> name_stmt s1
+  | Sgoto lbl -> ()
+
+and name_lblstmts = function
+  | LSnil -> ()
+  | LScons(lbl, s, ls) -> name_stmt s; name_lblstmts ls
+
+let name_function f =
+  List.iter (fun (id, ty) -> name_temporary id) f.fn_temps;
+  name_stmt f.fn_body
+
+let name_globdef (id, g) =
+  match g with
+  | Gfun(Internal f) -> name_function f
+  | _ -> ()
+
+let name_program p =
+  List.iter name_globdef p.prog_defs
+  
 (* All together *)
 
 let print_program p prog =
+  Hashtbl.clear temp_names;
+  name_program prog;
   fprintf p "@[<v 0>";
   fprintf p "%s" prologue;
-  Hashtbl.clear temp_names;
-  all_temp_names := StringSet.empty;
   define_idents p;
   List.iter (print_globdef p) prog.prog_defs;
   fprintf p "Definition composites : list composite_definition :=@ ";