src/clight/clightLabelling.ml

   1
   2 (** This module defines the labelling of a [Clight] program. *)
   3
   4 open Clight
   5 open CostLabel
   6
   7
   8 (* Add a cost label in front of a statement. *)
   9
  10 let add_starting_cost_label cost_universe stmt =
  11   Clight.Scost (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   Clight.Ssequence (stmt, add_starting_cost_label cost_universe Clight.Sskip)
  17
  18
  19 let int_type = Tint (I32, AST.Signed)
  20 let const_int i = Expr (Econst_int i, int_type)
  21
  22
  23 let typeof e = let Expr (_,t) = e in t
  24
  25
  26 let add_cost_label_e cost_universe e =
  27   Expr (Ecost (CostLabel.Gen.fresh cost_universe, e), typeof e)
  28
  29
  30 (* Add cost labels to an expression. *)
  31
  32 let rec add_cost_labels_e cost_universe = function
  33   | Expr (exp,cty) -> Expr (add_cost_labels_expr cost_universe exp,cty)
  34
  35 and add_cost_labels_expr cost_universe exp = match exp with
  36   | Econst_int _ | Econst_float _ | Evar _ | Esizeof _ -> exp
  37   | Ederef e -> Ederef (add_cost_labels_e cost_universe e)
  38   | Eaddrof e -> Eaddrof (add_cost_labels_e cost_universe e)
  39   | Eunop (op,e) -> Eunop (op,(add_cost_labels_e cost_universe e))
  40   | Ebinop (op,e1,e2) ->
  41       Ebinop (op,
  42               add_cost_labels_e cost_universe e1,
  43               add_cost_labels_e cost_universe e2)
  44   | Ecast (t,e) -> Ecast (t, add_cost_labels_e cost_universe e)
  45   | Eandbool (e1,e2) ->
  46       let e1' = add_cost_labels_e cost_universe e1 in
  47       let e2' = add_cost_labels_e cost_universe e2 in
  48       let b1 = add_cost_label_e cost_universe (const_int 1) in
  49       let b2 = add_cost_label_e cost_universe (const_int 0) in
  50       let e2' = Expr (Econdition (e2', b1, b2), int_type) in
  51       let e2' = add_cost_label_e cost_universe e2' in
  52       let e3' = add_cost_label_e cost_universe (const_int 0) in
  53       Econdition (e1', e2', e3')
  54   | Eorbool (e1,e2) ->
  55       let e1' = add_cost_labels_e cost_universe e1 in
  56       let e2' = add_cost_label_e cost_universe (const_int 1) in
  57       let e3' = add_cost_labels_e cost_universe e2 in
  58       let b1 = add_cost_label_e cost_universe (const_int 1) in
  59       let b2 = add_cost_label_e cost_universe (const_int 0) in
  60       let e3' = Expr (Econdition (e3', b1, b2), int_type) in
  61       let e3' = add_cost_label_e cost_universe e3' in
  62       Econdition (e1', e2', e3')
  63   | Efield (e,id) -> Efield (add_cost_labels_e cost_universe e,id)
  64   | Econdition (e1,e2,e3) ->
  65       let e1' = add_cost_labels_e cost_universe e1 in
  66       let e2' = add_cost_labels_e cost_universe e2 in
  67       let e2' = add_cost_label_e cost_universe e2' in
  68       let e3' = add_cost_labels_e cost_universe e3 in
  69       let e3' = add_cost_label_e cost_universe e3' in
  70       Econdition (e1', e2', e3')
  71   | Ecost (_,_) | Ecall _ -> assert false (* Should not happen *)
  72
  73 let add_cost_labels_opt cost_universe = function
  74   | None -> None
  75   | Some e -> Some (add_cost_labels_e cost_universe e)
  76
  77 let add_cost_labels_lst cost_universe l =
  78   List.map (add_cost_labels_e cost_universe) l
  79
  80
  81 (* Add cost labels to a statement. *)
  82
  83 let rec add_cost_labels_st cost_universe = function
  84   | Sskip -> Sskip
  85   | Sassign (e1,e2) ->
  86       Sassign (add_cost_labels_e cost_universe e1,
  87                add_cost_labels_e cost_universe e2)
  88   | Scall (e1,e2,lst) ->
  89       Scall (add_cost_labels_opt cost_universe e1,
  90              add_cost_labels_e cost_universe e2,
  91              add_cost_labels_lst cost_universe lst)
  92   | Ssequence (s1,s2) ->
  93       Ssequence (add_cost_labels_st cost_universe s1,
  94                  add_cost_labels_st cost_universe s2)
  95   | Sifthenelse (e,s1,s2) ->
  96       let s1' = add_cost_labels_st cost_universe s1 in
  97       let s1' = add_starting_cost_label cost_universe s1' in
  98       let s2' = add_cost_labels_st cost_universe s2 in
  99       let s2' = add_starting_cost_label cost_universe s2' in
 100       Sifthenelse (add_cost_labels_e cost_universe e, s1', s2')
 101   | Swhile (e,s) ->
 102       let s' = add_cost_labels_st cost_universe s in
 103       let s' = add_starting_cost_label cost_universe s' in
 104       add_ending_cost_label cost_universe
 105         (Swhile (add_cost_labels_e cost_universe e, s'))
 106   | Sdowhile (e,s) ->
 107       let s = add_cost_labels_st cost_universe s in
 108       let s' = add_starting_cost_label cost_universe s in
 109       add_ending_cost_label cost_universe
 110         (Sdowhile (add_cost_labels_e cost_universe e, s'))
 111   | Sfor (s1,e,s2,s3) ->
 112       let s1' = add_cost_labels_st cost_universe s1 in
 113       let s2' = add_cost_labels_st cost_universe s2 in
 114       let s3' = add_cost_labels_st cost_universe s3 in
 115       let s3' = add_starting_cost_label cost_universe s3' in
 116       add_ending_cost_label cost_universe
 117         (Sfor (s1', add_cost_labels_e cost_universe e, s2', s3'))
 118   | Sreturn e -> Sreturn (add_cost_labels_opt cost_universe e)
 119   | Sswitch (e,ls) ->
 120       Sswitch (add_cost_labels_e cost_universe e,
 121                add_cost_labels_ls cost_universe ls)
 122   | Slabel (lbl,s) ->
 123       let s' = add_cost_labels_st cost_universe s in
 124       let s' = add_starting_cost_label cost_universe s' in
 125       Slabel (lbl,s')
 126   | Scost (_,_) -> assert false
 127   | _ as stmt -> stmt
 128
 129 and add_cost_labels_ls cost_universe = function
 130   | LSdefault s ->
 131       let s' = add_cost_labels_st cost_universe s in
 132       let s' = add_starting_cost_label cost_universe s' in
 133       LSdefault s'
 134   | LScase (i,s,ls) ->
 135       let s' = add_cost_labels_st cost_universe s in
 136       let s' = add_starting_cost_label cost_universe s' in
 137       LScase (i, s', add_cost_labels_ls cost_universe ls)
 138
 139
 140 (* Add cost labels to a function. *)
 141
 142 let add_cost_labels_f cost_universe = function
 143   | (id,Internal fd) -> (id,Internal {
 144       fn_return = fd.fn_return ;
 145       fn_params = fd.fn_params ;
 146       fn_vars = fd.fn_vars ;
 147       fn_body = add_starting_cost_label cost_universe
 148                              (add_cost_labels_st cost_universe fd.fn_body)
 149     })
 150   | (id,External (a,b,c)) -> (id,External (a,b,c))
 151
 152
 153 (** [add_cost_labels prog] inserts some labels to enable
 154     cost annotation. *)
 155
 156 let add_cost_labels p =
 157   let labs = ClightAnnotator.all_labels p in
 158   let labs = StringTools.Set.fold CostLabel.Set.add labs CostLabel.Set.empty in
 159   let cost_prefix = CostLabel.Gen.fresh_prefix labs "__cost" in
 160   let cost_universe = CostLabel.Gen.new_universe cost_prefix in
 161   {
 162     prog_funct = List.map (add_cost_labels_f cost_universe) p.prog_funct;
 163     prog_main = p.prog_main;
 164     prog_vars = p.prog_vars
 165   }