From b5692de75c9c23105bac4a0b2510d868bb7c2631 Mon Sep 17 00:00:00 2001 From: Xavier Leroy 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/SimplExpr.v | 60 +++++++++++++++------------------------------- cfrontend/SimplExprproof.v | 5 ++-- cfrontend/SimplExprspec.v | 31 ++++++++++++------------ 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. -- cgit