blob: f826632bcf532b040a5191b482546811ea991ccb (
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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* David Monniaux CNRS, VERIMAG *)
(* Cyril Six Kalray *)
(* Léo Gourdin UGA, VERIMAG *)
(* *)
(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
(** Implementation (and basic properties) of the verified postpass scheduler *)
Require Import Coqlib Errors AST Integers.
Require Import Asmblock Axioms Memory Globalenvs.
Require Import Asmblockdeps Asmblockprops.
Require Import IterList.
Local Open Scope error_monad_scope.
(** * Oracle taking as input a basic block,
returns a scheduled basic block *)
Axiom schedule: bblock -> (list basic) * option control.
Axiom peephole_opt: (list basic) -> list basic.
Extract Constant schedule => "PostpassSchedulingOracle.schedule".
Extract Constant peephole_opt => "PeepholeOracle.peephole_opt".
Section verify_schedule.
Variable lk: aarch64_linker.
Definition verify_schedule (bb bb' : bblock) : res unit :=
match bblock_simub bb bb' with
| true => OK tt
| false => Error (msg "PostpassScheduling.verify_schedule")
end.
Definition verify_size bb bb' := if (Z.eqb (size bb) (size bb')) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size").
Lemma verify_size_size:
forall bb bb', verify_size bb bb' = OK tt -> size bb = size bb'.
Proof.
intros. unfold verify_size in H. destruct (size bb =? size bb') eqn:SIZE; try discriminate.
apply Z.eqb_eq. assumption.
Qed.
Program Definition make_bblock_from_basics lb :=
match lb with
| nil => Error (msg "PostpassScheduling.make_bblock_from_basics")
| b :: lb => OK {| header := nil; body := b::lb; exit := None |}
end.
Program Definition schedule_to_bblock (lb: list basic) (oc: option control) : res bblock :=
match oc with
| None => make_bblock_from_basics lb
| Some c => OK {| header := nil; body := lb; exit := Some c |}
end.
Next Obligation.
unfold Is_true, non_empty_bblockb.
unfold non_empty_exit. rewrite orb_true_r. reflexivity.
Qed.
Definition do_schedule (bb: bblock) : res bblock :=
if (Z.eqb (size bb) 1) then OK (bb)
else match (schedule bb) with (lb, oc) => schedule_to_bblock lb oc end.
(*Definition do_peephole (bb: bblock) : bblock :=*)
(*let res := Peephole.optimize_bblock bb in*)
(*if (size res =? size bb) then res else bb.*)
Program Definition do_peephole (bb : bblock) :=
let optimized := peephole_opt (body bb) in
let wf_ok := non_empty_bblockb optimized (exit bb) in
{| header := header bb;
body := if wf_ok then optimized else (body bb);
exit := exit bb |}.
Next Obligation.
destruct (non_empty_bblockb (peephole_opt (body bb))) eqn:Rwf.
- rewrite Rwf. cbn. trivial.
- exact (correct bb).
Qed.
Definition verified_schedule (bb : bblock) : res bblock :=
let nhbb := no_header bb in
let phbb := do_peephole nhbb in
do schbb <- do_schedule phbb;
let bb' := stick_header (header bb) schbb in
do sizecheck <- verify_size bb bb';
do schedcheck <- verify_schedule bb bb';
OK (bb').
Lemma verified_schedule_size:
forall bb bb', verified_schedule bb = OK bb' -> size bb = size bb'.
Proof.
intros. unfold verified_schedule in H.
monadInv H.
unfold verify_size in EQ1.
destruct (size _ =? size _) eqn:ESIZE_H in EQ1; try discriminate.
rewrite Z.eqb_eq in ESIZE_H; rewrite ESIZE_H; reflexivity.
Qed.
Theorem verified_schedule_correct:
forall ge f bb bb',
verified_schedule bb = OK bb' ->
bblock_simu lk ge f bb bb'.
Proof.
intros.
monadInv H.
eapply bblock_simub_correct.
unfold verify_schedule in EQ0.
destruct (bblock_simub _ _) in *; try discriminate; auto.
Qed.
End verify_schedule.
Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=
match lbb with
| nil => OK nil
| bb :: lbb =>
do tlbb <- transf_blocks lbb;
do tbb <- verified_schedule bb;
OK (tbb :: tlbb)
end.
Definition transl_function (f: function) : res function :=
do lb <- transf_blocks (fn_blocks f);
OK (mkfunction (fn_sig f) lb).
Definition transf_function (f: function) : res function :=
do tf <- transl_function f;
if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
then Error (msg "code size exceeded")
else OK tf.
Definition transf_fundef (f: fundef) : res fundef :=
transf_partial_fundef transf_function f.
Definition transf_program (p: program) : res program :=
transform_partial_program transf_fundef p.
|
