diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-04-03 16:32:59 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-04-03 16:32:59 +0200 |
| commit | e0fb40f126c980819869bf2a2f32f7332b1b4a5a (patch) | |
| tree | e80686110986df274bb14e1bb167c446ff4dacab /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 34261e53d0da905307eb3e0a0b711571365b078e (diff) | |
| download | compcert-kvx-e0fb40f126c980819869bf2a2f32f7332b1b4a5a.tar.gz compcert-kvx-e0fb40f126c980819869bf2a2f32f7332b1b4a5a.zip | |
Preuve des load/store registre registre. Reste des modifs mineures dans les preuves de Asmblockdeps
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 77014bdc..c5f432a6 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -100,7 +100,7 @@ Lemma exec_load_offset_pc_var: exec_load_offset ge t rs m rd ra ofs = Next rs' m' -> exec_load_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. - intros. unfold exec_load_offset in *. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. + intros. unfold exec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - discriminate. @@ -111,7 +111,7 @@ Lemma exec_load_reg_pc_var: 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'. Proof. - intros. unfold exec_load_reg in *. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (rs ro); try discriminate. + intros. unfold exec_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. @@ -122,7 +122,7 @@ Lemma exec_store_offset_pc_var: exec_store_offset ge t rs m rd ra ofs = Next rs' m' -> exec_store_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. - intros. unfold exec_store_offset in *. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. + intros. unfold exec_store_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. destruct (Mem.storev _ _ _). - inv H. apply next_eq; auto. @@ -134,8 +134,7 @@ Lemma exec_store_reg_pc_var: exec_store_reg t rs m rd ra ro = Next rs' m' -> exec_store_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. Proof. - intros. unfold exec_store_reg in *. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. - destruct (rs ro); try discriminate. + intros. unfold exec_store_reg in *. rewrite Pregmap.gso; try discriminate. destruct (Mem.storev _ _ _). - inv H. apply next_eq; auto. - discriminate. |