From 246553dadbf6a089bd92bcdea645cff95e26f3ed Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sun, 6 Dec 2020 22:15:54 +0100 Subject: Asmgen proof completely proved with ldp/stp --- aarch64/Asmgenproof.v | 166 ++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 120 insertions(+), 46 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index d412b129..eac406a1 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -814,14 +814,24 @@ Lemma exec_basic_dont_move_PC bi rs m rs' m': forall Proof. destruct bi; simpl; intros. - inv BASIC. exploit exec_arith_instr_dont_move_PC; eauto. - - admit. - (*unfold exec_load in BASIC.*) - (*destruct Mem.loadv. 2: { discriminate BASIC. }*) - (*inv BASIC. rewrite Pregmap.gso; try discriminate; auto.*) - - admit. - (*unfold exec_store in BASIC.*) - (*destruct Mem.storev. 2: { discriminate BASIC. }*) - (*inv BASIC; reflexivity.*) + - unfold exec_load in BASIC. + destruct ld. + + unfold exec_load_rd_a in BASIC. + destruct Mem.loadv. 2: { discriminate BASIC. } + inv BASIC. rewrite Pregmap.gso; try discriminate; auto. + + unfold exec_load_double, is_pair_addressing_mode_correct in BASIC. + destruct a; try discriminate BASIC. + do 2 (destruct Mem.loadv; try discriminate BASIC). + inv BASIC. rewrite Pregmap.gso; try discriminate; auto. + - unfold exec_store in BASIC. + destruct st. + + unfold exec_store_rs_a in BASIC. + destruct Mem.storev. 2: { discriminate BASIC. } + inv BASIC; reflexivity. + + unfold exec_store_double in BASIC. + destruct a; try discriminate BASIC. + do 2 (destruct Mem.storev; try discriminate BASIC). + inv BASIC; reflexivity. - destruct Mem.alloc, Mem.store. 2: { discriminate BASIC. } inv BASIC. repeat (rewrite Pregmap.gso; try discriminate). reflexivity. - destruct Mem.loadv. 2: { discriminate BASIC. } @@ -831,8 +841,8 @@ Proof. - inv BASIC; rewrite Pregmap.gso; try discriminate; auto. - inv BASIC; rewrite Pregmap.gso; try discriminate; auto. - inv BASIC; rewrite Pregmap.gso; try discriminate; auto. -(*Qed.*) -Admitted. + - inv BASIC; auto. +Qed. Lemma exec_body_dont_move_PC_aux: forall bis rs m rs' m' @@ -1064,16 +1074,15 @@ Proof. rewrite <- Ptrofs.add_unsigned; rewrite <- Val.offset_ptr_assoc; rewrite AGPC; eauto. Qed. -(* TODO -Lemma load_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk f a: forall +Lemma load_rd_a_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk f a: forall (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) - (HLOAD: exec_load lk chk f a rd rs1 m1 = Next rs1' m1'), + (HLOAD: exec_load_rd_a lk chk f a rd rs1 m1 = Next rs1' m1'), exists (rs2' : regset) (m2' : mem), Asm.exec_load tge chk f a rd rs2 m2 = Next rs2' m2' /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). Proof. intros. - unfold exec_load, Asm.exec_load in *. + unfold exec_load_rd_a, Asm.exec_load in *. inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. rewrite <- (eval_addressing_preserved a rs1 rs2); auto. destruct (Mem.loadv _ _ _). @@ -1083,26 +1092,81 @@ Proof. * eapply ptrofs_nextinstr_agree; eauto. + next_stuck_cong. Qed. - *) + +Lemma load_double_preserved n rs1 m1 rs1' m1' rs2 m2 rd1 rd2 chk f a: forall + (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) + (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) + (HLOAD: exec_load_double lk chk f a rd1 rd2 rs1 m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.exec_load_double tge chk f a rd1 rd2 rs2 m2 = Next rs2' m2' + /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). +Proof. + intros. + unfold exec_load_double, Asm.exec_load_double in *. + inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. + erewrite <- !eval_addressing_preserved; eauto. + destruct (is_pair_addressing_mode_correct a); try discriminate. + destruct (Mem.loadv _ _ _); + destruct (Mem.loadv chk m2 + (eval_addressing lk + (get_offset_addr a match chk with + | Mint32 => 4 + | _ => 8 + end) rs1)); + inversion HLOAD; auto. + repeat (econstructor; eauto). + * eapply nextinstr_agree_but_pc; intros. + destruct (PregEq.eq r rd2); destruct (PregEq.eq r rd1). + - try update_x_access_x. + - try update_x_access_x. + - subst; repeat rewrite Pregmap.gso, Pregmap.gss; auto. + - try update_x_access_r. + * eapply ptrofs_nextinstr_agree; eauto. +Qed. -(*Lemma store_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk a: forall*) - (*(BOUNDED: 0 <= n <= Ptrofs.max_unsigned)*) - (*(MATCHI: match_internal n (State rs1 m1) (State rs2 m2))*) - (*(HSTORE: exec_store lk chk a rd rs1 m1 = Next rs1' m1'),*) - (*exists (rs2' : regset) (m2' : mem), Asm.exec_store tge chk a rd rs2 m2 = Next rs2' m2'*) - (*/\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').*) -(*Proof.*) - (*intros.*) - (*unfold exec_store, Asm.exec_store in *.*) - (*inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.*) - (*rewrite <- (eval_addressing_preserved a rs1 rs2); auto.*) - (*destruct (Mem.storev _ _ _ _).*) - (*+ inversion HSTORE; auto. repeat (econstructor; eauto).*) - (** eapply nextinstr_agree_but_pc; intros.*) - (*subst. apply EQR. auto.*) - (** eapply ptrofs_nextinstr_agree; subst; eauto.*) - (*+ next_stuck_cong.*) -(*Qed.*) +Lemma store_rs_a_preserved n rs1 m1 rs1' m1' rs2 m2 v chk a: forall + (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) + (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) + (HSTORE: exec_store_rs_a lk chk a v rs1 m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.exec_store tge chk a v rs2 m2 = Next rs2' m2' + /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). +Proof. + intros. + unfold exec_store_rs_a, Asm.exec_store in *. + inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. + rewrite <- (eval_addressing_preserved a rs1 rs2); auto. + destruct (Mem.storev _ _ _ _). + + inversion HSTORE; auto. repeat (econstructor; eauto). + * eapply nextinstr_agree_but_pc; intros. + subst. apply EQR. auto. + * eapply ptrofs_nextinstr_agree; subst; eauto. + + next_stuck_cong. +Qed. + +Lemma store_double_preserved n rs1 m1 rs1' m1' rs2 m2 v1 v2 chk a: forall + (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) + (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) + (HSTORE: exec_store_double lk chk a v1 v2 rs1 m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.exec_store_double tge chk a v1 v2 rs2 m2 = Next rs2' m2' + /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). +Proof. + intros. + unfold exec_store_double, Asm.exec_store_double in *. + inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. + erewrite <- !eval_addressing_preserved; eauto. + destruct (is_pair_addressing_mode_correct a); try discriminate. + destruct (Mem.storev _ _ _ _); + try destruct (Mem.storev chk m + (eval_addressing lk + (get_offset_addr a match chk with + | Mint32 => 4 + | _ => 8 + end) rs1) v2); + inversion HSTORE; auto. + repeat (econstructor; eauto). + * eapply nextinstr_agree_but_pc; intros. + subst. apply EQR. auto. + * eapply ptrofs_nextinstr_agree; subst; eauto. +Qed. Lemma next_inst_preserved n rs1 m1 rs1' m1' rs2 m2 (x: dreg) v: forall (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) @@ -1271,14 +1335,17 @@ Proof. try (destruct_reg_size); try (exploit next_inst_preserved; eauto); try (find_rwrt_ag). } } - { (* PLoad TODO *) - admit. - (*destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_preserved; eauto;*) - (*intros; simpl in *; destruct sz; eauto. }*)} + { (* PLoad *) + destruct ld. + - destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_rd_a_preserved; eauto; + intros; simpl in *; destruct sz; eauto. + - destruct ld; monadInv TRANSBI; exploit load_double_preserved; eauto. } { (* PStore *) - admit. } - (*destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_preserved; eauto;*) - (*simpl in *; inv_matchi; find_rwrt_ag. }*) + destruct st. + - destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_rs_a_preserved; eauto; + simpl in *; inv_matchi; find_rwrt_ag. + - destruct st; monadInv TRANSBI; exploit store_double_preserved; eauto; + simpl in *; inv_matchi; find_rwrt_ag. } { (* Pallocframe *) monadInv TRANSBI; inv_matchi; try pc_not_sp; @@ -1309,8 +1376,15 @@ Proof. try (exploit next_inst_preserved; eauto); rewrite symbol_addresses_preserved; eauto; try (find_rwrt_ag). -(*Qed.*) -Admitted. + { (* Pnop *) + monadInv TRANSBI; inv_matchi. + inversion BASIC. + repeat (econstructor; eauto). + eapply nextinstr_agree_but_pc; intros; + try rewrite <- H0, AG; auto. + try eapply ptrofs_nextinstr_agree; auto; rewrite <- H0; + assumption. } +Qed. Lemma find_basic_instructions b ofs f bb tc: forall (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) @@ -1592,11 +1666,11 @@ Lemma no_label_in_basic_inst: forall a lbl x, Proof. intros. destruct a; simpl in *; - repeat destruct i; simpl in *; + repeat destruct i; + repeat destruct ld; repeat destruct st; + simpl in *; try (try destruct_reg_inv; monadInv H; simpl in *; reflexivity). - admit. -(*Qed.*) -Admitted. +Qed. Lemma label_pos_body bdy: forall c1 c2 z ex lbl (HUNF : unfold_body bdy = OK c2), -- cgit