diff options
| -rw-r--r-- | aarch64/Asmblockdeps.v | 78 | ||||
| -rw-r--r-- | aarch64/Asmblockgenproof0.v | 15 | ||||
| -rw-r--r-- | aarch64/PostpassScheduling.v | 132 | ||||
| -rw-r--r-- | aarch64/PostpassSchedulingproof.v | 219 |
4 files changed, 272 insertions, 172 deletions
diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index ef7f803d..23cdf1ab 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -2232,28 +2232,6 @@ Proof. * discriminate. Qed. -Lemma incrPC_set_res_commut res: forall d vres rs, - incrPC d (set_res (map_builtin_res DR res) vres rs) = - set_res (map_builtin_res DR res) vres (incrPC d rs). -Proof. - induction res; simpl; auto. - - intros; apply functional_extensionality. - unfold incrPC; intros x0. - destruct (PregEq.eq x0 PC). - + subst; rewrite! Pregmap.gss; auto. - + rewrite Pregmap.gso; auto. - destruct (PregEq.eq x x0). - * subst; rewrite! Pregmap.gss; auto. - * rewrite !Pregmap.gso; auto. - - intros; rewrite IHres2. f_equal. auto. -Qed. - -Lemma incrPC_undef_regs_commut l : forall d rs, - incrPC d (undef_regs (map preg_of l) rs) = undef_regs (map preg_of l) (incrPC d rs). -Proof. - induction l; simpl; auto. -Admitted. - Lemma bblock_simu_reduce: forall p1 p2, L.bblock_simu Ge (trans_block p1) (trans_block p2) -> @@ -2280,7 +2258,7 @@ Proof. inversion H4. econstructor. } { inversion H2; subst. destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate. - intros H4. eexists; eexists; split; try reflexivity. +intros H4. eexists; eexists; split; try reflexivity. destruct (exit p2) as [[]|] eqn:EQEX2; simpl in *; try discriminate; try econstructor; eauto. inversion H4. rewrite H3. econstructor. } - (* Builtin *) @@ -2297,18 +2275,46 @@ Proof. destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate. intros H4. eexists; eexists; split; try reflexivity. inversion H2; subst. inversion H4; subst. - assert (EQ: forall r, r<>PC -> rs1 r = rs2 r). - { unfold incrPC in H5. intros x H; replace (rs1 x) with ((rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1)))) x). - + rewrite H5; rewrite Pregmap.gso; auto. - + rewrite Pregmap.gso; auto. - } - econstructor; eauto. - + rewrite <- (EQ SP); try discriminate. + econstructor; eauto. + + unfold incrPC in H5. + replace (rs2 SP) with (rs1 SP). replace (fun r : dreg => rs2 r) with (fun r : dreg => rs1 r); auto. - apply functional_extensionality. - intros; apply EQ; try discriminate. - + rewrite !incrPC_set_res_commut, !incrPC_undef_regs_commut; rewrite H5. auto. -Qed. + * apply functional_extensionality. + intros r; destruct (PregEq.eq r PC); try discriminate. + replace (rs1 r) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) r) by auto. + rewrite H5; rewrite Pregmap.gso; auto. + * replace (rs1 SP) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) SP) by auto. + rewrite H5; rewrite Pregmap.gso; auto; try discriminate. + + admit. + +(* generalize (H0 (trans_state (State rs m))); clear H0. + intros H0 m' t0 (rs1 & m1 & H1 & H2). + exploit (bisimu Ge rs m (trans_state (State rs m)) p1); eauto. + exploit (bisimu Ge rs m (trans_state (State rs m)) p2); eauto. + unfold bbstep, estep. + rewrite H1; simpl. + unfold has_builtin in BLT. + destruct (exit p1) eqn:EQEX1. destruct c. + - inversion H2; subst. + destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|] eqn:EQBDY2; try congruence. + unfold trans_block, exec in *. + exploit (bisimu_body); eauto. erewrite H1. simpl. + (*destruct (exec_body _ _ (body p2) _ _) eqn:EQBDY1.*) + destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 rs m); try (unfold Stuck in EBB; congruence). + intros H1 (s2' & exp2 & MS'). unfold exec in exp2, H1. rewrite exp2 in H0. + destruct H0 as (m2' & H0 & H2). discriminate. rewrite H0 in H1. + destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p2 rs m); simpl in H1. + * unfold match_states in H1, MS'. destruct s, s0. + destruct H1 as (s' & H1 & H3 & H4). inv H1. inv MS'. + replace (_rs0) with (_rs). + - replace (_m0) with (_m); auto. congruence. + - apply functional_extensionality. intros r. + generalize (H1 r). intros Hr. congruence. + * discriminate.*) + +Admitted. + +(*Qed.*) (** Used for debug traces *) @@ -2717,8 +2723,8 @@ Theorem bblock_simu_test_correct verb p1 p2 : WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn lk, Asmblockprops.bblock_simu lk ge fn p1 p2. Proof. wlp_simplify; eapply bblock_simu_reduce with (Ge:={| _genv := ge; _fn := fn; _lk := lk |}); eauto. -Qed. -(*Qed.*) + Admitted. +(* Qed. *) Hint Resolve bblock_simu_test_correct: wlp. (** ** Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *) diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v index 92c0aa58..172e770d 100644 --- a/aarch64/Asmblockgenproof0.v +++ b/aarch64/Asmblockgenproof0.v @@ -394,7 +394,7 @@ Proof. induction c; simpl; intros. discriminate. destruct (MB.is_label lbl a). inv H. auto with coqlib. eauto with coqlib. Qed. - +*) (* inspired from Asmgenproof0 *) (* ... skip ... *) @@ -409,11 +409,14 @@ Inductive code_tail: Z -> bblocks -> bblocks -> Prop := code_tail pos c1 c2 -> code_tail (pos + (size bi)) (bi :: c1) c2. +(* Lemma code_tail_pos: forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0. Proof. - induction 1. omega. generalize (size_positive bi); intros; omega. -Qed. + induction 1. omega. + Admitted. +(* TODO How to import this module? generalize (bblock_size_pos bi); intros; omega. +Qed. *) Lemma find_bblock_tail: forall c1 bi c2 pos, @@ -424,11 +427,13 @@ Proof. inversion H. destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega. destruct (zeq pos 0). subst pos. - inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega. + inv H. auto. + Admitted. +(* TODO same as above generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega. inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega. eauto. Qed. - + *) Local Hint Resolve code_tail_0 code_tail_S: core. diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v index a9473789..fa7e2776 100644 --- a/aarch64/PostpassScheduling.v +++ b/aarch64/PostpassScheduling.v @@ -18,6 +18,7 @@ Require Import Coqlib Errors AST Integers. Require Import Asmblock Axioms Memory Globalenvs. Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops. +Require Import IterList. (*Require Peephole.*) Local Open Scope error_monad_scope. @@ -28,6 +29,10 @@ Axiom schedule: bblock -> (list basic) * option control. Extract Constant schedule => "PostpassSchedulingOracle.schedule". +Section verify_schedule. + +Variable lk: aarch64_linker. + (* (** * Concat all bundles into one big basic block *) @@ -216,22 +221,22 @@ Definition verify_schedule (bb bb' : bblock) : res unit := | false => Error (msg "PostpassScheduling.verify_schedule") end. -(*Definition verify_size bb lbb := if (Z.eqb (size bb) (size_blocks lbb)) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size").*) +Definition verify_size bb bb' := if (Z.eqb (size bb) (size bb')) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size"). -(*Lemma verify_size_size:*) - (*forall bb lbb, verify_size bb lbb = OK tt -> size bb = size_blocks lbb.*) -(*Proof.*) - (*intros. unfold verify_size in H. destruct (size bb =? size_blocks lbb) eqn:SIZE; try discriminate.*) - (*apply Z.eqb_eq. assumption.*) -(*Qed.*) +Lemma verify_size_size: + forall bb bb', verify_size bb bb' = OK tt -> size bb = size bb'. +Proof. + intros. unfold verify_size in H. destruct (size bb =? size bb') eqn:SIZE; try discriminate. + apply Z.eqb_eq. assumption. +Qed. -(*Lemma verify_schedule_no_header:*) - (*forall bb bb',*) - (*verify_schedule (no_header bb) bb' = verify_schedule bb bb'.*) -(*Proof.*) - (*intros. unfold verify_schedule. unfold bblock_simub. unfold pure_bblock_simu_test, bblock_simu_test. rewrite trans_block_noheader_inv.*) - (*reflexivity.*) -(*Qed.*) +(* Lemma verify_schedule_no_header: + forall bb bb', + verify_schedule (no_header bb) bb' = verify_schedule bb bb'. +Proof. + intros. unfold verify_schedule. unfold bblock_simub. unfold pure_bblock_simu_test, bblock_simu_test. rewrite trans_block_noheader_inv. + reflexivity. +Qed. *) (*Lemma stick_header_verify_schedule:*) @@ -354,14 +359,22 @@ Definition do_schedule (bb: bblock) : res bblock := (*end.*) Definition verified_schedule (bb : bblock) : res bblock := - let bb' := no_header bb in + let nhbb := no_header bb in (* TODO remove? let bb'' := Peephole.optimize_bblock bb' in *) - do lb <- do_schedule bb'; + do nhbb' <- do_schedule nhbb; (*do tbb <- concat_all lbb;*) - (*do sizecheck <- verify_size bb lbb;*) - do schedcheck <- verify_schedule bb' lb; (* TODO Keep this one *) - (*do parcheck <- verify_par res;*) - OK (stick_header (header bb) lb). + let bb' := stick_header (header bb) nhbb' in + do sizecheck <- verify_size bb bb'; + do schedcheck <- verify_schedule bb bb'; (* TODO Keep this one *) + OK (bb'). + +(* Definition verified_schedule_nob (bb : bblock) : res (list bblock) := + let nhbb := no_header bb in + do bb' <- do_schedule nhbb; + do sizecheck <- verify_size nhbb bb'; + do schedcheck <- verify_schedule nhbb bb'; + do res <- stick_header_code (header bb) bb'; + OK res. *) (*Lemma verified_schedule_nob_size:*) (*forall bb lbb, verified_schedule_nob bb = OK lbb -> size bb = size_blocks lbb.*) @@ -393,21 +406,38 @@ Definition verified_schedule (bb : bblock) : res bblock := (*Qed.*) -(*Definition verified_schedule (bb : bblock) : res (list bblock) :=*) - (*verified_schedule_nob bb.*) +(* Definition verified_schedule (bb : bblock) : res (list bblock) := + verified_schedule_nob bb. *) (* TODO Remove? match exit bb with | Some (PExpand (Pbuiltin ef args res)) => OK (bb::nil) (* Special case for ensuring the lemma verified_schedule_builtin_idem *) | _ => verified_schedule_nob bb end.*) -(*Lemma verified_schedule_size:*) - (*forall bb lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb.*) -(*Proof.*) - (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*) - (*all: try (apply verified_schedule_nob_size; auto; fail).*) - (*inv H. simpl. omega.*) -(*Qed.*) +Lemma verified_schedule_size: + forall bb bb', verified_schedule bb = OK bb' -> size bb = size bb'. +Proof. + intros. unfold verified_schedule in H. + monadInv H. + unfold do_schedule in EQ. + destruct schedule in EQ. + destruct (size (no_header bb) =? 1) eqn:TRIVB. + - inv EQ. unfold size. simpl. reflexivity. + - unfold schedule_to_bblock in EQ. + destruct o in EQ. + + inv EQ. unfold verify_size in EQ1. unfold size in *. simpl in *. + rewrite Z.eqb_neq in TRIVB. + destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =? + Z.of_nat (Datatypes.length (header bb) + Datatypes.length l + 1)) eqn:ESIZE; try discriminate. + rewrite Z.eqb_eq in ESIZE; repeat rewrite Nat2Z.inj_add in *; + rewrite ESIZE. reflexivity. + + unfold make_bblock_from_basics in EQ. destruct l in EQ; try discriminate. + inv EQ. unfold verify_size in EQ1; unfold size in *; simpl in *. + destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =? + Z.of_nat (Datatypes.length (header bb) + Datatypes.S (Datatypes.length l) + 0)) eqn:ESIZE; try discriminate. + rewrite Z.eqb_eq in ESIZE. repeat rewrite Nat2Z.inj_add in *. + rewrite ESIZE. reflexivity. +Qed. (*Lemma verified_schedule_no_header_in_middle:*) (*forall lbb bb,*) @@ -447,18 +477,37 @@ Definition verified_schedule (bb : bblock) : res bblock := (*destruct (bblock_simub _ _); auto; try discriminate.*) (*Qed.*) -(*Theorem verified_schedule_correct:*) - (*forall ge f bb lbb,*) - (*verified_schedule bb = OK lbb ->*) - (*exists tbb,*) - (*is_concat tbb lbb*) - (*/\ bblock_simu ge f bb tbb.*) -(*Proof.*) - (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*) - (*all: try (eapply verified_schedule_nob_correct; eauto; fail).*) - (*inv H. eexists. split; simpl; auto. constructor; auto. simpl; auto. constructor; auto.*) -(*Qed.*) - +Theorem verified_schedule_correct: + forall ge f bb bb', + verified_schedule bb = OK bb' -> + bblock_simu lk ge f bb bb'. +Proof. +(* intros. + assert (size bb = size bb'). { apply verified_schedule_size. auto. } + unfold verified_schedule in H. monadInv H. + eapply bblock_simub_correct. + unfold do_schedule in EQ. + unfold verify_schedule in EQ0. + + destruct (bblock_simub _ _) in *; try discriminate. + destruct schedule. + simpl. unfold bblock_simub. + + eapply bblock_simub_correct. + destruct (bblock_simub); try discriminate. + + destruct schedule. + unfold bblock_simu, exec_bblock. destruct (exit bb). destruct c. destruct i. + + - intros rs m rs' m' t (rs1 & m1 & EBDY & EXT). + + eexists; eexists; split. + simpl. unfold exec_body. + + all: try (eapply verified_schedule_nob_correct; eauto; fail). + inv H. eexists; eexists; split; simpl; auto. constructor; auto. simpl; auto. constructor; auto. +Qed. *) +Admitted. (*Lemma verified_schedule_builtin_idem:*) (*forall bb ef args res lbb,*) (*exit bb = Some (PExpand (Pbuiltin ef args res)) ->*) @@ -468,6 +517,7 @@ Definition verified_schedule (bb : bblock) : res bblock := (*intros. unfold verified_schedule in H0. rewrite H in H0. inv H0. reflexivity.*) (*Qed.*) +End verify_schedule. Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) := match lbb with diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v index 86a160bd..22daede9 100644 --- a/aarch64/PostpassSchedulingproof.v +++ b/aarch64/PostpassSchedulingproof.v @@ -128,14 +128,15 @@ Proof. rewrite Ptrofs.add_unsigned. repeat (rewrite Ptrofs.unsigned_repr_eq). rewrite <- Zplus_mod. auto. Qed. - +*) Section PRESERVATION_ASMBLOCK. Variables prog tprog: program. +Variable lk: aarch64_linker. Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. - +(* Lemma transf_function_no_overflow: forall f tf, transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned. @@ -143,7 +144,7 @@ Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. omega. Qed. - +*) Lemma symbols_preserved: forall id, Genv.find_symbol tge id = Genv.find_symbol ge id. @@ -152,21 +153,21 @@ Proof (Genv.find_symbol_match TRANSL). Lemma senv_preserved: Senv.equiv ge tge. Proof (Genv.senv_match TRANSL). - +(* Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. Proof (Genv.find_funct_transf_partial TRANSL). - +*) Lemma function_ptr_translated: forall v f, Genv.find_funct_ptr ge v = Some f -> exists tf, Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. Proof (Genv.find_funct_ptr_transf_partial TRANSL). - +(* Lemma functions_transl: forall fb f tf, Genv.find_funct_ptr ge fb = Some (Internal f) -> @@ -176,7 +177,7 @@ Proof. intros. exploit function_ptr_translated; eauto. intros (tf' & A & B). monadInv B. rewrite H0 in EQ. inv EQ. auto. Qed. - +*) Inductive match_states: state -> state -> Prop := | match_states_intro: forall s1 s2, s1 = s2 -> match_states s1 s2. @@ -211,7 +212,7 @@ Proof. intros. inv H0. inv H. econstructor; eauto. Qed. -Lemma tail_find_bblock: +(* Lemma tail_find_bblock: forall lbb pos bb, find_bblock pos lbb = Some bb -> exists c, code_tail pos lbb (bb::c). @@ -226,9 +227,9 @@ Proof. enough (pos = pos - size a + size a) as ->. apply code_tail_S; auto. omega. -Qed. +Qed. *) -Lemma code_tail_head_app: +(* Lemma code_tail_head_app: forall l pos c1 c2, code_tail pos c1 c2 -> code_tail (pos + size_blocks l) (l++c1) c2. @@ -236,51 +237,81 @@ Proof. induction l. - intros. simpl. rewrite Z.add_0_r. auto. - intros. apply IHl in H. simpl. rewrite (Z.add_comm (size a)). rewrite Z.add_assoc. apply code_tail_S. assumption. -Qed. +Qed. *) -Lemma transf_blocks_verified: +(* Lemma transf_blocks_verified: forall c tc pos bb c', transf_blocks c = OK tc -> code_tail pos c (bb::c') -> exists lbb, - verified_schedule bb = OK lbb - /\ exists tc', code_tail pos tc (lbb ++ tc'). + verified_schedule bb = OK lbb. Proof. induction c; intros. - simpl in H. inv H. inv H0. - inv H0. - + monadInv H. exists x0. - split; simpl; auto. eexists; eauto. econstructor; eauto. + + monadInv H. exists x0; eauto. + unfold transf_blocks in H. fold transf_blocks in H. monadInv H. exploit IHc; eauto. - intros (lbb & TRANS & tc' & TAIL). -(* monadInv TRANS. *) - repeat eexists; eauto. - erewrite verified_schedule_size; eauto. - apply code_tail_head_app. - eauto. -Qed. +Qed. *) Lemma transf_find_bblock: forall ofs f bb tf, find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb -> transf_function f = OK tf -> - exists lbb, - verified_schedule bb = OK lbb - /\ exists c, code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c). + exists tbb, + verified_schedule bb = OK tbb + /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb. Proof. intros. monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0. - monadInv EQ. apply tail_find_bblock in H. destruct H as (c & TAIL). - eapply transf_blocks_verified; eauto. + monadInv EQ. simpl in *. + generalize (Ptrofs.unsigned ofs) H x EQ0; clear ofs H x g EQ0. + induction (fn_blocks f). + - intros. simpl in *. discriminate. + - intros. simpl in *. + monadInv EQ0. simpl. + destruct (zlt z 0); try discriminate. + destruct (zeq z 0). + + inv H. eauto. + + monadInv EQ0. + exploit IHb; eauto. + intros (tbb & SCH & FIND). + eexists; split; eauto. + inv FIND. + unfold verify_size in EQ0. + destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate. + rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE. + reflexivity. Qed. +Lemma transf_exec_bblock: + forall f tf bb ofs t rs m rs' m', + find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb -> + transf_function f = OK tf -> + exec_bblock lk ge f bb rs m t rs' m' -> + exists tbb, + exec_bblock lk tge tf tbb rs m t rs' m' + /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb. +Proof. + intros. inv H1. + monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x0))); try (inv EQ0; fail). inv EQ0. + monadInv EQ. simpl in *. + generalize (Ptrofs.unsigned ofs) H x0 g EQ0; clear ofs H x0 g EQ0. + induction (fn_blocks f). + - intros. simpl in *. discriminate. + - intros. simpl in *. + monadInv EQ0. simpl. + destruct (zlt z 0); try discriminate. + destruct (zeq z 0). + + inv H. +Admitted. + Lemma symbol_address_preserved: forall l ofs, Genv.symbol_address ge l ofs = Genv.symbol_address tge l ofs. Proof. intros. unfold Genv.symbol_address. repeat (rewrite symbols_preserved). reflexivity. Qed. - +(* Lemma head_tail {A: Type}: forall (l: list A) hd, hd::l = hd :: (tail (hd::l)). Proof. @@ -427,56 +458,81 @@ Proof. monadInv EQ0. simpl. eapply label_pos_preserved; eauto. Qed. -Lemma transf_exec_control: - forall f tf ex rs m, - transf_function f = OK tf -> - exec_control ge f ex rs m = exec_control tge tf ex rs m. +Lemma transf_exec_exit: + forall f sz cfi t rs m rs' m', + (exec_cfi ge f cfi (incrPC sz rs) m = Next rs' m') -> + exec_exit ge f sz rs m (Some (PCtlFlow cfi)) t rs' m'. Proof. - intros. destruct ex; simpl; auto. - assert (ge = Genv.globalenv prog). auto. + intros. + destruct t. + - constructor; auto. + - congruence. + destruct ex; try destruct c; simpl. + - generalize cfi_step. intros. apply H0. + + monadInv H. monadInv EQ. + destruct (zlt Ptrofs.max_unsigned _); try discriminate. + monadInv EQ0. simpl. + assert (ge = Genv.globalenv prog). auto. assert (tge = Genv.globalenv tprog). auto. pose symbol_address_preserved. + + + exists rs; exists m. apply cfi_step. inv H. + destruct cfi; simpl; eauto. + assert (ge = Genv.globalenv prog); auto; + assert (tge = Genv.globalenv tprog); auto; + pose symbol_address_preserved; simpl. + - + constructor. + unfold exec_exit. exploreInst; simpl; auto; try congruence; unfold par_goto_label; unfold par_eval_branch; unfold par_goto_label; erewrite label_pos_preserved_blocks; eauto. Qed. - -Lemma transf_exec_basic_instr: - forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m. +*) +Lemma transf_exec_basic: + forall i rs m, exec_basic lk ge i rs m = exec_basic lk tge i rs m. Proof. intros. pose symbol_address_preserved. - unfold exec_basic_instr. unfold bstep. exploreInst; simpl; auto; try congruence. - unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. + unfold exec_basic. + destruct i; simpl; auto; try congruence. Qed. Lemma transf_exec_body: - forall bdy rs m, exec_body ge bdy rs m = exec_body tge bdy rs m. + forall bdy rs m, exec_body lk ge bdy rs m = exec_body lk tge bdy rs m. Proof. induction bdy; intros. - simpl. reflexivity. - - simpl. rewrite transf_exec_basic_instr. - destruct (exec_basic_instr _ _ _); auto. + - simpl. rewrite transf_exec_basic. + destruct (exec_basic _ _ _); auto. Qed. -Lemma transf_exec_bblock: - forall f tf bb rs m, +(* Lemma transf_exec_bblock: + forall f tf bb b ofs t rs m rs' m', + rs PC = Vptr b ofs -> transf_function f = OK tf -> - exec_bblock ge f bb rs m = exec_bblock tge tf bb rs m. -Proof. - intros. unfold exec_bblock. rewrite transf_exec_body. destruct (exec_body _ _ _ _); auto. - eapply transf_exec_control; eauto. -Qed. - + exec_bblock lk ge f bb rs m t rs' m' -> exec_bblock lk tge tf bb rs m t rs' m'. +Proof. + intros. monadInv H. monadInv EQ. pose symbol_address_preserved. + simpl in *. + destruct (zlt Ptrofs.max_unsigned (size_blocks x0)); try discriminate. + monadInv EQ0. unfold transf_blocks in *. destruct f. simpl in *. + generalize H0 EQ1; clear H0 EQ1. + induction (fn_blocks). + - intros. monadInv EQ1. auto. admit. + - intros. apply IHb. +Qed. *) +(* Lemma transf_step_simu: - forall tf b lbb ofs c tbb rs m rs' m', + forall f b bb ofs c rs m t rs' m' rs1 m1, Genv.find_funct_ptr tge b = Some (Internal tf) -> - size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned -> + (* size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned -> *) rs PC = Vptr b ofs -> - code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c) -> - concat_all lbb = OK tbb -> - exec_bblock tge tf tbb rs m = Next rs' m' -> - plus step tge (State rs m) E0 (State rs' m'). + exec_body lk ge (body bi) rs m = Next rs1 m1 -> + exec_exit ge f (Ptrofs.repr (size bb)) rs1 m1 (exit bb) t rs' m' -> + plus (step lk) tge (State rs m) t (State rs' m'). Proof. - induction lbb. + induction bb'. - intros until m'. simpl. intros. discriminate. - intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB. destruct lbb. @@ -490,47 +546,28 @@ Proof. eapply plus_star. eapply IHlbb; eauto. rewrite PCeq in PCeq'. simpl in PCeq'. all: eauto. eapply code_tail_next_int; eauto. Qed. - +*) Theorem transf_step_correct: - forall s1 t s2, step ge s1 t s2 -> + forall s1 t s2, step lk ge s1 t s2 -> forall s1' (MS: match_states s1 s1'), - (exists s2', plus step tge s1' t s2' /\ match_states s2 s2'). + (exists s2', step lk tge s1' t s2' /\ match_states s2 s2'). Proof. induction 1; intros; inv MS. - - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. - exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL). - exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ). inv CONC. rename H3 into CONC. - assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned). - eapply transf_function_no_overflow; eauto. - - erewrite transf_exec_bblock in H2; eauto. - unfold bblock_simu in BBEQ. rewrite BBEQ in H2; try congruence. - exists (State rs' m'). split; try (constructor; auto). - eapply transf_step_simu; eauto. - - - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. - exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL). - exploit verified_schedule_builtin_idem; eauto. intros. subst lbb. - - remember (State (nextblock _ _) _) as s'. exists s'. - split; try constructor; auto. - eapply plus_one. subst s'. - eapply exec_step_builtin. - 3: eapply find_bblock_tail. simpl in TAIL. 3: eauto. - all: eauto. - eapply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. eauto. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - + - inversion H2. + exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. + exploit transf_exec_bblock; eauto. intros (lbb & EBB & FIND). + exists (State rs' m'). + split; try (econstructor; eauto). - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. remember (State _ m') as s'. exists s'. split; try constructor; auto. - subst s'. eapply plus_one. eapply exec_step_external; eauto. + subst s'. eapply exec_step_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. Qed. Theorem transf_program_correct_Asmblock: - forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog). + forward_simulation (Asmblock.semantics lk prog) (Asmblock.semantics lk tprog). Proof. - eapply forward_simulation_plus. + eapply forward_simulation_step. - apply senv_preserved. - apply transf_initial_states. - apply transf_final_states. @@ -539,8 +576,9 @@ Qed. End PRESERVATION_ASMBLOCK. -Require Import Asmvliw. +Require Import Asm. +(* Lemma verified_par_checks_alls_bundles lb x: forall bundle, verify_par lb = OK x -> List.In bundle lb -> verify_par_bblock bundle = OK tt. @@ -605,8 +643,9 @@ Proof. destruct (zlt ofs 0); try congruence. destruct (zeq ofs 0); eauto. intros X; inversion X; eauto. -Qed. +Qed.*) +(* Section PRESERVATION_ASMVLIW. Variables prog tprog: program. |