Ignore:
Timestamp:
Oct 11, 2011, 5:42:20 PM (10 years ago)
Author:
tranquil
Message:
  • changed implementation of constant indexings with extensible arrays
  • work on ASM completed
  • next: optimizations!
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLInterpret.ml

    r1345 r1357  
    4545let change_trace st trace = { st with trace = trace }
    4646let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
    47 
    48 let forget_ind st = match st.inds with
    49     | _ :: tail -> {st with inds = tail}
    50     | _ -> assert false (* indexing list must be non-empty *)
    51 let curr_ind st = match st.inds with
    52     | ind :: _ -> ind
    53     | _ -> assert false (* indexing list must be non-empty *)
    54 let allocate_ind st n = { st with inds = Array.make n 0 :: st.inds }
    55 
    56 let max_depth graph =
    57     let f_stmt _ = function
    58         | LTL.St_ind_0(i,_) | LTL.St_ind_inc(i,_) -> max (i + 1)
    59         | _ -> fun x -> x in
    60     Label.Map.fold f_stmt graph 0
     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
    6152
    6253let empty_state =
     
    111102let init_fun_call lbls_offs st ptr def =
    112103  let pc = entry_pc lbls_offs ptr def in
    113         let st = allocate_ind st (max_depth def.LTL.f_graph) in
     104        let st = new_ind st in
    114105  change_pc st pc
    115106
     
    246237
    247238    | LTL.St_cost (cost_lbl, lbl) ->
    248                         let cost_lbl = CostLabel.apply_const_indexing (curr_ind st) cost_lbl in
     239                        let cost_lbl = ev_label st cost_lbl in
    249240      let st = add_trace st cost_lbl in
    250241      next_pc st lbl
    251242
    252243    | LTL.St_ind_0 (i, lbl) ->
    253             CostLabel.enter_loop (Some i) (curr_ind st);
     244            enter_loop st i;
    254245            next_pc st lbl
    255246
    256247    | LTL.St_ind_inc (i, lbl) ->
    257       CostLabel.continue_loop (Some i) (curr_ind st);
     248      continue_loop st i;
    258249      next_pc st lbl
    259250
Note: See TracChangeset for help on using the changeset viewer.