From 57ddece94f4c4b44e8e3127c6f5f72aaa5962250 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 May 2019 22:20:35 +0200 Subject: does not yet work, arity mismatch --- mppa_k1c/SelectOp.vp | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'mppa_k1c/SelectOp.vp') diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 25f09e2e..28b91728 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -53,6 +53,7 @@ Require Import CminorSel. Require Import OpHelpers. Require Import ExtValues. Require Import DecBoolOps. +Require Import Chunks. Local Open Scope cminorsel_scope. @@ -584,6 +585,11 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := | Eop (Oaddrsymbol id ofs) Enil => if Archi.pic_code 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) => + 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) | Eop Oaddl (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil) | _ => (Aindexed Ptrofs.zero, e:::Enil) end. -- cgit From 9f256a4ad30c93749e6c1192a84f996feac3b023 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 2 May 2019 09:32:49 +0200 Subject: command line options (still incomplete) --- mppa_k1c/SelectOp.vp | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'mppa_k1c/SelectOp.vp') diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 28b91728..6adcebe5 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -54,6 +54,7 @@ Require Import OpHelpers. Require Import ExtValues. Require Import DecBoolOps. Require Import Chunks. +Require Compopts. Local Open Scope cminorsel_scope. @@ -582,14 +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) => - 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) + (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. -- cgit