Changeset 1433 for Deliverables/D2.2


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
Location:
Deliverables/D2.2/8051-indexed-labels-branch/src
Files:
4 added
10 edited

Legend:

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

    r1345 r1433  
    3939        the intermediate programs. *)
    4040    Languages.compile (Options.is_debug_enabled ())
    41       src_language tgt_language input_ast
     41      (Options.get_transformations ()) src_language tgt_language input_ast
    4242  in
    4343  let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
  • 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 *)
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightToCminor.ml

    r1422 r1433  
    647647
    648648let translate p =
    649         (* apply loop peeling *)
    650         let p = LoopPeeling.apply p in
    651649  let fresh = ClightAnnotator.make_fresh "_tmp" p in
    652650  { Cminor.vars = List.map translate_global p.Clight.prog_vars ;
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml

    r1421 r1433  
    172172let constant_map d x =
    173173  Set.fold (fun k accu -> Map.add k x accu) d Map.empty
     174
    174175       
    175         (**  **)
     176                (**  **)
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli

    r1421 r1433  
    107107val constant_map : Set.t -> 'a -> 'a Map.t
    108108
     109
  • Deliverables/D2.2/8051-indexed-labels-branch/src/dev_test.ml

    r818 r1433  
    1717    let p = Languages.add_runtime p in
    1818    let p = Languages.labelize p in
    19     let ps = Languages.compile false Languages.Clight target p in
     19    let ps = Languages.compile false [] Languages.Clight target p in
    2020    let f f' p = match Languages.language_of_ast p with
    2121      | l when l = target -> f' p
  • Deliverables/D2.2/8051-indexed-labels-branch/src/languages.ml

    r818 r1433  
    3535  | AstLIN    of LIN.program
    3636  | AstASM    of ASM.program
     37
     38type transformation = name * (ast -> ast)
    3739
    3840let language_of_ast = function
     
    134136]
    135137
    136 let compile debug src tgt =
    137   (* Find the maximal suffix of the chain that starts with the
    138      language [src]. *)
    139   let rec subchain = function
    140     | [] ->
    141       (* The chain is assumed to be well-formed: such a suffix
    142          exists. *)
    143       assert false
    144     | ((l, _, _) :: _) as chain when l = src -> chain
    145     | _ :: chain -> subchain chain
    146   in
     138let insert_transformations ts chain =
     139        (* turn transformation into elements of the compilation chain *)
     140        let trans_to_comp (n, t) = (n, n, t) in
     141        let ts = List.map trans_to_comp ts in
     142        (* ts and chain are merged, and then sorted so that the resulting list is *)
     143        (* still a well formed compilation chain. Stable sort preserves order *)
     144        (* between transformations on the same language as appearing in ts *)
     145        let compare (n1, n2, s) (m1, m2, t) = compare (n1, n2) (m1, m2) in
     146        List.stable_sort compare (ts @ chain)
     147
     148let compile debug ts src tgt =
     149        (* insert intermediate transformations *)
     150  let chain = insert_transformations ts compilation_chain in
     151        (* erase transformations whose source is strictly before src *)
     152        let chain = List.filter (function (l1, _, _) -> l1 >= src) chain in
     153  (* erase transformations whose target is strictly after tgt *)
     154        let chain = List.filter (function (_, l2, _) -> l2 <= tgt) chain in
    147155  (* Compose the atomic translations to build a compilation function
    148156     from [src] to [tgt]. Again, we assume that the compilation chain
     
    151159     translation from [src] to [tgt]. *)
    152160  let rec compose iprogs src tgt chains ast =
    153     if src = tgt then List.rev (ast :: iprogs)
    154     else
    155       match chains with
    156         | [] ->
     161    match chains with
     162        | [] when src = tgt -> List.rev (ast :: iprogs)
     163        | [] -> 
    157164          Error.global_error "During compilation configuration"
    158165            (Printf.sprintf "It is not possible to compile from `%s' to `%s'."
     
    166173          ast :: l2_to_tgt iprog
    167174  in
    168   compose [] src tgt (subchain compilation_chain)
     175  compose [] src tgt chain
    169176
    170177
  • Deliverables/D2.2/8051-indexed-labels-branch/src/languages.mli

    r818 r1433  
    3030  | AstASM     of ASM.program
    3131
     32
     33(** The type of additional transfromations, with the language they take place
     34    in and the actual transformation *)
     35type transformation = name * (ast -> ast)
     36
    3237(** [language_of_ast ast] returns the programming language of the
    3338    abstract syntax tree [ast]. *)
     
    4045(** {2 Compilation} *)
    4146
    42 (** [compile debug l1 l2] returns the compilation function that
    43     translates the language [l1] to the language [l2]. This may be the
     47(** [compile debug ts l1 l2] returns the compilation function that
     48    translates the language [l1] to the language [l2], employing the
     49                transformations in [ts] along the way . This may be the
    4450    composition of several compilation functions. If [debug] is
    4551    [true], all the intermediate programs are inserted in the
    4652    output. *)
    47 val compile : bool -> name -> name -> (ast -> ast list)
     53val compile : bool -> transformation list -> name -> name -> (ast -> ast list)
    4854
    4955(** [add_runtime ast] adds runtime functions for the operations not supported by
  • Deliverables/D2.2/8051-indexed-labels-branch/src/options.ml

    r1328 r1433  
    4848let is_debug_enabled ()         = !debug_flag
    4949
     50let transformations = ref []
     51let add_transformation t () = transformations := t :: !transformations
     52let get_transformations () = !transformations
     53
    5054(*
    5155let print_result_flag           = ref false
     
    8387  "-o", Arg.String set_output_files,
    8488  " Prefix of the output files.";
     89       
     90        "-peel", Arg.Unit (add_transformation LoopPeeling.trans),
     91        " Apply loop peeling.";
    8592
    8693(*
  • Deliverables/D2.2/8051-indexed-labels-branch/src/options.mli

    r1328 r1433  
    3232val is_debug_enabled : unit -> bool
    3333
     34(** {2 Intermediate transformations } *)
     35val get_transformations : unit -> Languages.transformation list
    3436(*
    3537(** {2 Print results requests} *)
Note: See TracChangeset for help on using the changeset viewer.