diff options
Diffstat (limited to 'aarch64/PostpassScheduling.v')
-rw-r--r-- | aarch64/PostpassScheduling.v | 146 |
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. |