diff options
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 221 |
1 files changed, 188 insertions, 33 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index a2a1b461..72b52375 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -71,7 +71,11 @@ Lemma rhs_eval_to_exten: Proof. intros. inv H; simpl in *. - constructor. rewrite valnums_val_exten by assumption. auto. -- econstructor; eauto. rewrite valnums_val_exten by assumption. auto. +- eapply load_eval_to; eauto. rewrite valnums_val_exten by assumption. auto. +(* +- apply load_notrap1_eval_to; auto. rewrite valnums_val_exten by assumption. assumption. +- eapply load_notrap2_eval_to; eauto. rewrite valnums_val_exten by assumption. assumption. +*) Qed. Lemma equation_holds_exten: @@ -393,6 +397,39 @@ Proof. + intros. apply Regmap.gso; auto. Qed. +(* +Lemma add_load_holds_none1: + forall valu1 ge sp rs m n addr (args: list reg) chunk dst, + numbering_holds valu1 ge sp rs m n -> + eval_addressing ge sp addr rs##args = None -> + exists valu2, numbering_holds valu2 ge sp (rs#dst <- Vundef) m (add_load n dst chunk addr args). +Proof. + unfold add_load; intros. + destruct (valnum_regs n args) as [n1 vl] eqn:VN. + exploit valnum_regs_holds; eauto. + intros (valu2 & A & B & C & D & E). + eapply add_rhs_holds; eauto. ++ rewrite Regmap.gss; auto. eapply load_notrap1_eval_to. rewrite <- B; eauto. ++ intros. apply Regmap.gso; auto. +Qed. + +Lemma add_load_holds_none2: + forall valu1 ge sp rs m n addr (args: list reg) a chunk dst, + numbering_holds valu1 ge sp rs m n -> + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = None -> + exists valu2, numbering_holds valu2 ge sp (rs#dst <- Vundef) m (add_load n dst NOTRAP chunk addr args). +Proof. + unfold add_load; intros. + destruct (valnum_regs n args) as [n1 vl] eqn:VN. + exploit valnum_regs_holds; eauto. + intros (valu2 & A & B & C & D & E). + eapply add_rhs_holds; eauto. ++ rewrite Regmap.gss; auto. eapply load_notrap2_eval_to. rewrite <- B; eauto. assumption. ++ intros. apply Regmap.gso; auto. +Qed. + *) + Lemma set_unknown_holds: forall valu ge sp rs m n r v, numbering_holds valu ge sp rs m n -> @@ -456,8 +493,8 @@ Lemma kill_all_loads_hold: Proof. intros. eapply kill_equations_hold; eauto. unfold filter_loads; intros. inv H1. - constructor. rewrite <- H2. apply op_depends_on_memory_correct; auto. - discriminate. + 1: constructor; rewrite <- H2; apply op_depends_on_memory_correct; auto. + all: discriminate. Qed. Lemma kill_loads_after_store_holds: @@ -486,6 +523,20 @@ Proof. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va. +(* +- eapply load_notrap1_eval_to; assumption. +- destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate. + eapply load_notrap2_eval_to; eauto. + rewrite <- H9. + destruct a; simpl in H1; try discriminate. + destruct a0; simpl in H9; try discriminate; simpl; trivial. + rewrite negb_false_iff in H6. unfold aaddressing in H6. + eapply Mem.load_store_other. eauto. + eapply pdisjoint_sound; eauto. + apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. + erewrite <- regs_valnums_sound by eauto. eauto with va. + apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va. +*) Qed. Lemma store_normalized_range_sound: @@ -562,6 +613,19 @@ Proof. unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. auto. +(* +- eapply load_notrap1_eval_to; assumption. +- destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate. + eapply load_notrap2_eval_to; eauto. rewrite <- H11. + destruct a; simpl in H10; try discriminate; simpl; trivial. + rewrite negb_false_iff in H8. + eapply Mem.load_storebytes_other. eauto. + rewrite H6. rewrite Z2Nat.id by lia. + eapply pdisjoint_sound. eauto. + unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. + erewrite <- regs_valnums_sound by eauto. eauto with va. + auto. +*) Qed. Lemma load_memcpy: @@ -1034,36 +1098,126 @@ Proof. destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. destruct SAT as [valu1 NH1]. exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). - destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?. -+ (* replaced by move *) - exploit find_rhs_sound; eauto. intros (v' & EV & LD). - assert (v' = v) by (inv EV; congruence). subst v'. - econstructor; split. - eapply exec_Iop; eauto. simpl; eauto. - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - eapply add_load_holds; eauto. - apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. -+ (* load is preserved, but addressing is possibly simplified *) - destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?. - assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). - { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. - intros; eapply combine_addr_sound; eauto. } - exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR. - intros [a' [A B]]. - assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a'). - { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. } - exploit Mem.loadv_extends; eauto. - intros [v' [X Y]]. - econstructor; split. - eapply exec_Iload; eauto. - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - eapply add_load_holds; eauto. - apply set_reg_lessdef; auto. - + destruct trap; inv H0. + + + (* TRAP *) + { destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?. + * (* replaced by move *) + exploit find_rhs_sound; eauto. intros (v' & EV & LD). + assert (v' = v) by (inv EV; congruence). subst v'. + econstructor; split. + eapply exec_Iop; eauto. simpl; eauto. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + eapply add_load_holds; eauto. + apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. + * (* load is preserved, but addressing is possibly simplified *) + destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?. + assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). + { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. + intros; eapply combine_addr_sound; eauto. } + exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR. + intros [a' [A B]]. + assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a'). + { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. } + exploit Mem.loadv_extends; eauto. + intros [v' [X Y]]. + econstructor; split. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + eapply add_load_holds; eauto. + apply set_reg_lessdef; auto. } + + + (* NOTRAP1 *) + { assert (exists a' : val, + eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a') + as Haa'. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + destruct Haa' as [a' [Ha'1 Ha'2]]. + + assert ( + exists v' : val, + Mem.loadv chunk m' a' = Some v' /\ Val.lessdef v v') as Hload' by + (apply Mem.loadv_extends with (m1 := m) (addr1 := a); assumption). + destruct Hload' as [v' [Hv'1 Hv'2]]. + + econstructor. split. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + apply set_reg_lessdef; assumption. + } + + + (* NOTRAP2 *) + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + assert (exists a' : val, + eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef v a') + as Haa'. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + destruct Haa' as [a' [Ha'1 Ha'2]]. + + destruct (Mem.loadv chunk m' a') eqn:Hload'. + + { + econstructor. split. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + apply set_reg_lessdef; eauto. + } + { + econstructor. split. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + try (intros a EVAL'; + rewrite eval_addressing_preserved with (ge1 := ge) in EVAL'; [| exact symbols_preserved]; + inv Ha'2; rewrite Ha'1 in EVAL'; inv EVAL'; auto). + + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + apply set_reg_lessdef. + constructor. assumption. + } + * econstructor. split. + -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + rewrite eval_addressing_preserved with (ge1 := ge). + intros a EVAL'. eapply eval_addressing_lessdef_none with (vl1 := rs ## args) in EVAL. + erewrite EVAL in EVAL'. congruence. + apply regs_lessdef_regs; assumption. + exact symbols_preserved. + + -- econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + apply set_reg_lessdef. + constructor. assumption. + - (* Istore *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. destruct SAT as [valu1 NH1]. @@ -1154,6 +1308,7 @@ Proof. + apply CASE2; inv H1; auto. + apply CASE1. + apply CASE2; inv H1; auto. + + apply CASE2; inv H1; auto. * apply set_res_lessdef; auto. - (* Icond *) |