Ignore:
Timestamp:
May 19, 2011, 4:03:04 PM (10 years ago)
Author:
ayache
Message:

32 and 16 bits operations support in D2.2/8051

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

Legend:

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

    r740 r818  
    99   RTLabs is the last language of the frontend. It is intended to
    1010   ease retargetting. *)
    11 
    12 
    13 (* The following type represents the possible addresses to load from or store to
    14    memory. *)
    15 
    16 type addressing =
    17 
    18   (* Address is r1 + offset *)
    19   | Aindexed of AST.immediate
    20 
    21   (* Address is r1 + r2 *)
    22   | Aindexed2
    23 
    24   (* Address is symbol + offset *)
    25   | Aglobal of AST.ident * AST.immediate
    26 
    27   (* Address is symbol + offset + r1 *)
    28   | Abased of AST.ident * AST.immediate
    29 
    30   (* Address is stack_pointer + offset *)
    31   | Ainstack of AST.immediate
    3211
    3312
     
    5837
    5938  (* 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
     39     register containing the address, the destination register and the label
    6140     of the next statement. *)
    62   | St_load of Memory.quantity * addressing * Register.t list * Register.t *
    63                Label.t
     41  | St_load of AST.quantity * Register.t * Register.t * Label.t
    6442
    6543  (* 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
     44     register containing the address, the source register and the label of the
    6745     next statement. *)
    68   | St_store of Memory.quantity * addressing * Register.t list * Register.t *
    69                 Label.t
     46  | St_store of AST.quantity * Register.t * Register.t * Label.t
    7047
    7148  (* Call to a function given its name. Parameters are the name of the
     
    7350     register, the signature of the function and the label of the next
    7451     statement. *)
    75   | St_call_id of AST.ident * Register.t list * Register.t *
     52  | St_call_id of AST.ident * Register.t list * Register.t option *
    7653                  AST.signature * Label.t
    7754
     
    8360     differenciate the two to allow translation to a formalism with no
    8461     function pointer. *)
    85   | St_call_ptr of Register.t * Register.t list * Register.t *
     62  | St_call_ptr of Register.t * Register.t list * Register.t option *
    8663                   AST.signature * Label.t
    8764
     
    9774  | St_tailcall_ptr of Register.t * Register.t list * AST.signature
    9875
    99   (* Constant branch. Parameters are the constant, the label to go to when the
    100      constant evaluates to true (not 0), and the label to go to when the
    101      constant evaluates to false (0). *)
    102   | St_condcst of AST.cst * Label.t * Label.t
    103 
    104   (* Unary branch. Parameters are the operation, its argument, the
    105      label to go to when the operation on the argument evaluates to
    106      true (not 0), and the label to go to when the operation on the
    107      argument evaluates to false (0). *)
    108   | St_cond1 of AST.op1 * Register.t * Label.t * Label.t
    109 
    110   (* Binary branch. Parameters are the operation, its arguments, the
    111      label to go to when the operation on the arguments evaluates to
    112      true (not 0), and the label to go to when the operation on the
    113      arguments evaluates to false (0). *)
    114   | St_cond2 of AST.op2 * Register.t * Register.t * Label.t * Label.t
     76  (* Branch. Parameters are the register holding the value to branch on, the
     77     label to go to when the value evaluates to true (not 0), and the label
     78     to go to when the value evaluates to false (0). *)
     79  | St_cond of Register.t * Label.t * Label.t
    11580
    11681  (* Jump statement. Parameters are a register and a list of
     
    12085
    12186  (* Return statement. *)
    122   | St_return of Register.t
     87  | St_return of Register.t option
    12388
    12489
     
    12893    { f_luniverse : Label.Gen.universe ;
    12994      f_runiverse : Register.universe ;
    130       f_sig       : AST.signature ;
    131       f_result    : Register.t ;
    132       f_params    : Register.t list ;
    133       f_locals    : Register.t list ;
    134       f_ptrs      : Register.t list ;
    135       f_stacksize : int ;
     95      f_result    : (Register.t * AST.sig_type) option ;
     96      f_params    : (Register.t * AST.sig_type) list ;
     97      f_locals    : (Register.t * AST.sig_type) list ;
     98      f_stacksize : AST.abstract_size ;
    13699      f_graph     : graph ;
    137100      f_entry     : Label.t ;
     
    146109
    147110type program =
    148     { vars   : (AST.ident * int (* size *)) list ;
     111    { vars   : (AST.ident * AST.abstract_size) list ;
    149112      functs : (AST.ident * function_def) list ;
    150113      main   : AST.ident option }
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml

    r740 r818  
    1616
    1717
    18 (* Local environments. They associate a value to the registers of the function
    19    being executed. *)
    20 
    21 type local_env = Val.t Register.Map.t
    22 
    23 (* Call frames. The execution state has a call stack, each element of
    24    the stack being composed of the return registers to store the result
    25    of the callee, the graph, the stack pointer, the node and the local
    26    environment to resume the execution of the caller. *)
     18(* Local environments. They associate a value and a type to the registers of the
     19   function being executed. *)
     20
     21type local_env = (Val.t * AST.sig_type) Register.Map.t
     22
     23(* Call frames. The execution state has a call stack, each element of the stack
     24   being composed of the return registers to store the result of the callee, the
     25   graph, the stack pointer, the node, the local environment and the typing
     26   environments to resume the execution of the caller. *)
    2727
    2828type stack_frame =
    29     { ret_reg  : Register.t ;
     29    { ret_reg  : Register.t option ;
    3030      graph    : RTLabs.graph ;
    3131      sp       : Val.address ;
     
    4747
    4848let string_of_local_env lenv =
    49   let f x v s =
     49  let f x (v, _) s =
    5050    s ^
    5151      (if Val.eq v Val.undef then ""
     
    7878  Mem.find_fun_def mem addr
    7979
    80 let get_local_value (lenv : local_env) (r : Register.t) : Val.t =
    81   if Register.Map.mem r lenv then Register.Map.find r lenv
     80let get_local_env f lenv r =
     81  if Register.Map.mem r lenv then f (Register.Map.find r lenv)
    8282  else error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
    83 let get_arg_values lenv args = List.map (get_local_value lenv) args
    84 
    85 let adds rs vs lenv =
    86   let f lenv r v = Register.Map.add r v lenv in
     83
     84let get_value = get_local_env fst
     85let get_args lenv args = List.map (get_value lenv) args
     86
     87let get_type = get_local_env snd
     88
     89let update_local r v lenv =
     90  let f (_, t) = Register.Map.add r (v, t) lenv in
     91  get_local_env f lenv r
     92
     93let update_locals rs vs lenv =
     94  let f lenv r v = update_local r v lenv in
    8795  List.fold_left2 f lenv rs vs
    8896
     
    9199
    92100
    93 let eval_addressing
    94     (mem  : memory)
    95     (sp   : Val.address)
    96     (mode : RTLabs.addressing)
    97     (args : Val.t list) :
    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)
    105 
    106       | RTLabs.Aglobal (id, off), _ ->
    107         Val.add_address (Mem.find_global mem id) (Val.Offset.of_int off)
    108 
    109       | RTLabs.Abased (id, off), 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)
    113 
    114       | RTLabs.Ainstack off, _ ->
    115         Val.add_address sp (Val.Offset.of_int off)
    116 
    117       | _, _ -> error "Bad addressing mode."
    118 
    119 
    120 let eval_cst mem sp = function
    121   | AST.Cst_int i -> Val.of_int i
    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))
    126 
    127 let eval_op1 = function
    128   | AST.Op_cast8unsigned -> Val.cast8unsigned
    129   | AST.Op_cast8signed -> Val.cast8signed
    130   | AST.Op_cast16unsigned -> Val.cast16unsigned
    131   | AST.Op_cast16signed -> Val.cast16signed
    132   | AST.Op_negint -> Val.negint
    133   | AST.Op_notbool -> Val.notbool
    134   | AST.Op_notint -> Val.notint
    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 ()
    142   | AST.Op_id -> (fun (v : Val.t) -> v)
    143   | AST.Op_intofptr | AST.Op_ptrofint -> assert false (* TODO or not? *)
    144 
    145 let rec eval_op2 = function
    146   | AST.Op_add | AST.Op_addp -> Val.add
    147   | AST.Op_sub | AST.Op_subp -> Val.sub
    148   | AST.Op_mul -> Val.mul
    149   | AST.Op_div -> Val.div
    150   | AST.Op_divu -> Val.divu
    151   | AST.Op_mod -> Val.modulo
    152   | AST.Op_modu -> Val.modulou
    153   | AST.Op_and -> Val.and_op
    154   | AST.Op_or -> Val.or_op
    155   | AST.Op_xor -> Val.xor
    156   | AST.Op_shl -> Val.shl
    157   | AST.Op_shr -> Val.shr
    158   | AST.Op_shru -> Val.shru
    159   | AST.Op_cmp AST.Cmp_eq -> Val.cmp_eq
    160   | AST.Op_cmp AST.Cmp_ne -> Val.cmp_ne
    161   | AST.Op_cmp AST.Cmp_lt -> Val.cmp_lt
    162   | AST.Op_cmp AST.Cmp_le -> Val.cmp_le
    163   | AST.Op_cmp AST.Cmp_gt -> Val.cmp_gt
    164   | AST.Op_cmp AST.Cmp_ge -> Val.cmp_ge
    165   | AST.Op_cmpu AST.Cmp_eq -> Val.cmp_eq_u
    166   | AST.Op_cmpu AST.Cmp_ne -> Val.cmp_ne_u
    167   | AST.Op_cmpu AST.Cmp_lt -> Val.cmp_lt_u
    168   | AST.Op_cmpu AST.Cmp_le -> Val.cmp_le_u
    169   | AST.Op_cmpu AST.Cmp_gt -> Val.cmp_gt_u
    170   | AST.Op_cmpu AST.Cmp_ge -> Val.cmp_ge_u
    171   | 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 ()
     101module Eval = CminorInterpret.Eval_op (Mem)
     102
     103let concrete_stacksize = Eval.concrete_stacksize
     104
    177105
    178106(* Assign a value to some destinations registers. *)
    179107
    180108let assign_state sfrs graph sp lbl lenv mem trace destr v =
    181   let lenv = Register.Map.add destr v lenv in
     109  let lenv = update_local destr v lenv in
    182110  State (sfrs, graph, sp, lbl, lenv, mem, trace)
    183111
     
    205133    state = match stmt with
    206134
    207       | RTLabs.St_skip lbl -> State (sfrs, graph, sp, lbl, lenv, mem, trace)
     135      | RTLabs.St_skip lbl ->
     136        State (sfrs, graph, sp, lbl, lenv, mem, trace)
    208137
    209138      | RTLabs.St_cost (cost_lbl, lbl) ->
     
    211140
    212141      | RTLabs.St_cst (destr, cst, lbl) ->
    213         let v = eval_cst mem sp cst in
     142        let v = Eval.cst mem sp (get_type lenv destr) cst in
    214143        assign_state sfrs graph sp lbl lenv mem trace destr v
    215144
    216145      | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
    217         let v = eval_op1 op1 (get_local_value lenv srcr) in
     146        let v =
     147          Eval.op1 (get_type lenv destr) (get_type lenv srcr) op1
     148            (get_value lenv srcr) in
    218149        assign_state sfrs graph sp lbl lenv mem trace destr v
    219150
    220151      | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
    221152        let v =
    222           eval_op2 op2
    223             (get_local_value lenv srcr1)
    224             (get_local_value lenv srcr2) in
     153          Eval.op2
     154            (get_type lenv destr) (get_type lenv srcr1) (get_type lenv srcr2)
     155            op2
     156            (get_value lenv srcr1)
     157            (get_value lenv srcr2) in
    225158        assign_state sfrs graph sp lbl lenv mem trace destr v
    226159
    227       | RTLabs.St_load (q, mode, args, destr, lbl) ->
    228         let addr = eval_addressing mem sp mode (get_arg_values lenv args) in
     160      | RTLabs.St_load (q, addr, destr, lbl) ->
     161        let addr = address_of_value (get_value lenv addr) in
    229162        let v = Mem.loadq mem q addr in
    230163        assign_state sfrs graph sp lbl lenv mem trace destr v
    231164
    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
     165      | 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
    235168        let mem = Mem.storeq mem q addr v in
    236169        State (sfrs, graph, sp, lbl, lenv, mem, trace)
     
    238171      | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
    239172        let f_def = find_function mem f in
    240         let args = get_arg_values lenv args in
     173        let args = get_args lenv args in
    241174        (* Save the stack frame. *)
    242175        let sf =
     
    246179
    247180      | RTLabs.St_call_ptr (r, args, destr, sg, lbl) ->
    248         let addr = get_local_value lenv r in
     181        let addr = get_value lenv r in
    249182        let f_def = Mem.find_fun_def mem (address_of_value addr) in
    250         let args = get_arg_values lenv args in
     183        let args = get_args lenv args in
    251184        (* Save the stack frame. *)
    252185        let sf =
     
    257190      | RTLabs.St_tailcall_id (f, args, sg) ->
    258191        let f_def = find_function mem f in
    259         let args = get_arg_values lenv args in
     192        let args = get_args lenv args in
    260193        (* No need to save the stack frame. But free the stack. *)
    261194        let mem = Mem.free mem sp in
     
    263196
    264197      | RTLabs.St_tailcall_ptr (r, args, sg) ->
    265         let addr = get_local_value lenv r in
     198        let addr = get_value lenv r in
    266199        let f_def = Mem.find_fun_def mem (address_of_value addr) in
    267         let args = get_arg_values lenv args in
     200        let args = get_args lenv args in
    268201        (* No need to save the stack frame. But free the stack. *)
    269202        let mem = Mem.free mem sp in
    270203        CallState (sfrs, f_def, args, mem, trace)
    271204
    272       | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
    273         let v = eval_cst mem sp cst in
     205      | RTLabs.St_cond (srcr, lbl_true, lbl_false) ->
     206        let v = get_value lenv srcr in
    274207        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
    275208
     209(*
     210      | RTLabs.St_condcst (cst, t, lbl_true, lbl_false) ->
     211        let v = Eval.cst mem sp t cst in
     212        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
     213
    276214      | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
    277         let v = eval_op1 op1 (get_local_value lenv srcr) in
     215        let v =
     216          Eval.op1 (get_type lenv srcr) (get_type lenv srcr)
     217            op1 (get_value lenv srcr) in
    278218        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
    279219
    280220      | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
    281221        let v =
    282           eval_op2 op2
    283             (get_local_value lenv srcr1)
    284             (get_local_value lenv srcr2) in
     222          Eval.op2 op2
     223            (get_value lenv srcr1)
     224            (get_value lenv srcr2) in
    285225        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
     226*)
    286227
    287228      | RTLabs.St_jumptable (r, table) -> assert false (* TODO: jumptable *)
    288229      (*
    289         let i = match get_local_value lenv r with
     230        let i = match get_value lenv r with
    290231        | Val.Val_int i -> i
    291232        | Val.Val_ptr _ -> error "Illegal cast from pointer to integer."
     
    299240      *)
    300241
    301       | RTLabs.St_return r ->
    302         let v = get_local_value lenv r in
     242      | RTLabs.St_return None ->
     243        let mem = Mem.free mem sp in
     244        ReturnState (sfrs, Val.undef, mem, trace)
     245
     246      | RTLabs.St_return (Some r) ->
     247        let v = get_value lenv r in
    303248        let mem = Mem.free mem sp in
    304249        ReturnState (sfrs, v, mem, trace)
     
    308253
    309254let interpret_external mem f args = match InterpretExternal.t mem f args with
    310   | (mem', InterpretExternal.V v) -> (mem', v)
     255  | (mem', InterpretExternal.V vs) ->
     256    let v = if List.length vs = 0 then Val.undef else List.hd vs in
     257    (mem', v)
    311258  | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr)
    312259
     260
    313261let init_locals
    314     (locals : Register.t list)
    315     (params : Register.t list)
    316     (args   : Val.t list) :
     262    (locals           : (Register.t * AST.sig_type) list)
     263    (params           : (Register.t * AST.sig_type) list)
     264    (args             : Val.t list) :
    317265    local_env =
    318   let f lenv r = Register.Map.add r Val.undef lenv in
    319   let lenv = List.fold_left f Register.Map.empty locals in
    320   let f lenv r v = Register.Map.add r v lenv in
    321   List.fold_left2 f lenv params args
     266  let f_param lenv (r, t) v = Register.Map.add r (v, t) lenv in
     267  let f_local lenv (r, t) = Register.Map.add r (Val.undef, t) lenv in
     268  let lenv = List.fold_left2 f_param Register.Map.empty params args in
     269  List.fold_left f_local lenv locals
    322270
    323271let state_after_call
     
    330278  match f_def with
    331279    | RTLabs.F_int def ->
    332       let (mem', sp) = Mem.alloc mem def.RTLabs.f_stacksize in
    333       State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry,
    334              init_locals def.RTLabs.f_locals def.RTLabs.f_params args,
    335              mem', trace)
     280      let (mem', sp) =
     281        Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in
     282      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)
    336285    | RTLabs.F_ext def ->
    337286      let (mem', v) = interpret_external mem def.AST.ef_tag args in
     
    346295    (trace   : CostLabel.t list) :
    347296    state =
    348   let lenv = Register.Map.add sf.ret_reg ret_val sf.lenv in
     297  let lenv = match sf.ret_reg with
     298    | None -> sf.lenv
     299    | Some ret_reg -> update_local ret_reg ret_val sf.lenv in
    349300  State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace)
    350301
     
    363314
    364315let compute_result v =
    365   if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
    366   else IntValue.Int8.zero
     316  if Val.is_int v then IntValue.Int32.cast (Val.to_int_repr v)
     317  else IntValue.Int32.zero
    367318
    368319let rec iter_small_step debug st =
     320  let print_and_return_result (res, cost_labels) =
     321    if debug then Printf.printf "Result = %s\n%!"
     322      (IntValue.Int32.to_string res) ;
     323    (res, cost_labels) in
    369324  if debug then print_state st ;
    370325  match small_step st with
    371     | ReturnState ([], v, mem, trace) -> (compute_result v, List.rev trace)
     326    | ReturnState ([], v, mem, trace) ->
     327      print_and_return_result (compute_result v, List.rev trace)
    372328    | st' -> iter_small_step debug st'
    373329
    374330
    375331let add_global_vars =
    376   List.fold_left
    377     (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
     332  List.fold_left (fun mem (id, size) -> Mem.add_var mem id size None)
    378333
    379334let add_fun_defs =
     
    381336
    382337
    383 (* The memory is initialized by load the code into it, and by reserving space
     338(* The memory is initialized by loading the code into it, and by reserving space
    384339   for the global variables. *)
    385340
     
    391346
    392347let interpret debug p =
    393   if debug then Printf.printf "*** RTLabs ***\n\n%!" ;
     348  Printf.printf "*** RTLabs interpret ***\n%!" ;
    394349  match p.RTLabs.main with
    395     | None -> (IntValue.Int8.zero, [])
     350    | None -> (IntValue.Int32.zero, [])
    396351    | Some main ->
    397352      let mem = init_mem p in
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml

    r740 r818  
    33
    44
     5let rec print_size = function
     6  | AST.SQ q -> Memory.string_of_quantity q
     7  | AST.SProd l -> "struct {" ^ (print_size_list l) ^ "}"
     8  | AST.SSum l -> "union {" ^ (print_size_list l) ^ "}"
     9  | AST.SArray (i, se) ->
     10    (print_size se) ^ "[" ^ (string_of_int i) ^ "]"
     11and print_size_list l =
     12  MiscPottier.string_of_list ", " print_size l
     13
    514let print_global n (x, size) =
    6   Printf.sprintf "%s\"%s\" [%d]" (n_spaces n) x size
     15  Printf.sprintf "%s\"%s\" { %s }" (n_spaces n) x (print_size size)
    716
    817let print_globals n globs =
     
    1423let print_reg = Register.print
    1524
     25let print_oreg = function
     26  | None -> "_"
     27  | Some r -> print_reg r
     28
     29let print_decl (r, t) =
     30  (Primitive.print_type t) ^ " " ^ (Register.print r)
     31
    1632let rec print_args args =
    1733  Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg args)
    1834
    19 let print_result r = print_reg r
     35let print_result = function
     36  | None -> "_"
     37  | Some (r, t) -> (Primitive.print_type t) ^ " " ^ (Register.print r)
    2038
    2139let print_params r =
    22   Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_reg r)
     40  Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_decl r)
    2341
    2442let print_locals r =
    25   Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_reg r)
     43  Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_decl r)
    2644
    2745
     
    3452  | AST.Cmp_le -> "le"
    3553
     54let rec print_size = function
     55  | AST.SQ q -> Memory.string_of_quantity q
     56  | AST.SProd l -> "struct {" ^ (print_size_list l) ^ "}"
     57  | AST.SSum l -> "union {" ^ (print_size_list l) ^ "}"
     58  | AST.SArray (i, se) ->
     59    (print_size se) ^ "[" ^ (string_of_int i) ^ "]"
     60and print_size_list l =
     61  MiscPottier.string_of_list ", " print_size l
     62
     63let print_stacksize = print_size
     64
     65let print_offset (size, depth) =
     66  (print_size size) ^ ", " ^ (string_of_int depth)
     67
     68let print_sizeof = print_size
     69
    3670let print_cst = function
    3771  | AST.Cst_int i -> Printf.sprintf "imm_int %d" i
    3872  | AST.Cst_float f -> Printf.sprintf "imm_float %f" f
    3973  | AST.Cst_addrsymbol id -> Printf.sprintf "imm_addr \"%s\"" id
    40   | AST.Cst_stackoffset off -> Printf.sprintf "imm_addr %d(STACK)" off
     74  | AST.Cst_stack -> "imm_addr STACK"
     75  | AST.Cst_offset off -> Printf.sprintf "imm_offset { %s }" (print_offset off)
     76  | AST.Cst_sizeof t -> "imm_sizeof (" ^ (print_size t) ^ ")"
     77
     78let string_of_signedness = function
     79  | AST.Signed -> "s"
     80  | AST.Unsigned -> "u"
     81
     82let string_of_int_type (size, sign) =
     83  Printf.sprintf "%d%s" size (string_of_signedness sign)
    4184
    4285let print_op1 = function
    43   | AST.Op_cast8unsigned -> "cast8u"
    44   | AST.Op_cast8signed -> "cast8"
    45   | AST.Op_cast16unsigned -> "cast16u"
    46   | AST.Op_cast16signed -> "cast16"
     86  | AST.Op_cast (int_type, dest_size) ->
     87    Printf.sprintf "int%sto%d" (string_of_int_type int_type) dest_size
    4788  | AST.Op_negint -> "negint"
    4889  | AST.Op_notbool -> "notbool"
    4990  | AST.Op_notint -> "notint"
    50   | AST.Op_negf -> "negf"
    51   | AST.Op_absf -> "absf"
    52   | AST.Op_singleoffloat -> "singleoffloat"
    53   | AST.Op_intoffloat -> "intoffloat"
    54   | AST.Op_intuoffloat -> "intuoffloat"
    55   | AST.Op_floatofint -> "floatofint"
    56   | AST.Op_floatofintu -> "floatofintu"
    5791  | AST.Op_id -> "id"
    5892  | AST.Op_ptrofint -> "ptrofint"
     
    6498  | AST.Op_mul -> "mul"
    6599  | AST.Op_div -> "div"
    66   | AST.Op_divu -> "divu"
     100  | AST.Op_divu -> "/u"
    67101  | AST.Op_mod -> "mod"
    68102  | AST.Op_modu -> "modu"
     
    73107  | AST.Op_shr -> "shr"
    74108  | AST.Op_shru -> "shru"
    75   | AST.Op_addf -> "addf"
    76   | AST.Op_subf -> "subf"
    77   | AST.Op_mulf -> "mulf"
    78   | AST.Op_divf -> "divf"
    79109  | AST.Op_cmp cmp -> print_cmp cmp
    80   | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u"
    81   | AST.Op_cmpf cmp -> (print_cmp cmp) ^ "f"
    82110  | AST.Op_addp -> "addp"
    83111  | AST.Op_subp -> "subp"
     112  | AST.Op_subpp -> "subpp"
    84113  | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p"
    85 
    86 
     114  | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u"
     115
     116
     117(*
    87118let print_addressing = function
    88   | RTLabs.Aindexed off -> Printf.sprintf "%d" off
     119  | RTLabs.Aindexed off -> Printf.sprintf "{ %s }" (print_offset off)
    89120  | RTLabs.Aindexed2 -> "add"
    90   | RTLabs.Aglobal (id, off) -> Printf.sprintf "%d(\"%s\")" off id
    91   | RTLabs.Abased (id, off) -> Printf.sprintf "add, %d(\"%s\")" off id
    92   | RTLabs.Ainstack off -> Printf.sprintf "%d(STACK)" off
     121  | RTLabs.Aglobal (id, off) ->
     122    Printf.sprintf "{ %s }(\"%s\")" (print_offset off) id
     123  | RTLabs.Abased (id, off) ->
     124    Printf.sprintf "add, { %s }(\"%s\")" (print_offset off) id
     125  | RTLabs.Ainstack off -> Printf.sprintf "{ %s }(STACK)" (print_offset off)
     126*)
    93127
    94128
     
    121155        (print_reg srcr2)
    122156        lbl
    123   | RTLabs.St_load (q, mode, args, destr, lbl) ->
    124       Printf.sprintf "load %s, %s, %s, %s --> %s"
     157  | RTLabs.St_load (q, addr, destr, lbl) ->
     158      Printf.sprintf "load %s, %s, %s --> %s"
    125159        (Memory.string_of_quantity q)
    126         (print_addressing mode)
    127         (print_args args)
    128         (print_reg destr)
    129         lbl
    130   | RTLabs.St_store (q, mode, args, srcr, lbl) ->
    131       Printf.sprintf "store %s, %s, %s, %s --> %s"
     160        (print_reg addr)
     161        (print_reg destr)
     162        lbl
     163  | RTLabs.St_store (q, addr, srcr, lbl) ->
     164      Printf.sprintf "store %s, %s, %s --> %s"
    132165        (Memory.string_of_quantity q)
    133         (print_addressing mode)
    134         (print_args args)
     166        (print_reg addr)
    135167        (print_reg srcr)
    136168        lbl
     
    138170      Printf.sprintf "call \"%s\", %s, %s: %s --> %s"
    139171        f
    140         (print_params args)
    141         (print_reg res)
     172        (print_args args)
     173        (print_oreg res)
    142174        (Primitive.print_sig sg)
    143175        lbl
     
    145177      Printf.sprintf "call_ptr %s, %s, %s: %s --> %s"
    146178        (print_reg f)
    147         (print_params args)
    148         (print_reg res)
     179        (print_args args)
     180        (print_oreg res)
    149181        (Primitive.print_sig sg)
    150182        lbl
     
    152184      Printf.sprintf "tailcall \"%s\", %s: %s"
    153185        f
    154         (print_params args)
     186        (print_args args)
    155187        (Primitive.print_sig sg)
    156188  | RTLabs.St_tailcall_ptr (f, args, sg) ->
    157189      Printf.sprintf "tailcall_ptr \"%s\", %s: %s"
    158190        (print_reg f)
    159         (print_params args)
    160         (Primitive.print_sig sg)
    161   | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
    162       Printf.sprintf "%s --> %s, %s"
     191        (print_args args)
     192        (Primitive.print_sig sg)
     193  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
     194      Printf.sprintf "%s? --> %s, %s"
     195        (print_reg r)
     196        lbl_true
     197        lbl_false
     198(*
     199  | RTLabs.St_condcst (cst, t, lbl_true, lbl_false) ->
     200      Printf.sprintf "(%s) %s --> %s, %s"
     201        (Primitive.print_type t)
    163202        (print_cst cst)
    164203        lbl_true
     
    177216        lbl_true
    178217        lbl_false
     218*)
    179219  | RTLabs.St_jumptable (r, tbl) ->
    180220      Printf.sprintf "j_tbl %s --> %s"
    181221        (print_reg r)
    182222        (print_table tbl)
    183   | RTLabs.St_return r -> Printf.sprintf "return %s" (print_reg r)
     223  | RTLabs.St_return None -> Printf.sprintf "return"
     224  | RTLabs.St_return (Some r) -> Printf.sprintf "return %s" (print_reg r)
    184225
    185226
     
    197238
    198239  Printf.sprintf
    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"
     240    "%s\"%s\"%s\n%slocals: %s\n%sresult: %s\n%sstacksize: %s\n%sentry: %s\n%sexit: %s\n\n%s"
    200241    (n_spaces n)
    201242    f
    202243    (print_params def.RTLabs.f_params)
    203     (Primitive.print_sig def.RTLabs.f_sig)
    204244    (n_spaces (n+2))
    205245    (print_locals def.RTLabs.f_locals)
    206246    (n_spaces (n+2))
    207     (print_locals def.RTLabs.f_ptrs)
    208     (n_spaces (n+2))
    209247    (print_result def.RTLabs.f_result)
    210248    (n_spaces (n+2))
    211     def.RTLabs.f_stacksize
     249    (print_stacksize def.RTLabs.f_stacksize)
    212250    (n_spaces (n+2))
    213251    def.RTLabs.f_entry
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

    r740 r818  
    1010let error_float () = error "float not supported."
    1111let error_shift () = error "Shift operations not supported."
     12
    1213
    1314let add_graph lbl stmt def =
     
    3031let addr_regs regs = match regs with
    3132  | r1 :: r2 :: _ -> (r1, r2)
    32   | _ -> 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 
    38 type reg_type =
    39   | Int of Register.t
    40   | Ptr of Register.t * Register.t
    41 
    42 type local_env = reg_type Register.Map.t
    43 
    44 let 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
     33  | _ -> error "registers are not an address."
     34
     35let rec register_freshes runiverse n =
     36  if n <= 0 then []
     37  else (Register.fresh runiverse) :: (register_freshes runiverse (n-1))
     38
     39let choose_rest rest1 rest2 = match rest1, rest2 with
     40  | [], _ -> rest2
     41  | _, [] -> rest1
     42  | _ -> assert false (* do not use on these arguments *)
     43
     44let complete_regs def srcrs1 srcrs2 =
     45  let nb_added = (List.length srcrs1) - (List.length srcrs2) in
     46  let (def, added_regs) = fresh_regs def nb_added in
     47  if nb_added > 0 then (srcrs1, srcrs2 @ added_regs, added_regs)
     48  else (srcrs1 @ added_regs, srcrs2, added_regs)
     49
     50
     51let size_of_sig_type = function
     52  | AST.Sig_int (i, _) -> i / Driver.TargetArch.int_size
     53  | AST.Sig_float _ -> error_float ()
     54  | AST.Sig_offset -> Driver.TargetArch.int_size
     55  | AST.Sig_ptr -> Driver.TargetArch.ptr_size
     56
     57let concrete_size = Driver.RTLMemory.concrete_size
     58
     59let concrete_offset = Driver.RTLMemory.concrete_offset
     60
     61
     62(* Local environments *)
     63
     64type local_env = Register.t list Register.Map.t
     65
     66let mem_local_env = Register.Map.mem
     67let add_local_env = Register.Map.add
     68let find_local_env = Register.Map.find
     69
     70let initialize_local_env runiverse registers result =
     71  let registers =
     72    registers @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
     73  let f lenv (r, t) =
     74    let rs = register_freshes runiverse (size_of_sig_type t) in
     75    add_local_env r rs lenv in
    5076  List.fold_left f Register.Map.empty registers
    5177
    52 let 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 
    59 let list_of_reg_type = function
    60   | Int r -> [r]
    61   | Ptr (r1, r2) -> [r1 ; r2]
    62 
    63 let find_and_list r lenv = list_of_reg_type (Register.Map.find r lenv)
    64 
    65 let find_and_list_args args lenv =
    66   List.map (fun r -> find_and_list r lenv) args
    67 
    68 let find_and_addr r lenv = match find_and_list r lenv with
     78let map_list_local_env lenv regs =
     79  let f res r = res @ (find_local_env r lenv) in
     80  List.fold_left f [] regs
     81
     82let make_addr = function
    6983  | r1 :: r2 :: _ -> (r1, r2)
    7084  | _ -> assert false (* do not use on these arguments *)
    7185
    72 let rtl_args regs_list lenv = List.flatten (find_and_list_args regs_list lenv)
    73    
     86let find_and_addr r lenv = make_addr (find_local_env r lenv)
     87
     88let rtl_args regs_list lenv =
     89  List.flatten (List.map (fun r -> find_local_env r lenv) regs_list)
    7490
    7591
     
    8197  | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl)
    8298  | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl)
    83   | RTL.St_opaccs (opaccs, dstr, srcr1, srcr2, _) ->
    84     RTL.St_opaccs (opaccs, dstr, srcr1, srcr2, lbl)
     99  | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, _) ->
     100    RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl)
    85101  | RTL.St_op1 (op1, dstr, srcr, _) -> RTL.St_op1 (op1, dstr, srcr, lbl)
    86102  | RTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
    87103    RTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
    88104  | RTL.St_clear_carry _ -> RTL.St_clear_carry lbl
     105  | RTL.St_set_carry _ -> RTL.St_set_carry lbl
    89106  | RTL.St_load (dstrs, addr1, addr2, _) ->
    90107    RTL.St_load (dstrs, addr1, addr2, lbl)
     
    96113  | RTL.St_tailcall_id (f, args) -> RTL.St_tailcall_id (f, args)
    97114  | RTL.St_tailcall_ptr (f1, f2, args) -> RTL.St_tailcall_ptr (f1, f2, args)
    98   | RTL.St_condacc _ as inst -> inst
     115  | RTL.St_cond _ as inst -> inst
    99116  | RTL.St_return regs -> RTL.St_return regs
    100117
     
    103120
    104121let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with
    105   | [] -> def
     122  | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
    106123  | [stmt] ->
    107124    add_graph start_lbl (change_label dest_lbl stmt) def
     
    117134let rec add_translates translate_list start_lbl dest_lbl def =
    118135  match translate_list with
    119     | [] -> def
     136    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
    120137    | [trans] -> trans start_lbl dest_lbl def
    121138    | trans :: translate_list ->
     
    125142
    126143
    127 let rec translate_move destrs srcrs start_lbl dest_lbl def =
    128   match destrs, srcrs with
    129     | [], [] -> def
    130     | [destr], [srcr] ->
    131       add_graph start_lbl (RTL.St_move (destr, srcr, dest_lbl)) def
    132     | destr :: destrs, srcr :: srcrs ->
    133       let tmp_lbl = fresh_label def in
    134       let def =
    135         add_graph start_lbl (RTL.St_move (destr, srcr, tmp_lbl)) def in
    136       translate_move destrs srcrs tmp_lbl dest_lbl def
    137     | _ -> assert false (* wrong number of arguments *)
    138 
    139 
    140 let translate_cst cst destrs start_lbl dest_lbl def = match cst, destrs with
    141 
    142   | AST.Cst_int i, [r] ->
    143     add_graph start_lbl (RTL.St_int (r, i, dest_lbl)) def
    144 
    145   | AST.Cst_addrsymbol id, [r1 ; r2] ->
    146     add_graph start_lbl (RTL.St_addr (r1, r2, id, dest_lbl)) def
    147 
    148   | AST.Cst_stackoffset off, [r1 ; r2] ->
    149     let (def, tmpr) = fresh_reg def in
    150     adds_graph
    151       [RTL.St_stackaddr (r1, r2, start_lbl) ;
    152        RTL.St_int (tmpr, off, start_lbl) ;
    153        RTL.St_op2 (I8051.Add, r1, r1, tmpr, start_lbl) ;
    154        RTL.St_int (tmpr, 0, start_lbl) ;
    155        RTL.St_op2 (I8051.Addc, r2, r2, tmpr, start_lbl)]
    156       start_lbl dest_lbl def
    157 
    158   | AST.Cst_float _, _ ->
    159     error_float ()
    160 
    161   | _, _ -> assert false (* wrong number of arguments *)
    162 
    163 
    164 let translate_op1 op1 destrs srcrs start_lbl dest_lbl def =
    165   match op1, destrs, srcrs with
    166 
    167     | AST.Op_cast8unsigned, _, _ | AST.Op_cast8signed, _, _
    168     | AST.Op_cast16unsigned, _, _ | AST.Op_cast16signed, _, _ ->
    169       translate_move destrs srcrs start_lbl dest_lbl def
    170 
    171     | AST.Op_negint, [destr], [srcr] ->
    172       adds_graph
    173         [RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) ;
    174          RTL.St_op1 (I8051.Inc, destr, destr, start_lbl)]
    175         start_lbl dest_lbl def
    176 
    177     | AST.Op_notint, [destr], [srcr] ->
    178       adds_graph
    179         [RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl)]
    180         start_lbl dest_lbl def
    181 
    182     | AST.Op_id, _, _ ->
    183       translate_move destrs srcrs start_lbl dest_lbl def
    184 
    185     | AST.Op_ptrofint, [destr1 ; destr2], [srcr] ->
    186       adds_graph
    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 ; _] ->
    192       add_graph start_lbl (RTL.St_move (destr, srcr, dest_lbl)) def
    193 
    194     | AST.Op_notbool, [destr], [srcr] ->
    195       let (def, tmpr) = fresh_reg def in
    196       adds_graph
    197         [RTL.St_int (tmpr, 0, start_lbl) ;
    198          RTL.St_clear_carry start_lbl ;
    199          RTL.St_op2 (I8051.Sub, destr, tmpr, srcr, start_lbl) ;
    200          RTL.St_int (destr, 0, dest_lbl) ;
    201          RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl) ;
    202          RTL.St_int (tmpr, 1, dest_lbl) ;
    203          RTL.St_op2 (I8051.Xor, destr, destr, tmpr, start_lbl)]
    204         start_lbl dest_lbl def
    205 
    206     | AST.Op_negf, _, _ | AST.Op_absf, _, _ | AST.Op_singleoffloat, _, _
    207     | AST.Op_intoffloat, _, _ | AST.Op_intuoffloat, _, _
    208     | AST.Op_floatofint, _, _ | AST.Op_floatofintu, _, _ ->
    209       error_float ()
    210 
    211     | _ -> assert false (* wrong number of arguments *)
    212 
     144(*
    213145
    214146let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
    215147  match op2, destrs, srcrs1, srcrs2 with
    216148
    217     | AST.Op_add, [destr], [srcr1], [srcr2] ->
    218       adds_graph
    219         [RTL.St_op2 (I8051.Add, destr, srcr1, srcr2, start_lbl)]
    220         start_lbl dest_lbl def
    221 
    222     | AST.Op_sub, [destr], [srcr1], [srcr2] ->
    223       adds_graph
    224         [RTL.St_clear_carry start_lbl ;
    225          RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl)]
    226         start_lbl dest_lbl def
    227 
    228     | AST.Op_mul, [destr], [srcr1], [srcr2] ->
     149    | AST.Op_mul (1, _), [destr], [srcr1], [srcr2] ->
    229150      adds_graph
    230151        [RTL.St_opaccs (I8051.Mul, destr, srcr1, srcr2, start_lbl)]
    231152        start_lbl dest_lbl def
    232153
    233     | AST.Op_div, _, _, _ ->
    234       error "Signed division not supported."
    235 
    236     | AST.Op_divu, [destr], [srcr1], [srcr2] ->
    237       adds_graph
    238         [RTL.St_opaccs (I8051.Divu, destr, srcr1, srcr2, start_lbl)]
    239         start_lbl dest_lbl def
    240 
    241     | AST.Op_modu, [destr], [srcr1], [srcr2] ->
    242       adds_graph
    243         [RTL.St_opaccs (I8051.Modu, destr, srcr1, srcr2, start_lbl)]
    244         start_lbl dest_lbl def
    245 
    246     | AST.Op_mod, _, _, _ ->
    247       error "Signed modulo not supported."
    248 
    249     | AST.Op_and, [destr], [srcr1], [srcr2] ->
    250       adds_graph
    251         [RTL.St_op2 (I8051.And, destr, srcr1, srcr2, start_lbl)]
    252         start_lbl dest_lbl def
    253 
    254     | AST.Op_or, [destr], [srcr1], [srcr2] ->
    255       adds_graph
    256         [RTL.St_op2 (I8051.Or, destr, srcr1, srcr2, start_lbl)]
    257         start_lbl dest_lbl def
    258 
    259     | AST.Op_xor, [destr], [srcr1], [srcr2] ->
    260       adds_graph
    261         [RTL.St_op2 (I8051.Xor, destr, srcr1, srcr2, start_lbl)]
    262         start_lbl dest_lbl def
    263 
    264     | AST.Op_shru, _, _, _ | AST.Op_shr, _, _, _ | AST.Op_shl, _, _, _ ->
     154    | AST.Op_shr _, _, _, _ ->
    265155      error_shift ()
    266156
    267     | AST.Op_addf, _, _, _ | AST.Op_subf, _, _, _ | AST.Op_mulf, _, _, _
    268     | AST.Op_divf, _, _, _ | AST.Op_cmpf _, _, _, _ ->
    269       error_float ()
    270 
    271     | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2]
    272     | AST.Op_addp, [destr1 ; destr2], [srcr2], [srcr11 ; srcr12] ->
    273       let (def, tmpr1) = fresh_reg def in
    274       let (def, tmpr2) = fresh_reg def in
    275       adds_graph
    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 ; _] ->
    283       let (def, tmpr1) = fresh_reg def in
    284       let (def, tmpr2) = fresh_reg def in
    285       adds_graph
    286         [RTL.St_op1 (I8051.Cmpl, tmpr1, srcr2, start_lbl) ;
    287          RTL.St_int (tmpr2, 1, start_lbl) ;
    288          RTL.St_op2 (I8051.Add, tmpr1, tmpr1, tmpr2, start_lbl) ;
    289          RTL.St_op2 (I8051.Add, destr, srcr1, tmpr1, start_lbl)]
    290         start_lbl dest_lbl def
    291 
    292     | AST.Op_subp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] ->
    293       adds_graph
    294         [RTL.St_clear_carry 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)]
    298         start_lbl dest_lbl def
    299 
    300     | AST.Op_cmp AST.Cmp_eq, _, _, _
    301     | AST.Op_cmpu AST.Cmp_eq, _, _, _ ->
    302       add_translates
    303         [translate_op2 AST.Op_sub destrs srcrs1 srcrs2 ;
    304          translate_op1 AST.Op_notbool destrs destrs]
    305         start_lbl dest_lbl def
    306 
    307     | AST.Op_cmp AST.Cmp_ne, _, _, _
    308     | AST.Op_cmpu AST.Cmp_ne, _, _, _ ->
    309       translate_op2 AST.Op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    310 
    311     | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
     157    | AST.Op_cmp (AST.Cmp_lt, (1, AST.Unsigned)), [destr], [srcr1], [srcr2] ->
    312158      let (def, tmpr) = fresh_reg def in
    313159      adds_graph
     
    318164        start_lbl dest_lbl def
    319165
    320     | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
    321       translate_op2 (AST.Op_cmpu AST.Cmp_lt)
    322         destrs srcrs2 srcrs1 start_lbl dest_lbl def
    323 
    324     | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
    325       add_translates
    326         [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
    327          translate_op1 AST.Op_notbool destrs destrs]
    328         start_lbl dest_lbl def
    329 
    330     | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
    331       add_translates
    332         [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
    333          translate_op1 AST.Op_notbool destrs destrs]
    334         start_lbl dest_lbl def
    335 
    336     | AST.Op_cmp cmp, _, _, _ ->
     166    | AST.Op_cmp (cmp, ((size, AST.Signed) as int_type)), _, _, _ ->
    337167      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
    338168      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
     
    340170        [translate_cst (AST.Cst_int 128) tmprs1 ;
    341171         translate_cst (AST.Cst_int 128) tmprs2 ;
    342          translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
    343          translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
    344          translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2]
    345         start_lbl dest_lbl def
    346 
    347     | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
    348       let (def, tmpr) = fresh_reg def in
    349       add_translates
    350         [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
    351          translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
    352          translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
    353          adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
    354          translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
     172         translate_op2 (AST.Op_add int_type) tmprs1 srcrs1 tmprs1 ;
     173         translate_op2 (AST.Op_add int_type) tmprs2 srcrs2 tmprs2 ;
     174         translate_op2 (AST.Op_cmp (cmp, (size, AST.Unsigned)))
     175           destrs tmprs1 tmprs2]
    355176        start_lbl dest_lbl def
    356177
     
    359180      let (def, tmpr2) = fresh_reg def in
    360181      add_translates
    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] ;
     182        [translate_op2 (AST.Op_cmp (AST.Cmp_lt, uint))
     183            [tmpr1] [srcr12] [srcr22] ;
     184         translate_op2 (AST.Op_cmp (AST.Cmp_eq, uint))
     185            [tmpr2] [srcr12] [srcr22] ;
     186         translate_op2 (AST.Op_cmp (AST.Cmp_lt, uint))
     187            [destr] [srcr11] [srcr21] ;
    364188         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
    365189         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
    366190        start_lbl dest_lbl def
    367191
    368     | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
     192    | _ -> error_int ()
     193*)
     194
     195let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with
     196
     197  | AST.Cst_int _ when destrs = [] ->
     198    add_graph start_lbl (RTL.St_skip dest_lbl) def
     199
     200  | AST.Cst_int i ->
     201    let size = List.length destrs in
     202    let module M = IntValue.Make (struct let size = size end) in
     203    let is = List.map M.to_int (M.break (M.of_int i) size) in
     204    let f r i = RTL.St_int (r, i, dest_lbl) in
     205    let l = List.map2 f destrs is in
     206    adds_graph l start_lbl dest_lbl def
     207
     208  | AST.Cst_float _ -> error_float ()
     209
     210  | AST.Cst_addrsymbol id ->
     211    let (r1, r2) = make_addr destrs in
     212    add_graph start_lbl (RTL.St_addr (r1, r2, id, dest_lbl)) def
     213
     214  | AST.Cst_stack ->
     215    let (r1, r2) = make_addr destrs in
     216    add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def
     217
     218  | AST.Cst_offset off ->
     219    let i = concrete_offset off in
     220    translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
     221
     222  | AST.Cst_sizeof size ->
     223    let i = concrete_size size in
     224    translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
     225
     226
     227let rec translate_move destrs srcrs start_lbl =
     228  let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
     229  let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
     230  let translates1 = adds_graph (List.map2 f_common common1 common2) in
     231  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
     232  add_translates [translates1 ; translates2] start_lbl
     233
     234
     235let translate_cast_unsigned destrs start_lbl dest_lbl def =
     236  let (def, tmp_zero) = fresh_reg def in
     237  let zeros = MiscPottier.make tmp_zero (List.length destrs) in
     238  add_translates
     239    [adds_graph [RTL.St_int (tmp_zero, 0, start_lbl)] ;
     240     translate_move destrs zeros]
     241    start_lbl dest_lbl def
     242
     243let translate_cast_signed destrs srcr start_lbl dest_lbl def =
     244  let (def, tmp_128) = fresh_reg def in
     245  let (def, tmp_255) = fresh_reg def in
     246  let (def, tmpr) = fresh_reg def in
     247  let (def, dummy) = fresh_reg def in
     248  let insts =
     249    [RTL.St_int (tmp_128, 128, start_lbl) ;
     250     RTL.St_op2 (I8051.And, tmpr, tmp_128, srcr, start_lbl) ;
     251     RTL.St_opaccs (I8051.DivuModu, tmpr, dummy, tmpr, tmp_128, start_lbl) ;
     252     RTL.St_int (tmp_255, 255, start_lbl) ;
     253     RTL.St_opaccs (I8051.Mul, tmpr, dummy, tmpr, tmp_255, start_lbl)] in
     254  let srcrs = MiscPottier.make tmpr (List.length destrs) in
     255  add_translates [adds_graph insts ; translate_move destrs srcrs]
     256    start_lbl dest_lbl def
     257
     258let translate_cast src_size src_sign dest_size destrs srcrs =
     259  if List.length srcrs = 0 then adds_graph []
     260  else
     261    if dest_size < src_size then translate_move destrs srcrs
     262    else
     263      let ((common1, rest1), (common2, _)) = MiscPottier.reduce destrs srcrs in
     264      let insts_common = translate_move common1 common2 in
     265      let sign_reg = MiscPottier.last srcrs in
     266      let insts_sign = match src_sign with
     267        | AST.Unsigned -> translate_cast_unsigned rest1
     268        | AST.Signed -> translate_cast_signed rest1 sign_reg in
     269      add_translates [insts_common ; insts_sign]
     270
     271
     272let translate_negint destrs srcrs start_lbl dest_lbl def =
     273  assert (List.length destrs = List.length srcrs) ;
     274  let (def, tmpr) = fresh_reg def in
     275  let f_cmpl destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
     276  let insts_cmpl = List.map2 f_cmpl destrs srcrs in
     277  let insts_init =
     278    [RTL.St_set_carry start_lbl ;
     279     RTL.St_int (tmpr, 0, start_lbl)] in
     280  let f_add destr = RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl) in
     281  let insts_add = List.map f_add destrs in
     282  adds_graph (insts_cmpl @ insts_init @ insts_add)
     283    start_lbl dest_lbl def
     284
     285
     286let translate_notbool destrs srcrs start_lbl dest_lbl def = match destrs with
     287  | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
     288  | destr :: destrs ->
     289    let (def, tmpr) = fresh_reg def in
     290    let (def, tmp_srcrs) = fresh_regs def (List.length srcrs) in
     291    let save_srcrs = translate_move tmp_srcrs srcrs in
     292    let init_destr = RTL.St_int (destr, 1, start_lbl) in
     293    let f tmp_srcr =
     294      [RTL.St_clear_carry start_lbl ;
     295       RTL.St_int (tmpr, 0, start_lbl) ;
     296       RTL.St_op2 (I8051.Sub, tmpr, tmpr, tmp_srcr, start_lbl) ;
     297       RTL.St_int (tmpr, 0, start_lbl) ;
     298       RTL.St_op2 (I8051.Addc, tmpr, tmpr, tmpr, start_lbl) ;
     299       RTL.St_op2 (I8051.Xor, destr, destr, tmpr, start_lbl)] in
     300    let insts = init_destr :: (List.flatten (List.map f tmp_srcrs)) in
     301    let epilogue = translate_cst (AST.Cst_int 0) destrs in
     302    add_translates [save_srcrs ; adds_graph insts ; epilogue]
     303      start_lbl dest_lbl def
     304
     305
     306let translate_op1 op1 destrs srcrs start_lbl dest_lbl def = match op1 with
     307
     308  | AST.Op_cast ((src_size, src_sign), dest_size) ->
     309    translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl
     310      def
     311
     312  | AST.Op_negint ->
     313    translate_negint destrs srcrs start_lbl dest_lbl def
     314
     315  | AST.Op_notbool ->
     316    translate_notbool destrs srcrs start_lbl dest_lbl def
     317
     318  | AST.Op_notint ->
     319    let f destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
     320    let l = List.map2 f destrs srcrs in
     321    adds_graph l start_lbl dest_lbl def
     322
     323  | AST.Op_ptrofint | AST.Op_intofptr | AST.Op_id ->
     324    translate_move destrs srcrs start_lbl dest_lbl def
     325
     326
     327let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     328  let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) =
     329    MiscPottier.reduce srcrs1 srcrs2 in
     330  let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in
     331  let ((destrs_common, destrs_rest), _) =
     332    MiscPottier.reduce destrs srcrs1_common in
     333  let ((destrs_cted, destrs_rest), (srcrs_cted, _)) =
     334    MiscPottier.reduce destrs_rest srcrs_rest in
     335  let (def, tmpr) = fresh_reg def in
     336  let insts_init =
     337    [RTL.St_clear_carry start_lbl ;
     338     RTL.St_int (tmpr, 0, start_lbl)] in
     339  let f_add destr srcr1 srcr2 =
     340    RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
     341  let insts_add =
     342    MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in
     343  let f_add_cted destr srcr =
     344    RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in
     345  let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
     346  let f_rest destr =
     347    RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in
     348  let insts_rest = List.map f_rest destrs_rest in
     349  adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest)
     350    start_lbl dest_lbl def
     351
     352
     353let rec translate_mul1 dummy tmpr destrs srcrs1 srcr2 start_lbl =
     354  match destrs, srcrs1 with
     355    | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl
     356    | [destr], [] ->
     357      adds_graph [RTL.St_int (tmpr, 0, start_lbl) ;
     358                  RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]
     359        start_lbl
     360    | destr1 :: destr2 :: destrs, [] ->
     361      add_translates
     362        [adds_graph [RTL.St_int (tmpr, 0, start_lbl) ;
     363                     RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl) ;
     364                     RTL.St_op2 (I8051.Addc, destr2, tmpr, tmpr, start_lbl)] ;
     365         translate_cst (AST.Cst_int 0) destrs]
     366        start_lbl
     367    | [destr], srcr1 :: _ ->
     368      adds_graph
     369        [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ;
     370         RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]
     371        start_lbl
     372    | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 ->
     373      add_translates
     374        [adds_graph
     375            [RTL.St_opaccs
     376                (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ;
     377             RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl)] ;
     378         translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2]
     379        start_lbl
     380
     381let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates
     382    srcr2i =
     383  let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in
     384  translates @
     385    (match tmp_destrs2 with
     386      | [] -> []
     387      | tmp_destr2 :: tmp_destrs2 ->
     388        [adds_graph [RTL.St_clear_carry dummy_lbl ;
     389                     RTL.St_int (tmp_destr2, 0, dummy_lbl)] ;
     390         translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
     391         translate_cst (AST.Cst_int 0) tmp_destrs1 ;
     392         adds_graph [RTL.St_clear_carry dummy_lbl] ;
     393         translate_op I8051.Addc destrs destrs tmp_destrs])
     394
     395let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     396  let (def, dummy) = fresh_reg def in
     397  let (def, tmpr) = fresh_reg def in
     398  let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
     399  let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
     400  let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in
     401  let insts_init =
     402    [translate_move fresh_srcrs1 srcrs1 ;
     403     translate_move fresh_srcrs2 srcrs2 ;
     404     translate_cst (AST.Cst_int 0) destrs] in
     405  let f = translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
     406  let insts_mul = MiscPottier.foldi f [] srcrs2 in
     407  add_translates (insts_init @ insts_mul) start_lbl dest_lbl def
     408
     409
     410let translate_divumodu8 order destrs srcr1 srcr2 start_lbl dest_lbl def =
     411  match destrs with
     412    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
     413    | destr :: destrs ->
     414      let (def, dummy) = fresh_reg def in
     415      let (destr1, destr2) = if order then (destr, dummy) else (dummy, destr) in
     416      let inst_div =
     417        adds_graph [RTL.St_opaccs (I8051.DivuModu, destr1, destr2,
     418                                   srcr1, srcr2, start_lbl)] in
     419      let insts_rest = translate_cst (AST.Cst_int 0) destrs in
     420      add_translates [inst_div ; insts_rest] start_lbl dest_lbl def
     421
     422
     423let translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     424  match destrs with
     425    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
     426    | destr :: destrs ->
     427      let (def, tmpr) = fresh_reg def in
     428      let (def, tmp_zero) = fresh_reg def in
     429      let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in
     430      let save_srcrs1 = translate_move tmp_srcrs1 srcrs1 in
     431      let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in
     432      let save_srcrs2 = translate_move tmp_srcrs2 srcrs2 in
     433      let ((common1, rest1), (common2, rest2)) =
     434        MiscPottier.reduce tmp_srcrs1 tmp_srcrs2 in
     435      let rest = choose_rest rest1 rest2 in
     436      let inits =
     437        [RTL.St_int (destr, 0, start_lbl) ;
     438         RTL.St_int (tmp_zero, 0, start_lbl)] in
     439      let f_common tmp_srcr1 tmp_srcr2 =
     440        [RTL.St_clear_carry start_lbl ;
     441         RTL.St_op2 (I8051.Sub, tmpr, tmp_srcr1, tmp_srcr2, start_lbl) ;
     442         RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in
     443      let insts_common = List.flatten (List.map2 f_common common1 common2) in
     444      let f_rest tmp_srcr =
     445        [RTL.St_clear_carry start_lbl ;
     446         RTL.St_op2 (I8051.Sub, tmpr, tmp_zero, tmp_srcr, start_lbl) ;
     447         RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in
     448      let insts_rest = List.flatten (List.map f_rest rest) in
     449      let insts = inits @ insts_common @ insts_rest in
     450      let epilogue = translate_cst (AST.Cst_int 0) destrs in
     451      add_translates [save_srcrs1 ; save_srcrs2 ; adds_graph insts ; epilogue]
     452        start_lbl dest_lbl def
     453
     454
     455let translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl
     456    (srcr1, srcr2) =
     457  [RTL.St_clear_carry dummy_lbl ;
     458   RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ;
     459   RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ;
     460   RTL.St_op2 (I8051.Sub, tmpr2, srcr2, srcr1, dummy_lbl) ;
     461   RTL.St_op2 (I8051.Addc, tmpr2, tmp_zero, tmp_zero, dummy_lbl) ;
     462   RTL.St_op2 (I8051.Or, tmpr1, tmpr1, tmpr2, dummy_lbl) ;
     463   RTL.St_op2 (I8051.Xor, tmpr1, tmpr1, tmp_one, dummy_lbl) ;
     464   RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)]
     465
     466let translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 destr leq dummy_lbl =
     467  let f = translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
     468  (RTL.St_int (destr, 1, dummy_lbl)) :: (List.flatten (List.map f leq))
     469
     470let translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq
     471    srcr1 srcr2 =
     472  (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @
     473  [RTL.St_clear_carry dummy_lbl ;
     474   RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ;
     475   RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ;
     476   RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ;
     477   RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)]
     478
     479let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl
     480    srcrs1 srcrs2 =
     481  let f (insts, leq) srcr1 srcr2 =
     482    let added_insts =
     483      translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq
     484        srcr1 srcr2 in
     485    (insts @ added_insts, leq @ [(srcr1, srcr2)]) in
     486  fst (List.fold_left2 f ([], []) srcrs1 srcrs2)
     487
     488let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     489  match destrs with
     490    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
     491    | _ ->
     492      let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
     493      let tmp_destr = List.hd tmp_destrs in
     494      let (def, tmp_zero) = fresh_reg def in
     495      let (def, tmp_one) = fresh_reg def in
     496      let (def, tmpr1) = fresh_reg def in
     497      let (def, tmpr2) = fresh_reg def in
     498      let (def, tmpr3) = fresh_reg def in
     499      let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in
     500      let srcrs1 = List.rev srcrs1 in
     501      let srcrs2 = List.rev srcrs2 in
     502      let insts_init =
     503        [translate_cst (AST.Cst_int 0) tmp_destrs ;
     504         translate_cst (AST.Cst_int 0) added ;
     505         adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ;
     506                     RTL.St_int (tmp_one, 1, start_lbl)]] in
     507      let insts_main =
     508        translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl
     509          srcrs1 srcrs2 in
     510      let insts_main = [adds_graph insts_main] in
     511      let insts_exit = [translate_move destrs tmp_destrs] in
     512      add_translates (insts_init @ insts_main @ insts_exit )
     513        start_lbl dest_lbl def
     514
     515
     516let add_128_to_last tmp_128 rs start_lbl = match rs with
     517  | [] -> adds_graph [] start_lbl
     518  | _ ->
     519    let r = MiscPottier.last rs in
     520    adds_graph [RTL.St_op2 (I8051.Add, r, r, tmp_128, start_lbl)] start_lbl
     521
     522let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     523  let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in
     524  let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in
     525  let (def, tmp_128) = fresh_reg def in
     526  add_translates
     527    [translate_move tmp_srcrs1 srcrs1 ;
     528     translate_move tmp_srcrs2 srcrs2 ;
     529     adds_graph [RTL.St_int (tmp_128, 128, start_lbl)] ;
     530     add_128_to_last tmp_128 tmp_srcrs1 ;
     531     add_128_to_last tmp_128 tmp_srcrs2 ;
     532     translate_lt destrs tmp_srcrs1 tmp_srcrs2]
     533    start_lbl dest_lbl def
     534
     535
     536let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     537  match op2 with
     538
     539    | AST.Op_add | AST.Op_addp ->
     540      translate_op I8051.Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
     541
     542    | AST.Op_sub | AST.Op_subp | AST.Op_subpp ->
     543      translate_op I8051.Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     544
     545    | AST.Op_mul ->
     546      translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
     547
     548    | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
     549      translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2)
     550        start_lbl dest_lbl def
     551
     552    | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
     553      translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2)
     554        start_lbl dest_lbl def
     555
     556    | AST.Op_and ->
     557      translate_op I8051.And destrs srcrs1 srcrs2 start_lbl dest_lbl def
     558
     559    | AST.Op_or ->
     560      translate_op I8051.Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
     561
     562    | AST.Op_xor ->
     563      translate_op I8051.Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
     564
     565    | AST.Op_cmp AST.Cmp_eq
     566    | AST.Op_cmpu AST.Cmp_eq
     567    | AST.Op_cmpp AST.Cmp_eq ->
     568      add_translates
     569        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ;
     570         translate_op1 AST.Op_notbool destrs destrs]
     571        start_lbl dest_lbl def
     572
     573    | AST.Op_cmp AST.Cmp_ne
     574    | AST.Op_cmpu AST.Cmp_ne
     575    | AST.Op_cmpp AST.Cmp_ne ->
     576      translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
     577
     578    | AST.Op_cmp AST.Cmp_lt ->
     579      translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def
     580
     581    | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
     582      translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def
     583
     584    | AST.Op_cmp AST.Cmp_le ->
     585      add_translates
     586        [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
     587         translate_op1 AST.Op_notbool destrs destrs]
     588        start_lbl dest_lbl def
     589
     590    | AST.Op_cmpu AST.Cmp_le ->
     591      add_translates
     592        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ;
     593         translate_op1 AST.Op_notbool destrs destrs]
     594        start_lbl dest_lbl def
     595
     596    | AST.Op_cmpp AST.Cmp_le ->
     597      add_translates
     598        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
     599         translate_op1 AST.Op_notbool destrs destrs]
     600        start_lbl dest_lbl def
     601
     602    | AST.Op_cmp AST.Cmp_gt ->
     603      translate_op2 (AST.Op_cmp AST.Cmp_lt)
     604        destrs srcrs2 srcrs1 start_lbl dest_lbl def
     605
     606    | AST.Op_cmpu AST.Cmp_gt ->
     607      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
     608        destrs srcrs2 srcrs1 start_lbl dest_lbl def
     609
     610    | AST.Op_cmpp AST.Cmp_gt ->
    369611      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
    370612        destrs srcrs2 srcrs1 start_lbl dest_lbl def
    371613
    372     | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
    373       add_translates
    374         [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
     614    | AST.Op_cmp AST.Cmp_ge ->
     615      add_translates
     616        [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
    375617         translate_op1 AST.Op_notbool destrs destrs]
    376618        start_lbl dest_lbl def
    377619
    378     | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
     620    | AST.Op_cmpu AST.Cmp_ge ->
     621      add_translates
     622        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
     623         translate_op1 AST.Op_notbool destrs destrs]
     624        start_lbl dest_lbl def
     625
     626    | AST.Op_cmpp AST.Cmp_ge ->
    379627      add_translates
    380628        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
     
    382630        start_lbl dest_lbl def
    383631
    384     | _ -> assert false (* wrong number of arguments *)
    385 
    386 
    387 let translate_condptr r1 r2 start_lbl lbl_true lbl_false def =
     632    | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
     633    | AST.Op_shr | AST.Op_shru ->
     634      (* Unsupported, should have been replaced by a runtime function. *)
     635      assert false
     636
     637
     638let translate_cond srcrs start_lbl lbl_true lbl_false def =
    388639  let (def, tmpr) = fresh_reg def in
    389   adds_graph
    390     [RTL.St_op2 (I8051.Or, tmpr, r1, r2, start_lbl) ;
    391      RTL.St_condacc (tmpr, lbl_true, lbl_false)]
    392     start_lbl start_lbl def
    393 
    394 
    395 let translate_condcst cst start_lbl lbl_true lbl_false def = match cst with
    396 
    397   | AST.Cst_int i ->
    398     let (def, tmpr) = fresh_reg def in
    399     adds_graph
    400       [RTL.St_int (tmpr, i, start_lbl) ;
    401        RTL.St_condacc (tmpr, lbl_true, lbl_false)]
    402       start_lbl start_lbl def
    403 
    404   | AST.Cst_addrsymbol x ->
    405     let (def, r1) = fresh_reg def in
    406     let (def, r2) = fresh_reg def in
    407     let lbl = fresh_label def in
    408     let def = add_graph start_lbl (RTL.St_addr (r1, r2, x, lbl)) def in
    409     translate_condptr r1 r2 lbl lbl_true lbl_false def
    410 
    411   | AST.Cst_stackoffset off ->
    412     let (def, r1) = fresh_reg def in
    413     let (def, r2) = fresh_reg def in
    414     let tmp_lbl = fresh_label def in
    415     let def =
    416       translate_cst (AST.Cst_stackoffset off) [r1 ; r2] start_lbl tmp_lbl def in
    417     translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def
    418 
    419   | AST.Cst_float _ ->
    420     error_float ()
    421 
    422 
    423 let size_of_op1_ret = function
    424   | AST.Op_cast8unsigned
    425   | AST.Op_cast8signed
    426   | AST.Op_cast16unsigned
    427   | AST.Op_cast16signed
    428   | AST.Op_negint
    429   | AST.Op_notbool
    430   | AST.Op_notint
    431   | AST.Op_intofptr -> 1
    432   | AST.Op_ptrofint -> 2
    433   | AST.Op_id -> raise (Invalid_argument "RTLabsToRTL.size_of_op1_ret")
    434   | AST.Op_negf
    435   | AST.Op_absf
    436   | AST.Op_singleoffloat
    437   | AST.Op_intoffloat
    438   | AST.Op_intuoffloat
    439   | AST.Op_floatofint
    440   | AST.Op_floatofintu -> error_float ()
    441 
    442 let rec translate_cond1 op1 srcrs start_lbl lbl_true lbl_false def =
    443   match op1, srcrs with
    444 
    445     | AST.Op_id, [srcr] ->
    446       adds_graph
    447         [RTL.St_condacc (srcr, lbl_true, lbl_false)]
    448         start_lbl start_lbl def
    449 
    450     | AST.Op_id, [srcr1 ; srcr2] ->
    451       translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def
    452 
    453     | AST.Op_id, _ -> assert false (* wrong number of arguments *)
    454 
    455     | _, srcrs ->
    456       let (def, destrs) = fresh_regs def (size_of_op1_ret op1) in
    457       let lbl = fresh_label def in
    458       let def = translate_op1 op1 destrs srcrs start_lbl lbl def in
    459       translate_cond1 AST.Op_id destrs lbl lbl_true lbl_false def
    460 
    461 
    462 let size_of_op2_ret n = function
    463   | AST.Op_add
    464   | AST.Op_sub
    465   | AST.Op_mul
    466   | AST.Op_div
    467   | AST.Op_divu
    468   | AST.Op_mod
    469   | AST.Op_modu
    470   | AST.Op_and
    471   | AST.Op_or
    472   | AST.Op_xor
    473   | AST.Op_shl
    474   | AST.Op_shr
    475   | AST.Op_shru
    476   | AST.Op_cmp _
    477   | AST.Op_cmpu _
    478   | AST.Op_cmpp _ -> 1
    479   | AST.Op_addp -> 2
    480   | AST.Op_subp ->
    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
    483   | AST.Op_addf
    484   | AST.Op_subf
    485   | AST.Op_mulf
    486   | AST.Op_divf
    487   | AST.Op_cmpf _ -> error_float ()
    488 
    489 let translate_cond2 op2 srcrs1 srcrs2 start_lbl lbl_true lbl_false def =
    490   match op2, srcrs1, srcrs2 with
    491 
    492     | AST.Op_cmp AST.Cmp_eq, [srcr1], [srcr2] ->
    493       let (def, tmpr) = fresh_reg def in
    494       adds_graph
    495         [RTL.St_clear_carry start_lbl ;
    496          RTL.St_op2 (I8051.Sub, tmpr, srcr1, srcr2, start_lbl) ;
    497          RTL.St_condacc (tmpr, lbl_false, lbl_true)]
    498         start_lbl start_lbl def
    499 
    500     | _, _, _ ->
    501       let n = (List.length srcrs1) + (List.length srcrs2) in
    502       let (def, destrs) = fresh_regs def (size_of_op2_ret n op2) in
    503       let lbl = fresh_label def in
    504       let def = translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def in
    505       translate_cond1 AST.Op_id destrs lbl lbl_true lbl_false def
    506 
    507 
    508 let rec addressing_pointer mode args destr1 destr2 start_lbl dest_lbl def =
    509   let destrs = [destr1 ; destr2] in
    510   match mode, args with
    511 
    512     | RTLabs.Aindexed off, [[srcr1 ; srcr2]] ->
    513       let (def, tmpr) = fresh_reg def in
    514       add_translates
     640  let tmp_lbl = fresh_label def in
     641  let init = RTL.St_int (tmpr, 0, start_lbl) in
     642  let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, srcr, start_lbl) in
     643  let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
     644  add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def
     645
     646
     647let translate_load addr destrs start_lbl dest_lbl def =
     648  let (def, save_addr) = fresh_regs def (List.length addr) in
     649  let (def, tmp_addr) = fresh_regs def (List.length addr) in
     650  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
     651  let (def, tmpr) = fresh_reg def in
     652  let insts_save_addr = translate_move save_addr addr in
     653  let f (translates, off) r =
     654    let translates =
     655      translates @
    515656        [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
    516          translate_op2 AST.Op_addp destrs [srcr1 ; srcr2] [tmpr]]
    517         start_lbl dest_lbl def
    518 
    519     | RTLabs.Aindexed2, [[srcr11 ; srcr12] ; [srcr2]]
    520     | RTLabs.Aindexed2, [[srcr2] ; [srcr11 ; srcr12]] ->
    521       translate_op2 AST.Op_addp destrs [srcr11 ; srcr12] [srcr2]
    522         start_lbl dest_lbl def
    523 
    524     | RTLabs.Aglobal (x, off), _ ->
    525       let (def, tmpr) = fresh_reg def in
    526       add_translates
    527         [adds_graph [RTL.St_int (tmpr, off, start_lbl) ;
    528                      RTL.St_addr (destr1, destr2, x, start_lbl)] ;
    529          translate_op2 AST.Op_addp destrs destrs [tmpr]]
    530         start_lbl dest_lbl def
    531 
    532     | RTLabs.Abased (x, off), [srcrs] ->
    533       let (def, tmpr1) = fresh_reg def in
    534       let (def, tmpr2) = fresh_reg def in
    535       add_translates
    536         [addressing_pointer (RTLabs.Aglobal (x, off)) [] tmpr1 tmpr2 ;
    537          translate_op2 AST.Op_addp destrs [tmpr1 ; tmpr2] srcrs]
    538         start_lbl dest_lbl def
    539 
    540     | RTLabs.Ainstack off, _ ->
    541       let (def, tmpr) = fresh_reg def in
    542       add_translates
    543         [adds_graph [RTL.St_int (tmpr, off, start_lbl) ;
    544                      RTL.St_stackaddr (destr1, destr2, start_lbl)] ;
    545          translate_op2 AST.Op_addp destrs destrs [tmpr]]
    546         start_lbl dest_lbl def
    547 
    548     | _ -> assert false (* wrong number of arguments *)
    549 
    550 
    551 let 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] ->
    563       let (def, addr1) = fresh_reg def in
    564       let (def, addr2) = fresh_reg def in
    565       let addr = [addr1 ; addr2] in
    566       let (def, tmpr) = fresh_reg def in
    567       add_translates
    568         [addressing_pointer mode args addr1 addr2 ;
    569          adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl) ;
    570                      RTL.St_int (tmpr, 1, start_lbl)] ;
    571          translate_op2 AST.Op_addp addr addr [tmpr] ;
    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 
    578 let translate_store q mode args srcrs start_lbl dest_lbl def =
    579   match q, srcrs with
    580 
    581     | Memory.QInt 1, [srcr] ->
    582       let (def, addr1) = fresh_reg def in
    583       let (def, addr2) = fresh_reg def in
    584       add_translates
    585         [addressing_pointer mode args addr1 addr2 ;
    586          adds_graph [RTL.St_store (addr1, addr2, srcr, dest_lbl)]]
    587         start_lbl dest_lbl def
    588 
    589     | Memory.QPtr, [srcr1 ; srcr2] ->
    590       let (def, addr1) = fresh_reg def in
    591       let (def, addr2) = fresh_reg def in
    592       let addr = [addr1 ; addr2] in
    593       let (def, tmpr) = fresh_reg def in
    594       add_translates
    595         [addressing_pointer mode args addr1 addr2 ;
    596          adds_graph [RTL.St_store (addr1, addr2, srcr1, start_lbl) ;
    597                      RTL.St_int (tmpr, 1, start_lbl)] ;
    598          translate_op2 AST.Op_addp addr addr [tmpr] ;
    599          adds_graph [RTL.St_store (addr1, addr2, srcr2, dest_lbl)]]
    600         start_lbl dest_lbl def
    601 
    602     | _ -> error "Size error in store."
     657         translate_op2 AST.Op_addp tmp_addr save_addr [tmpr] ;
     658         adds_graph [RTL.St_load (r, tmp_addr1, tmp_addr2, dest_lbl)]] in
     659    (translates, off + Driver.TargetArch.int_size) in
     660  let (translates, _) = List.fold_left f ([], 0) destrs in
     661  add_translates (insts_save_addr :: translates) start_lbl dest_lbl def
     662
     663
     664let translate_store addr srcrs start_lbl dest_lbl def =
     665  let (def, tmp_addr) = fresh_regs def (List.length addr) in
     666  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
     667  let (def, tmpr) = fresh_reg def in
     668  let f (translates, off) srcr =
     669    let translates =
     670      translates @
     671        [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
     672         translate_op2 AST.Op_addp tmp_addr addr [tmpr] ;
     673         adds_graph [RTL.St_store (tmp_addr1, tmp_addr2, srcr, dest_lbl)]] in
     674    (translates, off + Driver.TargetArch.int_size) in
     675  let (translates, _) = List.fold_left f ([], 0) srcrs in
     676  add_translates translates start_lbl dest_lbl def
    603677
    604678
     
    612686
    613687  | RTLabs.St_cst (destr, cst, lbl') ->
    614     translate_cst cst (find_and_list destr lenv) lbl lbl' def
     688    translate_cst cst (find_local_env destr lenv) lbl lbl' def
    615689
    616690  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
    617     translate_op1 op1 (find_and_list destr lenv) (find_and_list srcr lenv)
     691    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
    618692      lbl lbl' def
    619693
    620694  | 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') ->
     695    translate_op2 op2 (find_local_env destr lenv)
     696      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
     697
     698  | RTLabs.St_load (_, addr, destr, lbl') ->
     699    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
     700      lbl lbl' def
     701
     702  | RTLabs.St_store (_, addr, srcr, lbl') ->
     703    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
     704      lbl lbl' def
     705
     706  | RTLabs.St_call_id (f, args, None, _, lbl') ->
     707    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
     708
     709  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
    633710    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') ->
     711                                   find_local_env retr lenv, lbl')) def
     712
     713  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
     714    let (f1, f2) = find_and_addr f lenv in
     715    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
     716
     717  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
    637718    let (f1, f2) = find_and_addr f lenv in
    638719    add_graph lbl
    639720      (RTL.St_call_ptr
    640          (f1, f2, rtl_args args lenv, find_and_list retr lenv, lbl')) def
     721         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
    641722
    642723  | RTLabs.St_tailcall_id (f, args, _) ->
     
    647728    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
    648729
    649   | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
    650     translate_condcst cst lbl lbl_true lbl_false def
    651 
    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
     730  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
     731    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
    659732
    660733  | RTLabs.St_jumptable _ ->
    661734    error "Jump tables not supported yet."
    662735
    663   | RTLabs.St_return r ->
    664     add_graph lbl (RTL.St_return (find_and_list r lenv)) def
     736  | RTLabs.St_return None ->
     737    add_graph lbl (RTL.St_return []) def
     738
     739  | RTLabs.St_return (Some r) ->
     740    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
    665741
    666742
     
    668744  let runiverse = def.RTLabs.f_runiverse in
    669745  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
     746    initialize_local_env runiverse
     747      (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in
    673748  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
     749  let params = map_list_local_env lenv (List.map fst def.RTLabs.f_params) in
     750  let locals = map_list_local_env lenv (List.map fst def.RTLabs.f_locals) in
    676751  let locals = set_of_list locals in
     752  let result = match def.RTLabs.f_result with
     753    | None -> []
     754    | Some (r, _) -> find_local_env r lenv in
    677755  let res =
    678756    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
    679757      RTL.f_runiverse = runiverse ;
    680       RTL.f_sig       = def.RTLabs.f_sig ;
    681758      RTL.f_result    = result ;
    682759      RTL.f_params    = params ;
    683760      RTL.f_locals    = locals ;
    684       RTL.f_stacksize = def.RTLabs.f_stacksize ;
     761      RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ;
    685762      RTL.f_graph     = Label.Map.empty ;
    686763      RTL.f_entry     = def.RTLabs.f_entry ;
     
    695772
    696773let translate p =
    697   let f (id, fun_def) = (id, translate_fun_def fun_def) in
    698   { RTL.vars   = p.RTLabs.vars ;
    699     RTL.functs = List.map f p.RTLabs.functs ;
     774  let f_global (id, size) = (id, concrete_size size) in
     775  let f_funct (id, fun_def) = (id, translate_fun_def fun_def) in
     776  { RTL.vars   = List.map f_global p.RTLabs.vars ;
     777    RTL.functs = List.map f_funct p.RTLabs.functs ;
    700778    RTL.main   = p.RTLabs.main }
Note: See TracChangeset for help on using the changeset viewer.