From e312c62c864611d88651bf745a14a67de40e3fd6 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 12 Mar 2019 15:28:49 +0100 Subject: fix trans_pcincr for parcheck. (Proof is broken. cf FIXME) --- mppa_k1c/Asmblockdeps.v | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'mppa_k1c') 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). -- cgit