diff options
Diffstat (limited to 'backend/Duplicatepasses.v')
-rw-r--r-- | backend/Duplicatepasses.v | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/backend/Duplicatepasses.v b/backend/Duplicatepasses.v new file mode 100644 index 00000000..7e58eedf --- /dev/null +++ b/backend/Duplicatepasses.v @@ -0,0 +1,58 @@ +Require Import RTL. +Require Import Maps. +Require Import Duplicate. +Require Import Duplicateproof. + +(** Static Prediction *) + +Module StaticPredictOracle <: DuplicateOracle. + Axiom duplicate_aux : function -> code * node * (PTree.t node). + Extract Constant duplicate_aux => "Duplicateaux.static_predict". +End StaticPredictOracle. + +Module Staticpredictproof := DuplicateProof StaticPredictOracle. + +Module Staticpredict := Staticpredictproof. + +(** Unrolling one iteration out of the body *) + +Module UnrollSingleOracle <: DuplicateOracle. + Axiom duplicate_aux : function -> code * node * (PTree.t node). + Extract Constant duplicate_aux => "Duplicateaux.unroll_single". +End UnrollSingleOracle. + +Module Unrollsingleproof := DuplicateProof UnrollSingleOracle. + +Module Unrollsingle := Unrollsingleproof. + +(** Unrolling the body of innermost loops *) + +Module UnrollBodyOracle <: DuplicateOracle. + Axiom duplicate_aux : function -> code * node * (PTree.t node). + Extract Constant duplicate_aux => "Duplicateaux.unroll_body". +End UnrollBodyOracle. + +Module Unrollbodyproof := DuplicateProof UnrollBodyOracle. + +Module Unrollbody := Unrollbodyproof. + +(** Tail Duplication *) + +Module TailDuplicateOracle <: DuplicateOracle. + Axiom duplicate_aux : function -> code * node * (PTree.t node). + Extract Constant duplicate_aux => "Duplicateaux.tail_duplicate". +End TailDuplicateOracle. + +Module Tailduplicateproof := DuplicateProof TailDuplicateOracle. + +Module Tailduplicate := Tailduplicateproof. + +(** Loop Rotate *) + +Module LoopRotateOracle <: DuplicateOracle. + Axiom duplicate_aux : function -> code * node * (PTree.t node). + Extract Constant duplicate_aux => "Duplicateaux.loop_rotate". +End LoopRotateOracle. + +Module Looprotateproof := DuplicateProof LoopRotateOracle. +Module Looprotate := Looprotateproof. |