diff options
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Peephole.v | 22 | ||||
| -rw-r--r-- | mppa_k1c/extractionMachdep.v | 3 |
2 files changed, 24 insertions, 1 deletions
diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v index 56e547e5..b7931aca 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -1,6 +1,26 @@ +Require Import Coqlib. Require Import Asmvliw. +Require Import Values. +Require Import Integers. -Definition optimize_body (insns : list basic) := insns. +Parameter print_found_store : forall A : Type, Z -> A -> A. + +Fixpoint optimize_body (insns : list basic) : list basic := + match insns with + | nil => nil + | h0 :: t0 => + match t0 with + | h1 :: t1 => + match h0, h1 with + | (PStoreRRO Psd_a rs0 ra0 (Ofsimm ofs0)), + (PStoreRRO Psd_a rs1 ra1 (Ofsimm ofs1)) => + let h0' := print_found_store basic (Ptrofs.signed ofs0) h0 in + h0' :: (optimize_body t0) + | _, _ => h0 :: (optimize_body t0) + end + | nil => h0 :: nil + end + end. Program Definition optimize_bblock (bb : bblock) := let optimized := optimize_body (body bb) in diff --git a/mppa_k1c/extractionMachdep.v b/mppa_k1c/extractionMachdep.v index e70f51de..fdecd2a3 100644 --- a/mppa_k1c/extractionMachdep.v +++ b/mppa_k1c/extractionMachdep.v @@ -22,6 +22,9 @@ Require Archi Asm. Extract Constant Archi.ptr64 => " Configuration.model = ""64"" ". Extract Constant Archi.pic_code => "fun () -> false". (* for the time being *) +Extract Constant Peephole.print_found_store => +"fun offset x -> Printf.printf ""found offset = %ld\n"" (Camlcoq.camlint_of_coqint offset); x". + (* Asm *) (* Extract Constant Asm.low_half => "fun _ _ _ -> assert false". |