diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 21:20:14 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 21:20:14 +0200 |
| commit | 56ab9fea6dc937dac56e883a64f06cae3c931551 (patch) | |
| tree | 82e3e350b56b2e99561e6f043e69e85762db41db /mppa_k1c/Peephole.v | |
| parent | e967c0669d17f9a04a301d2f600c4b55a0618fc7 (diff) | |
| download | compcert-kvx-56ab9fea6dc937dac56e883a64f06cae3c931551.tar.gz compcert-kvx-56ab9fea6dc937dac56e883a64f06cae3c931551.zip | |
detect consecutive ones
Diffstat (limited to 'mppa_k1c/Peephole.v')
| -rw-r--r-- | mppa_k1c/Peephole.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v index b7931aca..47e04aec 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -14,8 +14,12 @@ Fixpoint optimize_body (insns : list basic) : list basic := match h0, h1 with | (PStoreRRO Psd_a rs0 ra0 (Ofsimm ofs0)), (PStoreRRO Psd_a rs1 ra1 (Ofsimm ofs1)) => - let h0' := print_found_store basic (Ptrofs.signed ofs0) h0 in - h0' :: (optimize_body t0) + let zofs0 := Ptrofs.signed ofs0 in + let zofs1 := Ptrofs.signed ofs1 in + if zofs1 =? zofs0 + 8 + then let h0' := print_found_store basic zofs0 h0 in + h0' :: (optimize_body t0) + else h0 :: (optimize_body t0) | _, _ => h0 :: (optimize_body t0) end | nil => h0 :: nil |