1 | |
---|
2 | (** This module performs a switch simplification: they are replaced by |
---|
3 | equivalent if-then-else statements. This is a temporary hack before |
---|
4 | implementing switch tables. *) |
---|
5 | |
---|
6 | let type_of (Clight.Expr (_, t)) = t |
---|
7 | |
---|
8 | |
---|
9 | let f_expr e _ = e |
---|
10 | |
---|
11 | let f_stmt lbl stmt sub_exprs_res sub_stmts_res = |
---|
12 | match stmt, sub_stmts_res with |
---|
13 | | Clight.Sbreak, _ -> Clight.Sgoto lbl |
---|
14 | | Clight.Swhile _, _ | Clight.Sdowhile _, _ |
---|
15 | | Clight.Sfor _, _ | Clight.Sswitch _, _ -> stmt |
---|
16 | | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res |
---|
17 | |
---|
18 | let replace_undeep_break lbl = ClightFold.statement2 f_expr (f_stmt lbl) |
---|
19 | |
---|
20 | |
---|
21 | let add_starting_lbl fresh stmt = |
---|
22 | let lbl = fresh () in |
---|
23 | (lbl, Clight.Slabel (lbl, stmt)) |
---|
24 | |
---|
25 | let add_starting_lbl_list fresh stmts = List.map (add_starting_lbl fresh) stmts |
---|
26 | |
---|
27 | let add_ending_goto lbl stmt = |
---|
28 | Clight.Ssequence (stmt, Clight.Slabel (lbl, Clight.Sskip)) |
---|
29 | |
---|
30 | let make_sequence stmts = |
---|
31 | let f sequence stmt = Clight.Ssequence (sequence, stmt) in |
---|
32 | List.fold_left f Clight.Sskip stmts |
---|
33 | |
---|
34 | let simplify_switch fresh e cases stmts = |
---|
35 | let exit_lbl = fresh () in |
---|
36 | let (lbls, stmts) = List.split (add_starting_lbl_list fresh stmts) in |
---|
37 | let stmts = List.map (replace_undeep_break exit_lbl) stmts in |
---|
38 | let rec aux cases lbls = match cases, lbls with |
---|
39 | | Clight.LSdefault _, lbl :: _ -> [Clight.Sgoto lbl] |
---|
40 | | Clight.LScase (i, _, cases), lbl :: lbls -> |
---|
41 | let next_cases = aux cases lbls in |
---|
42 | let ret_type = Clight.Tint (Clight.I32, AST.Signed) in |
---|
43 | let cst_i = Clight.Expr (Clight.Econst_int i, type_of e) in |
---|
44 | let test = Clight.Expr (Clight.Ebinop (Clight.Oeq, e, cst_i), ret_type) in |
---|
45 | Clight.Sifthenelse (test, Clight.Sgoto lbl, Clight.Sskip) :: next_cases |
---|
46 | | _ -> |
---|
47 | (* Do not use on these arguments: wrong list size. *) |
---|
48 | assert false in |
---|
49 | add_ending_goto exit_lbl (make_sequence ((aux cases lbls) @ stmts)) |
---|
50 | |
---|
51 | let f_expr e _ = e |
---|
52 | |
---|
53 | let f_stmt fresh stmt sub_exprs_res sub_stmts_res = |
---|
54 | match stmt, sub_stmts_res with |
---|
55 | | Clight.Sswitch (e, cases), sub_stmts -> |
---|
56 | simplify_switch fresh e cases sub_stmts |
---|
57 | | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res |
---|
58 | |
---|
59 | let simplify_statement fresh = ClightFold.statement2 f_expr (f_stmt fresh) |
---|
60 | |
---|
61 | let simplify_fundef fresh = function |
---|
62 | | Clight.Internal cfun -> |
---|
63 | let fn_body = simplify_statement fresh cfun.Clight.fn_body in |
---|
64 | Clight.Internal { cfun with Clight.fn_body = fn_body } |
---|
65 | | fundef -> fundef |
---|
66 | |
---|
67 | let simplify p = |
---|
68 | let labels = ClightAnnotator.all_labels p in |
---|
69 | let fresh = StringTools.make_fresh labels "_tmp_switch" in |
---|
70 | let f (id, fundef) = (id, simplify_fundef fresh fundef) in |
---|
71 | { p with Clight.prog_funct = List.map f p.Clight.prog_funct } |
---|