source: Deliverables/D2.2/8051/src/clight/clightSwitch.ml @ 1664

Last change on this file since 1664 was 1462, checked in by ayache, 8 years ago

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size: 2.6 KB
Line 
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
6let type_of (Clight.Expr (_, t)) = t
7
8
9let f_expr e _ = e
10
11let 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
18let replace_undeep_break lbl = ClightFold.statement2 f_expr (f_stmt lbl)
19
20
21let add_starting_lbl fresh stmt =
22  let lbl = fresh () in
23  (lbl, Clight.Slabel (lbl, stmt))
24
25let add_starting_lbl_list fresh stmts = List.map (add_starting_lbl fresh) stmts
26
27let add_ending_goto lbl stmt =
28  Clight.Ssequence (stmt, Clight.Slabel (lbl, Clight.Sskip))
29
30let make_sequence stmts =
31  let f sequence stmt = Clight.Ssequence (sequence, stmt) in
32  List.fold_left f Clight.Sskip stmts
33
34let 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
51let f_expr e _ = e
52
53let 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
59let simplify_statement fresh = ClightFold.statement2 f_expr (f_stmt fresh)
60
61let 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
67let 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 }
Note: See TracBrowser for help on using the repository browser.