command line options (still incomplete)

1 files changed, 11 insertions, 5 deletions

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.