forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
loop_liveScript.sml
215 lines (194 loc) · 7.34 KB
/
loop_liveScript.sml
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
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
(*
Correctness proof for loop to loop_remove
*)
open preamble loopLangTheory
loop_callTheory
val _ = new_theory "loop_live";
Definition vars_of_exp_def:
vars_of_exp (loopLang$Var v) l = insert v () l ∧
vars_of_exp (Const _) l = l ∧
vars_of_exp (BaseAddr) l = l ∧
vars_of_exp (Lookup _) l = l ∧
vars_of_exp (Load a) l = vars_of_exp a l ∧
vars_of_exp (Op x vs) l = vars_of_exp_list vs l ∧
vars_of_exp (Shift _ x _) l = vars_of_exp x l ∧
vars_of_exp_list xs l =
(case xs of [] => l
| (x::xs) => vars_of_exp x (vars_of_exp_list xs l))
Termination
WF_REL_TAC ‘measure (λx. case x of INL (x,_) => exp_size (K 0) x
| INR (x,_) => exp1_size (K 0) x)’
End
Theorem size_mk_BN:
∀t1 t2. size (mk_BN t1 t2) = size (BN t1 t2)
Proof
Cases \\ Cases \\ fs [mk_BN_def,size_def]
QED
Theorem size_mk_BS:
∀t1 t2 x. size (mk_BS t1 x t2) = size (BS t1 x t2)
Proof
Cases \\ Cases \\ fs [mk_BS_def,size_def]
QED
Theorem size_inter:
∀l1 l2. size (inter l1 l2) <= size l1
Proof
Induct \\ fs [inter_def]
\\ Cases_on ‘l2’ \\ fs [size_mk_BN,size_mk_BS]
\\ rewrite_tac [ADD_ASSOC,DECIDE “m+1≤n+1 ⇔ m ≤ n:num”]
\\ metis_tac [DECIDE “n1 ≤ m1 ∧ n2 ≤ m2 ⇒ n1+n2 ≤ m1+m2:num ∧ n1+n2 ≤ m1+m2+1”]
QED
Definition arith_vars:
arith_vars (LLongMul r1 r2 r3 r4) l =
insert r3 () $ insert r4 () $ delete r1 $ delete r2 l ∧
arith_vars (LDiv r1 r2 r3) l = insert r2 () $ insert r3 () $ delete r1 l ∧
arith_vars (LLongDiv r1 r2 r3 r4 r5) l =
insert r3 () $ insert r4 () $ insert r5 () $ delete r1 $ delete r2 l
End
(* This optimisation shrinks all cutsets and also deletes assignments
to unused variables. The Loop case is the interesting one: an
auxiliary function is used to find a fixed-point. *)
Definition shrink_def:
(shrink b (Seq p1 p2) l =
let (p2,l) = shrink b p2 l in
let (p1,l) = shrink b p1 l in
(Seq p1 p2, l)) /\
(shrink b (Loop live_in body live_out) l =
let l2 = inter live_out l in
case fixedpoint live_in LN l2 body of
| SOME (body,l0) =>
(let l = inter live_in l0 in (Loop l body l2, l))
| NONE => let (b,_) = shrink (live_in,l2) body l2 in
(Loop live_in b l2, live_in)) /\
(shrink b (If x1 x2 x3 p1 p2 l1) l =
let l = inter l l1 in
let (p1,l1) = shrink b p1 l in
let (p2,l2) = shrink b p2 l in
let l3 = (case x3 of Reg r => insert r () LN | _ => LN) in
(If x1 x2 x3 p1 p2 l, insert x2 () (union l3 (union l1 l2)))) /\
(shrink b (Mark p1) l = shrink b p1 l) /\
(shrink b Break l = (Break,SND b)) /\
(shrink b Continue l = (Continue,FST b)) /\
(shrink b Fail l = (Fail,LN)) /\
(shrink b Skip l = (Skip,l)) /\
(shrink b (Return v) l = (Return v, insert v () LN)) /\
(shrink b (Raise v) l = (Raise v, insert v () LN)) /\
(shrink b (Arith arith) l =
(Arith arith, arith_vars arith l)
) ∧
(shrink b (LocValue n m) l =
case lookup n l of
| NONE => (Skip,l)
| SOME _ => (LocValue n m, delete n l)) ∧
(shrink b (Assign n x) l =
case lookup n l of
| NONE => (Skip,l)
| SOME _ => (Assign n x, vars_of_exp x (delete n l))) ∧
(shrink b (ShMem op r ad) l =
(ShMem op r ad, (*case lookup r l of
NONE => l
| _ => if is_load op
then vars_of_exp ad (insert r () l)
else l)*)
vars_of_exp ad (insert r () l))) ∧
(shrink b (Store e n) l =
(Store e n, vars_of_exp e (insert n () l))) ∧
(shrink b (SetGlobal name e) l =
(SetGlobal name e, vars_of_exp e l)) ∧
(shrink b (Call ret dest args handler) l =
let a = fromAList (MAP (λx. (x,())) args) in
case ret of
| NONE => (Call NONE dest args NONE, union a l)
| SOME (n,l1) =>
case handler of
| NONE => let l3 = (delete n (inter l l1)) in
(Call (SOME (n,l3)) dest args NONE, union a l3)
| SOME (e,h,r,live_out) =>
let (r,l2) = shrink b r l in
let (h,l3) = shrink b h l in
let l1 = inter l1 (union (delete n l2) (delete e l3)) in
(Call (SOME (n,l1)) dest args (SOME (e,h,r,inter l live_out)),
union a l1)) ∧
(shrink b (FFI n r1 r2 r3 r4 l1) l =
(FFI n r1 r2 r3 r4 (inter l1 l),
insert r1 () (insert r2 () (insert r3 () (insert r4 () (inter l1 l)))))) ∧
(shrink b (LoadByte x y) l =
(LoadByte x y, insert x () (delete y l))) ∧
(shrink b (StoreByte x y) l =
(StoreByte x y, insert x () (insert y () l))) ∧
(shrink b prog l = (prog,l)) /\
(fixedpoint live_in l1 l2 body =
let (b,l0) = shrink (inter live_in l1,l2) body l2 in
let l0' = inter live_in l0 in
if l0' = l1 then (* fixed point found! *) SOME (b,l0) else
if size l0' ≤ size l1 then (* no progress made, not possible *) NONE else
fixedpoint live_in l0' l2 body)
Termination
WF_REL_TAC `inv_image (measure I LEX measure I LEX measure I)
(λx. case x of
| INL (_,c,_) => (prog_size (K 0) c, 0:num, 0)
| INR (live_in,l1,l2,body) =>
(prog_size (K 0) body, 1, size live_in - size l1))`
\\ rw [] \\ fs [GSYM NOT_LESS]
\\ qsuff_tac ‘size l1 < size live_in’ \\ fs []
\\ match_mp_tac LESS_LESS_EQ_TRANS
\\ asm_exists_tac \\ fs [size_inter]
End
Theorem exp_ind = vars_of_exp_ind
|> Q.SPECL [‘λx l. P x’,‘λx l. Q x’]
|> SIMP_RULE std_ss []
|> Q.GENL [‘P’,‘Q’];
Theorem fixedpoint_thm:
∀live_in l1 l2 (body:'a loopLang$prog) l0 b.
fixedpoint live_in l1 l2 body = SOME (b, l0) ⇒
shrink (inter live_in l0, l2) body l2 = (b, l0)
Proof
qmatch_abbrev_tac ‘entire_goal’
\\ qsuff_tac
‘(∀b (prog:'a loopLang$prog) l d. shrink b prog l = d ⇒ T) ∧ entire_goal’
THEN1 fs []
\\ unabbrev_all_tac
\\ ho_match_mp_tac shrink_ind \\ fs [] \\ rw []
\\ pop_assum mp_tac \\ once_rewrite_tac [shrink_def]
\\ fs [] \\ pairarg_tac \\ fs []
\\ fs [CaseEq"bool"] \\ rw [] \\ fs []
\\ fs [inter_assoc]
\\ pop_assum (fn th => rewrite_tac [GSYM th])
\\ rpt AP_THM_TAC \\ AP_TERM_TAC \\ fs []
\\ fs [lookup_inter_alt] \\ rw []
\\ fs [domain_lookup]
\\ Cases_on ‘lookup x live_in’ \\ fs []
QED
Definition mark_all_def:
(mark_all (Seq p1 p2) =
let (p1,t1) = mark_all p1 in
let (p2,t2) = mark_all p2 in
let t3 = (t1 /\ t2) in
(if t3 then Mark (Seq p1 p2) else Seq p1 p2, t3)) /\
(mark_all (Loop l1 body l2) =
let (body,t1) = mark_all body in
(Loop l1 body l2, F)) /\
(mark_all (If x1 x2 x3 p1 p2 l1) =
let (p1,t1) = mark_all p1 in
let (p2,t2) = mark_all p2 in
let p3 = If x1 x2 x3 p1 p2 l1 in
let t3 = (t1 /\ t2) in
(if t3 then Mark p3 else p3, t3)) /\
(mark_all (Mark p1) = mark_all p1) /\
(mark_all (Call ret dest args handler) =
case handler of
| NONE => (Mark (Call ret dest args handler), T)
| SOME (n,p1,p2,l) =>
let (p1,t1) = mark_all p1 in
let (p2,t2) = mark_all p2 in
let t3 = (t1 ∧ t2) in
let p3 = Call ret dest args (SOME (n,p1,p2,l)) in
(if t3 then Mark p3 else p3, t3)) /\
(mark_all prog = (Mark prog,T))
End
Definition comp_def:
comp prog = FST (mark_all (FST (shrink (LN,LN) prog LN)))
End
Definition optimise_def:
optimise prog = (comp o FST o loop_call$comp LN) prog
End
val _ = export_theory();