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

merge of indexed labels branch

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/LIN/LINInterpret.ml

    r1488 r1542  
    2121
    2222type hdw_reg_env = Val.t I8051.RegisterMap.t
     23
     24
     25type indexing = CostLabel.const_indexing
    2326
    2427(* Execution states. *)
     
    3134      renv   : hdw_reg_env ;
    3235      mem    : memory ;
     36      inds   : indexing list ;
    3337      trace  : CostLabel.t list }
    3438
     
    4448let change_trace st trace = { st with trace = trace }
    4549let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
     50let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds)
     51let new_ind st = { st with inds = CostLabel.new_const_ind st.inds }
     52let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds }
     53let enter_loop st = CostLabel.enter_loop st.inds
     54let continue_loop st = CostLabel.continue_loop st.inds
    4655
    4756let empty_state =
     
    5261    renv   = I8051.RegisterMap.empty ;
    5362    mem    = Mem.empty ;
     63    inds   = [] ;
    5464    trace  = [] }
    5565
     
    7282
    7383let init_fun_call st ptr =
     84  let st = new_ind st in
    7485  change_pc st (Val.change_address_offset ptr Val.Offset.zero)
    7586
     
    176187
    177188let interpret_return st =
     189  let st = forget_ind st in
    178190  let (st, pc) = return_pc st in
    179191  change_pc st pc
     
    195207
    196208    | LIN.St_cost cost_lbl ->
     209      let cost_lbl = ev_label st cost_lbl in
    197210      let st = add_trace st cost_lbl in
     211      next_pc st
     212
     213    | LIN.St_ind_0 i ->
     214      enter_loop st i;
     215      next_pc st
     216
     217    | LIN.St_ind_inc i ->
     218      continue_loop st i;
    198219      next_pc st
    199220
Note: See TracChangeset for help on using the changeset viewer.