Changeset 1340


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

work on RTLabs and RTL completed

Location:
Deliverables/D2.2/8051-indexed-labels-branch/src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTL/RTL.mli

    r818 r1340  
    1616  (* Emit a cost label. *)
    1717  | St_cost of CostLabel.t * Label.t
     18
     19  (* Reset to 0 a loop index *)
     20  | St_ind_0 of CostLabel.index * Label.t
     21
     22  (* Increment a loop index *)
     23  | St_ind_inc of CostLabel.index * Label.t
    1824
    1925  (* Assign the address of a symbol to registers. Parameters are the destination
  • 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
  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTL/RTLPrinter.ml

    r1291 r1340  
    4545    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    4646    Printf.sprintf "emit %s --> %s" cost_lbl lbl
     47  | RTL.St_ind_0 (i, lbl) ->
     48    Printf.sprintf "index %d --> %s" i lbl
     49  | RTL.St_ind_inc (i, lbl) ->
     50    Printf.sprintf "increment %d --> %s" i lbl
    4751  | RTL.St_addr (dstr1, dstr2, id, lbl) ->
    4852    Printf.sprintf "imm (%s, %s), %s --> %s"
  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabs.mli

    r818 r1340  
    2121  (* Emit a cost label. *)
    2222  | St_cost of CostLabel.t * Label.t
     23
     24  (* Reset to 0 a loop index *)
     25        | St_ind_0 of CostLabel.index * Label.t
     26
     27  (* Increment a loop index *)
     28        | St_ind_inc of CostLabel.index * Label.t
    2329
    2430  (* Assign a constant to registers. Parameters are the destination register,
  • 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
  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsPrinter.ml

    r1291 r1340  
    138138    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    139139    Printf.sprintf "emit %s --> %s" cost_lbl lbl
     140  | RTLabs.St_ind_0 (i, lbl) ->
     141    Printf.sprintf "index %d --> %s" i lbl
     142  | RTLabs.St_ind_inc (i, lbl) ->
     143    Printf.sprintf "increment %d --> %s" i lbl
    140144  | RTLabs.St_cst (destr, cst, lbl) ->
    141145      Printf.sprintf "imm %s, %s --> %s"
  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsToRTL.ml

    r818 r1340  
    9393  | RTL.St_skip _ -> RTL.St_skip lbl
    9494  | RTL.St_cost (cost_lbl, _) -> RTL.St_cost (cost_lbl, lbl)
     95  | RTL.St_ind_0 (i, _) -> RTL.St_ind_0 (i, lbl)
     96  | RTL.St_ind_inc (i, _) -> RTL.St_ind_inc (i, lbl)
    9597  | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl)
    9698  | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl)
     
    685687    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
    686688
     689  | RTLabs.St_ind_0 (i, lbl') ->
     690    add_graph lbl (RTL.St_ind_0 (i, lbl')) def
     691
     692  | RTLabs.St_ind_inc (i, lbl') ->
     693    add_graph lbl (RTL.St_ind_inc (i, lbl')) def
     694
    687695  | RTLabs.St_cst (destr, cst, lbl') ->
    688696    translate_cst cst (find_local_env destr lenv) lbl lbl' def
  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorToRTLabs.ml

    r818 r1340  
    371371      generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
    372372
     373    | Cminor.St_ind_0 (i, s) ->
     374      let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
     375      let old_entry = rtlabs_fun.RTLabs.f_entry in
     376      generate rtlabs_fun (RTLabs.St_ind_0 (i, old_entry))
     377
     378    | Cminor.St_ind_inc (s, i) ->
     379      let old_entry = rtlabs_fun.RTLabs.f_entry in
     380            let rtlabs_fun = generate rtlabs_fun (RTLabs.St_ind_inc(i, old_entry)) in
     381      translate_stmt rtlabs_fun lenv exits s
     382
    373383    | Cminor.St_goto lbl ->
    374384      change_entry rtlabs_fun lbl
Note: See TracChangeset for help on using the changeset viewer.