k1c -> kvx changes

1 files changed, 0 insertions, 158 deletions

diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v
deleted file mode 100644
index 35f4bbd9..00000000
--- a/mppa_k1c/Peephole.v
+++ /dev/null
@@ -1,158 +0,0 @@
-(* *************************************************************)
-(*                                                             *)
-(*             The Compcert verified compiler                  *)
-(*                                                             *)
-(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
-(*           David Monniaux     CNRS, VERIMAG                  *)
-(*           Cyril Six          Kalray                         *)
-(*                                                             *)
-(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
-(*  This file is distributed under the terms of the INRIA      *)
-(*  Non-Commercial License Agreement.                          *)
-(*                                                             *)
-(* *************************************************************)
-
-Require Import Coqlib.
-Require Import Asmvliw.
-Require Import Values.
-Require Import Integers.
-Require Import AST.
-Require Compopts.
-
-Definition gpreg_q_list : list gpreg_q :=
-R0R1 :: R2R3 :: R4R5 :: R6R7 :: R8R9
-:: R10R11 :: R12R13 :: R14R15 :: R16R17 :: R18R19
-:: R20R21 :: R22R23 :: R24R25 :: R26R27 :: R28R29
-:: R30R31 :: R32R33 :: R34R35 :: R36R37 :: R38R39
-:: R40R41 :: R42R43 :: R44R45 :: R46R47 :: R48R49
-:: R50R51 :: R52R53 :: R54R55 :: R56R57 :: R58R59
-:: R60R61 :: R62R63 :: nil.
-
-Definition gpreg_o_list : list gpreg_o :=
-R0R1R2R3 :: R4R5R6R7 :: R8R9R10R11 :: R12R13R14R15
-:: R16R17R18R19 :: R20R21R22R23 :: R24R25R26R27 :: R28R29R30R31
-:: R32R33R34R35 :: R36R37R38R39 :: R40R41R42R43 :: R44R45R46R47
-:: R48R49R50R51 :: R52R53R54R55 :: R56R57R58R59 :: R60R61R62R63 :: nil.
-
-Fixpoint gpreg_q_search_rec r0 r1 l :=
-  match l with
-  | h :: t =>
-    let (s0, s1) := gpreg_q_expand h in
-    if (gpreg_eq r0 s0) && (gpreg_eq r1 s1)
-    then Some h
-    else gpreg_q_search_rec r0 r1 t
-  | nil => None
-  end.
-
-Fixpoint gpreg_o_search_rec r0 r1 r2 r3 l :=
-  match l with
-  | h :: t =>
-    match gpreg_o_expand h with
-    | (((s0, s1), s2), s3) =>
-      if (gpreg_eq r0 s0) && (gpreg_eq r1 s1) &&
-         (gpreg_eq r2 s2) && (gpreg_eq r3 s3)
-      then Some h
-      else gpreg_o_search_rec r0 r1 r2 r3 t
-    end
-  | nil => None
-  end.
-
-Definition gpreg_q_search (r0 : gpreg) (r1 : gpreg) : option gpreg_q :=
-  gpreg_q_search_rec r0 r1 gpreg_q_list.
-
-Definition gpreg_o_search r0 r1 r2 r3 : option gpreg_o :=
-  gpreg_o_search_rec r0 r1 r2 r3 gpreg_o_list.
-
-Parameter print_found_store: forall A, Z -> A -> A.
-
-Definition coalesce_octuples := true.
-
-Fixpoint coalesce_mem (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 ofs0),
-          (PStoreRRO Psd_a rs1 ra1 ofs1) =>
-          match gpreg_q_search rs0 rs1 with
-          | Some rs0rs1 =>
-            let zofs0 := Ptrofs.signed ofs0 in
-            let zofs1 := Ptrofs.signed ofs1 in
-            if (zofs1 =? zofs0 + 8) && (ireg_eq ra0 ra1)
-            then
-              if coalesce_octuples
-              then
-                match t1 with
-                | (PStoreRRO Psd_a rs2 ra2 ofs2) :: 
-                  (PStoreRRO Psd_a rs3 ra3 ofs3) :: t3 =>
-                  match gpreg_o_search rs0 rs1 rs2 rs3 with
-                  | Some octuple =>
-                    let zofs2 := Ptrofs.signed ofs2 in
-                    let zofs3 := Ptrofs.signed ofs3 in
-                    if (zofs2 =? zofs0 + 16) && (ireg_eq ra0 ra2) &&
-                                             (zofs3 =? zofs0 + 24) && (ireg_eq ra0 ra3)
-                    then (PStore (PStoreORRO octuple ra0 ofs0)) :: Pnop :: Pnop :: Pnop :: (coalesce_mem t3)
-                    else (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
-                  | None => (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
-                  end
-                | _ => (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
-                end
-              else (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
-            else h0 :: (coalesce_mem t0)
-          | None => h0 :: (coalesce_mem t0)
-          end
-            
-        | (PLoad (PLoadRRO TRAP Pld_a rd0 ra0 ofs0)),
-          (PLoad (PLoadRRO TRAP Pld_a rd1 ra1 ofs1)) =>
-          match gpreg_q_search rd0 rd1 with
-          | Some rd0rd1 =>
-            let zofs0 := Ptrofs.signed ofs0 in
-            let zofs1 := Ptrofs.signed ofs1 in
-            if (zofs1 =? zofs0 + 8) && (ireg_eq ra0 ra1) && negb (ireg_eq ra0 rd0)
-            then
-              if coalesce_octuples
-              then
-                match t1 with
-                | (PLoad (PLoadRRO TRAP Pld_a rd2 ra2 ofs2)) :: 
-                  (PLoad (PLoadRRO TRAP Pld_a rd3 ra3 ofs3)) :: t3 =>
-                  match gpreg_o_search rd0 rd1 rd2 rd3 with
-                  | Some octuple =>
-                    let zofs2 := Ptrofs.signed ofs2 in
-                    let zofs3 := Ptrofs.signed ofs3 in
-                    if (zofs2 =? zofs0 + 16) && (ireg_eq ra0 ra2) &&
-                       (zofs3 =? zofs0 + 24) && (ireg_eq ra0 ra3) &&
-                       negb (ireg_eq ra0 rd1) && negb (ireg_eq ra0 rd2)
-                    then (PLoad (PLoadORRO octuple ra0 ofs0)) :: Pnop :: Pnop :: Pnop :: (coalesce_mem t3)
-                    else (PLoad (PLoadQRRO rd0rd1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
-                  | None  => (PLoad (PLoadQRRO rd0rd1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
-                  end
-                | _ =>  (PLoad (PLoadQRRO rd0rd1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
-                end
-              else (PLoad (PLoadQRRO rd0rd1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
-            else h0 :: (coalesce_mem t0)
-          | None => h0 :: (coalesce_mem t0)
-          end
-        | _, _ => 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
-  {| header := header bb;
-     body := if wf_ok then optimized else (body bb);
-     exit := exit bb |}.
-Next Obligation.
-  destruct (wf_bblockb (optimize_body (body bb))) eqn:Rwf.
-  - rewrite Rwf. simpl. trivial.
-  - exact (correct bb).
-Qed.