diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-08 14:50:34 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-08 14:50:34 +0200 |
| commit | a57ba1a8a0036853cac31d9401a6f71b877e70c1 (patch) | |
| tree | e1cab9e85e4a90fb41c3db8784033991f39f1e78 /mppa_k1c | |
| parent | 2b2ad7fc33fecfd77598e485ae0af82be3f23471 (diff) | |
| download | compcert-kvx-a57ba1a8a0036853cac31d9401a6f71b877e70c1.tar.gz compcert-kvx-a57ba1a8a0036853cac31d9401a6f71b877e70c1.zip | |
a couple "Admitted" and the Coq compiles
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 30 |
1 files changed, 18 insertions, 12 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 21af276b..867c10c5 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -96,36 +96,42 @@ Proof. Qed. Lemma exec_load_offset_pc_var: - forall t rs m rd ra ofs rs' m' v, - exec_load_offset t rs m rd ra ofs = Next rs' m' -> - exec_load_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. + forall trap t rs m rd ra ofs rs' m' v, + exec_load_offset trap t rs m rd ra ofs = Next rs' m' -> + exec_load_offset trap t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ofs); try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - discriminate. + - unfold parexec_incorrect_load in *. + destruct trap; try discriminate. + inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. Qed. Lemma exec_load_reg_pc_var: - forall t rs m rd ra ro rs' m' v, - exec_load_reg t rs m rd ra ro = Next rs' m' -> - exec_load_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. + forall trap t rs m rd ra ro rs' m' v, + exec_load_reg trap t rs m rd ra ro = Next rs' m' -> + exec_load_reg trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. Proof. intros. unfold exec_load_reg in *. unfold parexec_load_reg in *. rewrite Pregmap.gso; try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - discriminate. + - unfold parexec_incorrect_load in *. + destruct trap; try discriminate. + inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. Qed. Lemma exec_load_regxs_pc_var: - forall t rs m rd ra ro rs' m' v, - exec_load_regxs t rs m rd ra ro = Next rs' m' -> - exec_load_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. + forall trap t rs m rd ra ro rs' m' v, + exec_load_regxs trap t rs m rd ra ro = Next rs' m' -> + exec_load_regxs trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. Proof. intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - discriminate. + - unfold parexec_incorrect_load in *. + destruct trap; try discriminate. + inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. Qed. Lemma exec_load_offset_q_pc_var: |