Ignore:
Timestamp:
Oct 10, 2011, 4:34:54 PM (8 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/RTL/RTLInterpret.ml

    r818 r1340  
    3434      carry    : Val.t }
    3535
     36type indexing = CostLabel.const_indexing
     37
    3638(* Execution states. There are three possible states :
    3739   - The constructor [State] represents a state when executing a function
     
    4143type state =
    4244  | State of stack_frame list * RTL.graph * Label.t * Val.address (* sp *) *
    43              local_env * Val.t (* carry *) * memory * CostLabel.t list
     45             local_env * Val.t (* carry *) * memory * indexing list *
     46                                                 CostLabel.t list
    4447  | CallState of stack_frame list * RTL.function_def *
    45                  Val.t list (* args *) * memory * CostLabel.t list
     48              Val.t list (* args *) * memory * indexing list * CostLabel.t list
    4649  | ReturnState of stack_frame list * Val.t list (* return values *) *
    47                    memory * CostLabel.t list
     50                   memory * indexing list * CostLabel.t list
    4851
    4952let string_of_local_env lenv =
     
    5962
    6063let print_state = function
    61   | State (_, _, lbl, sp, lenv, carry, mem, _) ->
    62     Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
     64  | State (_, _, lbl, sp, lenv, carry, mem, ind::_, _) ->
     65    Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:"
    6366      (Val.string_of_address sp)
    6467      (Val.to_string carry)
    6568      (string_of_local_env lenv)
    66       (Mem.to_string mem)
     69      (Mem.to_string mem);
     70                        Array.iter (fun a -> Printf.printf "%d, " a) ind;
     71                        Printf.printf "Regular state: %s\n\n%!"
    6772      lbl
    68   | CallState (_, _, args, mem, _) ->
     73        | State (_, _, _, _, _, _, _, [], _) -> assert false (* indexings non-empty *)
     74  | CallState (_, _, args, mem, _, _) ->
    6975    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
    7076      (Mem.to_string mem)
    7177      (string_of_args args)
    72   | ReturnState (_, vs, mem, _) ->
     78  | ReturnState (_, vs, mem, _, _) ->
    7379    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    7480      (Mem.to_string mem)
     
    96102(* Assign a value to some destinations registers. *)
    97103
    98 let assign_state sfrs graph lbl sp lenv carry mem trace destrs vs =
     104let assign_state sfrs graph lbl sp lenv carry mem inds trace destrs vs =
    99105  let lenv = adds destrs vs lenv in
    100   State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
     106  State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    101107
    102108(* Branch on a value. *)
    103109
    104 let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v =
     110let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v =
    105111  let next_lbl =
    106112    if Val.is_true v then lbl_true
     
    108114      if Val.is_false v then lbl_false
    109115      else error "Undefined conditional value." in
    110   State (sfrs, graph, next_lbl, sp, lenv, carry, mem, trace)
     116  State (sfrs, graph, next_lbl, sp, lenv, carry, mem, inds, trace)
     117
     118let curr_ind : indexing list -> indexing = function
     119    | ind :: _ -> ind
     120    | _ -> assert false (* indexing list must be non-empty *)
     121
     122let forget_ind : indexing list -> indexing list = function
     123    | _ :: tail -> tail
     124    | _ -> assert false (* indexing list must be non-empty *)
     125
     126let max_depth graph =
     127    let f_stmt _ = function
     128        | RTL.St_ind_0(i,_) | RTL.St_ind_inc(i,_) -> max (i + 1)
     129        | _ -> fun x -> x in
     130    Label.Map.fold f_stmt graph 0
    111131
    112132
     
    120140    (carry : Val.t)
    121141    (mem   : memory)
     142                (inds  : indexing list)
    122143    (stmt  : RTL.statement)
    123144    (trace : CostLabel.t list) :
     
    125146
    126147      | RTL.St_skip lbl ->
    127         State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
     148        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    128149
    129150      | RTL.St_cost (cost_lbl, lbl) ->
    130         State (sfrs, graph, lbl, sp, lenv, carry, mem, cost_lbl :: trace)
     151        let cost_lbl = CostLabel.apply_const_indexing (curr_ind inds) cost_lbl in
     152        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, cost_lbl :: trace)
     153
     154      | RTL.St_ind_0 (i, lbl) ->
     155  CostLabel.enter_loop (Some i) (curr_ind inds);
     156  State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
     157
     158      | RTL.St_ind_inc (i, lbl) ->
     159  CostLabel.continue_loop (Some i) (curr_ind inds);
     160  State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    131161
    132162      | RTL.St_addr (r1, r2, x, lbl) ->
    133         assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2]
     163        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2]
    134164          (Mem.find_global mem x)
    135165
    136166      | RTL.St_stackaddr (r1, r2, lbl) ->
    137         assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2] sp
     167        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] sp
    138168
    139169      | RTL.St_int (r, i, lbl) ->
    140         assign_state sfrs graph lbl sp lenv carry mem trace [r] [Val.of_int i]
     170        assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i]
    141171
    142172      | RTL.St_move (destr, srcr, lbl) ->
    143         assign_state sfrs graph lbl sp lenv carry mem trace [destr]
     173        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr]
    144174          [get_local_value lenv srcr]
    145175
     
    149179            (get_local_value lenv srcr1)
    150180            (get_local_value lenv srcr2) in
    151         assign_state sfrs graph lbl sp lenv carry mem trace
     181        assign_state sfrs graph lbl sp lenv carry mem inds trace
    152182          [destr1 ; destr2] [v1 ; v2]
    153183
    154184      | RTL.St_op1 (op1, destr, srcr, lbl) ->
    155185        let v = Eval.op1 op1 (get_local_value lenv srcr) in
    156         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
     186        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
    157187
    158188      | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
     
    161191            (get_local_value lenv srcr1)
    162192            (get_local_value lenv srcr2) in
    163         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
     193        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
    164194
    165195      | RTL.St_clear_carry lbl ->
    166         State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace)
     196        State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, inds, trace)
    167197
    168198      | RTL.St_set_carry lbl ->
    169         State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, trace)
     199        State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, inds, trace)
    170200
    171201      | RTL.St_load (destr, addr1, addr2, lbl) ->
    172202        let addr = get_local_addr lenv addr1 addr2 in
    173203        let v = Mem.load mem chunk addr in
    174         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
     204        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
    175205
    176206      | RTL.St_store (addr1, addr2, srcr, lbl) ->
    177207        let addr = get_local_addr lenv addr1 addr2 in
    178208        let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in
    179         State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
     209        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    180210
    181211      | RTL.St_call_id (f, args, ret_regs, lbl) ->
     
    186216            sp = sp ; lenv = lenv ; carry = carry }
    187217        in
    188         CallState (sf :: sfrs, f_def, args, mem, trace)
     218        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    189219
    190220      | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
     
    194224        let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
    195225                   sp = sp ; lenv = lenv ; carry = carry } in
    196         CallState (sf :: sfrs, f_def, args, mem, trace)
     226        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    197227
    198228      | RTL.St_tailcall_id (f, args) ->
     
    200230        let args = get_arg_values lenv args in
    201231        let mem = Mem.free mem sp in
    202         CallState (sfrs, f_def, args, mem, trace)
     232        CallState (sfrs, f_def, args, mem, inds, trace)
    203233
    204234      | RTL.St_tailcall_ptr (f1, f2, args) ->
     
    207237        let args = get_arg_values lenv args in
    208238        let mem = Mem.free mem sp in
    209         CallState (sfrs, f_def, args, mem, trace)
     239        CallState (sfrs, f_def, args, mem, inds, trace)
    210240
    211241      | RTL.St_cond (srcr, lbl_true, lbl_false) ->
    212242        let v = get_local_value lenv srcr in
    213         branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v
     243        branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v
    214244
    215245      | RTL.St_return rl ->
    216246        let vl = List.map (get_local_value lenv) rl in
    217247        let mem = Mem.free mem sp in
    218         ReturnState (sfrs, vl, mem, trace)
     248        ReturnState (sfrs, vl, mem, inds, trace)
    219249
    220250
     
    240270    (args  : Val.t list)
    241271    (mem   : memory)
     272                (inds  : indexing list)
    242273    (trace : CostLabel.t list) :
    243274    state =
    244275  match f_def with
    245276    | RTL.F_int def ->
     277                        let ind = Array.make (max_depth def.RTL.f_graph) 0 in
    246278      let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
    247279      State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
    248280             init_locals def.RTL.f_locals def.RTL.f_params args,
    249              Val.undef, mem', trace)
     281             Val.undef, mem', ind::inds, trace)
    250282    | RTL.F_ext def ->
    251283      let (mem', vs) = interpret_external mem def.AST.ef_tag args in
    252       ReturnState (sfrs, vs, mem', trace)
     284      ReturnState (sfrs, vs, mem', inds, trace)
    253285
    254286let state_after_return
     
    257289    (ret_vals : Val.t list)
    258290    (mem      : memory)
     291                (inds     : indexing list)
    259292    (trace    : CostLabel.t list) :
    260293    state =
    261294  let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
    262295  let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
    263   State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, trace)
     296        let inds = forget_ind inds in
     297  State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace)
    264298
    265299
    266300let small_step (st : state) : state = match st with
    267   | State (sfrs, graph, pc, sp, lenv, carry, mem, trace) ->
     301  | State (sfrs, graph, pc, sp, lenv, carry, mem, inds, trace) ->
    268302    let stmt = Label.Map.find pc graph in
    269     interpret_statement sfrs graph sp lenv carry mem stmt trace
    270   | CallState (sfrs, f_def, args, mem, trace) ->
    271     state_after_call sfrs f_def args mem trace
    272   | ReturnState ([], ret_vals, mem, trace) ->
     303    interpret_statement sfrs graph sp lenv carry mem inds stmt trace
     304  | CallState (sfrs, f_def, args, mem, inds, trace) ->
     305    state_after_call sfrs f_def args mem inds trace
     306  | ReturnState ([], ret_vals, mem, inds, trace) ->
    273307    assert false (* End of execution; handled in iter_small_step. *)
    274   | ReturnState (sf :: sfrs, ret_vals, mem, trace) ->
    275     state_after_return sf sfrs ret_vals mem trace
     308  | ReturnState (sf :: sfrs, ret_vals, mem, inds, trace) ->
     309    state_after_return sf sfrs ret_vals mem inds trace
    276310
    277311
     
    292326  if debug then print_state st ;
    293327  match small_step st with
    294     | ReturnState ([], vs, mem, trace) ->
    295       print_and_return_result (compute_result vs, List.rev trace)
     328    | ReturnState ([], vs, mem, _, trace) ->
     329      print_and_return_result (compute_result vs, trace)
    296330    | st' -> iter_small_step debug st'
    297331
     
    321355      let mem = init_mem p in
    322356      let main_def = find_function mem main in
    323       let st = CallState ([], main_def, [], mem, []) in
     357      let st = CallState ([], main_def, [], mem, [], []) in
    324358      iter_small_step debug st
Note: See TracChangeset for help on using the changeset viewer.