diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-07-30 11:33:51 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-07-30 11:33:51 +0200 |
| commit | 5b4560bd853cbcf1ef195da1b625f37609ec00ec (patch) | |
| tree | 985a9b244ccb9a9a7b3370f72a841d170ad824c0 /mppa_k1c/Asmblockdeps.v | |
| parent | 211382d21013c038c3c716454fcfa5a375dba8ba (diff) | |
| download | compcert-kvx-5b4560bd853cbcf1ef195da1b625f37609ec00ec.tar.gz compcert-kvx-5b4560bd853cbcf1ef195da1b625f37609ec00ec.zip | |
(#139) - Quelques renommages
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 9855afa2..a7fa5cff 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -846,7 +846,7 @@ Theorem bisimu_par_wio_basic ge fn rsr rsw mr mw sr sw bi: Ge = Genv ge fn -> match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> - match_outcome (parexec_basic_instr ge bi rsr rsw mr mw) (inst_prun Ge (trans_basic bi) sw sr sr). + match_outcome (bstep ge bi rsr rsw mr mw) (inst_prun Ge (trans_basic bi) sw sr sr). Proof. (* a little tactic to automate reasoning on preg_eq *) @@ -1004,7 +1004,7 @@ Proof. induction bdy as [|i bdy]; simpl; eauto. intros. exploit (bisimu_par_wio_basic ge fn rsr rsw mr mw sr sw i); eauto. - destruct (parexec_basic_instr _ _ _ _ _ _); simpl. + destruct (bstep _ _ _ _ _ _); simpl. - intros (s' & X1 & X2). rewrite X1; simpl; eauto. - intros X; rewrite X; simpl; auto. Qed. @@ -1015,7 +1015,7 @@ Theorem bisimu_par_control ex sz aux ge fn rsr rsw mr mw sr sw: match_states (State rsw mw) sw -> match_outcome (parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) (rsw#PC <- aux) mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). Proof. - intros GENV MSR MSW; unfold parexec_exit. + intros GENV MSR MSW; unfold estep. simpl in *. inv MSR. inv MSW. destruct ex. - destruct c; destruct i; try discriminate; simpl. @@ -1071,9 +1071,9 @@ Theorem bisimu_par_exit ex sz ge fn rsr rsw mr mw sr sw: Ge = Genv ge fn -> match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> - match_outcome (parexec_exit ge fn ex (Ptrofs.repr sz) rsr rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). + match_outcome (estep ge fn ex (Ptrofs.repr sz) rsr rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). Proof. - intros; unfold parexec_exit. + intros; unfold estep. exploit (bisimu_par_control ex sz rsw#PC ge fn rsr rsw mr mw sr sw); eauto. cutrewrite (rsw # PC <- (rsw PC) = rsw); auto. apply extensionality. intros; destruct x; simpl; auto. |