blob: 74c2438e155c4dc4499dfe7f1712ceb61db95f0b (
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
|
(* *************************************************************)
(* *)
(* 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.
Extract Constant schedule => "PostpassSchedulingOracle.schedule".
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 verified_schedule (bb : bblock) : res bblock :=
let nhbb := no_header bb in
do nhbb' <- do_schedule nhbb;
let bb' := stick_header (header bb) nhbb' 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 do_schedule in EQ.
destruct schedule in EQ.
destruct (size (no_header bb) =? 1) eqn:TRIVB.
- inv EQ. unfold size. simpl. reflexivity.
- unfold schedule_to_bblock in EQ.
destruct o in EQ.
+ inv EQ. unfold verify_size in EQ1. unfold size in *. simpl in *.
rewrite Z.eqb_neq in TRIVB.
destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =?
Z.of_nat (Datatypes.length (header bb) + Datatypes.length l + 1)) eqn:ESIZE; try discriminate.
rewrite Z.eqb_eq in ESIZE; repeat rewrite Nat2Z.inj_add in *;
rewrite ESIZE. reflexivity.
+ unfold make_bblock_from_basics in EQ. destruct l in EQ; try discriminate.
inv EQ. unfold verify_size in EQ1; unfold size in *; simpl in *.
destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =?
Z.of_nat (Datatypes.length (header bb) + Datatypes.S (Datatypes.length l) + 0)) eqn:ESIZE; try discriminate.
rewrite Z.eqb_eq in ESIZE. repeat rewrite Nat2Z.inj_add in *.
rewrite ESIZE. 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.
|
