diff options
| -rw-r--r-- | arm/Asmexpand.ml | 4 | ||||
| -rw-r--r-- | common/AST.v | 217 | ||||
| -rw-r--r-- | extraction/extraction.v | 1 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 23 |
4 files changed, 220 insertions, 25 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index d13015ff..da08bf7c 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -403,7 +403,7 @@ let expand_function fn = with Error s -> Errors.Error (Errors.msg (coqstring_of_camlstring s)) -let expand_fundef = function +let expand_fundef _ = function | Internal f -> begin match expand_function f with | Errors.OK tf -> Errors.OK (Internal tf) @@ -413,4 +413,4 @@ let expand_fundef = function Errors.OK (External ef) let expand_program (p: Asm.program) : Asm.program Errors.res = - AST.transform_partial_program expand_fundef p + AST.transform_partial_ident_program expand_fundef p diff --git a/common/AST.v b/common/AST.v index 4d929f13..4e02b3d4 100644 --- a/common/AST.v +++ b/common/AST.v @@ -264,10 +264,46 @@ Qed. End TRANSF_PROGRAM. +(** General iterator over program that applies a given code transfomration + function to all function descriptions with their identifers and leaves + teh other parts of the program unchanged. *) + +Section TRANSF_PROGRAM_IDENT. + +Variable A B V: Type. +Variable transf: ident -> A -> B. + +Definition transform_program_globdef_ident (idg: ident * globdef A V) : ident * globdef B V := + match idg with + | (id, Gfun f) => (id, Gfun (transf id f)) + | (id, Gvar v) => (id, Gvar v) + end. + +Definition transform_program_ident (p: program A V): program B V := + mkprogram + (List.map transform_program_globdef_ident p.(prog_defs)) + p.(prog_public) + p.(prog_main). + +Lemma tranforma_program_function_ident: + forall p i tf, + In (i, Gfun tf) (transform_program_ident p).(prog_defs) -> + exists f, In (i, Gfun f) p.(prog_defs) /\ transf i f = tf. +Proof. + simpl. unfold transform_program_ident. intros. + exploit list_in_map_inv; eauto. + intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. + exists f; auto. +Qed. + +End TRANSF_PROGRAM_IDENT. + (** The following is a more general presentation of [transform_program] where global variable information can be transformed, in addition to function definitions. Moreover, the transformation functions can fail and - return an error message. *) + return an error message. Also the transformation functions are defined + for the case the identifier of the function is passed as additional + argument *) Open Local Scope error_monad_scope. Open Local Scope string_scope. @@ -276,12 +312,18 @@ Section TRANSF_PROGRAM_GEN. Variables A B V W: Type. Variable transf_fun: A -> res B. +Variable transf_fun_ident: ident -> A -> res B. Variable transf_var: V -> res W. +Variable transf_var_ident: ident -> V -> res W. Definition transf_globvar (g: globvar V) : res (globvar W) := do info' <- transf_var g.(gvar_info); OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)). +Definition transf_globvar_ident (i: ident) (g: globvar V) : res (globvar W) := + do info' <- transf_var_ident i g.(gvar_info); + OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)). + Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) := match l with | nil => OK nil @@ -299,10 +341,31 @@ Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * gl end end. +Fixpoint transf_globdefs_ident (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) := + match l with + | nil => OK nil + | (id, Gfun f) :: l' => + match transf_fun_ident id f with + | Error msg => Error (MSG "In function " :: CTX id :: MSG ": " :: msg) + | OK tf => + do tl' <- transf_globdefs_ident l'; OK ((id, Gfun tf) :: tl') + end + | (id, Gvar v) :: l' => + match transf_globvar_ident id v with + | Error msg => Error (MSG "In variable " :: CTX id :: MSG ": " :: msg) + | OK tv => + do tl' <- transf_globdefs_ident l'; OK ((id, Gvar tv) :: tl') + end + end. + Definition transform_partial_program2 (p: program A V) : res (program B W) := do gl' <- transf_globdefs p.(prog_defs); OK (mkprogram gl' p.(prog_public) p.(prog_main)). +Definition transform_partial_ident_program2 (p: program A V) : res (program B W) := + do gl' <- transf_globdefs_ident p.(prog_defs); + OK (mkprogram gl' p.(prog_public) p.(prog_main)). + Lemma transform_partial_program2_function: forall p tp i tf, transform_partial_program2 p = OK tp -> @@ -321,6 +384,24 @@ Proof. exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. Qed. +Lemma transform_partial_ident_program2_function: + forall p tp i tf, + transform_partial_ident_program2 p = OK tp -> + In (i, Gfun tf) tp.(prog_defs) -> + exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun_ident i f = OK tf. +Proof. + intros. monadInv H. simpl in H0. + revert x EQ H0. induction (prog_defs p); simpl; intros. + inv EQ. contradiction. + destruct a as [id [f|v]]. + destruct (transf_fun_ident id f) as [tf1|msg] eqn:?; monadInv EQ. + simpl in H0; destruct H0. inv H. exists f; auto. + exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. + destruct (transf_globvar_ident id v) as [tv1|msg] eqn:?; monadInv EQ. + simpl in H0; destruct H0. inv H. + exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. +Qed. + Lemma transform_partial_program2_variable: forall p tp i tv, transform_partial_program2 p = OK tp -> @@ -342,6 +423,28 @@ Proof. exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. Qed. + +Lemma transform_partial_ident_program2_variable: + forall p tp i tv, + transform_partial_ident_program2 p = OK tp -> + In (i, Gvar tv) tp.(prog_defs) -> + exists v, + In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs) + /\ transf_var_ident i v = OK tv.(gvar_info). +Proof. + intros. monadInv H. simpl in H0. + revert x EQ H0. induction (prog_defs p); simpl; intros. + inv EQ. contradiction. + destruct a as [id [f|v]]. + destruct (transf_fun_ident id f) as [tf1|msg] eqn:?; monadInv EQ. + simpl in H0; destruct H0. inv H. + exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. + destruct (transf_globvar_ident id v) as [tv1|msg] eqn:?; monadInv EQ. + simpl in H0; destruct H0. inv H. + monadInv Heqr. simpl. exists (gvar_info v). split. left. destruct v; auto. auto. + exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. +Qed. + Lemma transform_partial_program2_succeeds: forall p tp i g, transform_partial_program2 p = OK tp -> @@ -361,6 +464,25 @@ Proof. destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto. Qed. +Lemma transform_partial_ident_program2_succeeds: + forall p tp i g, + transform_partial_ident_program2 p = OK tp -> + In (i, g) p.(prog_defs) -> + match g with + | Gfun fd => exists tfd, transf_fun_ident i fd = OK tfd + | Gvar gv => exists tv, transf_var_ident i gv.(gvar_info) = OK tv + end. +Proof. + intros. monadInv H. + revert x EQ H0. induction (prog_defs p); simpl; intros. + contradiction. + destruct a as [id1 g1]. destruct g1. + destruct (transf_fun_ident id1 f) eqn:TF; try discriminate. monadInv EQ. + destruct H0. inv H. econstructor; eauto. eapply IHl; eauto. + destruct (transf_globvar_ident id1 v) eqn:TV; try discriminate. monadInv EQ. + destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto. +Qed. + Lemma transform_partial_program2_main: forall p tp, transform_partial_program2 p = OK tp -> @@ -369,6 +491,14 @@ Proof. intros. monadInv H. reflexivity. Qed. +Lemma transform_partial_ident_program2_main: + forall p tp, + transform_partial_ident_program2 p = OK tp -> + tp.(prog_main) = p.(prog_main). +Proof. + intros. monadInv H. reflexivity. +Qed. + Lemma transform_partial_program2_public: forall p tp, transform_partial_program2 p = OK tp -> @@ -377,6 +507,14 @@ Proof. intros. monadInv H. reflexivity. Qed. +Lemma transform_partial_ident_program2_public: + forall p tp, + transform_partial_ident_program2 p = OK tp -> + tp.(prog_public) = p.(prog_public). +Proof. + intros. monadInv H. reflexivity. +Qed. + (** Additionally, we can also "augment" the program with new global definitions and a different "main" function. *) @@ -397,6 +535,18 @@ Proof. intros. monadInv H. reflexivity. Qed. +Definition transform_partial_augment_ident_program (p: program A V) : res (program B W) := + do gl' <- transf_globdefs_ident p.(prog_defs); + OK(mkprogram (gl' ++ new_globs) p.(prog_public) new_main). + +Lemma transform_partial_augment_ident_program_main: + forall p tp, + transform_partial_augment_ident_program p = OK tp -> + tp.(prog_main) = new_main. +Proof. + intros. monadInv H. reflexivity. +Qed. + End AUGMENT. Remark transform_partial_program2_augment: @@ -409,6 +559,16 @@ Proof. simpl. f_equal. f_equal. rewrite <- app_nil_end. auto. Qed. +Remark transform_partial_ident_program2_augment: + forall p, + transform_partial_ident_program2 p = + transform_partial_augment_ident_program nil p.(prog_main) p. +Proof. + unfold transform_partial_ident_program2, transform_partial_augment_ident_program; intros. + destruct (transf_globdefs_ident (prog_defs p)); auto. + simpl. f_equal. f_equal. rewrite <- app_nil_end. auto. +Qed. + End TRANSF_PROGRAM_GEN. (** The following is a special case of [transform_partial_program2], @@ -418,10 +578,14 @@ Section TRANSF_PARTIAL_PROGRAM. Variable A B V: Type. Variable transf_partial: A -> res B. +Variable transf_partial_ident: ident -> A -> res B. Definition transform_partial_program (p: program A V) : res (program B V) := transform_partial_program2 transf_partial (fun v => OK v) p. +Definition transform_partial_ident_program (p: program A V) : res (program B V) := + transform_partial_ident_program2 transf_partial_ident (fun _ v => OK v) p. + Lemma transform_partial_program_main: forall p tp, transform_partial_program p = OK tp -> @@ -430,6 +594,14 @@ Proof. apply transform_partial_program2_main. Qed. +Lemma transform_partial_ident_program_main: + forall p tp, + transform_partial_ident_program p = OK tp -> + tp.(prog_main) = p.(prog_main). +Proof. + apply transform_partial_ident_program2_main. +Qed. + Lemma transform_partial_program_public: forall p tp, transform_partial_program p = OK tp -> @@ -438,6 +610,14 @@ Proof. apply transform_partial_program2_public. Qed. +Lemma transform_partial_ident_program_public: + forall p tp, + transform_partial_ident_program p = OK tp -> + tp.(prog_public) = p.(prog_public). +Proof. + apply transform_partial_ident_program2_public. +Qed. + Lemma transform_partial_program_function: forall p tp i tf, transform_partial_program p = OK tp -> @@ -447,6 +627,15 @@ Proof. apply transform_partial_program2_function. Qed. +Lemma transform_partial_ident_program_function: + forall p tp i tf, + transform_partial_ident_program p = OK tp -> + In (i, Gfun tf) tp.(prog_defs) -> + exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial_ident i f = OK tf. +Proof. + apply transform_partial_ident_program2_function. +Qed. + Lemma transform_partial_program_succeeds: forall p tp i fd, transform_partial_program p = OK tp -> @@ -457,6 +646,16 @@ Proof. exploit transform_partial_program2_succeeds; eauto. Qed. +Lemma transform_partial_ident_program_succeeds: + forall p tp i fd, + transform_partial_ident_program p = OK tp -> + In (i, Gfun fd) p.(prog_defs) -> + exists tfd, transf_partial_ident i fd = OK tfd. +Proof. + unfold transform_partial_ident_program; intros. + exploit transform_partial_ident_program2_succeeds; eauto. +Qed. + End TRANSF_PARTIAL_PROGRAM. Lemma transform_program_partial_program: @@ -475,6 +674,22 @@ Proof. destruct v; auto. Qed. +Lemma transform_program_partial_ident_program: + forall (A B V: Type) (transf: ident -> A -> B) (p: program A V), + transform_partial_ident_program (fun id f => OK(transf id f)) p = OK(transform_program_ident transf p). +Proof. + intros. + unfold transform_partial_ident_program, transform_partial_ident_program2, transform_program; intros. + replace (transf_globdefs_ident (fun id f => OK (transf id f)) (fun _ v => OK v) p.(prog_defs)) + with (OK (map (transform_program_globdef_ident transf) p.(prog_defs))). + auto. + induction (prog_defs p); simpl. + auto. + destruct a as [id [f|v]]; rewrite <- IHl. + auto. + destruct v; auto. +Qed. + (** The following is a relational presentation of [transform_partial_augment_preogram]. Given relations between function definitions and between variable information, it defines a relation diff --git a/extraction/extraction.v b/extraction/extraction.v index 6327f871..dc7522b8 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -168,4 +168,5 @@ Separate Extraction Machregs.mregs_for_operation Machregs.mregs_for_builtin Machregs.two_address_op Machregs.is_stack_reg AST.signature_main + AST.transform_partial_ident_program Parser.translation_unit_file. diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 878c7e5d..bf7e4c3e 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -713,26 +713,5 @@ let expand_fundef id = function | External ef -> Errors.OK (External ef) -let rec transform_partial_prog transfun p = - match p with - | [] -> Errors.OK [] - | (id,Gvar v)::l -> - (match transform_partial_prog transfun l with - | Errors.OK x -> Errors.OK ((id,Gvar v)::x) - | Errors.Error msg -> Errors.Error msg) - | (id,Gfun f)::l -> - (match transfun id f with - | Errors.OK tf -> - (match transform_partial_prog transfun l with - | Errors.OK x -> Errors.OK ((id,Gfun tf)::x) - | Errors.Error msg -> Errors.Error msg) - | Errors.Error msg -> - Errors.Error ((Errors.MSG (coqstring_of_camlstring "In function"))::((Errors.CTX - id) :: (Errors.MSG (coqstring_of_camlstring ": ") :: msg)))) - let expand_program (p: Asm.program) : Asm.program Errors.res = - match transform_partial_prog expand_fundef p.prog_defs with - | Errors.OK x-> - Errors.OK { prog_defs = x; prog_public = p.prog_public; prog_main = - p.prog_main } - | Errors.Error msg -> Errors.Error msg + AST.transform_partial_ident_program expand_fundef p |