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

merge of indexed labels branch

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml

    r818 r1542  
    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, inds, _) ->
     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    let i = CostLabel.curr_const_ind inds in
     68    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
     69    Printf.printf "Regular state: %s\n\n%!"
    6570      lbl
    66   | CallState (_, _, args, mem, _) ->
     71  | CallState (_, _, args, mem, _, _) ->
    6772    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
    6873      (Mem.to_string mem)
    6974      (string_of_args args)
    70   | ReturnState (_, v, mem, _) ->
     75  | ReturnState (_, v, mem, _, _) ->
    7176    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    7277      (Mem.to_string mem)
     
    106111(* Assign a value to some destinations registers. *)
    107112
    108 let assign_state sfrs graph sp lbl lenv mem trace destr v =
     113let assign_state sfrs graph sp lbl lenv mem inds trace destr v =
    109114  let lenv = update_local destr v lenv in
    110   State (sfrs, graph, sp, lbl, lenv, mem, trace)
     115  State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
    111116
    112117(* Branch on a value. *)
    113118
    114 let branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v =
     119let branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v =
    115120  let next_lbl =
    116121    if Val.is_true v then lbl_true
     
    118123      if Val.is_false v then lbl_false
    119124      else error "Undefined conditional value." in
    120   State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
    121 
     125  State (sfrs, graph, sp, next_lbl, lenv, mem, inds, trace)
     126
     127let curr_ind = CostLabel.curr_const_ind
     128
     129let forget_ind = CostLabel.forget_const_ind
     130
     131let new_ind = CostLabel.new_const_ind
     132
     133let eval_arg lenv mem sp = function
     134  | RTLabs.Reg r -> get_value lenv r
     135  | RTLabs.Imm (c, t) -> Eval.cst mem sp t c
     136
     137let get_type_arg lenv = function
     138  | RTLabs.Reg r -> get_type lenv r
     139  | RTLabs.Imm (_, typ) -> typ
    122140
    123141(* Interpret statements. *)
     
    130148    (mem   : memory)
    131149    (stmt  : RTLabs.statement)
     150    (inds  : indexing list)
    132151    (trace : CostLabel.t list) :
    133152    state = match stmt with
    134153
    135154      | RTLabs.St_skip lbl ->
    136         State (sfrs, graph, sp, lbl, lenv, mem, trace)
     155        State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
    137156
    138157      | RTLabs.St_cost (cost_lbl, lbl) ->
    139         State (sfrs, graph, sp, lbl, lenv, mem, cost_lbl :: trace)
     158        let cost_lbl =
     159          CostLabel.ev_indexing (curr_ind inds) cost_lbl in
     160        State (sfrs, graph, sp, lbl, lenv,
     161               mem, inds, cost_lbl :: trace)
     162
     163      | RTLabs.St_ind_0 (i, lbl) ->
     164        CostLabel.enter_loop inds i;
     165        State (sfrs, graph, sp, lbl, lenv,
     166               mem, inds, trace)
     167
     168      | RTLabs.St_ind_inc (i, lbl) ->
     169        CostLabel.continue_loop inds i;
     170        State (sfrs, graph, sp, lbl, lenv,
     171               mem, inds, trace)
    140172
    141173      | RTLabs.St_cst (destr, cst, lbl) ->
    142174        let v = Eval.cst mem sp (get_type lenv destr) cst in
    143         assign_state sfrs graph sp lbl lenv mem trace destr v
     175        assign_state sfrs graph sp lbl lenv mem inds trace destr v
    144176
    145177      | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
     
    147179          Eval.op1 (get_type lenv destr) (get_type lenv srcr) op1
    148180            (get_value lenv srcr) in
    149         assign_state sfrs graph sp lbl lenv mem trace destr v
     181        assign_state sfrs graph sp lbl lenv mem inds trace destr v
    150182
    151183      | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
    152184        let v =
    153185          Eval.op2
    154             (get_type lenv destr) (get_type lenv srcr1) (get_type lenv srcr2)
     186            (get_type lenv destr)
     187            (get_type_arg lenv srcr1)
     188            (get_type_arg lenv srcr2)
    155189            op2
    156             (get_value lenv srcr1)
    157             (get_value lenv srcr2) in
    158         assign_state sfrs graph sp lbl lenv mem trace destr v
     190            (eval_arg lenv mem sp srcr1)
     191            (eval_arg lenv mem sp srcr2) in
     192        assign_state sfrs graph sp lbl lenv mem inds trace destr v
    159193
    160194      | RTLabs.St_load (q, addr, destr, lbl) ->
    161         let addr = address_of_value (get_value lenv addr) in
     195        let addr = address_of_value (eval_arg lenv mem sp addr) in
    162196        let v = Mem.loadq mem q addr in
    163         assign_state sfrs graph sp lbl lenv mem trace destr v
     197        assign_state sfrs graph sp lbl lenv mem inds trace destr v
    164198
    165199      | RTLabs.St_store (q, addr, srcr, lbl) ->
    166         let addr = address_of_value (get_value lenv addr) in
    167         let v = get_value lenv srcr in
     200        let addr = address_of_value (eval_arg lenv mem sp addr) in
     201        let v = eval_arg lenv mem sp srcr in
    168202        let mem = Mem.storeq mem q addr v in
    169         State (sfrs, graph, sp, lbl, lenv, mem, trace)
     203        State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
    170204
    171205      | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
     
    176210          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
    177211        in
    178         CallState (sf :: sfrs, f_def, args, mem, trace)
     212        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    179213
    180214      | RTLabs.St_call_ptr (r, args, destr, sg, lbl) ->
     
    186220          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
    187221        in
    188         CallState (sf :: sfrs, f_def, args, mem, trace)
     222        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    189223
    190224      | RTLabs.St_tailcall_id (f, args, sg) ->
     
    193227        (* No need to save the stack frame. But free the stack. *)
    194228        let mem = Mem.free mem sp in
    195         CallState (sfrs, f_def, args, mem, trace)
     229        CallState (sfrs, f_def, args, mem, inds, trace)
    196230
    197231      | RTLabs.St_tailcall_ptr (r, args, sg) ->
     
    201235        (* No need to save the stack frame. But free the stack. *)
    202236        let mem = Mem.free mem sp in
    203         CallState (sfrs, f_def, args, mem, trace)
     237        CallState (sfrs, f_def, args, mem, inds, trace)
    204238
    205239      | RTLabs.St_cond (srcr, lbl_true, lbl_false) ->
    206240        let v = get_value lenv srcr in
    207         branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
     241        branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v
    208242
    209243(*
     
    242276      | RTLabs.St_return None ->
    243277        let mem = Mem.free mem sp in
    244         ReturnState (sfrs, Val.undef, mem, trace)
     278        ReturnState (sfrs, Val.undef, mem, inds, trace)
    245279
    246280      | RTLabs.St_return (Some r) ->
    247281        let v = get_value lenv r in
    248282        let mem = Mem.free mem sp in
    249         ReturnState (sfrs, v, mem, trace)
     283        ReturnState (sfrs, v, mem, inds, trace)
    250284
    251285
     
    274308    (args  : Val.t list)
    275309    (mem   : memory)
     310    (inds  : indexing list)
    276311    (trace : CostLabel.t list) :
    277312    state =
     
    281316        Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in
    282317      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)
     318      (* allocate new constant indexing *)
     319      let graph = def.RTLabs.f_graph in
     320      let inds = new_ind inds in
     321      State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace)
    285322    | RTLabs.F_ext def ->
    286323      let (mem', v) = interpret_external mem def.AST.ef_tag args in
    287       ReturnState (sfrs, v, mem', trace)
     324      ReturnState (sfrs, v, mem', inds, trace)
    288325
    289326
     
    293330    (ret_val : Val.t)
    294331    (mem     : memory)
     332    (inds    : indexing list)
    295333    (trace   : CostLabel.t list) :
    296334    state =
     
    298336    | None -> sf.lenv
    299337    | Some ret_reg -> update_local ret_reg ret_val sf.lenv in
    300   State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace)
     338      (* erase current indexing and revert to previous one *)
     339      let inds = forget_ind inds in
     340      State (sfrs, sf.graph, sf.sp, sf.pc, lenv,
     341             mem, inds, trace)
    301342
    302343
    303344let small_step (st : state) : state = match st with
    304   | State (sfrs, graph, sp, pc, lenv, mem, trace) ->
     345  | State (sfrs, graph, sp, pc, lenv, mem, inds, trace) ->
    305346    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) ->
     347    interpret_statement sfrs graph sp lenv mem stmt inds trace
     348  | CallState (sfrs, f_def, args, mem, inds, trace) ->
     349    state_after_call sfrs f_def args mem inds trace
     350  | ReturnState ([], ret_val, mem, inds, trace) ->
    310351    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
     352  | ReturnState (sf :: sfrs, ret_val, mem, inds, trace) ->
     353    state_after_return sf sfrs ret_val mem inds trace
    313354
    314355
     
    324365  if debug then print_state st ;
    325366  match small_step st with
    326     | ReturnState ([], v, mem, trace) ->
     367    | ReturnState ([], v, mem, inds, trace) ->
    327368      print_and_return_result (compute_result v, List.rev trace)
    328369    | st' -> iter_small_step debug st'
     
    352393      let mem = init_mem p in
    353394      let main_def = find_function mem main in
    354       let st = CallState ([], main_def, [], mem, []) in
     395      let st = CallState ([], main_def, [], mem, [], []) in
    355396      iter_small_step debug st
Note: See TracChangeset for help on using the changeset viewer.