diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-14 17:54:52 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-14 17:54:52 +0100 |
commit | 3a1f893783ce2933cb1fc57504a482f3684c5720 (patch) | |
tree | be7170a97db53e1232f41fcf2a07ec2aef3facdb | |
parent | 35b2c76267c50eb56cfa89371a3627f1bd46ff1b (diff) | |
download | compcert-kvx-3a1f893783ce2933cb1fc57504a482f3684c5720.tar.gz compcert-kvx-3a1f893783ce2933cb1fc57504a482f3684c5720.zip |
More lemmas in PostpassScheduling
-rw-r--r-- | mppa_k1c/PostpassScheduling.v | 32 |
1 files changed, 26 insertions, 6 deletions
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 6f26ac58..64ad0db6 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -57,6 +57,18 @@ Axiom forward_simu: exec' ge fn (trans_block b) rs1' m1' = Next' rs2' m2'
/\ match_states (State rs2 m2) (State' rs2' m2').
+Axiom forward_simu_stuck:
+ forall rs1 m1 rs1' m1' b ge fn,
+ exec ge fn b rs1 m1 = Stuck ->
+ match_states (State rs1 m1) (State' rs1' m1') ->
+ exec' ge fn (trans_block b) rs1' m1' = Stuck'.
+
+Axiom trans_block_reverse_stuck:
+ forall ge fn b rs m rs' m',
+ exec' ge fn (trans_block b) rs' m' = Stuck' ->
+ match_states (State rs m) (State' rs' m') ->
+ exec ge fn b rs m = Stuck.
+
Axiom state_equiv:
forall S1 S2 S', match_states S1 S' /\ match_states S2 S' -> S1 = S2.
@@ -72,14 +84,22 @@ Lemma trans_state_State: forall rs m,
exists rs' m', trans_state (State rs m) = State' rs' m'.
Proof.
-Admitted.
+ intros. destruct (trans_state _). eauto.
+Qed.
Lemma trans_equiv_stuck:
- forall b1 b2 ge fn rs1 m1 rs2 m2,
+ forall b1 b2 ge fn rs m,
bblock_equiv' ge fn (trans_block b1) (trans_block b2) ->
- (exec ge fn b1 rs1 m1 = Stuck <-> exec ge fn b2 rs2 m2 = Stuck).
+ (exec ge fn b1 rs m = Stuck <-> exec ge fn b2 rs m = Stuck).
Proof.
-Admitted.
+ intros. inv H.
+ pose (trans_state_match (State rs m)). pose (trans_state_State rs m). destruct e as (rs' & m' & TST). rewrite TST in m0. clear TST.
+ split.
+ - intros. eapply forward_simu_stuck in H; eauto. rewrite H0 in H. eapply trans_block_reverse_stuck; eassumption.
+ - intros. eapply forward_simu_stuck in H; eauto. rewrite <- H0 in H. eapply trans_block_reverse_stuck; eassumption.
+Qed.
+
+
Lemma bblock_equiv'_comm:
forall ge fn b1 b2,
@@ -105,8 +125,8 @@ Proof. rewrite H0 in EXEB'. rewrite EXEB'2 in EXEB'. inv EXEB'.
exploit (state_equiv (State rs2 m2) (State rs3 m3) (State' rs2' m2')). eauto.
congruence.
- - rewrite trans_equiv_stuck in EXEB2. 2: eapply bblock_equiv'_comm; eauto. rewrite EXEB2 in EXEB. discriminate.
- - rewrite trans_equiv_stuck in EXEB; eauto. rewrite EXEB in EXEB2. discriminate.
+ - rewrite trans_equiv_stuck in EXEB2. 2: eapply bblock_equiv'_comm; eauto. unfold exec in EXEB2. rewrite EXEB2 in EXEB. discriminate.
+ - rewrite trans_equiv_stuck in EXEB; eauto. unfold exec in EXEB. rewrite EXEB in EXEB2. discriminate.
Qed.
|