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

merge of indexed labels branch

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.