Ignore:
Timestamp:
Nov 23, 2011, 5:43:24 PM (9 years ago)
Author:
tranquil
Message:

merge of indexed labels branch

Location:
Deliverables/D2.2/8051/src/LTL
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/LTL/LTL.mli

    r1488 r1542  
    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/src/LTL/LTLInterpret.ml

    r1488 r1542  
    3131      renv   : hdw_reg_env ;
    3232      mem    : memory ;
     33      inds   : CostLabel.const_indexing list ;
    3334      trace  : CostLabel.t list }
    3435
     
    4445let change_trace st trace = { st with trace = trace }
    4546let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
     47let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds)
     48let new_ind st = { st with inds = CostLabel.new_const_ind st.inds }
     49let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds }
     50let enter_loop st = CostLabel.enter_loop st.inds
     51let continue_loop st = CostLabel.continue_loop st.inds
    4652
    4753let empty_state =
     
    5258    renv   = I8051.RegisterMap.empty ;
    5359    mem    = Mem.empty ;
     60    inds   = [] ;
    5461    trace  = [] }
    5562
     
    95102let init_fun_call lbls_offs st ptr def =
    96103  let pc = entry_pc lbls_offs ptr def in
     104  let st = new_ind st in
    97105  change_pc st pc
    98106
     
    207215
    208216let interpret_return lbls_offs st =
     217  let st = forget_ind st in
    209218  let (st, pc) = return_pc st in
    210219  change_pc st pc
     
    227236
    228237    | LTL.St_cost (cost_lbl, lbl) ->
     238      let cost_lbl = ev_label st cost_lbl in
    229239      let st = add_trace st cost_lbl in
     240      next_pc st lbl
     241
     242    | LTL.St_ind_0 (i, lbl) ->
     243      enter_loop st i;
     244      next_pc st lbl
     245
     246    | LTL.St_ind_inc (i, lbl) ->
     247      continue_loop st i;
    230248      next_pc st lbl
    231249
  • Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml

    r1488 r1542  
    2525    Printf.sprintf "*** %s *** --> %s" s lbl
    2626  | LTL.St_cost (cost_lbl, lbl) ->
     27    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    2728    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
    2833  | LTL.St_int (dstr, i, lbl) ->
    2934    Printf.sprintf "imm %s, %d --> %s" (print_reg dstr) i lbl
  • Deliverables/D2.2/8051/src/LTL/LTLToLIN.ml

    r1488 r1542  
    2222  | LTL.St_cost (lbl, _) ->
    2323    LIN.St_cost lbl
     24  | LTL.St_ind_0 (i, _) ->
     25    LIN.St_ind_0 i
     26  | LTL.St_ind_inc (i, _) ->
     27    LIN.St_ind_inc i
    2428  | LTL.St_int (r, i, _) ->
    2529    LIN.St_int (r, i)
  • Deliverables/D2.2/8051/src/LTL/LTLToLINI.ml

    r1488 r1542  
    117117        | LTL.St_comment (_, l)
    118118        | LTL.St_cost (_, l)
     119        | LTL.St_ind_0 (_, l)
     120        | LTL.St_ind_inc (_, l)
    119121        | LTL.St_int (_, _, l)
    120122        | LTL.St_pop l
  • Deliverables/D2.2/8051/src/LTL/branch.ml

    r1488 r1542  
    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)
Note: See TracChangeset for help on using the changeset viewer.