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.

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