blob: 62833dc33b0fc843fd1911862d1bd215aa71ff06 (
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
|
Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep Op Registers OptionMonad.
Require Import Errors RTL BTL BTLmatchRTL.
(** TODO: adapt stuff RTLpathLivegen *)
Local Open Scope lazy_bool_scope.
Local Open Scope option_monad_scope.
Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool :=
match rl with
| nil => true
| r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive
end.
Definition reg_option_mem (or: option reg) (alive: Regset.t) :=
match or with None => true | Some r => Regset.mem r alive end.
Definition reg_sum_mem (ros: reg + ident) (alive: Regset.t) :=
match ros with inl r => Regset.mem r alive | inr s => true end.
(* NB: definition following [regmap_setres] in [RTL.step] semantics *)
Definition reg_builtin_res (res: builtin_res reg) (alive: Regset.t): Regset.t :=
match res with
| BR r => Regset.add r alive
| _ => alive
end.
Definition exit_checker {A} (btl: code) (alive: Regset.t) (s: node) (v: A): option A :=
SOME next <- btl!s IN
ASSERT Regset.subset next.(input_regs) alive IN
Some v.
Fixpoint exit_list_checker (btl: code) (alive: Regset.t) (l: list node): bool :=
match l with
| nil => true
| s :: l' => exit_checker btl alive s true &&& exit_list_checker btl alive l'
end.
Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option unit :=
match fin with
| Bgoto s =>
exit_checker btl alive s tt
| Breturn oreg =>
ASSERT reg_option_mem oreg alive IN Some tt
| Bcall _ ros args res s =>
ASSERT list_mem args alive IN
ASSERT reg_sum_mem ros alive IN
exit_checker btl (Regset.add res alive) s tt
| Btailcall _ ros args =>
ASSERT list_mem args alive IN
ASSERT reg_sum_mem ros alive IN Some tt
| Bbuiltin _ args res s =>
ASSERT list_mem (params_of_builtin_args args) alive IN
exit_checker btl (reg_builtin_res res alive) s tt
| Bjumptable arg tbl =>
ASSERT Regset.mem arg alive IN
ASSERT exit_list_checker btl alive tbl IN Some tt
end.
Definition is_none {A} (oa: option A): bool :=
match oa with
| Some _ => false
| None => true
end.
Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option (Regset.t*option final) :=
match ib with
| Bseq ib1 ib2 =>
SOME res <- body_checker btl ib1 alive IN
ASSERT is_none (snd res) IN
body_checker btl ib2 (fst res)
| Bnop _ => Some (alive, None)
| Bop _ args dest _ =>
ASSERT list_mem args alive IN
Some (Regset.add dest alive, None)
| Bload _ _ _ args dest _ =>
ASSERT list_mem args alive IN
Some (Regset.add dest alive, None)
| Bstore _ _ args src _ =>
ASSERT Regset.mem src alive IN
ASSERT list_mem args alive IN
Some (alive, None)
| Bcond _ args (BF (Bgoto s) _) (Bnop None) _ =>
ASSERT list_mem args alive IN
exit_checker btl alive s (alive, None)
| BF fin _ => Some (alive, Some fin)
| _ => None
end.
Definition iblock_checker (btl: code) (ib: iblock) (alive: Regset.t) : option unit :=
SOME res <- body_checker btl ib alive IN
SOME fin <- snd res IN
final_inst_checker btl (fst res) fin.
Fixpoint list_iblock_checker (btl: code) (l: list (node*iblock_info)): bool :=
match l with
| nil => true
| (_, ibf) :: l' => iblock_checker btl ibf.(entry) ibf.(input_regs) &&& list_iblock_checker btl l'
end.
Lemma lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true.
Proof.
destruct o; simpl; intuition.
- eauto.
- firstorder. try_simplify_someHyps.
Qed.
Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true.
Proof.
intros; rewrite lazy_and_Some_true; firstorder.
destruct x; auto.
Qed.
Lemma list_iblock_checker_correct btl l:
list_iblock_checker btl l = true -> forall e, List.In e l -> iblock_checker btl (snd e).(entry) (snd e).(input_regs) = Some tt.
Proof.
intros CHECKER e H; induction l as [|(n & ibf) l]; intuition.
simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
Qed.
Definition liveness_checker (f: BTL.function): res unit :=
match list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) with
| true => OK tt
| false => Error (msg "BTL_Livecheck: liveness_checker failed")
end.
Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt.
(** TODO: adapt stuff RTLpathLivegenproof *)
Local Notation ext alive := (fun r => Regset.In r alive).
Lemma regset_add_spec live r1 r2: Regset.In r1 (Regset.add r2 live) <-> (r1 = r2 \/ Regset.In r1 live).
Proof.
destruct (Pos.eq_dec r1 r2).
- subst. intuition; eapply Regset.add_1; auto.
- intuition.
* right. eapply Regset.add_3; eauto.
* eapply Regset.add_2; auto.
Qed.
Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop :=
forall r, (alive r) -> rs1#r = rs2#r.
(* continue to adapt stuff RTLpathLivegenproof *)
Section FSEM_SIMULATES_CFGSEM.
Variable prog: BTL.program.
Let ge := Genv.globalenv prog.
Hypothesis liveness_checker_correct: forall b f, Genv.find_funct_ptr ge b = Some (Internal f) -> liveness_ok_function f.
Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog).
Proof.
exploit liveness_checker_correct.
Admitted.
End FSEM_SIMULATES_CFGSEM.
|
