Added versions of the tranform_* functions in AST to work with functions

taking the ident as argument.

This functions are currently not used inside the proven part but it
is nice to have them already there, when they are used by some future
pass. They also come equiped with the corresponding proofs.

1 files changed, 216 insertions, 1 deletions

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