src/cminor/cminorLabelling.ml

   1
   2 (** This module defines the labelling of a [Cminor] program. *)
   3
   4
   5 let prefix = "_cost"
   6
   7
   8 (* Add a cost label in front of a statement. *)
   9
  10 let add_starting_cost_label cost_universe stmt =
  11   Cminor.St_cost (CostLabel.Gen.fresh cost_universe, stmt)
  12
  13 (* Add a cost label at the end of a statement. *)
  14
  15 let add_ending_cost_label cost_universe stmt =
  16   Cminor.St_seq (stmt, add_starting_cost_label cost_universe Cminor.St_skip)
  17
  18
  19 (* This function adds cost labels to an expression, given the result on its
  20    sub-expressions. *)
  21
  22 let f_add_cost_labels_exp cost_universe e subexp_res = match e, subexp_res with
  23   | Cminor.Id _, _ | Cminor.Cst _, _ -> e
  24   | Cminor.Op1 (op1, _), [e] -> Cminor.Op1 (op1, e)
  25   | Cminor.Op2 (op2, _, _), [e1 ; e2] -> Cminor.Op2 (op2, e1, e2)
  26   | Cminor.Mem (chunk, _), [e] -> Cminor.Mem (chunk, e)
  27   | Cminor.Cond _, [e1 ; e2 ; e3] ->
  28     let e2 = Cminor.Exp_cost (CostLabel.Gen.fresh cost_universe, e2) in
  29     let e3 = Cminor.Exp_cost (CostLabel.Gen.fresh cost_universe, e3) in
  30     Cminor.Cond (e1, e2, e3)
  31   | Cminor.Exp_cost (lab, _), [e] -> Cminor.Exp_cost (lab, e)
  32   | _ -> assert false (* wrong number of arguments *)
  33
  34 (* This function adds cost labels to a statement, given the result on its
  35    sub-expressions and sub-statements. *)
  36
  37 let f_add_cost_labels_body cost_universe stmt subexp_res substmt_res =
  38   match stmt, subexp_res, substmt_res with
  39     | Cminor.St_skip, _, _ | Cminor.St_exit _, _, _
  40     | Cminor.St_goto _, _, _ | Cminor.St_return None, _, _ ->
  41       stmt
  42     | Cminor.St_assign (x, _), [e], _ ->
  43       Cminor.St_assign (x, e)
  44     | Cminor.St_store (chunk, _, _), [e1 ; e2], _ ->
  45       Cminor.St_store (chunk, e1, e2)
  46     | Cminor.St_call (x, _, _, sg), f :: args, _ ->
  47       Cminor.St_call (x, f, args, sg)
  48     | Cminor.St_tailcall (_, _, sg), f :: args, _ ->
  49       Cminor.St_tailcall (f, args, sg)
  50     | Cminor.St_seq _, _, [stmt1 ; stmt2] ->
  51       Cminor.St_seq (stmt1, stmt2)
  52     | Cminor.St_ifthenelse _, [e], [stmt1 ; stmt2] ->
  53       let stmt1 = add_starting_cost_label cost_universe stmt1 in
  54       let stmt2 = add_starting_cost_label cost_universe stmt2 in
  55       Cminor.St_ifthenelse (e, stmt1, stmt2)
  56     | Cminor.St_loop _, _, [stmt] ->
  57       let stmt = add_starting_cost_label cost_universe stmt in
  58       add_ending_cost_label cost_universe (Cminor.St_loop stmt)
  59     | Cminor.St_block _, _, [stmt] ->
  60       Cminor.St_block stmt
  61     | Cminor.St_switch (_, tbl, dflt), [e], _ ->
  62       add_ending_cost_label cost_universe (Cminor.St_switch (e, tbl, dflt))
  63     | Cminor.St_return _, [e], _ ->
  64       Cminor.St_return (Some e)
  65     | Cminor.St_label (lab, _), _, [stmt] ->
  66       let stmt = add_starting_cost_label cost_universe stmt in
  67       Cminor.St_label (lab, stmt)
  68     | Cminor.St_cost (lab, _), _, [stmt] ->
  69       Cminor.St_cost (lab, stmt)
  70     | _ -> assert false (* wrong number of arguments *)
  71
  72 (* Add cost labels to a statement. *)
  73
  74 let add_cost_labels_body cost_universe stmt =
  75   CminorFold.statement
  76     (f_add_cost_labels_exp cost_universe)
  77     (f_add_cost_labels_body cost_universe)
  78     stmt
  79
  80 (* Add cost labels to a function definition. *)
  81
  82 let add_cost_labels_functs cost_universe functs (f_id, f_def) =
  83   match f_def with
  84     | Cminor.F_int def ->
  85         let body = add_cost_labels_body cost_universe def.Cminor.f_body in
  86         let body = add_starting_cost_label cost_universe body in
  87         let def' = { def with Cminor.f_body = body } in
  88         functs @ [(f_id, Cminor.F_int def')]
  89     | Cminor.F_ext _ -> functs @ [(f_id, f_def)]
  90
  91 (** [add_cost_labels prog] inserts some labels to enable cost annotation. *)
  92
  93 let add_cost_labels prog =
  94   let labs = CminorAnnotator.all_labels prog in
  95   let labs = StringTools.Set.fold CostLabel.Set.add labs CostLabel.Set.empty in
  96   let cost_prefix = CostLabel.Gen.fresh_prefix labs prefix in
  97   let cost_universe = CostLabel.Gen.new_universe cost_prefix in
  98   let functs =
  99     List.fold_left (add_cost_labels_functs cost_universe) []
 100       prog.Cminor.functs in
 101   { prog with Cminor.functs = functs }