From 8c5e82fdd011d68e7dcba3adb88d6b5036e47958 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 4 Dec 2018 17:57:04 +0100 Subject: Added definitions and proof sketch for PostpassScheduling --- mppa_k1c/PostpassScheduling.v | 34 +++++++++++++++++++--------------- 1 file changed, 19 insertions(+), 15 deletions(-) (limited to 'mppa_k1c/PostpassScheduling.v') diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 8ec72f90..381e1214 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -10,29 +10,33 @@ (* *) (* *********************************************************************) +Require Import Coqlib Errors AST. Require Import Asmblock. +Local Open Scope error_monad_scope. + (** Oracle taking as input a basic block, - returns a basic block with its instruction reordered *) + returns a basic block with its instructions 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 *) +(* TODO - implement the verificator *) +Definition transf_block (b : bblock) : res bblock := OK (schedule b). -Definition postpass_schedule (lb : list bblock) : list bblock := +Fixpoint transf_blocks (lb : list bblock) : res (list bblock) := match lb with - | nil => nil - | (cons b lb) => split (schedule b) ++ lb + | nil => OK nil + | (cons b lb) => + do lb' <- transf_blocks lb; + do b' <- transf_block b; + OK (b' :: lb') end. -Definition transf_function (f: function) : function := - mkfunction (fn_sig f) (postpass_schedule (fn_blocks f)). +Definition transf_function (f: function) : res function := + do lb <- transf_blocks (fn_blocks f); + OK (mkfunction (fn_sig f) lb). -Definition transf_fundef (f: fundef) : fundef := - AST.transf_fundef transf_function f. +Definition transf_fundef (f: fundef) : res fundef := + transf_partial_fundef transf_function f. -Definition transf_program (p: program) : program := - AST.transform_program transf_fundef p. \ No newline at end of file +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. \ No newline at end of file -- cgit