Changeset 1345 for Deliverables/D2.2


Ignore:
Timestamp:
Oct 10, 2011, 5:50:56 PM (8 years ago)
Author:
tranquil
Message:

work on ERTL and LTL completed

Location:
Deliverables/D2.2/8051-indexed-labels-branch/src
Files:
16 edited

Legend:

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

    r818 r1345  
    4848  (* Emit a cost label. *)
    4949  | St_cost of CostLabel.t * Label.t
     50
     51  (* Reset to 0 a loop index *)
     52  | St_ind_0 of CostLabel.index * Label.t
     53
     54  (* Increment a loop index *)
     55  | St_ind_inc of CostLabel.index * Label.t
    5056
    5157  (* Assign the content of a hardware register to a pseudo register. Parameters
  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTLInterpret.ml

    r818 r1345  
    3232
    3333type stack_frame = local_env
     34
     35type indexing = CostLabel.const_indexing
    3436
    3537(* Execution states. *)
     
    4446      renv   : hdw_reg_env ;
    4547      mem    : memory ;
     48                        inds   : indexing list;
    4649      trace  : CostLabel.t list }
    4750
     
    6366let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
    6467
     68let forget_ind st = match st.inds with
     69        | _ :: tail -> {st with inds = tail}
     70        | _ -> assert false (* indexing list must be non-empty *)
     71let curr_ind st = match st.inds with
     72        | ind :: _ -> ind
     73        | _ -> assert false (* indexing list must be non-empty *)
     74let allocate_ind st n = { st with inds = Array.make n 0 :: st.inds }
     75
     76let max_depth graph =
     77    let f_stmt _ = function
     78        | ERTL.St_ind_0(i,_) | ERTL.St_ind_inc(i,_) -> max (i + 1)
     79        | _ -> fun x -> x in
     80    Label.Map.fold f_stmt graph 0
     81
    6582let empty_state =
    6683  { st_frs = [] ;
     
    7289    renv   = I8051.RegisterMap.empty ;
    7390    mem    = Mem.empty ;
     91                inds   = [] ;
    7492    trace  = [] }
    7593
     
    118136  let lenv = Register.Set.fold f def.ERTL.f_locals Register.Map.empty in
    119137  let pc = entry_pc lbls_offs ptr def in
     138        let st = allocate_ind st (max_depth def.ERTL.f_graph) in
    120139  change_lenv (change_pc st pc) lenv
    121140
     
    222241      let st = save_ra lbls_offs st ra in
    223242      let st = save_frame st in
     243                        let max_depth = max_depth def.ERTL.f_graph in
    224244      init_fun_call lbls_offs st ptr def
    225245    | ERTL.F_ext def ->
     
    229249
    230250let interpret_return lbls_offs st =
     251        let st = forget_ind st in
    231252  let st = pop_st_frs st in
    232253  let (st, pch) = pop st in
     
    252273
    253274    | ERTL.St_cost (cost_lbl, lbl) ->
     275                        let cost_lbl = CostLabel.apply_const_indexing (curr_ind st) cost_lbl in
    254276      let st = add_trace st cost_lbl in
     277      next_pc st lbl
     278
     279    | ERTL.St_ind_0 (i, lbl) ->
     280                        CostLabel.enter_loop (Some i) (curr_ind st);
     281                        next_pc st lbl
     282
     283    | ERTL.St_ind_inc (i, lbl) ->
     284      CostLabel.continue_loop (Some i) (curr_ind st);
    255285      next_pc st lbl
    256286
  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTLPrinter.ml

    r1291 r1345  
    4545                let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    4646    Printf.sprintf "emit %s --> %s" cost_lbl lbl
     47  | ERTL.St_ind_0 (i, lbl) ->
     48    Printf.sprintf "index %d --> %s" i lbl
     49  | ERTL.St_ind_inc (i, lbl) ->
     50    Printf.sprintf "increment %d --> %s" i lbl
    4751  | ERTL.St_get_hdw (r1, r2, lbl) ->
    4852    Printf.sprintf "move %s, %s --> %s"
  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTLToLTLI.ml

    r818 r1345  
    163163
    164164      | ERTL.St_cost (cost_lbl, l) ->
    165         LTL.St_cost (cost_lbl, l)
     165    LTL.St_cost (cost_lbl, l)
     166
     167      | ERTL.St_ind_0 (i, l) ->
     168    LTL.St_ind_0 (i, l)
     169
     170      | ERTL.St_ind_inc (i, l) ->
     171    LTL.St_ind_inc (i, l)
    166172
    167173      | ERTL.St_get_hdw (destr, sourcehwr, l) ->
  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/liveness.ml

    r818 r1345  
    1818  | St_comment (_, l)
    1919  | St_cost (_, l)
     20  | St_ind_0 (_, l)
     21  | St_ind_inc (_, l)
    2022  | St_set_hdw (_, _, l)
    2123  | St_get_hdw (_, _, l)
     
    116118  | St_comment _
    117119  | St_cost _
     120        | St_ind_0 _
     121        | St_ind_inc _
    118122  | St_push _
    119123  | St_store _
     
    168172  | St_comment _
    169173  | St_cost _
     174  | St_ind_0 _
     175  | St_ind_inc _
    170176  | St_framesize _
    171177  | St_pop _
     
    222228  | St_comment _
    223229  | St_cost _
     230  | St_ind_0 _
     231  | St_ind_inc _
    224232  | St_newframe _
    225233  | St_delframe _
  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/uses.ml

    r818 r1345  
    2020  | St_comment _
    2121  | St_cost _
     22  | St_ind_0 _
     23  | St_ind_inc _
    2224  | St_hdw_to_hdw _
    2325  | St_newframe _
  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTL.mli

    r818 r1345  
    1818  (* Emit a cost label. *)
    1919  | St_cost of CostLabel.t * Label.t
     20
     21  (* Reset to 0 a loop index *)
     22  | St_ind_0 of CostLabel.index * Label.t
     23
     24  (* Increment a loop index *)
     25  | St_ind_inc of CostLabel.index * Label.t
    2026
    2127  (* Assign an integer constant to a register. Parameters are the destination
  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLInterpret.ml

    r818 r1345  
    3131      renv   : hdw_reg_env ;
    3232      mem    : memory ;
     33                        inds   : CostLabel.const_indexing list ;
    3334      trace  : CostLabel.t list }
    3435
     
    4546let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
    4647
     48let forget_ind st = match st.inds with
     49    | _ :: tail -> {st with inds = tail}
     50    | _ -> assert false (* indexing list must be non-empty *)
     51let curr_ind st = match st.inds with
     52    | ind :: _ -> ind
     53    | _ -> assert false (* indexing list must be non-empty *)
     54let allocate_ind st n = { st with inds = Array.make n 0 :: st.inds }
     55
     56let max_depth graph =
     57    let f_stmt _ = function
     58        | LTL.St_ind_0(i,_) | LTL.St_ind_inc(i,_) -> max (i + 1)
     59        | _ -> fun x -> x in
     60    Label.Map.fold f_stmt graph 0
     61
    4762let empty_state =
    4863  { pc     = Val.null ;
     
    5267    renv   = I8051.RegisterMap.empty ;
    5368    mem    = Mem.empty ;
     69                inds   = [] ;
    5470    trace  = [] }
    5571
     
    95111let init_fun_call lbls_offs st ptr def =
    96112  let pc = entry_pc lbls_offs ptr def in
     113        let st = allocate_ind st (max_depth def.LTL.f_graph) in
    97114  change_pc st pc
    98115
     
    208225
    209226let interpret_return lbls_offs st =
     227        let st = forget_ind st in
    210228  let (st, pc) = return_pc st in
    211229  change_pc st pc
     
    228246
    229247    | LTL.St_cost (cost_lbl, lbl) ->
     248                        let cost_lbl = CostLabel.apply_const_indexing (curr_ind st) cost_lbl in
    230249      let st = add_trace st cost_lbl in
    231250      next_pc st lbl
    232251
    233     | LTL.St_int (r, i, lbl) ->
     252    | LTL.St_ind_0 (i, lbl) ->
     253            CostLabel.enter_loop (Some i) (curr_ind st);
     254            next_pc st lbl
     255
     256    | LTL.St_ind_inc (i, lbl) ->
     257      CostLabel.continue_loop (Some i) (curr_ind st);
     258      next_pc st lbl
     259
     260                | LTL.St_int (r, i, lbl) ->
    234261      let st = add_reg r (Val.of_int i) st in
    235262      next_pc st lbl
  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLPrinter.ml

    r1291 r1345  
    2727    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    2828    Printf.sprintf "emit %s --> %s" cost_lbl lbl
     29  | LTL.St_ind_0 (i, lbl) ->
     30    Printf.sprintf "index %d --> %s" i lbl
     31  | LTL.St_ind_inc (i, lbl) ->
     32    Printf.sprintf "increment %d --> %s" i lbl
    2933  | LTL.St_int (dstr, i, lbl) ->
    3034    Printf.sprintf "imm %s, %d --> %s" (print_reg dstr) i lbl
  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/branch.ml

    r818 r1345  
    5252    | LTL.St_cost (lbl, l) ->
    5353      LTL.St_cost (lbl, rep l)
     54                | LTL.St_ind_0 (i, l) ->
     55                        LTL.St_ind_0 (i, rep l)
     56    | LTL.St_ind_inc (i, l) ->
     57            LTL.St_ind_inc (i, rep l)
    5458    | LTL.St_int (r, i, l) ->
    5559      LTL.St_int (r, i, rep l)
  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTL/RTLInterpret.ml

    r1340 r1345  
    327327  match small_step st with
    328328    | ReturnState ([], vs, mem, _, trace) ->
    329       print_and_return_result (compute_result vs, trace)
     329      print_and_return_result (compute_result vs, List.rev trace)
    330330    | st' -> iter_small_step debug st'
    331331
  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTL/RTLToERTL.ml

    r818 r1345  
    2222  | ERTL.St_comment (s, _) -> ERTL.St_comment (s, lbl)
    2323  | ERTL.St_cost (cost_lbl, _) -> ERTL.St_cost (cost_lbl, lbl)
     24  | ERTL.St_ind_0 (i, _) -> ERTL.St_ind_0 (i, lbl)
     25  | ERTL.St_ind_inc (i, _) -> ERTL.St_ind_inc (i, lbl)
    2426  | ERTL.St_get_hdw (r1, r2, _) -> ERTL.St_get_hdw (r1, r2, lbl)
    2527  | ERTL.St_set_hdw (r1, r2, _) -> ERTL.St_set_hdw (r1, r2, lbl)
     
    317319    add_graph lbl (ERTL.St_cost (cost_lbl, lbl')) def
    318320
     321  | RTL.St_ind_0 (i, lbl') ->
     322    add_graph lbl (ERTL.St_ind_0 (i, lbl')) def
     323
     324  | RTL.St_ind_inc (i, lbl') ->
     325    add_graph lbl (ERTL.St_ind_inc (i, lbl')) def
     326
    319327  | RTL.St_addr (r1, r2, x, lbl') ->
    320328    adds_graph
     
    428436      let graph = Label.Map.add lbl (ERTL.St_skip next_lbl) def.ERTL.f_graph in
    429437      (Some cost_label, { def with ERTL.f_graph = graph })
     438                | ERTL.St_ind_0 (_, lbl) | ERTL.St_ind_inc (_, lbl)
    430439    | ERTL.St_skip lbl | ERTL.St_comment (_, lbl) | ERTL.St_get_hdw (_, _, lbl)
    431440    | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl)
  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsInterpret.ml

    r1340 r1345  
    360360  match small_step st with
    361361    | ReturnState ([], v, mem, inds, trace) ->
    362       print_and_return_result (compute_result v, trace)
     362      print_and_return_result (compute_result v, List.rev trace)
    363363    | st' -> iter_small_step debug st'
    364364
  • Deliverables/D2.2/8051-indexed-labels-branch/src/acc.ml

    r1328 r1345  
    6565                                        Printf.printf "%s, " (CostLabel.string_of_cost_label
    6666                                                               ~pretty:true l) in
    67                           let print_ls ls = List.iter print_l (List.rev ls) in
     67                          let print_ls ls = List.iter print_l ls in
    6868                                let print_trace (v, ls) =
    6969                                        Printf.printf "%s | " (Big_int.string_of_big_int v);
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightInterpret.ml

    r1334 r1345  
    638638    if debug then Printf.printf "Result = %s\n%!"
    639639      (IntValue.Int32.to_string res) ;
    640     (res, cost_labels) in
     640    (res, List.rev cost_labels) in
    641641  if debug then print_state state ;
    642642  match state with
  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorInterpret.ml

    r1334 r1345  
    394394    if debug then Printf.printf "Result = %s\n%!"
    395395      (IntValue.Int32.to_string res) ;
    396     (res, cost_labels) in
     396    (res, List.rev cost_labels) in
    397397  if debug then print_state state ;
    398398  match state with
Note: See TracChangeset for help on using the changeset viewer.