diff options
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 157 |
1 files changed, 55 insertions, 102 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index a5880128..92630772 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -810,80 +810,78 @@ Proof. destruct (ireg_eq g rd); subst; Simpl. Qed. -Lemma forward_simu_basic: - forall ge fn b rs m rs' m' s, - exec_basic_instr ge b rs m = Next rs' m' -> +Theorem forward_simu_basic_gen ge fn b rs m s: match_states (State rs m) s -> - exists s', - inst_run (Genv ge fn) (trans_basic b) s s = Some s' - /\ match_states (State rs' m') s'. + match_outcome (exec_basic_instr ge b rs m) (inst_run (Genv ge fn) (trans_basic b) s s). Proof. - intros. destruct b. + intros. destruct b; inversion H; simpl. (* Arith *) - - simpl in H. inv H. simpl inst_run. eapply trans_arith_correct; eauto. + - eapply trans_arith_correct; eauto. (* Load *) - - simpl in H. destruct i. + - destruct i. (* Load Offset *) - + destruct i. all: - unfold exec_load_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; - destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0; - eexists; split; try split; [ - simpl; rewrite EVALOFF; rewrite H; rewrite (H1 ra); simpl in MEML; rewrite MEML; reflexivity - | Simpl - | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. - (* Load Reg *) - + destruct i. all: - unfold exec_load_reg in H; destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0; - eexists; split; try split; - [ simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); unfold exec_load_deps_reg; simpl in MEML; rewrite MEML; reflexivity - | Simpl - | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. + + destruct i; simpl; + unfold exec_load_offset; rewrite (H1 ra); rewrite H0; + destruct (eval_offset _ _); simpl; auto; destruct (Mem.loadv _ _); simpl; auto; + eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + + destruct i; simpl; + unfold exec_load_reg; rewrite (H1 ra); rewrite (H1 rofs); rewrite H0; unfold exec_load_deps_reg; + destruct (Mem.loadv _ _); simpl; auto; + eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. (* Store *) - - simpl in H. destruct i. + - destruct i. (* Store Offset *) - + destruct i. all: - unfold exec_store_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; - destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0; - eexists; split; try split; - [ simpl; rewrite EVALOFF; rewrite H; rewrite (H1 ra); rewrite (H1 rs0); simpl in MEML; rewrite MEML; reflexivity - | Simpl - | intros rr; destruct rr; Simpl ]. - (* Store Reg *) - + destruct i. all: - unfold exec_store_reg in H; - destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0; - eexists; split; try split; - [ simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); rewrite (H1 rs0); unfold exec_store_deps_reg; - simpl in MEML; rewrite MEML; reflexivity - | Simpl - | intros rr; destruct rr; Simpl ]. + + destruct i; simpl; + rewrite (H1 rs0); rewrite (H1 ra); rewrite H0; unfold exec_store_offset; destruct (eval_offset _ _); simpl; auto; + destruct (Mem.storev _ _ _ _); simpl; auto; + eexists; split; try split; Simpl; intros rr; destruct rr; Simpl. + + + destruct i; simpl; + rewrite (H1 rs0); rewrite (H1 ra); rewrite (H1 rofs); rewrite H0; unfold exec_store_reg; unfold exec_store_deps_reg; + destruct (Mem.storev _ _ _ _); simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl. (* Allocframe *) - - simpl in H. destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS; try discriminate. - inv H. inv H0. eexists. split; try split. - * simpl. Simpl. pose (H1 GPR12); simpl in e; rewrite e. rewrite H. rewrite MEMAL. rewrite MEMS. Simpl. - rewrite H. rewrite MEMAL. rewrite MEMS. reflexivity. + - Simpl. rewrite (H1 SP). rewrite H0. destruct (Mem.alloc _ _ _) eqn:ALLOC; simpl; auto. destruct (Mem.store _ _ _ _) eqn:STORE; simpl; auto. + eexists; split; try split. + * Simpl. rewrite H0. rewrite ALLOC. rewrite STORE. reflexivity. * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl. + * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl. + (* Freeframe *) - - simpl in H. destruct (Mem.loadv _ _ _) eqn:MLOAD; try discriminate. destruct (rs GPR12) eqn:SPeq; try discriminate. - destruct (Mem.free _ _ _ _) eqn:MFREE; try discriminate. inv H. inv H0. - eexists. split; try split. - * simpl. pose (H1 GPR12); simpl in e; rewrite e. rewrite H. rewrite SPeq. rewrite MLOAD. rewrite MFREE. - Simpl. rewrite e. rewrite SPeq. rewrite MLOAD. rewrite MFREE. reflexivity. + - rewrite (H1 SP). rewrite H0. destruct (Mem.loadv _ _ _) eqn:LOAD; simpl; auto. destruct (rs GPR12) eqn:SPeq; simpl; auto. + destruct (Mem.free _ _ _ _) eqn:FREE; simpl; auto. Simpl. rewrite (H1 SP). eexists; split; try split. + * rewrite SPeq. rewrite LOAD. rewrite FREE. reflexivity. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl. + (* Pget *) - - simpl in H. destruct rs0 eqn:rs0eq; try discriminate. inv H. inv H0. - eexists. split; try split. Simpl. intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. + - destruct rs0; simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. + (* Pset *) - - simpl in H. destruct rd eqn:rdeq; try discriminate. inv H. inv H0. - eexists. split; try split. Simpl. intros rr; destruct rr; Simpl. + - destruct rd; simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. + (* Pnop *) - - simpl in H. inv H. inv H0. eexists. split; try split. assumption. assumption. + - eexists; split; try split. assumption. assumption. +Qed. + +Lemma forward_simu_basic ge fn b rs m rs' m' s: + exec_basic_instr ge b rs m = Next rs' m' -> + match_states (State rs m) s -> + exists s', + inst_run (Genv ge fn) (trans_basic b) s s = Some s' + /\ match_states (State rs' m') s'. +Proof. + intros. exploit forward_simu_basic_gen; eauto. intros. rewrite H in H1. inv H1. eexists. eassumption. +Qed. + +Lemma forward_simu_basic_instr_stuck i ge fn rs m s: + Ge = Genv ge fn -> + exec_basic_instr ge i rs m = Stuck -> + match_states (State rs m) s -> + exec Ge [trans_basic i] s = None. +Proof. + intros. exploit forward_simu_basic_gen; eauto. intros. rewrite H0 in H2. inv H2. unfold exec. unfold run. rewrite H4. reflexivity. Qed. Lemma forward_simu_body: @@ -1147,51 +1145,6 @@ Proof. - left. reflexivity. Qed. -Lemma forward_simu_basic_instr_stuck: - forall i ge fn rs m s, - Ge = Genv ge fn -> - exec_basic_instr ge i rs m = Stuck -> - match_states (State rs m) s -> - exec Ge [trans_basic i] s = None. -Proof. - intros. inv H1. unfold exec_basic_instr in H0. destruct i; try discriminate. -(* PLoad *) - - destruct i. - (* Load Offset *) - + destruct i. all: - simpl; rewrite H2; rewrite (H3 ra); unfold exec_load_offset in H0; destruct (eval_offset _ _); auto; - simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate. - (* Load Reg *) - + destruct i. all: - simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); unfold exec_load_reg in H0; unfold exec_load_deps_reg; - destruct (rs rofs); auto; simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate. - -(* PStore *) - - destruct i. - (* Store Offset *) - + destruct i. all: - simpl; rewrite H2; rewrite (H3 ra); rewrite (H3 rs0); unfold exec_store_offset in H0; destruct (eval_offset _ _); auto; - simpl in H0; destruct (Mem.storev _ _ _); auto; discriminate. - (* Store Reg *) - + destruct i. all: - simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); rewrite (H3 rs0); simpl in H0; unfold exec_store_reg in H0; - unfold exec_store_deps_reg; destruct (rs rofs); auto; - destruct (Mem.storev _ _ _ _); auto; discriminate. - -(* Pallocframe *) - - simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2. destruct (Mem.alloc _ _ _). simpl in H0. - destruct (Mem.store _ _ _ _); try discriminate. reflexivity. -(* Pfreeframe *) - - simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2. - destruct (Mem.loadv _ _ _); auto. destruct (rs GPR12); auto. destruct (Mem.free _ _ _ _); auto. - discriminate. -(* Pget *) - - simpl. destruct rs0; subst; try discriminate. - all: simpl; auto. - - simpl. destruct rd; subst; try discriminate. - all: simpl; auto. -Qed. - Lemma forward_simu_body_stuck: forall bdy ge fn rs m s, Ge = Genv ge fn -> |