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

2 files changed, 18 insertions, 36 deletions

diff --git a/powerpc/Constprop.v b/powerpc/Constprop.v
index 76ea153..109125c 100644
--- a/powerpc/Constprop.v
+++ b/powerpc/Constprop.v
@@ -674,7 +674,7 @@ Definition transfer (f: function) (pc: node) (before: D.t) :=
 Module DS := Dataflow_Solver(D)(NodeSetForward).
 
 Definition analyze (f: RTL.function): PMap.t D.t :=
-  match DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) 
+  match DS.fixpoint (successors f) (transfer f) 
                     ((f.(fn_entrypoint), D.top) :: nil) with
   | None => PMap.init D.top
   | Some res => res
@@ -1062,19 +1062,6 @@ Definition transf_instr (approx: D.t) (instr: instruction) :=
 Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code :=
   PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.
 
-Lemma transf_code_wf:
-  forall f approxs,
-  (forall pc, Plt pc f.(fn_nextpc) \/ f.(fn_code)!pc = None) ->
-  (forall pc, Plt pc f.(fn_nextpc)
-      \/ (transf_code approxs f.(fn_code))!pc = None).
-Proof.
-  intros. 
-  elim (H pc); intro.
-  left; auto.
-  right. unfold transf_code. rewrite PTree.gmap. 
-  unfold option_map; rewrite H0. reflexivity.
-Qed.
-
 Definition transf_function (f: function) : function :=
   let approxs := analyze f in
   mkfunction
@@ -1082,9 +1069,7 @@ Definition transf_function (f: function) : function :=
     f.(fn_params)
     f.(fn_stacksize)
     (transf_code approxs f.(fn_code))
-    f.(fn_entrypoint)
-    f.(fn_nextpc)
-    (transf_code_wf f approxs f.(fn_code_wf)).
+    f.(fn_entrypoint).
 
 Definition transf_fundef (fd: fundef) : fundef :=
   AST.transf_fundef transf_function fd.
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 *)