diff options
Diffstat (limited to 'common/AST.v')
| -rw-r--r-- | common/AST.v | 283 |
1 files changed, 247 insertions, 36 deletions
diff --git a/common/AST.v b/common/AST.v index 4d929f13..16673c47 100644 --- a/common/AST.v +++ b/common/AST.v @@ -16,8 +16,8 @@ (** This file defines a number of data types and operations used in the abstract syntax trees of many of the intermediate languages. *) +Require Import String. Require Import Coqlib. -Require String. Require Import Errors. Require Import Integers. Require Import Floats. @@ -33,8 +33,6 @@ Definition ident := positive. Definition ident_eq := peq. -Parameter ident_of_string : String.string -> ident. - (** The intermediate languages are weakly typed, using the following types: *) Inductive typ : Type := @@ -123,7 +121,7 @@ Definition proj_sig_res (s: signature) : typ := Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}. Proof. generalize opt_typ_eq, list_typ_eq; intros; decide equality. - generalize bool_dec; intros. decide equality. + generalize bool_dec; intros. decide equality. Defined. Global Opaque signature_eq. @@ -257,31 +255,72 @@ Lemma transform_program_function: exists f, In (i, Gfun f) p.(prog_defs) /\ transf f = tf. Proof. simpl. unfold transform_program. intros. - exploit list_in_map_inv; eauto. - intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. + 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. -(** The following is a more general presentation of [transform_program] where +(** 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. +Local Open Scope error_monad_scope. 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,28 +338,67 @@ 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 -> In (i, Gfun tf) tp.(prog_defs) -> exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun f = OK tf. Proof. - intros. monadInv H. simpl in H0. + 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 f) as [tf1|msg] eqn:?; monadInv EQ. - simpl in H0; destruct H0. inv H. exists f; auto. + simpl in H0; destruct H0. inv H. exists f; auto. exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. destruct (transf_globvar 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_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 -> @@ -329,7 +407,7 @@ Lemma transform_partial_program2_variable: In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs) /\ transf_var v = OK tv.(gvar_info). Proof. - intros. monadInv H. simpl in H0. + 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]]. @@ -342,6 +420,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 -> @@ -351,16 +451,35 @@ Lemma transform_partial_program2_succeeds: | Gvar gv => exists tv, transf_var gv.(gvar_info) = OK tv end. Proof. - intros. monadInv H. + intros. monadInv H. revert x EQ H0. induction (prog_defs p); simpl; intros. contradiction. destruct a as [id1 g1]. destruct g1. - destruct (transf_fun f) eqn:TF; try discriminate. monadInv EQ. + destruct (transf_fun f) eqn:TF; try discriminate. monadInv EQ. destruct H0. inv H. econstructor; eauto. eapply IHl; eauto. destruct (transf_globvar v) eqn:TV; try discriminate. monadInv EQ. 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 +488,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 +504,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 +532,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 +556,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 +575,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 +591,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,13 +607,30 @@ 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 -> In (i, Gfun tf) tp.(prog_defs) -> exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial f = OK tf. Proof. - apply transform_partial_program2_function. + 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: @@ -453,8 +639,18 @@ Lemma transform_partial_program_succeeds: In (i, Gfun fd) p.(prog_defs) -> exists tfd, transf_partial fd = OK tfd. Proof. - unfold transform_partial_program; intros. - exploit transform_partial_program2_succeeds; eauto. + unfold transform_partial_program; intros. + 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. @@ -467,7 +663,23 @@ Proof. unfold transform_partial_program, transform_partial_program2, transform_program; intros. replace (transf_globdefs (fun f => OK (transf f)) (fun v => OK v) p.(prog_defs)) with (OK (map (transform_program_globdef transf) p.(prog_defs))). - auto. + auto. + induction (prog_defs p); simpl. + auto. + destruct a as [id [f|v]]; rewrite <- IHl. + auto. + 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. @@ -475,11 +687,11 @@ Proof. destruct v; auto. Qed. -(** The following is a relational presentation of +(** The following is a relational presentation of [transform_partial_augment_preogram]. Given relations between function definitions and between variable information, it defines a relation between programs stating that the two programs have appropriately related - shapes (global names are preserved and possibly augmented, etc) + shapes (global names are preserved and possibly augmented, etc) and that identically-named function definitions and variable information are related. *) @@ -511,24 +723,24 @@ Lemma transform_partial_augment_program_match: forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) - (p: program A V) + (p: program A V) (new_globs : list (ident * globdef B W)) (new_main : ident) (tp: program B W), transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK tp -> - match_program + match_program (fun fd tfd => transf_fun fd = OK tfd) (fun info tinfo => transf_var info = OK tinfo) new_globs new_main p tp. Proof. - unfold transform_partial_augment_program; intros. monadInv H. + unfold transform_partial_augment_program; intros. monadInv H. red; simpl. split; auto. exists x; split; auto. revert x EQ. generalize (prog_defs p). induction l; simpl; intros. monadInv EQ. constructor. - destruct a as [id [f|v]]. + destruct a as [id [f|v]]. (* function *) - destruct (transf_fun f) as [tf|?] eqn:?; monadInv EQ. + destruct (transf_fun f) as [tf|?] eqn:?; monadInv EQ. constructor; auto. constructor; auto. (* variable *) unfold transf_globvar in EQ. @@ -545,10 +757,10 @@ Qed. and associated operations. *) Inductive external_function : Type := - | EF_external (name: ident) (sg: signature) + | EF_external (name: string) (sg: signature) (** A system call or library function. Produces an event in the trace. *) - | EF_builtin (name: ident) (sg: signature) + | EF_builtin (name: string) (sg: signature) (** A compiler built-in function. Behaves like an external, but can be inlined by the compiler. *) | EF_vload (chunk: memory_chunk) @@ -571,15 +783,15 @@ Inductive external_function : Type := Produces no observable event. *) | EF_memcpy (sz: Z) (al: Z) (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *) - | EF_annot (text: ident) (targs: list typ) + | EF_annot (text: string) (targs: list typ) (** A programmer-supplied annotation. Takes zero, one or several arguments, produces an event carrying the text and the values of these arguments, and returns no value. *) - | EF_annot_val (text: ident) (targ: typ) + | EF_annot_val (text: string) (targ: typ) (** Another form of annotation that takes one argument, produces an event carrying the text and the value of this argument, and returns the value of the argument. *) - | EF_inline_asm (text: ident) (sg: signature) (clobbers: list String.string) + | EF_inline_asm (text: string) (sg: signature) (clobbers: list string) (** Inline [asm] statements. Semantically, treated like an annotation with no parameters ([EF_annot text nil]). To be used with caution, as it can invalidate the semantic @@ -637,9 +849,8 @@ Definition ef_reloads (ef: external_function) : bool := Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}. Proof. - generalize ident_eq signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. + generalize ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. decide equality. - apply list_eq_dec. apply String.string_dec. Defined. Global Opaque external_function_eq. @@ -679,7 +890,7 @@ End TRANSF_PARTIAL_FUNDEF. (** * Arguments and results to builtin functions *) -Set Contextual Implicit. +Set Contextual Implicit. Inductive builtin_arg (A: Type) : Type := | BA (x: A) @@ -737,7 +948,7 @@ Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_ar | BA_addrstack ofs => BA_addrstack ofs | BA_loadglobal chunk id ofs => BA_loadglobal chunk id ofs | BA_addrglobal id ofs => BA_addrglobal id ofs - | BA_splitlong hi lo => + | BA_splitlong hi lo => BA_splitlong (map_builtin_arg f hi) (map_builtin_arg f lo) end. @@ -745,7 +956,7 @@ Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_re match a with | BR x => BR (f x) | BR_none => BR_none - | BR_splitlong hi lo => + | BR_splitlong hi lo => BR_splitlong (map_builtin_res f hi) (map_builtin_res f lo) end. |