|
| 1 | +(* *********************************************************************) |
| 2 | +(* *) |
| 3 | +(* The Compcert verified compiler *) |
| 4 | +(* *) |
| 5 | +(* Xavier Leroy, Collège de France and Inria *) |
| 6 | +(* *) |
| 7 | +(* Copyright Institut National de Recherche en Informatique et en *) |
| 8 | +(* Automatique. All rights reserved. This file is distributed *) |
| 9 | +(* under the terms of the GNU Lesser General Public License as *) |
| 10 | +(* published by the Free Software Foundation, either version 2.1 of *) |
| 11 | +(* the License, or (at your option) any later version. *) |
| 12 | +(* This file is also distributed under the terms of the *) |
| 13 | +(* INRIA Non-Commercial License Agreement. *) |
| 14 | +(* *) |
| 15 | +(* *********************************************************************) |
| 16 | + |
| 17 | +(* Normalization of structured "switch" statements |
| 18 | + and emulation of unstructured "switch" statements (e.g. Duff's device) *) |
| 19 | + |
| 20 | +(* Assumes: code without blocks |
| 21 | + Produces: code without blocks and with normalized "switch" statements *) |
| 22 | + |
| 23 | +(* A normalized switch has the following form: |
| 24 | + Sswitch(e, Sseq (Slabeled(lbl1, case1), |
| 25 | + Sseq (... |
| 26 | + Sseq (Slabeled(lblN,caseN), Sskip) ...))) |
| 27 | +*) |
| 28 | + |
| 29 | +open Printf |
| 30 | +open C |
| 31 | +open Cutil |
| 32 | + |
| 33 | +let support_unstructured = ref false |
| 34 | + |
| 35 | +type switchlabel = |
| 36 | + | Case of exp * int64 |
| 37 | + | Default |
| 38 | + |
| 39 | +type switchbody = |
| 40 | + | Label of switchlabel * location |
| 41 | + | Stmt of stmt |
| 42 | + |
| 43 | +let rec flatten_switch = function |
| 44 | + | {sdesc = Sseq(s1, s2)} :: rem -> |
| 45 | + flatten_switch (s1 :: s2 :: rem) |
| 46 | + | {sdesc = Slabeled(Scase(e, n), s1); sloc = loc} :: rem -> |
| 47 | + Label(Case(e, n), loc) :: flatten_switch (s1 :: rem) |
| 48 | + | {sdesc = Slabeled(Sdefault, s1); sloc = loc} :: rem -> |
| 49 | + Label(Default, loc) :: flatten_switch (s1 :: rem) |
| 50 | + | {sdesc = Slabeled(Slabel lbl, s1); sloc = loc} :: rem -> |
| 51 | + Stmt {sdesc = Slabeled(Slabel lbl, Cutil.sskip); sloc = loc} |
| 52 | + :: flatten_switch (s1 :: rem) |
| 53 | + | s :: rem -> |
| 54 | + Stmt s :: flatten_switch rem |
| 55 | + | [] -> |
| 56 | + [] |
| 57 | + |
| 58 | +let rec group_switch = function |
| 59 | + | [] -> |
| 60 | + (Cutil.sskip, []) |
| 61 | + | Label(case, loc) :: rem -> |
| 62 | + let (fst, cases) = group_switch rem in |
| 63 | + (Cutil.sskip, (case, loc, fst) :: cases) |
| 64 | + | Stmt s :: rem -> |
| 65 | + let (fst, cases) = group_switch rem in |
| 66 | + (Cutil.sseq s.sloc s fst, cases) |
| 67 | + |
| 68 | +let label_of_switchlabel = function |
| 69 | + | Case(e, n) -> Scase(e, n) |
| 70 | + | Default -> Sdefault |
| 71 | + |
| 72 | +let make_slabeled (l, loc, s) = |
| 73 | + { sdesc = Slabeled(label_of_switchlabel l, s); sloc = loc } |
| 74 | + |
| 75 | +let make_sequence sl = |
| 76 | + List.fold_right (Cutil.sseq no_loc) sl Cutil.sskip |
| 77 | + |
| 78 | +let make_normalized_switch e cases = |
| 79 | + Sswitch(e, make_sequence (List.map make_slabeled cases)) |
| 80 | + |
| 81 | +let rec all_cases accu s = |
| 82 | + match s.sdesc with |
| 83 | + | Sseq(s1, s2) -> all_cases (all_cases accu s1) s2 |
| 84 | + | Sif(_, s1, s2) -> all_cases (all_cases accu s1) s2 |
| 85 | + | Swhile(_, s1) -> all_cases accu s1 |
| 86 | + | Sdowhile(s1, _) -> all_cases accu s1 |
| 87 | + | Sfor(s1, _, s2, s3) -> all_cases (all_cases (all_cases accu s1) s2) s3 |
| 88 | + | Sswitch(_, _) -> accu |
| 89 | + | Slabeled(Scase(e, n), s1) -> all_cases (Case(e, n) :: accu) s1 |
| 90 | + | Slabeled(Sdefault, s1) -> all_cases (Default :: accu) s1 |
| 91 | + | Slabeled(Slabel _, s1) -> all_cases accu s1 |
| 92 | + | Sblock _ -> assert false |
| 93 | + | _ -> accu |
| 94 | + |
| 95 | +let substitute_cases case_table body end_label = |
| 96 | + let sub = Hashtbl.create 32 in |
| 97 | + List.iter |
| 98 | + (fun (case, lbl) -> Hashtbl.add sub case (Slabel lbl)) |
| 99 | + case_table; |
| 100 | + let transf_label = function |
| 101 | + | Scase(e, n) -> |
| 102 | + (try Hashtbl.find sub (Case(e, n)) with Not_found -> assert false) |
| 103 | + | Sdefault -> |
| 104 | + (try Hashtbl.find sub Default with Not_found -> assert false) |
| 105 | + | Slabel _ as lbl -> lbl in |
| 106 | + let rec transf inloop s = |
| 107 | + {s with sdesc = |
| 108 | + match s.sdesc with |
| 109 | + | Sseq(s1, s2) -> Sseq(transf inloop s1, transf inloop s2) |
| 110 | + | Sif(e, s1, s2) -> Sif(e, transf inloop s1, transf inloop s2) |
| 111 | + | Swhile(e, s1) -> Swhile(e, transf true s1) |
| 112 | + | Sdowhile(s1, e) -> Sdowhile(transf true s1, e) |
| 113 | + | Sfor(s1, e, s2, s3) -> |
| 114 | + Sfor(transf inloop s1, e, transf inloop s2, transf true s3) |
| 115 | + | Sbreak -> if inloop then Sbreak else Sgoto end_label |
| 116 | + | Slabeled(lbl, s1) -> Slabeled(transf_label lbl, transf inloop s1) |
| 117 | + | Sblock _ -> assert false |
| 118 | + | sd -> sd } |
| 119 | + in transf false body |
| 120 | + |
| 121 | +let rec is_skip_or_debug s = |
| 122 | + match s.sdesc with |
| 123 | + | Sseq (a, b) -> is_skip_or_debug a && is_skip_or_debug b |
| 124 | + | Sskip -> true |
| 125 | + | _ -> Cutil.is_debug_stmt s |
| 126 | + |
| 127 | +let new_label = ref 0 |
| 128 | + |
| 129 | +let gen_label () = incr new_label; sprintf "@%d" !new_label |
| 130 | + |
| 131 | +let normalize_switch loc e body = |
| 132 | + let (init, cases) = [body] |> flatten_switch |> group_switch |
| 133 | + and allcases = List.rev (all_cases [] body) in |
| 134 | + if is_skip_or_debug init && List.length cases = List.length allcases then |
| 135 | + (* This is a structured switch *) |
| 136 | + make_normalized_switch e cases |
| 137 | + else begin |
| 138 | + (* This switch needs to be converted *) |
| 139 | + if not !support_unstructured then |
| 140 | + Diagnostics.error loc |
| 141 | + "unsupported feature: non-structured 'switch' statement \ |
| 142 | + (consider adding option [-funstructured-switch])"; |
| 143 | + let case_table = List.map (fun case -> (case, gen_label())) allcases in |
| 144 | + let end_lbl = gen_label() in |
| 145 | + let newbody = substitute_cases case_table body end_lbl in |
| 146 | + let goto_case (case, lbl) = |
| 147 | + (case, no_loc, {sdesc = Sgoto lbl; sloc = no_loc}) in |
| 148 | + let case_table' = |
| 149 | + if List.mem_assoc Default case_table |
| 150 | + then case_table |
| 151 | + else (Default, end_lbl) :: case_table in |
| 152 | + Sseq({sdesc = make_normalized_switch e (List.map goto_case case_table'); |
| 153 | + sloc = loc}, |
| 154 | + sseq no_loc newbody |
| 155 | + {sdesc = Slabeled(Slabel end_lbl, sskip); sloc = no_loc}) |
| 156 | + end |
| 157 | + |
| 158 | +let rec transform_stmt s = |
| 159 | + { s with sdesc = |
| 160 | + match s.sdesc with |
| 161 | + | Sseq(s1, s2) -> Sseq(transform_stmt s1, transform_stmt s2) |
| 162 | + | Sif(e, s1, s2) -> Sif(e, transform_stmt s1, transform_stmt s2) |
| 163 | + | Swhile(e, s1) -> Swhile(e, transform_stmt s1) |
| 164 | + | Sdowhile(s1, e) -> Sdowhile(transform_stmt s1, e) |
| 165 | + | Sfor(s1, e, s2, s3) -> |
| 166 | + Sfor(transform_stmt s1, e, transform_stmt s2, transform_stmt s3) |
| 167 | + | Sswitch(e, s1) -> normalize_switch s.sloc e (transform_stmt s1) |
| 168 | + | Slabeled(lbl, s1) -> Slabeled(lbl, transform_stmt s1) |
| 169 | + | Sblock sl -> Sblock(List.map transform_stmt sl) |
| 170 | + | sd -> sd} |
| 171 | + |
| 172 | +let transform_fundef env loc fd = |
| 173 | + { fd with fd_body = transform_stmt fd.fd_body } |
| 174 | + |
| 175 | +(* Entry point *) |
| 176 | + |
| 177 | +let program unstructured p = |
| 178 | + support_unstructured := unstructured; |
| 179 | + Transform.program ~fundef: transform_fundef p |
0 commit comments