1 | include "Clight/Csyntax.ma". |
---|
2 | include "Clight/fresh.ma". |
---|
3 | include "basics/lists/list.ma". |
---|
4 | |
---|
5 | (* This file implements transformation of switches to linear, nested sequences of |
---|
6 | * if/then/else. The implementation roughly follows the lines of the prototype. |
---|
7 | * /!\ We assume that the program is well-typed (the type of the evaluated |
---|
8 | * expression must match the constants on each branch of the switch). /!\ *) |
---|
9 | |
---|
10 | (* Property of a Clight statement of containing no switch. Could be generalized into a kind of |
---|
11 | * statement_P, if useful elsewhere. *) |
---|
12 | let rec switch_free (st : statement) : Prop ≝ |
---|
13 | match st with |
---|
14 | [ Sskip ⇒ True |
---|
15 | | Sassign _ _ ⇒ True |
---|
16 | | Scall _ _ _ ⇒ True |
---|
17 | | Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2 |
---|
18 | | Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2 |
---|
19 | | Swhile e body ⇒ switch_free body |
---|
20 | | Sdowhile e body ⇒ switch_free body |
---|
21 | | Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3 |
---|
22 | | Sbreak ⇒ True |
---|
23 | | Scontinue ⇒ True |
---|
24 | | Sreturn _ ⇒ True |
---|
25 | | Sswitch _ _ ⇒ False |
---|
26 | | Slabel _ body ⇒ switch_free body |
---|
27 | | Sgoto _ ⇒ True |
---|
28 | | Scost _ body ⇒ switch_free body |
---|
29 | ]. |
---|
30 | |
---|
31 | definition sf_statement ≝ Σs:statement. switch_free s. |
---|
32 | |
---|
33 | definition stlist ≝ list (label × (𝚺sz.bvint sz) × sf_statement). |
---|
34 | |
---|
35 | (* Property of a list of labeled statements of being switch-free *) |
---|
36 | let rec branches_switch_free (sts : labeled_statements) : Prop ≝ |
---|
37 | match sts with |
---|
38 | [ LSdefault st => |
---|
39 | switch_free st |
---|
40 | | LScase _ _ st tl => |
---|
41 | switch_free st ∧ branches_switch_free tl |
---|
42 | ]. |
---|
43 | |
---|
44 | let rec branch_switch_free_ind |
---|
45 | (sts : labeled_statements) |
---|
46 | (H : labeled_statements → Prop) |
---|
47 | (defcase : ∀st. H (LSdefault st)) |
---|
48 | (indcase : ∀sz.∀int.∀st.∀sub_cases. H sub_cases → H (LScase sz int st sub_cases)) ≝ |
---|
49 | match sts with |
---|
50 | [ LSdefault st ⇒ |
---|
51 | defcase st |
---|
52 | | LScase sz int st tl ⇒ |
---|
53 | indcase sz int st tl (branch_switch_free_ind tl H defcase indcase) |
---|
54 | ]. |
---|
55 | |
---|
56 | let rec add_starting_lbl_list |
---|
57 | (l : labeled_statements) |
---|
58 | (H : branches_switch_free l) |
---|
59 | (uv : universe SymbolTag) |
---|
60 | (acc : stlist) : stlist × (label × sf_statement) × (universe SymbolTag) ≝ |
---|
61 | match l return λl'. l = l' → stlist × (label × sf_statement) × (universe SymbolTag) with |
---|
62 | [ LSdefault st ⇒ λEq. |
---|
63 | let 〈default_lab, uv'〉 ≝ fresh ? uv in |
---|
64 | 〈rev ? acc, 〈default_lab, «st, ?»〉, uv'〉 |
---|
65 | | LScase sz tag st other_cases ⇒ λEq. |
---|
66 | let 〈lab, uv'〉 ≝ fresh ? uv in |
---|
67 | let acc' ≝ 〈lab, (mk_DPair ?? sz tag), «st, ?»〉 :: acc in |
---|
68 | add_starting_lbl_list other_cases ? uv' acc' |
---|
69 | ] (refl ? l). |
---|
70 | [ 1: destruct whd in H; // |
---|
71 | | 2: letin H1 ≝ H >Eq in H1; |
---|
72 | #H' normalize in H'; elim H' // |
---|
73 | | 3: >Eq in H; normalize * // |
---|
74 | ] qed. |
---|
75 | |
---|
76 | let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝ |
---|
77 | match st with |
---|
78 | [ Sbreak ⇒ |
---|
79 | Sgoto lab |
---|
80 | | Ssequence s1 s2 ⇒ |
---|
81 | Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab) |
---|
82 | | Sifthenelse e iftrue iffalse ⇒ |
---|
83 | Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab) |
---|
84 | | Sfor init e update body ⇒ |
---|
85 | Sfor (convert_break_to_goto init lab) e update body |
---|
86 | | Slabel l body ⇒ |
---|
87 | Slabel l (convert_break_to_goto body lab) |
---|
88 | | Scost cost body ⇒ |
---|
89 | Scost cost (convert_break_to_goto body lab) |
---|
90 | | _ ⇒ st |
---|
91 | ]. |
---|
92 | |
---|
93 | lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label). |
---|
94 | #s elim s // |
---|
95 | [ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/ |
---|
96 | | 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/ |
---|
97 | | 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize |
---|
98 | try @conj try @conj /3/ |
---|
99 | | 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/ |
---|
100 | | 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/ |
---|
101 | ] qed. |
---|
102 | |
---|
103 | (* We assume that the expression e is consistely typed w.r.t. the switch branches *) |
---|
104 | |
---|
105 | alias id "bvzero" = "cic:/matita/cerco/ASM/BitVector/zero.def(2)". |
---|
106 | |
---|
107 | let rec produce_cond |
---|
108 | (e : expr) |
---|
109 | (switch_cases : stlist) |
---|
110 | (def_case : ident × sf_statement) |
---|
111 | (exit : label) on switch_cases : sf_statement × label ≝ |
---|
112 | match switch_cases with |
---|
113 | [ nil ⇒ |
---|
114 | match def_case with |
---|
115 | [ mk_Prod default_label default_statement ⇒ |
---|
116 | 〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉 |
---|
117 | ] |
---|
118 | | cons switch_case tail ⇒ |
---|
119 | let 〈case_label, case_value, case_statement〉 ≝ switch_case in |
---|
120 | match case_value with |
---|
121 | [ mk_DPair sz val ⇒ |
---|
122 | let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in |
---|
123 | (* let test ≝ Expr (Ebinop Oeq e e) (Tint I32 Unsigned) in *) |
---|
124 | (* let test ≝ Expr (Econst_int I32 (bvzero 32)) (Tint I32 Signed) in *) |
---|
125 | let 〈sub_statement, sub_label〉 ≝ produce_cond e tail def_case exit in |
---|
126 | let result ≝ |
---|
127 | Sifthenelse test |
---|
128 | (Slabel case_label |
---|
129 | (Ssequence (convert_break_to_goto (pi1 … case_statement) exit) |
---|
130 | (Sgoto sub_label))) |
---|
131 | (pi1 … sub_statement) |
---|
132 | in |
---|
133 | 〈«result, ?», case_label〉 |
---|
134 | ] |
---|
135 | ]. |
---|
136 | [ 1: normalize @convert_break_lift elim default_statement // |
---|
137 | | 2: whd @conj normalize try @conj try // |
---|
138 | [ 1: @convert_break_lift elim case_statement // |
---|
139 | | 2: elim sub_statement // ] |
---|
140 | ] qed. |
---|
141 | |
---|
142 | (* takes an expression, a list of switch-free cases and a freshgen and returns a |
---|
143 | * switch-free equivalent, along an updated freshgen and a new local variable |
---|
144 | * (for storing the value of the expr). *) |
---|
145 | definition simplify_switch : |
---|
146 | expr → ∀l:labeled_statements. branches_switch_free l → (universe SymbolTag) → sf_statement × (universe SymbolTag) ≝ |
---|
147 | λe.λswitch_cases.λH.λuv. |
---|
148 | let 〈exit_label, uv1〉 ≝ fresh ? uv in |
---|
149 | let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list switch_cases ? uv1 [ ] in |
---|
150 | let 〈result, useless_label〉 ≝ produce_cond e switch_cases defcase exit_label in |
---|
151 | 〈«Ssequence (pi1 … result) (Slabel exit_label Sskip), ?», uv2〉. |
---|
152 | [ 1: normalize try @conj try @conj try // elim result // |
---|
153 | | 2: @H ] |
---|
154 | qed. |
---|
155 | |
---|
156 | (* recursively convert a statement into a switch-free one. *) |
---|
157 | |
---|
158 | let rec switch_removal |
---|
159 | (st : statement) |
---|
160 | (vars : list (ident × type)) |
---|
161 | (uv : universe SymbolTag) : (Σresult.switch_free result) × (list (ident × type)) × (universe SymbolTag) ≝ |
---|
162 | match st return λs.s = st → ? with |
---|
163 | [ Sskip ⇒ λEq. 〈«st,?», vars, uv〉 |
---|
164 | | Sassign _ _ ⇒ λEq. 〈«st,?», vars, uv〉 |
---|
165 | | Scall _ _ _ ⇒ λEq. 〈«st,?», vars, uv〉 |
---|
166 | | Ssequence s1 s2 ⇒ λEq. |
---|
167 | let 〈s1', vars1, uv'〉 ≝ switch_removal s1 vars uv in |
---|
168 | let 〈s2', vars2, uv''〉 ≝ switch_removal s2 vars1 uv' in |
---|
169 | 〈«Ssequence (pi1 … s1') (pi1 … s2'),?», vars2, uv''〉 |
---|
170 | | Sifthenelse e s1 s2 ⇒ λEq. |
---|
171 | let 〈s1', vars1, uv'〉 ≝ switch_removal s1 vars uv in |
---|
172 | let 〈s2', vars2, uv''〉 ≝ switch_removal s2 vars1 uv' in |
---|
173 | 〈«Sifthenelse e (pi1 … s1') (pi1 … s2'),?», vars2, uv''〉 |
---|
174 | | Swhile e body ⇒ λEq. |
---|
175 | let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in |
---|
176 | 〈«Swhile e (pi1 … body'),?», vars', uv'〉 |
---|
177 | | Sdowhile e body ⇒ λEq. |
---|
178 | let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in |
---|
179 | 〈«Sdowhile e (pi1 … body'),?», vars', uv'〉 |
---|
180 | | Sfor s1 e s2 s3 ⇒ λEq. |
---|
181 | let 〈s1', vars1, uv'〉 ≝ switch_removal s1 vars uv in |
---|
182 | let 〈s2', vars2, uv''〉 ≝ switch_removal s2 vars1 uv' in |
---|
183 | let 〈s3', vars3, uv'''〉 ≝ switch_removal s3 vars2 uv'' in |
---|
184 | 〈«Sfor (pi1 … s1') e (pi1 … s2') (pi1 … s3'),?», vars3, uv'''〉 |
---|
185 | | Sbreak ⇒ λEq. |
---|
186 | 〈«st,?», vars, uv〉 |
---|
187 | | Scontinue ⇒ λEq. |
---|
188 | 〈«st,?», vars, uv〉 |
---|
189 | | Sreturn _ ⇒ λEq. |
---|
190 | 〈«st,?», vars, uv〉 |
---|
191 | | Sswitch e branches ⇒ λEq. |
---|
192 | let 〈sf_branches, vars', uv1〉 ≝ switch_removal_branches branches vars uv in |
---|
193 | match sf_branches with |
---|
194 | [ mk_Sig branches' H ⇒ |
---|
195 | let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in |
---|
196 | let ident ≝ Expr (Evar switch_tmp) (typeof e) in |
---|
197 | let assign ≝ Sassign ident e in |
---|
198 | let 〈result, uv3〉 ≝ simplify_switch ident branches' H uv2 in |
---|
199 | 〈«Ssequence assign (pi1 … result), ?», (〈switch_tmp, typeof e〉 :: vars'), uv3〉 |
---|
200 | ] |
---|
201 | | Slabel label body ⇒ λEq. |
---|
202 | let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in |
---|
203 | 〈«Slabel label (pi1 … body'), ?», vars', uv'〉 |
---|
204 | | Sgoto _ ⇒ λEq. |
---|
205 | 〈«st, ?», vars, uv〉 |
---|
206 | | Scost cost body ⇒ λEq. |
---|
207 | let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in |
---|
208 | 〈«Scost cost (pi1 … body'),?», vars', uv'〉 |
---|
209 | ] (refl ? st) |
---|
210 | |
---|
211 | and switch_removal_branches |
---|
212 | (l : labeled_statements) |
---|
213 | (vars : list (ident × type)) |
---|
214 | (uv : universe SymbolTag) : (Σl'.branches_switch_free l') × (list (ident × type)) × (universe SymbolTag) ≝ |
---|
215 | match l with |
---|
216 | [ LSdefault st ⇒ |
---|
217 | let 〈st, vars', uv'〉 ≝ switch_removal st vars uv in |
---|
218 | 〈«LSdefault (pi1 … st), ?», vars', uv'〉 |
---|
219 | | LScase sz int st tl => |
---|
220 | let 〈tl_result, vars', uv'〉 ≝ switch_removal_branches tl vars uv in |
---|
221 | let 〈st', vars'', uv''〉 ≝ switch_removal st vars' uv' in |
---|
222 | 〈«LScase sz int st' (pi1 … tl_result), ?», vars'', uv''〉 |
---|
223 | ]. |
---|
224 | try @conj destruct try elim s1' try elim s2' try elim s3' try elim body' whd try // |
---|
225 | [ 1: #st1 #H1 #st2 #H2 #st3 #H3 @conj // |
---|
226 | | 2: elim result // |
---|
227 | | 3: elim st // |
---|
228 | | 4: elim st' // |
---|
229 | | 5: elim tl_result // |
---|
230 | ] qed. |
---|
231 | |
---|
232 | let rec program_switch_removal (p : clight_program) : clight_program ≝ |
---|
233 | let uv ≝ universe_for_program p in |
---|
234 | let prog_funcs ≝ prog_funct ?? p in |
---|
235 | |
---|
236 | let 〈sf_funcs, final_uv〉 ≝ |
---|
237 | foldr ?? (λcl_fundef.λacc. |
---|
238 | let 〈fundefs, uv1〉 ≝ acc in |
---|
239 | let 〈fun_id, fun_def〉 ≝ cl_fundef in |
---|
240 | match fun_def with |
---|
241 | [ CL_Internal func ⇒ |
---|
242 | let 〈body', fun_vars, uv2〉 ≝ switch_removal (fn_body func) (fn_vars func) uv1 in |
---|
243 | let new_func ≝ mk_function (fn_return func) (fn_params func) fun_vars (pi1 … body') in |
---|
244 | 〈(〈fun_id, CL_Internal new_func〉 :: fundefs), uv2〉 |
---|
245 | | CL_External _ _ _ ⇒ |
---|
246 | 〈cl_fundef :: fundefs, uv1〉 |
---|
247 | ] |
---|
248 | ) 〈[ ], uv〉 prog_funcs |
---|
249 | in |
---|
250 | mk_program ?? |
---|
251 | (prog_vars … p) |
---|
252 | sf_funcs |
---|
253 | (prog_main … p) |
---|
254 | . |
---|
255 | |
---|
256 | |
---|
257 | |
---|
258 | |
---|
259 | |
---|
260 | |
---|
261 | |
---|
262 | |
---|
263 | |
---|
264 | |
---|