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
:: 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.

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.

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, Z -> A -> A.

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 (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
            else h0 :: (coalesce_mem t0)
          | None => h0 :: (coalesce_mem t0)
          end
        | (PLoadRRO Pld_a rd0 ra0 ofs0),
          (PLoadRRO 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 (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.