From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 9 Feb 2006 14:55:48 +0000 Subject: Initial import of compcert git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Tunnelingproof.v | 311 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 311 insertions(+) create mode 100644 backend/Tunnelingproof.v (limited to 'backend/Tunnelingproof.v') diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v new file mode 100644 index 0000000..111d1d8 --- /dev/null +++ b/backend/Tunnelingproof.v @@ -0,0 +1,311 @@ +(** Correctness proof for the branch tunneling optimization. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. +Require Import Op. +Require Import Locations. +Require Import LTL. +Require Import Tunneling. + +(** * Properties of branch target computation *) + +Lemma is_goto_block_correct: + forall b s, + is_goto_block b = Some s -> b = Some (Bgoto s). +Proof. + unfold is_goto_block; intros. + destruct b. destruct b; discriminate || congruence. + discriminate. +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(Bgoto pc'). +Proof. + intros. destruct n; simpl. + right; left; auto. + caseEq (is_goto_block f.(fn_code)!pc); intros. + right; right. exists n0. apply is_goto_block_correct; auto. + left; auto. +Qed. + +Lemma branch_target_rec_2: + forall f n pc1 pc2 pc3, + f.(fn_code)!pc1 = Some (Bgoto pc2) -> + branch_target_rec f pc1 n = Some pc3 -> + branch_target_rec f pc2 n = Some pc3. +Proof. + induction n. + simpl. intros; discriminate. + intros pc1 pc2 pc3 ATpc1 H. simpl in H. + unfold is_goto_block in H; rewrite ATpc1 in H. + simpl. caseEq (is_goto_block f.(fn_code)!pc2); intros. + apply IHn with pc2. apply is_goto_block_correct; auto. auto. + destruct n; simpl in H. discriminate. rewrite H0 in H. auto. +Qed. + +(** The following lemma captures the property of [branch_target] + on which the proof of semantic preservation relies. *) + +Lemma branch_target_characterization: + forall f pc, + branch_target f pc = pc \/ + (exists pc', f.(fn_code)!pc = Some(Bgoto pc') + /\ branch_target f pc' = branch_target f pc). +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. + rewrite (branch_target_rec_2 _ _ _ _ _ AT BT). auto. + intro. left; auto. +Qed. + +(** * Preservation of semantics *) + +Section PRESERVATION. + +Variable p: program. +Let tp := tunnel_program p. +Let ge := Genv.globalenv p. +Let tge := Genv.globalenv tp. + +Lemma functions_translated: + forall v f, + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (tunnel_function f). +Proof (@Genv.find_funct_transf _ _ tunnel_function p). + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + Genv.find_funct_ptr tge v = Some (tunnel_function f). +Proof (@Genv.find_funct_ptr_transf _ _ tunnel_function p). + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof (@Genv.find_symbol_transf _ _ tunnel_function p). + +(** These are inversion lemmas, characterizing what happens in the LTL + semantics when executing [Bgoto] instructions or basic blocks. *) + +Lemma exec_instrs_Bgoto_inv: + forall sp b1 ls1 m1 b2 ls2 m2, + exec_instrs ge sp b1 ls1 m1 b2 ls2 m2 -> + forall s1, + b1 = Bgoto s1 -> b2 = b1 /\ ls2 = ls1 /\ m2 = m1. +Proof. + induction 1. + intros. tauto. + intros. subst b1. inversion H. + intros. generalize (IHexec_instrs1 s1 H1). intros [A [B C]]. + subst b2; subst rs2; subst m2. eauto. +Qed. + +Lemma exec_block_Bgoto_inv: + forall sp s ls1 m1 out ls2 m2, + exec_block ge sp (Bgoto s) ls1 m1 out ls2 m2 -> + out = Cont s /\ ls2 = ls1 /\ m2 = m1. +Proof. + intros. inversion H; + generalize (exec_instrs_Bgoto_inv _ _ _ _ _ _ _ H0 s (refl_equal _)); + intros [A [B C]]. + split. congruence. tauto. + discriminate. + discriminate. + discriminate. +Qed. + +Lemma exec_blocks_Bgoto_inv: + forall c sp pc1 ls1 m1 out ls2 m2 s, + exec_blocks ge c sp pc1 ls1 m1 out ls2 m2 -> + c!pc1 = Some (Bgoto s) -> + (out = Cont pc1 /\ ls2 = ls1 /\ m2 = m1) + \/ exec_blocks ge c sp s ls1 m1 out ls2 m2. +Proof. + induction 1; intros. + left; tauto. + assert (b = Bgoto s). congruence. subst b. + generalize (exec_block_Bgoto_inv _ _ _ _ _ _ _ H0). + intros [A [B C]]. subst out; subst rs'; subst m'. + right. apply exec_blocks_refl. + elim (IHexec_blocks1 H1). + intros [A [B C]]. + assert (pc2 = pc1). congruence. subst rs2; subst m2; subst pc2. + apply IHexec_blocks2; auto. + intro. right. apply exec_blocks_trans with pc2 rs2 m2; auto. +Qed. + +(** The following [exec_*_prop] predicates state the correctness + of the tunneling transformation: for each LTL execution + in the original code (of an instruction, a sequence of instructions, + a basic block, a sequence of basic blocks, etc), there exists + a similar LTL execution in the tunneled code. + + Note that only the control-flow is changed: the values of locations + and the memory states are identical in the original and transformed + codes. *) + +Definition tunnel_outcome (f: function) (out: outcome) := + match out with + | Cont pc => Cont (branch_target f pc) + | Return => Return + end. + +Definition exec_instr_prop + (sp: val) (b1: block) (ls1: locset) (m1: mem) + (b2: block) (ls2: locset) (m2: mem) : Prop := + forall f, + exec_instr tge sp (tunnel_block f b1) ls1 m1 + (tunnel_block f b2) ls2 m2. + +Definition exec_instrs_prop + (sp: val) (b1: block) (ls1: locset) (m1: mem) + (b2: block) (ls2: locset) (m2: mem) : Prop := + forall f, + exec_instrs tge sp (tunnel_block f b1) ls1 m1 + (tunnel_block f b2) ls2 m2. + +Definition exec_block_prop + (sp: val) (b1: block) (ls1: locset) (m1: mem) + (out: outcome) (ls2: locset) (m2: mem) : Prop := + forall f, + exec_block tge sp (tunnel_block f b1) ls1 m1 + (tunnel_outcome f out) ls2 m2. + +Definition tunneled_code (f: function) := + PTree.map (fun pc b => tunnel_block f b) (fn_code f). + +Definition exec_blocks_prop + (c: code) (sp: val) + (pc: node) (ls1: locset) (m1: mem) + (out: outcome) (ls2: locset) (m2: mem) : Prop := + forall f, + f.(fn_code) = c -> + exec_blocks tge (tunneled_code f) sp + (branch_target f pc) ls1 m1 + (tunnel_outcome f out) ls2 m2. + +Definition exec_function_prop + (f: function) (ls1: locset) (m1: mem) + (ls2: locset) (m2: mem) : Prop := + exec_function tge (tunnel_function f) ls1 m1 ls2 m2. + +Scheme exec_instr_ind5 := Minimality for LTL.exec_instr Sort Prop + with exec_instrs_ind5 := Minimality for LTL.exec_instrs Sort Prop + with exec_block_ind5 := Minimality for LTL.exec_block Sort Prop + with exec_blocks_ind5 := Minimality for LTL.exec_blocks Sort Prop + with exec_function_ind5 := Minimality for LTL.exec_function Sort Prop. + +(** The proof of semantic preservation is a structural induction + over the LTL evaluation derivation of the original program, + using the [exec_*_prop] predicates above as induction hypotheses. *) + +Lemma tunnel_function_correct: + forall f ls1 m1 ls2 m2, + exec_function ge f ls1 m1 ls2 m2 -> + exec_function_prop f ls1 m1 ls2 m2. +Proof. + apply (exec_function_ind5 ge + exec_instr_prop + exec_instrs_prop + exec_block_prop + exec_blocks_prop + exec_function_prop); + intros; red; intros; simpl. + (* getstack *) + constructor. + (* setstack *) + constructor. + (* op *) + constructor. rewrite <- H. apply eval_operation_preserved. + exact symbols_preserved. + (* load *) + apply exec_Bload with a. rewrite <- H. + apply eval_addressing_preserved. exact symbols_preserved. + auto. + (* store *) + apply exec_Bstore with a. rewrite <- H. + apply eval_addressing_preserved. exact symbols_preserved. + auto. + (* call *) + apply exec_Bcall with (tunnel_function f). + generalize H; unfold find_function; destruct ros. + intro. apply functions_translated; auto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge i). + intro. apply function_ptr_translated; auto. congruence. + rewrite H0; reflexivity. + apply H2. + (* instr_refl *) + apply exec_refl. + (* instr_one *) + apply exec_one. apply H0. + (* instr_trans *) + apply exec_trans with (tunnel_block f b2) rs2 m2; auto. + (* goto *) + apply exec_Bgoto. red in H0. simpl in H0. apply H0. + (* cond, true *) + eapply exec_Bcond_true. red in H0. simpl in H0. apply H0. auto. + (* cond, false *) + eapply exec_Bcond_false. red in H0. simpl in H0. apply H0. auto. + (* return *) + apply exec_Breturn. red in H0. simpl in H0. apply H0. + (* block_refl *) + apply exec_blocks_refl. + (* block_one *) + red in H1. + elim (branch_target_characterization f pc). + intro. rewrite H3. apply exec_blocks_one with (tunnel_block f b). + unfold tunneled_code. rewrite PTree.gmap. rewrite H2; rewrite H. + reflexivity. apply H1. + intros [pc' [ATpc BTS]]. + assert (b = Bgoto pc'). congruence. subst b. + generalize (exec_block_Bgoto_inv _ _ _ _ _ _ _ H0). + intros [A [B C]]. subst out; subst rs'; subst m'. + simpl. rewrite BTS. apply exec_blocks_refl. + (* blocks_trans *) + apply exec_blocks_trans with (branch_target f pc2) rs2 m2. + exact (H0 f H3). exact (H2 f H3). + (* function *) + econstructor. eexact H. + change (fn_code (tunnel_function f)) with (tunneled_code f). + simpl. + elim (branch_target_characterization f (fn_entrypoint f)). + intro BT. rewrite <- BT. exact (H1 f (refl_equal _)). + intros [pc [ATpc BT]]. + apply exec_blocks_trans with + (branch_target f (fn_entrypoint f)) (call_regs rs) m1. + eapply exec_blocks_one. + unfold tunneled_code. rewrite PTree.gmap. rewrite ATpc. + simpl. reflexivity. + apply exec_Bgoto. rewrite BT. apply exec_refl. + exact (H1 f (refl_equal _)). +Qed. + +End PRESERVATION. + +Theorem transf_program_correct: + forall (p: program) (r: val), + exec_program p r -> + exec_program (tunnel_program p) r. +Proof. + intros p r [b [f [ls [m [FIND1 [FIND2 [SIG [EX RES]]]]]]]]. + red. exists b; exists (tunnel_function f); exists ls; exists m. + split. change (prog_main (tunnel_program p)) with (prog_main p). + rewrite <- FIND1. apply symbols_preserved. + split. apply function_ptr_translated. assumption. + split. rewrite <- SIG. reflexivity. + split. apply tunnel_function_correct. + unfold tunnel_program. rewrite Genv.init_mem_transf. auto. + exact RES. +Qed. -- cgit v1.2.3