From 95dc0730b9fa0f7d60222f53d7cdc3aed14206da Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 17 Dec 2020 15:25:31 +0100 Subject: Some progress in Asmblockgenproof --- aarch64/Asmblockgen.v | 29 +- aarch64/Asmblockgenproof.v | 1635 +++++-------------------------------------- aarch64/Asmblockgenproof0.v | 173 ++++- aarch64/Asmblockgenproof1.v | 223 +++++- 4 files changed, 566 insertions(+), 1494 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index e260bd69..325f238c 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -579,47 +579,47 @@ Definition cond_for_cond (cond: condition) := without setting then testing condition flags. *) Definition transl_cond_branch_default - (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*control) := + (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*cf_instruction) := do ccode <- transl_cond c args k; - OK(ccode, PCtlFlow (Pbc (cond_for_cond c) lbl)). + OK(ccode, Pbc (cond_for_cond c) lbl). Definition transl_cond_branch - (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*control) := + (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*cf_instruction) := match args, c with | a1 :: nil, (Ccompimm Cne n | Ccompuimm Cne n) => if Int.eq n Int.zero - then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbnz W r1 lbl))) + then (do r1 <- ireg_of a1; OK (k, Pcbnz W r1 lbl)) else transl_cond_branch_default c args lbl k | a1 :: nil, (Ccompimm Ceq n | Ccompuimm Ceq n) => if Int.eq n Int.zero - then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbz W r1 lbl))) + then (do r1 <- ireg_of a1; OK (k, Pcbz W r1 lbl)) else transl_cond_branch_default c args lbl k | a1 :: nil, (Ccomplimm Cne n | Ccompluimm Cne n) => if Int64.eq n Int64.zero - then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbnz X r1 lbl))) + then (do r1 <- ireg_of a1; OK (k, Pcbnz X r1 lbl)) else transl_cond_branch_default c args lbl k | a1 :: nil, (Ccomplimm Ceq n | Ccompluimm Ceq n) => if Int64.eq n Int64.zero - then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbz X r1 lbl))) + then (do r1 <- ireg_of a1; OK (k, Pcbz X r1 lbl)) else transl_cond_branch_default c args lbl k | a1 :: nil, Cmaskzero n => match Int.is_power2 n with - | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbz W r1 bit lbl)) + | Some bit => do r1 <- ireg_of a1; OK (k, Ptbz W r1 bit lbl) | None => transl_cond_branch_default c args lbl k end | a1 :: nil, Cmasknotzero n => match Int.is_power2 n with - | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbnz W r1 bit lbl)) + | Some bit => do r1 <- ireg_of a1; OK (k, Ptbnz W r1 bit lbl) | None => transl_cond_branch_default c args lbl k end | a1 :: nil, Cmasklzero n => match Int64.is_power2' n with - | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbz X r1 bit lbl)) + | Some bit => do r1 <- ireg_of a1; OK (k, Ptbz X r1 bit lbl) | None => transl_cond_branch_default c args lbl k end | a1 :: nil, Cmasklnotzero n => match Int64.is_power2' n with - | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbnz X r1 bit lbl)) + | Some bit => do r1 <- ireg_of a1; OK (k, Ptbnz X r1 bit lbl) | None => transl_cond_branch_default c args lbl k end | _, _ => @@ -1234,7 +1234,7 @@ Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) : res OK (make_epilogue f, PCtlFlow (Pbr r1 sig)) | MBbuiltin ef args res => OK (nil, Pbuiltin ef (List.map (map_builtin_arg dreg_of) args) (map_builtin_res dreg_of res)) | MBgoto lbl => OK (nil, PCtlFlow (Pb lbl)) - | MBcond cond args lbl => transl_cond_branch cond args lbl nil + | MBcond cond args lbl => do (bc, c) <- transl_cond_branch cond args lbl nil; OK (bc, PCtlFlow c) | MBreturn => OK (make_epilogue f, PCtlFlow (Pret RA)) | MBjumptable arg tbl => do r <- ireg_of arg; OK (nil, PCtlFlow (Pbtbl r tbl)) @@ -1272,7 +1272,8 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: Program Definition make_prologue (f: Machblock.function) (k:bblocks) := {| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::bi - storeptr_bc RA XSP f.(fn_retaddr_ofs) nil; +(* storeptr_bc RA XSP f.(fn_retaddr_ofs) nil; *) + ((PSt_rs_a Pstrx RA) (ADimm XSP (Ptrofs.to_int64 (f.(fn_retaddr_ofs))))) ::bi nil; exit := None |} :: k. (* Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b @@ -1290,7 +1291,7 @@ Definition transf_function (f: Machblock.function) : res Asmblock.function := else OK tf. Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef := - transf_partial_fundef transl_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *) + transf_partial_fundef transf_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *) Definition transf_program (p: Machblock.program) : res Asmblock.program := transform_partial_program transf_fundef p. diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v index 55f50b7a..586286bd 100644 --- a/aarch64/Asmblockgenproof.v +++ b/aarch64/Asmblockgenproof.v @@ -63,8 +63,7 @@ Lemma functions_transl: Genv.find_funct_ptr tge fb = Some (Internal tf). Proof. intros. exploit functions_translated; eauto. intros [tf' [A B]]. - monadInv B. unfold transf_function in H0. monadInv H0. - destruct zlt; try discriminate. rewrite EQ in EQ0. inv EQ0; inv EQ1; auto. + monadInv B. rewrite H0 in EQ; inv EQ; auto. Qed. Lemma transf_function_no_overflow: @@ -347,67 +346,34 @@ Ltac exploreInst := (** Some translation properties *) -Lemma no_builtin_preserved: - forall f ex x1 x2, - (forall ef args res, ex <> Some (MBbuiltin ef args res)) -> - transl_exit f ex = OK(x1, x2) -> - (exists i, x2 = Some (PCtlFlow i)) - \/ x2 = None. -Proof. - intros until x2. intros Hbuiltin TIC. - destruct ex. - - destruct c. - (* MBcall *) - + simpl in TIC. monadInv TIC. exploreInst; simpl; eauto. - (* MBtailcall *) - + simpl in TIC. monadInv TIC. exploreInst; simpl; eauto. - (* MBbuiltin *) - + assert (H: Some (MBbuiltin e l b) <> Some (MBbuiltin e l b)). - apply Hbuiltin. contradict H; auto. - (* MBgoto *) - + simpl in TIC. exploreInst; simpl; eauto. - (* MBcond *) - + simpl in TIC. unfold transl_cond_branch, transl_cond_branch_default in TIC. - monadInv TIC; exploreInst; simpl; eauto. - (* MBjumptable *) - + simpl in TIC. monadInv TIC. exploreInst; simpl; eauto. - (* MBreturn *) - + simpl in TIC. monadInv TIC. simpl. eauto. - - monadInv TIC. simpl; auto. -Qed. - Lemma transl_blocks_distrib: forall c f bb tbb tc ep, transl_blocks f (bb::c) ep = OK (tbb::tc) - -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> transl_block f bb (if MB.header bb then ep else false) = OK (tbb :: nil) /\ transl_blocks f c false = OK tc. Proof. - intros until ep. intros TLBS Hbuiltin. + intros until ep. intros TLBS. destruct bb as [hd bdy ex]. monadInv TLBS. monadInv EQ. - exploit no_builtin_preserved; eauto. intros Hectl. destruct Hectl. - - destruct H as [i Hectl]. - unfold cons_bblocks in H0. rewrite Hectl in H0. - destruct (x3 @@ x1) eqn: CBDY; inv H0; inv EQ0; - simpl in *; unfold transl_block; simpl; rewrite H0; simpl; - rewrite EQ; simpl; rewrite CBDY; auto. - - unfold cons_bblocks in H0. rewrite H in H0. - destruct (x3 @@ x1) eqn: CBDY; inv H0; inv EQ0; - simpl in *; unfold transl_block; simpl; rewrite H0; simpl; - rewrite EQ; simpl; rewrite CBDY; auto. + unfold transl_block. + rewrite EQ0; simpl. + simpl in EQ; rewrite EQ; simpl. + unfold cons_bblocks in *. simpl in EQ0. + destruct ex. + - simpl in *. monadInv EQ0. + destruct (x3 @@ x1) eqn: CBDY; inv H0; inv EQ1; auto. + - simpl in *. inv EQ0. destruct (x3 @@ nil) eqn: CBDY; inv H0; inv EQ1; auto. Qed. -Lemma cons_bblocks_nobuiltin: +Lemma cons_bblocks_decomp: forall thd tbdy tex tbb, (tbdy <> nil \/ tex <> None) -> - (forall ef args res, tex <> Some (Pbuiltin ef args res)) -> cons_bblocks thd tbdy tex = tbb :: nil -> header tbb = thd /\ body tbb = tbdy /\ exit tbb = tex. Proof. - intros until tbb. intros Hnonil Hnobuiltin CONSB. unfold cons_bblocks in CONSB. + intros until tbb. intros Hnonil CONSB. unfold cons_bblocks in CONSB. destruct (tex) eqn:ECTL. - destruct tbdy; inv CONSB; simpl; auto. - inversion Hnonil. @@ -622,21 +588,6 @@ Proof. - contradict Hnonil; auto. Qed. -Lemma transl_exit_nobuiltin: - forall f ex bdy x, - (forall ef args res, ex <> Some (MBbuiltin ef args res)) -> - transl_exit f ex = OK (bdy, x) -> - (forall ef args res, x <> Some (Pbuiltin ef args res)). -Proof. - intros until x. intros Hnobuiltin TIC. intros until res. - unfold transl_exit, transl_control in TIC. exploreInst. monadInv TIC. - exploreInst. - all: try discriminate. - - assert False. eapply Hnobuiltin; eauto. destruct H. - - unfold transl_cond_branch, transl_cond_branch_default in EQ. exploreInst. - all: try discriminate. -Qed. - Theorem app_nonil: forall A (l1 l2: list A), l1 <> nil -> l1 @@ l2 <> nil. @@ -650,7 +601,6 @@ Qed. Theorem match_state_codestate: forall mbs abs s fb sp bb c ms m, - (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> (MB.body bb <> nil \/ MB.exit bb <> None) -> mbs = (Machblock.State s fb sp (bb::c) ms m) -> match_states mbs abs -> @@ -663,16 +613,15 @@ Theorem match_state_codestate: /\ cur cs = tbb /\ rem cs = tc /\ pstate cs = abs. Proof. - intros until m. intros Hnobuiltin Hnotempty Hmbs MS. subst. inv MS. + intros until m. intros Hnotempty Hmbs MS. subst. inv MS. inv AT. clear H0. exploit transl_blocks_nonil; eauto. intros (tbb & tc' & Htc). subst. exploit transl_blocks_distrib; eauto. intros (TLB & TLBS). clear H2. - monadInv TLB. exploit cons_bblocks_nobuiltin; eauto. + monadInv TLB. exploit cons_bblocks_decomp; eauto. { inversion Hnotempty. - destruct (MB.body bb) as [|bi bdy]; try (contradict H0; simpl; auto; fail). left. apply app_nonil. eapply transl_basic_code_nonil; eauto. - destruct (MB.exit bb) as [ei|]; try (contradict H0; simpl; auto; fail). right. eapply transl_exit_nonil; eauto. } - eapply transl_exit_nobuiltin; eauto. intros (Hth & Htbdy & Htexit). exists {| pstate := (State rs m'); pheader := (Machblock.header bb); pbody1 := x1; pbody2 := x; pctl := x0; ep := ep0; rem := tc'; cur := tbb |}, fb, f, tbb, tc', ep0. @@ -740,30 +689,22 @@ Proof. intros. destruct (PregEq.eq r X30); [ rewrite e in H; simpl in H; discriminate | auto ]. Qed. +Lemma X16_not_data_preg: forall r , + data_preg r = true -> + r <> X16. +Proof. + intros. destruct (PregEq.eq r X16); [ rewrite e in H; simpl in H; discriminate | auto ]. +Qed. + Ltac Simpl := rewrite Pregmap.gso; try apply PC_not_data_preg; try apply X30_not_data_preg. -Ltac ArgsInv := - repeat (match goal with - | [ H: Error _ = OK _ |- _ ] => discriminate - | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args - | [ H: bind _ _ = OK _ |- _ ] => monadInv H - | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv - | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv - end); - subst; - repeat (match goal with - | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in * - | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in * - end). - (* See (C) in the diagram. The proofs are mostly adapted from the previous Mach->Asm proofs, but are unfortunately quite cumbersome. To reproduce them, it's best to have a Coq IDE with you and see by yourself the steps *) Theorem step_simu_control: forall bb' fb fn s sp c ms' m' rs2 m2 t S'' rs1 m1 tbb tbdy2 tex cs2, MB.body bb' = nil -> - (forall ef args res, MB.exit bb' <> Some (MBbuiltin ef args res)) -> Genv.find_funct_ptr tge fb = Some (Internal fn) -> pstate cs2 = (State rs2 m2) -> pbody1 cs2 = nil -> pbody2 cs2 = tbdy2 -> pctl cs2 = tex -> @@ -775,8 +716,8 @@ Theorem step_simu_control: exec_body lk tge tbdy2 rs2 m2 = Next rs3 m3 /\ exec_exit tge fn (Ptrofs.repr (size tbb)) rs3 m3 tex t rs4 m4 /\ match_states S'' (State rs4 m4)). -Proof. Admitted. (* - intros until cs2. intros Hbody Hbuiltin FIND Hpstate Hpbody1 Hpbody2 Hpctl Hcur MCS MAS ESTEP. +Proof. + intros until cs2. intros Hbody FIND Hpstate Hpbody1 Hpbody2 Hpctl Hcur MCS MAS ESTEP. inv ESTEP. - inv MCS. inv MAS. simpl in *. inv Hpstate. @@ -873,8 +814,37 @@ Proof. Admitted. (* - eauto with asmgen. } { rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H11. auto. } + (* MBbuiltin (contradiction) *) - assert (MB.exit bb' <> Some (MBbuiltin e l b)) by (apply Hbuiltin). - rewrite <- H in H1. contradict H1; auto. + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + + assert (f0 = f) by congruence. subst f0. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. + remember (Ptrofs.add _ _) as ofs'. + assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc). + econstructor; eauto. + (* exploit return_address_offset_correct; eauto. intros; subst ra. + repeat eexists. + econstructor; eauto. econstructor. *) + + monadInv TBC. monadInv TIC. inv H0. + + +exploit builtin_args_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. + intros [vres' [m2' [A [B [C D]]]]]. + + + repeat eexists. econstructor. erewrite <- sp_val by eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. eauto. + econstructor; eauto. + unfold incrPC. rewrite Pregmap.gss. + rewrite set_res_other. rewrite undef_regs_other_2. unfold Val.offset_ptr. rewrite PCeq. + eauto. rewrite preg_notin_charact. intros. auto with asmgen. + auto with asmgen. apply agree_nextblock. eapply agree_set_res; auto. + eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. + intros. discriminate. + (* MBgoto *) destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. inv TBC. inv TIC. inv H0. @@ -903,71 +873,46 @@ Proof. Admitted. (* congruence. + (* MBcond *) destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. - inv TBC. inv TIC. inv H0. + inv TBC. inv TIC. inv H0. monadInv H1. monadInv EQ. * (* MBcond true *) assert (f0 = f) by congruence. subst f0. exploit eval_condition_lessdef. eapply preg_vals; eauto. all: eauto. - intros EC. monadInv H1. - unfold transl_cond_branch in EQ. ArgsInv. - { unfold transl_cond_branch_default in EQ. monadInv EQ. unfold transl_cond in EQ0. - destruct c0; try discriminate. } - { destruct c0; ArgsInv; - try (unfold transl_cond_branch_default, transl_cond in EQ; try monadInv EQ; discriminate). - - destruct c0. - 3:{ unfold transl_cond_branch_default, transl_cond in EQ. monadInv EQ. monadInv EQ0. - repeat eexists. destruct is_arith_imm32. - - simpl. eauto. - - destruct is_arith_imm32; simpl; eauto. - - discriminate. - destruct c0; ArgsInv. unfold transl_cond_branch_default in EQ; try monadInv EQ; try unfold transl_cond in EQ0; - try discriminate. - { destruct c0; try discriminate. } - - - { monadInv EQ. unfold transl_cond in EQ0. destruct c0; try discriminate. } - { apply IHl. discriminate. - { destruct l, c0; simpl in *; try congruence. - destruct c0; simpl. simpl in EQ. monadInv EQ. - - exploit (transl_cbranch_correct); eauto. intros (rsX & mX & rsY & mY & A & B & C). - - exists rsX. exists mX. exists rsY. exists mY. split. eauto. eauto. - - assert (PCeq': rs2 PC = rs' PC). { admit. (* inv A; auto. erewrite <- exec_straight_pc. 2: eapply H. eauto. *) } + intros EC. + exploit transl_cbranch_correct_true; eauto. intros (rs', H). + destruct H as [ES [ECFI]]. + exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC). + assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. } rewrite PCeq' in PCeq. assert (f1 = f) by congruence. subst f1. exploit find_label_goto_label. - 4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs')). unfold incrPC. - rewrite Pregmap.gss. - unfold Val.offset_ptr. rewrite PCeq. eauto. + 4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs')). + unfold incrPC, Val.offset_ptr. rewrite PCeq. rewrite Pregmap.gss. eauto. intros (tc' & rs3 & GOTOL & TLPC & Hrs3). exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'. assert (tf = fn) by congruence. subst tf. repeat eexists. rewrite <- BTC. simpl. rewrite app_nil_r. eauto. - eapply (cfi_step tge fn (Ptrofs.repr (size tbb)) rs' m2 (Some x0) E0 _ _). rewrite <- BTC. simpl. econstructor. rewrite B. eauto. + rewrite <- BTC. simpl. econstructor. rewrite ECFI. eauto. econstructor; eauto. eapply agree_exten with rs2; eauto with asmgen. - { intros. destruct r; try destruct g; try discriminate. - all: rewrite Hrs3; try discriminate; unfold nextblock, incrPC; Simpl. } + { intros. rewrite Hrs3; unfold incrPC. Simpl. rewrite H. all: auto. apply PC_not_data_preg; auto. } intros. discriminate. - * (* MBcond false *) - assert (f0 = f) by congruence. subst f0. + assert (f0 = f) by congruence. subst f0. monadInv H1. monadInv EQ. exploit eval_condition_lessdef. eapply preg_vals; eauto. all: eauto. intros EC. - exploit transl_cbranch_correct_false; eauto. intros (rs' & jmp & A & B & C). + exploit transl_cbranch_correct_false; eauto. intros (rs', H). + destruct H as [ES [ECFI]]. exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC). - assert (PCeq': rs2 PC = rs' PC). { inv A; auto. erewrite <- exec_straight_pc. 2: eapply H. eauto. } + assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. } rewrite PCeq' in PCeq. exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'. assert (tf = fn) by congruence. subst tf. @@ -977,39 +922,38 @@ Proof. Admitted. (* generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. repeat eexists. - rewrite H6. rewrite <- BTC. rewrite extract_basics_to_code. simpl. rewrite app_nil_r. eauto. - rewrite H7. rewrite <- BTC. rewrite extract_ctl_basics_to_code. simpl extract_ctl. rewrite B. eauto. + rewrite <- BTC. simpl. rewrite app_nil_r. eauto. + rewrite <- BTC. simpl. econstructor. rewrite ECFI. eauto. econstructor; eauto. - unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto. + unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto. eapply agree_exten with rs2; eauto with asmgen. - { intros. destruct r; try destruct g; try discriminate. - all: rewrite <- C; try discriminate; unfold nextblock, incrPC; Simpl. } + { intros. unfold incrPC. Simpl. rewrite H. all: auto. } intros. discriminate. + (* MBjumptable *) destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. inv TBC. inv TIC. inv H0. assert (f0 = f) by congruence. subst f0. - monadInv H1. + monadInv H1. monadInv EQ. generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV. assert (f1 = f) by congruence. subst f1. - exploit find_label_goto_label. 4: eapply H16. 1-2: eauto. instantiate (2 := (nextblock tbb rs2) # GPR62 <- Vundef # GPR63 <- Vundef). - unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity. + exploit find_label_goto_label. 4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs2) # X16 <- Vundef # X17 <- Vundef). + unfold incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity. discriminate. exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn. intros [tc' [rs' [A [B C]]]]. - exploit ireg_val; eauto. rewrite H13. intros LD; inv LD. + exploit ireg_val; eauto. rewrite H11. intros LD; inv LD. - repeat eexists. - rewrite H6. simpl extract_basic. simpl. eauto. - rewrite H7. simpl extract_ctl. simpl. Simpl. rewrite <- H1. unfold Mach.label in H14. unfold label. rewrite H14. eapply A. + repeat eexists. econstructor. simpl. Simpl. 2: { eapply ireg_of_not_X16''; eauto. } + unfold incrPC. rewrite Pregmap.gso; try discriminate. rewrite <- H1. + simpl. unfold Mach.label in H12. unfold label. rewrite H12. eapply A. econstructor; eauto. eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen. - { assert (destroyed_by_jumptable = R62 :: R63 :: nil) by auto. rewrite H2 in H0. simpl in H0. inv H0. - destruct (preg_eq r' GPR63). subst. contradiction. - destruct (preg_eq r' GPR62). subst. contradiction. - destruct r'; Simpl. } + { unfold incrPC. repeat Simpl; auto. assert (destroyed_by_jumptable = R17 :: nil) by auto. + rewrite H2 in H0. simpl in H0. destruct r'; try discriminate. + destruct d; try discriminate. destruct i; try discriminate. + destruct r; try discriminate. } discriminate. + (* MBreturn *) destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. @@ -1021,33 +965,33 @@ Proof. Admitted. (* exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). exploit exec_straight_body; eauto. simpl. eauto. - intros EXEB. + intros EXEB. destruct EXEB as [l [MKEPI EXEB]]. assert (f1 = f) by congruence. subst f1. repeat eexists. - rewrite H6. simpl extract_basic. eauto. - rewrite H7. simpl extract_ctl. simpl. reflexivity. + rewrite app_nil_r in MKEPI. rewrite <- MKEPI in EXEB. eauto. + econstructor. simpl. reflexivity. econstructor; eauto. - unfold nextblock, incrPC. repeat apply agree_set_other; auto with asmgen. + unfold incrPC. repeat apply agree_set_other; auto with asmgen. - inv MCS. inv MAS. simpl in *. subst. inv Hpstate. destruct bb' as [hd' bdy' ex']; simpl in *. subst. - monadInv TBC. monadInv TIC. simpl in *. rewrite H5. rewrite H6. + monadInv TBC. monadInv TIC. simpl in *. simpl. repeat eexists. - econstructor. 4: instantiate (3 := false). all:eauto. - unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. + econstructor. econstructor. 4: instantiate (3 := false). all:eauto. + unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq. assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). eapply transf_function_no_overflow; eauto. assert (f = f0) by congruence. subst f0. econstructor; eauto. generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. eauto. - eapply agree_exten; eauto. intros. Simpl. + eapply agree_exten; eauto. intros. unfold incrPC; Simpl; auto. discriminate. -Qed.*) +Qed. (* Handling the individual instructions of theorem (B) in the above diagram. A bit less cumbersome, but still tough *) Theorem step_simu_basic: forall bb bb' s fb sp c ms m rs1 m1 ms' m' bi cs1 tbdy bdy, - MB.header bb = nil -> MB.body bb = bi::(bdy) -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> + MB.header bb = nil -> MB.body bb = bi::(bdy) -> bb' = {| MB.header := nil; MB.body := bdy; MB.exit := MB.exit bb |} -> basic_step ge s fb sp ms m bi ms' m' -> pstate cs1 = (State rs1 m1) -> pbody1 cs1 = tbdy -> @@ -1059,7 +1003,7 @@ Theorem step_simu_basic: /\ exec_body lk tge l rs1 m1 = Next rs2 m2 /\ match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2). Proof. - intros until bdy. intros Hheader Hbody Hnobuiltin (* Hnotempty *) Hbb' BSTEP Hpstate Hpbody1 MCS. inv MCS. + intros until bdy. intros Hheader Hbody (* Hnotempty *) Hbb' BSTEP Hpstate Hpbody1 MCS. inv MCS. simpl in *. inv Hpstate. rewrite Hbody in TBC. monadInv TBC. inv BSTEP. @@ -1212,56 +1156,8 @@ Local Transparent destroyed_by_op. intro Hep. simpl in Hep. discriminate. - (* MBload notrap1 *) simpl in EQ0. unfold transl_load in EQ0. discriminate. - (*destruct addr; simpl in H; destruct chunk; monadInv EQ0. - all: - destruct args as [|h0 t0]; try discriminate; - destruct t0 as [|h1 t1]; try discriminate; - destruct t1 as [|h2 t2]; try discriminate.*) - - (* MBload notrap2 *) simpl in EQ0. unfold transl_load in EQ0. discriminate. - (*simpl in EQ0. rewrite Hheader in DXP. - - assert (Op.eval_addressing tge sp addr (map ms args) = Some a). - rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. - intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. - exploit transl_load_correct; eauto. - intros [rs2 [P [Q R]]]. - - destruct (Mem.loadv chunk m1 a') as [v' | ] eqn:Hload. - { - exploit transl_load_correct; eauto. - intros [rs2 [P [Q R]]]. - - eapply exec_straight_body in P. - destruct P as (l & ll & EXECB). - exists rs2, m1, l. - eexists. eexists. split. instantiate (1 := x). eauto. - repeat (split; auto). - eapply match_codestate_intro; eauto. - - eapply agree_set_undef_mreg; eauto. intros; auto with asmgen. - - simpl in *. discriminate. - } - { - exploit transl_load_correct_notrap2; eauto. - intros [rs2 [P [Q R]]]. - - eapply exec_straight_body in P. - destruct P as (l & ll & EXECB). - exists rs2, m1, l. - eexists. eexists. split. instantiate (1 := x). eauto. - repeat (split; auto). - remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. -(* assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. } - rewrite <- Hheadereq. *) subst. - eapply match_codestate_intro; eauto. - - eapply agree_set_undef_mreg; eauto. intros; auto with asmgen. - simpl in *. discriminate. - }*) - (* MBstore *) simpl in EQ0. rewrite Hheader in DXP. @@ -1337,7 +1233,6 @@ Qed. Theorem step_simu_body: forall bb s fb sp c ms m rs1 m1 ms' cs1 m', MB.header bb = nil -> - (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> body_step ge s fb sp (MB.body bb) ms m ms' m' -> pstate cs1 = (State rs1 m1) -> match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 -> @@ -1348,17 +1243,17 @@ Theorem step_simu_body: /\ match_codestate fb (MB.State s fb sp ({| MB.header := nil; MB.body := nil; MB.exit := MB.exit bb |}::c) ms' m') cs2). Proof. intros bb. destruct bb as [hd bdy ex]; simpl; auto. induction bdy as [|bi bdy]. - - intros until m'. intros Hheader Hnobuiltin BSTEP Hpstate MCS. + - intros until m'. intros Hheader BSTEP Hpstate MCS. inv BSTEP. exists rs1, m1, cs1, (ep cs1). inv MCS. inv Hpstate. simpl in *. monadInv TBC. repeat (split; simpl; auto). econstructor; eauto. - - intros until m'. intros Hheader Hnobuiltin BSTEP Hpstate MCS. inv BSTEP. + - intros until m'. intros Hheader BSTEP Hpstate MCS. inv BSTEP. rename ms' into ms''. rename m' into m''. rename rs' into ms'. rename m'0 into m'. exploit (step_simu_basic); eauto. simpl. eauto. simpl; auto. simpl; auto. intros (rs2 & m2 & l & cs2 & tbdy' & Hcs2 & Happ & EXEB & MCS'). simpl in *. - exploit IHbdy. auto. 2: eapply H6. 3: eapply MCS'. all: eauto. subst; eauto. simpl; auto. + exploit IHbdy. auto. eapply H6. 2: eapply MCS'. all: eauto. subst; eauto. simpl; auto. intros (rs3 & m3 & cs3 & ep & Hcs3 & EXEB' & MCS''). exists rs3, m3, cs3, ep. repeat (split; simpl; auto). subst. simpl in *. auto. @@ -1368,16 +1263,15 @@ Qed. (* Bringing theorems (A), (B) and (C) together, for the case of the absence of builtin instruction *) (* This more general form is easier to prove, but the actual theorem is step_simulation_bblock further below *) Lemma step_simulation_bblock': - forall sf f sp bb bb' bb'' rs m rs' m' s'' c S1, + forall t sf f sp bb bb' bb'' rs m rs' m' s'' c S1, bb' = mb_remove_header bb -> body_step ge sf f sp (Machblock.body bb') rs m rs' m' -> bb'' = mb_remove_body bb' -> - (forall ef args res, MB.exit bb'' <> Some (MBbuiltin ef args res)) -> - exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') E0 s'' -> + exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') t s'' -> match_states (Machblock.State sf f sp (bb :: c) rs m) S1 -> - exists S2 : state, plus (step lk) tge S1 E0 S2 /\ match_states s'' S2. + exists S2 : state, plus (step lk) tge S1 t S2 /\ match_states s'' S2. Proof. - intros until S1. intros Hbb' BSTEP Hbb'' Hbuiltin ESTEP MS. + intros until S1. intros Hbb' BSTEP Hbb'' ESTEP MS. destruct (mbsize bb) eqn:SIZE. - apply mbsize_eqz in SIZE. destruct SIZE as (Hbody & Hexit). destruct bb as [hd bdy ex]; simpl in *; subst. @@ -1386,9 +1280,7 @@ Proof. eexists. split. + eapply plus_one. exploit functions_translated; eauto. intros (tf0 & FIND' & TRANSF'). monadInv TRANSF'. - assert (x = tf). { unfold transf_function in H1. monadInv H1. - destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x0))); try congruence. } - subst x. + assert (x = tf) by congruence. subst x. eapply exec_step_internal; eauto. eapply find_bblock_tail; eauto. unfold exec_bblock. simpl. eexists; eexists; split; eauto. @@ -1412,7 +1304,7 @@ Proof. (* initial setting *) exploit match_state_codestate. - 2: eapply Hnotempty. + eapply Hnotempty. all: eauto. intros (cs1 & fb & f0 & tbb & tc & ep & MCS & MAS & FIND & TLBS & Hbody & Hexit & Hcur & Hrem & Hpstate). @@ -1428,8 +1320,8 @@ Proof. (* step_simu_body part *) assert (Hpstate': pstate cs1' = pstate cs1). { inv EXEH; auto. } exploit step_simu_body. - 3: eapply BSTEP. - 4: eapply MCS2. + 2: eapply BSTEP. + 3: eapply MCS2. all: eauto. rewrite Hpstate'. eauto. intros (rs2 & m2 & cs2 & ep' & Hcs2 & EXEB & MCS'). @@ -1439,8 +1331,8 @@ Proof. destruct H as (tf & FIND'). inv EXEH. simpl in *. subst. exploit step_simu_control. - 9: eapply MCS'. all: simpl. - 10: eapply ESTEP. + 8: eapply MCS'. all: simpl. + 9: eapply ESTEP. all: simpl; eauto. { inv MAS; simpl in *. inv Hpstate2. eapply match_asmstate_some; eauto. erewrite exec_body_pc; eauto. } @@ -1467,20 +1359,18 @@ Proof. assert (f1 = f0) by congruence. subst f0. rewrite PCeq in Hrs1pc. inv Hrs1pc. exploit functions_translated; eauto. intros (tf1 & FIND'' & TRANS''). rewrite FIND' in FIND''. - inv FIND''. monadInv TRANS''. unfold transf_function in TRANSF0. monadInv TRANSF0. - destruct (zlt _ _) in EQ1; try discriminate. rewrite EQ in EQ0. inv EQ0. inv EQ1. + inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ. eapply find_bblock_tail; eauto. Qed. Theorem step_simulation_bblock: - forall sf f sp bb ms m ms' m' S2 c, + forall t sf f sp bb ms m ms' m' S2 c, body_step ge sf f sp (Machblock.body bb) ms m ms' m' -> - (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> - exit_step return_address_offset ge (Machblock.exit bb) (Machblock.State sf f sp (bb :: c) ms' m') E0 S2 -> + exit_step return_address_offset ge (Machblock.exit bb) (Machblock.State sf f sp (bb :: c) ms' m') t S2 -> forall S1', match_states (Machblock.State sf f sp (bb :: c) ms m) S1' -> - exists S2' : state, plus (step lk) tge S1' E0 S2' /\ match_states S2 S2'. + exists S2' : state, plus (step lk) tge S1' t S2' /\ match_states S2 S2'. Proof. - intros until c. intros BSTEP Hbuiltin ESTEP S1' MS. + intros until c. intros BSTEP ESTEP S1' MS. eapply step_simulation_bblock'; eauto. all: destruct bb as [hd bdy ex]; simpl in *; eauto. inv ESTEP. @@ -1488,76 +1378,19 @@ Proof. - econstructor. Qed. -(* Definition split (c: MB.code) := - match c with - | nil => nil - | bb::c => {| MB.header := MB.header bb; MB.body := MB.body bb; MB.exit := None |} - :: {| MB.header := nil; MB.body := nil; MB.exit := MB.exit bb |} :: c - end. - -Lemma cons_ok_eq3 {A: Type} : - forall (x:A) y z x' y' z', - x = x' -> y = y' -> z = z' -> - OK (x::y::z) = OK (x'::y'::z'). -Proof. - intros. subst. auto. -Qed. - -Lemma transl_blocks_split_builtin: - forall bb c ep f ef args res, - MB.exit bb = Some (MBbuiltin ef args res) -> MB.body bb <> nil -> - transl_blocks f (split (bb::c)) ep = transl_blocks f (bb::c) ep. -Proof. - intros until res. intros Hexit Hbody. simpl split. - unfold transl_blocks. fold transl_blocks. unfold transl_block. - simpl. remember (transl_basic_code _ _ _) as tbc. remember (transl_exit _ _) as tbi. - remember (transl_blocks _ _ _) as tlbs. - destruct tbc; destruct tbi; destruct tlbs. - - unfold cons_bblocks; try destruct p; try simpl; rewrite app_nil_r. - destruct l; destruct o; destruct b; simpl. auto. - - auto. - all: unfold cons_bblocks; try destruct p; try simpl; auto. - - simpl. rewrite Hexit in Heqtbi. simpl in Heqtbi. monadInv Heqtbi. simpl. - unfold cons_bblocks. simpl. destruct l. - + exploit transl_basic_code_nonil; eauto. intro. destruct H. - + simpl. rewrite app_nil_r. simpl. apply cons_ok_eq3. all: try eapply bblock_equality. all: simpl; auto. -Qed. - -Lemma transl_code_at_pc_split_builtin: - forall rs f f0 bb c ep tf tc ef args res, - MB.body bb <> nil -> MB.exit bb = Some (MBbuiltin ef args res) -> - transl_code_at_pc ge (rs PC) f f0 (bb :: c) ep tf tc -> - transl_code_at_pc ge (rs PC) f f0 (split (bb :: c)) ep tf tc. -Proof. - intros until res. intros Hbody Hexit AT. inv AT. - econstructor; eauto. erewrite transl_blocks_split_builtin; eauto. -Qed. - - -Theorem match_states_split_builtin: - forall sf f sp bb c rs m ef args res S1, - MB.body bb <> nil -> MB.exit bb = Some (MBbuiltin ef args res) -> +(* Theorem step_simulation_builtin: + forall t sf f sp bb bb' bb'' rs m rs' m' s'' c ef args res S1, + bb' = mb_remove_header bb -> + body_step ge sf f sp (Machblock.body bb') rs m rs' m' -> + bb'' = mb_remove_body bb' -> + MB.exit bb = Some (MBbuiltin ef args res) -> + exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') t s'' -> match_states (Machblock.State sf f sp (bb :: c) rs m) S1 -> - match_states (Machblock.State sf f sp (split (bb::c)) rs m) S1. -Proof. - intros until S1. intros Hbody Hexit MS. - inv MS. - econstructor; eauto. - eapply transl_code_at_pc_split_builtin; eauto. -Qed. *) - -Theorem step_simulation_builtin: - forall ef args res bb sf f sp c ms m t S2, - MB.body bb = nil -> MB.exit bb = Some (MBbuiltin ef args res) -> - exit_step return_address_offset ge (MB.exit bb) (Machblock.State sf f sp (bb :: c) ms m) t S2 -> - forall S1', match_states (Machblock.State sf f sp (bb :: c) ms m) S1' -> - exists S2' : state, plus (step lk) tge S1' t S2' /\ match_states S2 S2'. + exists S2 : state, plus (step lk) tge S1 E0 S2 /\ match_states s'' S2. Proof. - intros until S2. intros Hbody Hexit ESTEP S1' MS. + intros until S1. intros Hbb' BSTEP Hbb'' Hexit ESTEP MS. inv MS. inv AT. monadInv H2. monadInv EQ. - rewrite Hbody in EQ. monadInv EQ. - rewrite Hexit in EQ0. monadInv EQ0. + rewrite Hexit in EQ0. monadInv EQ0. simpl in ESTEP. rewrite Hexit in ESTEP. inv ESTEP. inv H4. exploit functions_transl; eauto. intro FN. @@ -1569,7 +1402,10 @@ Proof. simpl in H3. eapply exec_step_internal. eauto. eauto. eapply find_bblock_tail; eauto. - simpl. econstructor. eexists. simpl. split; eauto. + destruct (x3 @@ nil). + - eauto. + - eauto. + simpl. eauto. eexists. simpl. split; eauto. econstructor. erewrite <- sp_val by eauto. eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eauto. @@ -1586,7 +1422,7 @@ Proof. apply agree_nextblock. eapply agree_set_res; auto. eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. congruence. -Qed. +Qed. *) (* Measure to prove finite stuttering, see the other backends *) Definition measure (s: MB.state) : nat := @@ -1596,6 +1432,12 @@ Definition measure (s: MB.state) : nat := | MB.Returnstate _ _ _ => 1%nat end. +Lemma next_sep: + forall rs m rs' m', rs = rs' -> m = m' -> Next rs m = Next rs' m'. +Proof. + congruence. +Qed. + (* The actual MB.step/AB.step simulation, using the above theorems, plus extra proofs for the internal and external function cases *) Theorem step_simulation: @@ -1603,41 +1445,14 @@ Theorem step_simulation: forall S1' (MS: match_states S1 S1'), (exists S2', plus (step lk) tge S1' t S2' /\ match_states S2 S2') \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. -Proof. Admitted. -(* induction 1; intros. +Proof. + induction 1; intros. - (* bblock *) left. destruct (Machblock.exit bb) eqn:MBE; try destruct c0. all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; - try (rewrite MBE; try discriminate); eauto). - + (* MBbuiltin *) - destruct (MB.body bb) eqn:MBB. - * inv H. eapply step_simulation_builtin; eauto. rewrite MBE. eauto. - * (* eapply match_states_split_builtin in MS; eauto. - 2: rewrite MBB; discriminate. *) - (* simpl split in MS. *) - rewrite <- MBB in H. -(* remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb1. *) -(* assert (MB.body bb = MB.body bb1). { subst. simpl. auto. } *) -(* rewrite H1 in H. subst. *) - exploit step_simulation_bblock. eapply H. - discriminate. - simpl. constructor. - eauto. - intros (S2' & PLUS1 & MS'). - rewrite MBE in MS'. - assert (exit_step return_address_offset ge (Some (MBbuiltin e l b)) - (MB.State sf f sp ({| MB.header := nil; MB.body := nil; MB.exit := Some (MBbuiltin e l b) |}::c) - rs' m') t s'). - { inv H0. inv H3. econstructor. econstructor; eauto. } - exploit step_simulation_builtin. - 4: eapply MS'. - all: simpl; eauto. - intros (S3' & PLUS'' & MS''). - exists S3'. split; eauto. - eapply plus_trans. eapply PLUS1. eapply PLUS''. eauto. + try (rewrite MBE; try discriminate); eauto). + inversion H0. subst. eapply step_simulation_bblock; try (rewrite MBE; try discriminate); eauto. - - (* internal function *) inv MS. exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. @@ -1655,42 +1470,43 @@ Proof. Admitted. monadInv EQ0. set (tfbody := make_prologue f x0) in *. set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *. - set (rs2 := rs0#FP <- (parent_sp s) #SP <- sp #RTMP <- Vundef). - exploit (Pget_correct tge GPRA RA nil rs2 m2'); auto. - intros (rs' & U' & V'). - exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPRA nil rs' m2'). + set (rs2 := rs0#X29 <- (parent_sp s) #SP <- sp #X16 <- Vundef). + exploit (storeptr_correct lk tge XSP (fn_retaddr_ofs f) RA nil m2' m3' rs2). { rewrite chunk_of_Tptr in P. - assert (rs' GPRA = rs0 RA). { apply V'. } - assert (rs' SP = rs2 SP). { apply V'; discriminate. } - rewrite H4. rewrite H3. + assert (rs0 X30 = rs2 RA) by auto. + rewrite <- H3. rewrite ATLR. - change (rs2 SP) with sp. eexact P. } + change (rs2 XSP) with sp. eexact P. } + 1-2: discriminate. intros (rs3 & U & V). assert (EXEC_PROLOGUE: exists rs3', - exec_straight_blocks tge tf + exec_straight_blocks tge lk tf tf.(fn_blocks) rs0 m' x0 rs3' m3' - /\ forall r, r <> PC -> rs3' r = rs3 r). + /\ forall r, r <> PC -> r <> X16 -> rs3' r = rs3 r). { eexists. split. - change (fn_blocks tf) with tfbody; unfold tfbody. - econstructor; eauto. unfold exec_bblock. simpl exec_body. - rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. - Simpl. unfold parexec_store_offset. rewrite Ptrofs.of_int64_to_int64. unfold eval_offset. - rewrite chunk_of_Tptr in P. Simpl. rewrite ATLR. unfold Mptr in P. assert (Archi.ptr64 = true) by auto. 2: auto. rewrite H3 in P. rewrite P. - simpl. apply next_sep; eauto. reflexivity. - - intros. destruct V' as (V'' & V'). destruct r. - + Simpl. - destruct (gpreg_eq g0 GPR16). { subst. Simpl. rewrite V; try discriminate. rewrite V''. subst rs2. Simpl. } - destruct (gpreg_eq g0 GPR32). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. } - destruct (gpreg_eq g0 GPR12). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. } - destruct (gpreg_eq g0 GPR17). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. } - Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. { destruct g0; try discriminate. contradiction. } - + Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. - + contradiction. + econstructor; eauto. + assert (Archi.ptr64 = true) as SF; auto. + + unfold exec_bblock. simpl exec_body. + rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. + assert (Mptr = Mint64) by auto. rewrite H3 in F. simpl in F. rewrite F. simpl. + unfold exec_store_rs_a. repeat Simpl; try discriminate. + exists rs2. exists m3'. split. + * unfold eval_addressing. Simpl; try discriminate. rewrite Pregmap.gss. + rewrite chunk_of_Tptr in P. rewrite H3 in P. + unfold Val.addl. unfold Val.offset_ptr in P. + destruct sp; simpl; try discriminate. rewrite SF; simpl. + rewrite Ptrofs.of_int64_to_int64. unfold Mem.storev in P. rewrite ATLR. + rewrite P. simpl. apply next_sep; eauto. apply SF. + * econstructor. + + eauto. + - intros. unfold incrPC. + rewrite Pregmap.gso; auto. rewrite V; auto. } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3'). exploit exec_straight_steps_2; eauto using functions_transl. simpl fn_blocks. simpl fn_blocks in g. omega. constructor. - intros (ofs' & X & Y). + intros (ofs' & X & Y). left; exists (State rs3' m3'); split. eapply exec_straight_steps_1; eauto. simpl fn_blocks. simpl fn_blocks in g. omega. @@ -1703,22 +1519,15 @@ Proof. Admitted. apply agree_change_sp with (parent_sp s). apply agree_undef_regs with rs0. auto. Local Transparent destroyed_at_function_entry. - simpl; intros; Simpl. + simpl; intros; Simpl. auto. + assert (r' <> X29). { contradict H3; rewrite H3; unfold data_preg; auto. } auto. unfold sp; congruence. intros. - assert (r <> RTMP). { contradict H3; rewrite H3; unfold data_preg; auto. } - rewrite Heqrs3'. Simpl. rewrite V. inversion V'. rewrite H6. auto. - assert (r <> GPRA). { contradict H3; rewrite H3; unfold data_preg; auto. } - assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. } - contradict H3; rewrite H3; unfold data_preg; auto. - contradict H3; rewrite H3; unfold data_preg; auto. - contradict H3; rewrite H3; unfold data_preg; auto. - contradict H3; rewrite H3; unfold data_preg; auto. - intros. rewrite Heqrs3'. rewrite V by auto with asmgen. - assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. } - rewrite H4 by auto with asmgen. reflexivity. discriminate. + rewrite Heqrs3'. rewrite V. 2-5: try apply X16_not_data_preg; try apply PC_not_data_preg; auto. + auto. + intros. rewrite Heqrs3'; try discriminate. rewrite V by auto with asmgen. reflexivity. - (* external function *) inv MS. exploit functions_translated; eauto. @@ -1742,7 +1551,7 @@ Local Transparent destroyed_at_function_entry. right. split. omega. split. auto. rewrite <- ATPC in H5. econstructor; eauto. congruence. -Qed.*) +Qed. Lemma transf_initial_states: forall st1, MB.initial_state prog st1 -> @@ -1785,1112 +1594,6 @@ Proof. - eexact transf_initial_states. - eexact transf_final_states. - exact step_simulation. -Admitted. - -End PRESERVATION. - - -(* ORIGINAL aarch64/Asmgenproof file that needs to be adapted - -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, Collège de France and INRIA Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Correctness proof for AArch64 code generation. *) - -Require Import Coqlib Errors. -Require Import Integers Floats AST Linking. -Require Import Values Memory Events Globalenvs Smallstep. -Require Import Op Locations Mach Conventions Asm. -Require Import Asmgen Asmgenproof0 Asmgenproof1. - -Definition match_prog (p: Mach.program) (tp: Asm.program) := - match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. - -Lemma transf_program_match: - forall p tp, transf_program p = OK tp -> match_prog p tp. -Proof. - intros. eapply match_transform_partial_program; eauto. -Qed. - -Section PRESERVATION. - -Variable prog: Mach.program. -Variable tprog: Asm.program. -Hypothesis TRANSF: match_prog prog tprog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - -Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof (Genv.find_symbol_match TRANSF). - -Lemma senv_preserved: - Senv.equiv ge tge. -Proof (Genv.senv_match TRANSF). - -Lemma functions_translated: - forall b f, - Genv.find_funct_ptr ge b = Some f -> - exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial TRANSF). - -Lemma functions_transl: - forall fb f tf, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - transf_function f = OK tf -> - Genv.find_funct_ptr tge fb = Some (Internal tf). -Proof. - intros. exploit functions_translated; eauto. intros [tf' [A B]]. - monadInv B. rewrite H0 in EQ; inv EQ; auto. -Qed. - -(** * Properties of control flow *) - -Lemma transf_function_no_overflow: - forall f tf, - transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned. -Proof. - intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. - omega. -Qed. - -Lemma exec_straight_exec: - forall fb f c ep tf tc c' rs m rs' m', - transl_code_at_pc ge (rs PC) fb f c ep tf tc -> - exec_straight tge tf tc rs m c' rs' m' -> - plus step tge (State rs m) E0 (State rs' m'). -Proof. - intros. inv H. - eapply exec_straight_steps_1; eauto. - eapply transf_function_no_overflow; eauto. - eapply functions_transl; eauto. -Qed. - -Lemma exec_straight_at: - forall fb f c ep tf tc c' ep' tc' rs m rs' m', - transl_code_at_pc ge (rs PC) fb f c ep tf tc -> - transl_code f c' ep' = OK tc' -> - exec_straight tge tf tc rs m tc' rs' m' -> - transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'. -Proof. - intros. inv H. - exploit exec_straight_steps_2; eauto. - eapply transf_function_no_overflow; eauto. - eapply functions_transl; eauto. - intros [ofs' [PC' CT']]. - rewrite PC'. constructor; auto. -Qed. - -(** The following lemmas show that the translation from Mach to Asm - preserves labels, in the sense that the following diagram commutes: -<< - translation - Mach code ------------------------ Asm instr sequence - | | - | Mach.find_label lbl find_label lbl | - | | - v v - Mach code tail ------------------- Asm instr seq tail - translation ->> - The proof demands many boring lemmas showing that Asm constructor - functions do not introduce new labels. -*) - -Section TRANSL_LABEL. - -Remark loadimm_z_label: forall sz rd l k, tail_nolabel k (loadimm_z sz rd l k). -Proof. - intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel. - induction l as [ | [n p] l]; simpl; TailNoLabel. -Qed. - -Remark loadimm_n_label: forall sz rd l k, tail_nolabel k (loadimm_n sz rd l k). -Proof. - intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel. - induction l as [ | [n p] l]; simpl; TailNoLabel. -Qed. - -Remark loadimm_label: forall sz rd n k, tail_nolabel k (loadimm sz rd n k). -Proof. - unfold loadimm; intros. destruct Nat.leb; [apply loadimm_z_label|apply loadimm_n_label]. -Qed. -Hint Resolve loadimm_label: labels. - -Remark loadimm32_label: forall r n k, tail_nolabel k (loadimm32 r n k). -Proof. - unfold loadimm32; intros. destruct (is_logical_imm32 n); TailNoLabel. -Qed. -Hint Resolve loadimm32_label: labels. - -Remark loadimm64_label: forall r n k, tail_nolabel k (loadimm64 r n k). -Proof. - unfold loadimm64; intros. destruct (is_logical_imm64 n); TailNoLabel. -Qed. -Hint Resolve loadimm64_label: labels. - -Remark addimm_aux: forall insn rd r1 n k, - (forall rd r1 n, nolabel (insn rd r1 n)) -> - tail_nolabel k (addimm_aux insn rd r1 n k). -Proof. - unfold addimm_aux; intros. - destruct Z.eqb. TailNoLabel. destruct Z.eqb; TailNoLabel. -Qed. - -Remark addimm32_label: forall rd r1 n k, tail_nolabel k (addimm32 rd r1 n k). -Proof. - unfold addimm32; intros. - destruct Int.eq. apply addimm_aux; intros; red; auto. - destruct Int.eq. apply addimm_aux; intros; red; auto. - destruct Int.lt; eapply tail_nolabel_trans; TailNoLabel. -Qed. -Hint Resolve addimm32_label: labels. - -Remark addimm64_label: forall rd r1 n k, tail_nolabel k (addimm64 rd r1 n k). -Proof. - unfold addimm64; intros. - destruct Int64.eq. apply addimm_aux; intros; red; auto. - destruct Int64.eq. apply addimm_aux; intros; red; auto. - destruct Int64.lt; eapply tail_nolabel_trans; TailNoLabel. -Qed. -Hint Resolve addimm64_label: labels. - -Remark logicalimm32_label: forall insn1 insn2 rd r1 n k, - (forall rd r1 n, nolabel (insn1 rd r1 n)) -> - (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) -> - tail_nolabel k (logicalimm32 insn1 insn2 rd r1 n k). -Proof. - unfold logicalimm32; intros. - destruct (is_logical_imm32 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -Qed. - -Remark logicalimm64_label: forall insn1 insn2 rd r1 n k, - (forall rd r1 n, nolabel (insn1 rd r1 n)) -> - (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) -> - tail_nolabel k (logicalimm64 insn1 insn2 rd r1 n k). -Proof. - unfold logicalimm64; intros. - destruct (is_logical_imm64 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -Qed. - -Remark move_extended_label: forall rd r1 ex a k, tail_nolabel k (move_extended rd r1 ex a k). -Proof. - unfold move_extended, move_extended_base; intros. destruct Int.eq, ex; TailNoLabel. -Qed. -Hint Resolve move_extended_label: labels. - -Remark arith_extended_label: forall insnX insnS rd r1 r2 ex a k, - (forall rd r1 r2 x, nolabel (insnX rd r1 r2 x)) -> - (forall rd r1 r2 s, nolabel (insnS rd r1 r2 s)) -> - tail_nolabel k (arith_extended insnX insnS rd r1 r2 ex a k). -Proof. - unfold arith_extended; intros. destruct Int.ltu. - TailNoLabel. - destruct ex; simpl; TailNoLabel. -Qed. - -Remark loadsymbol_label: forall r id ofs k, tail_nolabel k (loadsymbol r id ofs k). -Proof. - intros; unfold loadsymbol. - destruct (Archi.pic_code tt); TailNoLabel. destruct Ptrofs.eq; TailNoLabel. -Qed. -Hint Resolve loadsymbol_label: labels. - -Remark transl_cond_label: forall cond args k c, - transl_cond cond args k = OK c -> tail_nolabel k c. -Proof. - unfold transl_cond; intros; destruct cond; TailNoLabel. -- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -Qed. - -Remark transl_cond_branch_default_label: forall cond args lbl k c, - transl_cond_branch_default cond args lbl k = OK c -> tail_nolabel k c. -Proof. - unfold transl_cond_branch_default; intros. - eapply tail_nolabel_trans; [eapply transl_cond_label;eauto|TailNoLabel]. -Qed. -Hint Resolve transl_cond_branch_default_label: labels. - -Remark transl_cond_branch_label: forall cond args lbl k c, - transl_cond_branch cond args lbl k = OK c -> tail_nolabel k c. -Proof. - unfold transl_cond_branch; intros; destruct args; TailNoLabel; destruct cond; TailNoLabel. -- destruct c0; TailNoLabel. -- destruct c0; TailNoLabel. -- destruct (Int.is_power2 n); TailNoLabel. -- destruct (Int.is_power2 n); TailNoLabel. -- destruct c0; TailNoLabel. -- destruct c0; TailNoLabel. -- destruct (Int64.is_power2' n); TailNoLabel. -- destruct (Int64.is_power2' n); TailNoLabel. -Qed. - -Remark transl_op_label: - forall op args r k c, - transl_op op args r k = OK c -> tail_nolabel k c. -Proof. - unfold transl_op; intros; destruct op; TailNoLabel. -- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. -- destruct (Float.eq_dec n Float.zero); TailNoLabel. -- destruct (Float32.eq_dec n Float32.zero); TailNoLabel. -- apply logicalimm32_label; unfold nolabel; auto. -- apply logicalimm32_label; unfold nolabel; auto. -- apply logicalimm32_label; unfold nolabel; auto. -- unfold shrx32. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel. -- apply arith_extended_label; unfold nolabel; auto. -- apply arith_extended_label; unfold nolabel; auto. -- apply logicalimm64_label; unfold nolabel; auto. -- apply logicalimm64_label; unfold nolabel; auto. -- apply logicalimm64_label; unfold nolabel; auto. -- unfold shrx64. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel. -- eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel. -- destruct (preg_of r); try discriminate; TailNoLabel; - (eapply tail_nolabel_trans; [eapply transl_cond_label; eauto | TailNoLabel]). -Qed. - -Remark transl_addressing_label: - forall sz addr args insn k c, - transl_addressing sz addr args insn k = OK c -> - (forall ad, nolabel (insn ad)) -> - tail_nolabel k c. -Proof. - unfold transl_addressing; intros; destruct addr; TailNoLabel; - eapply tail_nolabel_trans; TailNoLabel. - eapply tail_nolabel_trans. apply arith_extended_label; unfold nolabel; auto. TailNoLabel. -Qed. - -Remark transl_load_label: - forall trap chunk addr args dst k c, - transl_load trap chunk addr args dst k = OK c -> tail_nolabel k c. -Proof. - unfold transl_load; intros; destruct trap; try discriminate; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto. -Qed. - -Remark transl_store_label: - forall chunk addr args src k c, - transl_store chunk addr args src k = OK c -> tail_nolabel k c. -Proof. - unfold transl_store; intros; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto. -Qed. - -Remark indexed_memory_access_label: - forall insn sz base ofs k, - (forall ad, nolabel (insn ad)) -> - tail_nolabel k (indexed_memory_access insn sz base ofs k). -Proof. - unfold indexed_memory_access; intros. destruct offset_representable. - TailNoLabel. - eapply tail_nolabel_trans; TailNoLabel. -Qed. - -Remark loadind_label: - forall base ofs ty dst k c, - loadind base ofs ty dst k = OK c -> tail_nolabel k c. -Proof. - unfold loadind; intros. - destruct ty, (preg_of dst); inv H; apply indexed_memory_access_label; intros; exact I. -Qed. - -Remark storeind_label: - forall src base ofs ty k c, - storeind src base ofs ty k = OK c -> tail_nolabel k c. -Proof. - unfold storeind; intros. - destruct ty, (preg_of src); inv H; apply indexed_memory_access_label; intros; exact I. -Qed. - -Remark loadptr_label: - forall base ofs dst k, tail_nolabel k (loadptr base ofs dst k). -Proof. - intros. apply indexed_memory_access_label. unfold nolabel; auto. -Qed. - -Remark storeptr_label: - forall src base ofs k, tail_nolabel k (storeptr src base ofs k). -Proof. - intros. apply indexed_memory_access_label. unfold nolabel; auto. -Qed. - -Remark make_epilogue_label: - forall f k, tail_nolabel k (make_epilogue f k). -Proof. - unfold make_epilogue; intros. - (* FIXME destruct is_leaf_function. - { TailNoLabel. } *) - eapply tail_nolabel_trans. - apply loadptr_label. - TailNoLabel. -Qed. - -Lemma transl_instr_label: - forall f i ep k c, - transl_instr f i ep k = OK c -> - match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end. -Proof. - unfold transl_instr; intros; destruct i; TailNoLabel. -- eapply loadind_label; eauto. -- eapply storeind_label; eauto. -- destruct ep. eapply loadind_label; eauto. - eapply tail_nolabel_trans. apply loadptr_label. eapply loadind_label; eauto. -- eapply transl_op_label; eauto. -- eapply transl_load_label; eauto. -- eapply transl_store_label; eauto. -- destruct s0; monadInv H; TailNoLabel. -- destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]). -- eapply transl_cond_branch_label; eauto. -- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]. -Qed. - -Lemma transl_instr_label': - forall lbl f i ep k c, - transl_instr f i ep k = OK c -> - find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k. -Proof. - intros. exploit transl_instr_label; eauto. - destruct i; try (intros [A B]; apply B). - intros. subst c. simpl. auto. -Qed. - -Lemma transl_code_label: - forall lbl f c ep tc, - transl_code f c ep = OK tc -> - match Mach.find_label lbl c with - | None => find_label lbl tc = None - | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_code f c' false = OK tc' - end. -Proof. - induction c; simpl; intros. - inv H. auto. - monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0). - generalize (Mach.is_label_correct lbl a). - destruct (Mach.is_label lbl a); intros. - subst a. simpl in EQ. exists x; auto. - eapply IHc; eauto. -Qed. - -Lemma transl_find_label: - forall lbl f tf, - transf_function f = OK tf -> - match Mach.find_label lbl f.(Mach.fn_code) with - | None => find_label lbl tf.(fn_code) = None - | Some c => exists tc, find_label lbl tf.(fn_code) = Some tc /\ transl_code f c false = OK tc - end. -Proof. - intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. - monadInv EQ. rewrite transl_code'_transl_code in EQ0. unfold fn_code. - simpl. destruct (storeptr_label X30 XSP (fn_retaddr_ofs f) x) as [A B]; rewrite B. - eapply transl_code_label; eauto. -Qed. - -End TRANSL_LABEL. - -(** A valid branch in a piece of Mach code translates to a valid ``go to'' - transition in the generated Asm code. *) - -Lemma find_label_goto_label: - forall f tf lbl rs m c' b ofs, - Genv.find_funct_ptr ge b = Some (Internal f) -> - transf_function f = OK tf -> - rs PC = Vptr b ofs -> - Mach.find_label lbl f.(Mach.fn_code) = Some c' -> - exists tc', exists rs', - goto_label tf lbl rs m = Next rs' m - /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc' - /\ forall r, r <> PC -> rs'#r = rs#r. -Proof. - intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. - intros [tc [A B]]. - exploit label_pos_code_tail; eauto. instantiate (1 := 0). - intros [pos' [P [Q R]]]. - exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))). - split. unfold goto_label. rewrite P. rewrite H1. auto. - split. rewrite Pregmap.gss. constructor; auto. - rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. - auto. omega. - generalize (transf_function_no_overflow _ _ H0). omega. - intros. apply Pregmap.gso; auto. -Qed. - -(** Existence of return addresses *) - -Lemma return_address_exists: - forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> - exists ra, return_address_offset f c ra. -Proof. - intros. eapply Asmgenproof0.return_address_exists; eauto. -- intros. exploit transl_instr_label; eauto. - destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. -- intros. monadInv H0. - destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ. - rewrite transl_code'_transl_code in EQ0. - exists x; exists true; split; auto. unfold fn_code. - constructor. apply (storeptr_label X30 XSP (fn_retaddr_ofs f0) x). -- exact transf_function_no_overflow. -Qed. - -(** * Proof of semantic preservation *) - -(** Semantic preservation is proved using simulation diagrams - of the following form. -<< - st1 --------------- st2 - | | - t| *|t - | | - v v - st1'--------------- st2' ->> - The invariant is the [match_states] predicate below, which includes: -- The Asm code pointed by the PC register is the translation of - the current Mach code sequence. -- Mach register values and Asm register values agree. -*) - -Inductive match_states: Mach.state -> Asm.state -> Prop := - | match_states_intro: - forall s fb sp c ep ms m m' rs f tf tc - (STACKS: match_stack ge s) - (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) - (MEXT: Mem.extends m m') - (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc) - (AG: agree ms sp rs) - (DXP: ep = true -> rs#X29 = parent_sp s) - (LEAF: is_leaf_function f = true -> rs#RA = parent_ra s), - match_states (Mach.State s fb sp c ms m) - (Asm.State rs m') - | match_states_call: - forall s fb ms m m' rs - (STACKS: match_stack ge s) - (MEXT: Mem.extends m m') - (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = Vptr fb Ptrofs.zero) - (ATLR: rs RA = parent_ra s), - match_states (Mach.Callstate s fb ms m) - (Asm.State rs m') - | match_states_return: - forall s ms m m' rs - (STACKS: match_stack ge s) - (MEXT: Mem.extends m m') - (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = parent_ra s), - match_states (Mach.Returnstate s ms m) - (Asm.State rs m'). - -Lemma exec_straight_steps: - forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2, - match_stack ge s -> - Mem.extends m2 m2' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> - (forall k c (TR: transl_instr f i ep k = OK c), - exists rs2, - exec_straight tge tf c rs1 m1' k rs2 m2' - /\ agree ms2 sp rs2 - /\ (it1_is_parent ep i = true -> rs2#X29 = parent_sp s) - /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) -> - exists st', - plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s fb sp c ms2 m2) st'. -Proof. - intros. inversion H2. subst. monadInv H7. - exploit H3; eauto. intros [rs2 [A [B [C D]]]]. - exists (State rs2 m2'); split. - - eapply exec_straight_exec; eauto. - - econstructor; eauto. eapply exec_straight_at; eauto. -Qed. - -Lemma exec_straight_steps_goto: - forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c', - match_stack ge s -> - Mem.extends m2 m2' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mach.find_label lbl f.(Mach.fn_code) = Some c' -> - transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> - it1_is_parent ep i = false -> - (forall k c (TR: transl_instr f i ep k = OK c), - exists jmp, exists k', exists rs2, - exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' - /\ agree ms2 sp rs2 - /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2' - /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) -> - exists st', - plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s fb sp c' ms2 m2) st'. -Proof. - intros. inversion H3. subst. monadInv H9. - exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]]. - generalize (functions_transl _ _ _ H7 H8); intro FN. - generalize (transf_function_no_overflow _ _ H8); intro NOOV. - exploit exec_straight_steps_2; eauto. - intros [ofs' [PC2 CT2]]. - exploit find_label_goto_label; eauto. - intros [tc' [rs3 [GOTO [AT' OTH]]]]. - exists (State rs3 m2'); split. - eapply plus_right'. - eapply exec_straight_steps_1; eauto. - econstructor; eauto. - eapply find_instr_tail. eauto. - rewrite C. eexact GOTO. - traceEq. - econstructor; eauto. - apply agree_exten with rs2; auto with asmgen. - congruence. - rewrite OTH by congruence; auto. -Qed. - -Lemma exec_straight_opt_steps_goto: - forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c', - match_stack ge s -> - Mem.extends m2 m2' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mach.find_label lbl f.(Mach.fn_code) = Some c' -> - transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> - it1_is_parent ep i = false -> - (forall k c (TR: transl_instr f i ep k = OK c), - exists jmp, exists k', exists rs2, - exec_straight_opt tge tf c rs1 m1' (jmp :: k') rs2 m2' - /\ agree ms2 sp rs2 - /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2' - /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) -> - exists st', - plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s fb sp c' ms2 m2) st'. -Proof. - intros. inversion H3. subst. monadInv H9. - exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]]. - generalize (functions_transl _ _ _ H7 H8); intro FN. - generalize (transf_function_no_overflow _ _ H8); intro NOOV. - inv A. -- exploit find_label_goto_label; eauto. - intros [tc' [rs3 [GOTO [AT' OTH]]]]. - exists (State rs3 m2'); split. - apply plus_one. econstructor; eauto. - eapply find_instr_tail. eauto. - rewrite C. eexact GOTO. - econstructor; eauto. - apply agree_exten with rs2; auto with asmgen. - congruence. - rewrite OTH by congruence; auto. -- exploit exec_straight_steps_2; eauto. - intros [ofs' [PC2 CT2]]. - exploit find_label_goto_label; eauto. - intros [tc' [rs3 [GOTO [AT' OTH]]]]. - exists (State rs3 m2'); split. - eapply plus_right'. - eapply exec_straight_steps_1; eauto. - econstructor; eauto. - eapply find_instr_tail. eauto. - rewrite C. eexact GOTO. - traceEq. - econstructor; eauto. - apply agree_exten with rs2; auto with asmgen. - congruence. - rewrite OTH by congruence; auto. -Qed. - -(** We need to show that, in the simulation diagram, we cannot - take infinitely many Mach transitions that correspond to zero - transitions on the Asm side. Actually, all Mach transitions - correspond to at least one Asm transition, except the - transition from [Machsem.Returnstate] to [Machsem.State]. - So, the following integer measure will suffice to rule out - the unwanted behaviour. *) - -Definition measure (s: Mach.state) : nat := - match s with - | Mach.State _ _ _ _ _ _ => 0%nat - | Mach.Callstate _ _ _ _ => 0%nat - | Mach.Returnstate _ _ _ => 1%nat - end. - -Remark preg_of_not_X29: forall r, negb (mreg_eq r R29) = true -> IR X29 <> preg_of r. -Proof. - intros. change (IR X29) with (preg_of R29). red; intros. - exploit preg_of_injective; eauto. intros; subst r; discriminate. -Qed. - -Lemma sp_val': forall ms sp rs, agree ms sp rs -> sp = rs XSP. -Proof. - intros. eapply sp_val; eauto. -Qed. - -(** This is the simulation diagram. We prove it by case analysis on the Mach transition. *) - -Theorem step_simulation: - forall S1 t S2, Mach.step return_address_offset ge S1 t S2 -> - forall S1' (MS: match_states S1 S1') (WF: wf_state ge S1), - (exists S2', plus step tge S1' t S2' /\ match_states S2 S2') - \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. -Proof. - induction 1; intros; inv MS. - -- (* Mlabel *) - left; eapply exec_straight_steps; eauto; intros. - monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split. { apply agree_nextinstr; auto. } - split. { simpl; congruence. } - rewrite nextinstr_inv by congruence; assumption. - -- (* Mgetstack *) - unfold load_stack in H. - exploit Mem.loadv_extends; eauto. intros [v' [A B]]. - rewrite (sp_val _ _ _ AG) in A. - left; eapply exec_straight_steps; eauto. intros. simpl in TR. - exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q [R S]]]]. - exists rs'; split. eauto. - split. { eapply agree_set_mreg; eauto with asmgen. congruence. } - split. { simpl; congruence. } - rewrite S. assumption. - -- (* Msetstack *) - unfold store_stack in H. - assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto). - exploit Mem.storev_extends; eauto. intros [m2' [A B]]. - left; eapply exec_straight_steps; eauto. - rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR. - exploit storeind_correct; eauto with asmgen. intros [rs' [P [Q R]]]. - exists rs'; split. eauto. - split. eapply agree_undef_regs; eauto with asmgen. - simpl; intros. - split. rewrite Q; auto with asmgen. - rewrite R. assumption. - -- (* Mgetparam *) - assert (f0 = f) by congruence; subst f0. - unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H0. auto. - intros [parent' [A B]]. rewrite (sp_val' _ _ _ AG) in A. - exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'. - exploit Mem.loadv_extends. eauto. eexact H1. auto. - intros [v' [C D]]. -Opaque loadind. - left; eapply exec_straight_steps; eauto; intros. monadInv TR. - destruct ep. -(* X30 contains parent *) - exploit loadind_correct. eexact EQ. - instantiate (2 := rs0). simpl; rewrite DXP; eauto. simpl; congruence. - intros [rs1 [P [Q [R S]]]]. - exists rs1; split. eauto. - split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen. - simpl; split; intros. - { rewrite R; auto with asmgen. - apply preg_of_not_X29; auto. - } - { rewrite S; auto. } - -(* X30 does not contain parent *) - exploit loadptr_correct. eexact A. simpl; congruence. intros [rs1 [P [Q R]]]. - exploit loadind_correct. eexact EQ. instantiate (2 := rs1). simpl; rewrite Q. eauto. simpl; congruence. - intros [rs2 [S [T [U V]]]]. - exists rs2; split. eapply exec_straight_trans; eauto. - split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto. - instantiate (1 := rs1#X29 <- (rs2#X29)). intros. - rewrite Pregmap.gso; auto with asmgen. - congruence. - intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen. - split; simpl; intros. rewrite U; auto with asmgen. - apply preg_of_not_X29; auto. - rewrite V. rewrite R by congruence. auto. - -- (* Mop *) - assert (eval_operation tge sp op (map rs args) m = Some v). - { rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. } - exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0. - intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. - left; eapply exec_straight_steps; eauto; intros. simpl in TR. - exploit transl_op_correct; eauto. intros [rs2 [P [Q [R S]]]]. - exists rs2; split. eauto. split. - apply agree_set_undef_mreg with rs0; auto. - apply Val.lessdef_trans with v'; auto. - split; simpl; intros. InvBooleans. - rewrite R; auto. apply preg_of_not_X29; auto. -Local Transparent destroyed_by_op. - destruct op; try exact I; simpl; congruence. - rewrite S. - auto. -- (* Mload *) - destruct trap. - { - assert (Op.eval_addressing tge sp addr (map rs args) = Some a). - { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. } - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. - intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. - exploit Mem.loadv_extends; eauto. intros [v' [C D]]. - left; eapply exec_straight_steps; eauto; intros. simpl in TR. - exploit transl_load_correct; eauto. intros [rs2 [P [Q [R S]]]]. - exists rs2; split. eauto. - split. eapply agree_set_undef_mreg; eauto. congruence. - split. simpl; congruence. - rewrite S. assumption. - } - - (* Mload notrap1 *) - inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. - -- (* Mload notrap *) - inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. - -- (* Mload notrap *) - inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. - -- (* Mstore *) - assert (Op.eval_addressing tge sp addr (map rs args) = Some a). - { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. } - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. - intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. - assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto). - exploit Mem.storev_extends; eauto. intros [m2' [C D]]. - left; eapply exec_straight_steps; eauto. - intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P [Q R]]]. - exists rs2; split. eauto. - split. eapply agree_undef_regs; eauto with asmgen. - split. simpl; congruence. - rewrite R. assumption. - -- (* Mcall *) - assert (f0 = f) by congruence. subst f0. - inv AT. - assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). - { eapply transf_function_no_overflow; eauto. } - destruct ros as [rf|fid]; simpl in H; monadInv H5. -+ (* Indirect call *) - assert (rs rf = Vptr f' Ptrofs.zero). - { destruct (rs rf); try discriminate. - revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. } - assert (rs0 x0 = Vptr f' Ptrofs.zero). - { exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto. } - generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x). - { econstructor; eauto. } - exploit return_address_offset_correct; eauto. intros; subst ra. - left; econstructor; split. - apply plus_one. eapply exec_step_internal. Simpl. rewrite <- H2; simpl; eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl. eauto. - econstructor; eauto. - econstructor; eauto. - eapply agree_sp_def; eauto. - simpl. eapply agree_exten; eauto. intros. Simpl. - Simpl. rewrite <- H2. auto. -+ (* Direct call *) - generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x). - econstructor; eauto. - exploit return_address_offset_correct; eauto. intros; subst ra. - left; econstructor; split. - apply plus_one. eapply exec_step_internal. eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto. - econstructor; eauto. - econstructor; eauto. - eapply agree_sp_def; eauto. - simpl. eapply agree_exten; eauto. intros. Simpl. - Simpl. rewrite <- H2. auto. - -- (* Mtailcall *) - assert (f0 = f) by congruence. subst f0. - inversion AT; subst. - assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). - { eapply transf_function_no_overflow; eauto. } - exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]]. - destruct ros as [rf|fid]; simpl in H; monadInv H7. -+ (* Indirect call *) - assert (rs rf = Vptr f' Ptrofs.zero). - { destruct (rs rf); try discriminate. - revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. } - assert (rs0 x0 = Vptr f' Ptrofs.zero). - { exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. } - exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). - exploit exec_straight_steps_2; eauto using functions_transl. - intros (ofs' & P & Q). - left; econstructor; split. - (* execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q. - simpl. reflexivity. - traceEq. - (* match states *) - econstructor; eauto. - apply agree_set_other; auto with asmgen. - Simpl. rewrite Z by (rewrite <- (ireg_of_eq _ _ EQ1); eauto with asmgen). assumption. -+ (* Direct call *) - exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). - exploit exec_straight_steps_2; eauto using functions_transl. - intros (ofs' & P & Q). - left; econstructor; split. - (* execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q. - simpl. reflexivity. - traceEq. - (* match states *) - econstructor; eauto. - apply agree_set_other; auto with asmgen. - Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. - -- (* Mbuiltin *) - inv AT. monadInv H4. - exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H3); intro NOOV. - exploit builtin_args_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends; eauto. - intros [vres' [m2' [A [B [C D]]]]]. - left. econstructor; split. apply plus_one. - eapply exec_step_builtin. eauto. eauto. - eapply find_instr_tail; eauto. - erewrite <- sp_val by eauto. - eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - eauto. - econstructor; eauto. - instantiate (2 := tf); instantiate (1 := x). - unfold nextinstr. rewrite Pregmap.gss. - rewrite set_res_other. rewrite undef_regs_other_2. - rewrite <- H1. simpl. econstructor; eauto. - eapply code_tail_next_int; eauto. - rewrite preg_notin_charact. intros. auto with asmgen. - auto with asmgen. - apply agree_nextinstr. eapply agree_set_res; auto. - eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. - congruence. - - Simpl. - rewrite set_res_other by trivial. - rewrite undef_regs_other. - assumption. - intro. - rewrite in_map_iff. - intros (x0 & PREG & IN). - subst r'. - intro. - apply (preg_of_not_RA x0). - congruence. - -- (* Mgoto *) - assert (f0 = f) by congruence. subst f0. - inv AT. monadInv H4. - exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]]. - left; exists (State rs' m'); split. - apply plus_one. econstructor; eauto. - eapply functions_transl; eauto. - eapply find_instr_tail; eauto. - simpl; eauto. - econstructor; eauto. - eapply agree_exten; eauto with asmgen. - congruence. - - rewrite INV by congruence. - assumption. - -- (* Mcond true *) - assert (f0 = f) by congruence. subst f0. - exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. - left; eapply exec_straight_opt_steps_goto; eauto. - intros. simpl in TR. - exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D). - exists jmp; exists k; exists rs'. - split. eexact A. - split. apply agree_exten with rs0; auto with asmgen. - split. - exact B. - rewrite D. exact LEAF. - -- (* Mcond false *) - exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. - left; eapply exec_straight_steps; eauto. intros. simpl in TR. - exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D). - econstructor; split. - eapply exec_straight_opt_right. eexact A. apply exec_straight_one. eexact B. auto. - split. apply agree_exten with rs0; auto. intros. Simpl. - split. - simpl; congruence. - Simpl. rewrite D. - exact LEAF. - -- (* Mjumptable *) - assert (f0 = f) by congruence. subst f0. - inv AT. monadInv H6. - exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H5); intro NOOV. - exploit find_label_goto_label. eauto. eauto. - instantiate (2 := rs0#X16 <- Vundef #X17 <- Vundef). - Simpl. eauto. - eauto. - intros [tc' [rs' [A [B C]]]]. - exploit ireg_val; eauto. rewrite H. intros LD; inv LD. - left; econstructor; split. - apply plus_one. econstructor; eauto. - eapply find_instr_tail; eauto. - simpl. Simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. - econstructor; eauto. - eapply agree_undef_regs; eauto. - simpl. intros. rewrite C; auto with asmgen. Simpl. - congruence. - - rewrite C by congruence. - repeat rewrite Pregmap.gso by congruence. - assumption. - -- (* Mreturn *) - assert (f0 = f) by congruence. subst f0. - inversion AT; subst. simpl in H6; monadInv H6. - assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). - eapply transf_function_no_overflow; eauto. - exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). - exploit exec_straight_steps_2; eauto using functions_transl. - intros (ofs' & P & Q). - left; econstructor; split. - (* execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q. - simpl. reflexivity. - traceEq. - (* match states *) - econstructor; eauto. - apply agree_set_other; auto with asmgen. - -- (* internal function *) - - exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. - generalize EQ; intros EQ'. monadInv EQ'. - destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0. - unfold store_stack in *. - exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. - intros [m1' [C D]]. - exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. - intros [m2' [F G]]. - simpl chunk_of_type in F. - exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. - intros [m3' [P Q]]. - change (chunk_of_type Tptr) with Mint64 in *. - (* Execution of function prologue *) - monadInv EQ0. rewrite transl_code'_transl_code in EQ1. - set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) :: - storeptr RA XSP (fn_retaddr_ofs f) x0) in *. - set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *. - set (rs2 := nextinstr (rs0#X29 <- (parent_sp s) #SP <- sp #X16 <- Vundef)). - exploit (storeptr_correct tge tf XSP (fn_retaddr_ofs f) RA x0 m2' m3' rs2). - simpl preg_of_iregsp. change (rs2 X30) with (rs0 X30). rewrite ATLR. - change (rs2 X2) with sp. eexact P. - simpl; congruence. congruence. - intros (rs3 & U & V & W). - assert (EXEC_PROLOGUE: - exec_straight tge tf - tf.(fn_code) rs0 m' - x0 rs3 m3'). - { change (fn_code tf) with tfbody; unfold tfbody. - apply exec_straight_step with rs2 m2'. - unfold exec_instr. rewrite C. fold sp. - rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity. - reflexivity. - eexact U. } - exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor. - intros (ofs' & X & Y). - left; exists (State rs3 m3'); split. - eapply exec_straight_steps_1; eauto. omega. constructor. - econstructor; eauto. - rewrite X; econstructor; eauto. - apply agree_exten with rs2; eauto with asmgen. - unfold rs2. - apply agree_nextinstr. apply agree_set_other; auto with asmgen. - apply agree_change_sp with (parent_sp s). - apply agree_undef_regs with rs0. auto. -Local Transparent destroyed_at_function_entry. simpl. - simpl; intros; Simpl. - unfold sp; congruence. - intros. rewrite V by auto with asmgen. reflexivity. - - rewrite W. - unfold rs2. - Simpl. - -- (* external function *) - exploit functions_translated; eauto. - intros [tf [A B]]. simpl in B. inv B. - exploit extcall_arguments_match; eauto. - intros [args' [C D]]. - exploit external_call_mem_extends; eauto. - intros [res' [m2' [P [Q [R S]]]]]. - left; econstructor; split. - apply plus_one. eapply exec_step_external; eauto. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - econstructor; eauto. - unfold loc_external_result. apply agree_set_other; auto. apply agree_set_pair; auto. - apply agree_undef_caller_save_regs; auto. - -- (* return *) - inv STACKS. simpl in *. - right. split. omega. split. auto. - rewrite <- ATPC in H5. - econstructor; eauto. congruence. - inv WF. - inv STACK. - inv H1. - congruence. -Qed. - -Lemma transf_initial_states: - forall st1, Mach.initial_state prog st1 -> - exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2. -Proof. - intros. inversion H. unfold ge0 in *. - econstructor; split. - econstructor. - eapply (Genv.init_mem_transf_partial TRANSF); eauto. - replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero) - with (Vptr fb Ptrofs.zero). - econstructor; eauto. - constructor. - apply Mem.extends_refl. - split. auto. simpl. unfold Vnullptr; destruct Archi.ptr64; congruence. - intros. rewrite Regmap.gi. auto. - unfold Genv.symbol_address. - rewrite (match_program_main TRANSF). - rewrite symbols_preserved. - unfold ge; rewrite H1. auto. -Qed. - -Lemma transf_final_states: - forall st1 st2 r, - match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r. -Proof. - intros. inv H0. inv H. constructor. assumption. - compute in H1. inv H1. - generalize (preg_val _ _ _ R0 AG). rewrite H2. intros LD; inv LD. auto. -Qed. - -Theorem transf_program_correct: - forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). -Proof. - eapply forward_simulation_star with (measure := measure) - (match_states := fun S1 S2 => match_states S1 S2 /\ wf_state ge S1). - - apply senv_preserved. - - simpl; intros. exploit transf_initial_states; eauto. - intros (s2 & A & B). - exists s2; intuition auto. apply wf_initial; auto. - - simpl; intros. destruct H as [MS WF]. eapply transf_final_states; eauto. - - simpl; intros. destruct H0 as [MS WF]. - exploit step_simulation; eauto. intros [ (s2' & A & B) | (A & B & C) ]. - + left; exists s2'; intuition auto. eapply wf_step; eauto. - + right; intuition auto. eapply wf_step; eauto. Qed. -End PRESERVATION. -*) \ No newline at end of file +End PRESERVATION. \ No newline at end of file diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v index 4a35485e..a47654b8 100644 --- a/aarch64/Asmblockgenproof0.v +++ b/aarch64/Asmblockgenproof0.v @@ -167,6 +167,15 @@ Proof. red; intros; elim n. eapply preg_of_injective; eauto. Qed. +Corollary agree_set_mreg_parallel: + forall ms sp rs r v v', + agree ms sp rs -> + Val.lessdef v v' -> + agree (Mach.Regmap.set r v ms) sp (Pregmap.set (preg_of r) v' rs). +Proof. + intros. eapply agree_set_mreg; eauto. rewrite Pregmap.gss; auto. intros; apply Pregmap.gso; auto. +Qed. + Lemma agree_set_other: forall ms sp rs r v, agree ms sp rs -> @@ -184,6 +193,18 @@ Proof. intros. unfold incrPC. apply agree_set_other. auto. auto. Qed. +Lemma agree_set_pair: + forall sp p v v' ms rs, + agree ms sp rs -> + Val.lessdef v v' -> + agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs). +Proof. + intros. destruct p; simpl. +- apply agree_set_mreg_parallel; auto. +- apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto. + apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto. +Qed. + Lemma agree_set_res: forall res ms sp rs v v', agree ms sp rs -> @@ -230,6 +251,23 @@ Proof. intros. rewrite Pregmap.gso; auto. Qed. +Lemma agree_undef_caller_save_regs: + forall ms sp rs, + agree ms sp rs -> + agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs). +Proof. + intros. destruct H. unfold Mach.undef_caller_save_regs, undef_caller_save_regs; split. +- unfold proj_sumbool; rewrite dec_eq_true. auto. +- auto. +- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). + destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl. ++ apply list_in_map_inv in i. destruct i as (mr & A & B). + assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A. + apply List.filter_In in B. destruct B as [C D]. rewrite D. auto. ++ destruct (is_callee_save r) eqn:CS; auto. + elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. +Qed. + Lemma agree_change_sp: forall ms sp rs sp', agree ms sp rs -> sp' <> Vundef -> @@ -262,6 +300,62 @@ Proof. exists (v1' :: vl'); split; constructor; auto. apply builtin_arg_match; auto. Qed. +(** Connection between Mach and Asm calling conventions for external + functions. *) + +Lemma extcall_arg_match: + forall ms sp rs m m' l v, + agree ms sp rs -> + Mem.extends m m' -> + Mach.extcall_arg ms m sp l v -> + exists v', extcall_arg rs m' l v' /\ Val.lessdef v v'. +Proof. + intros. inv H1. + exists (rs#(preg_of r)); split. constructor. eapply preg_val; eauto. + unfold Mach.load_stack in H2. + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. + rewrite (sp_val _ _ _ H) in A. + exists v'; split; auto. + econstructor. eauto. assumption. +Qed. + +Lemma extcall_arg_pair_match: + forall ms sp rs m m' p v, + agree ms sp rs -> + Mem.extends m m' -> + Mach.extcall_arg_pair ms m sp p v -> + exists v', extcall_arg_pair rs m' p v' /\ Val.lessdef v v'. +Proof. + intros. inv H1. +- exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto. +- exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1). + exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2). + exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto. +Qed. + +Lemma extcall_args_match: + forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> + forall ll vl, + list_forall2 (Mach.extcall_arg_pair ms m sp) ll vl -> + exists vl', list_forall2 (extcall_arg_pair rs m') ll vl' /\ Val.lessdef_list vl vl'. +Proof. + induction 3; intros. + exists (@nil val); split. constructor. constructor. + exploit extcall_arg_pair_match; eauto. intros [v1' [A B]]. + destruct IHlist_forall2 as [vl' [C D]]. + exists (v1' :: vl'); split; constructor; auto. +Qed. + +Lemma extcall_arguments_match: + forall ms m m' sp rs sg args, + agree ms sp rs -> Mem.extends m m' -> + Mach.extcall_arguments ms m sp sg args -> + exists args', extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'. +Proof. + unfold Mach.extcall_arguments, extcall_arguments; intros. + eapply extcall_args_match; eauto. +Qed. + Lemma set_res_other: forall r res v rs, data_preg r = false -> @@ -639,9 +733,36 @@ Proof. intros. apply exec_straight_opt_intro. eapply exec_straight_opt_step; eauto. Qed. +(** Like exec_straight predicate, but on blocks *) + +Inductive exec_straight_blocks: bblocks -> regset -> mem -> + bblocks -> regset -> mem -> Prop := + | exec_straight_blocks_one: + forall b1 c rs1 m1 rs2 m2, + exec_bblock lk ge fn b1 rs1 m1 E0 rs2 m2 -> + rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b1)) -> + exec_straight_blocks (b1 :: c) rs1 m1 c rs2 m2 + | exec_straight_blocks_step: + forall b c rs1 m1 rs2 m2 c' rs3 m3, + exec_bblock lk ge fn b rs1 m1 E0 rs2 m2 -> + rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b)) -> + exec_straight_blocks c rs2 m2 c' rs3 m3 -> + exec_straight_blocks (b :: c) rs1 m1 c' rs3 m3. + +Lemma exec_straight_blocks_trans: + forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3, + exec_straight_blocks c1 rs1 m1 c2 rs2 m2 -> + exec_straight_blocks c2 rs2 m2 c3 rs3 m3 -> + exec_straight_blocks c1 rs1 m1 c3 rs3 m3. +Proof. + induction 1; intros. + eapply exec_straight_blocks_step; eauto. + eapply exec_straight_blocks_step; eauto. +Qed. + (** Linking exec_straight with exec_straight_blocks *) -(* Lemma exec_straight_pc: +Lemma exec_straight_pc: forall c c' rs1 m1 rs2 m2, exec_straight c rs1 m1 c' rs2 m2 -> rs2 PC = rs1 PC. @@ -651,7 +772,7 @@ Proof. - eapply exec_basic_instr_pc; eauto. - rewrite (IHc c' rs3 m3 rs2 m2); auto. erewrite exec_basic_instr_pc; eauto. -Qed. *) +Qed. Lemma exec_body_pc: forall ge l rs1 m1 rs2 m2, @@ -667,6 +788,54 @@ Proof. erewrite exec_basic_instr_pc; eauto. Qed. +(** The following lemmas show that straight-line executions + (predicate [exec_straight_blocks]) correspond to correct Asm executions. *) + +Lemma exec_straight_steps_1: + forall c rs m c' rs' m', + exec_straight_blocks c rs m c' rs' m' -> + size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned -> + forall b ofs, + rs#PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal fn) -> + code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c -> + plus (step lk) ge (State rs m) E0 (State rs' m'). +Proof. + induction 1; intros. + apply plus_one. + econstructor; eauto. + eapply find_bblock_tail. eauto. + eapply plus_left'. + econstructor; eauto. + eapply find_bblock_tail. eauto. + apply IHexec_straight_blocks with b0 (Ptrofs.add ofs (Ptrofs.repr (size b))). + auto. rewrite H0. rewrite H3. reflexivity. + auto. + apply code_tail_next_int; auto. + traceEq. +Qed. + +Lemma exec_straight_steps_2: + forall c rs m c' rs' m', + exec_straight_blocks c rs m c' rs' m' -> + size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned -> + forall b ofs, + rs#PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal fn) -> + code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c -> + exists ofs', + rs'#PC = Vptr b ofs' + /\ code_tail (Ptrofs.unsigned ofs') (fn_blocks fn) c'. +Proof. + induction 1; intros. + exists (Ptrofs.add ofs (Ptrofs.repr (size b1))). split. + rewrite H0. rewrite H2. auto. + apply code_tail_next_int; auto. + apply IHexec_straight_blocks with (Ptrofs.add ofs (Ptrofs.repr (size b))). + auto. rewrite H0. rewrite H3. reflexivity. auto. + apply code_tail_next_int; auto. +Qed. + End STRAIGHTLINE. (** * Properties of the Machblock call stack *) diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v index bc4302ca..870211b8 100644 --- a/aarch64/Asmblockgenproof1.v +++ b/aarch64/Asmblockgenproof1.v @@ -1121,32 +1121,213 @@ Proof. destruct r; try contradiction; destruct v1; auto; destruct v2; auto. Qed. -Lemma transl_cbranch_correct: - forall cond args lbl k c m ms b sp rs m' bdy t ofs, - transl_cond_branch cond args lbl k = OK (bdy, c) -> +Lemma cmpu_bool_some_b: forall n x rs m0 b tbb, + Int.eq n Int.zero = true -> + Val.cmp_bool Ceq (rs (preg_of m0)) (Vint n) = Some b -> + ireg_of m0 = OK x -> + Val_cmpu_bool Ceq (incrPC (Ptrofs.repr (size tbb)) rs x) (Vint Int.zero) = Some b. +Proof. + intros. + replace (Vint Int.zero) with (Vint n). + 2: { apply f_equal. apply Int.same_if_eq; auto. } + unfold incrPC. Simpl. replace (rs (preg_of m0)) with (rs x) in H0. auto. + apply f_equal. symmetry. apply ireg_of_eq; auto. +Qed. + +Lemma transl_cbranch_correct_1: + forall cond args lbl c k b m ms sp rs m' tbb bdy, + transl_cond_branch cond args lbl k = OK (bdy,c) -> eval_condition cond (List.map ms args) m = Some b -> agree ms sp rs -> Mem.extends m m' -> - exists rs' m' rs'' m'', - exec_body lk ge bdy rs m = Next rs' m' - /\ exec_exit ge fn ofs rs' m' (Some c) t rs'' m'' + exists rs', + exec_straight_opt ge lk bdy rs m' k rs' m' + /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m' = eval_branch fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m' (Some b) /\ forall r, data_preg r = true -> rs'#r = rs#r. Proof. + intros until bdy; intros TR EC AG MEMX. + set (vl' := map rs (map preg_of args)). + assert (EVAL': eval_condition cond vl' m' = Some b). + { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. } + destruct cond; unfold transl_cond_branch in TR; + try unfold transl_cond_branch_default in TR; + simpl in TR; destruct args; ArgsInv. +- (* Ccomp *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_signed_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_int rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_sint; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Ccompu *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_int rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_uint; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Ccompimm *) +admit. +(* destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]; + destruct c0; try destruct (Int.eq n Int.zero) eqn:IEQ; + monadInv TR; try monadInv EQ; econstructor; split; + try (econstructor; try apply exec_straight_one); + simpl in *; eauto; try (split; intros; auto). + all: try (erewrite (cmpu_bool_some_b n x rs m0 b tbb); eauto; assumption). + unfold incrPC; Simpl. + try (rewrite (cmpu_bool_some_b n x rs m0 b tbb); auto). + + monadInv TR; try monadInv EQ. econstructor; split. econstructor; apply exec_straight_one. simpl in *; eauto. + split; intros; auto. unfold compare_int, incrPC. Simpl. auto. + assert (Val_cmpu_bool Ceq (incrPC (Ptrofs.repr (size tbb)) rs x) (Vint Int.zero) = Some b). + { replace (Vint Int.zero) with (Vint n). + 2: { apply f_equal. apply Int.same_if_eq; auto. } + unfold incrPC. Simpl. replace (rs (preg_of m0)) with (rs x) in EVAL'. auto. + apply f_equal. symmetry. apply ireg_of_eq; auto. } + rewrite H; auto. + inv EQ. + split; intros; auto. assert (eval_testcond (cond_for_unsigned_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_int rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_uint; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. + + destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. ++ econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. ++ econstructor; split. + apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto. + split; intros. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. ++ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply eval_testcond_compare_sint; auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. *) +- (* Ccompuimm *) + admit. +- (* Ccompshift *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_signed_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) + (compare_int rs (rs x) (eval_shift_op_int (rs x0) (transl_shift s a)))) = Some b). + { apply eval_testcond_compare_sint; auto. rewrite transl_eval_shift; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Ccompushift *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) + (compare_int rs (rs x) (eval_shift_op_int (rs x0) (transl_shift s a)))) = Some b). + { apply eval_testcond_compare_uint; auto. rewrite transl_eval_shift; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Cmaskzero *) admit. +- (* Cmasknotzero *) admit. +- (* Ccompl *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_signed_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_long rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_slong; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Ccomplu *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_long rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_ulong; auto. eapply Val_cmplu_bool_correct; eauto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Ccomplimm *) admit. +- (* Ccompluimm *) admit. +- (* Ccomplshift *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_signed_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) + (compare_long rs (rs x) (eval_shift_op_long (rs x0) (transl_shift s a)))) = Some b). + { apply eval_testcond_compare_slong; auto. rewrite transl_eval_shiftl; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Ccomplushift *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) + (compare_long rs (rs x) (eval_shift_op_long (rs x0) (transl_shift s a)))) = Some b). + { apply eval_testcond_compare_ulong; auto. rewrite transl_eval_shiftl; auto. + eapply Val_cmplu_bool_correct; eauto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Cmasklzero *) admit. +- (* Cmasknotzero *) admit. +- (* Ccompf *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_float; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_float_inv; auto. +- (* Cnotcompf *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_not_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_not_float; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_float_inv; auto. +- (* Ccompfzero *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (Vfloat Float.zero))) = Some b). + { apply eval_testcond_compare_float; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_float_inv; auto. +- (* Cnotcompfzero *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_not_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (Vfloat Float.zero))) = Some b). + { apply eval_testcond_compare_not_float; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_float_inv; auto. +- (* Ccompfs *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_single; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_single_inv; auto. +- (* Cnotcompfs *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_not_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_not_single; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_single_inv; auto. +- (* Ccompfszero *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (Vsingle Float32.zero))) = Some b). + { apply eval_testcond_compare_single; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_single_inv; auto. +- (* Cnotcompfszero *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_not_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (Vsingle Float32.zero))) = Some b). + { apply eval_testcond_compare_not_single; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_single_inv; auto. Admitted. -(* Lemma transl_cbranch_correct_true: - forall cond args lbl k c m ms sp rs m' bdy, - transl_cond_branch cond args lbl k = OK (bdy, c) -> +Lemma transl_cbranch_correct_true: + forall cond args lbl k c m ms sp rs m' tbb bdy, + transl_cond_branch cond args lbl k = OK (bdy,c) -> eval_condition cond (List.map ms args) m = Some true -> agree ms sp rs -> Mem.extends m m' -> - exists rs', exists insn, + exists rs', exec_straight_opt ge lk bdy rs m' k rs' m' - /\ exec_cfi ge fn insn (nextinstr rs') m' = goto_label fn lbl (nextinstr rs') m' + /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m' = goto_label fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m' /\ forall r, data_preg r = true -> rs'#r = rs#r. Proof. intros. eapply transl_cbranch_correct_1 with (b := true); eauto. -Qed. *) +Qed. + +Lemma transl_cbranch_correct_false: + forall cond args lbl k c m ms sp rs m' tbb bdy, + transl_cond_branch cond args lbl k = OK (bdy,c) -> + eval_condition cond (List.map ms args) m = Some false -> + agree ms sp rs -> + Mem.extends m m' -> + exists rs', + exec_straight_opt ge lk bdy rs m' k rs' m' + /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m' = Next (incrPC (Ptrofs.repr (size tbb)) rs') m' + /\ forall r, data_preg r = true -> rs'#r = rs#r. +Proof. + intros. exploit transl_cbranch_correct_1. all: eauto. +Qed. Lemma transl_cond_correct: forall cond args k c rs m, @@ -1727,6 +1908,24 @@ Proof. split. Simpl. intros; Simpl. Qed. +Lemma storeptr_correct: forall (base: iregsp) ofs (src: ireg) k m m' (rs: regset), + Mem.storev Mint64 m (Val.offset_ptr rs#base ofs) rs#src = Some m' -> + preg_of_iregsp base <> IR X16 -> + (DR (IR (RR1 src))) <> (DR (IR (RR1 X16))) -> + exists rs', + exec_straight ge lk (storeptr_bc src base ofs k) rs m k rs' m' + /\ forall r, r <> PC -> r <> X16 -> rs' r = rs r. +Proof. + intros. + destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate. + exploit indexed_memory_access_correct; eauto. intros (ad & rs' & A & B & C). + econstructor; split. + eapply exec_straight_opt_right. eexact A. + apply exec_straight_one. simpl. unfold exec_store_rs_a. rewrite B, C, H. eauto. + discriminate. auto. + intros; Simpl. rewrite C; auto. +Qed. + Lemma loadind_correct: forall (base: iregsp) ofs ty dst k c (rs: regset) m v, loadind base ofs ty dst k = OK c -> -- cgit