diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2020-10-27 15:59:25 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2020-10-27 15:59:25 +0100 |
commit | f82bf792fdf0c03b5c76f4cef5c39d5f1fd32b81 (patch) | |
tree | 3a59298fd7cdd8d14d49fff53d854d90cafc58f7 /backend/Duplicatepasses.v | |
parent | 9bb6fd8219fcd4ef8da5d2b3a6d93f802fc777c3 (diff) | |
download | compcert-kvx-f82bf792fdf0c03b5c76f4cef5c39d5f1fd32b81.tar.gz compcert-kvx-f82bf792fdf0c03b5c76f4cef5c39d5f1fd32b81.zip |
Oops forgot Duplicatepasses.v
Diffstat (limited to 'backend/Duplicatepasses.v')
-rw-r--r-- | backend/Duplicatepasses.v | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/backend/Duplicatepasses.v b/backend/Duplicatepasses.v new file mode 100644 index 00000000..7f007251 --- /dev/null +++ b/backend/Duplicatepasses.v @@ -0,0 +1,64 @@ +Require Import RTL. +Require Import Maps. +Require Import Duplicate. +Require Import Duplicateproof. + +(** Static Prediction *) + +Axiom static_predict_aux : function -> code * node * (PTree.t node). +Extract Constant static_predict_aux => "Duplicateaux.static_predict". + +Module StaticPredictParam <: DuplicateParam. + Definition duplicate_aux := static_predict_aux. +End StaticPredictParam. + +Module StaticPredictDef := Duplicate StaticPredictParam. + +Module Staticpredictproof := DuplicateProof StaticPredictDef. + +Module Staticpredict := Staticpredictproof. + +(** Unrolling one iteration out of the body *) + +Axiom unroll_single_aux : function -> code * node * (PTree.t node). +Extract Constant unroll_single_aux => "Duplicateaux.unroll_single". + +Module UnrollSingleParam <: DuplicateParam. + Definition duplicate_aux := static_predict_aux. +End UnrollSingleParam. + +Module UnrollSingleDef := Duplicate UnrollSingleParam. + +Module Unrollsingleproof := DuplicateProof UnrollSingleDef. + +Module Unrollsingle := Unrollsingleproof. + +(** Unrolling the body of innermost loops *) + +Axiom unroll_body_aux : function -> code * node * (PTree.t node). +Extract Constant unroll_body_aux => "Duplicateaux.unroll_body". + +Module UnrollBodyParam <: DuplicateParam. + Definition duplicate_aux := static_predict_aux. +End UnrollBodyParam. + +Module UnrollBodyDef := Duplicate UnrollBodyParam. + +Module Unrollbodyproof := DuplicateProof UnrollBodyDef. + +Module Unrollbody := Unrollbodyproof. + +(** Tail Duplication *) + +Axiom tail_duplicate_aux : function -> code * node * (PTree.t node). +Extract Constant tail_duplicate_aux => "Duplicateaux.tail_duplicate". + +Module TailDuplicateParam <: DuplicateParam. + Definition duplicate_aux := static_predict_aux. +End TailDuplicateParam. + +Module TailDuplicateDef := Duplicate TailDuplicateParam. + +Module Tailduplicateproof := DuplicateProof TailDuplicateDef. + +Module Tailduplicate := Tailduplicateproof.
\ No newline at end of file |