Ignore:
Timestamp:
Nov 23, 2011, 5:43:24 PM (8 years ago)
Author:
tranquil
Message:

merge of indexed labels branch

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml

    r818 r1542  
    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    let i = CostLabel.curr_const_ind ind in
     71    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
     72    Printf.printf "Regular state: %s\n\n%!"
    6773      lbl
    68   | CallState (_, _, args, mem, _) ->
     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 = CostLabel.curr_const_ind
     119
     120let forget_ind = CostLabel.forget_const_ind
     121
     122let new_ind = CostLabel.new_const_ind
    111123
    112124
     
    120132    (carry : Val.t)
    121133    (mem   : memory)
     134    (inds  : indexing list)
    122135    (stmt  : RTL.statement)
    123136    (trace : CostLabel.t list) :
     
    125138
    126139      | RTL.St_skip lbl ->
    127         State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
     140        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    128141
    129142      | RTL.St_cost (cost_lbl, lbl) ->
    130         State (sfrs, graph, lbl, sp, lenv, carry, mem, cost_lbl :: trace)
     143        let cost_lbl = CostLabel.ev_indexing (curr_ind inds) cost_lbl in
     144        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, cost_lbl :: trace)
     145
     146      | RTL.St_ind_0 (i, lbl) ->
     147        CostLabel.enter_loop inds i;
     148        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
     149
     150      | RTL.St_ind_inc (i, lbl) ->
     151        CostLabel.continue_loop inds i;
     152        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    131153
    132154      | RTL.St_addr (r1, r2, x, lbl) ->
    133         assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2]
     155        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2]
    134156          (Mem.find_global mem x)
    135157
    136158      | RTL.St_stackaddr (r1, r2, lbl) ->
    137         assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2] sp
     159        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] sp
    138160
    139161      | RTL.St_int (r, i, lbl) ->
    140         assign_state sfrs graph lbl sp lenv carry mem trace [r] [Val.of_int i]
     162        assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i]
    141163
    142164      | RTL.St_move (destr, srcr, lbl) ->
    143         assign_state sfrs graph lbl sp lenv carry mem trace [destr]
     165        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr]
    144166          [get_local_value lenv srcr]
    145167
     
    149171            (get_local_value lenv srcr1)
    150172            (get_local_value lenv srcr2) in
    151         assign_state sfrs graph lbl sp lenv carry mem trace
     173        assign_state sfrs graph lbl sp lenv carry mem inds trace
    152174          [destr1 ; destr2] [v1 ; v2]
    153175
    154176      | RTL.St_op1 (op1, destr, srcr, lbl) ->
    155177        let v = Eval.op1 op1 (get_local_value lenv srcr) in
    156         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
     178        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
    157179
    158180      | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
     
    161183            (get_local_value lenv srcr1)
    162184            (get_local_value lenv srcr2) in
    163         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
     185        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
    164186
    165187      | RTL.St_clear_carry lbl ->
    166         State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace)
     188        State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, inds, trace)
    167189
    168190      | RTL.St_set_carry lbl ->
    169         State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, trace)
     191        State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, inds, trace)
    170192
    171193      | RTL.St_load (destr, addr1, addr2, lbl) ->
    172194        let addr = get_local_addr lenv addr1 addr2 in
    173195        let v = Mem.load mem chunk addr in
    174         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
     196        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
    175197
    176198      | RTL.St_store (addr1, addr2, srcr, lbl) ->
    177199        let addr = get_local_addr lenv addr1 addr2 in
    178200        let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in
    179         State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
     201        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    180202
    181203      | RTL.St_call_id (f, args, ret_regs, lbl) ->
     
    186208            sp = sp ; lenv = lenv ; carry = carry }
    187209        in
    188         CallState (sf :: sfrs, f_def, args, mem, trace)
     210        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    189211
    190212      | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
     
    194216        let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
    195217                   sp = sp ; lenv = lenv ; carry = carry } in
    196         CallState (sf :: sfrs, f_def, args, mem, trace)
     218        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    197219
    198220      | RTL.St_tailcall_id (f, args) ->
     
    200222        let args = get_arg_values lenv args in
    201223        let mem = Mem.free mem sp in
    202         CallState (sfrs, f_def, args, mem, trace)
     224        CallState (sfrs, f_def, args, mem, inds, trace)
    203225
    204226      | RTL.St_tailcall_ptr (f1, f2, args) ->
     
    207229        let args = get_arg_values lenv args in
    208230        let mem = Mem.free mem sp in
    209         CallState (sfrs, f_def, args, mem, trace)
     231        CallState (sfrs, f_def, args, mem, inds, trace)
    210232
    211233      | RTL.St_cond (srcr, lbl_true, lbl_false) ->
    212234        let v = get_local_value lenv srcr in
    213         branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v
     235        branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v
    214236
    215237      | RTL.St_return rl ->
    216238        let vl = List.map (get_local_value lenv) rl in
    217239        let mem = Mem.free mem sp in
    218         ReturnState (sfrs, vl, mem, trace)
     240        ReturnState (sfrs, vl, mem, inds, trace)
    219241
    220242
     
    240262    (args  : Val.t list)
    241263    (mem   : memory)
     264    (inds  : indexing list)
    242265    (trace : CostLabel.t list) :
    243266    state =
    244267  match f_def with
    245268    | RTL.F_int def ->
     269      let inds = new_ind inds in
    246270      let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
    247271      State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
    248272             init_locals def.RTL.f_locals def.RTL.f_params args,
    249              Val.undef, mem', trace)
     273             Val.undef, mem', inds, trace)
    250274    | RTL.F_ext def ->
    251275      let (mem', vs) = interpret_external mem def.AST.ef_tag args in
    252       ReturnState (sfrs, vs, mem', trace)
     276      ReturnState (sfrs, vs, mem', inds, trace)
    253277
    254278let state_after_return
     
    257281    (ret_vals : Val.t list)
    258282    (mem      : memory)
     283    (inds     : indexing list)
    259284    (trace    : CostLabel.t list) :
    260285    state =
    261286  let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
    262287  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)
     288  let inds = forget_ind inds in
     289  State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace)
    264290
    265291
    266292let small_step (st : state) : state = match st with
    267   | State (sfrs, graph, pc, sp, lenv, carry, mem, trace) ->
     293  | State (sfrs, graph, pc, sp, lenv, carry, mem, inds, trace) ->
    268294    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) ->
     295    interpret_statement sfrs graph sp lenv carry mem inds stmt trace
     296  | CallState (sfrs, f_def, args, mem, inds, trace) ->
     297    state_after_call sfrs f_def args mem inds trace
     298  | ReturnState ([], ret_vals, mem, inds, trace) ->
    273299    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
     300  | ReturnState (sf :: sfrs, ret_vals, mem, inds, trace) ->
     301    state_after_return sf sfrs ret_vals mem inds trace
    276302
    277303
     
    292318  if debug then print_state st ;
    293319  match small_step st with
    294     | ReturnState ([], vs, mem, trace) ->
     320    | ReturnState ([], vs, mem, _, trace) ->
    295321      print_and_return_result (compute_result vs, List.rev trace)
    296322    | st' -> iter_small_step debug st'
     
    321347      let mem = init_mem p in
    322348      let main_def = find_function mem main in
    323       let st = CallState ([], main_def, [], mem, []) in
     349      let st = CallState ([], main_def, [], mem, [], []) in
    324350      iter_small_step debug st
Note: See TracChangeset for help on using the changeset viewer.