From eb1f11a5be18a36783a44f6c0ddddc35b90cc90a Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 9 Oct 2020 18:40:14 +0200 Subject: slight refactoring, in order to avoid a duplication of the proof. --- aarch64/Asmgenproof.v | 76 ++++++++++++++++++++++++--------------------------- 1 file changed, 36 insertions(+), 40 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 6b5b0913..530166c2 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1141,54 +1141,51 @@ Lemma exec_body_simulation_plus_alt li: forall b ofs f bb rs m s2 rs' m' exists s2', plus Asm.step tge s2 E0 s2' /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'. Proof. - induction li as [|a [|b]]; simpl. - - (* len(body bb) == 0 *) - congruence. - - (* len(body bb) == 1 *) - (* Contruct the MI hypothesis. *) - intros. rewrite <- BLI in *. simpl in *. - exploit internal_functions_unfold; eauto. - intros (tc & FINDtf & TRANStf & _). - assert (BDYLENPOS: (0 < length (body bb))%nat). { rewrite <- BLI; simpl; omega. } - exploit find_basic_instructions; eauto. - rewrite <- BLI; intros FINDBI. - destruct FINDBI as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))). - inversion NTHBI; subst bi_next'. - destruct (exec_basic _ _ _ _ _) eqn:EXEC_BASIC; next_stuck_cong. - inversion BODY. subst. - destruct s as (rs1 & m1); simpl in *. - destruct s2 as (rs2 & m2); simpl in *. - exploit exec_basic_simulation; eauto. - intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT). + induction li as [|a li]; simpl; try congruence. + intros; rewrite <- BLI in *. simpl in *. + assert (BDYLENPOS: (0 < length (body bb))%nat). { rewrite <- BLI; simpl; omega. } + exploit internal_functions_unfold; eauto. + intros (tc & FINDtf & TRANStf & _). + exploit find_basic_instructions; eauto. + rewrite <- BLI; intros FINDBI. + destruct FINDBI as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))). + inversion NTHBI; subst bi_next'. + destruct (exec_basic _ _ _ _ _) eqn:EXEC_BASIC; next_stuck_cong. + destruct s as (rs1 & m1); simpl in *. + destruct s2 as (rs2 & m2); simpl in *. + exploit exec_basic_simulation; eauto. + intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT). - (* Code from the star' lemma bellow. We need this to exploit exec_step_internal. *) - 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']. - subst A. subst B. subst C. subst D. subst E. - rewrite ATPC in AGPC. symmetry in AGPC, ATPC_NEXT. + (* Code from the star' lemma bellow. We need this to exploit exec_step_internal. *) + 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']. + subst A. subst B. subst C. subst D. subst E. + rewrite ATPC in AGPC. symmetry in AGPC, ATPC_NEXT. - inv MATCHI. symmetry in AGPC0. - rewrite ATPC in AGPC0. - unfold Val.offset_ptr in AGPC0. - simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR. + inv MATCHI. symmetry in AGPC0. + rewrite ATPC in AGPC0. + 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). - - (* Execute internal step. *) - exploit (Asm.exec_step_internal tge b (Ptrofs.add ofs (Ptrofs.repr ((list_length_z (header bb))))) + 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). + + (* Execute internal step. *) + 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 rs2 m2); eauto. { unfold Ptrofs.add. repeat (rewrite Ptrofs.unsigned_repr); try rewrite length_agree; try split; try omega. simpl; rewrite <- length_agree; assumption. } - (* This is our STEP hypothesis. *) - intros STEP_NEXT. - + (* This is our STEP hypothesis. *) + intros STEP_NEXT. + destruct li as [|a' li]; simpl in *. + - (* case of a single instruction: this our base case in the induction *) (* XXX New code --> no need to use the star' lemma this way. *) + inversion BODY; subst. eexists; split. + apply plus_one. eauto. + assert (BDYLEN: list_length_z (body bb) = 1). @@ -1197,8 +1194,7 @@ Proof. { rewrite bblock_size_aux. omega. } rewrite BDYLEN in LEN1. rewrite LEN1. apply MI_NEXT. - (* len(body bb) >= 1 *) - (* Comment factoriser le code pour éviter de répéter les étapes du ca précédent ? Utiliser une ltac serait trop lourd ? *) - + (* TODO: apply the induction hypothesis IHli *) Admitted. Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall -- cgit