From b5692de75c9c23105bac4a0b2510d868bb7c2631 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 5 Feb 2016 11:38:04 +0100
Subject: 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.
---
 cfrontend/SimplExprspec.v | 31 ++++++++++++++++---------------
 1 file changed, 16 insertions(+), 15 deletions(-)

(limited to 'cfrontend/SimplExprspec.v')

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.
 
-- 
cgit