Ignore:
Timestamp:
Oct 21, 2011, 2:02:41 PM (8 years ago)
Author:
tranquil
Message:
  • added infrastructure to add same-language transformations along the compilation chain from command line options
  • started work on cost expression semplification
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.ml

    r1357 r1433  
    128128let const_int i = Clight.Expr (Clight.Econst_int i, int_typ)
    129129
     130let expr_of_cost_cond var = function
     131  | CostExpr.Ceq k ->
     132    Clight.Expr(Clight.Ebinop(Clight.Oeq, var, const_int k),int_typ)
     133  | CostExpr.Cgeq k ->
     134    Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ)
     135  | CostExpr.Cmod (a, b) ->
     136    let modulus =
     137      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
     138    Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ)
     139  | CostExpr.Cgeqmod (k, a, b) ->
     140    let modulus =
     141      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
     142        let modulus_eq =
     143             Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ) in
     144        let greater =
     145            Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) in
     146    Clight.Expr(Clight.Eandbool(modulus_eq, greater),int_typ)
     147 
     148let rec expr_of_cost_expr prefix = function
     149    | CostExpr.Exact k -> const_int k
     150    | CostExpr.Ternary(index, cond, if_true, if_false) ->
     151    let id = CostLabel.make_id prefix index in
     152    let var = Clight.Expr(Clight.Evar id, int_typ) in
     153    let cond_e = expr_of_cost_cond var cond in
     154    let if_true_e = expr_of_cost_expr prefix if_true in
     155    let if_false_e = expr_of_cost_expr prefix if_false in
     156    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)   
     157
    130158(* Instrument an expression. *)
    131159
    132 let rec instrument_expr cost_mapping cost_incr e =
     160let rec instrument_expr l_ind cost_mapping cost_incr e =
    133161  let Clight.Expr (e, t) = e in
    134   match e with
    135     | Clight.Ecost (lbl, e) when CostLabel.Map.find lbl cost_mapping = 0 ->
    136         e
    137     | _ ->
    138         let e' = instrument_expr_descr cost_mapping cost_incr e in
     162        let e' = instrument_expr_descr l_ind cost_mapping cost_incr e in
    139163        Clight.Expr (e', t)
    140 and instrument_expr_descr cost_mapping cost_incr e = match e with
     164and instrument_expr_descr l_ind cost_mapping cost_incr e = match e with
    141165  | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
    142166  | Clight.Esizeof _ -> e
    143167  | Clight.Ederef e ->
    144       let e' = instrument_expr cost_mapping cost_incr e in
     168      let e' = instrument_expr l_ind cost_mapping cost_incr e in
    145169      Clight.Ederef e'
    146170  | Clight.Eaddrof e ->
    147       let e' = instrument_expr cost_mapping cost_incr e in
     171      let e' = instrument_expr l_ind cost_mapping cost_incr e in
    148172      Clight.Eaddrof e'
    149173  | Clight.Eunop (op, e) ->
    150       let e' = instrument_expr cost_mapping cost_incr e in
     174      let e' = instrument_expr l_ind cost_mapping cost_incr e in
    151175      Clight.Eunop (op, e')
    152176  | Clight.Ebinop (op, e1, e2) ->
    153       let e1' = instrument_expr cost_mapping cost_incr e1 in
    154       let e2' = instrument_expr cost_mapping cost_incr e2 in
     177      let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
     178      let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
    155179      Clight.Ebinop (op, e1', e2')
    156180  | Clight.Ecast (t, e) ->
    157       let e' = instrument_expr cost_mapping cost_incr e in
     181      let e' = instrument_expr l_ind cost_mapping cost_incr e in
    158182      Clight.Ecast (t, e')
    159183  | Clight.Econdition (e1, e2, e3) ->
    160       let e1' = instrument_expr cost_mapping cost_incr e1 in
    161       let e2' = instrument_expr cost_mapping cost_incr e2 in
    162       let e3' = instrument_expr cost_mapping cost_incr e3 in
     184      let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
     185      let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
     186      let e3' = instrument_expr l_ind cost_mapping cost_incr e3 in
    163187      Clight.Econdition (e1', e2', e3')
    164188  | Clight.Eandbool (e1, e2) ->
    165       let e1' = instrument_expr cost_mapping cost_incr e1 in
    166       let e2' = instrument_expr cost_mapping cost_incr e2 in
     189      let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
     190      let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
    167191      Clight.Eandbool (e1', e2')
    168192  | Clight.Eorbool (e1, e2) ->
    169       let e1' = instrument_expr cost_mapping cost_incr e1 in
    170       let e2' = instrument_expr cost_mapping cost_incr e2 in
     193      let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
     194      let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
    171195      Clight.Eorbool (e1', e2')
    172196  | Clight.Efield (e, x) ->
    173       let e' = instrument_expr cost_mapping cost_incr e in
     197      let e' = instrument_expr l_ind cost_mapping cost_incr e in
    174198      Clight.Efield (e', x)
    175   | Clight.Ecost (lbl, e) when CostLabel.Map.mem lbl cost_mapping ->
    176       let e' = instrument_expr cost_mapping cost_incr e in
    177       let incr = CostLabel.Map.find lbl cost_mapping in
    178       if incr = 0 then let Clight.Expr (e'', _) = e' in e''
    179       else Clight.Ecall (cost_incr, const_int incr, e')
    180   | Clight.Ecost (_, e) ->
    181     let Clight.Expr (e', _) = instrument_expr cost_mapping cost_incr e in
    182     e'
     199  | Clight.Ecost (lbl, e) ->
     200      let e' = instrument_expr l_ind cost_mapping cost_incr e in
     201            let atom = lbl.CostLabel.name in
     202            let cost =
     203                try
     204                    CostLabel.Atom.Map.find atom cost_mapping
     205                with (* if atom is not present, then map to 0 *)
     206                    | Not_found -> CostExpr.Exact 0 in
     207      if cost = CostExpr.Exact 0 then let Clight.Expr (e'', _) = e' in e''
     208      else let cost = expr_of_cost_expr l_ind cost in
     209                  Clight.Ecall (cost_incr, cost, e')
    183210  | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *)
    184211
     
    186213        | None -> body
    187214        | Some d ->
    188                 let uint = Clight.Tint(Clight.I32, AST.Unsigned) in
    189                 let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), uint) in
    190                 let one = Clight.Expr(Clight.Econst_int 1, uint) in
    191                 let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), uint) in
    192                 Clight.Ssequence(body, Clight.Sassign(id, add id one))
     215                let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
     216                let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), int_typ) in
     217                Clight.Ssequence(body, Clight.Sassign(id, add id (const_int 1)))
    193218               
    194219let loop_reset_index prefix depth loop = match depth with
    195220        | None -> loop
    196221        | Some d ->
    197     let uint = Clight.Tint(Clight.I32, AST.Unsigned) in
    198     let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), uint) in
    199     let zero = Clight.Expr(Clight.Econst_int 0, uint) in
    200     Clight.Ssequence(Clight.Sassign(id, zero), loop)
     222    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
     223    Clight.Ssequence(Clight.Sassign(id, const_int 0), loop)
     224
    201225
    202226(* Instrument a statement. *)
     
    207231    stmt
    208232  | Clight.Sassign (e1, e2) ->
    209     let e1' = instrument_expr cost_mapping cost_incr e1 in
    210     let e2' = instrument_expr cost_mapping cost_incr e2 in
     233    let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
     234    let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
    211235    Clight.Sassign (e1', e2')
    212236  | Clight.Scall (eopt, f, args) ->
    213237    let eopt' = match eopt with
    214238      | None -> None
    215       | Some e -> Some (instrument_expr cost_mapping cost_incr e) in
    216     let f' = instrument_expr cost_mapping cost_incr f in
    217     let args' = List.map (instrument_expr cost_mapping cost_incr) args in
     239      | Some e -> Some (instrument_expr l_ind cost_mapping cost_incr e) in
     240    let f' = instrument_expr l_ind cost_mapping cost_incr f in
     241    let args' = List.map (instrument_expr l_ind cost_mapping cost_incr) args in
    218242    Clight.Scall (eopt', f', args')
    219243  | Clight.Ssequence (s1, s2) ->
     
    221245                      instrument_body l_ind cost_mapping cost_incr s2)
    222246  | Clight.Sifthenelse (e, s1, s2) ->
    223     let e' = instrument_expr cost_mapping cost_incr e in
     247    let e' = instrument_expr l_ind cost_mapping cost_incr e in
    224248    let s1' = instrument_body l_ind cost_mapping cost_incr s1 in
    225249    let s2' = instrument_body l_ind cost_mapping cost_incr s2 in
    226250    Clight.Sifthenelse (e', s1', s2')
    227251  | Clight.Swhile (i, e, s) ->
    228     let e' = instrument_expr cost_mapping cost_incr e in
     252    let e' = instrument_expr l_ind cost_mapping cost_incr e in
    229253    let s' = instrument_body l_ind cost_mapping cost_incr s in
    230254                let s' = loop_increment l_ind i s' in
    231255    loop_reset_index l_ind i (Clight.Swhile (None, e', s'))
    232256  | Clight.Sdowhile (i, e, s) ->
    233     let e' = instrument_expr cost_mapping cost_incr e in
     257    let e' = instrument_expr l_ind cost_mapping cost_incr e in
    234258    let s' = instrument_body l_ind cost_mapping cost_incr s in
    235259    let s' = loop_increment l_ind i s' in
     
    237261  | Clight.Sfor (i, s1, e, s2, s3) ->
    238262    let s1' = instrument_body l_ind cost_mapping cost_incr s1 in
    239     let e' = instrument_expr cost_mapping cost_incr e in
     263    let e' = instrument_expr l_ind cost_mapping cost_incr e in
    240264    let s2' = instrument_body l_ind cost_mapping cost_incr s2 in
    241265    let s3' = instrument_body l_ind cost_mapping cost_incr s3 in
     
    243267                loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3'))
    244268  | Clight.Sreturn (Some e) ->
    245     let e' = instrument_expr cost_mapping cost_incr e in
     269    let e' = instrument_expr l_ind cost_mapping cost_incr e in
    246270    Clight.Sreturn (Some e')
    247271  | Clight.Sswitch (e, ls) ->
    248     let e' = instrument_expr cost_mapping cost_incr e in
     272    let e' = instrument_expr l_ind cost_mapping cost_incr e in
    249273    let ls' = instrument_ls l_ind cost_mapping cost_incr ls in
    250274    Clight.Sswitch (e', ls')
     
    252276    let s' = instrument_body l_ind cost_mapping cost_incr s in
    253277    Clight.Slabel (lbl, s')
    254   | Clight.Scost (lbl, s) when CostLabel.Map.mem lbl cost_mapping ->
     278  | Clight.Scost (lbl, s) ->
    255279    (* Keep the cost label in the code. *)
    256280    let s' = instrument_body l_ind cost_mapping cost_incr s in
    257     let incr = CostLabel.Map.find lbl cost_mapping in
     281                let atom = lbl.CostLabel.name in
     282                let cost =
     283                        try
     284                                CostLabel.Atom.Map.find atom cost_mapping
     285                        with (* if atom is not present, then map to 0 *)
     286                                | Not_found -> CostExpr.Exact 0 in
     287                let cost = expr_of_cost_expr l_ind cost in
    258288    let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
    259289    let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
    260     let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
    261     Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
     290    Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, [cost]), s'))
    262291  (*
    263292    let s' = instrument_body l_ind cost_mapping cost_incr s in
     
    270299    Clight.Ssequence (Clight.Scall (None, f, args), s')
    271300  *)
    272   | Clight.Scost (lbl, s) ->
    273     (* Keep the cost label in the code and show the increment of 0. *)
    274     let s' = instrument_body l_ind cost_mapping cost_incr s in
    275     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
    276     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
    277     let args = [Clight.Expr (Clight.Econst_int 0, int_typ)] in
    278     Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
    279301  (*
    280302    instrument_body l_ind cost_mapping cost_incr s
     
    292314        if max_depth = 0 then [] else
    293315        let max_depth = max_depth - 1 in
    294   let uint = Clight.Tint(Clight.I32, AST.Unsigned) in
    295316        let id = CostLabel.make_id prefix max_depth in
    296         (id, uint) :: loop_indexes_defs prefix max_depth
     317        (id, int_typ) :: loop_indexes_defs prefix max_depth
    297318
    298319let max_depth =
     
    349370  flush cout ;
    350371  close_out cout
    351 
     372       
     373       
    352374(** [instrument prog cost_map] instruments the program [prog]. First a fresh
    353375    global variable --- the so-called cost variable --- is added to the program.
     
    372394      cost_incr_prefix in
    373395  let cost_incr_def = cost_incr_def cost_id cost_incr in
     396
     397  (* Turn the mapping from indexed cost labels to integers into one from *)
     398        (* cost atoms to cost expresisons *)
     399        let cost_mapping = CostExpr.cost_expr_mapping_of_cost_mapping cost_mapping in
    374400
    375401  (* Instrument each function *)
Note: See TracChangeset for help on using the changeset viewer.