[Draft] some lemmas copied for undef_regs.

1 files changed, 73 insertions, 27 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 0ea37a38..82fd0220 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1952,6 +1952,53 @@ Proof.
   - intros; simpl in *. rewrite IHres2. rewrite IHres1. reflexivity.
 Qed.
 
+(*Unset Printing Notations.*)
+(*Lemma undef_map_preg_not_pc (l: list mreg): forall rs,*)
+  (*undef_regs (map preg_of l) rs PC = rs PC.*)
+(*Proof.*)
+  (*induction l.*)
+  (*- simpl; reflexivity.*)
+  (*- simpl.*)
+
+Lemma undef_regs_other:
+  forall r rl rs,
+  (forall r', In r' rl -> r <> r') ->
+  undef_regs rl rs r = rs r.
+Proof.
+  induction rl; simpl; intros. auto.
+  rewrite IHrl by auto. rewrite Pregmap.gso; auto.
+Qed.
+
+Fixpoint preg_notin (r: preg) (rl: list mreg) : Prop :=
+  match rl with
+  | nil => True
+  | r1 :: nil => r <> preg_of r1
+  | r1 :: rl => r <> preg_of r1 /\ preg_notin r rl
+  end.
+
+Remark preg_notin_charact:
+  forall r rl,
+  preg_notin r rl <-> (forall mr, In mr rl -> r <> preg_of mr).
+Proof.
+  induction rl; simpl; intros.
+  tauto.
+  destruct rl.
+  simpl. split. intros. intuition congruence. auto.
+  rewrite IHrl. split.
+  intros [A B]. intros. destruct H. congruence. auto.
+  auto.
+Qed.
+
+Lemma undef_regs_other_2:
+  forall r rl rs,
+  preg_notin r rl ->
+  undef_regs (map preg_of rl) rs r = rs r.
+Proof.
+  intros. apply undef_regs_other. intros.
+  exploit list_in_map_inv; eauto. intros [mr [A B]]. subst.
+  rewrite preg_notin_charact in H. auto.
+Qed.
+
 Lemma exec_exit_simulation_plus b ofs f bb s2 t rs m rs' m': forall
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
   (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
@@ -2048,34 +2095,33 @@ Proof.
               erewrite !set_builtin_map_not_pc. rewrite HPC.
               eapply set_builtin_res_dont_move_pc_gen; intros.
               eapply set_buitin_res_sym; eauto.
-        (*-- simpl.*)
-           (*assert (HPC': Val.offset_ptr (set_res (map_builtin_res DR res)*)
-                          (*vres (undef_regs (map preg_of l)*)
-                          (*rs # (preg_of m) <- Vundef) PC) (Ptrofs.repr (size bb))*)
-                      (*= Val.offset_ptr (set_res (map_builtin_res DR res)*)
-                          (*vres (undef_regs (map preg_of l)*)
-                          (*_rs # (preg_of m) <- Vundef) PC) Ptrofs.one).*)
-           (*{ rewrite !set_builtin_map_not_pc.*)
-             (*induction l.*)
-             (*++ simpl. update_x_access_r; try discriminate.*)
-             (*++ simpl.*)
-                (*assert (rs # (preg_of m) <- Vundef = _rs # (preg_of m) <- Vundef).*)
-                (*{ destruct (PregEq.eq PC (preg_of m)). rewrite <- e.*)
-                  (*{ unfold Pregmap.set; apply functional_extensionality; intros.*)
-                  (*destruct (PregEq.eq x PC); try rewrite AG; eauto. }*)
-                  (*{ unfold Pregmap.set; apply functional_extensionality; intros.*)
-                  (*destruct (PregEq.eq x PC); try rewrite AG; eauto }*)
-
-                (*rewrite (Pregmap.gso (i := PC) (j := (preg_of a)) Vundef (rs # (preg_of m) <- Vundef)).*)
-                (*rewrite IHl. update_x_access_r; try discriminate.*)
-
-   (*(Ptrofs.repr (size bb))*)
-           (*induction res.*)
-           (*++ erewrite !set_builtin_map_not_pc.*)
+        -- simpl.
+           assert (HPC': (undef_regs (map preg_of l)
+                         rs # (preg_of m) <- Vundef) PC = rs PC).
+           { erewrite undef_regs_other_2.
+             2: eapply preg_notin_charact; intros; discriminate.
+             erewrite Pregmap.gso; eauto; try discriminate. }
+
+
+             ++ simpl. update_x_access_r; try discriminate.
+             ++ simpl. 
+                assert (rs # (preg_of m) <- Vundef = _rs # (preg_of m) <- Vundef).
+                { destruct (PregEq.eq PC (preg_of m)). rewrite <- e.
+                  { unfold Pregmap.set; apply functional_extensionality; intros.
+                  destruct (PregEq.eq x PC); try rewrite AG; eauto. }
+                  { unfold Pregmap.set; apply functional_extensionality; intros.
+                  destruct (PregEq.eq x PC); try rewrite AG; eauto }
+
+                rewrite (Pregmap.gso (i := PC) (j := (preg_of a)) Vundef (rs # (preg_of m) <- Vundef)).
+                rewrite IHl. update_x_access_r; try discriminate.
+
+   (Ptrofs.repr (size bb))
+           induction res.
+           ++ erewrite !set_builtin_map_not_pc.
               
-              (*eapply set_builtin_res_dont_move_pc_gen.*)
-(*erewrite !set_builtin_map_not_pc.*)
-              (*update_x_access_r; try congruence.*)
+              eapply set_builtin_res_dont_move_pc_gen.
+erewrite !set_builtin_map_not_pc.
+              update_x_access_r; try congruence.