From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: 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 --- backend/Tunnelingproof.v | 194 +++++++++++++++++++++++++++-------------------- 1 file changed, 112 insertions(+), 82 deletions(-) (limited to 'backend/Tunnelingproof.v') 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: -- cgit v1.2.3