blob: 7e58eedf84e6e4fe98e146578ab8c72f330d68a4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
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.
|
