Merge pull request #86 from AbsInt/clightgen-improved

Better treatment of names in the clightgen tool

4 files changed, 114 insertions, 90 deletions

diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 4fe8105d..a5a6ad66 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -91,14 +91,6 @@ Definition gensym (ty: type): mon ident :=
         (mkgenerator (Psucc (gen_next g)) ((gen_next g, ty) :: gen_trail g))
         (Ple_succ (gen_next g)).
 
-Definition reset_trail: mon unit :=
-  fun (g: generator) =>
-    Res tt (mkgenerator (gen_next g) nil) (Ple_refl (gen_next g)).
-
-Definition get_trail: mon (list (ident * type)) :=
-  fun (g: generator) =>
-    Res (gen_trail g) g (Ple_refl (gen_next g)).
-
 (** Construct a sequence from a list of statements.  To facilitate the
    proof, the sequence is nested to the left and starts with a [Sskip]. *)
 
@@ -113,7 +105,7 @@ Definition makeseq (l: list statement) : statement :=
 
 (** Smart constructor for [if ... then ... else]. *)
 
-Function eval_simpl_expr (a: expr) : option val :=
+Fixpoint eval_simpl_expr (a: expr) : option val :=
   match a with
   | Econst_int n _ => Some(Vint n)
   | Econst_float n _ => Some(Vfloat n)
@@ -502,49 +494,35 @@ with transl_lblstmt (ls: Csyntax.labeled_statements) : mon labeled_statements :=
 
 (** Translation of a function *)
 
-Definition transl_function (f: Csyntax.function) : mon function :=
-  do x <- reset_trail;
-  do tbody <- transl_stmt f.(Csyntax.fn_body);
-  do temps <- get_trail;
-  ret (mkfunction
+Definition transl_function (f: Csyntax.function) : res function :=
+  match transl_stmt f.(Csyntax.fn_body) (initial_generator tt) with
+  | Err msg =>
+      Error msg
+  | Res tbody g i =>
+      OK (mkfunction
               f.(Csyntax.fn_return)
               f.(Csyntax.fn_callconv)
               f.(Csyntax.fn_params)
               f.(Csyntax.fn_vars)
-              temps
-              tbody).
-
-Definition transl_fundef (fd: Csyntax.fundef) : mon fundef :=
-  match fd with
-  | Csyntax.Internal f =>
-      do tf <- transl_function f; ret (Internal tf)
-  | Csyntax.External ef targs tres cconv =>
-      ret (External ef targs tres cconv)
+              g.(gen_trail)
+              tbody)
   end.
 
 Local Open Scope error_monad_scope.
 
-Fixpoint transl_globdefs
-    (l: list (ident * globdef Csyntax.fundef type))
-    (g: generator) : res (list (ident * globdef Clight.fundef type)) :=
-  match l with
-  | nil => OK nil
-  | (id, Gfun f) :: l' =>
-      match transl_fundef f g with
-      | Err msg =>
-          Error (MSG "In function " :: CTX id :: MSG ": " :: msg)
-      | Res tf g' _ =>
-          do tl' <- transl_globdefs l' g'; OK ((id, Gfun tf) :: tl')
-      end
-  | (id, Gvar v) :: l' =>
-      do tl' <- transl_globdefs l' g; OK ((id, Gvar v) :: tl')
+Definition transl_fundef (fd: Csyntax.fundef) : res fundef :=
+  match fd with
+  | Csyntax.Internal f =>
+      do tf <- transl_function f; OK (Internal tf)
+  | Csyntax.External ef targs tres cc =>
+      OK (External ef targs tres cc)
   end.
 
 Definition transl_program (p: Csyntax.program) : res program :=
-  do gl' <- transl_globdefs (Csyntax.prog_defs p) (initial_generator tt);
-  OK {| prog_defs := gl';
-        prog_public := Csyntax.prog_public p;
-        prog_main := Csyntax.prog_main p;
+  do p1 <- AST.transform_partial_program transl_fundef p;
+  OK {| prog_defs := AST.prog_defs p1;
+        prog_public := AST.prog_public p1;
+        prog_main := AST.prog_main p1;
         prog_types := Csyntax.prog_types p;
         prog_comp_env := Csyntax.prog_comp_env p;
         prog_comp_env_eq := Csyntax.prog_comp_env_eq p |}.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 8f06e777..0c7c9ce7 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -2235,8 +2235,9 @@ Proof.
   econstructor; split.
   econstructor.
   exploit Genv.init_mem_match; eauto.
-  change (Genv.globalenv tprog) with (genv_genv tge). rewrite symbols_preserved.
-  rewrite <- H4; simpl; eauto.
+  change (Genv.globalenv tprog) with (genv_genv tge).
+  rewrite symbols_preserved. rewrite <- H4; simpl.
+  rewrite (transform_partial_program_main _ _ EQ). eauto. 
   eexact FIND.
   rewrite <- H3. apply type_of_fundef_preserved. auto.
   constructor. auto. constructor.
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 7003c78a..4077d7df 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -1088,7 +1088,8 @@ Opaque transl_expression transl_expr_stmt.
   monadInv TR; constructor; eauto.
 Qed.
 
-(** Relational presentation for the transformation of functions, fundefs, and variables. *)
+(** Relational presentation for the transformation of functions, fundefs, and va
+riables. *)
 
 Inductive tr_function: Csyntax.function -> Clight.function -> Prop :=
   | tr_function_intro: forall f tf,
@@ -1107,37 +1108,37 @@ Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop :=
       tr_fundef (Csyntax.External ef targs tres cconv) (External ef targs tres cconv).
 
 Lemma transl_function_spec:
-  forall f tf g g' i,
-  transl_function f g = Res tf g' i ->
+  forall f tf,
+  transl_function f = OK tf ->
   tr_function f tf.
 Proof.
-  unfold transl_function; intros. monadInv H.
+  unfold transl_function; intros.
+  destruct (transl_stmt (Csyntax.fn_body f) (initial_generator tt)) eqn:T; inv H.
   constructor; auto. simpl. eapply transl_stmt_meets_spec; eauto.
 Qed.
 
 Lemma transl_fundef_spec:
-  forall fd tfd g g' i,
-  transl_fundef fd g = Res tfd g' i ->
+  forall fd tfd,
+  transl_fundef fd = OK tfd ->
   tr_fundef fd tfd.
 Proof.
   unfold transl_fundef; intros.
-  destruct fd; monadInv H.
+  destruct fd; Errors.monadInv H.
 + constructor. eapply transl_function_spec; eauto.
 + constructor.
 Qed.
 
 Lemma transl_globdefs_spec:
-  forall l g l',
-  transl_globdefs l g = OK l' ->
+  forall l l',
+  transf_globdefs transl_fundef (fun v : type => OK v) l = OK l' ->
   list_forall2 (match_globdef tr_fundef (fun v1 v2 => v1 = v2)) l l'.
 Proof.
   induction l; simpl; intros.
 - inv H. constructor.
 - destruct a as [id gd]. destruct gd.
-  + destruct (transl_fundef f g) as [? | tf g' ?] eqn:E1; try discriminate.
-    destruct (transl_globdefs l g') eqn:E2; simpl in H; inv H.
+  + destruct (transl_fundef f) as [tf | ?] eqn:E1; Errors.monadInv H.
     constructor; eauto. constructor. eapply transl_fundef_spec; eauto.
-  + destruct (transl_globdefs l g) eqn:E2; simpl in H; inv H.
+  + Errors.monadInv H. 
     constructor; eauto. destruct v; constructor; auto.
 Qed.
 
@@ -1146,9 +1147,9 @@ Theorem transl_program_spec:
   transl_program p = OK tp ->
   match_program tr_fundef (fun v1 v2 => v1 = v2) nil (Csyntax.prog_main p) p tp.
 Proof.
-  unfold transl_program; intros.
-  destruct (transl_globdefs (Csyntax.prog_defs p) (initial_generator tt)) eqn:E; simpl in H; inv H.
-  split; auto. exists l; split. eapply transl_globdefs_spec; eauto.
+  unfold transl_program, transform_partial_program; intros. Errors.monadInv H. Errors.monadInv EQ; simpl.
+  split; auto. exists x0; split.
+  eapply transl_globdefs_spec; eauto.
   rewrite <- app_nil_end; auto.
 Qed.
 
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 :=@ ";