Restart the name generator at first_unused_ident for every function.

This makes it easier to generate semi-meaningful names for compiler-generated temporaries in the clightgen tool.

3 files changed, 38 insertions, 58 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.