From b74f67544239f020ca02c527b6fc1abc137eea2d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sun, 20 Dec 2020 16:01:54 +0100 Subject: Fix Asmblockgenproof after merge --- aarch64/Asmblockgenproof.v | 28 ++++++++++++++++++++-------- 1 file 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. -- cgit