diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 09:45:55 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 09:45:55 +0200 |
commit | 8058d6a89fe0cfda16f685ef5a96793b95cc4156 (patch) | |
tree | be0be3400453ad64313432b0c580234114788846 /mppa_k1c/SelectOp.vp | |
parent | 7962808d192f2b4d88e8ff1135e3f6e75cf8dea9 (diff) | |
parent | 98206d8c97cf9ecdff8d892ecafb9a9fa8455f74 (diff) | |
download | compcert-kvx-8058d6a89fe0cfda16f685ef5a96793b95cc4156.tar.gz compcert-kvx-8058d6a89fe0cfda16f685ef5a96793b95cc4156.zip |
Merge branch 'mppa-xsaddr' into mppa-work
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
-rw-r--r-- | mppa_k1c/SelectOp.vp | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 25f09e2e..6adcebe5 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -53,6 +53,8 @@ Require Import CminorSel. Require Import OpHelpers. Require Import ExtValues. Require Import DecBoolOps. +Require Import Chunks. +Require Compopts. Local Open Scope cminorsel_scope. @@ -581,9 +583,19 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). Nondetfunction addressing (chunk: memory_chunk) (e: expr) := match e with | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) - | Eop (Oaddrsymbol id ofs) Enil => if Archi.pic_code tt then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil) + | Eop (Oaddrsymbol id ofs) Enil => + (if (orb (Archi.pic_code tt) (negb (Compopts.optim_fglobaladdrtmp tt))) + then (Aindexed Ptrofs.zero, e:::Enil) + else (Aglobal id ofs, Enil)) | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil) | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil) + | Eop Oaddl (e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) => + (if Compopts.optim_fxsaddr tt + then let zscale := Int.unsigned scale in + if Z.eq_dec zscale (zscale_of_chunk chunk) + then (Aindexed2XS zscale, e1:::e2:::Enil) + else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) + else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil)) | Eop Oaddl (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil) | _ => (Aindexed Ptrofs.zero, e:::Enil) end. |