Fix Asmblockgenproof after merge

1 files changed, 20 insertions, 8 deletions

diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index 0b1123f7..6f7d39fa 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -682,6 +682,19 @@ Proof.
   intros. destruct (PregEq.eq r X16); [ rewrite e in H; simpl in H; discriminate | auto ].
 Qed.
 
+Lemma undef_regs_other_2':
+  forall r rl rs,
+  data_preg r = true ->
+  preg_notin r rl ->
+  undef_regs (DR (IR X16) :: DR (IR X30) :: map preg_of rl) rs r = rs r.
+Proof.
+  intros. apply undef_regs_other. intros. simpl in H1.
+  destruct H1 as [HX16 | [HX30 | HDES]]; subst.
+  apply X16_not_data_preg; auto. apply X30_not_data_preg; auto.
+  exploit list_in_map_inv; eauto. intros [mr [A B]]. subst.
+  rewrite preg_notin_charact in H0. auto.
+Qed.
+
 Ltac Simpl :=
   rewrite Pregmap.gso; try apply PC_not_data_preg; try apply X30_not_data_preg.
   
@@ -821,10 +834,12 @@ Proof.
       eapply external_call_symbols_preserved; eauto. apply senv_preserved. eauto.
       econstructor; eauto.
       unfold incrPC. rewrite Pregmap.gss.
-      rewrite set_res_other. rewrite undef_regs_other_2. unfold Val.offset_ptr. rewrite PCeq.
-      eauto. rewrite preg_notin_charact. intros. auto with asmgen.
+      rewrite set_res_other. rewrite undef_regs_other. unfold Val.offset_ptr. rewrite PCeq.
+      eauto. 
+      intros; simpl in *; destruct H as [HX16 | [HX30 | HDES]]; subst; try discriminate;
+      exploit list_in_map_inv; eauto; intros [mr [E F]]; subst; discriminate.
       auto with asmgen. apply agree_nextblock. eapply agree_set_res; auto.
-      eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
+      eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2'; auto.
       intros. discriminate.
     + (* MBgoto *)
       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
@@ -919,7 +934,7 @@ Proof.
       monadInv H1. monadInv EQ.
       generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV.
       assert (f1 = f) by congruence. subst f1.
-      exploit find_label_goto_label. 4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs2) # X16 <- Vundef # X17 <- Vundef).
+      exploit find_label_goto_label. 4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs2) # X16 <- Vundef).
         unfold incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity. discriminate.
       exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn.
 
@@ -931,10 +946,7 @@ Proof.
         simpl. unfold Mach.label in H12. unfold label. rewrite H12. eapply A.
       econstructor; eauto.
         eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen.
-        { unfold incrPC. repeat Simpl; auto. assert (destroyed_by_jumptable = R17 :: nil) by auto.
-          rewrite H2 in H0. simpl in H0. destruct r'; try discriminate.
-          destruct d; try discriminate. destruct i; try discriminate.
-          destruct r; try discriminate. }
+        { unfold incrPC. repeat Simpl; auto. apply X16_not_data_preg; auto. }
         discriminate.
     + (* MBreturn *)
       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.