Cil2Csyntax: added goto and labels; added assignment between structs

Kildall: simplified the interface
Constprop, CSE, Allocation, Linearize: updated for the new Kildall
RTL, LTL: removed the well-formedness condition on the CFG, 
  it is no longer necessary with the new Kildall and it is problematic
  for validated optimizations.
Maps: more efficient implementation of PTree.fold.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 16 insertions, 19 deletions

diff --git a/powerpc/Constpropproof.v b/powerpc/Constpropproof.v
index fb01f75..6e17f30 100644
--- a/powerpc/Constpropproof.v
+++ b/powerpc/Constpropproof.v
@@ -219,19 +219,19 @@ Qed.
   a solution of the forward dataflow inequations. *)
 
 Lemma analyze_correct_1:
-  forall f pc rs pc',
-  In pc' (successors f pc) ->
+  forall f pc rs pc' i,
+  f.(fn_code)!pc = Some i ->
+  In pc' (successors_instr i) ->
   regs_match_approx (transfer f pc (analyze f)!!pc) rs ->
   regs_match_approx (analyze f)!!pc' rs.
 Proof.
-  intros until pc'. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (fn_nextpc f) (transfer f)
+  intros until i. unfold analyze. 
+  caseEq (DS.fixpoint (successors f) (transfer f)
                       ((fn_entrypoint f, D.top) :: nil)).
   intros approxs; intros.
   apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
   eapply DS.fixpoint_solution; eauto.
-  elim (fn_code_wf f pc); intro. auto. 
-  unfold successors in H0; rewrite H2 in H0; simpl; contradiction.
+  unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto.
   auto.
   intros. rewrite PMap.gi. apply regs_match_approx_top. 
 Qed.
@@ -241,7 +241,7 @@ Lemma analyze_correct_3:
   regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs.
 Proof.
   intros. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (fn_nextpc f) (transfer f)
+  caseEq (DS.fixpoint (successors f) (transfer f)
                       ((fn_entrypoint f, D.top) :: nil)).
   intros approxs; intros.
   apply regs_match_approx_increasing with D.top.
@@ -756,7 +756,7 @@ Proof.
   TransfInstr; intro. eapply exec_Inop; eauto.
   econstructor; eauto.
   eapply analyze_correct_1 with (pc := pc); eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  simpl; auto.
   unfold transfer; rewrite H. auto.
 
   (* Iop *)
@@ -780,7 +780,7 @@ Proof.
   rewrite A; rewrite B; auto.
   econstructor; eauto. 
   eapply analyze_correct_1 with (pc := pc); eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  simpl; auto.
   unfold transfer; rewrite H. 
   apply regs_match_approx_update; auto. 
   eapply eval_static_operation_correct; eauto.
@@ -798,8 +798,7 @@ Proof.
   exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split.
   eapply exec_Iload; eauto.
   econstructor; eauto. 
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analyze_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
   apply regs_match_approx_update; auto. simpl; auto.
 
@@ -815,8 +814,7 @@ Proof.
   exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split.
   eapply exec_Istore; eauto.
   econstructor; eauto. 
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analyze_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. auto. 
 
   (* Icall *)
@@ -826,8 +824,7 @@ Proof.
   eapply exec_Icall; eauto. apply sig_function_translated; auto.
   constructor; auto. constructor; auto.
   econstructor; eauto. 
-  intros. apply analyze_correct_1 with pc; auto.
-  unfold successors; rewrite H; auto with coqlib.
+  intros. eapply analyze_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H.
   apply regs_match_approx_update; auto. simpl. auto.
 
@@ -854,8 +851,8 @@ Proof.
   replace b with true. intro; eapply exec_Inop; eauto. congruence.
   intros. eapply exec_Icond_true; eauto.
   econstructor; eauto.
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analyze_correct_1; eauto.
+  simpl; auto.
   unfold transfer; rewrite H; auto.
 
   (* Icond, false *)
@@ -874,8 +871,8 @@ Proof.
   replace b with false. intro; eapply exec_Inop; eauto. congruence.
   intros. eapply exec_Icond_false; eauto.
   econstructor; eauto.
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analyze_correct_1; eauto.
+  simpl; auto.
   unfold transfer; rewrite H; auto.
 
   (* Ireturn *)