src/cminor/cminorAnnotator.ml

   1
   2 let int_size = Driver.CminorMemory.int_size
   3
   4 let funct_vars (id, fun_def) = match fun_def with
   5   | Cminor.F_int def ->
   6     id :: (List.map fst (def.Cminor.f_params @ def.Cminor.f_vars))
   7   | _ -> [id]
   8
   9 let prog_idents p =
  10   let vars = List.map (fun (x, _, _) -> x) p.Cminor.vars in
  11   let f vars funct = vars @ (funct_vars funct) in
  12   let vars = List.fold_left f vars p.Cminor.functs in
  13   let f vars var = StringTools.Set.add var vars in
  14   List.fold_left f StringTools.Set.empty vars
  15
  16 let fresh_cost_id prefix p =
  17   let vars = prog_idents p in
  18   StringTools.Gen.fresh_prefix vars prefix
  19
  20
  21 (*
  22 let increment cost_id incr =
  23   let cost =
  24     Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol cost_id), AST.Sig_ptr) in
  25   let load = Cminor.Expr (Cminor.Mem (Memory.QInt 4, cost), AST.Sig_int 4) in
  26   let incr = Cminor.Expr (Cminor.Cst (AST.Cst_int incr), AST.Sig_int 4) in
  27   let incr = Cminor.Expr (Cminor.Op2 (AST.Op_add, load, incr), AST.Sig_int 4) in
  28   Cminor.St_store (Memory.QInt 4, cost, incr)
  29
  30
  31 let f_remove_cost_labels_exp e subexp_res = match e, subexp_res with
  32   | Cminor.Id _, _ | Cminor.Cst _, _ -> e
  33   | Cminor.Op1 (op, _), [e1] -> Cminor.Op1 (op, e1)
  34   | Cminor.Op2 (op, _, _), [e1 ; e2] -> Cminor.Op2 (op, e1, e2)
  35   | Cminor.Mem (chunk, _), [e] -> Cminor.Mem (chunk, e)
  36   | Cminor.Cond (_, _, _), [e1 ; e2 ; e3] -> Cminor.Cond (e1, e2, e3)
  37   | Cminor.Exp_cost _, [e] -> e
  38   | _ -> assert false (* wrong number of arguments *)
  39
  40 let remove_cost_labels_exp e =
  41   CminorFold.expression f_remove_cost_labels_exp e
  42
  43 let remove_cost_labels_exps exps =
  44   List.map remove_cost_labels_exp exps
  45
  46
  47 let list_seq l =
  48   let f res stmt = Cminor.St_seq (res, stmt) in
  49   List.fold_left f Cminor.St_skip l
  50
  51 let f_update_cost_exp costs_mapping cost_id e subexp_res =
  52   match e, subexp_res with
  53     | Cminor.Cond (e1, _, _), [stmt1 ; stmt2 ; stmt3] ->
  54       Cminor.St_seq (stmt1, Cminor.St_ifthenelse (e1, stmt2, stmt3))
  55     | Cminor.Exp_cost (lbl, _), [stmt2] ->
  56       let incr =
  57         if CostLabel.Map.mem lbl costs_mapping then
  58           CostLabel.Map.find lbl costs_mapping
  59         else 0 in
  60       let stmt1 = increment cost_id incr in
  61       Cminor.St_seq (stmt1, stmt2)
  62     | _ -> list_seq subexp_res
  63
  64 let update_cost_exp costs_mapping cost_id e =
  65   CminorFold.expression (f_update_cost_exp costs_mapping cost_id) e
  66
  67 let update_cost_exps costs_mapping cost_id exps =
  68   let l = List.map (update_cost_exp costs_mapping cost_id) exps in
  69   let f stmt upd = Cminor.St_seq (stmt, upd) in
  70   List.fold_left f Cminor.St_skip l
  71
  72
  73 let rec instrument_stmt costs_mapping cost_id body = match body with
  74   | Cminor.St_skip | Cminor.St_exit _ | Cminor.St_return None -> body
  75   | Cminor.St_assign (x, e) ->
  76       let upd = update_cost_exp costs_mapping cost_id e in
  77       let e = remove_cost_labels_exp e in
  78       Cminor.St_seq (upd, Cminor.St_assign (x, e))
  79   | Cminor.St_store (chunk, e1, e2) ->
  80       let upd = update_cost_exps costs_mapping cost_id [e1 ; e2] in
  81       let e1 = remove_cost_labels_exp e1 in
  82       let e2 = remove_cost_labels_exp e2 in
  83       Cminor.St_seq (upd, Cminor.St_store (chunk, e1, e2))
  84   | Cminor.St_call (ox, f, args, sg) ->
  85       let upd = update_cost_exps costs_mapping cost_id (f :: args) in
  86       let f = remove_cost_labels_exp f in
  87       let args = remove_cost_labels_exps args in
  88       Cminor.St_seq (upd, Cminor.St_call (ox, f, args, sg))
  89   | Cminor.St_tailcall (f, args, sg) ->
  90       let upd = update_cost_exps costs_mapping cost_id (f :: args) in
  91       let f = remove_cost_labels_exp f in
  92       let args = remove_cost_labels_exps args in
  93       Cminor.St_seq (upd, Cminor.St_tailcall (f, args, sg))
  94   | Cminor.St_seq (stmt1, stmt2) ->
  95       let stmt1 = instrument_stmt costs_mapping cost_id stmt1 in
  96       let stmt2 = instrument_stmt costs_mapping cost_id stmt2 in
  97       Cminor.St_seq (stmt1, stmt2)
  98   | Cminor.St_ifthenelse (e, stmt1, stmt2) ->
  99       let upd = update_cost_exp costs_mapping cost_id e in
 100       let e = remove_cost_labels_exp e in
 101       let stmt1 = instrument_stmt costs_mapping cost_id stmt1 in
 102       let stmt2 = instrument_stmt costs_mapping cost_id stmt2 in
 103       Cminor.St_seq (upd, Cminor.St_ifthenelse (e, stmt1, stmt2))
 104   | Cminor.St_loop stmt ->
 105       Cminor.St_loop (instrument_stmt costs_mapping cost_id stmt)
 106   | Cminor.St_block stmt ->
 107       Cminor.St_block (instrument_stmt costs_mapping cost_id stmt)
 108   | Cminor.St_switch (e, tbl, dflt) ->
 109       let upd = update_cost_exp costs_mapping cost_id e in
 110       let e = remove_cost_labels_exp e in
 111       Cminor.St_seq (upd, Cminor.St_switch (e, tbl, dflt))
 112   | Cminor.St_label (lbl, stmt) ->
 113       Cminor.St_label (lbl, instrument_stmt costs_mapping cost_id stmt)
 114   | Cminor.St_goto lbl -> body
 115   | Cminor.St_return (Some e) ->
 116       let upd = update_cost_exp costs_mapping cost_id e in
 117       let e = remove_cost_labels_exp e in
 118       Cminor.St_seq (upd, Cminor.St_return (Some e))
 119   | Cminor.St_cost (lbl, stmt) ->
 120       let incr =
 121         if CostLabel.Map.mem lbl costs_mapping then
 122           CostLabel.Map.find lbl costs_mapping
 123         else 0 in
 124       let stmt = instrument_stmt costs_mapping cost_id stmt in
 125       if incr = 0 then stmt
 126       else Cminor.St_seq (increment cost_id incr, stmt)
 127
 128
 129 let instrument_function costs_mapping cost_id = function
 130   | Cminor.F_int int_def ->
 131       let body = instrument_stmt costs_mapping cost_id int_def.Cminor.f_body in
 132       let def = { int_def with Cminor.f_body = body} in
 133       Cminor.F_int def
 134   | def -> def
 135
 136
 137 (** [instrument prog cost_map] instruments the program [prog]. First a fresh
 138     global variable --- the so-called cost variable --- is added to the program.
 139     Then, each cost label in the program is replaced by an increment of the cost
 140     variable, following the mapping [cost_map]. The function also returns the
 141     name of the cost variable and the name of the cost increment function. *)
 142
 143 let instrument p costs_mapping =
 144   let cost_id = fresh_cost_id "_cost" p in
 145   let vars = (cost_id, [AST.Data_int32 0]) :: p.Cminor.vars in
 146   let f (f_name, f_def) =
 147     (f_name, instrument_function costs_mapping cost_id f_def) in
 148   let functs = List.map f p.Cminor.functs in
 149   ({ Cminor.vars   = vars ;
 150      Cminor.functs = functs ;
 151      Cminor.main   = p.Cminor.main },
 152    "" (* TODO *),
 153    "" (* TODO *))
 154 *)
 155
 156
 157 (* Program cost labels and labels *)
 158
 159 let labels_empty = (CostLabel.Set.empty, Label.Set.empty)
 160
 161 let add_cost_label lbl (cost_label, user_label) =
 162   (CostLabel.Set.add lbl cost_label, user_label)
 163
 164 let add_label lbl (cost_label, user_label) =
 165   (cost_label, Label.Set.add lbl user_label)
 166
 167 let labels_union (cost_labels1, user_labels1) (cost_labels2, user_labels2) =
 168   (CostLabel.Set.union cost_labels1 cost_labels2,
 169    Label.Set.union user_labels1 user_labels2)
 170
 171 let labels_union_list l =
 172   let f res labels = labels_union res labels in
 173   List.fold_left f labels_empty l
 174
 175 let f_exp_labels (Cminor.Expr (ed, _)) subexp_res =
 176   let labels1 = labels_union_list subexp_res in
 177   let labels2 = match ed with
 178     | Cminor.Exp_cost (lbl, _) -> add_cost_label lbl labels_empty
 179     | _ -> labels_empty in
 180   labels_union labels1 labels2
 181
 182 let f_body_labels stmt subexp_res substmt_res =
 183   let labels1 = labels_union_list subexp_res in
 184   let labels2 = labels_union_list substmt_res in
 185   let labels = labels_union labels1 labels2 in
 186   let labels3 = match stmt with
 187     | Cminor.St_label (lbl, _) -> add_label lbl labels_empty
 188     | Cminor.St_cost (lbl, _) -> add_cost_label lbl labels_empty
 189     | _ -> labels_empty in
 190   labels_union labels labels3
 191
 192 let body_labels stmt = CminorFold.statement f_exp_labels f_body_labels stmt
 193
 194 let prog_labels p =
 195   let f lbls (_, f_def) = match f_def with
 196     | Cminor.F_int def ->
 197         labels_union lbls (body_labels def.Cminor.f_body)
 198     | _ -> lbls in
 199   List.fold_left f (CostLabel.Set.empty, Label.Set.empty) p.Cminor.functs
 200
 201 let cost_labels p = fst (prog_labels p)
 202 let user_labels p = snd (prog_labels p)
 203
 204 let all_labels p =
 205   let (cost_labels, user_labels) = prog_labels p in
 206   let all =
 207     CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls)
 208       cost_labels StringTools.Set.empty in
 209   Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all