-dclight output: use nicer names for temporary variables

The temporary variables introduced by SimplLocals reuse the same
integer identifiers as the local variables they come from.  This commit
ensures that these variables are printed as "$var", where "var"
is the original variable name, instead of "$NNN" as before.

The "$NNN" form is retained for temporary variables that do not
correspond to a source-level local variable, such as the temporary
variables introduced by SimplExpr.

This commit should make no difference for "ccomp -dclight", because
the Clight that is printed is the Clight version 1 produced by
SimplExpr, where every temporary is fresh and does not correspond
to a source-level local variable.

This commit does change the output of "clightgen -dclight", because
the Clight that is printed is the Clight version 2 produced by
SimplLocals.  The printed Clight is much more legible thanks to
the more meaningful temporary variable names.

1 files changed, 11 insertions, 2 deletions

diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index e63067a9..0e735d2d 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -23,9 +23,18 @@ open Cop
 open PrintCsyntax
 open Clight
 
-(* Naming temporaries *)
+(* Naming temporaries.
+   Some temporaries are obtained by lifting variables in SimplLocals.
+   For these we use a meaningful name "$var", as found in the table of
+   atoms.  Other temporaries are generated during SimplExpr, and are
+   not in the table of atoms.  We print them as "$NNN" (a unique
+   integer). *)
 
-let temp_name (id: AST.ident) = "$" ^ Z.to_string (Z.Zpos id)
+let temp_name (id: AST.ident) =
+  try
+    "$" ^ Hashtbl.find string_of_atom id
+  with Not_found ->
+    Printf.sprintf "$%d" (P.to_int id)
 
 (* Declarator (identifier + type) -- reuse from PrintCsyntax *)