Added 'going wrong' behaviors

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

1 files changed, 113 insertions, 108 deletions

diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 08f5f6cc..eccb62dd 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -14,6 +14,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Import UnionFind.
 Require Import AST.
 Require Import Values.
 Require Import Mem.
@@ -25,98 +26,112 @@ Require Import Locations.
 Require Import LTL.
 Require Import Tunneling.
 
-(** * Properties of branch target computation *)
+(** * Properties of the branch map computed using union-find. *)
 
-Lemma is_goto_instr_correct:
-  forall b s,
-  is_goto_instr b = Some s -> b = Some (Lnop s).
-Proof.
-  unfold is_goto_instr; intros.
-  destruct b; try discriminate.
-  destruct i; discriminate || congruence. 
-Qed. 
-
-Lemma branch_target_rec_1:
-  forall f pc n,
-  branch_target_rec f pc n = Some pc
-  \/ branch_target_rec f pc n = None
-  \/ exists pc', f.(fn_code)!pc = Some(Lnop pc').
-Proof.
-  intros. destruct n; simpl.
-  right; left; auto.
-  caseEq (is_goto_instr f.(fn_code)!pc); intros.
-  right; right. exists n0. apply is_goto_instr_correct; auto.
-  left; auto.
-Qed.
+(** A variant of [record_goto] that also incrementally computes a measure [f: node -> nat]
+  counting the number of [Lnop] instructions starting at a given [pc] that were eliminated. *)
 
-Lemma branch_target_rec_2:
-  forall f n pc1 pc2 pc3,
-  f.(fn_code)!pc1 = Some (Lnop pc2) ->
-  branch_target_rec f pc1 n = Some pc3 ->
-  branch_target_rec f pc2 n = Some pc3.
+Definition measure_edge (u: U.t) (pc s: node) (f: node -> nat) : node -> nat :=
+  fun x => if peq (U.repr u s) pc then f x
+           else if peq (U.repr u x) pc then (f x + f s + 1)%nat
+           else f x.
+
+Definition record_goto' (uf: U.t * (node -> nat)) (pc: node) (i: instruction) : U.t * (node -> nat) :=
+  match i with
+  | Lnop s => let (u, f) := uf in (U.union u pc s, measure_edge u pc s f)
+  | _ => uf
+  end.
+
+Definition branch_map_correct (c: code) (uf: U.t * (node -> nat)): Prop :=
+  forall pc,
+  match c!pc with
+  | Some(Lnop s) =>
+      U.repr (fst uf) pc = pc \/ (U.repr (fst uf) pc = U.repr (fst uf) s /\ snd uf s < snd uf pc)%nat
+  | _ =>
+      U.repr (fst uf) pc = pc
+  end.
+
+Lemma record_gotos'_correct:
+  forall c,
+  branch_map_correct c (PTree.fold record_goto' c (U.empty, fun (x: node) => O)).
 Proof.
-  induction n. 
-  simpl. intros; discriminate.
-  intros pc1 pc2 pc3 ATpc1 H. simpl in H. 
-  unfold is_goto_instr in H; rewrite ATpc1 in H.
-  simpl. caseEq (is_goto_instr f.(fn_code)!pc2); intros.
-  apply IHn with pc2. apply is_goto_instr_correct; auto. auto.
-  destruct n; simpl in H. discriminate. rewrite H0 in H. auto.
+  intros.
+  apply PTree_Properties.fold_rec with (P := fun c uf => branch_map_correct c uf).
+
+(* extensionality *)
+  intros. red; intros. rewrite <- H. apply H0.
+
+(* base case *)
+  red; intros; simpl. rewrite PTree.gempty. apply U.repr_empty.
+
+(* inductive case *)
+  intros m uf pc i; intros. destruct uf as [u f]. 
+  assert (PC: U.repr u pc = pc). 
+    generalize (H1 pc). rewrite H. auto.
+  assert (record_goto' (u, f) pc i = (u, f)
+          \/ exists s, i = Lnop s /\ record_goto' (u, f) pc i = (U.union u pc s, measure_edge u pc s f)).
+    unfold record_goto'; simpl. destruct i; auto. right. exists n; auto.
+  destruct H2 as [B | [s [EQ B]]].
+
+(* u and f are unchanged *)
+  rewrite B.
+  red. intro pc'. simpl. rewrite PTree.gsspec. destruct (peq pc' pc). subst pc'. 
+  destruct i; auto.
+  apply H1. 
+
+(* i is Lnop s, u becomes union u pc s, f becomes measure_edge u pc s f *)
+  rewrite B.
+  red. intro pc'. simpl. rewrite PTree.gsspec. destruct (peq pc' pc). subst pc'. rewrite EQ.
+
+(* The new instruction *)
+  rewrite (U.repr_union_2 u pc s); auto. rewrite U.repr_union_3. 
+  unfold measure_edge. destruct (peq (U.repr u s) pc). auto. right. split. auto.
+  rewrite PC. rewrite peq_true. omega.
+
+(* An old instruction *)
+  assert (U.repr u pc' = pc' -> U.repr (U.union u pc s) pc' = pc').
+    intro. rewrite <- H2 at 2. apply U.repr_union_1. congruence. 
+  generalize (H1 pc'). simpl. destruct (m!pc'); auto. destruct i0; auto.
+  intros [P | [P Q]]. left; auto. right.
+  split. apply U.sameclass_union_2. auto.
+  unfold measure_edge. destruct (peq (U.repr u s) pc). auto.
+  rewrite P. destruct (peq (U.repr u n0) pc). omega. auto. 
 Qed.
 
-(** Counting the number of consecutive gotos. *)
-
-Fixpoint count_goto_rec (f: LTL.function) (pc: node) (count: nat)
-                        {struct count} : nat :=
-  match count with
-  | Datatypes.O => Datatypes.O
-  | Datatypes.S count' =>
-      match is_goto_instr f.(fn_code)!pc with
-      | Some s => Datatypes.S (count_goto_rec f s count')
-      | None => Datatypes.O
-      end
-    end.
-
-Definition count_goto (f: LTL.function) (pc: node) : nat :=
-  count_goto_rec f pc 10%nat.
-
-Lemma count_goto_rec_prop:
-  forall f n pc1 pc2 pc3,
-  f.(fn_code)!pc1 = Some (Lnop pc2) ->
-  branch_target_rec f pc1 n = Some pc3 ->
-  (count_goto_rec f pc2 n < count_goto_rec f pc1 n)%nat.
+Definition record_gotos' (f: function) :=
+  PTree.fold record_goto' f.(fn_code) (U.empty, fun (x: node) => O).
+
+Lemma record_gotos_gotos':
+  forall f, fst (record_gotos' f) = record_gotos f.
 Proof.
-  induction n.
-  simpl; intros. discriminate.
-  intros pc1 pc2 pc3 ATpc1 H. simpl in H. 
-  unfold is_goto_instr in H; rewrite ATpc1 in H.
-  simpl. unfold is_goto_instr at 2. rewrite ATpc1. 
-  caseEq (is_goto_instr f.(fn_code)!pc2); intros.
-  exploit (IHn pc2); eauto. apply is_goto_instr_correct; eauto. 
-  omega.
-  omega.
+  intros. unfold record_gotos', record_gotos. 
+  repeat rewrite PTree.fold_spec.
+  generalize (PTree.elements (fn_code f)) (U.empty) (fun _ : node => O).
+  induction l; intros; simpl.
+  auto.
+  unfold record_goto' at 2. unfold record_goto at 2. 
+  destruct (snd a); apply IHl.
 Qed.
 
-(** The following lemma captures the property of [branch_target]
-  on which the proof of semantic preservation relies. *)
+Definition branch_target (f: function) (pc: node) : node :=
+  U.repr (record_gotos f) pc.
 
-Lemma branch_target_characterization:
+Definition count_gotos (f: function) (pc: node) : nat :=
+  snd (record_gotos' f) pc.
+
+Theorem record_gotos_correct:
   forall f pc,
-  branch_target f pc = pc \/
-  (exists pc', f.(fn_code)!pc = Some(Lnop pc')
-            /\ branch_target f pc' = branch_target f pc
-            /\ count_goto f pc' < count_goto f pc)%nat.
+  match f.(fn_code)!pc with
+  | Some(Lnop s) =>
+       branch_target f pc = pc \/
+       (branch_target f pc = branch_target f s /\ count_gotos f s < count_gotos f pc)%nat
+  | _ => branch_target f pc = pc
+  end.
 Proof.
-  intros. unfold branch_target. 
-  generalize (branch_target_rec_1 f pc 10%nat). 
-  intros [A|[A|[pc' AT]]].
-  rewrite A. left; auto.
-  rewrite A. left; auto.
-  caseEq (branch_target_rec f pc 10%nat). intros pcx BT.
-  right. exists pc'. split. auto. 
-  split. rewrite (branch_target_rec_2 _ _ _ _ _ AT BT). auto.
-  unfold count_goto. eapply count_goto_rec_prop; eauto. 
-  intro. left; auto.
+  intros. 
+  generalize (record_gotos'_correct f.(fn_code) pc). simpl.
+  fold (record_gotos' f). unfold branch_map_correct, branch_target, count_gotos.
+  rewrite record_gotos_gotos'. auto.
 Qed.
 
 (** * Preservation of semantics *)
@@ -186,7 +201,7 @@ Qed.
   original and transformed codes. *)
 
 Definition tunneled_code (f: function) :=
-  PTree.map (fun pc b => tunnel_instr f b) (fn_code f).
+  PTree.map (fun pc b => tunnel_instr (record_gotos f) b) (fn_code f).
 
 Inductive match_stackframes: stackframe -> stackframe -> Prop :=
   | match_stackframes_intro:
@@ -219,25 +234,15 @@ Inductive match_states: state -> state -> Prop :=
 
 Definition measure (st: state) : nat :=
   match st with
-  | State s f sp pc ls m => count_goto f pc
+  | State s f sp pc ls m => count_gotos f pc
   | Callstate s f ls m => 0%nat
   | Returnstate s ls m => 0%nat
   end.
 
-Lemma branch_target_identity:
-  forall f pc,
-  match f.(fn_code)!pc with Some(Lnop _) => False | _ => True end ->
-  branch_target f pc = pc.
-Proof.
-  intros. 
-  destruct (branch_target_characterization f pc) as [A | [pc' [B C]]].
-  auto. rewrite B in H. contradiction.
-Qed.
-
 Lemma tunnel_function_lookup:
   forall f pc i,
   f.(fn_code)!pc = Some i ->
-  (tunnel_function f).(fn_code)!pc = Some (tunnel_instr f i).
+  (tunnel_function f).(fn_code)!pc = Some (tunnel_instr (record_gotos f) i).
 Proof.
   intros. simpl. rewrite PTree.gmap. rewrite H. auto.
 Qed.
@@ -250,23 +255,23 @@ Lemma tunnel_step_correct:
 Proof.
   induction 1; intros; try inv MS.
   (* Lnop *)
-  destruct (branch_target_characterization f pc) as [A | [pc1 [B [C D]]]].
+  generalize (record_gotos_correct f pc); rewrite H. 
+  intros [A | [B C]].
   left; econstructor; split.
   eapply exec_Lnop. rewrite A. 
   rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.  
   econstructor; eauto. 
-  assert (pc1 = pc') by congruence. subst pc1.
   right. split. simpl. auto. split. auto. 
-  rewrite <- C. econstructor; eauto. 
+  rewrite B. econstructor; eauto. 
   (* Lop *)
-  rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
+  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
   left; econstructor; split.
   eapply exec_Lop with (v := v); eauto.
   rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.  
   rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
   econstructor; eauto.
   (* Lload *)
-  rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
+  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
   left; econstructor; split.
   eapply exec_Lload with (a := a). 
   rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.  
@@ -274,7 +279,7 @@ Proof.
   eauto.
   econstructor; eauto.
   (* Lstore *)
-  rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
+  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
   left; econstructor; split.
   eapply exec_Lstore with (a := a).
   rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.  
@@ -282,36 +287,36 @@ Proof.
   eauto.
   econstructor; eauto.
   (* Lcall *)
+  generalize (record_gotos_correct f pc); rewrite H; intro A.
   left; econstructor; split. 
   eapply exec_Lcall with (f' := tunnel_fundef f'); eauto.
-  rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
-  rewrite (tunnel_function_lookup _ _ _ H); simpl.
+  rewrite A. rewrite (tunnel_function_lookup _ _ _ H); simpl.
   rewrite sig_preserved. auto.
   apply find_function_translated; auto.
   econstructor; eauto.
   constructor; auto. 
   constructor; auto.
   (* Ltailcall *)
+  generalize (record_gotos_correct f pc); rewrite H; intro A.
   left; econstructor; split. 
   eapply exec_Ltailcall with (f' := tunnel_fundef f'); eauto.
-  rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
-  rewrite (tunnel_function_lookup _ _ _ H); simpl.
+  rewrite A. rewrite (tunnel_function_lookup _ _ _ H); simpl.
   rewrite sig_preserved. auto.
   apply find_function_translated; auto.
   econstructor; eauto.
   (* cond *)
-  rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
+  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
   left; econstructor; split.
   eapply exec_Lcond_true; eauto.
   rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
   econstructor; eauto.
-  rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
+  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
   left; econstructor; split.
   eapply exec_Lcond_false; eauto.
   rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
   econstructor; eauto.
   (* return *)
-  rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
+  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
   left; econstructor; split.
   eapply exec_Lreturn; eauto.
   rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
@@ -355,7 +360,7 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior),
+  forall (beh: program_behavior), not_wrong beh ->
   exec_program p beh -> exec_program tp beh.
 Proof.
   unfold exec_program; intros.