From f2059eb9fd40418a4957d278e42abecf22f171aa Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Mon, 21 Sep 2020 15:31:35 +0200 Subject: Proof of exec_body_simulation_plus Added exec_body_simulation_star' in order to prove it. exec_body_simulation_star' could also be used to prove exec_body_simulation_star directly (without using exec_body_simulation_plus). However, at least the way I did it the proof turns out to be longer. eexec_body_simulation_plus is still required/useful for exec_bblock_simulation. --- aarch64/Asmgenproof.v | 239 +++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 238 insertions(+), 1 deletion(-) (limited to 'aarch64') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index e656b199..2ee4d476 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -323,6 +323,29 @@ Proof. repeat (rewrite length_agree). repeat (rewrite Nat2Z.inj_add). reflexivity. Qed. +Lemma list_length_z_cons A hd (tl : list A): + list_length_z (hd :: tl) = list_length_z tl + 1. +Proof. + unfold list_length_z; simpl; rewrite list_length_add_acc; reflexivity. +Qed. + +Lemma header_size_lt_block_size bb: + list_length_z (header bb) < size bb. +Proof. + rewrite bblock_size_aux. + generalize (bblock_non_empty bb); intros NEMPTY; destruct NEMPTY as [HDR|EXIT]. + - destruct (body bb); try contradiction; rewrite list_length_z_cons; + repeat rewrite length_agree; omega. + - destruct (exit bb); try contradiction; simpl; repeat rewrite length_agree; omega. +Qed. + +Lemma body_size_le_block_size bb: + list_length_z (body bb) <= size bb. +Proof. + rewrite bblock_size_aux; repeat rewrite length_agree; omega. +Qed. + + Lemma bblock_size_pos bb: size bb >= 1. Proof. rewrite (bblock_size_aux bb). @@ -955,6 +978,135 @@ Lemma exec_basic_simulation: rs2 m2 = Next rs2' m2' /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). Admitted. + +Lemma exec_body_simulation_star': forall + b ofs f bb tc bis end_of_body rs_start m_start s_start rs_end m_end + (ATPC: rs_start PC = Vptr b ofs) + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (MATCHI: match_internal (end_of_body - list_length_z bis) (State rs_start m_start) s_start) + (BOUNDED: 0 <= Ptrofs.unsigned ofs + end_of_body <= Ptrofs.max_unsigned + /\ list_length_z bis <= end_of_body) + (UNFOLD: unfold (fn_blocks f) = OK tc) + (FINDBI: forall n : nat, (n < length bis)%nat -> + exists (i : Asm.instruction) (bi : basic), + list_nth_z bis (Z.of_nat n) = Some bi + /\ basic_to_instruction bi = OK i + /\ Asm.find_instr (Ptrofs.unsigned ofs + end_of_body - (list_length_z bis) + Z.of_nat n) tc = Some i) + (BODY: exec_body lk ge bis rs_start m_start = Next rs_end m_end), + exists s_end, star Asm.step tge s_start E0 s_end + /\ match_internal end_of_body (State rs_end m_end) s_end. +Proof. + induction bis as [| bi_next bis IH]. + - intros; eexists; split. + + apply star_refl. + + inv BODY; + unfold list_length_z in MATCHI; simpl in MATCHI; rewrite Z.sub_0_r in MATCHI; + assumption. + - intros. + exploit internal_functions_unfold; eauto. + intros (x & FINDtf & TRANStf & _). + assert (x = tc) by congruence; subst x. + + assert (FINDBI' := FINDBI). + specialize (FINDBI' 0%nat). + destruct FINDBI' as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))); try (simpl; omega). + inversion NTHBI; subst bi_next'. + simpl in BODY; destruct exec_basic as [s_next|] eqn:BASIC; try discriminate. + + destruct s_next as (rs_next & m_next); simpl in BODY. + destruct s_start as (rs_start' & m_start'). + 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 [? ? ? ? ? M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT OFS_NEXT RS RS']; subst. + rewrite ATPC in AGPC; symmetry in AGPC, ATPC_NEXT. + + inversion MATCHI as [? ? ? ? ? M_AGREE RS_AGREE ATPC' OFS RS RS']; subst. + symmetry in ATPC'. unfold list_length_z in ATPC'. + simpl in ATPC'. rewrite list_length_add_acc in ATPC'. + rewrite ATPC in ATPC'. + unfold Val.offset_ptr in ATPC'. + simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR. + unfold list_length_z in FIND_INSTR; simpl in FIND_INSTR. + rewrite list_length_add_acc in FIND_INSTR. + + destruct BOUNDED as [(? & LT_MAX) LT_END_OF_BODY]. + assert (list_length_z bis < end_of_body). + { unfold list_length_z in LT_END_OF_BODY; simpl in LT_END_OF_BODY; + rewrite list_length_add_acc 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 |} + i_next rs_start' m_start'); eauto. + { unfold Ptrofs.add; repeat (rewrite Ptrofs.unsigned_repr); + try (split; try omega; rewrite length_agree; omega). + rewrite Z.add_sub_assoc; assumption. } + intros STEP_NEXT. + + unfold list_length_z in MI_NEXT; simpl in MI_NEXT. + rewrite list_length_add_acc in MI_NEXT. + (* XXX use better tactics *) + replace (end_of_body - (list_length_z bis + 1) + 1) + with (end_of_body - list_length_z bis) in MI_NEXT by omega. + assert (0 <= Ptrofs.unsigned ofs + end_of_body <= Ptrofs.max_unsigned + /\ list_length_z bis <= end_of_body). { split; omega. } + exploit IH; eauto. + { (* XXX *) + intros n NLT. + assert (NLT': (n + 1 < length (bi_next :: bis))%nat). { simpl; omega. } + specialize (FINDBI (n + 1)%nat NLT'). + unfold list_length_z in FINDBI. simpl in FINDBI. rewrite list_length_add_acc in FINDBI. + destruct zeq as [e|]. { rewrite Nat2Z.inj_add in e. simpl in e. omega. } + unfold list_length_z in FINDBI. simpl in FINDBI. rewrite list_length_add_acc in FINDBI. + rewrite Nat2Z.inj_add in FINDBI; simpl in FINDBI. rewrite Z.add_0_r in FINDBI. + replace (Ptrofs.unsigned ofs + end_of_body - (list_length_z bis + 1) + (Z.of_nat n + 1)) + with (Ptrofs.unsigned ofs + end_of_body - list_length_z bis + Z.of_nat n) in FINDBI by omega. + replace (Z.pred (Z.of_nat n + 1)) with (Z.of_nat n) in FINDBI by omega. + assumption. } + intros IH'. + destruct IH' as (? & STEP_REST & MATCH_REST). + + eexists; split. + + eapply star_step; eauto. + + info_auto. +Qed. + +Lemma find_basic_instructions b ofs f bb tc: forall + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (UNFOLD: unfold (fn_blocks f) = OK tc), + forall n, + (n < length (body bb))%nat -> + exists (i : Asm.instruction) (bi : basic), + list_nth_z (body bb) (Z.of_nat n) = Some bi + /\ basic_to_instruction bi = OK i + /\ Asm.find_instr (Ptrofs.unsigned ofs + + (list_length_z (header bb)) + + Z.of_nat n) tc + = Some i. +Proof. + intros until n; intros NLT. + exploit internal_functions_unfold; eauto. + intros (tc' & FINDtf & TRANStf & _). + assert (tc' = tc) by congruence; subst. + exploit (find_instr_bblock (list_length_z (header bb) + Z.of_nat n)); eauto. + { unfold size; split. + - rewrite length_agree; omega. + - repeat (rewrite length_agree). repeat (rewrite Nat2Z.inj_add). omega. } + intros (i & NTH & FIND_INSTR). + exists i; intros. + inv NTH. + - (* absurd *) apply list_nth_z_range in H; omega. + - exists bi; + rewrite Z.add_simpl_l in H; + rewrite Z.add_assoc in FIND_INSTR; + intuition. + - (* absurd *) rewrite bblock_size_aux in H0; + rewrite H in H0; simpl in H0; repeat rewrite length_agree in H0; omega. +Qed. + Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall (ATPC: rs PC = Vptr b ofs) (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) @@ -964,7 +1116,92 @@ Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall (BODY: exec_body lk ge (body bb) rs m = Next 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'. -Admitted. +Proof. + intros. + exploit internal_functions_unfold; eauto. + intros (tc & FINDtf & TRANStf & _). + + (* Prove an Asm.step given that body bb is not empty *) + + destruct (body bb) as [| bi bis] eqn:BDY; try contradiction. + assert (H: (0 < length (body bb))%nat). { rewrite BDY; simpl; omega. } + exploit find_basic_instructions; eauto. clear H. rewrite BDY; intros FINDBI. + destruct FINDBI as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))). + inversion NTHBI; subst bi_next'. + simpl in BODY. destruct exec_basic as [s_next|] eqn:BASIC; try discriminate. + + destruct s_next as (rs_next & m_next); simpl in BODY. + destruct s2 as (rs_start' & m_start'). + 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']. + subst A. subst B. subst C. subst D. subst E. + rewrite ATPC in AGPC. symmetry in AGPC, ATPC_NEXT. + + inv MATCHI. symmetry in AGPC0. + unfold list_length_z in AGPC0. + simpl in AGPC0. rewrite list_length_add_acc in AGPC0. + rewrite ATPC in AGPC0. + unfold Val.offset_ptr in AGPC0. + simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR. + unfold list_length_z in FIND_INSTR; simpl in FIND_INSTR. + rewrite list_length_add_acc in FIND_INSTR. + rewrite Z.add_0_r in FIND_INSTR. + rewrite Z.add_0_r in AGPC0. + + 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. + { unfold Ptrofs.add. repeat (rewrite Ptrofs.unsigned_repr); + try rewrite length_agree; try split; try omega. + simpl; rewrite <- length_agree; assumption. } + intros STEP_NEXT. + + (* Now, use exec_body_simulation_star' to go the rest of the way 0+ steps *) + rewrite AGPC in ATPC_NEXT. + unfold Val.offset_ptr in ATPC_NEXT. + unfold Ptrofs.add in ATPC_NEXT. + rewrite Ptrofs.unsigned_repr in ATPC_NEXT. 2: { rewrite length_agree; split; omega. } + + (* give omega more facts to work with *) + assert (list_length_z (header bb) + list_length_z (body bb) <= size bb). { + rewrite bblock_size_aux. omega. } + generalize (body_size_le_block_size bb). rewrite length_agree. intros. + assert (0 <= Ptrofs.unsigned ofs + (list_length_z (header bb) + list_length_z (body bb)) + <= Ptrofs.max_unsigned + /\ list_length_z bis <= list_length_z (header bb) + list_length_z (body bb)). + { split; try omega. split; try omega. + - rewrite length_agree in H0; repeat (rewrite length_agree); omega. + - rewrite BDY. rewrite list_length_z_cons; repeat rewrite length_agree; omega. } + + exploit (exec_body_simulation_star' b ofs + f bb tc bis (list_length_z (header bb) + list_length_z (body bb))); eauto. + - rewrite BDY. unfold list_length_z. simpl. + repeat (rewrite list_length_add_acc). repeat (rewrite Z.add_0_r). + rewrite Z.add_assoc. rewrite Z.add_sub_swap. rewrite Z.add_simpl_r. + apply MI_NEXT. + - rewrite Z.add_assoc. + intros n NBOUNDS. + rewrite BDY. + assert (NBOUNDS': (n + 1 < length (body bb))%nat). { rewrite BDY; simpl; omega. } + exploit find_basic_instructions; eauto. rewrite BDY; intros FINDBI. + simpl in FINDBI. destruct zeq as [e|]. { rewrite Nat2Z.inj_add in e; simpl in e; omega. } + rewrite Nat2Z.inj_add in FINDBI; simpl in FINDBI. + replace (Z.pred (Z.of_nat n + 1)) with (Z.of_nat n) in FINDBI by omega. + rewrite list_length_z_cons, Z.add_assoc, Z.add_sub_swap, Z.add_simpl_r. + replace (Ptrofs.unsigned ofs + list_length_z (header bb) + (Z.of_nat n + 1)) + with (Ptrofs.unsigned ofs + list_length_z (header bb) + 1 + Z.of_nat n) in FINDBI by omega. + assumption. + - intros (s_end & STAR_STEP & MI_STAR). + eexists s_end; split. + + eapply plus_left; eauto. + + rewrite bblock_size_aux, Z.add_simpl_r. assumption. +Qed. Lemma exec_body_simulation_star b ofs f bb rs m s2 rs' m': forall (ATPC: rs PC = Vptr b ofs) -- cgit