From 10ae0441711eba798e852ca580c5895cb49576d9 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 13 Oct 2020 14:46:55 +0200 Subject: Fixing the propagation of the new BOUNDED hyp --- aarch64/Asmgenproof.v | 28 ++++++++++++++++++++-------- 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 35d30d06..a055bb42 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1087,6 +1087,7 @@ Proof. try (inversion MATCHI; subst; rewrite <- AG; try congruence); try (exploit next_inst_preserved; eauto); try (destruct_reg_size). + + all:admit. all:admit. @@ -1135,6 +1136,15 @@ Proof. destruct s_next as (rs_next & m_next); simpl in BODY. destruct s_start as (rs_start' & m_start'). + + destruct BOUNDED as [(LT_MIN & LT_MAX) LT_END_OF_BODY]. + assert (LT_END_OF_BODY_BIS: list_length_z bis < end_of_body) + by (rewrite list_length_z_cons in LT_END_OF_BODY; omega). + generalize (Ptrofs.unsigned_range_2 ofs); intros LT_OFS_MAXU. + + assert (list_length_z (bi_next :: bis) >= 0) by eapply list_length_z_pos. + assert (BOUNDED_BIS: 0 <= end_of_body - list_length_z (bi_next :: bis) <= Ptrofs.max_unsigned) by omega. + exploit exec_basic_simulation; eauto. intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT). exploit exec_basic_dont_move_PC; eauto; intros AGPC. @@ -1148,10 +1158,6 @@ Proof. simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR. rewrite list_length_z_cons in FIND_INSTR. - destruct BOUNDED as [(? & LT_MAX) LT_END_OF_BODY]. - assert (list_length_z bis < end_of_body) - by (rewrite list_length_z_cons in LT_END_OF_BODY; omega). - generalize (Ptrofs.unsigned_range_2 ofs); intros. exploit (Asm.exec_step_internal tge b (Ptrofs.add ofs (Ptrofs.repr (end_of_body - (list_length_z bis + 1)))) {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |} @@ -1325,7 +1331,17 @@ Proof. destruct s_next as (rs_next & m_next); simpl in BODY. destruct s2 as (rs_start' & m_start'). + + assert (list_length_z (header bb) >= 0) by eapply list_length_z_pos. + assert (LT_OFS_BB_MAXU: Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned) + by (eapply size_of_blocks_bounds; eauto). + generalize (header_size_lt_block_size bb). rewrite length_agree; intros HEADER_LT. + generalize (Ptrofs.unsigned_range_2 ofs). intros (LT_MIN & LT_MAX). + assert (list_length_z (header bb) <= Ptrofs.max_unsigned). + { rewrite length_agree; omega. } + assert (BOUNDED: 0 <= list_length_z (header bb) <= Ptrofs.max_unsigned) by omega. exploit exec_basic_simulation; eauto. + intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT). exploit exec_basic_dont_move_PC; eauto. intros AGPC. inversion MI_NEXT as [A B C D E M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT PC_OFS_NEXT RS RS']. @@ -1337,10 +1353,6 @@ Proof. unfold Val.offset_ptr in AGPC0. simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR. - assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned) - by (eapply size_of_blocks_bounds; eauto). - generalize (header_size_lt_block_size bb). rewrite length_agree; intros HEADER_LT. - generalize (Ptrofs.unsigned_range_2 ofs). intros (A & B). exploit (Asm.exec_step_internal tge b (Ptrofs.add ofs (Ptrofs.repr ((list_length_z (header bb))))) {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |} i_next rs_start' m_start'); eauto. -- cgit