src/clight/clightSwitch.ml

   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 }