diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 16:48:07 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 16:48:07 +0200 |
| commit | 3916ecbc8c77c99bab0bd69de184ae432fd9d3f4 (patch) | |
| tree | acc34ad011074be44abbda58118ffd33997a2a9d /mppa_k1c/Peephole.v | |
| parent | 919d1dfbf22967ae9686d5b982b51cfa707b5edd (diff) | |
| download | compcert-kvx-3916ecbc8c77c99bab0bd69de184ae432fd9d3f4.tar.gz compcert-kvx-3916ecbc8c77c99bab0bd69de184ae432fd9d3f4.zip | |
Lq finished ?
Diffstat (limited to 'mppa_k1c/Peephole.v')
| -rw-r--r-- | mppa_k1c/Peephole.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v index 6e06e7ea..3603c1d8 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -46,6 +46,17 @@ Fixpoint coalesce_mem (insns : list basic) : list basic := else h0 :: (coalesce_mem t0) | None => h0 :: (coalesce_mem t0) end + | (PLoadRRO Pld_a rd0 ra0 ofs0), + (PLoadRRO Pld_a rd1 ra1 ofs1) => + match gpreg_q_search rd0 rd1 with + | Some rd0rd1 => + let zofs0 := Ptrofs.signed ofs0 in + let zofs1 := Ptrofs.signed ofs1 in + if (zofs1 =? zofs0 + 8) && (ireg_eq ra0 ra1) && negb (ireg_eq ra0 rd0) + then (PLoad (PLoadQRRO rd0rd1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + else h0 :: (coalesce_mem t0) + | None => h0 :: (coalesce_mem t0) + end | _, _ => h0 :: (coalesce_mem t0) end | nil => h0 :: nil |