diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-04 09:25:25 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-04 09:25:25 +0200 |
| commit | c73ab51128c8fdbac327292f46cab289dd69fee5 (patch) | |
| tree | 28387cb9861201ad1c893bebac73fc672a530f2b /mppa_k1c/Asmblockdeps.v | |
| parent | 5abd0529197507395b83fc44f1e1a6fb6ac0096e (diff) | |
| parent | 064d62912f52ddb8d6666bc546ca141ac6575d5a (diff) | |
| download | compcert-kvx-c73ab51128c8fdbac327292f46cab289dd69fee5.tar.gz compcert-kvx-c73ab51128c8fdbac327292f46cab289dd69fee5.zip | |
Merge branch 'mppa-peephole' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-peephole
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index baaff273..77cc02e4 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -908,8 +908,7 @@ Proof. (* Load Quad word *) + unfold parexec_load_q_offset. destruct (gpreg_q_expand rd) as [rd0 rd1]. - destruct (ireg_eq rd0 ra) as [ OVERLAP0 | NOOVERLAP0 ]. - simpl. trivial. + destruct (ireg_eq rd0 ra) as [ OVERLAP0 | NOOVERLAP0 ]; simpl; auto. unfold exec_load_deps_offset. destruct Ge. unfold eval_offset. @@ -1081,12 +1080,10 @@ Proof. (* Store Quad Word *) + unfold parexec_store_q_offset. - simpl. destruct (gpreg_q_expand rs) as [s0 s1]. simpl. unfold exec_store_deps_offset. - repeat rewrite H0. - repeat rewrite H. + rewrite !H0, !H. destruct Ge. destruct (Mem.storev _ _ _ (rsr s0)) as [mem0 | ] eqn:MEML0; simpl. ++ rewrite MEML0. |