diff options
Diffstat (limited to 'powerpc/Asmgenproof.v')
| -rw-r--r-- | powerpc/Asmgenproof.v | 51 |
1 files changed, 32 insertions, 19 deletions
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index d653633c..85541118 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -69,7 +69,7 @@ Lemma transf_function_no_overflow: transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned. Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. - omega. + lia. Qed. Lemma exec_straight_exec: @@ -205,10 +205,13 @@ Remark loadind_label: forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> tail_nolabel k c. Proof. - unfold loadind, accessind; intros. set (ofs' := Ptrofs.to_int ofs) in *. + unfold loadind, accessind ; intros. + set (ofs' := Ptrofs.to_int ofs) in *. + set (ofs_mod := Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *. destruct ty; try discriminate; destruct (preg_of dst); try discriminate; destruct (Int.eq (high_s ofs') Int.zero); + destruct ofs_mod; TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. Qed. @@ -216,10 +219,13 @@ Remark storeind_label: forall base ofs ty src k c, storeind src base ofs ty k = OK c -> tail_nolabel k c. Proof. - unfold storeind, accessind; intros. set (ofs' := Ptrofs.to_int ofs) in *. + unfold storeind, accessind; + intros. set (ofs' := Ptrofs.to_int ofs) in *. + set (ofs_mod := Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *. destruct ty; try discriminate; destruct (preg_of src); try discriminate; destruct (Int.eq (high_s ofs') Int.zero); + destruct ofs_mod; TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. Qed. @@ -298,17 +304,22 @@ Qed. Remark transl_memory_access_label: forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - addr args temp k c, - transl_memory_access mk1 mk2 addr args temp k = OK c -> + unaligned addr args temp k c, + transl_memory_access mk1 mk2 unaligned addr args temp k = OK c -> (forall c r, nolabel (mk1 c r)) -> (forall r1 r2, nolabel (mk2 r1 r2)) -> tail_nolabel k c. Proof. - unfold transl_memory_access; intros; destruct addr; TailNoLabel. - destruct (Int.eq (high_s i) Int.zero); TailNoLabel. - destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. + unfold transl_memory_access, aindexed, aindexed2, aglobal, abased, ainstack; intros; destruct addr; TailNoLabel. + destruct (unaligned || Int.eq (Int.mods i (Int.repr 4)) Int.zero). destruct (Int.eq (high_s i) Int.zero); TailNoLabel. + eapply tail_nolabel_trans. apply loadimm_label. TailNoLabel. + destruct (symbol_is_small_data i i0). destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. + destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel. destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. + destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel. + destruct (unaligned || Int.eq (Int.mods (Ptrofs.to_int i) (Int.repr 4)) Int.zero). destruct (Int.eq (high_s (Ptrofs.to_int i)) Int.zero); TailNoLabel. + eapply tail_nolabel_trans. eapply addimm_label. TailNoLabel. Qed. Remark transl_epilogue_label: @@ -401,8 +412,8 @@ Proof. split. unfold goto_label. rewrite P. rewrite H1. auto. split. rewrite Pregmap.gss. constructor; auto. rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. - auto. omega. - generalize (transf_function_no_overflow _ _ H0). omega. + auto. lia. + generalize (transf_function_no_overflow _ _ H0). lia. intros. apply Pregmap.gso; auto. Qed. @@ -781,16 +792,18 @@ Opaque loadind. econstructor; eauto. instantiate (2 := tf); instantiate (1 := x). unfold nextinstr. rewrite Pregmap.gss. - rewrite set_res_other. rewrite undef_regs_other_2. + rewrite set_res_other. simpl. rewrite undef_regs_other_2. + rewrite Pregmap.gso by auto with asmgen. rewrite <- H1. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. rewrite preg_notin_charact. intros. auto with asmgen. auto with asmgen. apply agree_nextinstr. eapply agree_set_res; auto. - eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. + eapply agree_undef_regs; eauto. + intros. simpl. rewrite undef_regs_other_2; auto. apply Pregmap.gso. auto with asmgen. congruence. intros. Simpl. rewrite set_res_other by auto. - rewrite undef_regs_other_2; auto with asmgen. + simpl. rewrite undef_regs_other_2; auto with asmgen. - (* Mgoto *) assert (f0 = f) by congruence. subst f0. @@ -924,14 +937,14 @@ Local Transparent destroyed_by_jumptable. simpl const_low. rewrite ATLR. erewrite storev_offset_ptr by eexact P. auto. congruence. auto. auto. auto. left; exists (State rs5 m3'); split. - eapply exec_straight_steps_1; eauto. omega. constructor. + eapply exec_straight_steps_1; eauto. lia. constructor. econstructor; eauto. change (rs5 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one) Ptrofs.one). rewrite ATPC. simpl. constructor; eauto. - eapply code_tail_next_int. omega. - eapply code_tail_next_int. omega. - eapply code_tail_next_int. omega. - eapply code_tail_next_int. omega. + eapply code_tail_next_int. lia. + eapply code_tail_next_int. lia. + eapply code_tail_next_int. lia. + eapply code_tail_next_int. lia. constructor. unfold rs5, rs4, rs3, rs2. apply agree_nextinstr. apply agree_nextinstr. @@ -956,7 +969,7 @@ Local Transparent destroyed_by_jumptable. - (* return *) inv STACKS. simpl in *. - right. split. omega. split. auto. + right. split. lia. split. auto. rewrite <- ATPC in H5. econstructor; eauto. congruence. |