begin CSE proof for notrap load

1 files changed, 85 insertions, 3 deletions

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 *)