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

merge of indexed labels branch

Location:
Deliverables/D2.2/8051/src/RTLabs
Files:
5 edited

Legend:

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

    r818 r1542  
    1111
    1212
     13type argument =
     14  | Reg of Register.t
     15  | Imm of AST.cst*AST.sig_type
     16
    1317(* A function in RTLabs is a mapping from labels to
    1418   statements. Statements explicitely mention their successors. *)
     
    2226  | St_cost of CostLabel.t * Label.t
    2327
     28  (* Reset to 0 a loop index *)
     29  | St_ind_0 of CostLabel.index * Label.t
     30
     31  (* Increment a loop index *)
     32  | St_ind_inc of CostLabel.index * Label.t
     33
    2434  (* Assign a constant to registers. Parameters are the destination register,
    2535     the constant and the label of the next statement. *)
     
    3242
    3343  (* Application of a binary operation. Parameters are the operation, the
    34      destination register, the two argument registers and the label of the next
     44     destination register, the two arguments and the label of the next
    3545     statement. *)
    36   | St_op2 of AST.op2 * Register.t * Register.t * Register.t * Label.t
     46  | St_op2 of AST.op2 * Register.t * argument * argument * Label.t
    3747
    3848  (* Memory load. Parameters are the size in bytes of what to load, the
    3949     register containing the address, the destination register and the label
    4050     of the next statement. *)
    41   | St_load of AST.quantity * Register.t * Register.t * Label.t
     51  | St_load of AST.quantity * argument * Register.t * Label.t
    4252
    4353  (* Memory store. Parameters are the size in bytes of what to store, the
    4454     register containing the address, the source register and the label of the
    4555     next statement. *)
    46   | St_store of AST.quantity * Register.t * Register.t * Label.t
     56  | St_store of AST.quantity * argument * argument * Label.t
    4757
    4858  (* Call to a function given its name. Parameters are the name of the
  • 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
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml

    r818 r1542  
    4545
    4646let print_cmp = function
    47   | AST.Cmp_eq -> "eq"
    48   | AST.Cmp_ne -> "ne"
    49   | AST.Cmp_gt -> "gt"
    50   | AST.Cmp_ge -> "ge"
    51   | AST.Cmp_lt -> "lt"
    52   | AST.Cmp_le -> "le"
     47  | AST.Cmp_eq -> "="
     48  | AST.Cmp_ne -> "!="
     49  | AST.Cmp_gt -> ">"
     50  | AST.Cmp_ge -> ">="
     51  | AST.Cmp_lt -> "<"
     52  | AST.Cmp_le -> "<="
    5353
    5454let rec print_size = function
     
    8383  Printf.sprintf "%d%s" size (string_of_signedness sign)
    8484
    85 let print_op1 = function
     85let print_op1 op r = Printf.sprintf "%s %s"
     86  (match op with
    8687  | AST.Op_cast (int_type, dest_size) ->
    8788    Printf.sprintf "int%sto%d" (string_of_int_type int_type) dest_size
    88   | AST.Op_negint -> "negint"
    89   | AST.Op_notbool -> "notbool"
    90   | AST.Op_notint -> "notint"
    91   | AST.Op_id -> "id"
     89  | AST.Op_negint -> "-"
     90  | AST.Op_notbool -> "!"
     91  | AST.Op_notint -> "!i"
     92  | AST.Op_id -> ""
    9293  | AST.Op_ptrofint -> "ptrofint"
    93   | AST.Op_intofptr -> "intofptr"
    94 
    95 let print_op2 = function
    96   | AST.Op_add -> "add"
    97   | AST.Op_sub -> "sub"
    98   | AST.Op_mul -> "mul"
    99   | AST.Op_div -> "div"
     94  | AST.Op_intofptr -> "intofptr")
     95        (print_reg r)
     96
     97let print_arg = function
     98  | RTLabs.Reg r -> print_reg r
     99  | RTLabs.Imm (c, t) ->
     100    Printf.sprintf "(%s)%s" (Primitive.print_type t) (print_cst c)
     101
     102let print_op2 op r s = Printf.sprintf "%s %s %s"
     103  (print_arg r)
     104  (match op with
     105  | AST.Op_add -> "+"
     106  | AST.Op_sub -> "-"
     107  | AST.Op_mul -> "*"
     108  | AST.Op_div -> "/"
    100109  | AST.Op_divu -> "/u"
    101110  | AST.Op_mod -> "mod"
     
    104113  | AST.Op_or -> "or"
    105114  | AST.Op_xor -> "xor"
    106   | AST.Op_shl -> "shl"
    107   | AST.Op_shr -> "shr"
    108   | AST.Op_shru -> "shru"
     115  | AST.Op_shl -> "<<"
     116  | AST.Op_shr -> ">>"
     117  | AST.Op_shru -> ">>u"
    109118  | AST.Op_cmp cmp -> print_cmp cmp
    110   | AST.Op_addp -> "addp"
    111   | AST.Op_subp -> "subp"
    112   | AST.Op_subpp -> "subpp"
     119  | AST.Op_addp -> "+p"
     120  | AST.Op_subp -> "-p"
     121  | AST.Op_subpp -> "-pp"
    113122  | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p"
    114   | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u"
     123  | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u")
     124  (print_arg s)
    115125
    116126
     
    136146  | RTLabs.St_skip lbl -> "--> " ^ lbl
    137147  | RTLabs.St_cost (cost_lbl, lbl) ->
    138       Printf.sprintf "emit %s --> %s" cost_lbl lbl
     148    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
     149    Printf.sprintf "emit %s --> %s" cost_lbl lbl
     150  | RTLabs.St_ind_0 (i, lbl) ->
     151    Printf.sprintf "index %d --> %s" i lbl
     152  | RTLabs.St_ind_inc (i, lbl) ->
     153    Printf.sprintf "increment %d --> %s" i lbl
    139154  | RTLabs.St_cst (destr, cst, lbl) ->
    140       Printf.sprintf "imm %s, %s --> %s"
     155      Printf.sprintf "%s := %s --> %s"
    141156        (print_reg destr)
    142157        (print_cst cst)
    143158        lbl
    144159  | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
    145       Printf.sprintf "%s %s, %s --> %s"
    146         (print_op1 op1)
     160      Printf.sprintf "%s := %s --> %s"
    147161        (print_reg destr)
    148         (print_reg srcr)
     162  (print_op1 op1 srcr)
    149163        lbl
    150164  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
    151       Printf.sprintf "%s %s, %s, %s --> %s"
    152         (print_op2 op2)
     165      Printf.sprintf "%s := %s --> %s"
    153166        (print_reg destr)
    154         (print_reg srcr1)
    155         (print_reg srcr2)
     167  (print_op2 op2 srcr1 srcr2)
    156168        lbl
    157169  | RTLabs.St_load (q, addr, destr, lbl) ->
    158       Printf.sprintf "load %s, %s, %s --> %s"
     170      Printf.sprintf "%s := *(%s) %s --> %s"
     171        (print_reg destr)
    159172        (Memory.string_of_quantity q)
    160         (print_reg addr)
    161         (print_reg destr)
     173        (print_arg addr)
    162174        lbl
    163175  | RTLabs.St_store (q, addr, srcr, lbl) ->
    164       Printf.sprintf "store %s, %s, %s --> %s"
    165         (Memory.string_of_quantity q)
    166         (print_reg addr)
    167         (print_reg srcr)
    168         lbl
    169   | RTLabs.St_call_id (f, args, res, sg, lbl) ->
    170       Printf.sprintf "call \"%s\", %s, %s: %s --> %s"
     176      Printf.sprintf "*(%s)%s := %s --> %s"
     177        (Memory.string_of_quantity q)
     178        (print_arg addr)
     179        (print_arg srcr)
     180        lbl
     181  | RTLabs.St_call_id (f, args, Some r, sg, lbl) ->
     182      Printf.sprintf "%s := \"%s\"(%s) : %s --> %s"
     183        (print_reg r)
    171184        f
    172185        (print_args args)
    173         (print_oreg res)
    174         (Primitive.print_sig sg)
    175         lbl
    176   | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    177       Printf.sprintf "call_ptr %s, %s, %s: %s --> %s"
     186        (Primitive.print_sig sg)
     187        lbl
     188  | RTLabs.St_call_id (f, args, None, sg, lbl) ->
     189      Printf.sprintf "\"%s\"(%s) : %s --> %s"
     190        f
     191        (print_args args)
     192        (Primitive.print_sig sg)
     193        lbl
     194  | RTLabs.St_call_ptr (f, args, Some r, sg, lbl) ->
     195      Printf.sprintf "%s := *%s (%s) : %s --> %s"
     196        (print_reg r)
    178197        (print_reg f)
    179198        (print_args args)
    180         (print_oreg res)
     199        (Primitive.print_sig sg)
     200        lbl
     201  | RTLabs.St_call_ptr (f, args, None, sg, lbl) ->
     202      Printf.sprintf "*%s (%s) : %s --> %s"
     203        (print_reg f)
     204        (print_args args)
    181205        (Primitive.print_sig sg)
    182206        lbl
    183207  | RTLabs.St_tailcall_id (f, args, sg) ->
    184       Printf.sprintf "tailcall \"%s\", %s: %s"
     208      Printf.sprintf "tailcall \"%s\" (%s) : %s"
    185209        f
    186210        (print_args args)
    187211        (Primitive.print_sig sg)
    188212  | RTLabs.St_tailcall_ptr (f, args, sg) ->
    189       Printf.sprintf "tailcall_ptr \"%s\", %s: %s"
     213      Printf.sprintf "tailcall *%s (%s) : %s"
    190214        (print_reg f)
    191215        (print_args args)
     
    225249
    226250
    227 let print_graph n c =
     251let print_graph n c entry =
    228252  let f lbl stmt s =
    229253    Printf.sprintf "%s%s: %s\n%s"
     
    232256      (print_statement stmt)
    233257      s in
    234   Label.Map.fold f c ""
    235 
    236 
     258  let f' lbl stmt (reach, s) =
     259    (Label.Set.add lbl reach, f lbl stmt s) in
     260  let (reachable, str) =
     261    RTLabsUtilities.dfs_fold f' c entry (Label.Set.empty, "") in
     262  let filter lbl _ = not (Label.Set.mem lbl reachable) in
     263  let c_rest = Label.Map.filter filter c in
     264  if Label.Map.is_empty c_rest then str else
     265    let str' = Label.Map.fold f c_rest "" in
     266    str ^ "DEAD NODES:\n" ^ str'
     267       
    237268let print_internal_decl n f def =
    238269
     
    252283    (n_spaces (n+2))
    253284    def.RTLabs.f_exit
    254     (print_graph (n+2) def.RTLabs.f_graph)
     285    (print_graph (n+2) def.RTLabs.f_graph def.RTLabs.f_entry)
    255286
    256287
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.mli

    r740 r1542  
    44val print_statement : RTLabs.statement -> string
    55
     6val print_cst : AST.cst -> string
     7
     8val print_op1 : AST.op1 -> Register.t -> string
     9
     10val print_op2 : AST.op2 -> RTLabs.argument -> RTLabs.argument -> string
     11
    612val print_program : RTLabs.program -> string
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

    r818 r1542  
    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
     
    692700      lbl lbl' def
    693701
    694   | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
     702  | RTLabs.St_op2 (op2, destr, RTLabs.Reg srcr1, RTLabs.Reg srcr2, lbl') ->
    695703    translate_op2 op2 (find_local_env destr lenv)
    696704      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
    697705
    698   | RTLabs.St_load (_, addr, destr, lbl') ->
     706  | RTLabs.St_load (_, RTLabs.Reg addr, destr, lbl') ->
    699707    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
    700708      lbl lbl' def
    701709
    702   | RTLabs.St_store (_, addr, srcr, lbl') ->
     710  | RTLabs.St_store (_, RTLabs.Reg addr, RTLabs.Reg srcr, lbl') ->
    703711    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
    704712      lbl lbl' def
     
    739747  | RTLabs.St_return (Some r) ->
    740748    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
    741 
    742 
     749               
     750  | _ -> assert false (*not possible because of previous removal of immediates*)
     751
     752let remove_immediates def =
     753  let load_arg a lbl g rs = match a with
     754    | RTLabs.Reg r -> (lbl, g, rs, r)
     755    | RTLabs.Imm (c, t) ->
     756      let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in
     757      let new_r = Register.fresh def.RTLabs.f_runiverse in
     758      let g = Label.Map.add lbl (RTLabs.St_cst (new_r, c, new_l)) g in
     759      (new_l, g, (new_r, t) :: rs, new_r) in
     760  let f lbl stmt (g, rs) =
     761    match stmt with
     762      | RTLabs.St_op2(op, r, a1, a2, l) ->
     763        let (lbl', g, rs, r1) = load_arg a1 lbl g rs in
     764        let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in
     765        let s = RTLabs.St_op2 (op, r, RTLabs.Reg r1, RTLabs.Reg r2, l) in
     766        let g = Label.Map.add lbl' s g in
     767        (g, rs)
     768      | RTLabs.St_store(q, a1, a2, l) ->
     769        let (lbl', g, rs, r1) = load_arg a1 lbl g rs in
     770        let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in
     771        let s = RTLabs.St_store (q, RTLabs.Reg r1, RTLabs.Reg r2, l) in
     772        let g = Label.Map.add lbl' s g in
     773        (g, rs)
     774      | RTLabs.St_load (q, a, r, l) ->
     775        let (lbl', g, rs, r1) = load_arg a lbl g rs in
     776        let s = RTLabs.St_load (q, RTLabs.Reg r1, r, l) in
     777        let g = Label.Map.add lbl' s g in
     778        (g, rs)
     779      | _ -> (g, rs) in
     780  let g = def.RTLabs.f_graph in
     781  let (g, rs) = Label.Map.fold f g (g, []) in
     782  let locals = List.rev_append rs def.RTLabs.f_locals in
     783  { def with RTLabs.f_graph = g; RTLabs.f_locals = locals }
     784 
    743785let translate_internal def =
     786  let def = remove_immediates def in
    744787  let runiverse = def.RTLabs.f_runiverse in
    745788  let lenv =
Note: See TracChangeset for help on using the changeset viewer.