Changeset 1507 for Deliverables/D2.2


Ignore:
Timestamp:
Nov 15, 2011, 5:11:19 PM (8 years ago)
Author:
tranquil
Message:
  • added an option to not use ternary expressions in costs, to accomodate frama-c explosion of such expressions
  • corrected some typos in comments
  • added a check for well behaved for loops in loop unrolling, but intelligent unrolling is not done yet
  • TODO: peeling and unrolling can contradict preciseness (with difference between introduced branches around 2 cycles). I guess it can be corrected easily
Location:
Deliverables/D2.2/8051-indexed-labels-branch/src
Files:
12 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/constPropagation.mli

    r1477 r1507  
    1 (** Transofmration that performs a single pass of copy propagation. Does not
    2     use equivalence classes, so it can miss some copies. *)
     1(** Transformation that performs a single pass of constant propagation.
     2    A pass of dead code elimination is also performed. *)
    33
    44val trans : Languages.transformation
  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/copyPropagation.mli

    r1477 r1507  
    1 (** Transofmration that performs a single pass of copy propagation *)
     1(** Transformation that performs a pass of copy propagation with a very
     2    rough analysis. *)
    23
    34val trans : Languages.transformation
  • Deliverables/D2.2/8051-indexed-labels-branch/src/acc.ml

    r1433 r1507  
    4646    begin
    4747      let (annotated_input_ast, cost_id, cost_incr) =
    48         Languages.annotate input_ast final_ast in (
     48        let cost_tern = Options.is_cost_ternary_enabled () in
     49        Languages.annotate cost_tern input_ast final_ast in (
    4950          save ~suffix:"-annotated" annotated_input_ast;
    5051          Languages.save_cost output_filename cost_id cost_incr);
     
    6162      let label_traces = List.map (Languages.interpret debug) asts in
    6263      Printf.eprintf "Checking execution traces...%!";
    63                         if Options.trace_requested () then
    64                                 let print_l l =
    65                                         Printf.printf "%s, " (CostLabel.string_of_cost_label
    66                                                                ~pretty:true l) in
    67                           let print_ls ls = List.iter print_l ls in
    68                                 let print_trace (v, ls) =
    69                                         Printf.printf "%s | " (Big_int.string_of_big_int v);
    70                                         print_ls ls;
    71                                         Printf.printf "\n" in
    72                                 List.iter print_trace label_traces
    73                         else ();
     64      if Options.trace_requested () then
     65        let print_l l =
     66          Printf.printf "%s, " (CostLabel.string_of_cost_label
     67                                  ~pretty:true l) in
     68        let print_ls ls = List.iter print_l ls in
     69        let print_trace (v, ls) =
     70          Printf.printf "%s | " (Big_int.string_of_big_int v);
     71          print_ls ls;
     72          Printf.printf "\n" in
     73        List.iter print_trace label_traces
     74      else ();
    7475      Checker.same_traces (List.combine asts label_traces);
    7576      Printf.eprintf "OK.\n%!";
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.ml

    r1433 r1507  
    2727
    2828let empty_triple =
    29         (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty)
     29  (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty)
    3030
    3131let name_singleton id =
     
    7272  let def_idents = function
    7373    | Clight.Internal def ->
    74         let vars =
    75           string_set_of_list
    76             (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
    77         let (names, cost_labels, user_labels) =
    78           body_idents def.Clight.fn_body in
    79         (StringTools.Set.union vars names, cost_labels, user_labels)
     74      let vars =
     75        string_set_of_list
     76          (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
     77      let (names, cost_labels, user_labels) =
     78        body_idents def.Clight.fn_body in
     79      (StringTools.Set.union vars names, cost_labels, user_labels)
    8080    | Clight.External (id, _, _) ->
    81         (StringTools.Set.singleton id, CostLabel.Set.empty,
    82         Label.Set.empty) in
     81      (StringTools.Set.singleton id, CostLabel.Set.empty,
     82      Label.Set.empty) in
    8383  let fun_idents (id, f_def) =
    8484    let (names, cost_labels, user_labels) = def_idents f_def in
     
    9696let all_labels p =
    9797  let (_, cost_labels, user_labels) = prog_idents p in
    98         let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
     98  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
    9999  let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
    100100  Label.Set.fold StringTools.Set.add user_labels all
     
    102102let all_idents p =
    103103  let (names, cost_labels, user_labels) = prog_idents p in
    104         let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
     104  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
    105105  let cost_labels = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
    106106  let to_string_set fold set =
     
    140140    let modulus =
    141141      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
     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
    146146    Clight.Expr(Clight.Eandbool(modulus_eq, greater),int_typ)
    147  
     147
     148let rec expr_of_cost_gen_cond var gc =
     149  assert (not (CostExpr.CondSet.is_empty gc));
     150  let c = CostExpr.CondSet.min_elt gc in
     151  let c_expr = expr_of_cost_cond var c in
     152  let rest = CostExpr.CondSet.remove c gc in
     153  if CostExpr.CondSet.is_empty rest then c_expr else
     154    let rest_expr = expr_of_cost_gen_cond var rest in
     155    Clight.Expr(Clight.Eandbool(c_expr, rest_expr), int_typ)
     156
    148157let rec expr_of_cost_expr prefix = function
    149     | CostExpr.Exact k -> const_int k
    150     | CostExpr.Ternary(index, cond, if_true, if_false) ->
     158  | CostExpr.Exact k -> const_int k
     159  | CostExpr.Ternary(index, cond, if_true, if_false) ->
    151160    let id = CostLabel.make_id prefix index in
    152161    let var = Clight.Expr(Clight.Evar id, int_typ) in
    153     let cond_e = expr_of_cost_cond var cond in
     162    let cond_e = expr_of_cost_gen_cond var cond in
    154163    let if_true_e = expr_of_cost_expr prefix if_true in
    155164    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)   
     165    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
     166
     167(* as long as Clight parser will be called at the end, this hack works *)
     168(* this will be called in case -no-cost-tern is active. *)
     169let rec side_effect_expr_of_cost_expr prefix cost_incr cont e_type = function
     170  | CostExpr.Exact k ->
     171    Clight.Expr(Clight.Ecall (cost_incr, const_int k, cont), e_type)
     172  | CostExpr.Ternary(index, cond, if_true, if_false) ->
     173    let id = CostLabel.make_id prefix index in
     174    let var = Clight.Expr(Clight.Evar id, int_typ) in
     175    let cond_e = expr_of_cost_gen_cond var cond in
     176    let rec_call = side_effect_expr_of_cost_expr prefix cost_incr cont e_type in
     177    let if_true_e = rec_call if_true in
     178    let if_false_e = rec_call if_false in
     179    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
     180
     181let rec stmt_of_cost_expr prefix cost_incr = function
     182  | CostExpr.Exact k -> Clight.Scall (None, cost_incr, [const_int k])
     183  | CostExpr.Ternary(index, cond, if_true, if_false) ->
     184    let id = CostLabel.make_id prefix index in
     185    let var = Clight.Expr(Clight.Evar id, int_typ) in
     186    let cond_e = expr_of_cost_gen_cond var cond in
     187    let if_true_s = stmt_of_cost_expr prefix cost_incr if_true in
     188    let if_false_s = stmt_of_cost_expr prefix cost_incr if_false in
     189    Clight.Sifthenelse (cond_e, if_true_s, if_false_s)
    157190
    158191(* Instrument an expression. *)
    159192
    160 let rec instrument_expr l_ind cost_mapping cost_incr e =
    161   let Clight.Expr (e, t) = e in
    162         let e' = instrument_expr_descr l_ind cost_mapping cost_incr e in
    163         Clight.Expr (e', t)
    164 and instrument_expr_descr l_ind cost_mapping cost_incr e = match e with
    165   | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
    166   | Clight.Esizeof _ -> e
    167   | Clight.Ederef e ->
    168       let e' = instrument_expr l_ind cost_mapping cost_incr e in
    169       Clight.Ederef e'
    170   | Clight.Eaddrof e ->
    171       let e' = instrument_expr l_ind cost_mapping cost_incr e in
    172       Clight.Eaddrof e'
    173   | Clight.Eunop (op, e) ->
    174       let e' = instrument_expr l_ind cost_mapping cost_incr e in
    175       Clight.Eunop (op, e')
    176   | Clight.Ebinop (op, e1, e2) ->
    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
    179       Clight.Ebinop (op, e1', e2')
    180   | Clight.Ecast (t, e) ->
    181       let e' = instrument_expr l_ind cost_mapping cost_incr e in
    182       Clight.Ecast (t, e')
    183   | Clight.Econdition (e1, e2, e3) ->
    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
    187       Clight.Econdition (e1', e2', e3')
    188   | Clight.Eandbool (e1, e2) ->
    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
    191       Clight.Eandbool (e1', e2')
    192   | Clight.Eorbool (e1, e2) ->
    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
    195       Clight.Eorbool (e1', e2')
    196   | Clight.Efield (e, x) ->
    197       let e' = instrument_expr l_ind cost_mapping cost_incr e in
    198       Clight.Efield (e', x)
    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')
    210   | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *)
     193(* FIXME: follow cost_tern option *)
     194let instrument_expr cost_tern l_ind cost_mapping cost_incr =
     195  let f_expr (Clight.Expr(ed, et) as e) sub_res = match ed, sub_res with
     196  | Clight.Ecost (lbl, _), e' :: _ ->
     197    let atom = lbl.CostLabel.name in
     198    let cost =
     199      try
     200        CostLabel.Atom.Map.find atom cost_mapping
     201      with (* if atom is not present, then map to 0 *)
     202        | Not_found -> CostExpr.Exact 0 in
     203    if cost = CostExpr.Exact 0 then e' else
     204      if cost_tern then
     205        let cost = expr_of_cost_expr l_ind cost in
     206        Clight.Expr(Clight.Ecall (cost_incr, cost, e'), et)
     207      else
     208        side_effect_expr_of_cost_expr l_ind cost_incr e' et cost
     209  | Clight.Ecall (_, _, _), _ -> assert false (* Should not happen. *)
     210  | _ -> ClightFold.expr_fill_exprs e sub_res in
     211  ClightFold.expr2 f_expr
    211212
    212213let loop_increment prefix depth body = match depth  with
    213         | None -> body
    214         | Some d ->
    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)))
    218                
     214  | None -> body
     215  | Some d ->
     216    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
     217    let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), int_typ) in
     218    Clight.Ssequence(body, Clight.Sassign(id, add id (const_int 1)))
     219     
    219220let loop_reset_index prefix depth loop = match depth with
    220         | None -> loop
    221         | Some d ->
     221  | None -> loop
     222  | Some d ->
    222223    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
    223224    Clight.Ssequence(Clight.Sassign(id, const_int 0), loop)
     
    226227(* Instrument a statement. *)
    227228
    228 let rec instrument_body l_ind cost_mapping cost_incr stmt = match stmt with
    229   | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
    230   | Clight.Sgoto _ ->
    231     stmt
    232   | Clight.Sassign (e1, e2) ->
    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
    235     Clight.Sassign (e1', e2')
    236   | Clight.Scall (eopt, f, args) ->
    237     let eopt' = match eopt with
    238       | None -> None
    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
    242     Clight.Scall (eopt', f', args')
    243   | Clight.Ssequence (s1, s2) ->
    244     Clight.Ssequence (instrument_body l_ind cost_mapping cost_incr s1,
    245                       instrument_body l_ind cost_mapping cost_incr s2)
    246   | Clight.Sifthenelse (e, s1, s2) ->
    247     let e' = instrument_expr l_ind cost_mapping cost_incr e in
    248     let s1' = instrument_body l_ind cost_mapping cost_incr s1 in
    249     let s2' = instrument_body l_ind cost_mapping cost_incr s2 in
    250     Clight.Sifthenelse (e', s1', s2')
    251   | Clight.Swhile (i, e, s) ->
    252     let e' = instrument_expr l_ind cost_mapping cost_incr e in
    253     let s' = instrument_body l_ind cost_mapping cost_incr s in
    254                 let s' = loop_increment l_ind i s' in
    255     loop_reset_index l_ind i (Clight.Swhile (None, e', s'))
    256   | Clight.Sdowhile (i, e, s) ->
    257     let e' = instrument_expr l_ind cost_mapping cost_incr e in
    258     let s' = instrument_body l_ind cost_mapping cost_incr s in
    259     let s' = loop_increment l_ind i s' in
    260     loop_reset_index l_ind i (Clight.Sdowhile (None, e', s'))
    261   | Clight.Sfor (i, s1, e, s2, s3) ->
    262     let s1' = instrument_body l_ind cost_mapping cost_incr s1 in
    263     let e' = instrument_expr l_ind cost_mapping cost_incr e in
    264     let s2' = instrument_body l_ind cost_mapping cost_incr s2 in
    265     let s3' = instrument_body l_ind cost_mapping cost_incr s3 in
    266     let s3' = loop_increment l_ind i s3' in
    267                 loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3'))
    268   | Clight.Sreturn (Some e) ->
    269     let e' = instrument_expr l_ind cost_mapping cost_incr e in
    270     Clight.Sreturn (Some e')
    271   | Clight.Sswitch (e, ls) ->
    272     let e' = instrument_expr l_ind cost_mapping cost_incr e in
    273     let ls' = instrument_ls l_ind cost_mapping cost_incr ls in
    274     Clight.Sswitch (e', ls')
    275   | Clight.Slabel (lbl, s) ->
    276     let s' = instrument_body l_ind cost_mapping cost_incr s in
    277     Clight.Slabel (lbl, s')
    278   | Clight.Scost (lbl, s) ->
     229(* not using ClightFold as l_ind changes through loops *)
     230let rec instrument_body cost_tern l_ind cost_mapping cost_incr stmt =
     231  let instr_expr = instrument_expr cost_tern l_ind cost_mapping cost_incr in
     232  let instr_body = instrument_body cost_tern l_ind cost_mapping cost_incr in
     233  match stmt with
     234    | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
     235    | Clight.Sgoto _ ->
     236      stmt
     237    | Clight.Sassign (e1, e2) ->
     238      let e1' = instr_expr e1 in
     239      let e2' = instr_expr e2 in
     240      Clight.Sassign (e1', e2')
     241    | Clight.Scall (eopt, f, args) ->
     242      let eopt' = Option.map instr_expr eopt in
     243      let f' = instr_expr f in
     244      let args = List.map (instr_expr) args in
     245      Clight.Scall (eopt', f', args)
     246    | Clight.Ssequence (s1, s2) ->
     247      Clight.Ssequence (
     248        instr_body s1,
     249        instr_body s2)
     250    | Clight.Sifthenelse (e, s1, s2) ->
     251      let e' = instr_expr e in
     252      let s1' = instr_body s1 in
     253      let s2' = instr_body s2 in
     254      Clight.Sifthenelse (e', s1', s2')
     255    | Clight.Swhile (i, e, s) ->
     256      let e' = instr_expr e in
     257      let s' = instr_body s in
     258      let s' = loop_increment l_ind i s' in
     259      loop_reset_index l_ind i (Clight.Swhile (None, e', s'))
     260    | Clight.Sdowhile (i, e, s) ->
     261      let e' = instr_expr e in
     262      let s' = instr_body s in
     263      let s' = loop_increment l_ind i s' in
     264      loop_reset_index l_ind i (Clight.Sdowhile (None, e', s'))
     265    | Clight.Sfor (i, s1, e, s2, s3) ->
     266      let s1' = instr_body s1 in
     267      let e' = instr_expr e in
     268      let s2' = instr_body s2 in
     269      let s3' = instr_body s3 in
     270      let s3' = loop_increment l_ind i s3' in
     271      loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3'))
     272    | Clight.Sreturn (Some e) ->
     273      let e' = instr_expr e in
     274      Clight.Sreturn (Some e')
     275    | Clight.Sswitch (e, ls) ->
     276      let e' = instr_expr e in
     277      let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
     278      Clight.Sswitch (e', ls')
     279    | Clight.Slabel (lbl, s) ->
     280      let s' = instr_body s in
     281      Clight.Slabel (lbl, s')
     282    | Clight.Scost (lbl, s) ->
    279283    (* Keep the cost label in the code. *)
    280     let s' = instrument_body l_ind cost_mapping cost_incr s 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
    288     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
    289     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
    290     Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, [cost]), s'))
    291   (*
    292     let s' = instrument_body l_ind cost_mapping cost_incr s in
    293     let incr = CostLabel.Map.find lbl cost_mapping in
    294     if incr = 0 then s'
    295     else
    296     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
    297     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
    298     let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
    299     Clight.Ssequence (Clight.Scall (None, f, args), s')
    300   *)
    301   (*
    302     instrument_body l_ind cost_mapping cost_incr s
    303   *)
    304 and instrument_ls l_ind cost_mapping cost_incr = function
     284      let s' = instr_body s in
     285      let atom = lbl.CostLabel.name in
     286      let cost =
     287        try
     288          CostLabel.Atom.Map.find atom cost_mapping
     289        with (* if atom is not present, then map to 0 *)
     290          | Not_found -> CostExpr.Exact 0 in
     291      let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
     292      let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
     293      let cost_stmt =
     294        if not cost_tern then stmt_of_cost_expr l_ind f cost else
     295        let cost = expr_of_cost_expr l_ind cost in
     296        Clight.Scall(None, f, [cost]) in
     297      Clight.Scost (lbl, Clight.Ssequence (cost_stmt, s'))
     298(*
     299  let s' = instrument_body l_ind cost_mapping cost_incr s in
     300  let incr = CostLabel.Map.find lbl cost_mapping in
     301  if incr = 0 then s'
     302  else
     303  let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
     304  let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
     305  let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
     306  Clight.Ssequence (Clight.Scall (None, f, args), s')
     307*)
     308(*
     309  instrument_body l_ind cost_mapping cost_incr s
     310*)
     311and instrument_ls cost_tern l_ind cost_mapping cost_incr = function
    305312  | Clight.LSdefault s ->
    306     let s' = instrument_body l_ind cost_mapping cost_incr s in
     313    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
    307314    Clight.LSdefault s'
    308315  | Clight.LScase (i, s, ls) ->
    309     let s' = instrument_body l_ind cost_mapping cost_incr s in
    310     let ls' = instrument_ls l_ind cost_mapping cost_incr ls in
     316    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
     317    let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
    311318    Clight.LScase (i, s', ls')
    312                
     319     
    313320let rec loop_indexes_defs prefix max_depth =
    314         if max_depth = 0 then [] else
    315         let max_depth = max_depth - 1 in
    316         let id = CostLabel.make_id prefix max_depth in
    317         (id, int_typ) :: loop_indexes_defs prefix max_depth
     321  if max_depth = 0 then [] else
     322    let max_depth = max_depth - 1 in
     323    let id = CostLabel.make_id prefix max_depth in
     324    (id, int_typ) :: loop_indexes_defs prefix max_depth
    318325
    319326let max_depth =
    320         let f_expr _ _ = () in
    321         let f_stmt stmt _ res_stmts =
    322                 let curr_max = List.fold_left max 0 res_stmts in
    323                 if curr_max > 0 then curr_max else     
    324                 match stmt with
    325                 | Clight.Swhile(Some x,_,_) | Clight.Sdowhile(Some x,_,_)
    326                 | Clight.Sfor(Some x,_,_,_,_) -> x + 1
    327                 | _ -> 0 in
    328         ClightFold.statement2 f_expr f_stmt
     327  let f_expr _ _ = () in
     328  let f_stmt stmt _ res_stmts =
     329    let curr_max = List.fold_left max 0 res_stmts in
     330    if curr_max > 0 then curr_max else 
     331      match stmt with
     332        | Clight.Swhile(Some x,_,_) | Clight.Sdowhile(Some x,_,_)
     333        | Clight.Sfor(Some x,_,_,_,_) -> x + 1
     334        | _ -> 0 in
     335  ClightFold.statement2 f_expr f_stmt
    329336
    330337(* Instrument a function. *)
    331338
    332 let instrument_funct l_ind cost_mapping cost_incr (id, def) =
     339let instrument_funct cost_tern  l_ind cost_mapping cost_incr (id, def) =
    333340  let def = match def with
    334341    | Clight.Internal def ->
    335         let max_depth = max_depth def.Clight.fn_body in
    336         let vars = loop_indexes_defs l_ind max_depth in
    337         let vars = List.rev_append vars def.Clight.fn_vars in
    338         let body = instrument_body l_ind cost_mapping cost_incr def.Clight.fn_body in
    339         Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars}
     342      let max_depth = max_depth def.Clight.fn_body in
     343      let vars = loop_indexes_defs l_ind max_depth in
     344      let vars = List.rev_append vars def.Clight.fn_vars in
     345      let body = def.Clight.fn_body in
     346      let body =
     347        instrument_body cost_tern l_ind cost_mapping cost_incr body in
     348      Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars}
    340349    | Clight.External _ -> def
    341350  in
     
    370379  flush cout ;
    371380  close_out cout
    372        
    373        
     381   
     382   
    374383(** [instrument prog cost_map] instruments the program [prog]. First a fresh
    375384    global variable --- the so-called cost variable --- is added to the program.
     
    378387    name of the cost variable and the name of the cost increment function. *)
    379388
    380 let instrument p cost_mapping =
     389let instrument cost_tern p cost_mapping =
    381390
    382391  (* Create a fresh 'cost' variable. *)
     
    384393  let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
    385394  let cost_decl = cost_decl cost_id in
    386        
    387         (* Create a fresh loop index prefix *)
    388         let names = StringTools.Set.add cost_id names in
     395
     396  (* Create a fresh loop index prefix *)
     397  let names = StringTools.Set.add cost_id names in
    389398  let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in
    390399
     
    396405
    397406  (* 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
     407  (* cost atoms to cost expresisons *)
     408  let cost_mapping = CostExpr.cost_expr_mapping_of_cost_mapping cost_mapping in
    400409
    401410  (* Instrument each function *)
    402411  let prog_funct = p.Clight.prog_funct in
    403         let prog_funct =
    404     List.map (instrument_funct l_ind cost_mapping cost_incr) prog_funct in
     412  let prog_funct =
     413    let f = instrument_funct cost_tern l_ind cost_mapping cost_incr in
     414    List.map f prog_funct in
    405415
    406416  (* Glue all this together. *)
     
    416426  let tmp_file = Filename.temp_file "clight_instrument" ".c" in
    417427  save_tmp tmp_file (ClightPrinter.print_program p') ;
    418   let res = ClightParser.process tmp_file in
     428  let p' = ClightParser.process tmp_file in
    419429  Misc.SysExt.safe_remove tmp_file ;
    420   (res, cost_id, cost_incr)
     430  (p', cost_id, cost_incr)
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.mli

    r1291 r1507  
    22(** This module defines the instrumentation of a [Clight] program. *)
    33
    4 (** [instrument prog cost_map] instruments the program [prog]. First a fresh
    5     global variable --- the so-called cost variable --- is added to the program.
    6     Then, each cost label in the program is replaced by an increment of the cost
    7     variable, following the mapping [cost_map]. The function also returns the
    8     name of the cost variable and the name of the cost increment function.
    9                
     4(** [instrument cost_tern prog cost_map] instruments the program [prog]. First a
     5    fresh global variable --- the so-called cost variable --- is added to the
     6    program. Then, each cost label in the program is replaced by an increment of
     7    the cost variable, following the mapping [cost_map]. The function also
     8    returns the name of the cost variable and the name of the cost increment
     9    function. [cost_tern] rules whether cost increments are given by ternary
     10    expressions (more readable) or by branch statements (for frama-c
     11    itegration).
     12
    1013    TODO: int to expressions *)
    11 val instrument : Clight.program -> int CostLabel.Map.t ->
     14val instrument : bool -> Clight.program -> int CostLabel.Map.t ->
    1215                 Clight.program * string * string
    1316
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/loopUnrolling.ml

    r1483 r1507  
    88
    99let big_union : IdentSet.t list -> IdentSet.t =
    10         List.fold_left IdentSet.union IdentSet.empty
     10  List.fold_left IdentSet.union IdentSet.empty
    1111
    1212let referenced : statement -> IdentSet.t =
    1313  let f_expr e res_list =
    14                 let res = big_union res_list in
     14    let res = big_union res_list in
    1515    let Expr(ed, _) = e in
    1616    match ed with
    17         | Eaddrof (Expr(Evar x, _)) -> IdentSet.add x res
    18         | _ -> res in
     17      | Eaddrof (Expr(Evar x, _)) -> IdentSet.add x res
     18      | _ -> res in
    1919  let f_stmt stmt eres sres =
    20                 IdentSet.union (big_union eres) (big_union sres) in
     20    IdentSet.union (big_union eres) (big_union sres) in
    2121  ClightFold.statement2 f_expr f_stmt
    2222
    2323let mk_heuristic_global_info (max_factor : int) (p : program)
    2424    : heuristic_global_info =
    25         let f set ((id, _), _) = IdentSet.add id set in
    26         (max_factor, List.fold_left f IdentSet.empty p.prog_vars)
     25  let f set ((id, _), _) = IdentSet.add id set in
     26  (max_factor, List.fold_left f IdentSet.empty p.prog_vars)
    2727
    2828let mk_heuristic_local_info (f : cfunction) =   referenced f.fn_body
    2929
    3030let vars_of_expr, vars_of_stmt =
    31         let f_expr e res_list =
    32                 let res = big_union res_list in
     31  let f_expr e res_list =
     32    let res = big_union res_list in
    3333    let Expr(ed, _) = e in
    3434    match ed with
    35             | Evar x -> IdentSet.add x res
    36             | _ -> res in
     35      | Evar x -> IdentSet.add x res
     36      | _ -> res in
    3737  let f_stmt stmt eres sres =
    3838    IdentSet.union (big_union eres) (big_union sres) in
     
    4040
    4141let changed_in =
    42         let f_expr e _ = () in
     42  let f_expr e _ = () in
    4343  let f_stmt stmt _ sres =
    44                 let res = big_union sres in
    45                 match stmt with
    46                         | Sassign (Expr(Evar x, _), _) 
    47                         | Clight.Scall (Some (Expr(Evar x, _)), _, _) ->
    48                                 (* a situation like "*&x = ... " is avoided as dereferenced variables*)
    49                                 (* will be excluded a priori *)
    50                                 IdentSet.add x res
    51                         | _ -> res in
    52         ClightFold.statement2 f_expr f_stmt
     44    let res = big_union sres in
     45    match stmt with
     46      | Sassign (Expr(Evar x, _), _)
     47      | Clight.Scall (Some (Expr(Evar x, _)), _, _) ->
     48        (* a situation like "*&x = ... " is avoided as dereferenced variables*)
     49        (* will be excluded a priori *)
     50        IdentSet.add x res
     51      | _ -> res in
     52  ClightFold.statement2 f_expr f_stmt
     53
     54type sign =
     55  | Plus
     56  | Minus
     57
     58let find_increment = function
     59  | Sassign(
     60    Expr(Evar x,_),
     61    Expr(
     62      (Ebinop(Oadd,Expr(Evar y,_),inc) |
     63          Ebinop(Oadd,inc,Expr(Evar y,_)) ),_))
     64      when x = y -> Some (x, Plus, inc)
     65  | Sassign(
     66    Expr(Evar x,_),
     67    Expr(
     68      (Ebinop(Osub,Expr(Evar y,_),inc) |
     69          Ebinop(Osub,inc,Expr(Evar y,_)) ),_))
     70      when x = y -> Some (x, Minus, inc)
     71  | _ -> None
     72
     73let find_bound s x (Expr(ed, _)) = match s, ed with
     74  | Plus, Ebinop(Olt,Expr(Evar y,_),b)
     75  | Plus, Ebinop(Ogt,b,Expr(Evar y,_))
     76  | Minus, Ebinop(Olt,b,Expr(Evar y,_))
     77  | Minus, Ebinop(Ogt,Expr(Evar y,_),b)
     78    when y = x -> Some (false, b)
     79  | Plus, Ebinop(Ole,Expr(Evar y,_),b)
     80  | Plus, Ebinop(Oge,b,Expr(Evar y,_))
     81  | Minus, Ebinop(Ole,b,Expr(Evar y,_))
     82  | Minus, Ebinop(Oge,Expr(Evar y,_),b)
     83    when y = x -> Some (true, b)
     84  | _ -> None
    5385
    5486(* this function tells when to perform the optimization on a statement. It *)
    55 (* should always return [false] when the optimization cannot be applied *) 
     87(* should always return [false] when the optimization cannot be applied *)
    5688let heuristics
    5789    ((max_factor, global_vars) : heuristic_global_info)
    5890    (rfrncd_vars : heuristic_local_info)
    59                 : Clight.statement -> int option =
    60                         let global_referenced = IdentSet.union global_vars rfrncd_vars in
    61                         function
    62                         | Clight.Sfor (Some _, init, guard, tail, body) ->
    63                                 let head_vars =
    64                                         IdentSet.union
    65                                          (vars_of_stmt init)
    66                                          (IdentSet.union (vars_of_expr guard) (vars_of_stmt tail)) in
    67                                 let dangerous =
    68                                         IdentSet.union (changed_in body) global_referenced in
    69                                 if IdentSet.is_empty (IdentSet.inter head_vars dangerous) then
    70                                         Some max_factor
    71                                 else
    72                                         None
    73                                 (* TODO add a check for size *)
    74                         | _ -> None
     91    : Clight.statement -> (int * AST.ident * sign * expr * expr * bool) option =
     92  let global_referenced = IdentSet.union global_vars rfrncd_vars in
     93  function
     94    | Clight.Sfor (Some _, init, guard, tail, body) ->
     95      begin
     96        match find_increment tail with
     97          | Some (x, dir, inc) ->
     98            begin
     99              match find_bound dir x guard with
     100                | Some (included, bound) ->
     101                  let head_vars =
     102                    IdentSet.union (vars_of_expr guard) (vars_of_stmt tail) in
     103                  let dangerous =
     104                    IdentSet.union (changed_in body) global_referenced in
     105                  if IdentSet.is_empty (IdentSet.inter head_vars dangerous) then
     106                    Some (max_factor, x, dir, inc, bound, included)
     107                  else
     108                    None
     109                | None -> None
     110            end
     111          | None -> None
     112      end
     113    (* TODO add a check for size *)
     114    | _ -> None
    75115
    76116let sexpr a b = CostLabel.Sexpr(a,b)
     
    85125      | _ -> ClightFold.expr_fill_exprs e expr_res in
    86126  let f_stmt i s stmt expr_res stmt_res =
    87                 match stmt, stmt_res with
    88                         | Clight.Scost(lbl, _), stmt' :: _ ->
     127    match stmt, stmt_res with
     128      | Clight.Scost(lbl, _), stmt' :: _ ->
    89129        let lbl = CostLabel.comp_index i s lbl in
    90                                 Clight.Scost(lbl,stmt')
    91                         | _ -> ClightFold.statement_fill_subs stmt expr_res stmt_res in
    92         (fun i s -> ClightFold.expr2 (f_expr i s)),
     130        Clight.Scost(lbl,stmt')
     131      | _ -> ClightFold.statement_fill_subs stmt expr_res stmt_res in
     132  (fun i s -> ClightFold.expr2 (f_expr i s)),
    93133  (fun i s -> ClightFold.statement2 (f_expr i s) (f_stmt i s))
    94134
    95135let labels_of =
    96         let f_expr _ _ = () in
    97         let f_stmt stmt _ res_stmts =
    98                 let s = match stmt with
    99                         | Clight.Slabel(lbl, _) -> Label.Set.singleton lbl
    100                         | _ -> Label.Set.empty in
    101                 List.fold_left Label.Set.union s res_stmts in
    102         ClightFold.statement2 f_expr f_stmt
     136  let f_expr _ _ = () in
     137  let f_stmt stmt _ res_stmts =
     138    let s = match stmt with
     139      | Clight.Slabel(lbl, _) -> Label.Set.singleton lbl
     140      | _ -> Label.Set.empty in
     141    List.fold_left Label.Set.union s res_stmts in
     142  ClightFold.statement2 f_expr f_stmt
    103143
    104144let create_fresh_labels fresh lbl_set =
    105         let f_lbl lbl = Label.Map.add lbl (fresh ()) in
    106         Label.Set.fold f_lbl lbl_set Label.Map.empty
    107        
     145  let f_lbl lbl = Label.Map.add lbl (fresh ()) in
     146  Label.Set.fold f_lbl lbl_set Label.Map.empty
     147
    108148let apply_label_map map =
    109         let f_stmt stmt exprs stmts =
    110                 match stmt, stmts with
    111                         | Clight.Slabel (lbl, _), s :: _ ->
     149  let f_stmt stmt exprs stmts =
     150    match stmt, stmts with
     151      | Clight.Slabel (lbl, _), s :: _ ->
    112152                                (* lbl must be in domain of map *)
    113                                 Clight.Slabel (Label.Map.find lbl map, s)
    114                         | Clight.Sgoto lbl, _ ->
    115                                 Clight.Sgoto (
    116                                         try
    117                                                 Label.Map.find lbl map
    118                                   with
    119                                           | Not_found -> (* means it is an outgoing goto *)
    120                                             lbl)
    121                         | _ -> ClightFold.statement_fill_subs stmt exprs stmts in
    122         ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt
    123 
    124 (* unroll the k-th copy over a total of n *)   
     153        Clight.Slabel (Label.Map.find lbl map, s)
     154      | Clight.Sgoto lbl, _ ->
     155        Clight.Sgoto (
     156          try
     157            Label.Map.find lbl map
     158          with
     159            | Not_found -> (* means it is an outgoing goto *)
     160              lbl)
     161      | _ -> ClightFold.statement_fill_subs stmt exprs stmts in
     162  ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt
     163
     164(* unroll the k-th copy over a total of n *)
    125165let rec do_the_unrolling fresh k n i e sb st labels_of_sb =
    126         if k = 0 then reindex_stmt i (sexpr n 0) sb else
    127         let preamble = do_the_unrolling fresh (k-1) n i e sb st labels_of_sb in
    128   let st_pre = reindex_stmt i (sexpr n (k-1)) st in
    129   let e_next = reindex_expr i (sexpr n k) e in
    130         let sb_next = apply_label_map (create_fresh_labels fresh labels_of_sb) sb in
    131   let sb_next = reindex_stmt i (sexpr n k) sb_next in
    132         Ssequence(preamble,
    133         Ssequence(st_pre,
    134         Ssequence(Sifthenelse(e_next, Sskip, Sbreak),
    135                   sb_next)))
     166  if k = 0 then reindex_stmt i (sexpr n 0) sb else
     167    let preamble = do_the_unrolling fresh (k-1) n i e sb st labels_of_sb in
     168    let st_pre = reindex_stmt i (sexpr n (k-1)) st in
     169    let e_next = reindex_expr i (sexpr n k) e in
     170    let sb_next = apply_label_map (create_fresh_labels fresh labels_of_sb) sb in
     171    let sb_next = reindex_stmt i (sexpr n k) sb_next in
     172    Ssequence(preamble,
     173              Ssequence(st_pre,
     174                        Ssequence(Sifthenelse(e_next, Sskip, Sbreak),
     175                                  sb_next)))
    136176
    137177let unroll fresh g_info l_info =
    138         let f_stmt stmt exprs stmts =
    139                 match heuristics g_info l_info stmt, stmt, exprs, stmts with
    140                         | Some k, Clight.Sfor (Some i, _, _, _, _), e :: _, si :: st :: sb ::_ ->
    141               (* we can suppose no label in s3 is target of a goto outside of stmt, *)
    142               (* as loop is indexed and thus single entry. So we can freely rename *)
    143               (* labels in stmt. *)
    144                                 (* IMPORTANT: I am supposing no labels are in s1 and s2 *)
    145                                 let labels_of_sb = labels_of sb in
    146                                 let e_first = reindex_expr i (sexpr k 0) e in
    147                                 let st_last = reindex_stmt i (sexpr k (k-1)) st in
    148                                 let body = do_the_unrolling fresh (k-1) k i e sb st labels_of_sb in
    149                                 Sfor (Some i, si, e_first, st_last, body)
    150                         | Some _, _, _, _ ->
    151                                 assert false (* heuristics should have crossed out other cases *)
    152                         | _ -> ClightFold.statement_fill_subs stmt exprs stmts in
    153         ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt
     178  let f_stmt stmt exprs stmts =
     179    match heuristics g_info l_info stmt, stmt, exprs, stmts with
     180      | Some (k, x, dir, inc, bound, included),
     181    Clight.Sfor (Some i, _, _, _, _), e :: _, si :: st :: sb ::_ ->
     182      (* we can suppose no label in s3 is target of a goto outside of stmt, *)
     183      (* as loop is indexed and thus single entry. So we can freely rename *)
     184      (* labels in stmt. *)
     185      (* IMPORTANT: I am supposing no labels are in s1 and s2 *)
     186      let labels_of_sb = labels_of sb in
     187      let e_first = reindex_expr i (sexpr k 0) e in
     188      let st_last = reindex_stmt i (sexpr k (k-1)) st in
     189      let body = do_the_unrolling fresh (k-1) k i e sb st labels_of_sb in
     190      Sfor (Some i, si, e_first, st_last, body)
     191      | Some _, _, _, _ ->
     192        assert false (* heuristics should have crossed out other cases *)
     193      | _ -> ClightFold.statement_fill_subs stmt exprs stmts in
     194  ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt
    154195
    155196let unroll_funct fresh g_info = function
    156         | (id, Clight.Internal def) ->
    157                 let l_info = mk_heuristic_local_info def in
    158                 let body = unroll fresh g_info l_info def.Clight.fn_body in
    159                 (id, Clight.Internal {def with Clight.fn_body = body})
    160         | f -> f
     197  | (id, Clight.Internal def) ->
     198    let l_info = mk_heuristic_local_info def in
     199    let body = unroll fresh g_info l_info def.Clight.fn_body in
     200    (id, Clight.Internal {def with Clight.fn_body = body})
     201  | f -> f
    161202
    162203open Languages
    163204
    164205let trans ?(factor = 2) () = Clight, function
    165         | AstClight p ->
    166                 let g_info = mk_heuristic_global_info factor p in
    167                 let fresh = ClightAnnotator.make_fresh "_l" p in
     206  | AstClight p ->
     207    let g_info = mk_heuristic_global_info factor p in
     208    let fresh = ClightAnnotator.make_fresh "_l" p in
    168209    let functs = List.map (unroll_funct fresh g_info) p.Clight.prog_funct in
    169                 AstClight { p with Clight.prog_funct = functs }
    170         | _ -> assert false
    171                
     210    AstClight { p with Clight.prog_funct = functs }
     211  | _ -> assert false
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costExpr.ml

    r1483 r1507  
    2121type cost_expr =
    2222    | Exact of int
    23     | Ternary of index * cond * cost_expr * cost_expr
     23    | Ternary of index * CondSet.t * cost_expr * cost_expr
    2424
    2525(* compute from the set [s] a the 3-uple [Some (h, s_h, s_rest)] where *)
     
    4848            let if_true = cost_mapping_ind atom (h :: ind) m s_head in
    4949            let if_false = cost_mapping_ind atom ind m s_rest in
    50             Ternary(i, condition, if_true, if_false) 
     50            Ternary(i, CondSet.singleton condition, if_true, if_false) 
    5151
    5252let indexing_sets_from_cost_mapping m =
     
    236236        let rec simplify' conds = function
    237237                | Exact k -> Exact k
    238                 | Ternary (i, cond, if_true, if_false) ->
     238                | Ternary (i, gen_cond, if_true, if_false) ->
     239                        assert (CondSet.cardinal gen_cond = 1);
     240                        let cond = CondSet.choose gen_cond in
    239241                        (* if it is the first time a condition on i is encountered, we ensure *)
    240242                        (* that conds holds a default value that will be the "true" of these *)
     
    254256                                ExtArray.set conds i (cond_and_not conds_i cond);
    255257                                let if_false' = simplify' conds if_false in
    256                                 Ternary (i, cond', if_true', if_false')
     258                                Ternary (i, CondSet.singleton cond', if_true', if_false')
    257259                        end in
    258260        let conds = ExtArray.make ~buff:4 0 (CondSet.singleton (Cgeq 0)) in
    259261        simplify' conds
    260262
     263let gen_or = CondSet.union
     264
     265let gen_and s1 s2 =
     266        let f c s = CondSet.union s (cond_and s1 c) in
     267        CondSet.fold f s2 CondSet.empty
     268       
     269let gen_and_not s1 s2 =
     270        let f c s = cond_and_not s c in
     271        CondSet.fold f s2 s1
     272       
     273let gen_not s = gen_and_not (CondSet.singleton (Cgeq 0)) s
     274
    261275let rec remove_useless_branchings = function
    262276        | Exact k -> Exact k
    263         | Ternary (i, cond, if_true, if_false) ->
    264                 let if_true' = remove_useless_branchings if_true in
    265     let if_false' = remove_useless_branchings if_false in
    266                 if if_true = if_false then if_true else
    267                 Ternary (i, cond, if_true', if_false')
     277        | Ternary (i, c1, left, right) ->
     278                let left = remove_useless_branchings left in
     279    let right = remove_useless_branchings right in
     280                match left, right with
     281                        | _, _ when left = right -> left
     282                        | Ternary(j, c2, lleft, lright), _
     283                          when i = j && lleft = right ->
     284                                let c = gen_or (gen_not c1) c2 in
     285                                Ternary(i, c, lleft, lright)
     286      | Ternary(j, c2, lleft, lright), _
     287        when i = j && lright = right ->
     288        let c = gen_and c1 c2 in
     289        Ternary(i, c, lleft, lright)
     290      | _, Ternary(j, c2, rleft, rright)
     291        when i = j && left = rleft ->
     292        let c = gen_or c1 c2 in
     293        Ternary(i, c, rleft, rright)
     294      | _, Ternary(j, c2, rleft, rright)
     295        when i = j && left = rright ->
     296        let c = gen_and_not c2 c1 in
     297        Ternary(i, c, rleft, rright)
     298                        | _ -> Ternary (i, c1, left, right)
     299
     300let rec chose_smaller_cond = function
     301        | Exact k -> Exact k
     302        | Ternary (i, c, left, right) ->
     303                let left = chose_smaller_cond left in
     304                let right = chose_smaller_cond right in
     305                let c_not = gen_not c in
     306                if CondSet.cardinal c > CondSet.cardinal c_not then
     307                        Ternary (i, c_not, right, left)
     308                else
     309                        Ternary (i, c, left, right)
    268310
    269311let cost_expr_mapping_of_cost_mapping m =
     
    273315                        let e = remove_useless_branches e in
    274316                        let e = remove_useless_branchings e in
     317                        let e = chose_smaller_cond e in
    275318      Atom.Map.add at e in
    276319    Atom.Map.fold f sets Atom.Map.empty
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costExpr.mli

    r1468 r1507  
    1 open CostLabel
    2 
    31type cond =
    42    | Ceq of int         (** index is equal to *)
     
    64    | Cmod of int*int    (** index modulo equal to *)
    75    | Cgeqmod of int*int*int (** index greater than and modulo equal to *)
    8    
     6
     7module CondSet : Set.S with type elt = cond
     8
     9open CostLabel
     10
    911type cost_expr =
    1012    | Exact of int
    11     | Ternary of index * cond * cost_expr * cost_expr
     13    | Ternary of index * CondSet.t * cost_expr * cost_expr
    1214
    1315(** [expr_cost_mapping_of_cost_mapping] turns a cost mapping on indexed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/languages.ml

    r1433 r1507  
    215215
    216216(* FIXME *)
    217 let instrument costs_mapping = function
     217let instrument cost_tern costs_mapping = function
    218218  | AstClight p ->
    219     let (p', cost_id, cost_incr) = ClightAnnotator.instrument p costs_mapping in
     219    let (p', cost_id, cost_incr) =
     220      ClightAnnotator.instrument cost_tern p costs_mapping in
    220221    (AstClight p', cost_id, cost_incr)
    221222(*
     
    231232    (p, "", "")
    232233
    233 let annotate input_ast final =
     234let annotate cost_tern input_ast final =
    234235  let costs_mapping = compute_costs final in
    235   instrument costs_mapping input_ast
     236  instrument cost_tern costs_mapping input_ast
    236237
    237238let string_output = function
  • Deliverables/D2.2/8051-indexed-labels-branch/src/languages.mli

    r1433 r1507  
    7171val labelize : ast -> ast
    7272
    73 (** [annotate input_ast target_ast] inserts cost annotations into the input AST
    74     from the (final) target AST. It also returns the name of the cost variable
    75     and the name of the cost increment function. *)
    76 val annotate : ast -> ast -> (ast * string * string)
     73(** [annotate cost_tern input_ast target_ast] inserts cost annotations into the
     74    input AST from the (final) target AST. It also returns the name of the cost
     75    variable and the name of the cost increment function. The [cost_tern] flag
     76    rules whether cost increments are given by ternary expressions or branch
     77    statements. *)
     78val annotate : bool -> ast -> ast -> (ast * string * string)
    7779
    7880(** [interpret debug ast] runs the program [ast] from the default initial
  • Deliverables/D2.2/8051-indexed-labels-branch/src/options.ml

    r1483 r1507  
    5353let get_transformations () = !transformations
    5454
     55let cost_ternary_flag           = ref true
     56let set_cost_ternary            = (:=) cost_ternary_flag
     57let is_cost_ternary_enabled ()  = !cost_ternary_flag
     58
    5559(*
    5660let print_result_flag           = ref false
     
    6266let set_dev_test                = (:=) dev_test
    6367let is_dev_test_enabled ()      = !dev_test
     68
     69let help_specify_opt_stage (trans : Languages.transformation) =
     70        Printf.sprintf "(done at the %s stage)." (Languages.to_string (fst trans))
     71
     72let basic_optimizations =
     73        [
     74                LoopPeeling.trans;
     75                ConstPropagation.trans;
     76                CopyPropagation.trans;
     77                RedundancyElimination.trans;
     78    CopyPropagation.trans;
     79    RedundancyElimination.trans
     80        ]
     81 
    6482
    6583let options = OptionsParsing.register [
     
    88106  "-o", Arg.String set_output_files,
    89107  " Prefix of the output files.";
    90        
    91     "-peel", Arg.Unit (add_transformation LoopPeeling.trans),
    92     " Apply loop peeling.";
    93                
    94                 "-cst-prop", Arg.Unit (add_transformation ConstPropagation.trans),
    95     " Apply constant propagation.";
    96108
    97     "-cpy-prop", Arg.Unit (add_transformation CopyPropagation.trans),
    98     " Apply copy propagation.";
     109  "-peel", Arg.Unit (add_transformation LoopPeeling.trans),
     110  " Apply loop peeling " ^
     111    help_specify_opt_stage LoopPeeling.trans;
    99112
    100     "-pre", Arg.Unit (add_transformation RedundancyElimination.trans),
    101     " Apply partial redundancy elimination.";
    102                
    103                 "-unroll-for",
    104     Arg.Int (fun i -> add_transformation (LoopUnrolling.trans ~factor:i ()) ()),
    105                 " Apply loop unrolling (specifying factor).";
     113  "-cst-prop", Arg.Unit (add_transformation ConstPropagation.trans),
     114  " Apply constant propagation " ^
     115    help_specify_opt_stage ConstPropagation.trans;
    106116
     117  "-cpy-prop", Arg.Unit (add_transformation CopyPropagation.trans),
     118  " Apply copy propagation " ^
     119    help_specify_opt_stage CopyPropagation.trans;
     120
     121  "-pre", Arg.Unit (add_transformation RedundancyElimination.trans),
     122  " Apply partial redundancy elimination " ^
     123    help_specify_opt_stage RedundancyElimination.trans;
     124
     125  "-unroll-for",
     126  Arg.Int (fun i -> add_transformation (LoopUnrolling.trans ~factor:i ()) ()),
     127  " Apply loop unrolling, specifying factor " ^
     128  help_specify_opt_stage (LoopUnrolling.trans ());
     129
     130  "-unroll", Arg.Unit (add_transformation (LoopUnrolling.trans ())),
     131  " Apply loop unrolling " ^
     132  help_specify_opt_stage (LoopUnrolling.trans ());
     133
     134  "-O", Arg.Unit (add_transformations basic_optimizations),
     135  " Apply some optimizations.";
     136
     137  "-no-cost-tern",  Arg.Clear cost_ternary_flag,
     138  " Replace cost ternary expressions with equivalent branch statements.";
     139 
    107140(*
    108141  "-res", Arg.Set print_result_flag,
  • Deliverables/D2.2/8051-indexed-labels-branch/src/options.mli

    r1433 r1507  
    3232val is_debug_enabled : unit -> bool
    3333
     34(** {2 Cost ternary expressions} *)
     35val is_cost_ternary_enabled : unit -> bool
     36
    3437(** {2 Intermediate transformations } *)
    3538val get_transformations : unit -> Languages.transformation list
Note: See TracChangeset for help on using the changeset viewer.