command line options (still incomplete)

6 files changed, 46 insertions, 11 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 4d70d350..76afa4b4 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -66,3 +66,7 @@ let option_small_const = ref (!option_small_data)
 let option_timings = ref false
 let stdlib_path = ref Configuration.stdlib_path
 let use_standard_headers =  ref Configuration.has_standard_headers
+
+let option_fglobaladdrtmp = ref false
+let option_fglobaladdroffset = ref false
+let option_fxsaddr = ref true  
diff --git a/driver/Compopts.v b/driver/Compopts.v
index e6eecc9b..3bb7a474 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -42,6 +42,15 @@ Parameter optim_redundancy: unit -> bool.
 (** Flag -fpostpass. Postpass scheduling for K1 architecture *)
 Parameter optim_postpass: unit -> bool.
 
+(** FIXME TEMPORARY Flag -fglobaladdrtmp. Use a temporary register for loading the address of global variables (default false) *)
+Parameter optim_fglobaladdrtmp: unit -> bool.
+
+(** FIXME TEMPORARY Flag -fglobaladdroffset. Fold offsets into global addresses  (default false) *)
+Parameter optim_fglobaladdroffset: unit -> bool.
+
+(** FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true) *)
+Parameter optim_fxsaddr: unit -> bool.
+
 (** Flag -fthumb.  For the ARM back-end. *)
 Parameter thumb: unit -> bool.
 
diff --git a/driver/Driver.ml b/driver/Driver.ml
index c68c066a..505a1d35 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -367,6 +367,9 @@ let cmdline_actions =
   @ f_opt "postpass-ilp" option_fpostpass_ilp
   @ f_opt "inline" option_finline
   @ f_opt "inline-functions-called-once" option_finline_functions_called_once
+  @ f_opt "globaladdrtmp" option_fglobaladdrtmp
+  @ f_opt "globaladdroffset" option_fglobaladdroffset
+  @ f_opt "xsaddr" option_fxsaddr
 (* Code generation options *)
   @ f_opt "fpu" option_ffpu
   @ f_opt "sse" option_ffpu (* backward compatibility *)
diff --git a/extraction/extraction.v b/extraction/extraction.v
index f58991aa..0f336916 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -117,6 +117,12 @@ Extract Constant Compopts.thumb =>
   "fun _ -> !Clflags.option_mthumb".
 Extract Constant Compopts.debug =>
   "fun _ -> !Clflags.option_g".
+Extract Constant Compopts.optim_fglobaladdrtmp =>
+  "fun _ -> !Clflags.option_fglobaladdrtmp".
+Extract Constant Compopts.optim_fglobaladdroffset =>
+  "fun _ -> !Clflags.option_fglobaladdroffset".
+Extract Constant Compopts.optim_fxsaddr =>
+  "fun _ -> !Clflags.option_fxsaddr".
 
 (* Compiler *)
 Extract Constant Compiler.print_Clight => "PrintClight.print_if".
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.
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index a92ed572..9e2eec8b 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -1256,7 +1256,7 @@ Theorem eval_addressing:
 Proof.
   intros until v. unfold addressing; case (addressing_match a); intros; InvEval.
   - exists (@nil val);  split. eauto with evalexpr. simpl. auto.
-  - destruct (Archi.pic_code tt).
+  - destruct (orb _ _).
   + exists (Vptr b ofs0 :: nil); split.
     constructor. EvalOp. simpl. congruence. constructor. simpl. rewrite Ptrofs.add_zero. congruence.
   + exists (@nil val); split. constructor. simpl; auto.
@@ -1265,11 +1265,18 @@ Proof.
   - exists (v1 :: nil); split. eauto with evalexpr. simpl.
     destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. 
     simpl. auto.
-  - destruct (Z.eq_dec _ _).
-    + exists (v1 :: v2 :: nil); split. repeat (constructor; auto). simpl. rewrite Int.repr_unsigned. destruct v2; simpl in *; congruence.
-    + exists (v1 :: v0 :: nil); split. repeat (constructor; auto). econstructor.
-      repeat (constructor; auto). eassumption. simpl. congruence.
-      simpl. congruence.
+  - destruct (Compopts.optim_fxsaddr tt).
+    + destruct (Z.eq_dec _ _).
+      * exists (v1 :: v2 :: nil); split.
+        repeat (constructor; auto). simpl. rewrite Int.repr_unsigned. destruct v2; simpl in *; congruence.
+      * exists (v1 :: v0 :: nil); split.
+        repeat (constructor; auto). econstructor.
+        repeat (constructor; auto). eassumption. simpl. congruence.
+        simpl. congruence.
+    + exists (v1 :: v0 :: nil); split.
+        repeat (constructor; auto). econstructor.
+        repeat (constructor; auto). eassumption. simpl. congruence.
+        simpl. congruence.
   - exists (v1 :: v0 :: nil); split. repeat (constructor; auto). simpl. congruence.
   - exists (v :: nil);  split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto.
 Qed.