diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/Constprop.v | 19 | ||||
-rw-r--r-- | powerpc/Constpropproof.v | 35 |
2 files changed, 18 insertions, 36 deletions
diff --git a/powerpc/Constprop.v b/powerpc/Constprop.v index 76ea153c..109125c3 100644 --- a/powerpc/Constprop.v +++ b/powerpc/Constprop.v @@ -674,7 +674,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 @@ -1062,19 +1062,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 @@ -1082,9 +1069,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/powerpc/Constpropproof.v b/powerpc/Constpropproof.v index fb01f75b..6e17f307 100644 --- a/powerpc/Constpropproof.v +++ b/powerpc/Constpropproof.v @@ -219,19 +219,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. @@ -241,7 +241,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. @@ -756,7 +756,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 *) @@ -780,7 +780,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. @@ -798,8 +798,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. @@ -815,8 +814,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 *) @@ -826,8 +824,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. @@ -854,8 +851,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 *) @@ -874,8 +871,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 *) |