From e188b6c4a1c43fb83157670e1c28db5798f50f0b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 4 Sep 2019 22:58:55 +0200 Subject: going forward --- backend/CSEproof.v | 91 ++++++++++++++++++++++++++++++------------------------ 1 file changed, 50 insertions(+), 41 deletions(-) (limited to 'backend/CSEproof.v') diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 108aef31..50eb4637 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -72,8 +72,10 @@ Proof. intros. inv H; simpl in *. - constructor. 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: @@ -380,11 +382,11 @@ Proof. Qed. Lemma add_load_holds: - forall valu1 ge sp rs m n addr (args: list reg) a trap chunk v dst, + forall valu1 ge sp rs m n addr (args: list reg) a chunk v dst, numbering_holds valu1 ge sp rs m n -> eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> - exists valu2, numbering_holds valu2 ge sp (rs#dst <- v) m (add_load n dst trap chunk addr args). + exists valu2, numbering_holds valu2 ge sp (rs#dst <- v) m (add_load n dst chunk addr args). Proof. unfold add_load; intros. destruct (valnum_regs n args) as [n1 vl] eqn:VN. @@ -395,12 +397,12 @@ 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). + exists valu2, numbering_holds valu2 ge sp (rs#dst <- (default_notrap_load_value chunk)) m (add_load n dst chunk addr args). Proof. unfold add_load; intros. destruct (valnum_regs n args) as [n1 vl] eqn:VN. @@ -426,6 +428,7 @@ Proof. + 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, @@ -520,6 +523,7 @@ 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. @@ -532,6 +536,7 @@ 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. +*) Qed. Lemma store_normalized_range_sound: @@ -608,6 +613,7 @@ 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. @@ -619,6 +625,7 @@ Proof. 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: @@ -698,7 +705,7 @@ Lemma shift_memcpy_eq_holds: Proof with (try discriminate). intros. set (delta := dst - src) in *. unfold shift_memcpy_eq in H. destruct e as [l strict rhs] eqn:E. - destruct rhs as [op vl | trap chunk addr vl]... + destruct rhs as [op vl | chunk addr vl]... destruct addr... try (rename i into ofs). set (i1 := Ptrofs.unsigned ofs) in *. set (j := i1 + delta) in *. @@ -1091,44 +1098,14 @@ 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 trap 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. -- (* 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:?. + (* 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' = Vundef) by (inv EV; congruence). subst v'. + assert (v' = v) by (inv EV; congruence). subst v'. econstructor; split. eapply exec_Iop; eauto. simpl; eauto. econstructor; eauto. @@ -1154,9 +1131,41 @@ Proof. unfold transfer; rewrite H. eapply add_load_holds; eauto. apply set_reg_lessdef; auto. + } - (* TODO *) + (* NOTRAP *) + { + 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. + rewrite eval_addressing_preserved with (ge1 := ge). + exact Ha'1. + 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. + } +(* TODO *) + - (* Istore *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. destruct SAT as [valu1 NH1]. -- cgit