diff options
Diffstat (limited to 'mppa_k1c/PostpassScheduling.v')
| -rw-r--r-- | mppa_k1c/PostpassScheduling.v | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v new file mode 100644 index 00000000..8ec72f90 --- /dev/null +++ b/mppa_k1c/PostpassScheduling.v @@ -0,0 +1,38 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Asmblock. + +(** Oracle taking as input a basic block, + returns a basic block with its instruction reordered *) +Axiom schedule: bblock -> bblock. + +(** Oracle taking as input a basic block + splits it into several bblocks (representing bundles *) +Axiom split: bblock -> list bblock. + +(* TODO - separate the postpass_schedule in two phases *) + +Definition postpass_schedule (lb : list bblock) : list bblock := + match lb with + | nil => nil + | (cons b lb) => split (schedule b) ++ lb + end. + +Definition transf_function (f: function) : function := + mkfunction (fn_sig f) (postpass_schedule (fn_blocks f)). + +Definition transf_fundef (f: fundef) : fundef := + AST.transf_fundef transf_function f. + +Definition transf_program (p: program) : program := + AST.transform_program transf_fundef p.
\ No newline at end of file |