blob: 63b914ec310fc17232431946b3f06eea160e23c2 (
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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
|
Require Import Coqlib.
Require Import Maps.
Require Import Lattice.
Require Import AST.
Require Import Op.
Require Import Registers.
Require Import Globalenvs Smallstep RTL RTLpath.
Require Import Bool Errors.
Require Import Program.
Require RTLpathLivegen.
Local Open Scope lazy_bool_scope.
Local Open Scope option_monad_scope.
Definition exit_checker {A} (pm: path_map) (pc: node) (v:A): option A :=
SOME path <- pm!pc IN
Some v.
Lemma exit_checker_path_entry A (pm: path_map) (pc: node) (v:A) res:
exit_checker pm pc v = Some res -> path_entry pm pc.
Proof.
unfold exit_checker, path_entry.
inversion_SOME path; simpl; congruence.
Qed.
Lemma exit_checker_res A (pm: path_map) (pc: node) (v:A) res:
exit_checker pm pc v = Some res -> v=res.
Proof.
unfold exit_checker, path_entry.
inversion_SOME path; try_simplify_someHyps.
Qed.
Definition iinst_checker (pm: path_map) (i: instruction): option (node) :=
match i with
| Inop pc' | Iop _ _ _ pc' | Iload _ _ _ _ _ pc'
| Istore _ _ _ _ pc' => Some (pc')
| Icond cond args ifso ifnot _ =>
exit_checker pm ifso ifnot
| _ => None
end.
Local Hint Resolve exit_checker_path_entry: core.
Lemma iinst_checker_path_entry (pm: path_map) (i: instruction) res pc:
iinst_checker pm i = Some res ->
early_exit i = Some pc -> path_entry pm pc.
Proof.
destruct i; simpl; try_simplify_someHyps; subst.
Qed.
Lemma iinst_checker_default_succ (pm: path_map) (i: instruction) res pc:
iinst_checker pm i = Some res ->
pc = res ->
default_succ i = Some pc.
Proof.
destruct i; simpl; try_simplify_someHyps; subst;
repeat (inversion_ASSERT); try_simplify_someHyps.
intros; exploit exit_checker_res; eauto.
intros; subst. simpl; auto.
Qed.
Fixpoint ipath_checker (ps:nat) (f: RTL.function) (pm: path_map) (pc:node): option (node) :=
match ps with
| O => Some (pc)
| S p =>
SOME i <- f.(fn_code)!pc IN
SOME res <- iinst_checker pm i IN
ipath_checker p f pm res
end.
Lemma ipath_checker_wellformed f pm ps: forall pc res,
ipath_checker ps f pm pc = Some res ->
wellformed_path f.(fn_code) pm 0 res ->
wellformed_path f.(fn_code) pm ps pc.
Proof.
induction ps; simpl; try_simplify_someHyps.
inversion_SOME i; inversion_SOME res'.
intros. eapply wf_internal_node; eauto.
* eapply iinst_checker_default_succ; eauto.
* intros; eapply iinst_checker_path_entry; eauto.
Qed.
Fixpoint exit_list_checker (pm: path_map) (l: list node): bool :=
match l with
| nil => true
| pc::l' => exit_checker pm pc tt &&& exit_list_checker pm l'
end.
Lemma exit_list_checker_correct pm l pc:
exit_list_checker pm l = true -> List.In pc l -> exit_checker pm pc tt = Some tt.
Proof.
intros EXIT PC; induction l; intuition.
simpl in * |-. rewrite RTLpathLivegen.lazy_and_Some_tt_true in EXIT.
firstorder (subst; eauto).
Qed.
Local Hint Resolve exit_list_checker_correct: core.
Definition inst_checker (pm: path_map) (i: instruction): option unit :=
match i with
| Icall sig ros args res pc' =>
exit_checker pm pc' tt
| Itailcall sig ros args =>
Some tt
| Ibuiltin ef args res pc' =>
exit_checker pm pc' tt
| Ijumptable arg tbl =>
ASSERT exit_list_checker pm tbl IN
Some tt
| Ireturn optarg =>
Some tt
| _ =>
SOME res <- iinst_checker pm i IN
exit_checker pm res tt
end.
Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (i: instruction):
inst_checker pm i = Some tt ->
c!pc = Some i -> wellformed_path c pm 0 pc.
Proof.
intros CHECK PC. eapply wf_last_node; eauto.
clear c pc PC. intros pc PC.
destruct i; simpl in * |- *; intuition (subst; eauto);
try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
intros X; exploit exit_checker_res; eauto.
clear X. intros; subst; eauto.
Qed.
Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
SOME res <- ipath_checker (path.(psize)) f pm pc IN
SOME i <- f.(fn_code)!res IN
inst_checker pm i.
Lemma path_checker_wellformed f pm pc path:
path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc.
Proof.
unfold path_checker.
inversion_SOME res.
inversion_SOME i.
intros; eapply ipath_checker_wellformed; eauto.
eapply inst_checker_wellformed; eauto.
Qed.
Fixpoint list_path_checker f pm (l:list (node*path_info)): bool :=
match l with
| nil => true
| (pc, path)::l' =>
path_checker f pm pc path &&& list_path_checker f pm l'
end.
Lemma list_path_checker_correct f pm l:
list_path_checker f pm l = true -> forall e, List.In e l -> path_checker f pm (fst e) (snd e) = Some tt.
Proof.
intros CHECKER e H; induction l as [|(pc & path) l]; intuition.
simpl in * |- *. rewrite RTLpathLivegen.lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
Qed.
Definition function_checker (f: RTL.function) (pm: path_map): bool :=
pm!(f.(fn_entrypoint)) &&& list_path_checker f pm (PTree.elements pm).
Lemma function_checker_correct f pm pc path:
function_checker f pm = true ->
pm!pc = Some path ->
path_checker f pm pc path = Some tt.
Proof.
unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true.
intros (ENTRY & PATH) PC.
exploit list_path_checker_correct; eauto.
- eapply PTree.elements_correct; eauto.
- simpl; auto.
Qed.
Lemma function_checker_wellformed_path_map f pm:
function_checker f pm = true -> wellformed_path_map f.(fn_code) pm.
Proof.
unfold wellformed_path_map.
intros; eapply path_checker_wellformed; eauto.
intros; eapply function_checker_correct; eauto.
Qed.
Lemma function_checker_path_entry f pm:
function_checker f pm = true -> path_entry pm (f.(fn_entrypoint)).
Proof.
unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true;
unfold path_entry. firstorder congruence.
Qed.
|
