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

work on ERTL and LTL completed

File:
1 edited

Legend:

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