From 44f4bea5d16273b834b1bcc8624c8f00aefaf018 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 4 Sep 2019 10:23:03 +0200 Subject: begin CSE proof for notrap load --- backend/CSEproof.v | 88 ++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 85 insertions(+), 3 deletions(-) (limited to 'backend/CSEproof.v') diff --git a/backend/CSEproof.v b/backend/CSEproof.v index c0464ab8..def8003c 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -71,7 +71,9 @@ 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 +395,38 @@ 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 <- (default_notrap_load_value chunk)) 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_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 <- (default_notrap_load_value chunk)) 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 +490,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 +520,18 @@ 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 +608,8 @@ Proof. unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. auto. + +(* TODO *) Qed. Lemma load_memcpy: @@ -1064,6 +1112,40 @@ Proof. eapply add_load_holds; eauto. apply set_reg_lessdef; auto. +- (* Iload notrap1 *) + 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 NOTRAP chunk addr vl)) as [r|] eqn:?. ++ (* replaced by move *) + exploit find_rhs_sound; eauto. intros (v' & EV & LD). + assert (v' = Vundef) 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. + (* TODO *) - (* Istore *) -- cgit