-fcoalesce-mem

5 files changed, 19 insertions, 7 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 46f19dcf..b1afab6f 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -70,3 +70,4 @@ let use_standard_headers =  ref Configuration.has_standard_headers
 let option_fglobaladdrtmp = ref false
 let option_fglobaladdroffset = ref false
 let option_fxsaddr = ref true  
+let option_coalesce_mem = ref true  
diff --git a/driver/Compopts.v b/driver/Compopts.v
index 3bb7a474..f7de596c 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -51,6 +51,9 @@ Parameter optim_fglobaladdroffset: unit -> bool.
 (** FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true) *)
 Parameter optim_fxsaddr: unit -> bool.
 
+(** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *)
+Parameter optim_coalesce_mem: unit -> bool.
+
 (** Flag -fthumb.  For the ARM back-end. *)
 Parameter thumb: unit -> bool.
 
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 35b5db86..804fc3c9 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -375,6 +375,7 @@ let cmdline_actions =
   @ f_opt "globaladdrtmp" option_fglobaladdrtmp
   @ f_opt "globaladdroffset" option_fglobaladdroffset
   @ f_opt "xsaddr" option_fxsaddr
+  @ f_opt "coalesce-mem" option_coalesce_mem
 (* 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 0f336916..979e1d49 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -123,6 +123,8 @@ Extract Constant Compopts.optim_fglobaladdroffset =>
   "fun _ -> !Clflags.option_fglobaladdroffset".
 Extract Constant Compopts.optim_fxsaddr =>
   "fun _ -> !Clflags.option_fxsaddr".
+Extract Constant Compopts.optim_coalesce_mem =>
+  "fun _ -> !Clflags.option_coalesce_mem".
 
 (* Compiler *)
 Extract Constant Compiler.print_Clight => "PrintClight.print_if".
diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v
index 3e0d9ae9..6e06e7ea 100644
--- a/mppa_k1c/Peephole.v
+++ b/mppa_k1c/Peephole.v
@@ -2,6 +2,7 @@ Require Import Coqlib.
 Require Import Asmvliw.
 Require Import Values.
 Require Import Integers.
+Require Compopts.
 
 Definition gpreg_q_list : list gpreg_q :=
 R0R1 :: R2R3 :: R4R5 :: R6R7 :: R8R9
@@ -25,9 +26,9 @@ Fixpoint gpreg_q_search_rec r0 r1 l :=
 Definition gpreg_q_search (r0 : gpreg) (r1 : gpreg) : option gpreg_q :=
   gpreg_q_search_rec r0 r1 gpreg_q_list.
 
-Parameter print_found_store : forall A : Type, Z -> A -> A.
+Parameter print_found_store: forall A, Z -> A -> A.
 
-Fixpoint optimize_body (insns : list basic) : list basic :=
+Fixpoint coalesce_mem (insns : list basic) : list basic :=
   match insns with
   | nil => nil
   | h0 :: t0 =>
@@ -41,17 +42,21 @@ Fixpoint optimize_body (insns : list basic) : list basic :=
             let zofs0 := Ptrofs.signed ofs0 in
             let zofs1 := Ptrofs.signed ofs1 in
             if (zofs1 =? zofs0 + 8) && (ireg_eq ra0 ra1)
-            then let h0' := print_found_store basic zofs0 h0 in
-                 (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (optimize_body t1)
-            else h0 :: (optimize_body t0)
-          | None => h0 :: (optimize_body t0)
+            then (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
+            else h0 :: (coalesce_mem t0)
+          | None => h0 :: (coalesce_mem t0)
           end
-        | _, _ => h0 :: (optimize_body t0)
+        | _, _ => h0 :: (coalesce_mem t0)
         end   
     | nil => h0 :: nil
     end
   end.
 
+Definition optimize_body (insns : list basic) :=
+  if Compopts.optim_coalesce_mem tt
+  then coalesce_mem insns
+  else insns.
+
 Program Definition optimize_bblock (bb : bblock) :=
   let optimized := optimize_body (body bb) in
   let wf_ok := wf_bblockb optimized (exit bb) in