Ignore:
Timestamp:
Apr 4, 2011, 5:18:15 PM (9 years ago)
Author:
ayache
Message:

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

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

Legend:

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

    r486 r740  
    99   RTLabs is the last language of the frontend. It is intended to
    1010   ease retargetting. *)
    11 
    12 
    13 (* From the RTLabs point of view, a pseudo-register can represent a physical
    14    location or a pointer. When instruction selection is over, a pseudo-register
    15    represents a physical location. Thus, some operations --- those on pointers
    16    --- may involve several pseudo-registers when a pointer value is more than
    17    one physical location (which is the case of the 8051). *)
    18 
    19 type registers = Register.t list
    2011
    2112
     
    5243  | St_cost of CostLabel.t * Label.t
    5344
    54   (* Assign a constant to registers. Parameters are the destination registers,
     45  (* Assign a constant to registers. Parameters are the destination register,
    5546     the constant and the label of the next statement. *)
    56   | St_cst of registers * AST.cst * Label.t
     47  | St_cst of Register.t * AST.cst * Label.t
    5748
    5849  (* Application of an unary operation. Parameters are the operation, the
    59      destination registers, the argument registers and the label of the next
     50     destination register, the argument register and the label of the next
    6051     statement. *)
    61   | St_op1 of AST.op1 * registers * registers * Label.t
     52  | St_op1 of AST.op1 * Register.t * Register.t * Label.t
    6253
    6354  (* Application of a binary operation. Parameters are the operation, the
    64      destination register, the argument registers and the label of the next
     55     destination register, the two argument registers and the label of the next
    6556     statement. *)
    66   | St_op2 of AST.op2 * registers * registers * registers * Label.t
     57  | St_op2 of AST.op2 * Register.t * Register.t * Register.t * Label.t
    6758
    68   (* Memory load. Parameters are the size and type of what to load,
    69      the addressing mode and its arguments, the destination register
    70      and the label of the next statement. *)
    71   | St_load of Memory.memory_q * addressing * registers list *
    72                registers * Label.t
     59  (* Memory load. Parameters are the size in bytes of what to load, the
     60     addressing mode and its arguments, the destination register and the label
     61     of the next statement. *)
     62  | St_load of Memory.quantity * addressing * Register.t list * Register.t *
     63               Label.t
    7364
    74   (* Memory store. Parameters are the size and type of what to store,
    75      the addressing mode and its arguments, the source register
    76      and the label of the next statement. *)
    77   | St_store of Memory.memory_q * addressing * registers list *
    78                 registers * Label.t
     65  (* Memory store. Parameters are the size in bytes of what to store, the
     66     addressing mode and its arguments, the source register and the label of the
     67     next statement. *)
     68  | St_store of Memory.quantity * addressing * Register.t list * Register.t *
     69                Label.t
    7970
    8071  (* Call to a function given its name. Parameters are the name of the
    8172     function, the arguments of the function, the destination
    82      registers, the signature of the function and the label of the next
     73     register, the signature of the function and the label of the next
    8374     statement. *)
    84   | St_call_id of AST.ident * registers list * registers *
     75  | St_call_id of AST.ident * Register.t list * Register.t *
    8576                  AST.signature * Label.t
    8677
    87   (* Call to a function given its address. Parameters are registers
     78  (* Call to a function given its address. Parameters are the register
    8879     holding the address of the function, the arguments of the
    89      function, the destination registers, the signature of the function
     80     function, the destination register, the signature of the function
    9081     and the label of the next statement. This statement with an
    9182     [St_op] before can represent a [St_call_id]. However, we
    9283     differenciate the two to allow translation to a formalism with no
    9384     function pointer. *)
    94   | St_call_ptr of registers * registers list * registers *
     85  | St_call_ptr of Register.t * Register.t list * Register.t *
    9586                   AST.signature * Label.t
    9687
    97   (* Tail call to a function given its name. Parameters are the name
    98      of the function, the arguments of the function, the destination
    99      register, the signature of the function and the label of the next
    100      statement. *)
    101   | St_tailcall_id of AST.ident * registers list * AST.signature
     88  (* Tail call to a function given its name. Parameters are the name of the
     89     function, the arguments of the function, the signature of the function and
     90     the label of the next statement. *)
     91  | St_tailcall_id of AST.ident * Register.t list * AST.signature
    10292
    103   (* Tail call to a function given its address. Parameters are a
    104      register holding the address of the function, the arguments of
    105      the function, the destination register, the signature of the
    106      function and the label of the next statement. Same remark as for
    107      the [St_call_ptr]. *)
    108   | St_tailcall_ptr of registers * registers list * AST.signature
     93  (* Tail call to a function given its address. Parameters are a register
     94     holding the address of the function, the arguments of the function, the
     95     signature of the function and the label of the next statement. Same remark
     96     as for the [St_call_ptr]. *)
     97  | St_tailcall_ptr of Register.t * Register.t list * AST.signature
    10998
    11099  (* Constant branch. Parameters are the constant, the label to go to when the
     
    117106     true (not 0), and the label to go to when the operation on the
    118107     argument evaluates to false (0). *)
    119   | St_cond1 of AST.op1 * registers * Label.t * Label.t
     108  | St_cond1 of AST.op1 * Register.t * Label.t * Label.t
    120109
    121110  (* Binary branch. Parameters are the operation, its arguments, the
     
    123112     true (not 0), and the label to go to when the operation on the
    124113     arguments evaluates to false (0). *)
    125   | St_cond2 of AST.op2 * registers * registers * Label.t * Label.t
     114  | St_cond2 of AST.op2 * Register.t * Register.t * Label.t * Label.t
    126115
    127116  (* Jump statement. Parameters are a register and a list of
    128117     labels. The execution will go to the [n]th label of the list of
    129118     labels, where [n] is the natural value held in the register. *)
    130   | St_jumptable of registers * Label.t list
     119  | St_jumptable of Register.t * Label.t list
    131120
    132121  (* Return statement. *)
    133   | St_return of registers
     122  | St_return of Register.t
    134123
    135124
     
    140129      f_runiverse : Register.universe ;
    141130      f_sig       : AST.signature ;
    142       f_result    : registers ;
    143       f_params    : registers list ;
    144       f_locals    : registers list ;
     131      f_result    : Register.t ;
     132      f_params    : Register.t list ;
     133      f_locals    : Register.t list ;
     134      f_ptrs      : Register.t list ;
    145135      f_stacksize : int ;
    146136      f_graph     : graph ;
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml

    r619 r740  
    99module Mem = Driver.RTLabsMemory
    1010module Val = Mem.Value
     11
     12let error_float () = error "float not supported"
    1113
    1214
     
    2527
    2628type stack_frame =
    27     { ret_regs : Register.t list ;
     29    { ret_reg  : Register.t ;
    2830      graph    : RTLabs.graph ;
    29       sp       : Val.t ;
     31      sp       : Val.address ;
    3032      pc       : Label.t ;
    3133      lenv     : local_env }
     
    3739
    3840type state =
    39   | State of stack_frame list * RTLabs.graph * Val.t (* stack pointer *) *
     41  | State of stack_frame list * RTLabs.graph * Val.address (* stack pointer *) *
    4042             Label.t * local_env * memory * CostLabel.t list
    4143  | CallState of stack_frame list * RTLabs.function_def *
     
    4446                   memory * CostLabel.t list
    4547
     48let string_of_local_env lenv =
     49  let f x v s =
     50    s ^
     51      (if Val.eq v Val.undef then ""
     52       else (Register.print x) ^ " = " ^ (Val.to_string v) ^ "  ") in
     53  Register.Map.fold f lenv ""
     54
     55let string_of_args args =
     56  let f s v = s ^ " " ^ (Val.to_string v) in
     57  List.fold_left f "" args
     58
     59let 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%!"
     62      (Val.string_of_address sp)
     63      (string_of_local_env lenv)
     64      (Mem.to_string mem)
     65      lbl
     66  | CallState (_, _, args, mem, _) ->
     67    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
     68      (Mem.to_string mem)
     69      (string_of_args args)
     70  | ReturnState (_, v, mem, _) ->
     71    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
     72      (Mem.to_string mem)
     73      (Val.to_string v)
     74
    4675
    4776let find_function mem f =
    48   let v = Mem.find_global mem f in
    49   Mem.find_fun_def mem v
     77  let addr = Mem.find_global mem f in
     78  Mem.find_fun_def mem addr
    5079
    5180let get_local_value (lenv : local_env) (r : Register.t) : Val.t =
     
    5483let get_arg_values lenv args = List.map (get_local_value lenv) args
    5584
    56 let get_local_valuel (lenv : local_env) (rl : Register.t list) : Val.t =
    57   let vl = List.map (get_local_value lenv) rl in
    58   Val.merge vl
    59 let get_arg_valuesl lenv argsl = List.map (get_local_valuel lenv) argsl
    60 
    61 (* An address is represented by two pseudo-registers (because in 8051, addresses
    62    are coded on two bytes). Thus, assignments may involve several
    63    registers. When we want to assign a single value to several registers, we
    64    break the value into as many parts as there are registers, and then we update
    65    each register with a part of the value. *)
    66 
    67 let adds rs v lenv = match rs with
    68   | [] -> lenv
    69   | _ ->
    70     let vs = Val.break v (List.length rs) in
    71     let f lenv r v = Register.Map.add r v lenv in
    72     List.fold_left2 f lenv rs vs
     85let adds rs vs lenv =
     86  let f lenv r v = Register.Map.add r v lenv in
     87  List.fold_left2 f lenv rs vs
     88
     89let value_of_address = List.hd
     90let address_of_value v = [v]
    7391
    7492
    7593let eval_addressing
    7694    (mem  : memory)
    77     (sp   : Val.t)
     95    (sp   : Val.address)
    7896    (mode : RTLabs.addressing)
    7997    (args : Val.t list) :
    80     Val.t = match mode, args with
    81 
    82       | RTLabs.Aindexed off, addr :: _ when Val.is_pointer addr ->
    83         Val.add addr (Val.of_int off)
    84 
    85       | RTLabs.Aindexed2, addr :: shift :: _
    86         when Val.is_pointer addr && Val.is_int shift ->
    87         Val.add addr shift
    88 
    89       | RTLabs.Aindexed2, shift :: addr :: _
    90         when Val.is_pointer addr && Val.is_int shift ->
    91         Val.add addr shift
     98    Val.address = match mode, args with
     99
     100      | RTLabs.Aindexed off, v :: _ ->
     101        address_of_value (Val.add v (Val.of_int off))
     102
     103      | RTLabs.Aindexed2, v1 :: v2 :: _ ->
     104        address_of_value (Val.add v1 v2)
    92105
    93106      | RTLabs.Aglobal (id, off), _ ->
    94         Val.add (Mem.find_global mem id) (Val.of_int off)
     107        Val.add_address (Mem.find_global mem id) (Val.Offset.of_int off)
    95108
    96109      | RTLabs.Abased (id, off), v :: _ ->
    97         let addr = Val.add (Mem.find_global mem id) (Val.of_int off) in
    98         Val.add addr v
     110        let addr =
     111          Val.add_address (Mem.find_global mem id) (Val.Offset.of_int off) in
     112        address_of_value (Val.add (value_of_address addr) v)
    99113
    100114      | RTLabs.Ainstack off, _ ->
    101         Val.add sp (Val.of_int off)
     115        Val.add_address sp (Val.Offset.of_int off)
    102116
    103117      | _, _ -> error "Bad addressing mode."
     
    106120let eval_cst mem sp = function
    107121  | AST.Cst_int i -> Val.of_int i
    108   | AST.Cst_float f -> Val.of_float f
    109   | AST.Cst_addrsymbol id -> Mem.find_global mem id
    110   | AST.Cst_stackoffset shift -> Val.add sp (Val.of_int shift)
     122  | AST.Cst_float f -> error_float ()
     123  | AST.Cst_addrsymbol id -> value_of_address (Mem.find_global mem id)
     124  | AST.Cst_stackoffset shift ->
     125    value_of_address (Val.add_address sp (Val.Offset.of_int shift))
    111126
    112127let eval_op1 = function
     
    118133  | AST.Op_notbool -> Val.notbool
    119134  | AST.Op_notint -> Val.notint
    120   | AST.Op_negf -> Val.negf
    121   | AST.Op_absf -> Val.absf
    122   | AST.Op_singleoffloat -> Val.singleoffloat
    123   | AST.Op_intoffloat -> Val.intoffloat
    124   | AST.Op_intuoffloat -> Val.intuoffloat
    125   | AST.Op_floatofint -> Val.floatofint
    126   | AST.Op_floatofintu -> Val.floatofintu
     135  | AST.Op_negf
     136  | AST.Op_absf
     137  | AST.Op_singleoffloat
     138  | AST.Op_intoffloat
     139  | AST.Op_intuoffloat
     140  | AST.Op_floatofint
     141  | AST.Op_floatofintu -> error_float ()
    127142  | AST.Op_id -> (fun (v : Val.t) -> v)
    128   | AST.Op_intofptr | AST.Op_ptrofint -> assert false (* TODO? *)
     143  | AST.Op_intofptr | AST.Op_ptrofint -> assert false (* TODO or not? *)
    129144
    130145let rec eval_op2 = function
     
    142157  | AST.Op_shr -> Val.shr
    143158  | AST.Op_shru -> Val.shru
    144   | AST.Op_addf -> Val.addf
    145   | AST.Op_subf -> Val.subf
    146   | AST.Op_mulf -> Val.mulf
    147   | AST.Op_divf -> Val.divf
    148159  | AST.Op_cmp AST.Cmp_eq -> Val.cmp_eq
    149160  | AST.Op_cmp AST.Cmp_ne -> Val.cmp_ne
     
    158169  | AST.Op_cmpu AST.Cmp_gt -> Val.cmp_gt_u
    159170  | AST.Op_cmpu AST.Cmp_ge -> Val.cmp_ge_u
    160   | AST.Op_cmpf AST.Cmp_eq -> Val.cmp_eq_f
    161   | AST.Op_cmpf AST.Cmp_ne -> Val.cmp_ne_f
    162   | AST.Op_cmpf AST.Cmp_lt -> Val.cmp_lt_f
    163   | AST.Op_cmpf AST.Cmp_le -> Val.cmp_le_f
    164   | AST.Op_cmpf AST.Cmp_gt -> Val.cmp_gt_f
    165   | AST.Op_cmpf AST.Cmp_ge -> Val.cmp_ge_f
    166171  | AST.Op_cmpp cmp -> eval_op2 (AST.Op_cmp cmp)
     172  | AST.Op_addf
     173  | AST.Op_subf
     174  | AST.Op_mulf
     175  | AST.Op_divf
     176  | AST.Op_cmpf _ -> error_float ()
    167177
    168178(* Assign a value to some destinations registers. *)
    169179
    170 let assign_state cs c sp lbl lenv mem t destrs v =
    171   let lenv = adds destrs v lenv in
    172   State (cs, c, sp, lbl, lenv, mem, t)
     180let assign_state sfrs graph sp lbl lenv mem trace destr v =
     181  let lenv = Register.Map.add destr v lenv in
     182  State (sfrs, graph, sp, lbl, lenv, mem, trace)
    173183
    174184(* Branch on a value. *)
    175185
    176 let branch_state cs c sp lbl_true lbl_false lenv mem t v =
     186let branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v =
    177187  let next_lbl =
    178188    if Val.is_true v then lbl_true
     
    180190      if Val.is_false v then lbl_false
    181191      else error "Undefined conditional value." in
    182   State (cs, c, sp, next_lbl, lenv, mem, t)
     192  State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
    183193
    184194
     
    186196
    187197let interpret_statement
    188     (cs   : stack_frame list)
    189     (c    : RTLabs.graph)
    190     (sp   : Val.t)
    191     (lenv : local_env)
    192     (mem  : memory)
    193     (stmt : RTLabs.statement)
    194     (t    : CostLabel.t list) :
     198    (sfrs  : stack_frame list)
     199    (graph : RTLabs.graph)
     200    (sp    : Val.address)
     201    (lenv  : local_env)
     202    (mem   : memory)
     203    (stmt  : RTLabs.statement)
     204    (trace : CostLabel.t list) :
    195205    state = match stmt with
    196206
    197       | RTLabs.St_skip lbl -> State (cs, c, sp, lbl, lenv, mem, t)
     207      | RTLabs.St_skip lbl -> State (sfrs, graph, sp, lbl, lenv, mem, trace)
    198208
    199209      | RTLabs.St_cost (cost_lbl, lbl) ->
    200         State (cs, c, sp, lbl, lenv, mem, cost_lbl :: t)
    201 
    202       | RTLabs.St_cst (destrs, cst, lbl) ->
     210        State (sfrs, graph, sp, lbl, lenv, mem, cost_lbl :: trace)
     211
     212      | RTLabs.St_cst (destr, cst, lbl) ->
    203213        let v = eval_cst mem sp cst in
    204         assign_state cs c sp lbl lenv mem t destrs v
    205 
    206       | RTLabs.St_op1 (op1, destrs, srcrs, lbl) ->
    207         let v = eval_op1 op1 (get_local_valuel lenv srcrs) in
    208         assign_state cs c sp lbl lenv mem t destrs v
    209 
    210       | RTLabs.St_op2 (op2, destrs, srcrs1, srcrs2, lbl) ->
     214        assign_state sfrs graph sp lbl lenv mem trace destr v
     215
     216      | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
     217        let v = eval_op1 op1 (get_local_value lenv srcr) in
     218        assign_state sfrs graph sp lbl lenv mem trace destr v
     219
     220      | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
    211221        let v =
    212222          eval_op2 op2
    213             (get_local_valuel lenv srcrs1)
    214             (get_local_valuel lenv srcrs2) in
    215         assign_state cs c sp lbl lenv mem t destrs v
    216 
    217       | RTLabs.St_load (chunk, mode, args, destrs, lbl) ->
    218         let addr = eval_addressing mem sp mode (get_arg_valuesl lenv args) in
    219         let v = Mem.load mem chunk addr in
    220         assign_state cs c sp lbl lenv mem t destrs v
    221 
    222       | RTLabs.St_store (chunk, mode, args, srcrs, lbl) ->
    223         let addr = eval_addressing mem sp mode (get_arg_valuesl lenv args) in
    224         let mem = Mem.store mem chunk addr (get_local_valuel lenv srcrs) in
    225         State (cs, c, sp, lbl, lenv, mem, t)
     223            (get_local_value lenv srcr1)
     224            (get_local_value lenv srcr2) in
     225        assign_state sfrs graph sp lbl lenv mem trace destr v
     226
     227      | RTLabs.St_load (q, mode, args, destr, lbl) ->
     228        let addr = eval_addressing mem sp mode (get_arg_values lenv args) in
     229        let v = Mem.loadq mem q addr in
     230        assign_state sfrs graph sp lbl lenv mem trace destr v
     231
     232      | RTLabs.St_store (q, mode, args, srcr, lbl) ->
     233        let addr = eval_addressing mem sp mode (get_arg_values lenv args) in
     234        let v = get_local_value lenv srcr in
     235        let mem = Mem.storeq mem q addr v in
     236        State (sfrs, graph, sp, lbl, lenv, mem, trace)
    226237
    227238      | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
    228239        let f_def = find_function mem f in
    229         let args = get_arg_valuesl lenv args in
     240        let args = get_arg_values lenv args in
    230241        (* Save the stack frame. *)
    231242        let sf =
    232           { ret_regs = destr ; graph = c ; sp = sp ; pc = lbl ; lenv = lenv }
     243          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
    233244        in
    234         CallState (sf :: cs, f_def, args, mem, t)
    235 
    236       | RTLabs.St_call_ptr (rs, args, destrs, sg, lbl) ->
    237         let addr = get_local_valuel lenv rs in
    238         let f_def = Mem.find_fun_def mem addr in
    239         let args = get_arg_valuesl lenv args in
     245        CallState (sf :: sfrs, f_def, args, mem, trace)
     246
     247      | RTLabs.St_call_ptr (r, args, destr, sg, lbl) ->
     248        let addr = get_local_value lenv r in
     249        let f_def = Mem.find_fun_def mem (address_of_value addr) in
     250        let args = get_arg_values lenv args in
    240251        (* Save the stack frame. *)
    241252        let sf =
    242           { ret_regs = destrs ; graph = c ; sp = sp ; pc = lbl ; lenv = lenv }
     253          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
    243254        in
    244         CallState (sf :: cs, f_def, args, mem, t)
     255        CallState (sf :: sfrs, f_def, args, mem, trace)
    245256
    246257      | RTLabs.St_tailcall_id (f, args, sg) ->
    247258        let f_def = find_function mem f in
    248         let args = get_arg_valuesl lenv args in
     259        let args = get_arg_values lenv args in
    249260        (* No need to save the stack frame. But free the stack. *)
    250261        let mem = Mem.free mem sp in
    251         CallState (cs, f_def, args, mem, t)
    252 
    253       | RTLabs.St_tailcall_ptr (rs, args, sg) ->
    254         let addr = get_local_valuel lenv rs in
    255         let f_def = Mem.find_fun_def mem addr in
    256         let args = get_arg_valuesl lenv args in
     262        CallState (sfrs, f_def, args, mem, trace)
     263
     264      | RTLabs.St_tailcall_ptr (r, args, sg) ->
     265        let addr = get_local_value lenv r in
     266        let f_def = Mem.find_fun_def mem (address_of_value addr) in
     267        let args = get_arg_values lenv args in
    257268        (* No need to save the stack frame. But free the stack. *)
    258269        let mem = Mem.free mem sp in
    259         CallState (cs, f_def, args, mem, t)
     270        CallState (sfrs, f_def, args, mem, trace)
    260271
    261272      | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
    262273        let v = eval_cst mem sp cst in
    263         branch_state cs c sp lbl_true lbl_false lenv mem t v
    264 
    265       | RTLabs.St_cond1 (op1, srcrs, lbl_true, lbl_false) ->
    266         let v = eval_op1 op1 (get_local_valuel lenv srcrs) in
    267         branch_state cs c sp lbl_true lbl_false lenv mem t v
    268 
    269       | RTLabs.St_cond2 (op2, srcrs1, srcrs2, lbl_true, lbl_false) ->
     274        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
     275
     276      | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
     277        let v = eval_op1 op1 (get_local_value lenv srcr) in
     278        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
     279
     280      | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
    270281        let v =
    271282          eval_op2 op2
    272             (get_local_valuel lenv srcrs1)
    273             (get_local_valuel lenv srcrs2) in
    274         branch_state cs c sp lbl_true lbl_false lenv mem t v
    275 
    276       | RTLabs.St_jumptable (r, table) -> assert false (* TODO *)
     283            (get_local_value lenv srcr1)
     284            (get_local_value lenv srcr2) in
     285        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
     286
     287      | RTLabs.St_jumptable (r, table) -> assert false (* TODO: jumptable *)
    277288      (*
    278289        let i = match get_local_value lenv r with
     
    282293        (try
    283294        let next_lbl = List.nth table i in
    284         State (cs, c, sp, next_lbl, lenv, mem, t)
     295        State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
    285296        with
    286297        | Failure "nth" | Invalid_argument "List.nth" ->
     
    288299      *)
    289300
    290       | RTLabs.St_return rs ->
    291         let v = get_local_valuel lenv rs in
     301      | RTLabs.St_return r ->
     302        let v = get_local_value lenv r in
    292303        let mem = Mem.free mem sp in
    293         ReturnState (cs, v, mem, t)
    294 
    295 
    296 let get_int () =
    297   try Val.of_int (int_of_string (read_line ()))
    298   with Failure "int_of_string" -> error "Failed to scan an integer."
    299 let get_float () =
    300   try Val.of_float (float_of_string (read_line ()))
    301   with Failure "float_of_string" -> error "Failed to scan a float."
    302 
    303 let interpret_external
    304     (mem  : memory)
    305     (def  : AST.external_function)
    306     (args : Val.t list) :
    307     memory * Val.t =
    308   match def.AST.ef_tag, args with
    309     | s, _ when s = Primitive.scan_int ->
    310       (mem, get_int ())
    311     | "scan_float", _ ->
    312       (mem, get_float ())
    313     | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
    314       Printf.printf "%d" (Val.to_int v) ;
    315       (mem, Val.zero)
    316     | "print_float", v :: _ when Val.is_float v ->
    317       Printf.printf "%f" (Val.to_float v) ;
    318       (mem, Val.zero)
    319     | "print_ptr", v :: _ when Val.is_pointer v ->
    320       let (b, off) = Val.to_pointer v in
    321       Printf.printf "block: %s, offset: %s"
    322         (Val.Block.to_string b) (Val.Offset.to_string off) ;
    323       (mem, Val.zero)
    324     | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
    325       Printf.printf "%d\n" (Val.to_int v) ;
    326       (mem, Val.zero)
    327     | "print_floatln", v :: _ when Val.is_float v ->
    328       Printf.printf "%f" (Val.to_float v) ;
    329       (mem, Val.zero)
    330     | "print_ptrln", v :: _ when Val.is_pointer v ->
    331       let (b, off) = Val.to_pointer v in
    332       Printf.printf "block: %s, offset: %s\n"
    333         (Val.Block.to_string b) (Val.Offset.to_string off) ;
    334       (mem, Val.zero)
    335     | s, v :: _ when s = Primitive.alloc ->
    336       let (mem, ptr) = Mem.alloc mem (Val.to_int v) in
    337       (mem, ptr)
    338     | s, v1 :: v2 :: _ when s = Primitive.modulo ->
    339       (mem, Val.modulo v1 v2)
    340 
    341     (* The other cases are either a type error (only integers and pointers
    342        may not be differenciated during type checking) or an unknown
    343        function. *)
    344     | "print_int", _ | "print_intln", _ ->
    345       error "Illegal cast from pointer to integer."
    346     | "print_ptr", _ | "print_ptrln", _ ->
    347       error "Illegal cast from integer to pointer."
    348     | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
    349 
     304        ReturnState (sfrs, v, mem, trace)
     305
     306
     307module InterpretExternal = Primitive.Interpret (Mem)
     308
     309let interpret_external mem f args = match InterpretExternal.t mem f args with
     310  | (mem', InterpretExternal.V v) -> (mem', v)
     311  | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr)
    350312
    351313let init_locals
    352     (locals : Register.t list list)
    353     (params : Register.t list list)
     314    (locals : Register.t list)
     315    (params : Register.t list)
    354316    (args   : Val.t list) :
    355317    local_env =
    356   let f lenv rs = adds rs Val.undef lenv in
     318  let f lenv r = Register.Map.add r Val.undef lenv in
    357319  let lenv = List.fold_left f Register.Map.empty locals in
    358   let f lenv rs v = adds rs v lenv in
     320  let f lenv r v = Register.Map.add r v lenv in
    359321  List.fold_left2 f lenv params args
    360322
    361323let state_after_call
    362     (cs    : stack_frame list)
     324    (sfrs  : stack_frame list)
    363325    (f_def : RTLabs.function_def)
    364326    (args  : Val.t list)
    365327    (mem   : memory)
    366     (t    : CostLabel.t list) :
     328    (trace : CostLabel.t list) :
    367329    state =
    368330  match f_def with
    369331    | RTLabs.F_int def ->
    370332      let (mem', sp) = Mem.alloc mem def.RTLabs.f_stacksize in
    371       State (cs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry,
     333      State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry,
    372334             init_locals def.RTLabs.f_locals def.RTLabs.f_params args,
    373              mem', t)
     335             mem', trace)
    374336    | RTLabs.F_ext def ->
    375       let (mem', v) = interpret_external mem def args in
    376       ReturnState (cs, v, mem', t)
     337      let (mem', v) = interpret_external mem def.AST.ef_tag args in
     338      ReturnState (sfrs, v, mem', trace)
    377339
    378340
    379341let state_after_return
    380342    (sf      : stack_frame)
    381     (cs      : stack_frame list)
     343    (sfrs    : stack_frame list)
    382344    (ret_val : Val.t)
    383345    (mem     : memory)
    384     (t       : CostLabel.t list) :
     346    (trace   : CostLabel.t list) :
    385347    state =
    386   let lenv = adds sf.ret_regs ret_val sf.lenv in
    387   State (cs, sf.graph, sf.sp, sf.pc, lenv, mem, t)
     348  let lenv = Register.Map.add sf.ret_reg ret_val sf.lenv in
     349  State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace)
    388350
    389351
    390352let small_step (st : state) : state = match st with
    391   | State (cs, graph, sp, pc, lenv, mem, t) ->
     353  | State (sfrs, graph, sp, pc, lenv, mem, trace) ->
    392354    let stmt = Label.Map.find pc graph in
    393     interpret_statement cs graph sp lenv mem stmt t
    394   | CallState (cs, f_def, args, mem, t) ->
    395     state_after_call cs f_def args mem t
    396   | ReturnState ([], ret_val, mem, t) ->
     355    interpret_statement sfrs graph sp lenv mem stmt trace
     356  | CallState (sfrs, f_def, args, mem, trace) ->
     357    state_after_call sfrs f_def args mem trace
     358  | ReturnState ([], ret_val, mem, trace) ->
    397359    assert false (* End of execution; handled in iter_small_step. *)
    398   | ReturnState (sf :: cs, ret_val, mem, t) ->
    399     state_after_return sf cs ret_val mem t
     360  | ReturnState (sf :: sfrs, ret_val, mem, trace) ->
     361    state_after_return sf sfrs ret_val mem trace
    400362
    401363
     
    404366  else IntValue.Int8.zero
    405367
    406 let rec iter_small_step print_result st = match small_step st with
    407 (*
    408   (* <DEBUG> *)
    409   | ReturnState ([], v, mem, t) ->
    410     Mem.print mem ;
    411     Printf.printf "Return: %s\n%!" (Val.to_string v) ;
    412     List.rev t
    413   | CallState (_, _, _, mem, _)
    414   | ReturnState (_, _, mem, _)
    415   | State (_, _, _, _, _, mem, _) as st' -> Mem.print mem ; iter_small_step st'
    416   (* </DEBUG> *)
    417 *)
    418   | ReturnState ([], v, mem, t) ->
    419     let (res, cost_labels) as trace = (compute_result v, List.rev t) in
    420     if print_result then
    421       Printf.printf "RTLabs: %s\n%!" (IntValue.Int8.to_string res) ;
    422     trace
    423   | st' -> iter_small_step print_result st'
     368let rec iter_small_step debug st =
     369  if debug then print_state st ;
     370  match small_step st with
     371    | ReturnState ([], v, mem, trace) -> (compute_result v, List.rev trace)
     372    | st' -> iter_small_step debug st'
    424373
    425374
     
    441390(* Interpret the program only if it has a main. *)
    442391
    443 let interpret print_result p = match p.RTLabs.main with
    444   | None -> (IntValue.Int8.zero, [])
    445   | Some main ->
    446     let mem = init_mem p in
    447     let main_def = find_function mem main in
    448     let st = CallState ([], main_def, [], mem, []) in
    449     iter_small_step print_result st
     392let interpret debug p =
     393  if debug then Printf.printf "*** RTLabs ***\n\n%!" ;
     394  match p.RTLabs.main with
     395    | None -> (IntValue.Int8.zero, [])
     396    | Some main ->
     397      let mem = init_mem p in
     398      let main_def = find_function mem main in
     399      let st = CallState ([], main_def, [], mem, []) in
     400      iter_small_step debug st
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml

    r486 r740  
    1212
    1313
    14 let print_reg_list rl =
    15   Printf.sprintf "[%s]" (MiscPottier.string_of_list " ; " Register.print rl)
     14let print_reg = Register.print
    1615
    1716let rec print_args args =
    18   Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg_list args)
    19 
    20 let print_result rl = print_reg_list rl
    21 
    22 let print_params rl =
    23   Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_reg_list rl)
    24 
    25 let print_locals rl =
    26   Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_reg_list rl)
    27 
    28 
    29 let print_memory_q = Memory.string_of_memory_q
     17  Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg args)
     18
     19let print_result r = print_reg r
     20
     21let print_params r =
     22  Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_reg r)
     23
     24let print_locals r =
     25  Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_reg r)
    3026
    3127
     
    5955  | AST.Op_floatofint -> "floatofint"
    6056  | AST.Op_floatofintu -> "floatofintu"
    61   | AST.Op_id -> "mov"
     57  | AST.Op_id -> "id"
    6258  | AST.Op_ptrofint -> "ptrofint"
    6359  | AST.Op_intofptr -> "intofptr"
     
    107103  | RTLabs.St_cost (cost_lbl, lbl) ->
    108104      Printf.sprintf "emit %s --> %s" cost_lbl lbl
    109   | RTLabs.St_cst (dests, cst, lbl) ->
     105  | RTLabs.St_cst (destr, cst, lbl) ->
    110106      Printf.sprintf "imm %s, %s --> %s"
    111         (print_reg_list dests)
     107        (print_reg destr)
    112108        (print_cst cst)
    113109        lbl
    114   | RTLabs.St_op1 (op1, dests, srcs, lbl) ->
     110  | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
    115111      Printf.sprintf "%s %s, %s --> %s"
    116112        (print_op1 op1)
    117         (print_reg_list dests)
    118         (print_reg_list srcs)
    119         lbl
    120   | RTLabs.St_op2 (op2, dests, srcs1, srcs2, lbl) ->
     113        (print_reg destr)
     114        (print_reg srcr)
     115        lbl
     116  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
    121117      Printf.sprintf "%s %s, %s, %s --> %s"
    122118        (print_op2 op2)
    123         (print_reg_list dests)
    124         (print_reg_list srcs1)
    125         (print_reg_list srcs2)
    126         lbl
    127   | RTLabs.St_load (chunk, mode, args, dests, lbl) ->
     119        (print_reg destr)
     120        (print_reg srcr1)
     121        (print_reg srcr2)
     122        lbl
     123  | RTLabs.St_load (q, mode, args, destr, lbl) ->
    128124      Printf.sprintf "load %s, %s, %s, %s --> %s"
    129         (print_memory_q chunk)
     125        (Memory.string_of_quantity q)
    130126        (print_addressing mode)
    131127        (print_args args)
    132         (print_reg_list dests)
    133         lbl
    134   | RTLabs.St_store (chunk, mode, args, srcs, lbl) ->
     128        (print_reg destr)
     129        lbl
     130  | RTLabs.St_store (q, mode, args, srcr, lbl) ->
    135131      Printf.sprintf "store %s, %s, %s, %s --> %s"
    136         (print_memory_q chunk)
     132        (Memory.string_of_quantity q)
    137133        (print_addressing mode)
    138134        (print_args args)
    139         (print_reg_list srcs)
     135        (print_reg srcr)
    140136        lbl
    141137  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
     
    143139        f
    144140        (print_params args)
    145         (print_reg_list res)
     141        (print_reg res)
    146142        (Primitive.print_sig sg)
    147143        lbl
    148144  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    149145      Printf.sprintf "call_ptr %s, %s, %s: %s --> %s"
    150         (print_reg_list f)
    151         (print_params args)
    152         (print_reg_list res)
     146        (print_reg f)
     147        (print_params args)
     148        (print_reg res)
    153149        (Primitive.print_sig sg)
    154150        lbl
     
    160156  | RTLabs.St_tailcall_ptr (f, args, sg) ->
    161157      Printf.sprintf "tailcall_ptr \"%s\", %s: %s"
    162         (print_reg_list f)
     158        (print_reg f)
    163159        (print_params args)
    164160        (Primitive.print_sig sg)
     
    168164        lbl_true
    169165        lbl_false
    170   | RTLabs.St_cond1 (op1, srcs, lbl_true, lbl_false) ->
     166  | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
    171167      Printf.sprintf "%s %s --> %s, %s"
    172168        (print_op1 op1)
    173         (print_reg_list srcs)
     169        (print_reg srcr)
    174170        lbl_true
    175171        lbl_false
    176   | RTLabs.St_cond2 (op2, srcs1, srcs2, lbl_true, lbl_false) ->
     172  | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
    177173      Printf.sprintf "%s %s, %s --> %s, %s"
    178174        (print_op2 op2)
    179         (print_reg_list srcs1)
    180         (print_reg_list srcs2)
     175        (print_reg srcr1)
     176        (print_reg srcr2)
    181177        lbl_true
    182178        lbl_false
    183   | RTLabs.St_jumptable (rs, tbl) ->
     179  | RTLabs.St_jumptable (r, tbl) ->
    184180      Printf.sprintf "j_tbl %s --> %s"
    185         (print_reg_list rs)
     181        (print_reg r)
    186182        (print_table tbl)
    187   | RTLabs.St_return rs -> Printf.sprintf "return %s" (print_reg_list rs)
     183  | RTLabs.St_return r -> Printf.sprintf "return %s" (print_reg r)
    188184
    189185
     
    201197
    202198  Printf.sprintf
    203     "%s\"%s\"%s: %s\n%slocals: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"
     199    "%s\"%s\"%s: %s\n%slocals: %s\n%spointers: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"
    204200    (n_spaces n)
    205201    f
     
    208204    (n_spaces (n+2))
    209205    (print_locals def.RTLabs.f_locals)
     206    (n_spaces (n+2))
     207    (print_locals def.RTLabs.f_ptrs)
    210208    (n_spaces (n+2))
    211209    (print_result def.RTLabs.f_result)
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.mli

    r486 r740  
    22(** This module provides a function to print [RTLabs] programs. *)
    33
     4val print_statement : RTLabs.statement -> string
     5
    46val print_program : RTLabs.program -> string
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

    r486 r740  
    2828    (def, r :: res)
    2929
    30 let rtl_args regs_list = List.flatten regs_list
    31 
    3230let addr_regs regs = match regs with
    3331  | r1 :: r2 :: _ -> (r1, r2)
    3432  | _ -> error "Function pointer is not an address."
     33
     34
     35(* Local environments associate one (in case of an integer) or two (in case of a
     36   pointer) RTL pseudo-registers to one RTLabs pseudo-register. *)
     37
     38type reg_type =
     39  | Int of Register.t
     40  | Ptr of Register.t * Register.t
     41
     42type local_env = reg_type Register.Map.t
     43
     44let initialize_local_env runiverse ptrs registers =
     45  let f lenv r =
     46    let rt =
     47      if List.mem r ptrs then Ptr (r, Register.fresh runiverse)
     48      else Int r in
     49    Register.Map.add r rt lenv in
     50  List.fold_left f Register.Map.empty registers
     51
     52let filter_and_to_list_local_env lenv registers =
     53  let f l r =
     54    l @ (match Register.Map.find r lenv with
     55      | Int r -> [r]
     56      | Ptr (r1, r2) -> [r1 ; r2]) in
     57  List.fold_left f [] registers
     58
     59let list_of_reg_type = function
     60  | Int r -> [r]
     61  | Ptr (r1, r2) -> [r1 ; r2]
     62
     63let find_and_list r lenv = list_of_reg_type (Register.Map.find r lenv)
     64
     65let find_and_list_args args lenv =
     66  List.map (fun r -> find_and_list r lenv) args
     67
     68let find_and_addr r lenv = match find_and_list r lenv with
     69  | r1 :: r2 :: _ -> (r1, r2)
     70  | _ -> assert false (* do not use on these arguments *)
     71
     72let rtl_args regs_list lenv = List.flatten (find_and_list_args regs_list lenv)
     73   
    3574
    3675
     
    112151      [RTL.St_stackaddr (r1, r2, start_lbl) ;
    113152       RTL.St_int (tmpr, off, start_lbl) ;
    114        RTL.St_op2 (I8051.Add, r2, r2, tmpr, start_lbl) ;
     153       RTL.St_op2 (I8051.Add, r1, r1, tmpr, start_lbl) ;
    115154       RTL.St_int (tmpr, 0, start_lbl) ;
    116        RTL.St_op2 (I8051.Addc, r1, r1, tmpr, start_lbl)]
     155       RTL.St_op2 (I8051.Addc, r2, r2, tmpr, start_lbl)]
    117156      start_lbl dest_lbl def
    118157
     
    128167    | AST.Op_cast8unsigned, _, _ | AST.Op_cast8signed, _, _
    129168    | AST.Op_cast16unsigned, _, _ | AST.Op_cast16signed, _, _ ->
    130       def
     169      translate_move destrs srcrs start_lbl dest_lbl def
    131170
    132171    | AST.Op_negint, [destr], [srcr] ->
     
    146185    | AST.Op_ptrofint, [destr1 ; destr2], [srcr] ->
    147186      adds_graph
    148         [RTL.St_move (destr2, srcr, dest_lbl) ;
    149          RTL.St_int (destr1, 0, start_lbl)]
    150         start_lbl dest_lbl def
    151 
    152     | AST.Op_intofptr, [destr], [_ ; srcr] ->
     187        [RTL.St_move (destr1, srcr, dest_lbl) ;
     188         RTL.St_int (destr2, 0, start_lbl)]
     189        start_lbl dest_lbl def
     190
     191    | AST.Op_intofptr, [destr], [srcr ; _] ->
    153192      add_graph start_lbl (RTL.St_move (destr, srcr, dest_lbl)) def
    154193
     
    230269      error_float ()
    231270
    232     | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] ->
     271    | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2]
     272    | AST.Op_addp, [destr1 ; destr2], [srcr2], [srcr11 ; srcr12] ->
    233273      let (def, tmpr1) = fresh_reg def in
    234274      let (def, tmpr2) = fresh_reg def in
    235275      adds_graph
    236         [RTL.St_op2 (I8051.Add, tmpr2, srcr12, srcr2, start_lbl) ;
    237          RTL.St_int (tmpr1, 0, start_lbl) ;
    238          RTL.St_op2 (I8051.Addc, destr1, tmpr1, srcr11, start_lbl) ;
    239          RTL.St_move (destr2, tmpr2, start_lbl)]
    240         start_lbl dest_lbl def
    241 
    242     | AST.Op_subp, [destr], [_ ; srcr1], [_ ; srcr2] ->
     276        [RTL.St_op2 (I8051.Add, tmpr1, srcr11, srcr2, start_lbl) ;
     277         RTL.St_int (tmpr2, 0, start_lbl) ;
     278         RTL.St_op2 (I8051.Addc, destr2, tmpr2, srcr12, start_lbl) ;
     279         RTL.St_move (destr1, tmpr1, start_lbl)]
     280        start_lbl dest_lbl def
     281
     282    | AST.Op_subp, [destr], [srcr1 ; _], [srcr2 ; _] ->
    243283      let (def, tmpr1) = fresh_reg def in
    244284      let (def, tmpr2) = fresh_reg def in
     
    251291
    252292    | AST.Op_subp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] ->
    253       let (def, tmpr1) = fresh_reg def in
    254       let (def, tmpr2) = fresh_reg def in
    255       let (def, tmpr3) = fresh_reg def in
    256293      adds_graph
    257294        [RTL.St_clear_carry start_lbl ;
    258          RTL.St_op2 (I8051.Sub, destr2, srcr12, srcr2, start_lbl) ;
    259          RTL.St_int (destr1, 0, start_lbl) ;
    260          RTL.St_op2 (I8051.Sub, destr1, srcr11, destr1, start_lbl)]
     295         RTL.St_op2 (I8051.Sub, destr1, srcr11, srcr2, start_lbl) ;
     296         RTL.St_int (destr2, 0, start_lbl) ;
     297         RTL.St_op2 (I8051.Sub, destr2, srcr12, destr2, start_lbl)]
    261298        start_lbl dest_lbl def
    262299
     
    282319
    283320    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
    284       translate_op2 (AST.Op_cmp AST.Cmp_lt)
     321      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
    285322        destrs srcrs2 srcrs1 start_lbl dest_lbl def
    286323
     
    322359      let (def, tmpr2) = fresh_reg def in
    323360      add_translates
    324         [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr11] [srcr21] ;
    325          translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr11] [srcr21] ;
    326          translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr12] [srcr22] ;
     361        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
     362         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
     363         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
    327364         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
    328365         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
     
    366403
    367404  | AST.Cst_addrsymbol x ->
    368     let (def, rs) = fresh_regs def 2 in
    369     let r1 = List.nth rs 0 in
    370     let r2 = List.nth rs 1 in
     405    let (def, r1) = fresh_reg def in
     406    let (def, r2) = fresh_reg def in
    371407    let lbl = fresh_label def in
    372408    let def = add_graph start_lbl (RTL.St_addr (r1, r2, x, lbl)) def in
     
    417453    | AST.Op_id, _ -> assert false (* wrong number of arguments *)
    418454
    419     | _, _ ->
     455    | _, srcrs ->
    420456      let (def, destrs) = fresh_regs def (size_of_op1_ret op1) in
    421457      let lbl = fresh_label def in
     
    443479  | AST.Op_addp -> 2
    444480  | AST.Op_subp ->
    445     if n = 1 (* sub between pointer and integer *) then 2
    446     else (* sub between two pointers *) 1
     481    if n = 4 (* sub between two pointers, result is an integer *) then 1
     482    else (* sub between a pointer and an integer, result is a pointer *) 2
    447483  | AST.Op_addf
    448484  | AST.Op_subf
     
    463499
    464500    | _, _, _ ->
    465       let n = List.length srcrs2 in
     501      let n = (List.length srcrs1) + (List.length srcrs2) in
    466502      let (def, destrs) = fresh_regs def (size_of_op2_ret n op2) in
    467503      let lbl = fresh_label def in
     
    513549
    514550
    515 let translate_load chunk mode args destrs start_lbl dest_lbl def =
    516   match chunk, destrs with
    517 
    518     | Memory.MQ_pointer, [destr1 ; destr2] ->
     551let translate_load q mode args destrs start_lbl dest_lbl def =
     552  match q, destrs with
     553
     554    | Memory.QInt 1, [destr] ->
     555      let (def, addr1) = fresh_reg def in
     556      let (def, addr2) = fresh_reg def in
     557      add_translates
     558        [addressing_pointer mode args addr1 addr2 ;
     559         adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]]
     560        start_lbl dest_lbl def
     561
     562    | Memory.QPtr, [destr1 ; destr2] ->
    519563      let (def, addr1) = fresh_reg def in
    520564      let (def, addr2) = fresh_reg def in
     
    523567      add_translates
    524568        [addressing_pointer mode args addr1 addr2 ;
    525          adds_graph [RTL.St_load (destr2, addr1, addr2, start_lbl) ;
     569         adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl) ;
    526570                     RTL.St_int (tmpr, 1, start_lbl)] ;
    527571         translate_op2 AST.Op_addp addr addr [tmpr] ;
    528          adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl)]]
    529         start_lbl dest_lbl def
    530 
    531     | Memory.MQ_int8signed, [destr]
    532     | Memory.MQ_int8unsigned, [destr] ->
     572         adds_graph [RTL.St_load (destr2, addr1, addr2, start_lbl)]]
     573        start_lbl dest_lbl def
     574
     575    | _ -> error "Size error in load."
     576
     577
     578let translate_store q mode args srcrs start_lbl dest_lbl def =
     579  match q, srcrs with
     580
     581    | Memory.QInt 1, [srcr] ->
    533582      let (def, addr1) = fresh_reg def in
    534583      let (def, addr2) = fresh_reg def in
    535584      add_translates
    536585        [addressing_pointer mode args addr1 addr2 ;
    537          adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]]
    538         start_lbl dest_lbl def
    539 
    540     | Memory.MQ_int16signed, _ | Memory.MQ_int16unsigned, _
    541     | Memory.MQ_int32, _ ->
    542       error_int ()
    543 
    544     | Memory.MQ_float32, _ | Memory.MQ_float64, _ ->
    545       error_float ()
    546 
    547     | _ -> assert false (* wrong number of argument *)
    548 
    549 
    550 let translate_store chunk mode args srcrs start_lbl dest_lbl def =
    551   match chunk, srcrs with
    552 
    553     | Memory.MQ_pointer, [srcr1 ; srcr2] ->
     586         adds_graph [RTL.St_store (addr1, addr2, srcr, dest_lbl)]]
     587        start_lbl dest_lbl def
     588
     589    | Memory.QPtr, [srcr1 ; srcr2] ->
    554590      let (def, addr1) = fresh_reg def in
    555591      let (def, addr2) = fresh_reg def in
     
    558594      add_translates
    559595        [addressing_pointer mode args addr1 addr2 ;
    560          adds_graph [RTL.St_store (addr1, addr2, srcr2, start_lbl) ;
     596         adds_graph [RTL.St_store (addr1, addr2, srcr1, start_lbl) ;
    561597                     RTL.St_int (tmpr, 1, start_lbl)] ;
    562598         translate_op2 AST.Op_addp addr addr [tmpr] ;
    563          adds_graph [RTL.St_store (addr1, addr2, srcr1, dest_lbl)]]
    564         start_lbl dest_lbl def
    565 
    566     | Memory.MQ_int8signed, [srcr]
    567     | Memory.MQ_int8unsigned, [srcr] ->
    568       let (def, addr1) = fresh_reg def in
    569       let (def, addr2) = fresh_reg def in
    570       add_translates
    571         [addressing_pointer mode args addr1 addr2 ;
    572          adds_graph [RTL.St_store (addr1, addr2, srcr, dest_lbl)]]
    573         start_lbl dest_lbl def
    574 
    575     | Memory.MQ_int16signed, _ | Memory.MQ_int16unsigned, _
    576     | Memory.MQ_int32, _ ->
    577       error_int ()
    578 
    579     | Memory.MQ_float32, _ | Memory.MQ_float64, _ ->
    580       error_float ()
    581 
    582     | _ -> assert false (* wrong number of argument *)
    583 
    584 
    585 let translate_stmt lbl stmt def = match stmt with
     599         adds_graph [RTL.St_store (addr1, addr2, srcr2, dest_lbl)]]
     600        start_lbl dest_lbl def
     601
     602    | _ -> error "Size error in store."
     603
     604
     605let translate_stmt lenv lbl stmt def = match stmt with
    586606
    587607  | RTLabs.St_skip lbl' ->
     
    591611    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
    592612
    593   | RTLabs.St_cst (destrs, cst, lbl') ->
    594     translate_cst cst destrs lbl lbl' def
    595 
    596   | RTLabs.St_op1 (op1, destrs, srcrs, lbl') ->
    597     translate_op1 op1 destrs srcrs lbl lbl' def
    598 
    599   | RTLabs.St_op2 (op2, destrs, srcrs1, srcrs2, lbl') ->
    600     translate_op2 op2 destrs srcrs1 srcrs2 lbl lbl' def
    601 
    602   | RTLabs.St_load (chunk, mode, args, destrs, lbl') ->
    603     translate_load chunk mode args destrs lbl lbl' def
    604 
    605   | RTLabs.St_store (chunk, mode, args, srcrs, lbl') ->
    606     translate_store chunk mode args srcrs lbl lbl' def
    607 
    608   | RTLabs.St_call_id (f, args, retrs, _, lbl') ->
    609     add_graph lbl (RTL.St_call_id (f, rtl_args args, retrs, lbl')) def
    610 
    611   | RTLabs.St_call_ptr (f, args, retrs, _, lbl') ->
    612     let (f1, f2) = addr_regs f in
     613  | RTLabs.St_cst (destr, cst, lbl') ->
     614    translate_cst cst (find_and_list destr lenv) lbl lbl' def
     615
     616  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
     617    translate_op1 op1 (find_and_list destr lenv) (find_and_list srcr lenv)
     618      lbl lbl' def
     619
     620  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
     621    translate_op2 op2 (find_and_list destr lenv)
     622      (find_and_list srcr1 lenv) (find_and_list srcr2 lenv) lbl lbl' def
     623
     624  | RTLabs.St_load (q, mode, args, destr, lbl') ->
     625    translate_load q mode (find_and_list_args args lenv)
     626      (find_and_list destr lenv) lbl lbl' def
     627
     628  | RTLabs.St_store (q, mode, args, srcr, lbl') ->
     629    translate_store q mode (find_and_list_args args lenv)
     630      (find_and_list srcr lenv) lbl lbl' def
     631
     632  | RTLabs.St_call_id (f, args, retr, _, lbl') ->
     633    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
     634                                   find_and_list retr lenv, lbl')) def
     635
     636  | RTLabs.St_call_ptr (f, args, retr, _, lbl') ->
     637    let (f1, f2) = find_and_addr f lenv in
    613638    add_graph lbl
    614       (RTL.St_call_ptr (f1, f2, rtl_args args, retrs, lbl')) def
     639      (RTL.St_call_ptr
     640         (f1, f2, rtl_args args lenv, find_and_list retr lenv, lbl')) def
    615641
    616642  | RTLabs.St_tailcall_id (f, args, _) ->
    617     add_graph lbl (RTL.St_tailcall_id (f, rtl_args args)) def
     643    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
    618644
    619645  | RTLabs.St_tailcall_ptr (f, args, _) ->
    620     let (f1, f2) = addr_regs f in
    621     add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args)) def
     646    let (f1, f2) = find_and_addr f lenv in
     647    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
    622648
    623649  | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
    624650    translate_condcst cst lbl lbl_true lbl_false def
    625651
    626   | RTLabs.St_cond1 (op1, srcrs, lbl_true, lbl_false) ->
    627     translate_cond1 op1 srcrs lbl lbl_true lbl_false def
    628 
    629   | RTLabs.St_cond2 (op2, srcrs1, srcrs2, lbl_true, lbl_false) ->
    630     translate_cond2 op2 srcrs1 srcrs2 lbl lbl_true lbl_false def
     652  | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
     653    translate_cond1 op1 (find_and_list srcr lenv)
     654      lbl lbl_true lbl_false def
     655
     656  | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
     657    translate_cond2 op2 (find_and_list srcr1 lenv)
     658      (find_and_list srcr2 lenv) lbl lbl_true lbl_false def
    631659
    632660  | RTLabs.St_jumptable _ ->
    633661    error "Jump tables not supported yet."
    634662
    635   | RTLabs.St_return regs ->
    636     add_graph lbl (RTL.St_return regs) def
     663  | RTLabs.St_return r ->
     664    add_graph lbl (RTL.St_return (find_and_list r lenv)) def
    637665
    638666
    639667let translate_internal def =
    640   let set_of_list_list l =
    641     let l = List.flatten l in
    642     List.fold_left (fun res x -> Register.Set.add x res) Register.Set.empty l
    643   in
     668  let runiverse = def.RTLabs.f_runiverse in
     669  let lenv =
     670    initialize_local_env runiverse def.RTLabs.f_ptrs
     671      (def.RTLabs.f_params @ def.RTLabs.f_locals) in
     672  let result = find_and_list def.RTLabs.f_result lenv in
     673  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
     674  let params = filter_and_to_list_local_env lenv def.RTLabs.f_params in
     675  let locals = filter_and_to_list_local_env lenv def.RTLabs.f_locals in
     676  let locals = set_of_list locals in
    644677  let res =
    645678    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
    646       RTL.f_runiverse = def.RTLabs.f_runiverse ;
     679      RTL.f_runiverse = runiverse ;
    647680      RTL.f_sig       = def.RTLabs.f_sig ;
    648       RTL.f_result    = def.RTLabs.f_result ;
    649       RTL.f_params    = List.flatten def.RTLabs.f_params ;
    650       RTL.f_locals    = set_of_list_list def.RTLabs.f_locals ;
     681      RTL.f_result    = result ;
     682      RTL.f_params    = params ;
     683      RTL.f_locals    = locals ;
    651684      RTL.f_stacksize = def.RTLabs.f_stacksize ;
    652685      RTL.f_graph     = Label.Map.empty ;
    653686      RTL.f_entry     = def.RTLabs.f_entry ;
    654687      RTL.f_exit      = def.RTLabs.f_exit } in
    655   Label.Map.fold translate_stmt def.RTLabs.f_graph res
     688  Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res
    656689
    657690
Note: See TracChangeset for help on using the changeset viewer.