From bd649765a6833fee9daa8df88a8e5fd2e916cdd4 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 16 Oct 2020 22:42:00 +0200 Subject: Pb, Pbc, and nextinst incrPC preserved lemma --- aarch64/Asmgenproof.v | 120 +++++++++++++++++++++++++++++++++----------------- 1 file changed, 79 insertions(+), 41 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 895e354a..c89a4320 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1620,6 +1620,72 @@ Proof. exploit list_nth_z_range; eauto. omega. Qed. +Lemma basic_block_header_length: forall bb, + (length (header bb) <= 1)%nat. +Proof. +Admitted. + +Lemma label_pos_preserved f lbl z tf: forall + (FINDF: transf_function f = OK tf), + label_pos lbl z (fn_blocks f) = Asm.label_pos lbl z (Asm.fn_code tf). +Proof. +Admitted. + +Lemma goto_label_preserved bb rs1 m1 rs1' m1' rs2 m2 lbl f tf v: forall + (FINDF: transf_function f = OK tf) + (BOUNDED: size bb <= Ptrofs.max_unsigned) + (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2)) + (HGOTO: goto_label f lbl (incrPC v rs1) m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.goto_label tf lbl rs2 m2 = Next rs2' m2' + /\ match_states (State rs1' m1') (State rs2' m2'). +Proof. + intros. + unfold goto_label, Asm.goto_label in *. + rewrite <- (label_pos_preserved f); auto. + inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. + destruct label_pos; next_stuck_cong. + destruct (incrPC v rs1 PC) eqn:INCRPC; next_stuck_cong. + inversion HGOTO; auto. repeat (econstructor; eauto). + rewrite <- EQPC. + unfold incrPC in *. + rewrite !Pregmap.gss in *. + destruct (rs1 PC) eqn:EQRS1; simpl in *; try congruence. + replace (rs2 # PC <- (Vptr b0 (Ptrofs.repr z))) with ((rs1 # PC <- (Vptr b0 (Ptrofs.add i0 v))) # PC <- (Vptr b (Ptrofs.repr z))); auto. + eapply functional_extensionality. intros. + destruct (PregEq.eq x PC); subst. + rewrite !Pregmap.gss. congruence. + rewrite !Pregmap.gso; auto. +Qed. + +Lemma next_inst_incr_pc_preserved bb rs1 m1 rs1' m1' rs2 m2 f tf: forall + (FINDF: transf_function f = OK tf) + (BOUNDED: size bb <= Ptrofs.max_unsigned) + (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2)) + (NEXT: Next (incrPC (Ptrofs.repr (size bb)) rs1) m2 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), + Next (Asm.nextinstr rs2) m2 = Next rs2' m2' + /\ match_states (State rs1' m1') (State rs2' m2'). +Proof. + intros; simpl in *; unfold incrPC in NEXT; + inv_matchi; + assert (size bb >= 1) by eapply bblock_size_pos; + assert (0 <= size bb - 1 <= Ptrofs.max_unsigned) by omega; + inversion NEXT; subst; + eexists; eexists; split; eauto. + assert (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb))) = Asm.nextinstr rs2). { + unfold Pregmap.set. apply functional_extensionality. + intros x. destruct (PregEq.eq x PC). + -- unfold Asm.nextinstr. rewrite <- AGPC. + rewrite Val.offset_ptr_assoc. rewrite Ptrofs.add_unsigned. + rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega. + rewrite Ptrofs.unsigned_one. + replace (size bb - 1 + 1) with (size bb) by omega. + rewrite e. rewrite Pregmap.gss. + reflexivity. + -- eapply nextinstr_agree_but_pc; eauto. } + rewrite H1. econstructor. +Qed. + Lemma exec_cfi_simulation: forall bb f tf rs1 m1 rs1' m1' rs2 m2 cfi (SIZE: size bb <= Ptrofs.max_unsigned) @@ -1634,10 +1700,19 @@ Proof. intros. destruct cfi; inv CFI; simpl. - (* Pb *) - (*eexists; eexists; split.*) - (*eauto.*) - admit. - - (* Pbc *) admit. + exploit goto_label_preserved; eauto. + - (* Pbc *) + inv_matchi. + unfold eval_testcond in *. destruct c; + erewrite !incrPC_agree_but_pc in H0; try rewrite <- !AG; try congruence. + all: + destruct_reg_size; + try destruct b eqn:EQB. + 1,4,7,10,13,16,19,22,25,28,31,34: + exploit goto_label_preserved; eauto. + 1,3,5,7,9,11,13,15,17,19,21,23: + exploit next_inst_incr_pc_preserved; eauto. + all: repeat (econstructor; eauto). - (* Pbl *) eexists; eexists; split. + eauto. @@ -1774,43 +1849,6 @@ Proof. *) Admitted. -Lemma basic_block_header_length: forall bb, - (length (header bb) <= 1)%nat. -Proof. -Admitted. - -Lemma label_pos_preserved f lbl z tf: forall - (FINDF: transf_function f = OK tf), - label_pos lbl z (fn_blocks f) = Asm.label_pos lbl z (Asm.fn_code tf). -Proof. -Admitted. - -Lemma goto_label_preserved bb rs1 m1 rs1' m1' rs2 m2 lbl f tf v: forall - (FINDF: transf_function f = OK tf) - (BOUNDED: size bb <= Ptrofs.max_unsigned) - (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2)) - (HGOTO: goto_label f lbl (incrPC v rs1) m1 = Next rs1' m1'), - exists (rs2' : regset) (m2' : mem), Asm.goto_label tf lbl rs2 m2 = Next rs2' m2' - /\ match_states (State rs1' m1') (State rs2' m2'). -Proof. - intros. - unfold goto_label, Asm.goto_label in *. - rewrite <- (label_pos_preserved f); auto. - inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. - destruct label_pos; next_stuck_cong. - destruct (incrPC v rs1 PC) eqn:INCRPC; next_stuck_cong. - inversion HGOTO; auto. repeat (econstructor; eauto). - rewrite <- EQPC. - unfold incrPC in *. - rewrite !Pregmap.gss in *. - destruct (rs1 PC) eqn:EQRS1; simpl in *; try congruence. - replace (rs2 # PC <- (Vptr b0 (Ptrofs.repr z))) with ((rs1 # PC <- (Vptr b0 (Ptrofs.add i0 v))) # PC <- (Vptr b (Ptrofs.repr z))); auto. - eapply functional_extensionality. intros. - destruct (PregEq.eq x PC); subst. - rewrite !Pregmap.gss. congruence. - rewrite !Pregmap.gso; auto. -Qed. - Lemma last_instruction_cannot_be_label bb: list_nth_z (header bb) (size bb - 1) = None. Proof. -- cgit