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/ERTL
Files:
6 edited

Legend:

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

    r1462 r1542  
    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/src/ERTL/ERTLInterpret.ml

    r1462 r1542  
    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
     
    6265let change_trace st trace = { st with trace = trace }
    6366let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
     67let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds)
     68let new_ind st = { st with inds = CostLabel.new_const_ind st.inds }
     69let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds }
     70let enter_loop st = CostLabel.enter_loop st.inds
     71let continue_loop st = CostLabel.continue_loop st.inds
    6472
    6573let empty_state =
     
    7280    renv   = I8051.RegisterMap.empty ;
    7381    mem    = Mem.empty ;
     82    inds   = [] ;
    7483    trace  = [] }
    7584
     
    118127  let lenv = Register.Set.fold f def.ERTL.f_locals Register.Map.empty in
    119128  let pc = entry_pc lbls_offs ptr def in
     129  let st = new_ind st in
    120130  change_lenv (change_pc st pc) lenv
    121131
     
    231241
    232242let interpret_return lbls_offs st =
     243  let st = forget_ind st in
    233244  let st = pop_st_frs st in
    234245  let (st, pch) = pop st in
     
    254265
    255266    | ERTL.St_cost (cost_lbl, lbl) ->
     267      let cost_lbl = ev_label st cost_lbl in
    256268      let st = add_trace st cost_lbl in
     269      next_pc st lbl
     270
     271    | ERTL.St_ind_0 (i, lbl) ->
     272      enter_loop st i;
     273      next_pc st lbl
     274
     275    | ERTL.St_ind_inc (i, lbl) ->
     276      continue_loop st i;
    257277      next_pc st lbl
    258278
  • Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml

    r1462 r1542  
    4343    Printf.sprintf "*** %s *** --> %s" s lbl
    4444  | ERTL.St_cost (cost_lbl, lbl) ->
     45    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    4546    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
    4651  | ERTL.St_get_hdw (r1, r2, lbl) ->
    4752    Printf.sprintf "move %s, %s --> %s"
  • Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml

    r1488 r1542  
    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/src/ERTL/liveness.ml

    r1462 r1542  
    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)
     
    8385end
    8486
    85 module Label_ImperativeMap = struct
    86 
    87   type key =
    88       Label.Map.key
    89  
    90   type 'data t =
    91       'data Label.Map.t ref
    92      
    93   let create () =
    94     ref Label.Map.empty
    95 
    96   let clear t =
    97     t := Label.Map.empty
    98    
    99   let add k d t =
    100     t := Label.Map.add k d !t
    101 
    102   let find k t =
    103     Label.Map.find k !t
    104 
    105   let iter f t =
    106     Label.Map.iter f !t
    107 
    108 end
    109 
    110 module F = Fix.Make (Label_ImperativeMap) (L)
     87module F = Fix.Make (Label.ImpMap) (L)
    11188
    11289(* These are the sets of variables defined at (written by) a statement. *)
     
    11794  | St_comment _
    11895  | St_cost _
     96  | St_ind_0 _
     97  | St_ind_inc _
    11998  | St_push _
    12099  | St_store _
     
    169148  | St_comment _
    170149  | St_cost _
     150  | St_ind_0 _
     151  | St_ind_inc _
    171152  | St_framesize _
    172153  | St_pop _
     
    227208  | St_comment _
    228209  | St_cost _
     210  | St_ind_0 _
     211  | St_ind_inc _
    229212  | St_newframe _
    230213  | St_delframe _
  • Deliverables/D2.2/8051/src/ERTL/uses.ml

    r1462 r1542  
    2020  | St_comment _
    2121  | St_cost _
     22  | St_ind_0 _
     23  | St_ind_inc _
    2224  | St_hdw_to_hdw _
    2325  | St_newframe _
Note: See TracChangeset for help on using the changeset viewer.