From 03b20488fd4202970ed307dbec696cc0e64b8f31 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 3 Dec 2018 18:01:56 +0100 Subject: Tout début de développement d'un postpass Asmblock en Coq MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/PostpassScheduling.v | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 mppa_k1c/PostpassScheduling.v (limited to 'mppa_k1c/PostpassScheduling.v') 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 -- cgit