Ocaml peephole oracle and array datastruct instead of lists

1 files changed, 19 insertions, 4 deletions

diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v
index b8c16131..f826632b 100644
--- a/aarch64/PostpassScheduling.v
+++ b/aarch64/PostpassScheduling.v
@@ -19,7 +19,6 @@ Require Import Coqlib Errors AST Integers.
 Require Import Asmblock Axioms Memory Globalenvs.
 Require Import Asmblockdeps Asmblockprops.
 Require Import IterList.
-Require Peephole.
 
 Local Open Scope error_monad_scope.
 
@@ -27,8 +26,12 @@ Local Open Scope error_monad_scope.
     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.
@@ -68,9 +71,21 @@ 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.
+(*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