diff options
-rw-r--r-- | mppa_k1c/Asmblock.v | 30 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 10 | ||||
-rw-r--r-- | mppa_k1c/PostpassScheduling.v | 48 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 1344 |
4 files changed, 719 insertions, 713 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index b9c50517..cade1ba8 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -578,6 +578,36 @@ Proof. - destruct e; simpl; try omega. contradict H; simpl; auto. *)Qed. + +Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}. +Next Obligation. + destruct bb; simpl. assumption. +Defined. + +Lemma no_header_size: + forall bb, size (no_header bb) = size bb. +Proof. + intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity. +Qed. + +Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}. +Next Obligation. + destruct bb; simpl. assumption. +Defined. + +Lemma stick_header_size: + forall h bb, size (stick_header h bb) = size bb. +Proof. + intros. destruct bb. unfold stick_header. simpl. reflexivity. +Qed. + +Lemma stick_header_no_header: + forall bb, stick_header (header bb) (no_header bb) = bb. +Proof. + intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity. +Qed. + + Definition bblocks := list bblock. Fixpoint size_blocks (l: bblocks): Z := diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index a57f4241..4d1a0d38 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -620,6 +620,16 @@ Definition trans_pcincr (sz: Z) := [(#PC, Op (Control (OIncremPC sz)) (Name (#PC Definition trans_block (b: Asmblock.bblock) : L.bblock := trans_body (body b) ++ trans_pcincr (size b) ++ trans_exit (exit b). +Theorem trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb. +Proof. + intros. destruct bb as [hd bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity. +Qed. + +Theorem trans_block_header_inv: forall bb hd, trans_block (stick_header hd bb) = trans_block bb. +Proof. + intros. destruct bb as [hdr bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity. +Qed. + Definition state := L.mem. Definition exec := L.run. diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 4464f1b2..6bf97279 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -34,11 +34,12 @@ Definition exec := exec_bblock. Definition bblock_equivb' := bblock_equivb. -Lemma bblock_equivb'_refl: forall tbb, bblock_equivb' tbb tbb = true. +Lemma bblock_equivb'_refl (ge: Genv.t fundef unit) (fn: function): forall tbb, bblock_equivb' tbb tbb = true. Proof. intros. rewrite bblock_equiv'_eq. apply bblock_equiv'_refl. Unshelve. (* FIXME - problem of Genv and function *) -Admitted. + constructor; auto. +Qed. Lemma trans_equiv_stuck: forall b1 b2 ge fn rs m, @@ -270,10 +271,10 @@ Definition verify_schedule (bb bb' : bblock) : res unit := | false => Error (msg "PostpassScheduling.verify_schedule") end. -Lemma verify_schedule_refl: +Lemma verify_schedule_refl (ge: Genv.t fundef unit) (fn: function): forall bb, verify_schedule bb bb = OK tt. Proof. - intros. unfold verify_schedule. rewrite bblock_equivb'_refl. reflexivity. + intros. unfold verify_schedule. rewrite bblock_equivb'_refl. reflexivity. all: auto. Qed. @@ -287,21 +288,6 @@ Proof. apply Z.eqb_eq. assumption. Qed. - - -Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}. -Next Obligation. - destruct bb; simpl. assumption. -Defined. - -Lemma no_header_size: - forall bb, size (no_header bb) = size bb. -Proof. - intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity. -Qed. - -Axiom trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb. - Lemma verify_schedule_no_header: forall bb bb', verify_schedule (no_header bb) bb' = verify_schedule bb bb'. @@ -310,26 +296,6 @@ Proof. Qed. - -Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}. -Next Obligation. - destruct bb; simpl. assumption. -Defined. - -Axiom trans_block_header_inv: forall bb hd, trans_block (stick_header hd bb) = trans_block bb. - -Lemma stick_header_size: - forall h bb, size (stick_header h bb) = size bb. -Proof. - intros. destruct bb. unfold stick_header. simpl. reflexivity. -Qed. - -Lemma stick_header_no_header: - forall bb, stick_header (header bb) (no_header bb) = bb. -Proof. - intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity. -Qed. - Lemma stick_header_verify_schedule: forall hd bb' hbb' bb, stick_header hd bb' = hbb' -> @@ -448,13 +414,13 @@ Proof. destruct x0; try discriminate. assumption. Qed. -Lemma verified_schedule_single_inst: +Lemma verified_schedule_single_inst (ge: Genv.t fundef unit) (fn: function): forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil). Proof. intros. unfold verified_schedule. unfold do_schedule. rewrite no_header_size. rewrite H. simpl. unfold verify_size. simpl. rewrite no_header_size. rewrite Z.add_0_r. cutrewrite (size bb =? size bb = true). rewrite verify_schedule_refl. simpl. - apply stick_header_code_no_header. + apply stick_header_code_no_header. all: auto. rewrite H. reflexivity. Qed. diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 2c3b8454..2ecb494d 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -10,675 +10,675 @@ (* *) (* *********************************************************************) -Require Import Coqlib Errors.
-Require Import Integers Floats AST Linking.
-Require Import Values Memory Events Globalenvs Smallstep.
-Require Import Op Locations Machblock Conventions Asmblock.
-Require Import Asmblockgenproof0.
-Require Import PostpassScheduling.
-Require Import Asmblockgenproof.
-Require Import Axioms.
-
-Local Open Scope error_monad_scope.
-
-Definition match_prog (p tp: Asmblock.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.
-
-Remark builtin_body_nil:
- forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.
-Proof.
- intros. destruct bb as [hd bdy ex WF]. simpl in *.
- apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1.
- eapply H1; eauto.
-Qed.
-
-Lemma verified_schedule_builtin_idem:
- forall bb ef args res lbb,
- exit bb = Some (PExpand (Pbuiltin ef args res)) ->
- verified_schedule bb = OK lbb ->
- lbb = bb :: nil.
-Proof.
- intros. exploit builtin_body_nil; eauto. intros.
- rewrite verified_schedule_single_inst in H0.
- - inv H0. auto.
- - unfold size. rewrite H. rewrite H1. simpl. auto.
-Qed.
-
-Lemma exec_body_app:
- forall l l' ge rs m rs'' m'',
- exec_body ge (l ++ l') rs m = Next rs'' m'' ->
- exists rs' m',
- exec_body ge l rs m = Next rs' m'
- /\ exec_body ge l' rs' m' = Next rs'' m''.
-Proof.
- induction l.
- - intros. simpl in H. repeat eexists. auto.
- - intros. rewrite <- app_comm_cons in H. simpl in H.
- destruct (exec_basic_instr ge a rs m) eqn:EXEBI.
- + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2).
- repeat eexists. simpl. rewrite EXEBI. eauto. auto.
- + discriminate.
-Qed.
-
-Lemma exec_body_pc:
- forall l ge rs1 m1 rs2 m2,
- exec_body ge l rs1 m1 = Next rs2 m2 ->
- rs2 PC = rs1 PC.
-Proof.
- induction l.
- - intros. inv H. auto.
- - intros until m2. intro EXEB.
- inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate.
- eapply IHl in H0. rewrite H0.
- erewrite exec_basic_instr_pc; eauto.
-Qed.
-
-Lemma next_eq {A: Type}:
- forall (rs rs':A) m m',
- rs = rs' -> m = m' -> Next rs m = Next rs' m'.
-Proof.
- intros. congruence.
-Qed.
-
-Lemma regset_double_set:
- forall r1 r2 (rs: regset) v1 v2,
- r1 <> r2 ->
- (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1).
-Proof.
- intros. apply functional_extensionality. intros r. destruct (preg_eq r r1).
- - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto.
- - destruct (preg_eq r r2).
- + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto.
- + repeat (rewrite Pregmap.gso; auto).
-Qed.
-
-Lemma regset_double_set_id:
- forall r (rs: regset) v1 v2,
- (rs # r <- v1 # r <- v2) = (rs # r <- v2).
-Proof.
- intros. apply functional_extensionality. intros. destruct (preg_eq r x).
- - subst r. repeat (rewrite Pregmap.gss; auto).
- - repeat (rewrite Pregmap.gso); auto.
-Qed.
-
-Lemma exec_load_pc_var:
- forall ge t rs m rd ra ofs rs' m' v,
- exec_load ge t rs m rd ra ofs = Next rs' m' ->
- exec_load ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
-Proof.
- intros. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
- destruct (Mem.loadv _ _ _).
- - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
- - discriminate.
-Qed.
-
-Lemma exec_store_pc_var:
- forall ge t rs m rd ra ofs rs' m' v,
- exec_store ge t rs m rd ra ofs = Next rs' m' ->
- exec_store ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
-Proof.
- intros. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
- destruct (Mem.storev _ _ _).
- - inv H. apply next_eq; auto.
- - discriminate.
-Qed.
-
-Lemma exec_basic_instr_pc_var:
- forall ge i rs m rs' m' v,
- exec_basic_instr ge i rs m = Next rs' m' ->
- exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.
-Proof.
- intros. unfold exec_basic_instr in *. destruct i.
- - unfold exec_arith_instr in *. destruct i; destruct i.
- all: try (exploreInst; inv H; apply next_eq; auto;
- apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
-
- (* Some cases treated seperately because exploreInst destructs too much *)
- all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
- - exploreInst; apply exec_load_pc_var; auto.
- - exploreInst; apply exec_store_pc_var; auto.
- - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate).
- destruct (Mem.storev _ _ _ _); try discriminate.
- inv H. apply next_eq; auto. apply functional_extensionality. intros.
- rewrite (regset_double_set GPR32 PC); try discriminate.
- rewrite (regset_double_set GPR12 PC); try discriminate.
- rewrite (regset_double_set GPR14 PC); try discriminate. reflexivity.
- - repeat (rewrite Pregmap.gso; try discriminate).
- destruct (Mem.loadv _ _ _); try discriminate.
- destruct (rs GPR12); try discriminate.
- destruct (Mem.free _ _ _ _); try discriminate.
- inv H. apply next_eq; auto.
- rewrite (regset_double_set GPR32 PC).
- rewrite (regset_double_set GPR12 PC). reflexivity.
- all: discriminate.
- - destruct rs0; try discriminate. inv H. apply next_eq; auto.
- repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
- - destruct rd; try discriminate. inv H. apply next_eq; auto.
- repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
- - inv H. apply next_eq; auto.
-Qed.
-
-Lemma exec_body_pc_var:
- forall l ge rs m rs' m' v,
- exec_body ge l rs m = Next rs' m' ->
- exec_body ge l (rs # PC <- v) m = Next (rs' # PC <- v) m'.
-Proof.
- induction l.
- - intros. simpl. simpl in H. inv H. auto.
- - intros. simpl in *.
- destruct (exec_basic_instr ge a rs m) eqn:EXEBI; try discriminate.
- erewrite exec_basic_instr_pc_var; eauto.
-Qed.
-
-Lemma pc_set_add:
- forall rs v r x y,
- 0 <= x <= Ptrofs.max_unsigned ->
- 0 <= y <= Ptrofs.max_unsigned ->
- rs # r <- (Val.offset_ptr v (Ptrofs.repr (x + y))) = rs # r <- (Val.offset_ptr (rs # r <- (Val.offset_ptr v (Ptrofs.repr x)) r) (Ptrofs.repr y)).
-Proof.
- intros. apply functional_extensionality. intros r0. destruct (preg_eq r r0).
- - subst. repeat (rewrite Pregmap.gss); auto.
- destruct v; simpl; auto.
- rewrite Ptrofs.add_assoc.
- cutrewrite (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)); auto.
- unfold Ptrofs.add.
- cutrewrite (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)); auto.
- repeat (rewrite Ptrofs.unsigned_repr); auto.
- - repeat (rewrite Pregmap.gso; auto).
-Qed.
-
-Lemma concat2_straight:
- forall a b bb rs m rs'' m'' f ge,
- concat2 a b = OK bb ->
- exec_bblock ge f bb rs m = Next rs'' m'' ->
- exists rs' m',
- exec_bblock ge f a rs m = Next rs' m'
- /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))
- /\ exec_bblock ge f b rs' m' = Next rs'' m''.
-Proof.
- intros until ge. intros CONC2 EXEB.
- exploit concat2_zlt_size; eauto. intros (LTA & LTB).
- exploit concat2_noexit; eauto. intros EXA.
- exploit concat2_decomp; eauto. intros. inv H.
- unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate.
- rewrite H0 in EXEB'. apply exec_body_app in EXEB'. destruct EXEB' as (rs1 & m1 & EXEB1 & EXEB2).
- repeat eexists.
- unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto.
- exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto.
- unfold exec_bblock. unfold nextblock. erewrite exec_body_pc_var; eauto.
- rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id.
- assert (size bb = size a + size b).
- { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r.
- repeat (rewrite Nat2Z.inj_add). omega. }
- clear EXA H0 H1. rewrite H in EXEB.
- assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. }
- rewrite H0. rewrite <- pc_set_add; auto.
- exploit AB.size_positive. instantiate (1 := a). intro. omega.
- exploit AB.size_positive. instantiate (1 := b). intro. omega.
-Qed.
-
-Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) :
- forall a bb rs m lbb rs'' m'',
- lbb <> nil ->
- concat_all (a :: lbb) = OK bb ->
- exec_bblock ge f bb rs m = Next rs'' m'' ->
- exists bb' rs' m',
- concat_all lbb = OK bb'
- /\ exec_bblock ge f a rs m = Next rs' m'
- /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))
- /\ exec_bblock ge f bb' rs' m' = Next rs'' m''.
-Proof.
- intros until m''. intros Hnonil CONC EXEB.
- simpl in CONC.
- destruct lbb as [|b lbb]; try contradiction. clear Hnonil.
- monadInv CONC. exploit concat2_straight; eauto. intros (rs' & m' & EXEB1 & PCeq & EXEB2).
- exists x. repeat econstructor. all: eauto.
-Qed.
-
-Lemma ptrofs_add_repr :
- forall a b,
- Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr a) (Ptrofs.repr b)) = Ptrofs.unsigned (Ptrofs.repr (a + b)).
-Proof.
- intros a b.
- rewrite Ptrofs.add_unsigned. repeat (rewrite Ptrofs.unsigned_repr_eq).
- rewrite <- Zplus_mod. auto.
-Qed.
-
-Section PRESERVATION.
-
-Variables prog tprog: program.
-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.
-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.
-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) ->
- transf_function f = OK tf ->
- Genv.find_funct_ptr tge fb = Some (Internal tf).
-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.
-
-Lemma prog_main_preserved:
- prog_main tprog = prog_main prog.
-Proof (match_program_main TRANSL).
-
-Lemma prog_main_address_preserved:
- (Genv.symbol_address (Genv.globalenv prog) (prog_main prog) Ptrofs.zero) =
- (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero).
-Proof.
- unfold Genv.symbol_address. rewrite symbols_preserved.
- rewrite prog_main_preserved. auto.
-Qed.
-
-Lemma transf_initial_states:
- forall st1, initial_state prog st1 ->
- exists st2, initial_state tprog st2 /\ match_states st1 st2.
-Proof.
- intros. inv H.
- econstructor; split.
- - eapply initial_state_intro.
- eapply (Genv.init_mem_transf_partial TRANSL); eauto.
- - econstructor; eauto. subst ge0. subst rs0. rewrite prog_main_address_preserved. auto.
-Qed.
-
-Lemma transf_final_states:
- forall st1 st2 r,
- match_states st1 st2 -> final_state st1 r -> final_state st2 r.
-Proof.
- intros. inv H0. inv H. econstructor; eauto.
-Qed.
-
-Lemma tail_find_bblock:
- forall lbb pos bb,
- find_bblock pos lbb = Some bb ->
- exists c, code_tail pos lbb (bb::c).
-Proof.
- induction lbb.
- - intros. simpl in H. inv H.
- - intros. simpl in H.
- destruct (zlt pos 0); try (inv H; fail).
- destruct (zeq pos 0).
- + inv H. exists lbb. constructor; auto.
- + apply IHlbb in H. destruct H as (c & TAIL). exists c.
- cutrewrite (pos = pos - size a + size a). apply code_tail_S; auto.
- omega.
-Qed.
-
-Lemma code_tail_head_app:
- forall l pos c1 c2,
- code_tail pos c1 c2 ->
- code_tail (pos + size_blocks l) (l++c1) c2.
-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.
-
-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').
-Proof.
- induction c; intros.
- - simpl in H. inv H. inv H0.
- - inv H0.
- + monadInv H. exists x0.
- split; simpl; auto. eexists; eauto. econstructor; 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.
-
-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).
-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.
-Qed.
-
-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.
- intros. simpl. auto.
-Qed.
-
-Lemma verified_schedule_not_empty:
- forall bb lbb,
- verified_schedule bb = OK lbb -> lbb <> nil.
-Proof.
- intros. apply verified_schedule_size in H.
- pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g.
- destruct lbb; simpl in *; discriminate.
-Qed.
-
-Lemma header_nil_label_pos_none:
- forall lbb l p,
- Forall (fun b => header b = nil) lbb -> label_pos l p lbb = None.
-Proof.
- induction lbb.
- - intros. simpl. auto.
- - intros. inv H. simpl. unfold is_label. rewrite H2. destruct (in_dec l nil). { inv i. }
- auto.
-Qed.
-
-Lemma verified_schedule_label:
- forall bb tbb lbb l,
- verified_schedule bb = OK (tbb :: lbb) ->
- is_label l bb = is_label l tbb
- /\ label_pos l 0 lbb = None.
-Proof.
- intros. exploit verified_schedule_header; eauto.
- intros (HdrEq & HdrNil).
- split.
- - unfold is_label. rewrite HdrEq. reflexivity.
- - apply header_nil_label_pos_none. assumption.
-Qed.
-
-Lemma label_pos_app_none:
- forall c c' l p p',
- label_pos l p c = None ->
- label_pos l (p' + size_blocks c) c' = label_pos l p' (c ++ c').
-Proof.
- induction c.
- - intros. simpl in *. rewrite Z.add_0_r. reflexivity.
- - intros. simpl in *. destruct (is_label _ _) eqn:ISLABEL.
- + discriminate.
- + eapply IHc in H. rewrite Z.add_assoc. eauto.
-Qed.
-
-Remark label_pos_pvar_none_add:
- forall tc l p p' k,
- label_pos l (p+k) tc = None -> label_pos l (p'+k) tc = None.
-Proof.
- induction tc.
- - intros. simpl. auto.
- - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
- + discriminate.
- + pose (IHtc l p p' (k + size a)). repeat (rewrite Z.add_assoc in e). auto.
-Qed.
-
-Lemma label_pos_pvar_none:
- forall tc l p p',
- label_pos l p tc = None -> label_pos l p' tc = None.
-Proof.
- intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
- eapply label_pos_pvar_none_add; eauto.
-Qed.
-
-Remark label_pos_pvar_some_add_add:
- forall tc l p p' k k',
- label_pos l (p+k') tc = Some (p+k) -> label_pos l (p'+k') tc = Some (p'+k).
-Proof.
- induction tc.
- - intros. simpl in H. discriminate.
- - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
- + inv H. assert (k = k') by omega. subst. reflexivity.
- + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.
-Qed.
-
-Lemma label_pos_pvar_some_add:
- forall tc l p p' k,
- label_pos l p tc = Some (p+k) -> label_pos l p' tc = Some (p'+k).
-Proof.
- intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
- eapply label_pos_pvar_some_add_add; eauto.
-Qed.
-
-Remark label_pos_pvar_add:
- forall c tc l p p' k,
- label_pos l (p+k) c = label_pos l p tc ->
- label_pos l (p'+k) c = label_pos l p' tc.
-Proof.
- induction c.
- - intros. simpl in *.
- exploit label_pos_pvar_none; eauto.
- - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
- + exploit label_pos_pvar_some_add; eauto.
- + pose (IHc tc l p p' (k+size a)). repeat (rewrite Z.add_assoc in e). auto.
-Qed.
-
-Lemma label_pos_pvar:
- forall c tc l p p',
- label_pos l p c = label_pos l p tc ->
- label_pos l p' c = label_pos l p' tc.
-Proof.
- intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
- eapply label_pos_pvar_add; eauto.
-Qed.
-
-Lemma label_pos_head_app:
- forall c bb lbb l tc p,
- verified_schedule bb = OK lbb ->
- label_pos l p c = label_pos l p tc ->
- label_pos l p (bb :: c) = label_pos l p (lbb ++ tc).
-Proof.
- intros. simpl. destruct lbb as [|tbb lbb].
- - apply verified_schedule_not_empty in H. contradiction.
- - simpl. exploit verified_schedule_label; eauto. intros (ISLBL & LBLPOS).
- rewrite ISLBL.
- destruct (is_label l tbb) eqn:ISLBL'; simpl; auto.
- eapply label_pos_pvar in H0. erewrite H0.
- erewrite verified_schedule_size; eauto. simpl size_blocks. rewrite Z.add_assoc.
- erewrite label_pos_app_none; eauto.
-Qed.
-
-Lemma label_pos_preserved:
- forall c tc l,
- transf_blocks c = OK tc -> label_pos l 0 c = label_pos l 0 tc.
-Proof.
- induction c.
- - intros. simpl in *. inv H. reflexivity.
- - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. eapply IHc in EQ.
- eapply label_pos_head_app; eauto.
-Qed.
-
-Lemma label_pos_preserved_blocks:
- forall l f tf,
- transf_function f = OK tf ->
- label_pos l 0 (fn_blocks f) = label_pos l 0 (fn_blocks tf).
-Proof.
- intros. monadInv H. monadInv EQ.
- destruct (zlt Ptrofs.max_unsigned _); try discriminate.
- 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.
-Proof.
- intros. destruct ex; simpl; auto.
- assert (ge = Genv.globalenv prog). auto.
- assert (tge = Genv.globalenv tprog). auto.
- pose symbol_address_preserved.
- exploreInst; simpl; auto; try congruence.
- - unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
- - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
- - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
- - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
- - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-Qed.
-
-Lemma eval_offset_preserved:
- forall ofs, eval_offset ge ofs = eval_offset tge ofs.
-Proof.
- intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto.
-Qed.
-
-Lemma transf_exec_load:
- forall t rs m rd ra ofs, exec_load ge t rs m rd ra ofs = exec_load tge t rs m rd ra ofs.
-Proof.
- intros. unfold exec_load. rewrite eval_offset_preserved. reflexivity.
-Qed.
-
-Lemma transf_exec_store:
- forall t rs m rs0 ra ofs, exec_store ge t rs m rs0 ra ofs = exec_store tge t rs m rs0 ra ofs.
-Proof.
- intros. unfold exec_store. rewrite eval_offset_preserved. reflexivity.
-Qed.
-
-Lemma transf_exec_basic_instr:
- forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m.
-Proof.
- intros. pose symbol_address_preserved.
- unfold exec_basic_instr. exploreInst; simpl; auto; try congruence.
- 1: unfold exec_arith_instr; exploreInst; simpl; auto; try congruence.
- 1-10: apply transf_exec_load.
- all: apply transf_exec_store.
-Qed.
-
-Lemma transf_exec_body:
- forall bdy rs m, exec_body ge bdy rs m = exec_body tge bdy rs m.
-Proof.
- induction bdy; intros.
- - simpl. reflexivity.
- - simpl. rewrite transf_exec_basic_instr.
- destruct (exec_basic_instr _ _ _); auto.
-Qed.
-
-Lemma transf_exec_bblock:
- forall f tf bb rs m,
- 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.
-
-Lemma transf_step_simu:
- forall tf b lbb ofs c tbb rs m rs' m',
- Genv.find_funct_ptr tge b = Some (Internal tf) ->
- 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').
-Proof.
- induction lbb.
- - intros until m'. simpl. intros. discriminate.
- - intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB.
- destruct lbb.
- + simpl in *. clear IHlbb. inv CONC. eapply plus_one. econstructor; eauto. eapply find_bblock_tail; eauto.
- + exploit concat_all_exec_bblock; eauto; try discriminate.
- intros (tbb0 & rs0 & m0 & CONC0 & EXEB0 & PCeq' & EXEB1).
- eapply plus_left.
- econstructor.
- 3: eapply find_bblock_tail. rewrite <- app_comm_cons in TAIL. 3: eauto.
- all: eauto.
- 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' (MS: match_states s1 s1'),
- (exists s2', plus step 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).
- assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned).
- eapply transf_function_no_overflow; eauto.
-
- erewrite transf_exec_bblock in H2; eauto.
- inv BBEQ. rewrite H3 in H2.
- 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.
-
- - 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.
- eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-Qed.
-
-Theorem transf_program_correct:
- forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog).
-Proof.
- eapply forward_simulation_plus.
- - apply senv_preserved.
- - apply transf_initial_states.
- - apply transf_final_states.
- - apply transf_step_correct.
-Qed.
-
-End PRESERVATION.
+Require Import Coqlib Errors. +Require Import Integers Floats AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Op Locations Machblock Conventions Asmblock. +Require Import Asmblockgenproof0. +Require Import PostpassScheduling. +Require Import Asmblockgenproof. +Require Import Axioms. + +Local Open Scope error_monad_scope. + +Definition match_prog (p tp: Asmblock.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. + +Remark builtin_body_nil: + forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil. +Proof. + intros. destruct bb as [hd bdy ex WF]. simpl in *. + apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1. + eapply H1; eauto. +Qed. + +Lemma verified_schedule_builtin_idem (ge: Genv.t fundef unit) (fn: function): + forall bb ef args res lbb, + exit bb = Some (PExpand (Pbuiltin ef args res)) -> + verified_schedule bb = OK lbb -> + lbb = bb :: nil. +Proof. + intros. exploit builtin_body_nil; eauto. intros. + rewrite verified_schedule_single_inst in H0; auto. + - inv H0. auto. + - unfold size. rewrite H. rewrite H1. simpl. auto. +Qed. + +Lemma exec_body_app: + forall l l' ge rs m rs'' m'', + exec_body ge (l ++ l') rs m = Next rs'' m'' -> + exists rs' m', + exec_body ge l rs m = Next rs' m' + /\ exec_body ge l' rs' m' = Next rs'' m''. +Proof. + induction l. + - intros. simpl in H. repeat eexists. auto. + - intros. rewrite <- app_comm_cons in H. simpl in H. + destruct (exec_basic_instr ge a rs m) eqn:EXEBI. + + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2). + repeat eexists. simpl. rewrite EXEBI. eauto. auto. + + discriminate. +Qed. + +Lemma exec_body_pc: + forall l ge rs1 m1 rs2 m2, + exec_body ge l rs1 m1 = Next rs2 m2 -> + rs2 PC = rs1 PC. +Proof. + induction l. + - intros. inv H. auto. + - intros until m2. intro EXEB. + inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate. + eapply IHl in H0. rewrite H0. + erewrite exec_basic_instr_pc; eauto. +Qed. + +Lemma next_eq {A: Type}: + forall (rs rs':A) m m', + rs = rs' -> m = m' -> Next rs m = Next rs' m'. +Proof. + intros. congruence. +Qed. + +Lemma regset_double_set: + forall r1 r2 (rs: regset) v1 v2, + r1 <> r2 -> + (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1). +Proof. + intros. apply functional_extensionality. intros r. destruct (preg_eq r r1). + - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto. + - destruct (preg_eq r r2). + + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto. + + repeat (rewrite Pregmap.gso; auto). +Qed. + +Lemma regset_double_set_id: + forall r (rs: regset) v1 v2, + (rs # r <- v1 # r <- v2) = (rs # r <- v2). +Proof. + intros. apply functional_extensionality. intros. destruct (preg_eq r x). + - subst r. repeat (rewrite Pregmap.gss; auto). + - repeat (rewrite Pregmap.gso); auto. +Qed. + +Lemma exec_load_pc_var: + forall ge t rs m rd ra ofs rs' m' v, + exec_load ge t rs m rd ra ofs = Next rs' m' -> + exec_load ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. + destruct (Mem.loadv _ _ _). + - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. + - discriminate. +Qed. + +Lemma exec_store_pc_var: + forall ge t rs m rd ra ofs rs' m' v, + exec_store ge t rs m rd ra ofs = Next rs' m' -> + exec_store ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. + destruct (Mem.storev _ _ _). + - inv H. apply next_eq; auto. + - discriminate. +Qed. + +Lemma exec_basic_instr_pc_var: + forall ge i rs m rs' m' v, + exec_basic_instr ge i rs m = Next rs' m' -> + exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'. +Proof. + intros. unfold exec_basic_instr in *. destruct i. + - unfold exec_arith_instr in *. destruct i; destruct i. + all: try (exploreInst; inv H; apply next_eq; auto; + apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). + + (* Some cases treated seperately because exploreInst destructs too much *) + all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). + - exploreInst; apply exec_load_pc_var; auto. + - exploreInst; apply exec_store_pc_var; auto. + - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate). + destruct (Mem.storev _ _ _ _); try discriminate. + inv H. apply next_eq; auto. apply functional_extensionality. intros. + rewrite (regset_double_set GPR32 PC); try discriminate. + rewrite (regset_double_set GPR12 PC); try discriminate. + rewrite (regset_double_set GPR14 PC); try discriminate. reflexivity. + - repeat (rewrite Pregmap.gso; try discriminate). + destruct (Mem.loadv _ _ _); try discriminate. + destruct (rs GPR12); try discriminate. + destruct (Mem.free _ _ _ _); try discriminate. + inv H. apply next_eq; auto. + rewrite (regset_double_set GPR32 PC). + rewrite (regset_double_set GPR12 PC). reflexivity. + all: discriminate. + - destruct rs0; try discriminate. inv H. apply next_eq; auto. + repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate. + - destruct rd; try discriminate. inv H. apply next_eq; auto. + repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate. + - inv H. apply next_eq; auto. +Qed. + +Lemma exec_body_pc_var: + forall l ge rs m rs' m' v, + exec_body ge l rs m = Next rs' m' -> + exec_body ge l (rs # PC <- v) m = Next (rs' # PC <- v) m'. +Proof. + induction l. + - intros. simpl. simpl in H. inv H. auto. + - intros. simpl in *. + destruct (exec_basic_instr ge a rs m) eqn:EXEBI; try discriminate. + erewrite exec_basic_instr_pc_var; eauto. +Qed. + +Lemma pc_set_add: + forall rs v r x y, + 0 <= x <= Ptrofs.max_unsigned -> + 0 <= y <= Ptrofs.max_unsigned -> + rs # r <- (Val.offset_ptr v (Ptrofs.repr (x + y))) = rs # r <- (Val.offset_ptr (rs # r <- (Val.offset_ptr v (Ptrofs.repr x)) r) (Ptrofs.repr y)). +Proof. + intros. apply functional_extensionality. intros r0. destruct (preg_eq r r0). + - subst. repeat (rewrite Pregmap.gss); auto. + destruct v; simpl; auto. + rewrite Ptrofs.add_assoc. + cutrewrite (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)); auto. + unfold Ptrofs.add. + cutrewrite (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)); auto. + repeat (rewrite Ptrofs.unsigned_repr); auto. + - repeat (rewrite Pregmap.gso; auto). +Qed. + +Lemma concat2_straight: + forall a b bb rs m rs'' m'' f ge, + concat2 a b = OK bb -> + exec_bblock ge f bb rs m = Next rs'' m'' -> + exists rs' m', + exec_bblock ge f a rs m = Next rs' m' + /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a)) + /\ exec_bblock ge f b rs' m' = Next rs'' m''. +Proof. + intros until ge. intros CONC2 EXEB. + exploit concat2_zlt_size; eauto. intros (LTA & LTB). + exploit concat2_noexit; eauto. intros EXA. + exploit concat2_decomp; eauto. intros. inv H. + unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate. + rewrite H0 in EXEB'. apply exec_body_app in EXEB'. destruct EXEB' as (rs1 & m1 & EXEB1 & EXEB2). + repeat eexists. + unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto. + exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto. + unfold exec_bblock. unfold nextblock. erewrite exec_body_pc_var; eauto. + rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id. + assert (size bb = size a + size b). + { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r. + repeat (rewrite Nat2Z.inj_add). omega. } + clear EXA H0 H1. rewrite H in EXEB. + assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. } + rewrite H0. rewrite <- pc_set_add; auto. + exploit AB.size_positive. instantiate (1 := a). intro. omega. + exploit AB.size_positive. instantiate (1 := b). intro. omega. +Qed. + +Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) : + forall a bb rs m lbb rs'' m'', + lbb <> nil -> + concat_all (a :: lbb) = OK bb -> + exec_bblock ge f bb rs m = Next rs'' m'' -> + exists bb' rs' m', + concat_all lbb = OK bb' + /\ exec_bblock ge f a rs m = Next rs' m' + /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a)) + /\ exec_bblock ge f bb' rs' m' = Next rs'' m''. +Proof. + intros until m''. intros Hnonil CONC EXEB. + simpl in CONC. + destruct lbb as [|b lbb]; try contradiction. clear Hnonil. + monadInv CONC. exploit concat2_straight; eauto. intros (rs' & m' & EXEB1 & PCeq & EXEB2). + exists x. repeat econstructor. all: eauto. +Qed. + +Lemma ptrofs_add_repr : + forall a b, + Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr a) (Ptrofs.repr b)) = Ptrofs.unsigned (Ptrofs.repr (a + b)). +Proof. + intros a b. + rewrite Ptrofs.add_unsigned. repeat (rewrite Ptrofs.unsigned_repr_eq). + rewrite <- Zplus_mod. auto. +Qed. + +Section PRESERVATION. + +Variables prog tprog: program. +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. +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. +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) -> + transf_function f = OK tf -> + Genv.find_funct_ptr tge fb = Some (Internal tf). +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. + +Lemma prog_main_preserved: + prog_main tprog = prog_main prog. +Proof (match_program_main TRANSL). + +Lemma prog_main_address_preserved: + (Genv.symbol_address (Genv.globalenv prog) (prog_main prog) Ptrofs.zero) = + (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero). +Proof. + unfold Genv.symbol_address. rewrite symbols_preserved. + rewrite prog_main_preserved. auto. +Qed. + +Lemma transf_initial_states: + forall st1, initial_state prog st1 -> + exists st2, initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inv H. + econstructor; split. + - eapply initial_state_intro. + eapply (Genv.init_mem_transf_partial TRANSL); eauto. + - econstructor; eauto. subst ge0. subst rs0. rewrite prog_main_address_preserved. auto. +Qed. + +Lemma transf_final_states: + forall st1 st2 r, + match_states st1 st2 -> final_state st1 r -> final_state st2 r. +Proof. + intros. inv H0. inv H. econstructor; eauto. +Qed. + +Lemma tail_find_bblock: + forall lbb pos bb, + find_bblock pos lbb = Some bb -> + exists c, code_tail pos lbb (bb::c). +Proof. + induction lbb. + - intros. simpl in H. inv H. + - intros. simpl in H. + destruct (zlt pos 0); try (inv H; fail). + destruct (zeq pos 0). + + inv H. exists lbb. constructor; auto. + + apply IHlbb in H. destruct H as (c & TAIL). exists c. + cutrewrite (pos = pos - size a + size a). apply code_tail_S; auto. + omega. +Qed. + +Lemma code_tail_head_app: + forall l pos c1 c2, + code_tail pos c1 c2 -> + code_tail (pos + size_blocks l) (l++c1) c2. +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. + +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'). +Proof. + induction c; intros. + - simpl in H. inv H. inv H0. + - inv H0. + + monadInv H. exists x0. + split; simpl; auto. eexists; eauto. econstructor; 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. + +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). +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. +Qed. + +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. + intros. simpl. auto. +Qed. + +Lemma verified_schedule_not_empty: + forall bb lbb, + verified_schedule bb = OK lbb -> lbb <> nil. +Proof. + intros. apply verified_schedule_size in H. + pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g. + destruct lbb; simpl in *; discriminate. +Qed. + +Lemma header_nil_label_pos_none: + forall lbb l p, + Forall (fun b => header b = nil) lbb -> label_pos l p lbb = None. +Proof. + induction lbb. + - intros. simpl. auto. + - intros. inv H. simpl. unfold is_label. rewrite H2. destruct (in_dec l nil). { inv i. } + auto. +Qed. + +Lemma verified_schedule_label: + forall bb tbb lbb l, + verified_schedule bb = OK (tbb :: lbb) -> + is_label l bb = is_label l tbb + /\ label_pos l 0 lbb = None. +Proof. + intros. exploit verified_schedule_header; eauto. + intros (HdrEq & HdrNil). + split. + - unfold is_label. rewrite HdrEq. reflexivity. + - apply header_nil_label_pos_none. assumption. +Qed. + +Lemma label_pos_app_none: + forall c c' l p p', + label_pos l p c = None -> + label_pos l (p' + size_blocks c) c' = label_pos l p' (c ++ c'). +Proof. + induction c. + - intros. simpl in *. rewrite Z.add_0_r. reflexivity. + - intros. simpl in *. destruct (is_label _ _) eqn:ISLABEL. + + discriminate. + + eapply IHc in H. rewrite Z.add_assoc. eauto. +Qed. + +Remark label_pos_pvar_none_add: + forall tc l p p' k, + label_pos l (p+k) tc = None -> label_pos l (p'+k) tc = None. +Proof. + induction tc. + - intros. simpl. auto. + - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL. + + discriminate. + + pose (IHtc l p p' (k + size a)). repeat (rewrite Z.add_assoc in e). auto. +Qed. + +Lemma label_pos_pvar_none: + forall tc l p p', + label_pos l p tc = None -> label_pos l p' tc = None. +Proof. + intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1. + eapply label_pos_pvar_none_add; eauto. +Qed. + +Remark label_pos_pvar_some_add_add: + forall tc l p p' k k', + label_pos l (p+k') tc = Some (p+k) -> label_pos l (p'+k') tc = Some (p'+k). +Proof. + induction tc. + - intros. simpl in H. discriminate. + - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL. + + inv H. assert (k = k') by omega. subst. reflexivity. + + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto. +Qed. + +Lemma label_pos_pvar_some_add: + forall tc l p p' k, + label_pos l p tc = Some (p+k) -> label_pos l p' tc = Some (p'+k). +Proof. + intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1. + eapply label_pos_pvar_some_add_add; eauto. +Qed. + +Remark label_pos_pvar_add: + forall c tc l p p' k, + label_pos l (p+k) c = label_pos l p tc -> + label_pos l (p'+k) c = label_pos l p' tc. +Proof. + induction c. + - intros. simpl in *. + exploit label_pos_pvar_none; eauto. + - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL. + + exploit label_pos_pvar_some_add; eauto. + + pose (IHc tc l p p' (k+size a)). repeat (rewrite Z.add_assoc in e). auto. +Qed. + +Lemma label_pos_pvar: + forall c tc l p p', + label_pos l p c = label_pos l p tc -> + label_pos l p' c = label_pos l p' tc. +Proof. + intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1. + eapply label_pos_pvar_add; eauto. +Qed. + +Lemma label_pos_head_app: + forall c bb lbb l tc p, + verified_schedule bb = OK lbb -> + label_pos l p c = label_pos l p tc -> + label_pos l p (bb :: c) = label_pos l p (lbb ++ tc). +Proof. + intros. simpl. destruct lbb as [|tbb lbb]. + - apply verified_schedule_not_empty in H. contradiction. + - simpl. exploit verified_schedule_label; eauto. intros (ISLBL & LBLPOS). + rewrite ISLBL. + destruct (is_label l tbb) eqn:ISLBL'; simpl; auto. + eapply label_pos_pvar in H0. erewrite H0. + erewrite verified_schedule_size; eauto. simpl size_blocks. rewrite Z.add_assoc. + erewrite label_pos_app_none; eauto. +Qed. + +Lemma label_pos_preserved: + forall c tc l, + transf_blocks c = OK tc -> label_pos l 0 c = label_pos l 0 tc. +Proof. + induction c. + - intros. simpl in *. inv H. reflexivity. + - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. eapply IHc in EQ. + eapply label_pos_head_app; eauto. +Qed. + +Lemma label_pos_preserved_blocks: + forall l f tf, + transf_function f = OK tf -> + label_pos l 0 (fn_blocks f) = label_pos l 0 (fn_blocks tf). +Proof. + intros. monadInv H. monadInv EQ. + destruct (zlt Ptrofs.max_unsigned _); try discriminate. + 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. +Proof. + intros. destruct ex; simpl; auto. + assert (ge = Genv.globalenv prog). auto. + assert (tge = Genv.globalenv tprog). auto. + pose symbol_address_preserved. + exploreInst; simpl; auto; try congruence. + - unfold goto_label. erewrite label_pos_preserved_blocks; eauto. + - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto. + - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto. + - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto. + - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto. +Qed. + +Lemma eval_offset_preserved: + forall ofs, eval_offset ge ofs = eval_offset tge ofs. +Proof. + intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto. +Qed. + +Lemma transf_exec_load: + forall t rs m rd ra ofs, exec_load ge t rs m rd ra ofs = exec_load tge t rs m rd ra ofs. +Proof. + intros. unfold exec_load. rewrite eval_offset_preserved. reflexivity. +Qed. + +Lemma transf_exec_store: + forall t rs m rs0 ra ofs, exec_store ge t rs m rs0 ra ofs = exec_store tge t rs m rs0 ra ofs. +Proof. + intros. unfold exec_store. rewrite eval_offset_preserved. reflexivity. +Qed. + +Lemma transf_exec_basic_instr: + forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m. +Proof. + intros. pose symbol_address_preserved. + unfold exec_basic_instr. exploreInst; simpl; auto; try congruence. + 1: unfold exec_arith_instr; exploreInst; simpl; auto; try congruence. + 1-10: apply transf_exec_load. + all: apply transf_exec_store. +Qed. + +Lemma transf_exec_body: + forall bdy rs m, exec_body ge bdy rs m = exec_body tge bdy rs m. +Proof. + induction bdy; intros. + - simpl. reflexivity. + - simpl. rewrite transf_exec_basic_instr. + destruct (exec_basic_instr _ _ _); auto. +Qed. + +Lemma transf_exec_bblock: + forall f tf bb rs m, + 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. + +Lemma transf_step_simu: + forall tf b lbb ofs c tbb rs m rs' m', + Genv.find_funct_ptr tge b = Some (Internal tf) -> + 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'). +Proof. + induction lbb. + - intros until m'. simpl. intros. discriminate. + - intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB. + destruct lbb. + + simpl in *. clear IHlbb. inv CONC. eapply plus_one. econstructor; eauto. eapply find_bblock_tail; eauto. + + exploit concat_all_exec_bblock; eauto; try discriminate. + intros (tbb0 & rs0 & m0 & CONC0 & EXEB0 & PCeq' & EXEB1). + eapply plus_left. + econstructor. + 3: eapply find_bblock_tail. rewrite <- app_comm_cons in TAIL. 3: eauto. + all: eauto. + 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' (MS: match_states s1 s1'), + (exists s2', plus step 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). + assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + + erewrite transf_exec_bblock in H2; eauto. + inv BBEQ. rewrite H3 in H2. + 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. + + - 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. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. +Qed. + +Theorem transf_program_correct: + forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog). +Proof. + eapply forward_simulation_plus. + - apply senv_preserved. + - apply transf_initial_states. + - apply transf_final_states. + - apply transf_step_correct. +Qed. + +End PRESERVATION. |