From 4b119d6f9f0e846edccaf5c08788ca1615b22526 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 16 Aug 2009 15:35:09 +0000 Subject: 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 --- arm/Constprop.v | 19 ++----------------- arm/Constpropproof.v | 37 +++++++++++++++++-------------------- 2 files changed, 19 insertions(+), 37 deletions(-) (limited to 'arm') diff --git a/arm/Constprop.v b/arm/Constprop.v index 5bd84b6d..154a5fc1 100644 --- a/arm/Constprop.v +++ b/arm/Constprop.v @@ -702,7 +702,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 @@ -1219,19 +1219,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 @@ -1239,9 +1226,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/arm/Constpropproof.v b/arm/Constpropproof.v index 08c5baf3..a3e2b82b 100644 --- a/arm/Constpropproof.v +++ b/arm/Constpropproof.v @@ -213,19 +213,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. @@ -235,7 +235,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. @@ -772,7 +772,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 *) @@ -796,7 +796,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. @@ -814,8 +814,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. @@ -831,8 +830,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 *) @@ -842,8 +840,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. @@ -852,7 +849,7 @@ Proof. TransfInstr; intro. econstructor; split. eapply exec_Itailcall; eauto. apply sig_function_translated; auto. - constructor; auto. + constructor; auto. (* Icond, true *) exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. @@ -870,8 +867,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 *) @@ -890,8 +887,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 *) -- cgit