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

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: bblock -> list basic.

Extract Constant schedule => "PostpassSchedulingOracle.schedule".

Extract Constant peephole_opt => "PeepholeOracle.peephole_opt".

Section verify_schedule.

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

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.

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.

Program Definition do_peephole (bb : bblock) :=
  let optimized := peephole_opt 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 |}.

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

Theorem verified_schedule_correct:
  forall ge f bb bb',
  verified_schedule bb = OK bb' ->
  bblock_simu ge f bb bb'.

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.