fix trans_pcincr for parcheck. (Proof is broken. cf FIXME)

1 files changed, 12 insertions, 12 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index b93a9e59..c58b2973 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -468,10 +468,10 @@ Definition trans_control (ctl: control) : macro :=
   | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)]
   end.
 
-Definition trans_exit (ex: option control) : list L.macro :=
+Definition trans_exit (ex: option control) : L.macro :=
   match ex with
-  | None => nil
-  | Some ctl => trans_control ctl :: nil
+  | None => []
+  | Some ctl => trans_control ctl
   end
 .
 
@@ -516,10 +516,10 @@ Fixpoint trans_body (b: list basic) : list L.macro :=
   | b :: lb => (trans_basic b) :: (trans_body lb)
   end.
 
-Definition trans_pcincr (sz: Z) := [(#PC, Op (Control (OIncremPC sz)) (Name (#PC) @ Enil))] :: nil.
+Definition trans_pcincr (sz: Z) (k: L.macro) := [(#PC, Op (Control (OIncremPC sz)) (Name (#PC) @ Enil)) :: k].
 
 Definition trans_block (b: Asmblock.bblock) : L.bblock :=
-  trans_body (body b) ++ trans_pcincr (size b) ++ trans_exit (exit b).
+  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.
@@ -812,7 +812,7 @@ Lemma forward_simu_control:
   exec_control ge fn ex (nextblock b rs) m = Next rs2 m2 ->
   match_states (State rs m) s ->
   exists s',
-     exec Ge (trans_pcincr (size b) ++ trans_exit ex) s = Some s'
+     exec Ge (trans_pcincr (size b) (trans_exit ex)) s = Some s'
   /\ match_states (State rs2 m2) s'.
 Proof.
   intros. destruct ex.
@@ -967,21 +967,21 @@ Lemma exec_trans_pcincr_exec:
   forall rs m s b,
   match_states (State rs m) s ->
   exists s',
-     exec Ge (trans_pcincr (size b) ++ trans_exit (exit b)) s = exec Ge (trans_exit (exit b)) s'
+     exec Ge (trans_pcincr (size b) (trans_exit (exit b))) s = exec Ge [trans_exit (exit b)] s'
   /\ match_states (State (nextblock b rs) m) s'.
 Proof.
   intros. inv H. eexists. split. simpl.
-  unfold control_eval. pose (H1 PC); simpl in e; rewrite e. destruct Ge. reflexivity.
+  unfold control_eval. pose (H1 PC); simpl in e; rewrite e. destruct Ge. (* eapply eq_refl.
   simpl. split.
   - Simpl.
-  - intros rr; destruct rr; Simpl.
-Qed.
+  - intros rr; destruct rr; Simpl.*)
+Admitted. (* FIXME *)
 
 Lemma exec_exit_none:
   forall ge fn rs m s ex,
   Ge = Genv ge fn ->
   match_states (State rs m) s ->
-  exec Ge (trans_exit ex) s = None ->
+  exec Ge [trans_exit ex] s = None ->
   exec_control ge fn ex rs m = Stuck.
 Proof.
   intros. inv H0. destruct ex as [ctl|]; try discriminate.
@@ -1092,7 +1092,7 @@ Lemma forward_simu_exit_stuck:
   Ge = Genv ge fn ->
   exec_control ge fn ex rs m = Stuck ->
   match_states (State rs m) s ->
-  exec Ge (trans_exit ex) s = None.
+  exec Ge [(trans_exit ex)] s = None.
 Proof.
   intros. inv H1. destruct ex as [ctl|]; try discriminate.
   destruct ctl; destruct i; try discriminate; try (simpl; reflexivity).