(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
(*           David Monniaux     CNRS, VERIMAG                  *)
(*           Cyril Six          Kalray                         *)
(*           Léo Gourdin        UGA, VERIMAG                   *)
(*                                                             *)
(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)

(** Implementation (and basic properties) of the verified postpass scheduler *)

Require Import Coqlib Errors AST Integers.
Require Import Asmblock Axioms Memory Globalenvs.
Require Import Asmblockdeps Asmblockprops.
Require Import IterList.

Local Open Scope error_monad_scope.

(** * Oracle taking as input a basic block,
    returns a scheduled basic block *)
Axiom schedule: bblock -> (list basic) * option control.

Axiom peephole_opt: (list basic) -> list basic.

Extract Constant schedule => "PostpassSchedulingOracle.schedule".

Extract Constant peephole_opt => "PeepholeOracle.peephole_opt".

Section verify_schedule.

Variable lk: aarch64_linker.

Definition verify_schedule (bb bb' : bblock) : res unit :=
  match bblock_simub bb bb' with
  | true => OK tt
  | false => Error (msg "PostpassScheduling.verify_schedule")
  end.

Definition verify_size bb bb' := if (Z.eqb (size bb) (size bb')) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size").

Lemma verify_size_size:
  forall bb bb', verify_size bb bb' = OK tt -> size bb = size bb'.
Proof.
  intros. unfold verify_size in H. destruct (size bb =? size bb') eqn:SIZE; try discriminate.
  apply Z.eqb_eq. assumption.
Qed.

Program Definition make_bblock_from_basics lb :=
  match lb with
  | nil => Error (msg "PostpassScheduling.make_bblock_from_basics")
  | b :: lb => OK {| header := nil; body := b::lb; exit := None |}
  end.

Program Definition schedule_to_bblock (lb: list basic) (oc: option control) : res bblock :=
  match oc with
  | None => make_bblock_from_basics lb
  | Some c => OK {| header := nil; body := lb; exit := Some c |}
  end.
Next Obligation.
  unfold Is_true, non_empty_bblockb.
  unfold non_empty_exit. rewrite orb_true_r. reflexivity.
Qed.

Definition do_schedule (bb: bblock) : res bblock :=
  if (Z.eqb (size bb) 1) then OK (bb) 
  else match (schedule bb) with (lb, oc) => schedule_to_bblock lb oc end.

(*Definition do_peephole (bb: bblock) : bblock :=*)
  (*let res := Peephole.optimize_bblock bb in*)
  (*if (size res =? size bb) then res else bb.*)

Program Definition do_peephole (bb : bblock) :=
  let optimized := peephole_opt (body bb) in
  let wf_ok := non_empty_bblockb optimized (exit bb) in
  {| header := header bb;
     body := if wf_ok then optimized else (body bb);
     exit := exit bb |}.
Next Obligation.
  destruct (non_empty_bblockb (peephole_opt (body bb))) eqn:Rwf.
  - rewrite Rwf. cbn. trivial.
  - exact (correct bb).
Qed.

Definition verified_schedule (bb : bblock) : res bblock :=
  let nhbb  := no_header bb in
  let phbb := do_peephole nhbb in
  do schbb <- do_schedule phbb;
  let bb' := stick_header (header bb) schbb in
  do sizecheck <- verify_size bb bb';
  do schedcheck <- verify_schedule bb bb';
  OK (bb').

Lemma verified_schedule_size:
  forall bb bb', verified_schedule bb = OK bb' -> size bb = size bb'.
Proof.
  intros. unfold verified_schedule in H.
  monadInv H.
  unfold verify_size in EQ1.
  destruct (size _ =? size _) eqn:ESIZE_H in EQ1; try discriminate.
  rewrite Z.eqb_eq in ESIZE_H; rewrite ESIZE_H; reflexivity.
Qed.

Theorem verified_schedule_correct:
  forall ge f bb bb',
  verified_schedule bb = OK bb' ->
  bblock_simu lk ge f bb bb'.
Proof.
  intros.
  monadInv H.
  eapply bblock_simub_correct.
  unfold verify_schedule in EQ0.
  destruct (bblock_simub _ _) in *; try discriminate; auto.
Qed.

End verify_schedule.

Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=
  match lbb with
  | nil => OK nil
  | bb :: lbb =>
      do tlbb <- transf_blocks lbb;
      do tbb <- verified_schedule bb;
      OK (tbb :: tlbb)
  end.

Definition transl_function (f: function) : res function :=
  do lb <- transf_blocks (fn_blocks f); 
  OK (mkfunction (fn_sig f) lb).

Definition transf_function (f: function) : res function :=
  do tf <- transl_function f;
  if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
  then Error (msg "code size exceeded")
  else OK tf.

Definition transf_fundef (f: fundef) : res fundef :=
  transf_partial_fundef transf_function f.

Definition transf_program (p: program) : res program :=
  transform_partial_program transf_fundef p.