Require Import Classical.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Events.
Require Import Registers.
Require Import Floats.
Require Import Utils.
Require Import SSA.
Require Import SSAutils.
Require Import Utilsvalidproof.
Require Import DomCompute.
Require Import Axioms.
Require Import KildallComp.
Require Import OrderedType.
Require Import Ordered.
Require Import FSets.
Require FSetAVL.
Require Import Opt.
Require Import OptInv.
Require Import DLib.

Validation algorithm

Section Checker.
  
  Variable f : function.
  
  Notation code := (fn_code f).
  Notation phicode := (fn_phicode f).

  Definition certif := PTree.t ssa_def.
  Variable certificate : certif.
  
  Definition ssa_def_to_node (d:ssa_def) : node :=
    match d with
      | SDIop pc => pc
      | SDPhi pc _ => pc
    end.
  
  Definition top_set l : PTree.t unit :=
    fold_left (fun p s => PTree.set s tt p) l (PTree.empty _).
  
  Lemma in_top_set : forall l x, In x l -> PTree.get x (top_set l) = Some tt.
  
  Definition test_param_no_repr (s:PTree.t unit) : bool :=
    forall_ptree (fun r d =>
                     match get_ssa_eq f d with
                       | None => false
                       | Some e =>
                         let dst := ssa_eq_to_dst e in
                         match PTree.get dst s with
                           | Some _ => false
                           | None =>
                             match certificate ! dst with
                               | None => true
                               | Some _ => false
                             end
                         end
                     end) certificate.

  Definition make_repr (l:list reg) : reg -> (reg * node) :=
    let s := top_set l in
    if test_param_no_repr s then
      let map := PTree.map (fun r d => match get_ssa_eq f d with
                                          | None => (r, xH)
                                          | Some e => (ssa_eq_to_dst e, ssa_def_to_node d)
                                        end) certificate in
      (fun r => match PTree.get r map with
                | Some r' => r'
                | None => (r, xH)
                end)
    else (fun r => (r,xH)).

  Lemma make_repr_not_id : forall l r r',
    In r l -> fst (make_repr l r') = r -> r = r'.

  Lemma test_itempotent s :
    test_param_no_repr s = true ->
    let map := PTree.map (fun r d => match get_ssa_eq f d with
                                        | None => (r, xH)
                                        | Some e => (ssa_eq_to_dst e, ssa_def_to_node d)
                                      end) certificate in
    forall r r', PTree.get r map = Some r' -> PTree.get (fst r') map = None.

  Lemma make_repr_itempotent : forall l r,
    fst (make_repr l (fst (make_repr l r))) = fst (make_repr l r).
  
  Definition op_eq (x y:operation) : bool :=
    if eq_operation x y then true else false.

  Lemma op_eq_true_iff : forall x y,
    op_eq x y = true <-> x = y.

  
  Definition check_GVN_instr (f:function)
             (repr:reg-> (reg*node))
             (pc:node) (ins:instruction) : bool :=
    match ins with
      | Iop op args dst _ =>
        let dst' := fst (repr dst) in
        (peq dst dst')
          ||
          (match PTree.get dst certificate with
             | None => false
             | Some (SDIop pc') =>
               match get_ssa_eq f (SDIop pc') with
                 | Some (EqIop op' args' dst0') =>
                   (peq dst' dst0') &&
                   (op_eq op op') &&
                   (fn_dom_test f pc' pc) &&
                   (negb (op_depends_on_memory op)) &&
                   (forall_list2 (fun x y => peq (fst (repr x)) (fst (repr y))) args args')
                 | _ => false
               end
             | Some _ => false
           end)
      | _ => true
    end.

  Definition check_GVN_phiblock (f:function)
             (repr:reg-> (reg*node)) (pc:node) (phib:phiblock) : bool :=
        forallb
          (fun (phi:phiinstruction) =>
             let (args,dst) := phi in
             let dst' := fst (repr dst) in
             (peq dst dst')
               ||
               (match PTree.get dst certificate with
                  | None => false
                  | Some (SDPhi pc' idx) =>
                    (peq pc pc')
                      &&
                      (match get_ssa_eq f (SDPhi pc' idx) with
                         | Some (EqPhi dst0' args') =>
                           (peq dst' dst0')
                           &&
                           (forall_list2 (fun x y => peq (fst (repr x)) (fst (repr y))) args args')
                         | _ => false
                       end)
                  | Some _ => false
                end))
          phib.

  Definition dst_at_top l (m:PTree.t instruction) : list reg :=
    PTree.fold (fun l oc ins =>
                  match ins with
                    | Iload _ _ _ r _
                    | Icall _ _ _ r _ => r :: l
                    | Ibuiltin _ _ (BR r) _ => r :: l
                    | _ => l
                  end) m l.

  Lemma dst_at_top_prop1 : forall m l pc,
    match m!pc with
      | Some (Iload _ _ _ r _)
      | Some (Icall _ _ _ r _) => In r (dst_at_top l m)
      | Some (Ibuiltin _ _ (BR r) _) => In r (dst_at_top l m)
      | _ => True
    end.

  Lemma dst_at_top_prop0 : forall m l,
    forall r, In r l -> In r (dst_at_top l m).

  Definition check_GVN : option (reg-> (reg * node)) :=
    let top_list := dst_at_top (fn_ext_params f) (fn_code f) in
    let repr := make_repr top_list in
    let check_params := forallb (fun r => peq (fst (repr r)) r) top_list in
    let check_instr := forall_ptree (check_GVN_instr f repr) (fn_code f) in
    let check_phiblock := forall_ptree (check_GVN_phiblock f repr) (fn_phicode f) in
    if check_params && check_instr && check_phiblock
    then Some repr
    else None.

End Checker.

CSE optimisation based on GVN

Axiom extern_gvn: function -> certif.

Definition get_repr (f:function) (c:certif):=
  match check_GVN f c with
    | Some repr => repr
    | None => (fun x => (x,xH))
  end.

Definition get_extern_gvn (f:function): (reg -> (reg* node)) :=
  get_repr f (extern_gvn f).

Definition analysis (f: function) := ((get_extern_gvn f, f),P2Map.init true).

Definition res := ((reg -> reg*node)
                    * function
                   )%type.

Definition check_def (code:code) (pc:node) (x:reg) : bool :=
  match code!pc with
    | Some (Iop op args dst succ) => if peq x dst then true else false
    | Some (Iload chunk addr args dst succ) => if peq x dst then true else false
    | Some (Icall sig fn args dst succ) => if peq x dst then true else false
    | Some (Ibuiltin fn args (BR dst) succ) => if peq x dst then true else false
    | _ => false
  end.

Definition transf_instr (r:res) (pc:node) (instr:instruction) : instruction :=
  let '(repr,f) := r in
  match instr with
  | Iop op args dst s =>
    if is_trivial_op op then instr
      else
        let (dst',def') := repr dst in
        if negb (peq dst dst')
           && check_def (fn_code f) def' dst' && negb (peq def' pc)
        then Iop Omove (dst' :: nil) dst s
        else instr
  | _ => instr
  end.

Definition transf_function (f: function) :=
  @Opt.transf_function res analysis transf_instr f.
     
Definition transf_fundef (f: fundef) : fundef :=
  AST.transf_fundef transf_function f.

Definition transf_program (p: program) : program :=
  AST.transform_program transf_fundef p.