source: src/Clight/switchRemoval.ma @ 2016

Last change on this file since 2016 was 2016, checked in by garnier, 8 years ago

Slight change in simplification strategy to better match the semantics

  • Property svn:executable set to *
File size: 11.0 KB
Line 
1include "Clight/Csyntax.ma".
2include "Clight/fresh.ma".
3include "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. *)
12let rec switch_free (st : statement) : Prop ≝
13match 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
31definition sf_statement ≝ Σs:statement. switch_free s.
32
33definition stlist ≝ list (label × (𝚺sz.bvint sz) × sf_statement).
34
35(* Property of a list of labeled statements of being switch-free *)
36let rec branches_switch_free (sts : labeled_statements) : Prop ≝
37match sts with
38[ LSdefault st =>
39  switch_free st
40| LScase _ _ st tl =>
41  switch_free st ∧ branches_switch_free tl
42].
43
44let 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)) ≝
49match 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
56let 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) ≝
61match 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
76let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝
77match 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
93lemma 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 *)
104let rec produce_cond
105  (e : expr)
106  (switch_cases : stlist)
107  (def_case : ident × sf_statement)
108  (exit : label) on switch_cases : sf_statement × label ≝
109match switch_cases with
110[ nil ⇒
111  match def_case with
112  [ mk_Prod default_label default_statement ⇒
113    〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉
114  ]
115| cons switch_case tail ⇒
116  let 〈case_label, case_value, case_statement〉 ≝ switch_case in
117    match case_value with
118    [ mk_DPair sz val ⇒
119       let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in
120       (* let test ≝ Expr (Ebinop Oeq e e) (Tint I32 Unsigned) in *)
121       (* let test ≝ Expr (Econst_int I32 (bvzero 32)) (Tint I32 Signed)  in *)
122       let 〈sub_statement, sub_label〉 ≝ produce_cond e tail def_case exit in
123       let result ≝
124         Sifthenelse test
125          (Slabel case_label
126            (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)
127                       (Sgoto sub_label)))
128          (pi1 … sub_statement)
129      in
130      〈«result, ?», case_label〉
131    ]
132].
133[ 1: normalize @convert_break_lift elim default_statement //
134| 2: whd @conj normalize try @conj try //
135  [ 1: @convert_break_lift elim case_statement //
136  | 2: elim sub_statement // ]
137] qed.
138
139let rec produce_cond2
140  (e : expr)
141  (switch_cases : stlist)
142  (def_case : ident × sf_statement)
143  (exit : label) on switch_cases : sf_statement × label ≝
144match switch_cases with
145[ nil ⇒
146  let 〈default_label, default_statement〉 ≝ def_case in
147  〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉
148| cons switch_case tail ⇒
149  let 〈case_label, case_value, case_statement〉 ≝ switch_case in
150  match case_value with
151  [ mk_DPair sz val ⇒
152    let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in
153    let 〈sub_statement, sub_label〉 ≝ produce_cond2 e tail def_case exit in
154    let case_statement_res ≝
155       Sifthenelse test
156        (Slabel case_label
157          (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)
158                     (Sgoto sub_label)))
159        Sskip
160    in
161    〈«Ssequence case_statement_res (pi1 … sub_statement), ?», case_label〉
162  ]
163].
164[ 1: normalize @convert_break_lift elim default_statement //
165| 2: whd @conj
166     [ 1: whd @conj try // whd in match (switch_free ?); @conj
167          [ 1: @convert_break_lift elim case_statement //
168          | 2: // ]
169     | 2: elim sub_statement // ]
170] qed.     
171         
172
173
174(* takes an expression, a list of switch-free cases and a freshgen and returns a
175 * switch-free equivalent, along an updated freshgen and a new local variable
176 * (for storing the value of the expr). *)
177definition simplify_switch :
178  expr → ∀l:labeled_statements. branches_switch_free l → (universe SymbolTag) → sf_statement × (universe SymbolTag) ≝
179λe.λswitch_cases.λH.λuv.
180 let 〈exit_label, uv1〉            ≝ fresh ? uv in
181 let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list switch_cases ? uv1 [ ] in
182 let 〈result, useless_label〉      ≝ produce_cond2 e switch_cases defcase exit_label in
183 〈«Ssequence (pi1 … result) (Slabel exit_label Sskip), ?», uv2〉.
184[ 1:  normalize try @conj try @conj try // elim result //
185| 2: @H ]
186qed.
187
188(* recursively convert a statement into a switch-free one. *)
189let rec switch_removal
190  (st : statement)
191  (vars : list (ident × type))
192  (uv : universe SymbolTag) : (Σresult.switch_free result) × (list (ident × type)) × (universe SymbolTag) ≝
193match st return λs.s = st → ? with
194[ Sskip       ⇒ λEq. 〈«st,?», vars, uv〉
195| Sassign _ _ ⇒ λEq. 〈«st,?», vars, uv〉
196| Scall _ _ _ ⇒ λEq. 〈«st,?», vars, uv〉
197| Ssequence s1 s2 ⇒ λEq.
198  let 〈s1', vars1, uv'〉  ≝ switch_removal s1 vars uv in
199  let 〈s2', vars2, uv''〉 ≝ switch_removal s2 vars1 uv' in
200  〈«Ssequence (pi1 … s1') (pi1 … s2'),?», vars2, uv''〉
201| Sifthenelse e s1 s2 ⇒ λEq.
202  let 〈s1', vars1, uv'〉  ≝ switch_removal s1 vars uv in
203  let 〈s2', vars2, uv''〉 ≝ switch_removal s2 vars1 uv' in
204  〈«Sifthenelse e (pi1 … s1') (pi1 … s2'),?», vars2, uv''〉
205| Swhile e body ⇒ λEq.
206  let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in
207  〈«Swhile e (pi1 … body'),?», vars', uv'〉
208| Sdowhile e body ⇒ λEq.
209  let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in
210  〈«Sdowhile e (pi1 … body'),?», vars', uv'〉
211| Sfor s1 e s2 s3 ⇒ λEq.
212  let 〈s1', vars1, uv'〉   ≝ switch_removal s1 vars uv in
213  let 〈s2', vars2, uv''〉  ≝ switch_removal s2 vars1 uv' in
214  let 〈s3', vars3, uv'''〉 ≝ switch_removal s3 vars2 uv'' in 
215  〈«Sfor (pi1 … s1') e (pi1 … s2') (pi1 … s3'),?», vars3, uv'''〉 
216| Sbreak ⇒ λEq.
217  〈«st,?», vars, uv〉
218| Scontinue ⇒ λEq.
219  〈«st,?», vars, uv〉
220| Sreturn _ ⇒ λEq.
221  〈«st,?», vars, uv〉
222| Sswitch e branches ⇒ λEq.
223   let 〈sf_branches, vars', uv1〉 ≝ switch_removal_branches branches vars uv in
224   match sf_branches with
225   [ mk_Sig branches' H ⇒
226     let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in
227     let ident             ≝ Expr (Evar switch_tmp) (typeof e) in
228     let assign            ≝ Sassign ident e in     
229     let 〈result, uv3〉     ≝ simplify_switch ident branches' H uv2 in
230     〈«Ssequence assign (pi1 … result), ?», (〈switch_tmp, typeof e〉 :: vars'), uv3〉
231   ]
232| Slabel label body ⇒ λEq.
233  let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in
234  〈«Slabel label (pi1 … body'), ?», vars', uv'〉
235| Sgoto _ ⇒ λEq.
236  〈«st, ?», vars, uv〉
237| Scost cost body ⇒ λEq.
238  let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in
239  〈«Scost cost (pi1 … body'),?», vars', uv'〉
240] (refl ? st)
241
242and switch_removal_branches
243  (l : labeled_statements)
244  (vars : list (ident × type))
245  (uv : universe SymbolTag) : (Σl'.branches_switch_free l') × (list (ident × type)) × (universe SymbolTag) ≝
246match l with
247[ LSdefault st ⇒
248  let 〈st, vars',  uv'〉 ≝ switch_removal st vars uv in
249  〈«LSdefault (pi1 … st), ?», vars', uv'〉
250| LScase sz int st tl =>
251  let 〈tl_result, vars', uv'〉 ≝ switch_removal_branches tl vars uv in
252  let 〈st', vars'', uv''〉     ≝ switch_removal st vars' uv' in
253  〈«LScase sz int st' (pi1 … tl_result), ?», vars'', uv''〉
254].
255try @conj destruct try elim s1' try elim s2' try elim s3' try elim body' whd try //
256[ 1: #st1 #H1 #st2 #H2 #st3 #H3 @conj //
257| 2: elim result //
258| 3: elim st //
259| 4: elim st' //
260| 5: elim tl_result //
261] qed.
262
263let rec program_switch_removal (p : clight_program) : clight_program ≝
264 let uv         ≝ universe_for_program p in
265 let prog_funcs ≝ prog_funct ?? p in
266 let 〈sf_funcs, final_uv〉 ≝
267  foldr ?? (λcl_fundef.λacc.
268    let 〈fundefs, uv1〉    ≝ acc in
269    let 〈fun_id, fun_def〉 ≝ cl_fundef in
270    match fun_def with
271    [ CL_Internal func ⇒
272      let 〈body', fun_vars, uv2〉 ≝ switch_removal (fn_body func) (fn_vars func) uv1 in
273      let new_func ≝ mk_function (fn_return func) (fn_params func) fun_vars (pi1 … body') in
274      〈(〈fun_id, CL_Internal new_func〉 :: fundefs), uv2〉
275    | CL_External _ _ _ ⇒
276      〈cl_fundef :: fundefs, uv1〉
277    ]
278   ) 〈[ ], uv〉 prog_funcs
279 in
280 mk_program ??
281  (prog_vars … p)
282  sf_funcs
283  (prog_main … p).
284
285
286
287
288
289
290
291
292
293
Note: See TracBrowser for help on using the repository browser.