Big merge of the newregalloc-int64 branch. Lots of changes in two directions:

1- new register allocator (+ live range splitting, spilling&reloading, etc)
   based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").


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

1 files changed, 112 insertions, 82 deletions

diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index d589260..d02cb2e 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -36,16 +36,16 @@ Definition measure_edge (u: U.t) (pc s: node) (f: node -> nat) : node -> nat :=
            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)
+Definition record_goto' (uf: U.t * (node -> nat)) (pc: node) (b: bblock) : U.t * (node -> nat) :=
+  match b with
+  | Lbranch s :: b' => 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) =>
+  | Some(Lbranch s :: b) =>
       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
@@ -65,21 +65,21 @@ Proof.
   red; intros; simpl. rewrite PTree.gempty. apply U.repr_empty.
 
 (* inductive case *)
-  intros m uf pc i; intros. destruct uf as [u f]. 
+  intros m uf pc bb; 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]]].
+  assert (record_goto' (u, f) pc bb = (u, f)
+          \/ exists s, exists bb', bb = Lbranch s :: bb' /\ record_goto' (u, f) pc bb = (U.union u pc s, measure_edge u pc s f)).
+    unfold record_goto'; simpl. destruct bb; auto. destruct i; auto. right. exists s; exists bb; auto.
+  destruct H2 as [B | [s [bb' [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.
+  destruct bb; auto. destruct i; auto.
   apply H1. 
 
-(* i is Lnop s, u becomes union u pc s, f becomes measure_edge u pc s f *)
+(* b is Lbranch 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.
 
@@ -91,11 +91,11 @@ Proof.
 (* 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.
+  generalize (H1 pc'). simpl. destruct (m!pc'); auto. destruct b; auto. destruct i; 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. 
+  rewrite P. destruct (peq (U.repr u s0) pc). omega. auto. 
 Qed.
 
 Definition record_gotos' (f: function) :=
@@ -110,7 +110,7 @@ Proof.
   induction l; intros; simpl.
   auto.
   unfold record_goto' at 2. unfold record_goto at 2. 
-  destruct (snd a); apply IHl.
+  destruct (snd a). apply IHl. destruct i; apply IHl.
 Qed.
 
 Definition branch_target (f: function) (pc: node) : node :=
@@ -122,7 +122,7 @@ Definition count_gotos (f: function) (pc: node) : nat :=
 Theorem record_gotos_correct:
   forall f pc,
   match f.(fn_code)!pc with
-  | Some(Lnop s) =>
+  | Some(Lbranch s :: b) =>
        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
@@ -204,15 +204,18 @@ Qed.
   the values of locations and the memory states are identical in the
   original and transformed codes. *)
 
+Definition tunneled_block (f: function) (b: bblock) :=
+  tunnel_block (record_gotos f) b.
+
 Definition tunneled_code (f: function) :=
-  PTree.map (fun pc b => tunnel_instr (record_gotos f) b) (fn_code f).
+  PTree.map1 (tunneled_block f) (fn_code f).
 
 Inductive match_stackframes: stackframe -> stackframe -> Prop :=
   | match_stackframes_intro:
-      forall res f sp ls0 pc,
+      forall f sp ls0 bb,
       match_stackframes
-         (Stackframe res f sp ls0 pc)
-         (Stackframe res (tunnel_function f) sp ls0 (branch_target f pc)).
+         (Stackframe f sp ls0 bb)
+         (Stackframe (tunnel_function f) sp ls0 (tunneled_block f bb)).
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
@@ -220,6 +223,16 @@ Inductive match_states: state -> state -> Prop :=
       list_forall2 match_stackframes s ts ->
       match_states (State s f sp pc ls m)
                    (State ts (tunnel_function f) sp (branch_target f pc) ls m)
+  | match_states_block:
+      forall s f sp bb ls m ts,
+      list_forall2 match_stackframes s ts ->
+      match_states (Block s f sp bb ls m)
+                   (Block ts (tunnel_function f) sp (tunneled_block f bb) ls m)
+  | match_states_interm:
+      forall s f sp pc bb ls m ts,
+      list_forall2 match_stackframes s ts ->
+      match_states (Block s f sp (Lbranch pc :: bb) ls m)
+                   (State ts (tunnel_function f) sp (branch_target f pc) ls m)
   | match_states_call:
       forall s f ls m ts,
       list_forall2 match_stackframes s ts ->
@@ -238,17 +251,19 @@ Inductive match_states: state -> state -> Prop :=
 
 Definition measure (st: state) : nat :=
   match st with
-  | State s f sp pc ls m => count_gotos f pc
+  | State s f sp pc ls m => (count_gotos f pc * 2)%nat
+  | Block s f sp (Lbranch pc :: _) ls m => (count_gotos f pc * 2 + 1)%nat
+  | Block s f sp bb ls m => 0%nat
   | Callstate s f ls m => 0%nat
   | Returnstate s ls m => 0%nat
   end.
 
-Lemma tunnel_function_lookup:
-  forall f pc i,
-  f.(fn_code)!pc = Some i ->
-  (tunnel_function f).(fn_code)!pc = Some (tunnel_instr (record_gotos f) i).
+Lemma match_parent_locset:
+  forall s ts,
+  list_forall2 match_stackframes s ts ->
+  parent_locset ts = parent_locset s.
 Proof.
-  intros. simpl. rewrite PTree.gmap. rewrite H. auto.
+  induction 1; simpl. auto. inv H; auto.
 Qed.
 
 Lemma tunnel_step_correct:
@@ -258,98 +273,113 @@ Lemma tunnel_step_correct:
   \/ (measure st2 < measure st1 /\ t = E0 /\ match_states st2 st1')%nat.
 Proof.
   induction 1; intros; try inv MS.
-  (* Lnop *)
-  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. 
-  right. split. simpl. auto. split. auto. 
-  rewrite B. econstructor; eauto. 
+
+  (* entering a block *)
+  assert (DEFAULT: branch_target f pc = pc ->
+    (exists st2' : state,
+     step tge (State ts (tunnel_function f) sp (branch_target f pc) rs m) E0 st2'
+     /\ match_states (Block s f sp bb rs m) st2')).
+  intros. rewrite H0. econstructor; split. 
+  econstructor. simpl. rewrite PTree.gmap1. rewrite H. simpl. eauto. 
+  econstructor; eauto.
+
+  generalize (record_gotos_correct f pc). rewrite H. 
+  destruct bb; auto. destruct i; auto. 
+  intros [A | [B C]]. auto. 
+  right. split. simpl. omega. 
+  split. auto.
+  rewrite B. econstructor; eauto.
+
   (* Lop *)
-  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
-  left; econstructor; split.
+  left; simpl; 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.
+  rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
   econstructor; eauto.
   (* Lload *)
-  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
-  left; econstructor; split.
+  left; simpl; econstructor; split.
   eapply exec_Lload with (a := a). 
-  rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.  
-  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  eauto.
+  rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+  eauto. eauto.
+  econstructor; eauto.
+  (* Lgetstack *)
+  left; simpl; econstructor; split.
+  econstructor; eauto.
+  econstructor; eauto.
+  (* Lsetstack *)
+  left; simpl; econstructor; split.
+  econstructor; eauto.
   econstructor; eauto.
   (* Lstore *)
-  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
-  left; econstructor; split.
+  left; simpl; econstructor; split.
   eapply exec_Lstore with (a := a).
-  rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.  
-  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  eauto.
+  rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+  eauto. 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 A. rewrite (tunnel_function_lookup _ _ _ H); simpl.
-  rewrite sig_preserved. auto.
+  left; simpl; econstructor; split. 
+  eapply exec_Lcall with (fd := tunnel_fundef fd); eauto.
   apply find_function_translated; auto.
+  rewrite sig_preserved. 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 A. rewrite (tunnel_function_lookup _ _ _ H); simpl.
-  rewrite sig_preserved. auto.
+  left; simpl; econstructor; split. 
+  eapply exec_Ltailcall with (fd := tunnel_fundef fd); eauto.
+  erewrite match_parent_locset; eauto. 
   apply find_function_translated; auto.
+  apply sig_preserved.
+  erewrite <- match_parent_locset; eauto.
   econstructor; eauto.
   (* Lbuiltin *)
-  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
-  left; econstructor; split.
+  left; simpl; econstructor; split.
   eapply exec_Lbuiltin; eauto. 
-  rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.
-  eapply external_call_symbols_preserved; eauto.
+  eapply external_call_symbols_preserved'; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
-  (* cond *)
-  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
-  left; econstructor; split.
+  (* Lannot *)
+  left; simpl; econstructor; split.
+  eapply exec_Lannot; eauto. 
+  eapply external_call_symbols_preserved'; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  econstructor; eauto.
+
+  (* Lbranch (preserved) *)
+  left; simpl; econstructor; split.
+  eapply exec_Lbranch; eauto. 
+  fold (branch_target f pc). econstructor; eauto.
+  (* Lbranch (eliminated) *)
+  right; split. simpl. omega. split. auto. constructor; auto. 
+
+  (* Lcond *)
+  left; simpl; econstructor; split.
   eapply exec_Lcond; eauto.
-  rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
   destruct b; econstructor; eauto.
-  (* jumptable *)
-  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
-  left; econstructor; split.
+  (* Ljumptable *)
+  left; simpl; econstructor; split.
   eapply exec_Ljumptable. 
-  rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
-  eauto. rewrite list_nth_z_map. change U.elt with node. rewrite H1. reflexivity. 
+  eauto. rewrite list_nth_z_map. change U.elt with node. rewrite H0. reflexivity. eauto.
   econstructor; eauto. 
-  (* return *)
-  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
-  left; econstructor; split.
+  (* Lreturn *)
+  left; simpl; econstructor; split.
   eapply exec_Lreturn; eauto.
-  rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
-  simpl. constructor; auto.
+  erewrite <- match_parent_locset; eauto.
+  constructor; auto.
   (* internal function *)
-  simpl. left; econstructor; split.
+  left; simpl; econstructor; split.
   eapply exec_function_internal; eauto.
   simpl. econstructor; eauto. 
   (* external function *)
-  simpl. left; econstructor; split.
+  left; simpl; econstructor; split.
   eapply exec_function_external; eauto.
-  eapply external_call_symbols_preserved; eauto.
+  eapply external_call_symbols_preserved'; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   simpl. econstructor; eauto. 
   (* return *)
   inv H3. inv H1.
   left; econstructor; split.
   eapply exec_return; eauto.
-  constructor. auto.
+  constructor; auto.
 Qed.
 
 Lemma transf_initial_states:
@@ -357,7 +387,7 @@ Lemma transf_initial_states:
   exists st2, initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H. 
-  exists (Callstate nil (tunnel_fundef f) nil m0); split.
+  exists (Callstate nil (tunnel_fundef f) (Locmap.init Vundef) m0); split.
   econstructor; eauto.
   apply Genv.init_mem_transf; auto.
   change (prog_main tprog) with (prog_main prog).
@@ -371,7 +401,7 @@ Lemma transf_final_states:
   forall st1 st2 r, 
   match_states st1 st2 -> final_state st1 r -> final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv H4. constructor.  
+  intros. inv H0. inv H. inv H6. econstructor; eauto.  
 Qed.
 
 Theorem transf_program_correct: