Ignore:
Timestamp:
Oct 10, 2011, 5:50:56 PM (8 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/LTL/LTLInterpret.ml

    r818 r1345  
    3131      renv   : hdw_reg_env ;
    3232      mem    : memory ;
     33                        inds   : CostLabel.const_indexing list ;
    3334      trace  : CostLabel.t list }
    3435
     
    4546let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
    4647
     48let forget_ind st = match st.inds with
     49    | _ :: tail -> {st with inds = tail}
     50    | _ -> assert false (* indexing list must be non-empty *)
     51let curr_ind st = match st.inds with
     52    | ind :: _ -> ind
     53    | _ -> assert false (* indexing list must be non-empty *)
     54let allocate_ind st n = { st with inds = Array.make n 0 :: st.inds }
     55
     56let 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
     61
    4762let empty_state =
    4863  { pc     = Val.null ;
     
    5267    renv   = I8051.RegisterMap.empty ;
    5368    mem    = Mem.empty ;
     69                inds   = [] ;
    5470    trace  = [] }
    5571
     
    95111let init_fun_call lbls_offs st ptr def =
    96112  let pc = entry_pc lbls_offs ptr def in
     113        let st = allocate_ind st (max_depth def.LTL.f_graph) in
    97114  change_pc st pc
    98115
     
    208225
    209226let interpret_return lbls_offs st =
     227        let st = forget_ind st in
    210228  let (st, pc) = return_pc st in
    211229  change_pc st pc
     
    228246
    229247    | LTL.St_cost (cost_lbl, lbl) ->
     248                        let cost_lbl = CostLabel.apply_const_indexing (curr_ind st) cost_lbl in
    230249      let st = add_trace st cost_lbl in
    231250      next_pc st lbl
    232251
    233     | LTL.St_int (r, i, lbl) ->
     252    | LTL.St_ind_0 (i, lbl) ->
     253            CostLabel.enter_loop (Some i) (curr_ind st);
     254            next_pc st lbl
     255
     256    | LTL.St_ind_inc (i, lbl) ->
     257      CostLabel.continue_loop (Some i) (curr_ind st);
     258      next_pc st lbl
     259
     260                | LTL.St_int (r, i, lbl) ->
    234261      let st = add_reg r (Val.of_int i) st in
    235262      next_pc st lbl
Note: See TracChangeset for help on using the changeset viewer.