(* this type should hold global information used by the heuristics to take a *)
(* decision. As for now we employ a trivial heuristics, no information *)
(* is actually needed. *)
type heuristics_info = unit
let mk_heuristics_info (p : Clight.program) = ()
(* this function tells when to perform the optimization on a statement. It *)
(* should always return [false] when the optimization cannot be applied *)
let heuristics
(_ : heuristics_info)
: Clight.statement -> bool = function
| Clight.Swhile (Some _, _, _) | Clight.Sfor (Some _, _, _, _, _)
| Clight.Sdowhile (Some _, _, _) -> true
| _ -> false
let zero_sexpr = CostLabel.Sexpr(0,0)
let succ_sexpr = CostLabel.Sexpr(1,1)
let f_expr_reindex i s e expr_res =
match e, expr_res with
| Clight.Expr (Clight.Ecost (lbl, _), t), e::_ ->
let lbl = CostLabel.comp_index i s lbl in
Clight.Expr (Clight.Ecost (lbl, e), t)
| _ -> ClightFold.expr_fill_exprs e expr_res
(** compose the mapping i |--> s with all labels in a statement *)
let reindex_stmt i s =
let f_stmt stmt expr_res stmt_res =
match stmt, stmt_res with
| Clight.Scost(lbl, _), stmt' :: _ ->
let lbl = CostLabel.comp_index i s lbl in
Clight.Scost(lbl,stmt')
| _ -> ClightFold.statement_fill_subs stmt expr_res stmt_res in
ClightFold.statement2 (f_expr_reindex i s) f_stmt
(** compose the mapping i |--> s with all labels in an expression *)
let reindex_expr i s =
ClightFold.expr2 (f_expr_reindex i s)
let labels_of =
let f_expr _ _ = () in
let f_stmt stmt _ res_stmts =
let s = match stmt with
| Clight.Slabel(lbl, _) -> Label.Set.singleton lbl
| _ -> Label.Set.empty in
List.fold_left Label.Set.union s res_stmts in
ClightFold.statement2 f_expr f_stmt
let create_fresh_labels fresh lbl_set =
let f_lbl lbl = Label.Map.add lbl (fresh ()) in
Label.Set.fold f_lbl lbl_set Label.Map.empty
let apply_label_map map =
let f_stmt stmt exprs stmts =
match stmt, stmts with
| Clight.Slabel (lbl, _), s :: _ ->
(* lbl must be in domain of map *)
Clight.Slabel (Label.Map.find lbl map, s)
| Clight.Sgoto lbl, _ ->
Clight.Sgoto (
try
Label.Map.find lbl map
with
| Not_found -> (* means it is an outgoing goto *)
lbl)
| _ -> ClightFold.statement_fill_subs stmt exprs stmts in
ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt
let remove_cnt_brk cnt_lbl brk_lbl =
let f_stmt stmt exprs stmts =
match stmt with
| Clight.Sbreak -> Clight.Sgoto brk_lbl
| Clight.Scontinue -> Clight.Sgoto cnt_lbl
| _ ->ClightFold. statement_fill_subs stmt exprs stmts in
ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt
let peel fresh info =
let process_cnt_brk peeled_body has_brk has_cnt =
let (brk_lbl, add_tail) = if has_brk then
let new_lbl = fresh () in
(new_lbl, fun stmt ->
Clight.Ssequence (stmt, Clight.Slabel (new_lbl, Clight.Sskip)))
else
(Label.dummy, fun stmt -> stmt) in
let (cnt_lbl, add_head) = if has_cnt then
let new_lbl = fresh () in
(new_lbl, fun stmt -> Clight.Slabel(new_lbl, stmt))
else
(Label.dummy, fun stmt -> stmt) in
(* we could avoid making a further pass, but sacrificing the use
of the fold machinery *)
let peeled_body = if has_brk || has_cnt then
remove_cnt_brk cnt_lbl brk_lbl peeled_body
else peeled_body in
(add_head, peeled_body, add_tail) in
let f_stmt stmt exprs stmts_w_flags =
if heuristics info stmt then
match stmt, exprs, stmts_w_flags with
| Clight.Swhile (Some i, _, _), e :: _, (s, (has_brk, has_cnt)) :: _ ->
(* we can suppose no label in stmt is target of a goto outside of stmt, *)
(* as loop is indexed and thus single entry. So we can freely rename *)
(* labels in stmt. Notice outgoing gotos are not changed *)
let label_map = create_fresh_labels fresh (labels_of s) in
let s_first = apply_label_map label_map s in
(* reindex to zero the copies of s and e *)
let s_first = reindex_stmt i zero_sexpr s_first in
let e_first = reindex_expr i zero_sexpr e in
(* reindex to successor the other copies of s and e *)
let s_next = reindex_stmt i succ_sexpr s in
let e_next = reindex_expr i succ_sexpr e in
(* rebuild the loop *)
let loop = Clight.Swhile(Some i, e_next, s_next) in
(* all break and continue statements, if any, must be replaced by
gotos in the peeled body *)
let (head, s_first, tail) = process_cnt_brk s_first has_brk has_cnt in
(* build the peeled loop *)
let peeled = Clight.Ssequence(s_first, head loop) in
(tail (Clight.Sifthenelse(e_first, peeled, Clight.Sskip)),
(false, false))
| Clight.Sdowhile (Some i, _, _), e :: _,
(s, (has_brk, has_cnt)) :: _ ->
(* we can suppose no label in stmt is target of a goto outside, *)
(* as loop is indexed and thus single entry. So we can freely rename *)
(* labels in stmt. *)
let label_map = create_fresh_labels fresh (labels_of s) in
let s_first = apply_label_map label_map s in
(* reindex to zero the copies of s and e *)
let s_first = reindex_stmt i zero_sexpr s_first in
let e_first = reindex_expr i zero_sexpr e in
(* reindex to successor the other copies of s and e *)
let s_next = reindex_stmt i succ_sexpr s in
let e_next = reindex_expr i succ_sexpr e in
(* rebuild the loop *)
let loop = Clight.Sdowhile(Some i, e_next, s_next) in
let (head, s_first, tail) = process_cnt_brk s_first has_brk has_cnt in
(* put a guard before the following iterations of the loop *)
let guarded_loop =
Clight.Sifthenelse(e_first, head loop, Clight.Sskip) in
(* build the peeled loop *)
(tail (Clight.Ssequence(s_first, guarded_loop)), (false, false))
| Clight.Sfor (Some i, _, _, _, _), e :: _,
(s1, _) :: (s2, _) :: (s3, (has_brk, has_cnt)) ::_ ->
(* we can suppose no label in s3 is target of a goto outside of stmt, *)
(* as loop is indexed and thus single entry. So we can freely rename *)
(* labels in stmt. *)
(* IMPORTANT: I am supposing no labels are in s1 and s2 *)
let label_map = create_fresh_labels fresh (labels_of s3) in
let s3_first = apply_label_map label_map s3 in
(* reindex to zero the copies of s2, s3 and e *)
let s2_first = reindex_stmt i zero_sexpr s2 in
let s3_first = reindex_stmt i zero_sexpr s3_first in
let e_first = reindex_expr i zero_sexpr e in
(* reindex to successor the other copies of s2, s3 and e *)
let s2_next = reindex_stmt i succ_sexpr s2 in
let s3_next = reindex_stmt i succ_sexpr s3 in
let e_next = reindex_expr i succ_sexpr e in
(* rebuild the loop *)
let loop = Clight.Sfor(Some i, s2_first, e_next, s2_next, s3_next) in
let (head, s3_first, tail) =
process_cnt_brk s3_first has_brk has_cnt in
(* build the peeled loop *)
let peeled = Clight.Ssequence(s3_first, head loop) in
let guarded = Clight.Sifthenelse(e_first, peeled, Clight.Sskip) in
(* add the guard at the start *)
(tail (Clight.Ssequence(s1, guarded)), (false, false))
| _ -> assert false (* heuristics should have crossed out other cases *)
else match stmt with
| Clight.Sbreak -> (Clight.Sbreak, (true, false))
| Clight.Scontinue -> (Clight.Scontinue, (false, true))
| _ ->
let stmts, flags = List.split stmts_w_flags in
let f (b1, b2) (c1, c2) = (b1 || c1, b2 || c2) in
(ClightFold.statement_fill_subs stmt exprs stmts,
List.fold_left f (false, false) flags) in
ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt
let peel_funct fresh info = function
| (id, Clight.Internal def) ->
let body, _ = peel fresh info def.Clight.fn_body in
(id, Clight.Internal {def with Clight.fn_body = body})
| _ as p -> p
let apply p =
let fresh = ClightAnnotator.make_fresh "_l" p in
let info = mk_heuristics_info p in
let functs = List.map (peel_funct fresh info) p.Clight.prog_funct in
{p with Clight.prog_funct = functs}
open Languages
let trans =
(Clight, function (AstClight p) -> AstClight (apply p) | _ -> assert false)