diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 11:29:40 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 11:29:40 +0200 |
commit | cba53c98b999eea7984e4ffd24a9449abea3e0e2 (patch) | |
tree | d50cb8a1bde1fa5c893a1752f386d08e990519e3 | |
parent | a289d73e791be5a760c8a9b2f3de2064f001a770 (diff) | |
download | compcert-kvx-cba53c98b999eea7984e4ffd24a9449abea3e0e2.tar.gz compcert-kvx-cba53c98b999eea7984e4ffd24a9449abea3e0e2.zip |
-fcoalesce-mem
-rw-r--r-- | driver/Clflags.ml | 1 | ||||
-rw-r--r-- | driver/Compopts.v | 3 | ||||
-rw-r--r-- | driver/Driver.ml | 1 | ||||
-rw-r--r-- | extraction/extraction.v | 2 | ||||
-rw-r--r-- | mppa_k1c/Peephole.v | 19 |
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 |