source: src/Clight/switchRemoval.ma @ 1915

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

Correction of a typo in switchRemoval.

  • Property svn:executable set to *
File size: 9.8 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 *)
104
105alias id "bvzero" = "cic:/matita/cerco/ASM/BitVector/zero.def(2)".
106
107let 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 ≝
112match 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). *)
145definition 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 ]
154qed.
155
156(* recursively convert a statement into a switch-free one. *)
157
158let rec switch_removal
159  (st : statement)
160  (vars : list (ident × type))
161  (uv : universe SymbolTag) : (Σresult.switch_free result) × (list (ident × type)) × (universe SymbolTag) ≝
162match 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
211and 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) ≝
215match 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].
224try @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
232let 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
Note: See TracBrowser for help on using the repository browser.