Ignore:
Timestamp:
Oct 10, 2011, 4:34:54 PM (9 years ago)
Author:
tranquil
Message:

work on RTLabs and RTL completed

File:
1 edited

Legend:

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

    r818 r1340  
    3333      lenv     : local_env }
    3434
     35type indexing = CostLabel.const_indexing
     36
    3537(* Execution states. There are three possible states :
    3638   - The constructor [State] represents a state when executing a function
     
    4042type state =
    4143  | State of stack_frame list * RTLabs.graph * Val.address (* stack pointer *) *
    42              Label.t * local_env * memory * CostLabel.t list
     44       Label.t * local_env * memory * indexing list * CostLabel.t list
    4345  | CallState of stack_frame list * RTLabs.function_def *
    44                  Val.t list (* args *) * memory * CostLabel.t list
     46              Val.t list (* args *) * memory * indexing list * CostLabel.t list
    4547  | ReturnState of stack_frame list * Val.t (* return value *) *
    46                    memory * CostLabel.t list
     48        memory * indexing list * CostLabel.t list
    4749
    4850let string_of_local_env lenv =
     
    5759  List.fold_left f "" args
    5860
    59 let print_state = function
    60   | State (_, _, sp, lbl, lenv, mem, _) ->
    61     Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
     61let print_state state = (match state with
     62  | State (_, _, sp, lbl, lenv, mem, ind::_, _) ->
     63    Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:"
    6264      (Val.string_of_address sp)
    6365      (string_of_local_env lenv)
    64       (Mem.to_string mem)
     66      (Mem.to_string mem);
     67                        Array.iter (fun a -> Printf.printf "%d, " a) ind;
     68                        Printf.printf "Regular state: %s\n\n%!"
    6569      lbl
    66   | CallState (_, _, args, mem, _) ->
     70  | CallState (_, _, args, mem, _, _) ->
    6771    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
    6872      (Mem.to_string mem)
    6973      (string_of_args args)
    70   | ReturnState (_, v, mem, _) ->
     74  | ReturnState (_, v, mem, _, _) ->
    7175    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    7276      (Mem.to_string mem)
    7377      (Val.to_string v)
     78        | _ -> assert false (* list of indexings in State should be non-empty *)
     79        ); Printf.printf "-----------------------------------------------------\n\n%!"
    7480
    7581
     
    106112(* Assign a value to some destinations registers. *)
    107113
    108 let assign_state sfrs graph sp lbl lenv mem trace destr v =
     114let assign_state sfrs graph sp lbl lenv mem inds trace destr v =
    109115  let lenv = update_local destr v lenv in
    110   State (sfrs, graph, sp, lbl, lenv, mem, trace)
     116  State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
    111117
    112118(* Branch on a value. *)
    113119
    114 let branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v =
     120let branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v =
    115121  let next_lbl =
    116122    if Val.is_true v then lbl_true
     
    118124      if Val.is_false v then lbl_false
    119125      else error "Undefined conditional value." in
    120   State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
    121 
     126  State (sfrs, graph, sp, next_lbl, lenv, mem, inds, trace)
     127
     128
     129let curr_ind : indexing list -> indexing = function
     130        | ind :: _ -> ind
     131        | _ -> assert false (* indexing list must be non-empty *)
     132
     133let forget_ind : indexing list -> indexing list = function
     134        | _ :: tail -> tail
     135        | _ -> assert false (* indexing list must be non-empty *)
     136
     137let max_depth graph =
     138        let f_stmt _ = function
     139                | RTLabs.St_ind_0(i,_) | RTLabs.St_ind_inc(i,_) -> max (i + 1)
     140                | _ -> fun x -> x in
     141        Label.Map.fold f_stmt graph 0
    122142
    123143(* Interpret statements. *)
     
    130150    (mem   : memory)
    131151    (stmt  : RTLabs.statement)
     152                (inds  : indexing list)
    132153    (trace : CostLabel.t list) :
    133154    state = match stmt with
    134155
    135156      | RTLabs.St_skip lbl ->
    136         State (sfrs, graph, sp, lbl, lenv, mem, trace)
     157        State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
    137158
    138159      | RTLabs.St_cost (cost_lbl, lbl) ->
    139         State (sfrs, graph, sp, lbl, lenv, mem, cost_lbl :: trace)
     160  let cost_lbl = CostLabel.apply_const_indexing (curr_ind inds) cost_lbl in
     161        State (sfrs, graph, sp, lbl, lenv, mem, inds, cost_lbl :: trace)
     162       
     163            | RTLabs.St_ind_0 (i, lbl) ->
     164        CostLabel.enter_loop (Some i) (curr_ind inds);
     165  State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
     166
     167      | RTLabs.St_ind_inc (i, lbl) ->
     168  CostLabel.continue_loop (Some i) (curr_ind inds);
     169  State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
    140170
    141171      | RTLabs.St_cst (destr, cst, lbl) ->
    142172        let v = Eval.cst mem sp (get_type lenv destr) cst in
    143         assign_state sfrs graph sp lbl lenv mem trace destr v
     173        assign_state sfrs graph sp lbl lenv mem inds trace destr v
    144174
    145175      | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
     
    147177          Eval.op1 (get_type lenv destr) (get_type lenv srcr) op1
    148178            (get_value lenv srcr) in
    149         assign_state sfrs graph sp lbl lenv mem trace destr v
     179        assign_state sfrs graph sp lbl lenv mem inds trace destr v
    150180
    151181      | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
     
    156186            (get_value lenv srcr1)
    157187            (get_value lenv srcr2) in
    158         assign_state sfrs graph sp lbl lenv mem trace destr v
     188        assign_state sfrs graph sp lbl lenv mem inds trace destr v
    159189
    160190      | RTLabs.St_load (q, addr, destr, lbl) ->
    161191        let addr = address_of_value (get_value lenv addr) in
    162192        let v = Mem.loadq mem q addr in
    163         assign_state sfrs graph sp lbl lenv mem trace destr v
     193        assign_state sfrs graph sp lbl lenv mem inds trace destr v
    164194
    165195      | RTLabs.St_store (q, addr, srcr, lbl) ->
     
    167197        let v = get_value lenv srcr in
    168198        let mem = Mem.storeq mem q addr v in
    169         State (sfrs, graph, sp, lbl, lenv, mem, trace)
     199        State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
    170200
    171201      | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
     
    174204        (* Save the stack frame. *)
    175205        let sf =
    176           { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
    177         in
    178         CallState (sf :: sfrs, f_def, args, mem, trace)
     206          {ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv} in
     207        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    179208
    180209      | RTLabs.St_call_ptr (r, args, destr, sg, lbl) ->
     
    186215          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
    187216        in
    188         CallState (sf :: sfrs, f_def, args, mem, trace)
     217        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    189218
    190219      | RTLabs.St_tailcall_id (f, args, sg) ->
     
    193222        (* No need to save the stack frame. But free the stack. *)
    194223        let mem = Mem.free mem sp in
    195         CallState (sfrs, f_def, args, mem, trace)
     224        CallState (sfrs, f_def, args, mem, inds, trace)
    196225
    197226      | RTLabs.St_tailcall_ptr (r, args, sg) ->
     
    201230        (* No need to save the stack frame. But free the stack. *)
    202231        let mem = Mem.free mem sp in
    203         CallState (sfrs, f_def, args, mem, trace)
     232        CallState (sfrs, f_def, args, mem, inds, trace)
    204233
    205234      | RTLabs.St_cond (srcr, lbl_true, lbl_false) ->
    206235        let v = get_value lenv srcr in
    207         branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
     236        branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v
    208237
    209238(*
     
    242271      | RTLabs.St_return None ->
    243272        let mem = Mem.free mem sp in
    244         ReturnState (sfrs, Val.undef, mem, trace)
     273        ReturnState (sfrs, Val.undef, mem, inds, trace)
    245274
    246275      | RTLabs.St_return (Some r) ->
    247276        let v = get_value lenv r in
    248277        let mem = Mem.free mem sp in
    249         ReturnState (sfrs, v, mem, trace)
     278        ReturnState (sfrs, v, mem, inds, trace)
    250279
    251280
     
    274303    (args  : Val.t list)
    275304    (mem   : memory)
     305                (inds  : indexing list)
    276306    (trace : CostLabel.t list) :
    277307    state =
     
    281311        Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in
    282312      let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in
    283       State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry, lenv, mem',
    284              trace)
     313            (* allocate new constant indexing *)
     314                        let graph = def.RTLabs.f_graph in
     315                        let ind = Array.make (max_depth graph) 0 in
     316      State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', ind::inds, trace)
    285317    | RTLabs.F_ext def ->
    286318      let (mem', v) = interpret_external mem def.AST.ef_tag args in
    287       ReturnState (sfrs, v, mem', trace)
     319      ReturnState (sfrs, v, mem', inds, trace)
    288320
    289321
     
    293325    (ret_val : Val.t)
    294326    (mem     : memory)
     327                (inds    : indexing list)
    295328    (trace   : CostLabel.t list) :
    296329    state =
     
    298331    | None -> sf.lenv
    299332    | Some ret_reg -> update_local ret_reg ret_val sf.lenv in
    300   State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace)
     333        (* erase current indexing and revert to previous one *)
     334  let inds = forget_ind inds in
     335  State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, inds, trace)
    301336
    302337
    303338let small_step (st : state) : state = match st with
    304   | State (sfrs, graph, sp, pc, lenv, mem, trace) ->
     339  | State (sfrs, graph, sp, pc, lenv, mem, inds, trace) ->
    305340    let stmt = Label.Map.find pc graph in
    306     interpret_statement sfrs graph sp lenv mem stmt trace
    307   | CallState (sfrs, f_def, args, mem, trace) ->
    308     state_after_call sfrs f_def args mem trace
    309   | ReturnState ([], ret_val, mem, trace) ->
     341    interpret_statement sfrs graph sp lenv mem stmt inds trace
     342  | CallState (sfrs, f_def, args, mem, inds, trace) ->
     343    state_after_call sfrs f_def args mem inds trace
     344  | ReturnState ([], ret_val, mem, inds, trace) ->
    310345    assert false (* End of execution; handled in iter_small_step. *)
    311   | ReturnState (sf :: sfrs, ret_val, mem, trace) ->
    312     state_after_return sf sfrs ret_val mem trace
     346  | ReturnState (sf :: sfrs, ret_val, mem, inds, trace) ->
     347    state_after_return sf sfrs ret_val mem inds trace
    313348
    314349
     
    324359  if debug then print_state st ;
    325360  match small_step st with
    326     | ReturnState ([], v, mem, trace) ->
    327       print_and_return_result (compute_result v, List.rev trace)
     361    | ReturnState ([], v, mem, inds, trace) ->
     362      print_and_return_result (compute_result v, trace)
    328363    | st' -> iter_small_step debug st'
    329364
     
    352387      let mem = init_mem p in
    353388      let main_def = find_function mem main in
    354       let st = CallState ([], main_def, [], mem, []) in
     389      let st = CallState ([], main_def, [], mem, [], []) in
    355390      iter_small_step debug st
Note: See TracChangeset for help on using the changeset viewer.