Ignore:
Timestamp:
Oct 10, 2011, 11:32:44 PM (9 years ago)
Author:
tranquil
Message:
  • work on LIN completed
  • small implementation of extensible arrays
File:
1 edited

Legend:

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

    r818 r1349  
    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
     
    4549let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
    4650
     51let forget_ind st = match st.inds with
     52    | _ :: tail -> {st with inds = tail}
     53    | _ -> assert false (* indexing list must be non-empty *)
     54let curr_ind st = match st.inds with
     55    | ind :: _ -> ind
     56    | _ -> assert false (* indexing list must be non-empty *)
     57let allocate_ind st n = { st with inds = Array.make n 0 :: st.inds }
     58
     59let max_depth =
     60    let f_stmt j = function
     61        | LIN.St_ind_0 i | LIN.St_ind_inc i -> max (i + 1) j
     62        | _ -> j in
     63    List.fold_left f_stmt 0
     64
    4765let empty_state =
    4866  { pc     = Val.null ;
     
    5270    renv   = I8051.RegisterMap.empty ;
    5371    mem    = Mem.empty ;
     72                inds   = [] ;
    5473    trace  = [] }
    5574
     
    7190  else error msg
    7291
    73 let init_fun_call st ptr =
     92let init_fun_call st ptr def =
     93        let st = allocate_ind st (max_depth def) in
    7494  change_pc st (Val.change_address_offset ptr Val.Offset.zero)
    7595
     
    171191    | LIN.F_int def ->
    172192      let st = save_ra st in
    173       init_fun_call st ptr
     193      init_fun_call st ptr def
    174194    | LIN.F_ext def ->
    175195      let st = next_pc st in
     
    177197
    178198let interpret_return st =
     199        let st = forget_ind st in
    179200  let (st, pc) = return_pc st in
    180201  change_pc st pc
     
    196217
    197218    | LIN.St_cost cost_lbl ->
     219                        let cost_lbl = CostLabel.apply_const_indexing (curr_ind st) cost_lbl in
    198220      let st = add_trace st cost_lbl in
    199221      next_pc st
     222                       
     223                | LIN.St_ind_0 i ->
     224                        CostLabel.enter_loop (Some i) (curr_ind st);
     225                        next_pc st
     226
     227    | LIN.St_ind_inc i ->
     228            CostLabel.continue_loop (Some i) (curr_ind st);
     229            next_pc st
    200230
    201231    | LIN.St_int (r, i) ->
     
    348378  match Mem.find_fun_def st.mem ptr with
    349379    | LIN.F_int def ->
    350       init_fun_call st ptr
     380      init_fun_call st ptr def
    351381    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
    352382
Note: See TracChangeset for help on using the changeset viewer.