diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-25 15:29:32 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-25 15:29:32 +0100 |
| commit | e61639d96fdeb361188a9a93e5d0648f0386a849 (patch) | |
| tree | 7e887a42688fe73852aa8a32baaf8d258df3b0c2 /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 6a2030b349446e749297c50f74c237bbce6dbd1a (diff) | |
| download | compcert-kvx-e61639d96fdeb361188a9a93e5d0648f0386a849.tar.gz compcert-kvx-e61639d96fdeb361188a9a93e5d0648f0386a849.zip | |
Avancement PostpassSchedulingproof
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 74 |
1 files changed, 69 insertions, 5 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 56662a0a..ef9f5f0d 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -16,6 +16,7 @@ Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Machblock Conventions Asmblock.
Require Import Asmblockgenproof0.
Require Import PostpassScheduling.
+Require Import Asmblockgenproof.
Local Open Scope error_monad_scope.
@@ -135,7 +136,64 @@ Proof. subst exa.
unfold concat2 in H; simpl in H.
destruct hdb.
-Admitted.
+ - destruct exb.
+ + destruct c.
+ * destruct i. discriminate.
+ * monadInv H. split; auto.
+ + monadInv H. split; auto.
+ - discriminate.
+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 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 *. exploreInst.
+ - inv H. unfold exec_arith_instr. exploreInst. Search (_ # _ <- _).
+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.
+ +
+Qed. *)
+
Lemma concat2_straight:
forall a b bb rs m rs'' m'' f ge,
@@ -147,12 +205,18 @@ Lemma concat2_straight: /\ exec_bblock ge f b rs' m' = Next rs'' m''.
Proof.
intros.
-
-
- apply concat2_noexit in H. destruct a as [hd bdy ex WF]. simpl in *. subst ex.
- repeat eexists. unfold exec_bblock. simpl.
+ exploit concat2_noexit; eauto. intros.
+ exploit concat2_decomp; eauto. intros. inv H2.
+(* destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bd ex WF]. *)
+ unfold exec_bblock in H0. destruct (exec_body ge (body bb) rs m) eqn:EXEB.
+ - rewrite H3 in EXEB. apply exec_body_app in EXEB. destruct EXEB as (rs1 & m1 & EXEB1 & EXEB2).
+ repeat eexists.
+ unfold exec_bblock. rewrite EXEB1. rewrite H1. simpl. eauto.
+ exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H2. auto.
+ unfold exec_bblock.
Admitted.
+
Lemma concat_exec_bblock_nonil (ge: Genv.t fundef unit) (f: function) :
forall a bb rs m lbb rs'' m'',
lbb <> nil ->
|