1 files changed, 146 insertions, 0 deletions
diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v
new file mode 100644
index 00000000..f826632b
--- /dev/null
+++ b/aarch64/PostpassScheduling.v
@@ -0,0 +1,146 @@
+(* *************************************************************)
+(*                                                             *)
+(*             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.