Changeset 818 for Deliverables/D2.2/8051


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

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

Location:
Deliverables/D2.2/8051
Files:
2 added
78 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D2.2/8051/README

    r619 r818  
    3434--------------
    3535
    36   - ocaml    (>= 3.11)
     36  - ocaml    (>= 3.13)
    3737  - menhir   (>= 20090505)
    3838  - CIL      (included in the distribution)

  • Deliverables/D2.2/8051/myocamlbuild_config.ml

    r742 r818  
    1 let parser_lib = "/home/dpm/Projects/Cerco/Deliverables/D2.2/8051/lib"
     1let parser_lib = "/home/ayache/Downloads/Bol/Deliverables/D2.2/8051/lib"

  • Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml

    r743 r818  
    19351935  let status = serial_port_output status out_cont in
    19361936  let status = interrupts status in
    1937   let status = { status with previous_p1_val = get_bit status.p3 4;
    1938                    previous_p3_val = get_bit status.p3 5 } in
    1939     status
     1937  { status with previous_p1_val = get_bit status.p3 4;
     1938    previous_p3_val = get_bit status.p3 5 }
    19401939;;
    19411940
    … …  
    19691968;;
    19701969
     1970
    19711971let load_program p =
    19721972  let st = load p.ASM.code initialize in
    … …  
    19821982
    19831983let result st =
    1984   let i = BitVectors.int_of_vect st.dpl in
    1985   IntValue.Int8.of_int i
    1986 
    1987 let interpret print_result p =
    1988   if print_result then Printf.printf "8051: %!" ;
     1984  let dpl = st.dpl in
     1985  let dpr = st.dph in
     1986  let addr i = BitVectors.vect_of_int i `Seven in
     1987  let get_ireg i = Physical.Byte7Map.find (addr i) st.low_internal_ram in
     1988  let r00 = get_ireg 0 in
     1989  let r01 = get_ireg 1 in
     1990  let is = [dpl ; dpr ; r00 ; r01] in
     1991  let f i = IntValue.Int32.of_int (BitVectors.int_of_vect i) in
     1992  IntValue.Int32.merge (List.map f is)
     1993
     1994let interpret debug p =
     1995  Printf.printf "*** 8051 interpret ***\n%!" ;
    19891996  if p.ASM.has_main then
    19901997    let st = load_program p in
    … …  
    19932000    let st = execute callback st in
    19942001    let res = result st in
    1995     if print_result then
    1996       Printf.printf "%s\n%!" (IntValue.Int8.to_string res) ;
     2002    if debug then
     2003      Printf.printf "Result = %s\n%!" (IntValue.Int32.to_string res) ;
    19972004    (res, List.rev !trace)
    1998   else (IntValue.Int8.zero, [])
     2005  else (IntValue.Int32.zero, [])

  • Deliverables/D2.2/8051/src/ASM/I8051.ml

    r740 r818  
    66type opaccs =
    77  | Mul
    8   | Divu
    9   | Modu
     8  | DivuModu
    109
    1110type op1 =
    … …  
    2322let print_opaccs = function
    2423  | Mul -> "mul"
    25   | Divu -> "divu"
    26   | Modu -> "modu"
     24  | DivuModu -> "divu"
    2725
    2826let print_op1 = function
    … …  
    4139module Eval (Val : Value.S) = struct
    4240
    43   let opaccs = function
    44     | Mul -> Val.mul
    45     | Divu -> Val.divu
    46     | Modu -> Val.modulou
     41  let eval_int_mul size i1 i2 =
     42    let module Int = IntValue.Make (struct let size = 2 * size end) in
     43    match Int.break (Int.mul i1 i2) 2 with
     44      | res1 :: res2 :: _ -> (Val.of_int_repr res1, Val.of_int_repr res2)
     45      | _ -> assert false (* should be impossible *)
     46
     47  let eval_mul v1 v2 =
     48    if Val.is_int v1 && Val.is_int v2 then
     49      eval_int_mul Val.int_size (Val.to_int_repr v1) (Val.to_int_repr v2)
     50    else (Val.undef, Val.undef)
     51
     52  let opaccs op v1 v2 = match op with
     53    | Mul -> eval_mul v1 v2
     54    | DivuModu -> (Val.divu v1 v2, Val.modulou v1 v2)
    4755
    4856  let op1 = function
    … …  
    152160  | _ -> assert false (* impossible *)
    153161
    154 let sst = r03
    155 let st0 = r04
    156 let st1 = r05
     162let sst = r10
     163let st0 = r02
     164let st1 = r03
     165let st2 = r04
     166let st3 = r05
     167let sts = [st0 ; st1 ; st2 ; st3]
    157168let spl = r06
    158169let sph = r07
     170let rets = [dpl ; dph ; r00 ; r01]
     171
     172let isp_addr = 129
     173let isp_init = 47
    159174
    160175let set_of_list rl = List.fold_right RegisterSet.add rl RegisterSet.empty
    … …  
    169184
    170185let forbidden =
    171   set_of_list [(* a ; b ; dpl ; dph ; *) spl ; sph ; st0 ; st1 ; sst]
     186  set_of_list
     187    [a ; b ; dpl ; dph ; spl ; sph ; st0 ; st1 ; st2 ; st3 ; sst]
    172188
    173189let parameters =

  • Deliverables/D2.2/8051/src/ASM/I8051.mli

    r740 r818  
    44type opaccs =
    55  | Mul
    6   | Divu
    7   | Modu
     6  | DivuModu
    87
    98type op1 =
    … …  
    2423
    2524module Eval (Val : Value.S) : sig
    26   val opaccs : opaccs -> Val.t -> Val.t -> Val.t
     25  val opaccs : opaccs -> Val.t -> Val.t ->
     26               (Val.t (* first result (ACC) *) *
     27                Val.t (* second result (BACC) *))
    2728  val op1    : op1 -> Val.t -> Val.t
    2829  val op2    : Val.t (* carry *) -> op2 -> Val.t -> Val.t ->
    … …  
    4748val st0 : register
    4849val st1 : register
     50val st2 : register
     51val st3 : register
     52val sts : register list
     53val rets : register list
    4954val sst : register
    5055val carry : register (* only used for the liveness analysis *)
     56
     57val isp_addr : int
     58val isp_init : int
    5159
    5260val registers : RegisterSet.t

  • Deliverables/D2.2/8051/src/ASM/Pretty.ml

    r645 r818  
    100100  let f (s, pc) _ =
    101101    let (inst, new_pc, cost) = ASMInterpret.fetch mem pc in
    102     (Printf.sprintf "%s% 6s  %- 18s ;; %d  %s\n"
     102    (Printf.sprintf "%s% 6X:  %- 18s ;; %d  %s\n"
    103103       s
    104        ((string_of_int (BitVectors.int_of_vect pc)) ^ ":")
     104       (BitVectors.int_of_vect pc)
    105105       (pp_instruction inst)
    106106       cost

  • Deliverables/D2.2/8051/src/ERTL/ERTL.mli

    r740 r818  
    104104
    105105  (* Apply a binary operation that will later be translated in an operation on
    106      the accumulators. Parameters are the operation, the destination register,
    107      the source registers, and the label of the next statement. *)
    108   | St_opaccs of I8051.opaccs * Register.t * Register.t * Register.t * Label.t
     106     the accumulators, keeping only the result in ACC. Parameters are the
     107     operation, the destination register, the source registers, and the label of
     108     the next statement. *)
     109  | St_opaccsA of I8051.opaccs * Register.t * Register.t * Register.t * Label.t
     110
     111  (* Apply a binary operation that will later be translated in an operation on
     112     the accumulators, keeping only the result in BACC. Parameters are the
     113     operation, the destination register, the source registers, and the label of
     114     the next statement. *)
     115  | St_opaccsB of I8051.opaccs * Register.t * Register.t * Register.t * Label.t
    109116
    110117  (* Apply an unary operation. Parameters are the operation, the destination
    … …  
    119126     statement. *)
    120127  | St_clear_carry of Label.t
     128
     129  (* Set the carry flag to 1. Parameter is the label of the next statement. *)
     130  | St_set_carry of Label.t
    121131
    122132  (* Load from external memory. Parameters are the destination register, the
    … …  
    152162     the label to go to when the value is not 0, and the label to go to when the
    153163     value is 0. *)
    154   | St_condacc of Register.t * Label.t * Label.t
     164  | St_cond of Register.t * Label.t * Label.t
    155165
    156166  (* Transfer control to the address stored in the return address registers. *)

  • Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml

    r740 r818  
    197197
    198198let interpret_external mem f args = match InterpretExternal.t mem f args with
    199   | (mem', InterpretExternal.V v) -> (mem', [v])
     199  | (mem', InterpretExternal.V vs) -> (mem', vs)
    200200  | (mem', InterpretExternal.A addr) -> (mem', addr)
    201201
    202 let fetch_external_args st =
    203   (* TODO: this is bad when parameters are the empty list. *)
    204   [get_reg (Hdw (List.hd I8051.parameters)) st]
    205 
    206 let set_result st = function
    207   | [] -> assert false (* should be impossible: at least one value returned *)
    208   | [v] -> add_reg (Hdw I8051.dpl) v st
    209   | v1 :: v2 :: _ ->
    210     let st = add_reg (Hdw I8051.dpl) v1 st in
    211     add_reg (Hdw I8051.dph) v2 st
     202let fetch_external_args f st =
     203  let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
     204  let params = MiscPottier.prefix size I8051.parameters in
     205  List.map (fun r -> get_reg (Hdw r) st) params
     206
     207let set_result st vs =
     208  let f st (r, v) = add_reg (Hdw r) v st in
     209  List.fold_left f st (MiscPottier.combine I8051.rets vs)
    212210
    213211let interpret_external_call st f next_pc =
    214   let args = fetch_external_args st in
     212  let args = fetch_external_args f st in
    215213  let (mem, vs) = interpret_external st.mem f args in
    216214  let st = change_mem st mem in
    … …  
    316314      next_pc st lbl
    317315
    318     | ERTL.St_opaccs (opaccs, destr, srcr1, srcr2, lbl) ->
    319       let v =
     316    | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, lbl) ->
     317      let (v, _) =
     318        Eval.opaccs opaccs
     319          (get_reg (Psd srcr1) st)
     320          (get_reg (Psd srcr2) st) in
     321      let st = add_reg (Psd destr) v st in
     322      next_pc st lbl
     323
     324    | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, lbl) ->
     325      let (_, v) =
    320326        Eval.opaccs opaccs
    321327          (get_reg (Psd srcr1) st)
    … …  
    342348      next_pc st lbl
    343349
     350    | ERTL.St_set_carry lbl ->
     351      let st = change_carry st (Val.of_int 1) in
     352      next_pc st lbl
     353
    344354    | ERTL.St_load (destr, addr1, addr2, lbl) ->
    345355      let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
    … …  
    357367      interpret_call lbls_offs st f lbl
    358368
    359     | ERTL.St_condacc (srcr, lbl_true, lbl_false) ->
     369    | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
    360370      let v = get_reg (Psd srcr) st in
    361371      let lbl =
    … …  
    390400  Printf.printf "SP: %s\n%!" (Val.string_of_address (get_sp st)) ;
    391401  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
     402  Printf.printf "Carry: %s%!" (Val.to_string st.carry) ;
    392403  print_lenv st.lenv ;
    393404  print_renv st.renv ;
    … …  
    396407
    397408let compute_result st ret_regs =
    398   try
    399     let v = get_reg (Psd (List.hd ret_regs)) st in
    400     if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
    401     else IntValue.Int8.zero
    402   with Not_found -> IntValue.Int8.zero
     409  let vs = List.map (fun r -> get_reg (Psd r) st) ret_regs in
     410  let f res v = res && (Val.is_int v) in
     411  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
     412  if is_int vs then
     413    let chunks =
     414      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
     415    IntValue.Int32.merge chunks
     416  else IntValue.Int32.zero
    403417
    404418let rec iter_small_step debug lbls_offs st =
     419  let print_and_return_result (res, cost_labels) =
     420    if debug then Printf.printf "Result = %s\n%!"
     421      (IntValue.Int32.to_string res) ;
     422    (res, cost_labels) in
    405423  if debug then print_state lbls_offs st ;
    406424  match fetch_stmt lbls_offs st with
    407425    | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit ->
    408       (compute_result st ret_regs, List.rev st.trace)
     426      print_and_return_result (compute_result st ret_regs, List.rev st.trace)
    409427    | stmt ->
    410428      let st' = interpret_stmt lbls_offs st stmt in
    … …  
    414432let add_global_vars =
    415433  List.fold_left
    416     (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
     434    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
    417435
    418436let add_fun_defs =
    … …  
    472490
    473491let interpret debug p =
    474   if debug then Printf.printf "*** ERTL ***\n\n%!" ;
     492  Printf.printf "*** ERTL interpret ***\n%!" ;
    475493  match p.ERTL.main with
    476     | None -> (IntValue.Int8.zero, [])
     494    | None -> (IntValue.Int32.zero, [])
    477495    | Some main ->
    478496      let lbls_offs = labels_offsets p in

  • Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml

    r486 r818  
    7272    Printf.sprintf "move %s, %s --> %s"
    7373      (Register.print dstr) (Register.print srcr) lbl
    74   | ERTL.St_opaccs (opaccs, dstr, srcr1, srcr2, lbl) ->
    75     Printf.sprintf "%s %s, %s, %s --> %s"
     74  | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl) ->
     75    Printf.sprintf "%sA %s, %s, %s --> %s"
     76      (I8051.print_opaccs opaccs)
     77      (Register.print dstr)
     78      (Register.print srcr1)
     79      (Register.print srcr2)
     80      lbl
     81  | ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, lbl) ->
     82    Printf.sprintf "%sB %s, %s, %s --> %s"
    7683      (I8051.print_opaccs opaccs)
    7784      (Register.print dstr)
    … …  
    94101  | ERTL.St_clear_carry lbl ->
    95102    Printf.sprintf "clear CARRY --> %s" lbl
     103  | ERTL.St_set_carry lbl ->
     104    Printf.sprintf "set CARRY --> %s" lbl
    96105  | ERTL.St_load (dstr, addr1, addr2, lbl) ->
    97106    Printf.sprintf "load %s, (%s, %s) --> %s"
    … …  
    127136      (print_args args)
    128137*)
    129   | ERTL.St_condacc (srcr, lbl_true, lbl_false) ->
     138  | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
    130139    Printf.sprintf "branch %s <> 0 --> %s, %s"
    131140      (Register.print srcr) lbl_true lbl_false

  • Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml

    r740 r818  
    214214        move (lookup r1) (lookup r2) l
    215215
    216       | ERTL.St_opaccs (I8051.Modu, destr, srcr1, srcr2, l) ->
    217         let (hdw, l) = write destr l in
    218         let l = generate (LTL.St_from_acc (hdw, l)) in
    219         let l = generate (LTL.St_to_acc (I8051.b, l)) in
    220         let l = generate (LTL.St_opaccs (I8051.Divu, l)) in
    221         let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    222         let l = generate (LTL.St_from_acc (I8051.b, l)) in
    223         let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    224         LTL.St_skip l
    225 
    226       | ERTL.St_opaccs (opaccs, destr, srcr1, srcr2, l) ->
     216      | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) ->
    227217        let (hdw, l) = write destr l in
    228218        let l = generate (LTL.St_from_acc (hdw, l)) in
    … …  
    233223        LTL.St_skip l
    234224
     225      | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) ->
     226        let (hdw, l) = write destr l in
     227        let l = generate (LTL.St_from_acc (hdw, l)) in
     228        let l = generate (LTL.St_to_acc (I8051.b, l)) in
     229        let l = generate (LTL.St_opaccs (opaccs, l)) in
     230        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     231        let l = generate (LTL.St_from_acc (I8051.b, l)) in
     232        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     233        LTL.St_skip l
     234
    235235      | ERTL.St_op1 (op1, destr, srcr, l) ->
    236236        let (hdw, l) = write destr l in
    … …  
    251251      | ERTL.St_clear_carry l ->
    252252        LTL.St_clear_carry l
     253
     254      | ERTL.St_set_carry l ->
     255        LTL.St_set_carry l
    253256
    254257      | ERTL.St_load (destr, addr1, addr2, l) ->
    … …  
    280283        LTL.St_call_id (f, l)
    281284
    282       | ERTL.St_condacc (srcr, lbl_true, lbl_false) ->
     285      | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
    283286        let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
    284287        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in

  • Deliverables/D2.2/8051/src/ERTL/liveness.ml

    r486 r818  
    3030  | St_int (_, _, l)
    3131  | St_move (_, _, l)
    32   | St_opaccs (_, _, _, _, l)
     32  | St_opaccsA (_, _, _, _, l)
     33  | St_opaccsB (_, _, _, _, l)
    3334  | St_op1 (_, _, _, l)
    3435  | St_op2 (_, _, _, _, l)
    3536  | St_clear_carry l
     37  | St_set_carry l
    3638  | St_load (_, _, _, l)
    3739  | St_store (_, _, _, l)
    3840  | St_call_id (_, _, l) ->
    3941    Label.Set.singleton l
    40   | St_condacc (_, l1, l2) ->
     42  | St_cond (_, l1, l2) ->
    4143    Label.Set.add l1 (Label.Set.singleton l2)
    4244
    … …  
    115117  | St_cost _
    116118  | St_push _
    117   | St_clear_carry _
    118119  | St_store _
    119   | St_condacc _
     120  | St_cond _
    120121  | St_return _ ->
    121122    L.bottom
     123  | St_clear_carry _
     124  | St_set_carry _ ->
     125    Register.Set.empty, I8051.RegisterSet.singleton I8051.carry
    122126  | St_op2 (I8051.Add, r, _, _, _)
    123127  | St_op2 (I8051.Addc, r, _, _, _)
    124128  | St_op2 (I8051.Sub, r, _, _, _) ->
    125129    L.join (L.hsingleton I8051.carry) (L.psingleton r)
    126   | St_op1 (I8051.Inc, r, _, _) ->
    127     L.join (L.hsingleton I8051.carry) (L.psingleton r)
     130  | St_op1 (I8051.Inc, r, _, _)
    128131  | St_get_hdw (r, _, _)
    129132  | St_framesize (r, _)
    … …  
    133136  | St_addrL (r, _, _)
    134137  | St_move (r, _, _)
    135   | St_opaccs (_, r, _, _, _)
     138  | St_opaccsA (_, r, _, _, _)
     139  | St_opaccsB (_, r, _, _, _)
    136140  | St_op1 (_, r, _, _)
    137141  | St_op2 (_, r, _, _, _)
    … …  
    153157(* This is the set of variables used at (read by) a statement. *)
    154158
    155 let dptr =
    156   I8051.RegisterSet.add I8051.dph (I8051.RegisterSet.singleton I8051.dpl)
     159let set_of_list =
     160  let f set r = I8051.RegisterSet.add r set in
     161  List.fold_left f I8051.RegisterSet.empty
     162
     163let ret_regs = set_of_list I8051.rets
    157164
    158165let used (stmt : statement) : L.t =
    … …  
    166173  | St_addrL _
    167174  | St_int _
    168   | St_clear_carry _ ->
     175  | St_clear_carry _
     176  | St_set_carry _ ->
    169177    L.bottom
    170178  | St_call_id (_, nparams, _) ->
    … …  
    179187  | St_move (_, r, _)
    180188  | St_op1 (_, _, r, _)
    181   | St_condacc (r, _, _) ->
     189  | St_cond (r, _, _) ->
    182190    L.psingleton r
    183191  | St_op2 (I8051.Addc, _, r1, r2, _) ->
    184192    L.join (L.join (L.psingleton r1) (L.psingleton r2))
    185193      (L.hsingleton I8051.carry)
    186   | St_opaccs (_, _, r1, r2, _)
     194  | St_opaccsA (_, _, r1, r2, _)
     195  | St_opaccsB (_, _, r1, r2, _)
    187196  | St_op2 (_, _, r1, r2, _)
    188197  | St_load (_, r1, r2, _) ->
    … …  
    194203    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)   
    195204  | St_return _ ->
    196     Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved dptr
     205    Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved ret_regs
    197206
    198207(* A statement is considered pure if it has no side effect, that is, if
    … …  
    218227  | St_push _
    219228  | St_clear_carry _
     229  | St_set_carry _
    220230  | St_store _
    221231  | St_call_id _
    222   | St_condacc _
     232  | St_cond _
    223233  | St_return _ ->
    224234    None
    … …  
    229239  | St_addrL (r, _, l)
    230240  | St_move (r, _, l)
    231   | St_opaccs (_, r, _, _, l)
     241  | St_opaccsA (_, r, _, _, l)
     242  | St_opaccsB (_, r, _, _, l)
    232243  | St_op1 (_, r, _, l)
    233244  | St_op2 (_, r, _, _, l)

  • Deliverables/D2.2/8051/src/ERTL/uses.ml

    r486 r818  
    2424  | St_delframe _
    2525  | St_clear_carry _
     26  | St_set_carry _
    2627  | St_call_id _
    2728  | St_return _ ->
    … …  
    3536  | St_addrH (r, _, _)
    3637  | St_addrL (r, _, _)
    37   | St_condacc (r, _, _) ->
     38  | St_cond (r, _, _) ->
    3839    count r uses
    3940  | St_move (r1, r2, _)
    4041  | St_op1 (_, r1, r2, _) ->
    4142    count r1 (count r2 uses)
    42   | St_opaccs (_, r1, r2, r3, _)
     43  | St_opaccsA (_, r1, r2, r3, _)
     44  | St_opaccsB (_, r1, r2, r3, _)
    4345  | St_op2 (_, r1, r2, r3, _)
    4446  | St_load (r1, r2, r3, _)

  • Deliverables/D2.2/8051/src/LIN/LIN.mli

    r486 r818  
    5454  | St_clear_carry
    5555
     56  (* Set the carry flag to 1. *)
     57  | St_set_carry
     58
    5659  (* Load from external memory (address in DPTR) to the accumulator. *)
    5760  | St_load

  • Deliverables/D2.2/8051/src/LIN/LINInterpret.ml

    r740 r818  
    148148
    149149let interpret_external mem f args = match InterpretExternal.t mem f args with
    150   | (mem', InterpretExternal.V v) -> (mem', [v])
     150  | (mem', InterpretExternal.V vs) -> (mem', vs)
    151151  | (mem', InterpretExternal.A addr) -> (mem', addr)
    152152
    153 let fetch_external_args st =
    154   (* TODO: this is bad when parameters are the empty list. *)
    155   [get_reg (List.hd I8051.parameters) st]
    156 
    157 let set_result st = function
    158   | [] -> assert false (* should be impossible: at least one value returned *)
    159   | [v] -> add_reg I8051.dpl v st
    160   | v1 :: v2 :: _ ->
    161     let st = add_reg I8051.dpl v1 st in
    162     add_reg I8051.dph v2 st
     153let fetch_external_args f st =
     154  let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
     155  let params = MiscPottier.prefix size I8051.parameters in
     156  List.map (fun r -> get_reg r st) params
     157
     158let set_result st vs =
     159  let f st (r, v) = add_reg r v st in
     160  List.fold_left f st (MiscPottier.combine I8051.rets vs)
    163161
    164162let interpret_external_call st f =
    165   let args = fetch_external_args st in
     163  let args = fetch_external_args f st in
    166164  let (mem, vs) = interpret_external st.mem f args in
    167165  let st = change_mem st mem in
    … …  
    230228
    231229    | LIN.St_opaccs opaccs ->
    232       let v =
     230      let (a, b) =
    233231        Eval.opaccs opaccs
    234232          (get_reg I8051.a st)
    235233          (get_reg I8051.b st) in
    236       let st = add_reg I8051.a v st in
     234      let st = add_reg I8051.a a st in
     235      let st = add_reg I8051.b b st in
    237236      next_pc st
    238237
    … …  
    255254      next_pc st
    256255
     256    | LIN.St_set_carry ->
     257      let st = change_carry st (Val.of_int 1) in
     258      next_pc st
     259
    257260    | LIN.St_load ->
    258261      let addr = dptr st in
    … …  
    282285
    283286let compute_result st =
    284   let v = get_reg I8051.dpl st in
    285   if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
    286   else IntValue.Int8.zero
     287  let vs = List.map (fun r -> get_reg r st) I8051.rets in
     288  let f res v = res && (Val.is_int v) in
     289  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
     290  if is_int vs then
     291    let chunks =
     292      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
     293    IntValue.Int32.merge chunks
     294  else IntValue.Int32.zero
    287295
    288296let rec iter_small_step debug st =
     297  let print_and_return_result (res, cost_labels) =
     298    if debug then Printf.printf "Result = %s\n%!"
     299      (IntValue.Int32.to_string res) ;
     300    (res, cost_labels) in
    289301  if debug then print_state st ;
    290302  match fetch_stmt st with
    291303    | LIN.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
    292       (compute_result st, List.rev st.trace)
     304      print_and_return_result (compute_result st, List.rev st.trace)
    293305    | stmt ->
    294306      let st' = interpret_stmt st stmt in
    … …  
    298310let add_global_vars =
    299311  List.fold_left
    300     (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
     312    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
    301313
    302314let add_fun_defs =
    … …  
    354366
    355367let interpret debug p =
    356   if debug then Printf.printf "*** LIN ***\n\n%!" ;
     368  Printf.printf "*** LIN interpret ***\n%!" ;
    357369  match p.LIN.main with
    358     | None -> (IntValue.Int8.zero, [])
     370    | None -> (IntValue.Int32.zero, [])
    359371    | Some main ->
    360372      let st = empty_state in

  • Deliverables/D2.2/8051/src/LIN/LINPrinter.ml

    r486 r818  
    4848      (I8051.print_op2 op2) print_a (print_reg srcr)
    4949  | LIN.St_clear_carry -> "clear CARRY"
     50  | LIN.St_set_carry -> "set CARRY"
    5051  | LIN.St_load ->
    5152    Printf.sprintf "movex %s, @DPTR" print_a

  • Deliverables/D2.2/8051/src/LIN/LINPrinter.mli

    r486 r818  
    22(** This module provides a function to print [LIN] programs. *)
    33
     4val print_statement : LIN.statement -> string
     5
    46val print_program: LIN.program -> string

  • Deliverables/D2.2/8051/src/LIN/LINToASM.ml

    r741 r818  
    11
    22(** This module translates a [LIN] program into a [ASM] program. *)
     3
     4
     5let error_prefix = "LIN to ASM"
     6let error s = Error.global_error error_prefix s
    37
    48
    … …  
    5256  | LIN.St_push ->
    5357    [`PUSH acc_addr]
     58  | LIN.St_addr x when List.mem_assoc x glbls_addr ->
     59    [`MOV (`U4 (`DPTR, data16_of_int (List.assoc x glbls_addr)))]
    5460  | LIN.St_addr x ->
    55     [`MOV (`U4 (`DPTR, data16_of_int (List.assoc x glbls_addr)))]
     61    error ("unknown global " ^ x ^ ".")
    5662  | LIN.St_from_acc r ->
    5763    [`MOV (`U3 (I8051.reg_addr r, `A))]
    … …  
    6066  | LIN.St_opaccs I8051.Mul ->
    6167    [`MUL (`A, `B)]
    62   | LIN.St_opaccs I8051.Divu ->
     68  | LIN.St_opaccs I8051.DivuModu ->
    6369    [`DIV (`A, `B)]
    64   | LIN.St_opaccs I8051.Modu ->
    65     assert false (* Should have been translated before. *)
    6670  | LIN.St_op1 I8051.Cmpl ->
    6771    [`CPL `A]
    … …  
    8286  | LIN.St_clear_carry ->
    8387    [`CLR `C]
     88  | LIN.St_set_carry ->
     89    [`SETB `C]
    8490  | LIN.St_load ->
    8591    [`MOVX (`U1 (`A, `EXT_IND_DPTR))]
    … …  
    99105let translate_fun_def glbls_addr (id, def) = match def with
    100106  | LIN.F_int code -> (`Label id) :: (translate_code glbls_addr code)
    101   | _ -> []
     107  | LIN.F_ext ext ->
     108    error ("potential call to unsupported external " ^ ext.AST.ef_tag ^ ".")
    102109
    103110let translate_functs glbls_addr exit_label main functs =
    104111  let preamble = match main with
    105112    | None -> []
    106     | Some main -> [`Call main ; `Label exit_label ; `Jmp exit_label] in
     113    | Some main ->
     114      [`MOV (`U3 (`DIRECT (byte_of_int I8051.isp_addr),
     115                  data_of_int I8051.isp_init)) ;
     116       `Call main ;
     117       `Label exit_label ; `Jmp exit_label] in
    107118  preamble @
    108     (List.flatten (List.map (translate_fun_def glbls_addr) functs))
     119  (List.flatten (List.map (translate_fun_def glbls_addr) functs))
    109120
    110121

  • Deliverables/D2.2/8051/src/LTL/LTL.mli

    r486 r818  
    6060  | St_clear_carry of Label.t
    6161
     62  (* Set the carry flag to 1. Parameter is the label of the next statement. *)
     63  | St_set_carry of Label.t
     64
    6265  (* Load from external memory (address in DPTR) to the accumulator. Parameter
    6366     is the label of the next statement. *)

  • Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

    r740 r818  
    177177
    178178let interpret_external mem f args = match InterpretExternal.t mem f args with
    179   | (mem', InterpretExternal.V v) -> (mem', [v])
     179  | (mem', InterpretExternal.V vs) -> (mem', vs)
    180180  | (mem', InterpretExternal.A addr) -> (mem', addr)
    181181
    182 let fetch_external_args st =
    183   (* TODO: this is bad when parameters are the empty list. *)
    184   [get_reg (List.hd I8051.parameters) st]
    185 
    186 let set_result st = function
    187   | [] -> assert false (* should be impossible: at least one value returned *)
    188   | [v] -> add_reg I8051.dpl v st
    189   | v1 :: v2 :: _ ->
    190     let st = add_reg I8051.dpl v1 st in
    191     add_reg I8051.dph v2 st
     182let fetch_external_args f st =
     183  let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
     184  let params = MiscPottier.prefix size I8051.parameters in
     185  List.map (fun r -> get_reg r st) params
     186
     187let set_result st vs =
     188  let f st (r, v) = add_reg r v st in
     189  List.fold_left f st (MiscPottier.combine I8051.rets vs)
    192190
    193191let interpret_external_call st f next_pc =
    194   let args = fetch_external_args st in
     192  let args = fetch_external_args f st in
    195193  let (mem, vs) = interpret_external st.mem f args in
    196194  let st = change_mem st mem in
    … …  
    262260
    263261    | LTL.St_opaccs (opaccs, lbl) ->
    264       let v =
     262      let (a, b) =
    265263        Eval.opaccs opaccs
    266264          (get_reg I8051.a st)
    267265          (get_reg I8051.b st) in
    268       let st = add_reg I8051.a v st in
     266      let st = add_reg I8051.a a st in
     267      let st = add_reg I8051.b b st in
    269268      next_pc st lbl
    270269
    … …  
    287286      next_pc st lbl
    288287
     288    | LTL.St_set_carry lbl ->
     289      let st = change_carry st (Val.of_int 1) in
     290      next_pc st lbl
     291
    289292    | LTL.St_load lbl ->
    290293      let addr = dptr st in
    … …  
    316319
    317320let compute_result st =
    318   let v = get_reg I8051.dpl st in
    319   if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
    320   else IntValue.Int8.zero
     321  let vs = List.map (fun r -> get_reg r st) I8051.rets in
     322  let f res v = res && (Val.is_int v) in
     323  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
     324  if is_int vs then
     325    let chunks =
     326      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
     327    IntValue.Int32.merge chunks
     328  else IntValue.Int32.zero
    321329
    322330let rec iter_small_step debug lbls_offs st =
     331  let print_and_return_result (res, cost_labels) =
     332    if debug then Printf.printf "Result = %s\n%!"
     333      (IntValue.Int32.to_string res) ;
     334    (res, cost_labels) in
    323335  if debug then print_state lbls_offs st ;
    324336  match fetch_stmt lbls_offs st with
    325337    | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
    326       (compute_result st, List.rev st.trace)
     338      print_and_return_result (compute_result st, List.rev st.trace)
    327339    | stmt ->
    328340      let st' = interpret_stmt lbls_offs st stmt in
    … …  
    332344let add_global_vars =
    333345  List.fold_left
    334     (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
     346    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
    335347
    336348let add_fun_defs =
    … …  
    390402
    391403let interpret debug p =
    392   if debug then Printf.printf "*** LTL ***\n\n%!" ;
     404  Printf.printf "*** LTL interpret ***\n%!" ;
    393405  match p.LTL.main with
    394406    | None -> (IntValue.Int8.zero, [])

  • Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml

    r486 r818  
    4848  | LTL.St_clear_carry lbl ->
    4949    Printf.sprintf "clear CARRY --> %s" lbl
     50  | LTL.St_set_carry lbl ->
     51    Printf.sprintf "set CARRY --> %s" lbl
    5052  | LTL.St_load lbl ->
    5153    Printf.sprintf "movex %s, @DPTR --> %s" print_a lbl

  • Deliverables/D2.2/8051/src/LTL/LTLToLIN.ml

    r486 r818  
    3232  | LTL.St_clear_carry _ ->
    3333    LIN.St_clear_carry
     34  | LTL.St_set_carry _ ->
     35    LIN.St_set_carry
    3436  | LTL.St_from_acc (r, _) ->
    3537    LIN.St_from_acc (r)

  • Deliverables/D2.2/8051/src/LTL/LTLToLINI.ml

    r486 r818  
    127127        | LTL.St_op2 (_, _, l)
    128128        | LTL.St_clear_carry l
     129        | LTL.St_set_carry l
    129130        | LTL.St_load l
    130131        | LTL.St_store l

  • Deliverables/D2.2/8051/src/LTL/branch.ml

    r486 r818  
    6262    | LTL.St_clear_carry l ->
    6363      LTL.St_clear_carry (rep l)
     64    | LTL.St_set_carry l ->
     65      LTL.St_set_carry (rep l)
    6466    | LTL.St_from_acc (r, l) ->
    6567      LTL.St_from_acc (r, rep l)

  • Deliverables/D2.2/8051/src/RTL/RTL.mli

    r740 r818  
    3535
    3636  (* Apply a binary operation that will later be translated in an operation on
    37      the accumulators. Parameters are the operation, the destination register,
    38      the source registers, and the label of the next statement. *)
    39   | St_opaccs of I8051.opaccs * Register.t * Register.t * Register.t * Label.t
     37     the accumulators. Parameters are the operation, the destination registers
     38     (ACC first, BACC second), the source registers, and the label of the next
     39     statement. *)
     40  | St_opaccs of I8051.opaccs * Register.t * Register.t *
     41                                Register.t * Register.t * Label.t
    4042
    4143  (* Apply an unary operation. Parameters are the operation, the destination
    … …  
    5052     statement. *)
    5153  | St_clear_carry of Label.t
     54
     55  (* Set the carry flag to 1. Parameter is the label of the next statement. *)
     56  | St_set_carry of Label.t
    5257
    5358  (* Load from external memory. Parameters are the destination register, the
    … …  
    8489     the label to go to when the value is not 0, and the label to go to when the
    8590     value is 0. *)
    86   | St_condacc of Register.t * Label.t * Label.t
     91  | St_cond of Register.t * Label.t * Label.t
    8792
    88   (* Return the value of some registers. Their may be no register in case of
    89      procedures, one register when returning an integer, or two registers when
    90      returning an address (low bytes first). *)
     93  (* Return the value of some registers (low bytes first). *)
    9194  | St_return of registers
    9295
    … …  
    97100    { f_luniverse : Label.Gen.universe ;
    98101      f_runiverse : Register.universe ;
    99       f_sig       : AST.signature ;
    100102      f_result    : Register.t list (* low byte first *) ;
    101103      f_params    : Register.t list ;

  • Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml

    r740 r818  
    144144          [get_local_value lenv srcr]
    145145
    146       | RTL.St_opaccs (opaccs, destr, srcr1, srcr2, lbl) ->
    147         let v =
     146      | RTL.St_opaccs (opaccs, destr1, destr2, srcr1, srcr2, lbl) ->
     147        let (v1, v2) =
    148148          Eval.opaccs opaccs
    149149            (get_local_value lenv srcr1)
    150150            (get_local_value lenv srcr2) in
    151         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
     151        assign_state sfrs graph lbl sp lenv carry mem trace
     152          [destr1 ; destr2] [v1 ; v2]
    152153
    153154      | RTL.St_op1 (op1, destr, srcr, lbl) ->
    … …  
    164165      | RTL.St_clear_carry lbl ->
    165166        State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace)
     167
     168      | RTL.St_set_carry lbl ->
     169        State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, trace)
    166170
    167171      | RTL.St_load (destr, addr1, addr2, lbl) ->
    … …  
    205209        CallState (sfrs, f_def, args, mem, trace)
    206210
    207       | RTL.St_condacc (srcr, lbl_true, lbl_false) ->
     211      | RTL.St_cond (srcr, lbl_true, lbl_false) ->
    208212        let v = get_local_value lenv srcr in
    209213        branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v
    … …  
    218222
    219223let interpret_external mem f args = match InterpretExternal.t mem f args with
    220   | (mem', InterpretExternal.V v) -> (mem', [v])
     224  | (mem', InterpretExternal.V vs) -> (mem', vs)
    221225  | (mem', InterpretExternal.A addr) -> (mem', addr)
    222226
    … …  
    273277
    274278let compute_result vs =
    275   try
    276     let v = List.hd vs in
    277     if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
    278     else IntValue.Int8.zero
    279   with Not_found -> IntValue.Int8.zero
     279  let f res v = res && (Val.is_int v) in
     280  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
     281  if is_int vs then
     282    let chunks =
     283      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
     284    IntValue.Int32.merge chunks
     285  else IntValue.Int32.zero
    280286
    281287let rec iter_small_step debug st =
     288  let print_and_return_result (res, cost_labels) =
     289    if debug then Printf.printf "Result = %s\n%!"
     290      (IntValue.Int32.to_string res) ;
     291    (res, cost_labels) in
    282292  if debug then print_state st ;
    283293  match small_step st with
    284     | ReturnState ([], vs, mem, trace) -> (compute_result vs, List.rev trace)
     294    | ReturnState ([], vs, mem, trace) ->
     295      print_and_return_result (compute_result vs, List.rev trace)
    285296    | st' -> iter_small_step debug st'
    286297
    … …  
    288299let add_global_vars =
    289300  List.fold_left
    290     (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
     301    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
    291302
    292303let add_fun_defs =
    … …  
    304315
    305316let interpret debug p =
    306   if debug then Printf.printf "*** RTL ***\n\n%!" ;
     317  Printf.printf "*** RTL interpret ***\n%!" ;
    307318  match p.RTL.main with
    308     | None -> (IntValue.Int8.zero, [])
     319    | None -> (IntValue.Int32.zero, [])
    309320    | Some main ->
    310321      let mem = init_mem p in

  • Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml

    r486 r818  
    5555    Printf.sprintf "move %s, %s --> %s"
    5656      (print_reg dstr) (print_reg srcr) lbl
    57   | RTL.St_opaccs (opaccs, dstr, srcr1, srcr2, lbl) ->
    58     Printf.sprintf "%s %s, %s, %s --> %s"
     57  | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl) ->
     58    Printf.sprintf "%s (%s, %s) %s, %s --> %s"
    5959      (I8051.print_opaccs opaccs)
    60       (print_reg dstr)
     60      (print_reg dstr1)
     61      (print_reg dstr2)
    6162      (print_reg srcr1)
    6263      (print_reg srcr2)
    … …  
    7475  | RTL.St_clear_carry lbl ->
    7576    Printf.sprintf "clear CARRY --> %s" lbl
     77  | RTL.St_set_carry lbl ->
     78    Printf.sprintf "set CARRY --> %s" lbl
    7679  | RTL.St_load (dstr, addr1, addr2, lbl) ->
    7780    Printf.sprintf "load %s, (%s, %s) --> %s"
    … …  
    108111      (print_reg f2)
    109112      (print_args args)
    110   | RTL.St_condacc (srcr, lbl_true, lbl_false) ->
     113  | RTL.St_cond (srcr, lbl_true, lbl_false) ->
    111114    Printf.sprintf "branch %s <> 0 --> %s, %s"
    112115      (print_reg srcr) lbl_true lbl_false
    … …  
    128131
    129132  Printf.sprintf
    130     "%s\"%s\"%s: %s\n%slocals: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"
     133    "%s\"%s\"%s\n%slocals: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"
    131134    (n_spaces n)
    132135    f
    133136    (print_params def.RTL.f_params)
    134     (Primitive.print_sig def.RTL.f_sig)
    135137    (n_spaces (n+2))
    136138    (print_locals def.RTL.f_locals)

  • Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

    r740 r818  
    3434  | ERTL.St_int (r, i, _) -> ERTL.St_int (r, i, lbl)
    3535  | ERTL.St_move (r1, r2, _) -> ERTL.St_move (r1, r2, lbl)
    36   | ERTL.St_opaccs (opaccs, dstr, srcr1, srcr2, _) ->
    37     ERTL.St_opaccs (opaccs, dstr, srcr1, srcr2, lbl)
     36  | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, _) ->
     37    ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl)
     38  | ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, _) ->
     39    ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, lbl)
    3840  | ERTL.St_op1 (op1, dstr, srcr, _) -> ERTL.St_op1 (op1, dstr, srcr, lbl)
    3941  | ERTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
    4042    ERTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
    4143  | ERTL.St_clear_carry _ -> ERTL.St_clear_carry lbl
     44  | ERTL.St_set_carry _ -> ERTL.St_set_carry lbl
    4245  | ERTL.St_load (dstrs, addr1, addr2, _) ->
    4346    ERTL.St_load (dstrs, addr1, addr2, lbl)
    … …  
    4548    ERTL.St_store (addr1, addr2, srcrs, lbl)
    4649  | ERTL.St_call_id (f, nb_args, _) -> ERTL.St_call_id (f, nb_args, lbl)
    47   | ERTL.St_condacc _ as inst -> inst
     50  | ERTL.St_cond _ as inst -> inst
    4851  | ERTL.St_return _ as inst -> inst
    4952
    … …  
    5255
    5356let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with
    54   | [] -> def
     57  | [] -> add_graph start_lbl (ERTL.St_skip dest_lbl) def
    5558  | [stmt] ->
    5659    add_graph start_lbl (change_label dest_lbl stmt) def
    … …  
    6669let rec add_translates translate_list start_lbl dest_lbl def =
    6770  match translate_list with
    68     | [] -> def
     71    | [] -> add_graph start_lbl (ERTL.St_skip dest_lbl) def
    6972    | [trans] -> trans start_lbl dest_lbl def
    7073    | trans :: translate_list ->
    … …  
    168171   before jumping out of the function. *)
    169172
    170 let save_return ret_regs = match ret_regs with
    171   | [] -> [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl]
    172   | [r] ->
    173     [fun start_lbl dest_lbl def ->
    174       let (def, r_tmp) = fresh_reg def in
    175       adds_graph [ERTL.St_int (r_tmp, 0, start_lbl) ;
    176                   ERTL.St_set_hdw (I8051.st0, r, start_lbl) ;
    177                   ERTL.St_set_hdw (I8051.st1, r_tmp, start_lbl)]
    178         start_lbl dest_lbl def]
    179   | r1 :: r2 :: _ ->
    180     [(fun start_lbl ->
    181       adds_graph [ERTL.St_set_hdw (I8051.st0, r1, start_lbl) ;
    182                   ERTL.St_set_hdw (I8051.st1, r2, start_lbl)] start_lbl)]
     173let save_return ret_regs start_lbl dest_lbl def =
     174  let (def, tmpr) = fresh_reg def in
     175  let ((common1, rest1), (common2, _)) =
     176    MiscPottier.reduce I8051.sts ret_regs in
     177  let init_tmpr = ERTL.St_int (tmpr, 0, start_lbl) in
     178  let f_save st r = ERTL.St_set_hdw (st, r, start_lbl) in
     179  let saves = List.map2 f_save common1 common2 in
     180  let f_default st = ERTL.St_set_hdw (st, tmpr, start_lbl) in
     181  let defaults = List.map f_default rest1 in
     182  adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
     183
     184let assign_result start_lbl =
     185  let ((common1, _), (common2, _)) = MiscPottier.reduce I8051.rets I8051.sts in
     186  let f ret st = ERTL.St_hdw_to_hdw (ret, st, start_lbl) in
     187  let insts = List.map2 f common1 common2 in
     188  adds_graph insts start_lbl
    183189
    184190let add_epilogue ret_regs sral srah sregs def =
    … …  
    190196      ([adds_graph [ERTL.St_comment ("Epilogue", start_lbl)]] @
    191197       (* save return value *)
    192        (save_return ret_regs) @
     198       [save_return ret_regs] @
    193199       (* restore callee-saved registers *)
    194200       [adds_graph [ERTL.St_comment ("Restore callee-saved registers",
    … …  
    204210       (* assign the result to actual return registers *)
    205211       [adds_graph [ERTL.St_comment ("Set result", start_lbl)]] @
    206        [adds_graph [ERTL.St_hdw_to_hdw (I8051.dpl, I8051.st0, start_lbl) ;
    207                     ERTL.St_hdw_to_hdw (I8051.dph, I8051.st1, start_lbl) ;
    208                     ERTL.St_comment ("End Epilogue", start_lbl)]])
     212       [assign_result] @
     213       [adds_graph [ERTL.St_comment ("End Epilogue", start_lbl)]])
    209214      start_lbl tmp_lbl def in
    210215  let def = add_graph tmp_lbl last_stmt def in
    … …  
    243248  let (def, tmpr) = fresh_reg def in
    244249  adds_graph
    245     [ERTL.St_int (addr2, off+I8051.int_size, start_lbl) ;
     250    [ERTL.St_int (addr1, off+I8051.int_size, start_lbl) ;
    246251     ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
    247252     ERTL.St_clear_carry start_lbl ;
    … …  
    275280   pseudo-register. *)
    276281
    277 let fetch_result ret_regs start_lbl = match ret_regs with
    278   | [] -> adds_graph [ERTL.St_skip start_lbl] start_lbl
    279   | [r] ->
    280       adds_graph
    281       [ERTL.St_hdw_to_hdw (I8051.st0, I8051.dpl, start_lbl) ;
    282        ERTL.St_get_hdw (r, I8051.st0, start_lbl)]
    283       start_lbl
    284   | r1 :: r2 :: _ ->
    285     adds_graph
    286       [ERTL.St_hdw_to_hdw (I8051.st0, I8051.dpl, start_lbl) ;
    287        ERTL.St_hdw_to_hdw (I8051.st1, I8051.dph, start_lbl) ;
    288        ERTL.St_get_hdw (r1, I8051.st0, start_lbl) ;
    289        ERTL.St_get_hdw (r2, I8051.st1, start_lbl)]
    290       start_lbl
     282let fetch_result ret_regs start_lbl =
     283  let ((common1, _), (common2, _)) = MiscPottier.reduce I8051.sts I8051.rets in
     284  let f_save st ret = ERTL.St_hdw_to_hdw (st, ret, start_lbl) in
     285  let saves = List.map2 f_save common1 common2 in
     286  let ((common1, _), (common2, _)) = MiscPottier.reduce ret_regs I8051.sts in
     287  let f_restore r st = ERTL.St_get_hdw (r, st, start_lbl) in
     288  let restores = List.map2 f_restore common1 common2 in
     289  adds_graph (saves @ restores) start_lbl
    291290
    292291(* When calling a function, we need to set its parameters in specific locations:
    … …  
    299298    ([adds_graph [ERTL.St_comment ("Starting a call", start_lbl)] ;
    300299      adds_graph [ERTL.St_comment ("Setting up parameters", start_lbl)]] @
    301         set_params args @
    302         [adds_graph [ERTL.St_call_id (f, nb_args, start_lbl)] ;
    303          adds_graph [ERTL.St_comment ("Fetching result", start_lbl)] ;
    304          fetch_result ret_regs])
     300     set_params args @
     301     [adds_graph [ERTL.St_call_id (f, nb_args, start_lbl)] ;
     302      adds_graph [ERTL.St_comment ("Fetching result", start_lbl)] ;
     303      fetch_result ret_regs ;
     304      adds_graph [ERTL.St_comment ("End of call sequence", start_lbl)]])
    305305    start_lbl dest_lbl def
    306306
    … …  
    334334    add_graph lbl (ERTL.St_move (r1, r2, lbl')) def
    335335
    336   | RTL.St_opaccs (op, destr, srcr1, srcr2, lbl') ->
    337     add_graph lbl (ERTL.St_opaccs (op, destr, srcr1, srcr2, lbl')) def
     336  | RTL.St_opaccs (op, destr1, destr2, srcr1, srcr2, lbl') ->
     337    adds_graph [ERTL.St_opaccsA (op, destr1, srcr1, srcr2, lbl) ;
     338                ERTL.St_opaccsB (op, destr2, srcr1, srcr2, lbl) ;]
     339      lbl lbl' def
    338340
    339341  | RTL.St_op1 (op1, destr, srcr, lbl') ->
    … …  
    345347  | RTL.St_clear_carry lbl' ->
    346348    add_graph lbl (ERTL.St_clear_carry lbl') def
     349
     350  | RTL.St_set_carry lbl' ->
     351    add_graph lbl (ERTL.St_set_carry lbl') def
    347352
    348353  | RTL.St_load (destr, addr1, addr2, lbl') ->
    … …  
    366371  *)
    367372
    368   | RTL.St_condacc (srcr, lbl_true, lbl_false) ->
    369     add_graph lbl (ERTL.St_condacc (srcr, lbl_true, lbl_false)) def
     373  | RTL.St_cond (srcr, lbl_true, lbl_false) ->
     374    add_graph lbl (ERTL.St_cond (srcr, lbl_true, lbl_false)) def
    370375
    371376  | RTL.St_return ret_regs ->
    … …  
    427432    | ERTL.St_pop (_, lbl) | ERTL.St_push (_, lbl) | ERTL.St_addrH (_, _, lbl)
    428433    | ERTL.St_addrL (_, _, lbl) | ERTL.St_int (_, _, lbl)
    429     | ERTL.St_move (_, _, lbl) | ERTL.St_opaccs (_, _, _, _, lbl)
     434    | ERTL.St_move (_, _, lbl) | ERTL.St_opaccsA (_, _, _, _, lbl)
     435    | ERTL.St_opaccsB (_, _, _, _, lbl)
    430436    | ERTL.St_op1 (_, _, _, lbl) | ERTL.St_op2 (_, _, _, _, lbl)
    431     | ERTL.St_clear_carry lbl | ERTL.St_load (_, _, _, lbl)
     437    | ERTL.St_clear_carry lbl | ERTL.St_set_carry lbl
     438    | ERTL.St_load (_, _, _, lbl)
    432439    | ERTL.St_store (_, _, _, lbl) | ERTL.St_call_id (_, _, lbl)
    433440    | ERTL.St_newframe lbl | ERTL.St_delframe lbl | ERTL.St_framesize (_, lbl)
    434441      ->
    435442      aux lbl
    436     | ERTL.St_condacc _ | ERTL.St_return _ ->
     443    | ERTL.St_cond _ | ERTL.St_return _ ->
    437444      (* No cost label found (no labelling performed). Indeed, the first cost
    438445         label must after some linear instructions. *)

  • 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 }

  • Deliverables/D2.2/8051/src/acc.ml

    r740 r818  
    88    1. Parse.
    99
    10     2. Labelize.
     10    2. Add runtime functions.
    1111
    12     3. Compile to the target language.
     12    3. Labelize.
     13
     14    4. Compile to the target language.
    1315       (And keep track of annotations if required).
    1416 
    15     4. Annotate the input program with collected costs.
     17    5. Annotate the input program with collected costs.
    1618
    17     5. Save the annotated input program.
     19    6. Save the annotated input program.
    1820
    1921    Optionnally, we can interpret the intermediate programs
    … …  
    2527  let tgt_language    = Options.get_target_language () in
    2628  let input_ast       = Languages.parse src_language filename in
     29  let input_ast       = Languages.add_runtime input_ast in
    2730  let input_ast       = Languages.labelize input_ast in
    2831  let (exact_output, output_filename) = match Options.get_output_files () with
    … …  
    5356  if Options.interpretation_requested () || Options.is_debug_enabled () then
    5457    begin
    55       let asts = input_ast :: target_asts in
    56       let label_traces = List.map (Languages.interpret false) asts in
     58      let asts = target_asts in
     59      let debug = Options.is_debug_enabled () in
     60      let label_traces = List.map (Languages.interpret debug) asts in
    5761      Printf.eprintf "Checking execution traces...%!";
    5862      Checker.same_traces (List.combine asts label_traces);

  • Deliverables/D2.2/8051/src/clight/clight.mli

    r486 r818  
    88(** ** Types *)
    99
    10 (** Clight types are similar to those of C.  They include numeric types,
    11   pointers, arrays, function types, and composite types (struct and
    12   union).  Numeric types (integers and floats) fully specify the
    13   bit size of the type.  An integer type is a pair of a signed/unsigned
    14   flag and a bit size: 8, 16 or 32 bits. *)
    15 
    16 type signedness = Signed | Unsigned
    17 
    1810type intsize = I8 | I16 | I32
    19 
    20 (** Float types come in two sizes: 32 bits (single precision)
    21   and 64-bit (double precision). *)
    2211
    2312type floatsize = F32 | F64
    … …  
    114103  | Econst_int of int                           (**r integer literal *)
    115104  | Econst_float of float                       (**r float literal *)
    116   | Evar of ident                       (**r variable *)
     105  | Evar of ident                               (**r variable *)
    117106  | Ederef of expr                              (**r pointer dereference (unary [*]) *)
    118107  | Eaddrof of expr                             (**r address-of operator ([&]) *)
    … …  
    124113  | Eorbool of expr*expr                        (**r sequential or ([||]) *)
    125114  | Esizeof of ctype                            (**r size of a type *)
    126   | Efield of expr*ident                (**r access to a member of a struct or union *)
     115  | Efield of expr*ident                        (**r access to a member of a struct or union *)
    127116
    128117  (** The following constructors are used by the annotation process only. *)
    … …  
    147136  | Ssequence of statement*statement            (**r sequence *)
    148137  | Sifthenelse of expr*statement*statement     (**r conditional *)
    149   | Swhile of expr*statement            (**r [while] loop *)
    150   | Sdowhile of expr*statement          (**r [do] loop *)
     138  | Swhile of expr*statement                    (**r [while] loop *)
     139  | Sdowhile of expr*statement                  (**r [do] loop *)
    151140  | Sfor of statement*expr*statement*statement  (**r [for] loop *)
    152141  | Sbreak                                      (**r [break] statement *)
    … …  
    158147  | Scost of CostLabel.t * statement
    159148
    160                and labeled_statements =            (**r cases of a [switch] *)
     149and labeled_statements =                        (**r cases of a [switch] *)
    161150  | LSdefault of statement
    162151  | LScase of int*statement*labeled_statements

  • Deliverables/D2.2/8051/src/clight/clight32ToClight8.ml

    r740 r818  
    1212
    1313
    14 let rec seq = function
    15   | [] -> Clight.Sskip
    16   | [stmt] -> stmt
    17   | stmt :: l -> Clight.Ssequence (stmt, seq l)
    18 
    19 
    20 let call tmp f_id args_and_type res_type =
     14let error_prefix = "Clight32 to Clight8"
     15let error s = Error.global_error error_prefix s
     16
     17
     18let cint32s = Clight.Tint (Clight.I32, AST.Signed)
     19let cint32u = Clight.Tint (Clight.I32, AST.Unsigned)
     20let cint8s = Clight.Tint (Clight.I8, AST.Signed)
     21let cint8u = Clight.Tint (Clight.I8, AST.Unsigned)
     22
     23
     24(* Change the main so that it returns a 8 bits integer. Indeed, 32 bits integers
     25   will be replaced by structures, and returning a structure from the main is
     26   not Clight compliant. *)
     27
     28let main_ret_type = function
     29  | Clight.Tint (_, AST.Signed) -> cint8s
     30  | Clight.Tint (_, AST.Unsigned) -> cint8u
     31  | _ -> error "The main should return an integer which is not the case."
     32
     33let f_ctype ctype _ = ctype
     34let f_expr e _ _ = e
     35let f_expr_descr ed _ _ = ed
     36
     37let f_stmt ret_type stmt sub_exprs_res sub_stmts_res =
     38  match stmt, sub_exprs_res with
     39    | Clight.Sreturn (Some _), e :: _ ->
     40      let e' = Clight.Expr (Clight.Ecast (ret_type, e), ret_type) in
     41      Clight.Sreturn (Some e')
     42    | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res
     43
     44let body_returns ret_type =
     45  ClightFold.statement f_ctype f_expr f_expr_descr (f_stmt ret_type)
     46
     47let fundef_returns_char = function
     48  | Clight.Internal cfun ->
     49    let ret_type = main_ret_type cfun.Clight.fn_return in
     50    let body = body_returns ret_type cfun.Clight.fn_body in
     51    Clight.Internal {cfun with Clight.fn_return = ret_type ;
     52                               Clight.fn_body = body }
     53  | Clight.External _ as fundef -> fundef
     54
     55let main_returns_char p = match p.Clight.prog_main with
     56  | None -> p
     57  | Some main ->
     58    let main_def = List.assoc main p.Clight.prog_funct in
     59    let main_def = fundef_returns_char main_def in
     60    let prog_funct =
     61      MiscPottier.update_list_assoc main main_def p.Clight.prog_funct in
     62    { p with Clight.prog_funct = prog_funct }
     63
     64
     65(* Replacement *)
     66
     67let seq =
     68  List.fold_left
     69    (fun stmt1 stmt2 -> Clight.Ssequence (stmt1, stmt2))
     70    Clight.Sskip
     71
     72let is_complex = function
     73  | Clight.Tstruct _ | Clight.Tunion _ -> true
     74  | _ -> false
     75
     76let is_subst_complex type_substitutions res_type =
     77  if List.mem_assoc res_type type_substitutions then
     78    is_complex (List.assoc res_type type_substitutions)
     79  else false
     80
     81let addrof_with_type e ctype =
     82  let ctype = Clight.Tpointer ctype in
     83  (Clight.Expr (Clight.Eaddrof e, ctype), ctype)
     84
     85let address_if_subst_complex type_substitutions =
     86  let f l (e, ctype) =
     87    let arg_and_type =
     88      if is_subst_complex type_substitutions ctype then addrof_with_type e ctype
     89      else (e, ctype) in
     90    l @ [arg_and_type] in
     91  List.fold_left f []
     92
     93let make_call_struct tmpe res_type f_var args args_types =
     94  let (res_e, res_type) = addrof_with_type tmpe res_type in
     95  let f_type = Clight.Tfunction (res_type :: args_types, Clight.Tvoid) in
     96  let f = Clight.Expr (f_var, f_type) in
     97  Clight.Scall (None, f, res_e :: args)
     98
     99let make_call_wo_struct tmpe res_type f_var args args_types =
     100  let f_type = Clight.Tfunction (args_types, res_type) in
     101  let f = Clight.Expr (f_var, f_type) in
     102  Clight.Scall (Some tmpe, f, args)
     103
     104let make_call type_substitutions tmp f_id args_with_types res_type =
    21105  let tmpe = Clight.Expr (Clight.Evar tmp, res_type) in
    22   let (args, args_type) = List.split args_and_type in
     106  let args_with_types =
     107    address_if_subst_complex type_substitutions args_with_types in
     108  let (args, args_types) = List.split args_with_types in
    23109  let f_var = Clight.Evar f_id in
    24   let f_type = Clight.Tfunction (args_type, res_type) in
    25   let f = Clight.Expr (f_var, f_type) in
    26   (tmpe, Clight.Scall (Some tmpe, f, args))
    27 
    28 let replace_primitives_expression fresh unop_assoc binop_assoc =
    29 
    30   let rec aux e =
    31     let Clight.Expr (ed, t) = e in
     110  let call =
     111    if is_subst_complex type_substitutions res_type then make_call_struct
     112    else make_call_wo_struct in
     113  (tmpe, call tmpe res_type f_var args args_types)
     114
     115let call fresh replaced type_substitutions replacement_assoc
     116    args added_stmt added_tmps ret_type =
     117  let tmp = fresh () in
     118  let replacement_fun_name = List.assoc replaced replacement_assoc in
     119  let (tmpe, call) =
     120    make_call type_substitutions tmp replacement_fun_name args ret_type in
     121  let stmt = seq (added_stmt @ [call]) in
     122  (tmpe, stmt, added_tmps @ [(tmp, ret_type)])
     123
     124let replace_ident replacement_assoc x t =
     125  let new_name = match t with
     126    | Clight.Tfunction _
     127        when List.mem_assoc (Runtime.Fun x) replacement_assoc ->
     128      let replacement_fun_name = List.assoc (Runtime.Fun x) replacement_assoc in
     129      replacement_fun_name
     130    | _ -> x in
     131  (Clight.Expr (Clight.Evar new_name, t), Clight.Sskip, [])
     132
     133let replace_expression fresh type_substitutions replacement_assoc e =
     134
     135  let rec aux (Clight.Expr (ed, t) as e) =
    32136    let expr ed = Clight.Expr (ed, t) in
    33137    match ed with
    34138
    35       | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
    36       | Clight.Esizeof _ ->
     139      | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Esizeof _ ->
    37140        (e, Clight.Sskip, [])
    38141
    39       | Clight.Ederef e ->
    40         let (e', stmt, tmps) = aux e in
     142      | Clight.Evar x -> replace_ident replacement_assoc x t
     143
     144      | Clight.Ederef e' ->
     145        let (e', stmt, tmps) = aux e' in
    41146        (expr (Clight.Ederef e'), stmt, tmps)
    42147
    43       | Clight.Eaddrof e ->
    44         let (e', stmt, tmps) = aux e in
     148      | Clight.Eaddrof e' ->
     149        let (e', stmt, tmps) = aux e' in
    45150        (expr (Clight.Eaddrof e'), stmt, tmps)
    46151
    47       | Clight.Eunop (unop, Clight.Expr (ed', t'))
    48           when List.mem_assoc (unop, t') unop_assoc ->
    49         let (e', stmt, tmps) = aux (Clight.Expr (ed', t')) in
    50         let tmp = fresh () in
    51         let (tmpe, call) =
    52           call tmp (List.assoc (unop, t') unop_assoc) [(e', t')] t in
    53         let stmt = seq [stmt ; call] in
    54         (tmpe, stmt, tmps @ [(tmp, t)])
    55 
    56       | Clight.Ebinop (binop, Clight.Expr (ed1, t1), Clight.Expr (ed2, t2))
    57           when List.mem_assoc (binop, t1, t2) binop_assoc ->
    58         let (e1, stmt1, tmps1) = aux (Clight.Expr (ed1, t1)) in
    59         let (e2, stmt2, tmps2) = aux (Clight.Expr (ed2, t2)) in
    60         let tmp = fresh () in
    61         let (tmpe, call) =
    62           call tmp (List.assoc (binop, t1, t2) binop_assoc)
    63             [(e1, t1) ; (e2, t2)] t in
    64         let stmt = seq [stmt1 ; stmt2 ; call] in
    65         (tmpe, stmt, tmps1 @ tmps2 @ [(tmp, t)])
    66 
    67       | _ -> (e, Clight.Sskip, []) (* TODO *)
     152      | Clight.Eunop (unop, (Clight.Expr (ed', t') as e'))
     153          when List.mem_assoc (Runtime.Unary (unop, t')) replacement_assoc ->
     154        let (e', stmt, tmps) = aux e' in
     155        call fresh (Runtime.Unary (unop, t'))
     156          type_substitutions replacement_assoc [(e', t')]
     157          [stmt] tmps t
     158
     159      | Clight.Eunop (unop, e') ->
     160        let (e', stmt, tmps) = aux e' in
     161        (expr (Clight.Eunop (unop, e')), stmt, tmps)
     162
     163      | Clight.Ebinop (binop,
     164                       (Clight.Expr (ed1, t1) as e1),
     165                       (Clight.Expr (ed2, t2) as e2))
     166          when
     167            List.mem_assoc (Runtime.Binary (binop, t1, t2)) replacement_assoc ->
     168        let (e1, stmt1, tmps1) = aux e1 in
     169        let (e2, stmt2, tmps2) = aux e2 in
     170        call fresh (Runtime.Binary (binop, t1, t2))
     171          type_substitutions replacement_assoc
     172          [(e1, t1) ; (e2, t2)] [stmt1 ; stmt2] (tmps1 @ tmps2) t
     173
     174      | Clight.Ebinop (binop, e1, e2) ->
     175        let (e1, stmt1, tmps1) = aux e1 in
     176        let (e2, stmt2, tmps2) = aux e2 in
     177        let stmt = seq [stmt1 ; stmt2] in
     178        (expr (Clight.Ebinop (binop, e1, e2)), stmt, tmps1 @ tmps2)
     179
     180      | Clight.Ecast (t, (Clight.Expr (_, t') as e'))
     181          when List.mem_assoc (Runtime.Cast (t, t')) replacement_assoc ->
     182        let (e', stmt, tmps) = aux e' in
     183        call fresh (Runtime.Cast (t, t'))
     184          type_substitutions replacement_assoc [(e', t')] [stmt]
     185          tmps t
     186
     187      | Clight.Ecast (t', e') ->
     188        let (e', stmt, tmps) = aux e' in
     189        (expr (Clight.Ecast (t', e')), stmt, tmps)
     190
     191      | Clight.Econdition (e1, e2, e3) ->
     192        let (e1, stmt1, tmps1) = aux e1 in
     193        let (e2, stmt2, tmps2) = aux e2 in
     194        let (e3, stmt3, tmps3) = aux e3 in
     195        let stmt = seq [stmt1 ; stmt2 ; stmt3] in
     196        (expr (Clight.Econdition (e1, e2, e3)), stmt, tmps1 @ tmps2 @ tmps3)
     197
     198      | Clight.Eandbool (e1, e2) ->
     199        let (e1, stmt1, tmps1) = aux e1 in
     200        let (e2, stmt2, tmps2) = aux e2 in
     201        let stmt = seq [stmt1 ; stmt2] in
     202        (expr (Clight.Eandbool (e1, e2)), stmt, tmps1 @ tmps2)
     203
     204      | Clight.Eorbool (e1, e2) ->
     205        let (e1, stmt1, tmps1) = aux e1 in
     206        let (e2, stmt2, tmps2) = aux e2 in
     207        let stmt = seq [stmt1 ; stmt2] in
     208        (expr (Clight.Eorbool (e1, e2)), stmt, tmps1 @ tmps2)
     209
     210      | Clight.Efield (e', field) ->
     211        let (e', stmt, tmps) = aux e' in
     212        (expr (Clight.Efield (e', field)), stmt, tmps)
     213
     214      | Clight.Ecost (lbl, e') ->
     215        let (e', stmt, tmps) = aux e' in
     216        (expr (Clight.Ecost (lbl, e')), stmt, tmps)
     217
     218      | Clight.Ecall (id, e1, e2) ->
     219        let (e1, stmt1, tmps1) = aux e1 in
     220        let (e2, stmt2, tmps2) = aux e2 in
     221        let stmt = seq [stmt1 ; stmt2] in
     222        (expr (Clight.Ecall (id, e1, e2)), stmt, tmps1 @ tmps2)
    68223
    69224  in
    70   aux
    71 
    72 
    73 let replace_primitives_expression_list fresh unop_assoc binop_assoc =
     225  aux e
     226
     227
     228let replace_expression_list fresh type_substitutions  replacement_assoc =
    74229  let f (l, stmt, tmps) e =
    75230    let (e', stmt', tmps') =
    76       replace_primitives_expression fresh unop_assoc binop_assoc e in
    77     (l @ [e], seq [stmt ; stmt'], tmps @ tmps') in
     231      replace_expression fresh type_substitutions replacement_assoc e in
     232    (l @ [e'], seq [stmt ; stmt'], tmps @ tmps') in
    78233  List.fold_left f ([], Clight.Sskip, [])
    79234
    80235
    81 let replace_primitives_statement fresh unop_assoc binop_assoc =
     236let replace_statement fresh type_substitutions replacement_assoc =
    82237  let aux_exp =
    83     replace_primitives_expression fresh unop_assoc binop_assoc in
     238    replace_expression fresh type_substitutions replacement_assoc in
    84239  let aux_exp_list =
    85     replace_primitives_expression_list fresh unop_assoc binop_assoc in
     240    replace_expression_list fresh type_substitutions replacement_assoc in
    86241
    87242  let rec aux = function
    … …  
    89244    | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sgoto _
    90245    | Clight.Sreturn None
    91       as stmt -> (stmt, [])
     246        as stmt -> (stmt, [])
    92247
    93248    | Clight.Slabel (lbl, stmt) ->
    … …  
    116271      let (args', stmt3, tmps3) = aux_exp_list args in
    117272      let stmt = seq [stmt1 ; stmt2 ; stmt3 ;
    118                            Clight.Scall (Some e', f', args')] in
     273                      Clight.Scall (Some e', f', args')] in
    119274      (stmt, tmps1 @ tmps2 @ tmps3)
    120275
    … …  
    144299      let (stmt3', tmps3) = aux stmt3 in
    145300      let stmt = seq [stmt1' ; stmte ;
    146                       Clight.Swhile (e', seq [stmt2' ; stmt3' ; stmte])] in
     301                      Clight.Swhile (e', seq [stmt3' ; stmt2' ; stmte])] in
    147302      (stmt, tmpse @ tmps1 @ tmps2 @ tmps3)
    148303
    … …  
    180335
    181336
    182 let replace_primitives_internal fresh unop_assoc binop_assoc def =
     337let f_ctype type_substitutions ctype sub_ctypes_res = match ctype with
     338  | _ when List.mem_assoc ctype type_substitutions ->
     339    List.assoc ctype type_substitutions
     340  | _ -> ClightFold.ctype_fill_subs ctype sub_ctypes_res
     341
     342let replace_ctype type_substitutions =
     343  ClightFold.ctype (f_ctype type_substitutions)
     344
     345let f_expr = ClightFold.expr_fill_subs
     346
     347let f_expr_descr = ClightFold.expr_descr_fill_subs
     348
     349let f_stmt = ClightFold.statement_fill_subs
     350
     351let statement_replace_ctype type_substitutions =
     352  ClightFold.statement (f_ctype type_substitutions) f_expr f_expr_descr f_stmt
     353
     354
     355let replace_internal fresh type_substitutions replacement_assoc def =
    183356  let (new_body, tmps) =
    184     replace_primitives_statement fresh unop_assoc binop_assoc
     357    replace_statement fresh type_substitutions replacement_assoc
    185358      def.Clight.fn_body in
    186   { def with Clight.fn_vars = def.Clight.fn_vars @ tmps ;
    187              Clight.fn_body = new_body }
    188 
    189 let replace_primitives_funct fresh unop_assoc binop_assoc (id, fundef) =
     359  let new_body = statement_replace_ctype type_substitutions new_body in
     360  let f (x, t) = (x, replace_ctype type_substitutions t) in
     361  let params = List.map f def.Clight.fn_params in
     362  let vars = List.map f (def.Clight.fn_vars @ tmps) in
     363  { Clight.fn_return = replace_ctype type_substitutions def.Clight.fn_return ;
     364    Clight.fn_params = params ;
     365    Clight.fn_vars = vars ;
     366    Clight.fn_body = new_body }
     367
     368let replace_funct fresh type_substitutions replacement_assoc (id, fundef) =
    190369  let fundef' = match fundef with
    191370    | Clight.Internal def ->
    192371      Clight.Internal
    193         (replace_primitives_internal fresh unop_assoc binop_assoc def)
     372        (replace_internal fresh type_substitutions replacement_assoc def)
    194373    | _ -> fundef in
    195374  (id, fundef')
    196375
    197 let replace_primitives fresh unop_assoc binop_assoc p =
     376let replace fresh type_substitutions replacement_assoc p =
    198377  let prog_funct =
    199     List.map (replace_primitives_funct fresh unop_assoc binop_assoc)
     378    List.map (replace_funct fresh type_substitutions replacement_assoc)
    200379      p.Clight.prog_funct in
    201380  { p with Clight.prog_funct = prog_funct }
    202381
    203382
     383(* The constant replacement replaces each 32 bits and 16 bits integer constant
     384   by a global variable of the same value. They will be replaced by the
     385   appropriate structural value by the global replacement that comes
     386   afterwards. *)
     387
     388module CstMap =
     389  Map.Make
     390    (struct
     391      type t = (int * Clight.intsize * Clight.ctype)
     392      let compare = Pervasives.compare
     393     end)
     394
     395let f_subs fresh replace subs map =
     396  let f (l, map) x =
     397    let (x, map) = replace fresh map x in
     398    (l @ [x], map) in
     399  List.fold_left f ([], map) subs
     400
     401let rec replace_constant_expr fresh map (Clight.Expr (ed, t) as e) =
     402  match ed, t with
     403    | Clight.Econst_int i, Clight.Tint (Clight.I8, _) ->
     404      (e, map)
     405    | Clight.Econst_int i, Clight.Tint (size, _)
     406      when CstMap.mem (i, size, t) map ->
     407      let id = CstMap.find (i, size, t) map in
     408      (Clight.Expr (Clight.Evar id, t), map)
     409    | Clight.Econst_int i, Clight.Tint (size, _) ->
     410      let id = fresh () in
     411      let map = CstMap.add (i, size, t) id map in
     412      let id = CstMap.find (i, size, t) map in
     413      (Clight.Expr (Clight.Evar id, t), map)
     414    | _ ->
     415      let (sub_ctypes, sub_exprs) = ClightFold.expr_descr_subs ed in
     416      let (sub_exprs, map) = f_subs fresh replace_constant_expr sub_exprs map in
     417      let ed = ClightFold.expr_descr_fill_subs ed sub_ctypes sub_exprs in
     418      (Clight.Expr (ed, t), map)
     419
     420let rec replace_constant_stmt fresh map stmt =
     421  let (sub_exprs, sub_stmts) = ClightFold.statement_subs stmt in
     422  let (sub_exprs, map) =
     423    f_subs fresh replace_constant_expr sub_exprs map in
     424  let (sub_stmts, map) =
     425    f_subs fresh replace_constant_stmt sub_stmts map in
     426  (ClightFold.statement_fill_subs stmt sub_exprs sub_stmts, map)
     427
     428let replace_constant_fundef fresh (functs, map) (id, fundef) =
     429  match fundef with
     430    | Clight.Internal cfun ->
     431      let (body, map) = replace_constant_stmt fresh map cfun.Clight.fn_body in
     432      let fundef = Clight.Internal { cfun with Clight.fn_body = body } in
     433      (functs @ [(id, fundef)], map)
     434    | Clight.External _ -> (functs @ [(id, fundef)], map)
     435
     436let init_datas i size =
     437  [match size with
     438    | Clight.I8 -> Clight.Init_int8 i
     439    | Clight.I16 -> Clight.Init_int16 i
     440    | Clight.I32 -> Clight.Init_int32 i]
     441
     442let globals_of_map map =
     443  let f (i, size, t) id l = l @ [((id, init_datas i size), t)] in
     444  CstMap.fold f map []
     445
     446let replace_constant p =
     447  let tmp_universe = ClightAnnotator.fresh_universe "_cst" p in
     448  let fresh () = StringTools.Gen.fresh tmp_universe in
     449  let (functs, map) =
     450    List.fold_left (replace_constant_fundef fresh)
     451      ([], CstMap.empty) p.Clight.prog_funct in
     452  let csts = globals_of_map map in
     453  { p with
     454    Clight.prog_funct = functs ; Clight.prog_vars = p.Clight.prog_vars @ csts }
     455
     456
     457(* Globals replacement *)
     458
     459let expand_int size i =
     460  let i = Big_int.big_int_of_int i in
     461  let i =
     462    if Big_int.ge_big_int i Big_int.zero_big_int then i
     463    else Big_int.add_big_int i (Big_int.power_int_positive_int 2 size) in
     464  let bound = Big_int.power_int_positive_int 2 8 in
     465  let rec aux n i =
     466    if n >= size then []
     467    else
     468      let (next, chunk) = Big_int.quomod_big_int i bound in
     469      chunk :: (aux (n+1) next) in
     470  List.map (fun i -> Clight.Init_int8 (Big_int.int_of_big_int i)) (aux 0 i)
     471
     472let expand_init_data = function
     473  | Clight.Init_int16 i -> expand_int 2 i
     474  | Clight.Init_int32 i -> expand_int 4 i
     475  | init_data -> [init_data]
     476
     477let expand_init_datas init_datas =
     478  List.flatten (List.map expand_init_data init_datas)
     479
     480let replace_global type_substitutions ((id, init_datas), t) =
     481  let init_datas = expand_init_datas init_datas in
     482  ((id, init_datas), replace_ctype type_substitutions t)
     483
     484let replace_globals type_substitutions p =
     485  let vars = List.map (replace_global type_substitutions) p.Clight.prog_vars in
     486  { p with Clight.prog_vars = vars }
     487
     488
     489(* Unsupported operations by the 8051. *)
     490
     491(* 8 bits signed division *)
     492
     493let divs_fun s _ =
     494  "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^
     495  "  unsigned char x1 = (unsigned char) x;\n" ^
     496  "  unsigned char y1 = (unsigned char) y;\n" ^
     497  "  signed char sign = 1;\n" ^
     498  "  if (x < 0) { x1 = (unsigned char) (-x); sign = -sign; }\n" ^
     499  "  if (y < 0) { y1 = (unsigned char) (-y); sign = -sign; }\n" ^
     500  "  return (sign * ((signed char) (x1/y1)));\n" ^
     501  "}\n\n"
     502
     503let divs =
     504  (Runtime.Binary (Clight.Odiv, cint8s, cint8s), "_divs", [], divs_fun, [])
     505
     506
     507(* 8 bits signed modulo *)
     508
     509let mods_fun s _ =
     510  "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^
     511  "  return (x - (x/y) * y);\n" ^
     512  "}\n\n"
     513
     514let mods =
     515  (Runtime.Binary (Clight.Omod, cint8s, cint8s), "_mods", [], mods_fun,
     516   [Runtime.Binary (Clight.Odiv, cint8s, cint8s)])
     517
     518
     519(* Shifts *)
     520
     521let sh_fun signedness op s _ =
     522  signedness ^ " char " ^ s ^ " (" ^ signedness ^ " char x, " ^
     523  signedness ^ " char y) {\n" ^
     524  "  " ^ signedness ^ " char res = x, i;\n" ^
     525  "  for (i = 0 ; i < y ; i++) res = res " ^ op ^ " 2;\n" ^
     526  "  return res;\n" ^
     527  "}\n\n"
     528
     529(* 8 bits shifts left *)
     530
     531let shls_fun = sh_fun "signed" "*"
     532
     533let shls =
     534  (Runtime.Binary (Clight.Oshl, cint8s, cint8s), "_shls", [], shls_fun, [])
     535
     536let shlu_fun s _ =
     537  "unsigned char " ^ s ^ " (unsigned char x, unsigned char y) {\n" ^
     538  "  return ((unsigned char) ((signed char) x << (signed char) y));\n" ^
     539  "}\n\n"
     540
     541let shlu =
     542  (Runtime.Binary (Clight.Oshl, cint8u, cint8u), "_shlu", [], shlu_fun,
     543   [Runtime.Binary (Clight.Oshl, cint8s, cint8s)])
     544
     545(* 8 bits shifts right *)
     546
     547let shrs_fun s _ =
     548  "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^
     549  "  signed char res = x, i;\n" ^
     550  "  for (i = 0 ; i < y ; i++) {\n" ^
     551  "    res = ((unsigned char) res) / 2;\n" ^
     552  "    res = res + ((signed char) 128);\n" ^
     553  "  }\n" ^
     554  "  return res;\n" ^
     555  "}\n\n"
     556
     557let shrs =
     558  (Runtime.Binary (Clight.Oshr, cint8s, cint8s), "_shrs", [], shrs_fun, [])
     559
     560let shru_fun = sh_fun "unsigned" "/"
     561
     562let shru =
     563  (Runtime.Binary (Clight.Oshr, cint8u, cint8u), "_shru", [], shru_fun, [])
     564
     565
     566(* int32 *)
     567
     568let struct_int32 name fields = match fields with
     569  | lolo :: lohi :: hilo :: hihi :: _ ->
     570    Clight.Tstruct
     571      (name,
     572       [(lolo, cint8u) ; (lohi, cint8u) ; (hilo, cint8u) ; (hihi, cint8u)])
     573  | _ -> error ("bad field names when defining type " ^ name ^ ".")
     574
     575let struct_int32_name = "struct _int32_"
     576
     577let new_int32 int32 =
     578  let lolo = "lolo" in
     579  let lohi = "lohi" in
     580  let hilo = "hilo" in
     581  let hihi = "hihi" in
     582  (int32, struct_int32_name, [lolo ; lohi ; hilo ; hihi], struct_int32)
     583
     584let int32s = new_int32 (Clight.Tint (Clight.I32, AST.Signed))
     585let int32u = new_int32 (Clight.Tint (Clight.I32, AST.Unsigned))
     586
     587(* 32 bits operations *)
     588
     589(* 32 bits equality *)
     590
     591let eq_int32s_fun s l =
     592  let (int32, lolo, lohi, hilo, hihi) = match l with
     593    | (int32, lolo :: lohi :: hilo :: hihi :: _) :: _ ->
     594      (int32, lolo, lohi, hilo, hihi)
     595    | _ -> error ("new type definition not coherent in function " ^ s ^ ".") in
     596  int32 ^ " " ^ s ^ " (" ^ int32 ^ " x, " ^ int32 ^ " y) {\n" ^
     597  "  " ^ int32 ^ " res;\n" ^
     598  "  res." ^ lolo ^ " = 1;\n" ^
     599  "  if (x." ^ lolo ^ " != y." ^ lolo ^ ") res." ^ lolo ^ " = 0;\n" ^
     600  "  if (x." ^ lohi ^ " != y." ^ lohi ^ ") res." ^ lolo ^ " = 0;\n" ^
     601  "  if (x." ^ hilo ^ " != y." ^ hilo ^ ") res." ^ lolo ^ " = 0;\n" ^
     602  "  if (x." ^ hihi ^ " != y." ^ hihi ^ ") res." ^ lolo ^ " = 0;\n" ^
     603  "  res." ^ lohi ^ " = 0;\n" ^
     604  "  res." ^ hilo ^ " = 0;\n" ^
     605  "  res." ^ hihi ^ " = 0;\n" ^
     606  "  return (res);\n" ^
     607  "}\n\n"
     608
     609let eq32s =
     610  (Runtime.Binary (Clight.Oeq, cint32s, cint32s), "eq_int32s",
     611   [struct_int32_name], eq_int32s_fun, [])
     612
     613(* 32 bits casts *)
     614
     615let int32s_to_int8s_fun s l =
     616  let (int32, lolo, lohi, hilo, hihi) = match l with
     617    | (int32, lolo :: lohi :: hilo :: hihi :: _) :: _ ->
     618      (int32, lolo, lohi, hilo, hihi)
     619    | _ -> error ("new type definition not coherent in function " ^ s ^ ".") in
     620  "signed char " ^ s ^ " (" ^ int32 ^ " x) {\n" ^
     621  "  return ((signed char) x." ^ lolo ^ ");\n" ^
     622  "}\n\n"
     623
     624let int32s_to_int8s =
     625  (Runtime.Cast (cint8s, cint32s), "int32s_to_int8s", [struct_int32_name],
     626   int32s_to_int8s_fun, [])
     627
     628
     629(* int16 *)
     630
     631let struct_int16 name fields = match fields with
     632  | lo :: hi :: _ ->
     633    Clight.Tstruct (name, [(lo, cint8u) ; (hi, cint8u)])
     634  | _ -> error ("bad field names when defining type " ^ name ^ ".")
     635
     636let struct_int16_name = "struct _int16_"
     637
     638let new_int16 int16 =
     639  let lo = "lo" in
     640  let hi = "hi" in
     641  (int16, struct_int16_name, [lo ; hi], struct_int16)
     642
     643let int16s = new_int16 (Clight.Tint (Clight.I16, AST.Signed))
     644let int16u = new_int16 (Clight.Tint (Clight.I16, AST.Unsigned))
     645
     646
     647(* int32 and int16 *)
     648
     649let int32_and_int16_types = [int32s ; int32u ; int16s ; int16u]
     650let int32_and_int16_replacements = [eq32s ; int32s_to_int8s]
     651
     652
     653let unsupported = [divs ; mods ; shls ; shlu ; shrs ; shru]
     654
     655
     656let save_and_parse p =
     657  let tmp_file = Filename.temp_file "clight32toclight8" ".c" in
     658  try
     659    let oc = open_out tmp_file in
     660    output_string oc (ClightPrinter.print_program p) ;
     661    close_out oc ;
     662    let res = ClightParser.process tmp_file in
     663    Misc.SysExt.safe_remove tmp_file ;
     664    res
     665  with Sys_error _ -> failwith "Error reparsing Clight8 transformation."
     666
     667let add_replacements p new_types replacements =
     668  let p = ClightCasts.simplify p in
     669  let (p, type_substitutions, replacement_assoc) =
     670    Runtime.add p new_types replacements in
     671  let p = ClightCasts.simplify p in
     672  let tmp_universe = ClightAnnotator.fresh_universe "_tmp" p in
     673  let fresh () = StringTools.Gen.fresh tmp_universe in
     674  let p = replace fresh type_substitutions replacement_assoc p in
     675  let p = replace_globals type_substitutions p in
     676  (* Printf.printf "%s\n%!" (ClightPrinter.print_program p) ; *)
     677  let p = save_and_parse p in
     678  ClightCasts.simplify p
     679
    204680let translate p =
    205   (* TODO: restore below *)
    206 (*
    207   let (p, unop_assoc, binop_assoc) = Runtime.add p in
    208   let p = ClightCasts.simplify p in
    209   let labs = ClightAnnotator.all_labels p in
    210   let tmp_prefix = StringTools.Gen.fresh_prefix labs "_tmp" in
    211   let tmp_universe = StringTools.Gen.new_universe tmp_prefix in
    212   let fresh () = StringTools.Gen.fresh tmp_universe in
    213   let p = replace_primitives fresh unop_assoc binop_assoc p in
    214   (* TODO: do the translation *)
    215   p
    216 *)
    217   ClightCasts.simplify p
     681  let p = main_returns_char p in
     682  let p = replace_constant p in
     683  let p =
     684    add_replacements p int32_and_int16_types int32_and_int16_replacements in
     685  add_replacements p [] unsupported

  • Deliverables/D2.2/8051/src/clight/clightAnnotator.ml

    r645 r818  
    1919
    2020let triple_union
    21     (var_names1, cost_labels1, user_labels1)
    22     (var_names2, cost_labels2, user_labels2) =
    23   (StringTools.Set.union var_names1 var_names2,
     21    (names1, cost_labels1, user_labels1)
     22    (names2, cost_labels2, user_labels2) =
     23  (StringTools.Set.union names1 names2,
    2424   CostLabel.Set.union cost_labels1 cost_labels2,
    2525   Label.Set.union user_labels1 user_labels2)
    … …  
    2727let empty_triple = (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty)
    2828
     29let name_singleton id =
     30  (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty)
     31
     32let cost_label_singleton cost_lbl =
     33  (StringTools.Set.empty, CostLabel.Set.singleton cost_lbl, Label.Set.empty)
     34
     35let label_singleton lbl =
     36  (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.singleton lbl)
     37
    2938let list_union l = List.fold_left triple_union empty_triple l
    3039
    31 let rec exp_idents e =
    32   let Clight.Expr (e, _) = e in
    33   match e with
    34     | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Esizeof _ ->
    35         empty_triple
    36     | Clight.Evar x ->
    37         (StringTools.Set.singleton x, CostLabel.Set.empty, Label.Set.empty)
    38     | Clight.Ederef e | Clight.Eaddrof e | Clight.Eunop (_, e)
    39     | Clight.Ecast (_, e) -> exp_idents e
    40     | Clight.Efield (e, x) ->
    41         let (var_names, cost_labels, user_labels) = exp_idents e in
    42         (StringTools.Set.add x var_names, cost_labels, user_labels)
    43     | Clight.Ebinop (_, e1, e2) | Clight.Eandbool (e1, e2)
    44     | Clight.Eorbool (e1, e2) -> list_union [exp_idents e1 ; exp_idents e2]
    45     | Clight.Econdition (e1, e2, e3) ->
    46         list_union [exp_idents e1 ; exp_idents e2 ; exp_idents e3]
    47     | Clight.Ecost (lbl, e) ->
    48         let (var_names, cost_labels, user_labels) = exp_idents e in
    49         (var_names, CostLabel.Set.add lbl cost_labels, user_labels)
    50     | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen *)
    51 
    52 let exp_idents_opt = function
    53   | None -> empty_triple
    54   | Some e -> exp_idents e
    55 
    56 let exp_idents_list l = list_union (List.map exp_idents l)
    57 
    58 let rec body_idents = function
    59   | Clight.Sskip | Clight.Sbreak | Clight.Scontinue -> empty_triple
    60   | Clight.Sassign (e1, e2) -> list_union [exp_idents e1 ; exp_idents e2]
    61   | Clight.Scall (eopt, f, args) ->
    62       list_union [exp_idents_opt eopt ; exp_idents f ; exp_idents_list args]
    63   | Clight.Ssequence (s1, s2) -> list_union [body_idents s1 ; body_idents s2]
    64   | Clight.Sifthenelse (e, s1, s2) ->
    65       list_union [exp_idents e ; body_idents s1 ; body_idents s2]
    66   | Clight.Swhile (e, s) | Clight.Sdowhile (e, s) ->
    67       list_union [exp_idents e ; body_idents s]
    68   | Clight.Sfor (s1, e, s2, s3) ->
    69       list_union [body_idents s1 ; exp_idents e ;
    70                   body_idents s2 ; body_idents s3]
    71   | Clight.Sreturn eopt -> exp_idents_opt eopt
    72   | Clight.Sswitch (e, ls) -> list_union [exp_idents e ; ls_idents ls]
    73   | Clight.Slabel (lbl, stmt) ->
    74       let (var_names, cost_labels, user_labels) = body_idents stmt in
    75       (var_names, cost_labels, Label.Set.add lbl user_labels)
    76   | Clight.Sgoto lbl ->
    77       (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.singleton lbl)
    78   | Clight.Scost (lbl, stmt) ->
    79       let (var_names, cost_labels, user_labels) = body_idents stmt in
    80       (var_names, CostLabel.Set.add lbl cost_labels, user_labels)
    81 and ls_idents = function
    82   | Clight.LSdefault stmt -> body_idents stmt
    83   | Clight.LScase (_, stmt, ls) -> list_union [body_idents stmt ; ls_idents ls]
     40let f_ctype ctype sub_ctypes_res =
     41  let res = match ctype with
     42    | Clight.Tstruct (id, fields) | Clight.Tunion (id, fields) ->
     43      (string_set_of_list (id :: (List.map fst fields)),
     44       CostLabel.Set.empty, Label.Set.empty)
     45    | Clight.Tcomp_ptr id -> name_singleton id
     46    | _ -> empty_triple in
     47  list_union (res :: sub_ctypes_res)
     48
     49let f_expr _ sub_ctypes_res sub_expr_descrs_res =
     50  list_union (sub_ctypes_res @ sub_expr_descrs_res)
     51
     52let f_expr_descr ed sub_ctypes_res sub_exprs_res =
     53  let res = match ed with
     54    | Clight.Evar id | Clight.Efield (_, id) | Clight.Ecall (id, _, _) ->
     55      name_singleton id
     56    | Clight.Ecost (cost_lbl, _) -> cost_label_singleton cost_lbl
     57    | _ -> empty_triple in
     58  list_union (res :: (sub_ctypes_res @ sub_exprs_res))
     59
     60let f_stmt stmt sub_exprs_res sub_stmts_res =
     61  let stmt_res = match stmt with
     62    | Clight.Slabel (lbl, _) | Clight.Sgoto lbl -> label_singleton lbl
     63    | Clight.Scost (cost_lbl, _) -> cost_label_singleton cost_lbl
     64    | _ -> empty_triple in
     65  list_union (stmt_res :: (sub_exprs_res @ sub_stmts_res))
     66
     67let body_idents = ClightFold.statement f_ctype f_expr f_expr_descr f_stmt
    8468
    8569let prog_idents p =
    … …  
    8973          string_set_of_list
    9074            (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
    91         let (var_names, cost_labels, user_labels) =
     75        let (names, cost_labels, user_labels) =
    9276          body_idents def.Clight.fn_body in
    93         (StringTools.Set.union vars var_names, cost_labels, user_labels)
     77        (StringTools.Set.union vars names, cost_labels, user_labels)
    9478    | Clight.External (id, _, _) ->
    9579        (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
    9680  let fun_idents (id, f_def) =
    97     let (var_names, cost_labels, user_labels) = def_idents f_def in
    98     (StringTools.Set.add id var_names, cost_labels, user_labels) in
     81    let (names, cost_labels, user_labels) = def_idents f_def in
     82    (StringTools.Set.add id names, cost_labels, user_labels) in
    9983  let f idents def = triple_union idents (fun_idents def) in
    10084  List.fold_left f empty_triple p.Clight.prog_funct
    10185
    102 let var_names p =
    103   let (var_names, _, _) = prog_idents p in var_names
     86let names p =
     87  let (names, _, _) = prog_idents p in names
    10488let cost_labels p =
    10589  let (_, cost_labels, _) = prog_idents p in cost_labels
    … …  
    11498  Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all
    11599
     100let all_idents p =
     101  let (names, cost_labels, user_labels) = prog_idents p in
     102  let to_string_set fold set =
     103    fold (fun lbl idents -> StringTools.Set.add lbl idents) set
     104      StringTools.Set.empty in
     105  let cost_labels = to_string_set CostLabel.Set.fold cost_labels in
     106  let user_labels = to_string_set Label.Set.fold user_labels in
     107  StringTools.Set.union names (StringTools.Set.union cost_labels user_labels)
     108
     109let fresh_ident base p =
     110  StringTools.Gen.fresh_prefix (all_idents p) base
     111
     112let fresh_universe base p =
     113  let universe = fresh_ident base p in
     114  StringTools.Gen.new_universe universe
     115
     116let make_fresh base p =
     117  let universe = fresh_universe base p in
     118  (fun () -> StringTools.Gen.fresh universe)
     119
    116120
    117121(* Instrumentation *)
    118122
    119 let int_typ = Clight.Tint (Clight.I32, Clight.Signed)
     123let int_typ = Clight.Tint (Clight.I32, AST.Signed)
    120124
    121125let const_int i = Clight.Expr (Clight.Econst_int i, int_typ)
    … …  
    311315
    312316  (* Create a fresh 'cost' variable. *)
    313   let var_names = var_names p in
    314   let cost_id = StringTools.Gen.fresh_prefix var_names cost_id_prefix in
     317  let names = names p in
     318  let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
    315319  let cost_decl = cost_decl cost_id in
    316320
    317321  (* Define an increment function for the cost variable. *)
    318322  let cost_incr =
    319     StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id var_names)
     323    StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id names)
    320324      cost_incr_prefix in
    321325  let cost_incr_def = cost_incr_def cost_id cost_incr in

  • Deliverables/D2.2/8051/src/clight/clightAnnotator.mli

    r640 r818  
    1414val user_labels : Clight.program -> Label.Set.t
    1515val all_labels  : Clight.program -> StringTools.Set.t
     16val all_idents  : Clight.program -> StringTools.Set.t
     17
     18val fresh_ident : string (* base *) -> Clight.program -> string
     19
     20val fresh_universe :
     21  string (* prefix *) -> Clight.program -> StringTools.Gen.universe
     22
     23val make_fresh :
     24  string (* prefix *) -> Clight.program -> (unit -> string)

  • Deliverables/D2.2/8051/src/clight/clightCasts.ml

    r740 r818  
    66    be polymorphic, but working only on homogene types. *)
    77
     8
     9let error_prefix = "Clight casts simplification"
     10let error = Error.global_error error_prefix
     11let error_float () = error "float not supported."
     12
     13
     14(* Int sizes *)
     15
     16let int_of_intsize = function
     17  | Clight.I8 -> 8
     18  | Clight.I16 -> 16
     19  | Clight.I32 -> 32
     20
     21let intsize_of_int = function
     22  | i when i <= 8 -> Clight.I8
     23  | i when i <= 16 -> Clight.I16
     24  | _ -> Clight.I32
     25
     26let cmp_intsize cmp size1 size2 =
     27  cmp (int_of_intsize size1) (int_of_intsize size2)
     28
     29let max_intsize size1 size2 =
     30  if (int_of_intsize size1) < (int_of_intsize size2) then size2 else size1
     31
     32let intsize_union size1 size2 =
     33  intsize_of_int ((int_of_intsize size1) + (int_of_intsize size2))
     34
     35let pow2 = MiscPottier.pow 2
     36
     37let belongs_to_int_type size sign i = match size, sign with
     38  | Clight.I8, AST.Unsigned -> 0 <= i && i <= (pow2 8) - 1
     39  | Clight.I8, AST.Signed -> -(pow2 7) <= i && i <= (pow2 7) - 1
     40  | Clight.I16, AST.Unsigned -> 0 <= i && i <= (pow2 16) - 1
     41  | Clight.I16, AST.Signed -> -(pow2 15) <= i && i <= (pow2 15) - 1
     42  | Clight.I32, AST.Unsigned -> 0 <= i
     43  | Clight.I32, AST.Signed ->
     44    let pow2_30 = pow2 30 in
     45    (-(pow2_30 + pow2_30)) <= i &&
     46    i <= ((pow2_30 - 1) + pow2_30) (* = 2^31 - 1 *)
     47
     48let smallest_int_type i =
     49  let (size, sign) = match i with
     50  | _ when belongs_to_int_type Clight.I8 AST.Signed i ->
     51    (Clight.I8, AST.Signed)
     52  | _ when belongs_to_int_type Clight.I8 AST.Unsigned i ->
     53    (Clight.I8, AST.Unsigned)
     54  | _ when belongs_to_int_type Clight.I16 AST.Signed i ->
     55    (Clight.I16, AST.Signed)
     56  | _ when belongs_to_int_type Clight.I16 AST.Unsigned i ->
     57    (Clight.I16, AST.Unsigned)
     58  | _ when belongs_to_int_type Clight.I32 AST.Unsigned i ->
     59    (Clight.I32, AST.Unsigned)
     60  | _ ->
     61    (Clight.I32, AST.Signed) in
     62  Clight.Tint (size, sign)
     63
     64
     65let type_of_expr (Clight.Expr (_, t)) = t
     66
     67let int_type_union t1 t2 =
     68  let (size, sign) = match t1, t2 with
     69    | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2)
     70      when sign1 = sign2 -> (max_intsize size1 size2, sign1)
     71    | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2) ->
     72      (intsize_union size1 size2, AST.Signed)
     73    | _ -> assert false (* only use on int types *)
     74  in
     75  Clight.Tint (size, sign)
     76
     77let cast_if_needed t (Clight.Expr (ed, t') as e) = match t, ed with
     78  | _ when t = t' -> e
     79  | Clight.Tint (size, sign), Clight.Econst_int i
     80    when belongs_to_int_type size sign i ->
     81    Clight.Expr (Clight.Econst_int i, t)
     82  | _ -> Clight.Expr (Clight.Ecast (t, e), t)
     83
     84let rec simplify_binop t binop
     85    (Clight.Expr (ed1, t1) as e1)
     86    (Clight.Expr (ed2, t2) as e2) =
     87  let e1' = simplify_expr e1 in
     88  let e2' = simplify_expr e2 in
     89  let make_int i t = Clight.Expr (Clight.Econst_int i, t) in
     90
     91  let (e1', e2', t') = match t1, t2, ed1, ed2 with
     92
     93    | Clight.Tint _, Clight.Tint _,
     94      Clight.Econst_int i1, Clight.Econst_int i2 ->
     95      let t1' = smallest_int_type i1 in
     96      let t2' = smallest_int_type i2 in
     97      let t' = int_type_union t1' t2' in
     98      (make_int i1 t', make_int i2 t', t')
     99
     100    | Clight.Tint _, Clight.Tint _, _, Clight.Econst_int i2 ->
     101      let t' = type_of_expr e1' in
     102      let e2' = make_int i2 t' in
     103      (e1', e2', t')
     104
     105    | Clight.Tint _, Clight.Tint _, Clight.Econst_int i1, _ ->
     106      let t' = type_of_expr e2' in
     107      let e1' = make_int i1 t' in
     108      (e1', e2', t')
     109
     110    | Clight.Tint _, Clight.Tint _, _, _ ->
     111      let t' = int_type_union (type_of_expr e1') (type_of_expr e2') in
     112      (cast_if_needed t' e1', cast_if_needed t' e2', t')
     113
     114    | _ -> (e1', e2', t)
     115
     116  in
     117
     118  Clight.Expr (Clight.Ebinop (binop, e1', e2'), t')
     119
     120and simplify_bool_op f_bool t e1 e2 =
     121  let (e1', e2', t') = simplify_and_same_type t e1 e2 in
     122  Clight.Expr (f_bool e1' e2', t')
     123
     124and simplify_and_same_type t e1 e2 =
     125  let e1' = simplify_expr e1 in
     126  let e2' = simplify_expr e2 in
     127  if type_of_expr e1' = type_of_expr e2' then (e1', e2', type_of_expr e1')
     128  else (cast_if_needed t e1', cast_if_needed t e2', t)
     129
     130and simplify_expr (Clight.Expr (ed, t) as e) = match ed with
     131
     132  | Clight.Econst_int i ->
     133    let t' = smallest_int_type i in
     134    Clight.Expr (ed, t')
     135
     136  | Clight.Evar _ -> e
     137
     138  | Clight.Esizeof _ -> Clight.Expr (ed, Clight.Tint (Clight.I8, AST.Unsigned))
     139
     140  | Clight.Econst_float _ -> error_float ()
     141
     142  | Clight.Ederef e ->
     143    let e' = simplify_expr e in
     144    Clight.Expr (Clight.Ederef e', t)
     145
     146  | Clight.Eaddrof e ->
     147    let e' = simplify_expr e in
     148    Clight.Expr (Clight.Eaddrof e', t)
     149
     150  | Clight.Eunop (unop, e) ->
     151    let e' = simplify_expr e in
     152    Clight.Expr (Clight.Eunop (unop, e'), type_of_expr e')
     153
     154  | Clight.Ebinop (binop, e1, e2) ->
     155    simplify_binop t binop e1 e2
     156
     157  | Clight.Ecast (Clight.Tint (Clight.I32, AST.Signed), e) -> simplify_expr e
     158
     159  | Clight.Ecast (t', e) ->
     160    Clight.Expr (Clight.Ecast (t', simplify_expr e), t')
     161
     162  | Clight.Econdition (e1, e2, e3) ->
     163    let e1' = simplify_expr e1 in
     164    let (e2', e3', t') = simplify_and_same_type t e2 e3 in
     165    Clight.Expr (Clight.Econdition (e1', e2', e3'), t')
     166
     167  | Clight.Eandbool (e1, e2) ->
     168    simplify_bool_op (fun e1' e2' -> Clight.Eandbool (e1', e2')) t e1 e2
     169
     170  | Clight.Eorbool (e1, e2) ->
     171    simplify_bool_op (fun e1' e2' -> Clight.Eorbool (e1', e2')) t e1 e2
     172
     173  | Clight.Efield (e, field) ->
     174    Clight.Expr (Clight.Efield (simplify_expr e, field), t)
     175
     176  | Clight.Ecost (lbl, e) ->
     177    Clight.Expr (Clight.Ecost (lbl, simplify_expr e), t)
     178
     179  | Clight.Ecall (id, e1, e2) ->
     180    assert false (* should be impossible *)
     181
     182
    8183let f_ctype ctype _ = ctype
    9184
    10 (*
    11 let f_expr = ClightFold.expr_fill_subs
    12 
    13 let f_expr_descr e sub_ctypes_res sub_exprs_res =
    14   match e, sub_exprs_res with
    15     | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _),
    16       Clight.Expr
    17         (Clight.Eunop
    18            (unop,
    19             Clight.Expr
    20               (Clight.Ecast
    21                  (Clight.Tint (Clight.I32, _),
    22                   (Clight.Expr (_, Clight.Tint (Clight.I8, signedness2)) as e)),
    23                _)),
    24          _) :: _ when signedness1 = signedness2 ->
    25       Clight.Eunop (unop, e)
    26     | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _),
    27       Clight.Expr
    28         (Clight.Ebinop
    29            (binop,
    30             Clight.Expr
    31               (Clight.Ecast
    32                  (Clight.Tint (Clight.I32, _),
    33                   (Clight.Expr (_,
    34                                 Clight.Tint (Clight.I8, signedness2)) as e1)),
    35                _),
    36             Clight.Expr
    37               (Clight.Ecast
    38                  (Clight.Tint (Clight.I32, _),
    39                   (Clight.Expr (_,
    40                                 Clight.Tint (Clight.I8, signedness3)) as e2)),
    41                _)),
    42          _) :: _ when signedness1 = signedness2 && signedness2 = signedness3 ->
    43       Clight.Ebinop (binop, e1, e2)
    44     | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _),
    45       Clight.Expr
    46         (Clight.Ebinop
    47            (binop,
    48             Clight.Expr
    49               (Clight.Ecast
    50                  (Clight.Tint (Clight.I32, _),
    51                   (Clight.Expr (_,
    52                                 Clight.Tint (Clight.I8, signedness2)) as e1)),
    53                _),
    54             Clight.Expr (Clight.Econst_int i, _)),
    55          _) :: _ when signedness1 = signedness2 ->
    56       Clight.Ebinop (binop, e1,
    57                      Clight.Expr (Clight.Econst_int i,
    58                                   Clight.Tint (Clight.I8, signedness1)))
    59     | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _),
    60       Clight.Expr
    61         (Clight.Ebinop
    62            (binop,
    63             Clight.Expr (Clight.Econst_int i, _),
    64             Clight.Expr
    65               (Clight.Ecast
    66                  (Clight.Tint (Clight.I32, _),
    67                   (Clight.Expr (_,
    68                                 Clight.Tint (Clight.I8, signedness2)) as e1)),
    69                _)),sub_ctypes_res sub_exprs_res
    70          _) :: _ when signedness1 = signedness2 ->
    71       Clight.Ebinop (binop,
    72                      Clight.Expr (Clight.Econst_int i,
    73                                   Clight.Tint (Clight.I8, signedness1)),
    74                      e1)
    75     | _ -> ClightFold.expr_descr_fill_subs e sub_ctypes_res sub_exprs_res
    76 *)
    77 
    78 let simplify_exp ctype_opt e = e (* TODO *)
    79 
    80185let f_expr e _ _ = e
    81186
    … …  
    83188
    84189let f_statement stmt _ sub_stmts_res =
    85   let sub_exprs = match stmt with
    86     | _ -> assert false in
     190  let f_expr b e =
     191    let e' = simplify_expr e in
     192    if b then cast_if_needed (type_of_expr e) e'
     193    else e' in
     194  let f_exprs b = List.map (f_expr b) in
     195  let f_sub_exprs = match stmt with
     196    | Clight.Sassign _ | Clight.Scall _ | Clight.Sreturn _ -> f_exprs true
     197    | _ -> f_exprs false in
     198  let sub_exprs = f_sub_exprs (ClightFold.statement_sub_exprs stmt) in
    87199  ClightFold.statement_fill_subs stmt sub_exprs sub_stmts_res
    88200
    … …  
    97209  (id, fundef')
    98210
    99 let simplify p = p
    100 (* (* TODO: below *)
     211let simplify p =
    101212  { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct }
    102 *)

  • Deliverables/D2.2/8051/src/clight/clightFold.ml

    r624 r818  
    7575  | _ -> assert false (* wrong arguments, do not use on these values *)
    7676
     77let expr_fill_exprs (Clight.Expr (ed, t)) exprs =
     78  let (sub_ctypes, _) = expr_descr_subs ed in
     79  let ed = expr_descr_fill_subs ed sub_ctypes exprs in
     80  Clight.Expr (ed, t)
     81
    7782let rec expr f_ctype f_expr f_expr_descr e =
    7883  let (sub_ctypes, sub_expr_descrs) = expr_subs e in
    … …  
    8893  let sub_ctypes_res = List.map (ctype f_ctype) sub_ctypes in
    8994  f_expr_descr e sub_ctypes_res sub_exprs_res
     95
     96
     97let expr_subs2 e =
     98  let (_, expr_descrs) = expr_subs e in
     99  let l = List.map expr_descr_subs expr_descrs in
     100  List.flatten (List.map snd l)
     101
     102let rec expr2 f e = f e (List.map (expr2 f) (expr_subs2 e))
    90103
    91104
    … …  
    108121  | Clight.Sswitch (e, lbl_stmts) -> ([e], labeled_statements_subs lbl_stmts)
    109122  | Clight.Slabel (_, stmt) | Clight.Scost (_, stmt) -> ([], [stmt])
     123
     124let statement_sub_exprs stmt = fst (statement_subs stmt)
    110125
    111126let rec labeled_statements_fill_subs lbl_stmts sub_statements =
    … …  
    149164    List.map (statement f_ctype f_expr f_expr_descr f_statement) sub_stmts in
    150165  f_statement stmt sub_exprs_res sub_stmts_res
     166
     167let rec statement2 f_expr f_statement stmt =
     168  let (sub_exprs, sub_stmts) = statement_subs stmt in
     169  let sub_exprs_res = List.map (expr2 f_expr) sub_exprs in
     170  let sub_stmts_res = List.map (statement2 f_expr f_statement) sub_stmts in
     171  f_statement stmt sub_exprs_res sub_stmts_res

  • Deliverables/D2.2/8051/src/clight/clightFold.mli

    r740 r818  
    1111  Clight.expr
    1212
     13val expr_fill_exprs :
     14  Clight.expr -> Clight.expr list -> Clight.expr
     15
    1316val expr :
    1417  (Clight.ctype -> 'a list -> 'a) ->
    … …  
    1720  Clight.expr ->
    1821  'c
     22
     23val expr2 :
     24  (Clight.expr -> 'a list -> 'a) -> Clight.expr -> 'a
     25
     26val expr_descr_subs :
     27  Clight.expr_descr -> Clight.ctype list * Clight.expr list
    1928
    2029val expr_descr_fill_subs :
    … …  
    2938  'b
    3039
     40val statement_subs :
     41  Clight.statement ->
     42  (Clight.expr list * Clight.statement list)
     43
     44val statement_sub_exprs : Clight.statement -> Clight.expr list
     45
    3146val statement_fill_subs :
    3247  Clight.statement -> Clight.expr list -> Clight.statement list ->
    … …  
    4055  Clight.statement ->
    4156  'd
     57
     58val statement2 :
     59  (Clight.expr -> 'a list -> 'a) ->
     60  (Clight.statement -> 'a list -> 'b list -> 'b) ->
     61  Clight.statement ->
     62  'b

  • Deliverables/D2.2/8051/src/clight/clightFromC.ml

    r486 r818  
    110110
    111111let typeStringLiteral s =
    112   Tarray(Tint(I8, Unsigned), String.length s + 1)
     112  Tarray(Tint(I8, AST.Unsigned), String.length s + 1)
    113113
    114114let global_for_string s id =
    … …  
    170170
    171171let convertIkind = function
    172   | C.IBool -> unsupported "'_Bool' type"; (Unsigned, I8)
    173   | C.IChar -> (Unsigned, I8)
    174   | C.ISChar -> (Signed, I8)
    175   | C.IUChar -> (Unsigned, I8)
    176   | C.IInt -> (Signed, I32)
    177   | C.IUInt -> (Unsigned, I32)
    178   | C.IShort -> (Signed, I16)
    179   | C.IUShort -> (Unsigned, I16)
    180   | C.ILong -> (Signed, I32)
    181   | C.IULong -> (Unsigned, I32)
     172  | C.IBool -> unsupported "'_Bool' type"; (AST.Unsigned, I8)
     173  | C.IChar -> (AST.Unsigned, I8)
     174  | C.ISChar -> (AST.Signed, I8)
     175  | C.IUChar -> (AST.Unsigned, I8)
     176  | C.IInt -> (AST.Signed, I32)
     177  | C.IUInt -> (AST.Unsigned, I32)
     178  | C.IShort -> (AST.Signed, I16)
     179  | C.IUShort -> (AST.Unsigned, I16)
     180  | C.ILong -> (AST.Signed, I32)
     181  | C.IULong -> (AST.Unsigned, I32)
    182182  | C.ILongLong ->
    183183      if not !ClightFlags.option_flonglong then unsupported "'long long' type";
    184       (Signed, I32)
     184      (AST.Signed, I32)
    185185  | C.IULongLong ->
    186186      if not !ClightFlags.option_flonglong then unsupported "'unsigned long long' type";
    187       (Unsigned, I32)
     187      (AST.Unsigned, I32)
    188188
    189189let convertFkind = function
    … …  
    268268(** Expressions *)
    269269
    270 let ezero = Expr(Econst_int(0), Tint(I32, Signed))
     270let ezero = Expr(Econst_int(0), Tint(I32, AST.Signed))
    271271
    272272let rec convertExpr env e =
    … …  
    393393let volatile_fun_suffix_type ty =
    394394  match ty with
    395   | Tint(I8, Unsigned) -> ("int8unsigned", ty)
    396   | Tint(I8, Signed) -> ("int8signed", ty)
    397   | Tint(I16, Unsigned) -> ("int16unsigned", ty)
    398   | Tint(I16, Signed) -> ("int16signed", ty)
    399   | Tint(I32, _) -> ("int32", Tint(I32, Signed))
     395  | Tint(I8, AST.Unsigned) -> ("int8unsigned", ty)
     396  | Tint(I8, AST.Signed) -> ("int8signed", ty)
     397  | Tint(I16, AST.Unsigned) -> ("int16unsigned", ty)
     398  | Tint(I16, AST.Signed) -> ("int16signed", ty)
     399  | Tint(I32, _) -> ("int32", Tint(I32, AST.Signed))
    400400  | Tfloat F32 -> ("float32", ty)
    401401  | Tfloat F64 -> ("float64", ty)

  • Deliverables/D2.2/8051/src/clight/clightInterpret.ml

    r740 r818  
    210210(* ctype functions *)
    211211
    212 let rec sizeof = function
    213   | Tint (I8, _)  -> 1
    214   | Tint (I16, _) -> 2
    215   | Tint (I32, _) -> 4
    216   | Tfloat _ -> error_float ()
    217   | Tcomp_ptr _ -> Mem.ptr_size
    218   | Tpointer _ -> Mem.ptr_size
    219   | Tarray (ty, n) -> n * (sizeof ty)
    220   | Tstruct (_, fields) ->
    221     let sizes = List.map sizeof (List.map snd fields) in
    222     snd (Mem.align 0 sizes)
    223   | Tunion (_, fields) ->
    224     MiscPottier.max_list (List.map sizeof (List.map snd fields))
    225   | _ -> assert false (* do not use on these arguments *)
     212let sizeof ctype = Mem.concrete_size (ClightToCminor.sizeof_ctype ctype)
    226213
    227214let size_of_ctype = function
    … …  
    279266(* Interpret *)
    280267
    281 let int_of_intsize = function
    282   | I8 -> 8
    283   | I16 -> 16
    284   | I32 -> 32
    285 
    286 let choose_cast signedness n m v =
    287   let f = match signedness with
     268let byte_of_intsize = function
     269  | I8 -> 1
     270  | I16 -> 2
     271  | I32 -> 4
     272
     273let choose_cast sign n m v =
     274  let f = match sign with
    288275    | Signed -> Value.sign_ext
    289276    | Unsigned -> Value.zero_ext in
    … …  
    292279let eval_cast = function
    293280  (* Cast Integer *)
    294   | (v,Tint(isize,signedness),Tint(isize',_)) ->
    295     choose_cast signedness (int_of_intsize isize) (int_of_intsize isize') v
     281  | (v,Tint(isize,sign),Tint(isize',_)) ->
     282    choose_cast sign (byte_of_intsize isize) (byte_of_intsize isize') v
    296283  | (v,_,_) -> v
    297284
    298 let eval_unop = function 
    299   | Onotbool -> Value.notbool
    300   | Onotint -> Value.notint
    301   | Oneg -> Value.negint
     285let to_int32 (v, t) = eval_cast (v, t, Tint (I32, Signed))
     286
     287let eval_unop ret_ctype ((_, t) as e) op =
     288  let v = to_int32 e in
     289  let v = match op with
     290    | Onotbool -> Value.notbool v
     291    | Onotint -> Value.notint v
     292    | Oneg -> Value.negint v in
     293  eval_cast (v, t, ret_ctype)
    302294
    303295let eval_add (v1,t1) (v2,t2) = match t1, t2 with
    … …  
    316308  | _ -> Value.sub v1 v2
    317309
    318 let choose_signedness op_signed op_unsigned v1 v2 t =
     310let choose_sign op_signed op_unsigned v1 v2 t =
    319311  let op = match t with
    320312    | Tint (_, Signed) -> op_signed
    … …  
    323315  op v1 v2
    324316
    325 let eval_binop ret_ctype ((v1,t1) as e1) ((v2,t2) as e2) op =
     317let eval_binop ret_ctype ((_, t1) as e1) ((_, t2) as e2) op =
     318  let v1 = to_int32 e1 in
     319  let v2 = to_int32 e2 in
     320  let e1 = (v1, t1) in
     321  let e2 = (v2, t2) in
    326322  let v = match op with
    327323    | Oadd -> eval_add e1 e2
    328324    | Osub -> eval_sub e1 e2
    329325    | Omul -> Value.mul v1 v2
    330     | Odiv -> choose_signedness Value.div Value.divu v1 v2 t1
    331     | Omod -> choose_signedness Value.modulo Value.modulou v1 v2 t1
     326    | Odiv -> choose_sign Value.div Value.divu v1 v2 t1
     327    | Omod -> choose_sign Value.modulo Value.modulou v1 v2 t1
    332328    | Oand -> Value.and_op v1 v2
    333329    | Oor -> Value.or_op v1 v2
    … …  
    335331    | Oshl-> Value.shl v1 v2
    336332    | Oshr-> Value.shr v1 v2
    337     | Oeq -> choose_signedness Value.cmp_eq Value.cmp_eq_u v1 v2 t1
    338     | One -> choose_signedness Value.cmp_ne Value.cmp_ne_u v1 v2 t1
    339     | Olt -> choose_signedness Value.cmp_lt Value.cmp_lt_u v1 v2 t1
    340     | Ole -> choose_signedness Value.cmp_le Value.cmp_le_u v1 v2 t1
    341     | Ogt -> choose_signedness Value.cmp_gt Value.cmp_gt_u v1 v2 t1
    342     | Oge -> choose_signedness Value.cmp_ge Value.cmp_ge_u v1 v2 t1 in
     333    | Oeq -> choose_sign Value.cmp_eq Value.cmp_eq_u v1 v2 t1
     334    | One -> choose_sign Value.cmp_ne Value.cmp_ne_u v1 v2 t1
     335    | Olt -> choose_sign Value.cmp_lt Value.cmp_lt_u v1 v2 t1
     336    | Ole -> choose_sign Value.cmp_le Value.cmp_le_u v1 v2 t1
     337    | Ogt -> choose_sign Value.cmp_gt Value.cmp_gt_u v1 v2 t1
     338    | Oge -> choose_sign Value.cmp_ge Value.cmp_ge_u v1 v2 t1 in
    343339  eval_cast (v, t1, ret_ctype)
    344340
    345 let rec get_offset_struct v id fields =
    346   let sizes = List.map (fun (_, ty) -> sizeof ty) fields in
    347   let (offsets, _) = Mem.align 0 sizes in
    348   let rec select = function
    349     | (x, _) :: _, off :: _ when x = id -> off
    350     | _ :: fields, _ :: offsets -> select (fields, offsets)
    351     | _ -> assert false (* should be impossible *) in
    352   let off = Value.of_int (select (fields, offsets)) in
     341let rec get_offset_struct v size id fields =
     342  let offsets = fst (Mem.concrete_offsets_size size) in
     343  let fields = List.combine (List.map fst fields) offsets in
     344  let off = Value.of_int (List.assoc id fields) in
    353345  Value.add v off
    354346
    355347let get_offset v id = function
    356   | Tstruct (_, fields) -> get_offset_struct v id fields
     348  | Tstruct (_, fields) as t ->
     349    let size = ClightToCminor.sizeof_ctype t in
     350    get_offset_struct v size id fields
    357351  | Tunion _ -> v
    358352  | _ -> assert false (* do not use on these arguments *)
    … …  
    390384      ((eval_binop tt v1 v2 op,tt),l1@l2)
    391385    | Eunop (op,exp) ->
    392       let ((v1,_),l1) = eval_expr localenv m exp in
    393       ((eval_unop op v1,tt),l1)
     386      let (e1,l1) = eval_expr localenv m exp in
     387      ((eval_unop tt e1 op,tt),l1)
    394388    | Econdition (e1,e2,e3) ->
    395389      let (v1,l1) = eval_expr localenv m e1 in
    … …  
    554548let interpret_external k mem f args =
    555549  let (mem', v) = match InterpretExternal.t mem f args with
    556     | (mem', InterpretExternal.V v) -> (mem', v)
     550    | (mem', InterpretExternal.V vs) ->
     551      let v = if List.length vs = 0 then Value.undef else List.hd vs in
     552      (mem', v)
    557553    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
    558554  Returnstate (v, k, mem')
    … …  
    583579  | Init_float32 f      -> error_float ()
    584580  | Init_float64 f      -> error_float ()
    585   | Init_space i        -> Data_reserve i
     581  | Init_space i        -> error "bad global initialization style."
    586582  | Init_addrof (x,off) -> assert false (* TODO: need the size of [x]'s cells *)
     583
     584let datas_of_init_datas = function
     585  | [Init_space _] -> None
     586  | l -> Some (List.map data_of_init_data l)
    587587
    588588let init_mem prog =
    589589  let f_var mem ((x, init_datas), ty) =
    590     Mem.add_var mem x (List.map data_of_init_data init_datas) in
     590    Mem.add_var mem x (ClightToCminor.sizeof_ctype ty)
     591      (datas_of_init_datas init_datas) in
    591592  let mem = List.fold_left f_var Mem.empty prog.prog_vars in
    592593  let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in
    … …  
    594595
    595596let compute_result v =
    596   if Value.is_int v then IntValue.Int8.cast (Value.to_int_repr v)
    597   else IntValue.Int8.zero
     597  if Value.is_int v then IntValue.Int32.cast (Value.to_int_repr v)
     598  else IntValue.Int32.zero
    598599
    599600let rec exec debug trace (state, l) =
    … …  
    601602  let print_and_return_result res =
    602603    if debug then Printf.printf "Result = %s\n%!"
    603       (IntValue.Int8.to_string res) ;
     604      (IntValue.Int32.to_string res) ;
    604605    (res, cost_labels) in
    605606  if debug then print_state state ;
    … …  
    608609      print_and_return_result (compute_result v)
    609610    | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *)
    610       print_and_return_result IntValue.Int8.zero
     611      print_and_return_result IntValue.Int32.zero
    611612    | state -> exec debug cost_labels (step state)
    612613
    613614let interpret debug prog =
    614   if debug then Printf.printf "*** Clight ***\n\n%!" ;
     615  Printf.printf "*** Clight interpret ***\n%!" ;
    615616  match prog.prog_main with
    616     | None -> (IntValue.Int8.zero, [])
     617    | None -> (IntValue.Int32.zero, [])
    617618    | Some main ->
    618619      let mem = init_mem prog in

  • Deliverables/D2.2/8051/src/clight/clightLabelling.ml

    r796 r818  
    1717
    1818
    19 let int_type = Tint (I32, Signed)
     19let int_type = Tint (I32, AST.Signed)
    2020let const_int i = Expr (Econst_int i, int_type)
    2121
    … …  
    105105        (Swhile (add_cost_labels_e cost_universe e, s'))
    106106  | Sdowhile (e,s) ->
    107       let s' = add_cost_labels_st cost_universe s in
    108       let s' = add_starting_cost_label cost_universe s' in
     107      let s1 = add_cost_labels_st cost_universe s in
     108      let s2 = add_cost_labels_st cost_universe s in
     109      let s2' = add_starting_cost_label cost_universe s2 in
    109110      add_ending_cost_label cost_universe
    110         (Sdowhile (add_cost_labels_e cost_universe e, s'))
     111        (Ssequence (s1, Swhile (add_cost_labels_e cost_universe e, s2')))
    111112  | Sfor (s1,e,s2,s3) ->
    112113      let s1' = add_cost_labels_st cost_universe s1 in

  • Deliverables/D2.2/8051/src/clight/clightParser.ml

    r740 r818  
    4242        | None -> failwith "Error during C to Clight pass."
    4343        | Some(pp) -> pp
    44       ) 
     44      )

  • Deliverables/D2.2/8051/src/clight/clightPrinter.ml

    r486 r818  
    541541  flush_str_formatter ()
    542542
     543let print_ctype_prot = name_type
     544
     545let print_ctype_def = function
     546  | Tstruct (name, fld) | Tunion (name, fld) ->
     547    let f_fld s (id, t) = s ^ "  " ^ (print_ctype_prot t) ^ " " ^ id ^ ";\n" in
     548    let s_fld = List.fold_left f_fld "" in
     549    name ^ " {\n" ^ (s_fld fld) ^ "};\n"
     550  | _ -> "" (* no definition associated to the other types *)

  • Deliverables/D2.2/8051/src/clight/clightPrinter.mli

    r486 r818  
    44val print_program: Clight.program -> string
    55
    6 val print_expression : Clight.expr -> string
     6val print_expression: Clight.expr -> string
    77
    88val string_of_ctype: Clight.ctype -> string
    99
    1010val print_statement: Clight.statement -> string
     11
     12val print_ctype_prot: Clight.ctype -> string
     13
     14val print_ctype_def: Clight.ctype -> string

  • Deliverables/D2.2/8051/src/clight/clightToCminor.ml

    r740 r818  
    1 open AST
    2 open Cminor
    3 open Clight
    4 
    5 
    6 let error_prefix = "Cminor to RTLabs"
     1
     2
     3let error_prefix = "Clight to Cminor"
    74let error = Error.global_error error_prefix
    85let error_float () = error "float not supported."
    96
    107
    11 (*For internal use*)
    12 type var_type =
     8(* General helpers *)
     9
     10let clight_type_of (Clight.Expr (_, t)) = t
     11
     12let cminor_type_of (Cminor.Expr (_, t)) = t
     13
     14
     15(* Translate types *)
     16
     17let byte_size_of_intsize = function
     18  | Clight.I8 -> 1
     19  | Clight.I16 -> 2
     20  | Clight.I32 -> 4
     21
     22let sig_type_of_ctype = function
     23  | Clight.Tvoid -> assert false (* do not use on this argument *)
     24  | Clight.Tint (intsize, sign) ->
     25    AST.Sig_int (byte_size_of_intsize intsize, sign)
     26  | Clight.Tfloat _ -> error_float ()
     27  | Clight.Tfunction _ | Clight.Tstruct _ | Clight.Tunion _
     28  | Clight.Tpointer _ | Clight.Tarray _ | Clight.Tcomp_ptr _ -> AST.Sig_ptr
     29
     30let translate_args_types = List.map sig_type_of_ctype
     31
     32let type_return_of_ctype = function
     33  | Clight.Tvoid -> AST.Type_void
     34  | t -> AST.Type_ret (sig_type_of_ctype t)
     35
     36let quantity_of_sig_type = function
     37  | AST.Sig_int (size, _) -> AST.QInt size
     38  | AST.Sig_float _ -> error_float ()
     39  | AST.Sig_offset -> AST.QOffset
     40  | AST.Sig_ptr -> AST.QPtr
     41
     42let quantity_of_ctype t = quantity_of_sig_type (sig_type_of_ctype t)
     43
     44let rec sizeof_ctype = function
     45  | Clight.Tvoid | Clight.Tfunction _ -> AST.SQ (AST.QInt 1)
     46  | Clight.Tfloat _ -> error_float ()
     47  | Clight.Tint (size, _) -> AST.SQ (AST.QInt (byte_size_of_intsize size))
     48  | Clight.Tpointer _
     49  | Clight.Tcomp_ptr _ -> AST.SQ AST.QPtr
     50  | Clight.Tarray (t, n) -> AST.SArray (n, sizeof_ctype t)
     51  | Clight.Tstruct (_, fields) ->
     52    AST.SProd (List.map sizeof_ctype (List.map snd fields))
     53  | Clight.Tunion (_, fields) ->
     54    AST.SSum (List.map sizeof_ctype (List.map snd fields))
     55
     56let global_size_of_ctype = sizeof_ctype
     57
     58
     59(** Helpers on abstract sizes and offsets *)
     60
     61let max_stacksize size1 size2 = match size1, size2 with
     62  | AST.SProd l1, AST.SProd l2 when List.length l1 > List.length l2 -> size1
     63  | AST.SProd l1, AST.SProd l2 -> size2
     64  | _ -> raise (Failure "ClightToCminor.max_stacksize")
     65
     66(** Hypothesis: [offset1] is a prefix of [offset2] or vice-versa. *)
     67let max_offset offset1 offset2 =
     68  if List.length offset1 > List.length offset2 then offset1
     69  else offset2
     70
     71let next_depth = function
     72  | AST.SProd l -> List.length l
     73  | _ -> raise (Failure "ClightToCminor.next_offset")
     74
     75let add_stack offset =
     76  let e1 = Cminor.Expr (Cminor.Cst AST.Cst_stack, AST.Sig_ptr) in
     77  let e2 = Cminor.Expr (Cminor.Cst (AST.Cst_offset offset), AST.Sig_offset) in
     78  Cminor.Op2 (AST.Op_addp, e1, e2)
     79
     80let add_stacksize t = function
     81  | AST.SProd l -> AST.SProd (l @ [sizeof_ctype t])
     82  | _ -> raise (Failure "ClightToCminor.add_stacksize")
     83
     84let struct_depth field fields =
     85  let rec aux i = function
     86    | [] -> error ("unknown field " ^ field ^ ".")
     87    | (field', t) :: _ when field' = field -> i
     88    | (_, t) :: fields -> aux (i+1) fields in
     89  aux 0 fields
     90
     91let struct_offset t field fields =
     92  let size = sizeof_ctype t in
     93  let depth = struct_depth field fields in
     94  let offset = (size, depth) in
     95  let t = AST.Sig_offset in
     96  Cminor.Expr (Cminor.Cst (AST.Cst_offset offset), t)
     97
     98
     99(** Sort variables: locals, parameters, globals, in stack. *)
     100
     101type location =
     102  | Local
     103  | LocalStack of AST.abstract_offset
     104  | Param
     105  | ParamStack of AST.abstract_offset
    13106  | Global
    14   | Stack of int (*Note: this is a constraint on the size of the stack.*)
    15   | Param
    16   | Local
    17 
    18 (*Parametrisation by int and pointer size *)
    19 let int_size = Driver.CminorMemory.int_size
    20 let ptr_size = Driver.CminorMemory.ptr_size
    21 let alignment = Driver.CminorMemory.alignment
    22 
    23 let fresh_tmp variables =
    24   let rec ft i =
    25     let tmp = "tmp"^(string_of_int i) in
    26       try (match Hashtbl.find variables tmp with _ -> ft (i+1))
    27       with Not_found -> tmp
    28   in ft 0
    29 
    30 let rec ctype_to_type_return t = match t with
    31   | Tvoid       -> Type_void
    32   | Tfloat _    -> Type_ret Sig_float (*Not supported*)
    33   | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_) -> Type_ret Sig_ptr
    34   | _           -> Type_ret Sig_int
    35 
    36 let rec ctype_to_sig_type t = match t with
    37   | Tfloat _    ->
    38       Sig_float (*Not supported but needed for external function from library*)
    39   | Tvoid       -> assert false
    40   | Tpointer _ | Tstruct (_,_) | Tunion (_,_) | Tarray(_,_) -> Sig_ptr
    41   | _           -> Sig_int
    42 
    43 let rec size_of_ty = function
    44   | Tvoid               -> assert false
    45   | Tfloat _            -> assert false (*Not supported*)
    46   | Tfunction (_,_)     -> assert false (*Not supported*)
    47   | Tint (I8,Signed)    -> 1
    48   | Tint (I8,Unsigned)  -> 1
    49   | Tint (I16,Signed)   -> 2
    50   | Tint (I16,Unsigned) -> 2
    51   (*FIXME MQ_int32 : signed or unsigned ? *)
    52   | Tint (I32,Signed)   -> 4
    53   | Tint (I32,Unsigned) -> 4
    54   | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_)
    55   | Tcomp_ptr _         -> ptr_size
    56 
    57 let size_of_intsize = function
    58   | I8 -> 1
    59   | I16 -> 2
    60   | I32 -> 4
    61 
    62 let quantity_of_ty = function
    63   | Tvoid               -> assert false (* do not use on this argument *)
    64   | Tint (size,_)       -> Memory.QInt (size_of_intsize size)
    65   | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_)
    66   | Tfunction (_,_)
    67   | Tcomp_ptr _         -> Memory.QPtr
    68   | Tfloat _            -> error_float ()
    69 
    70 let init_to_data l = List.map (
     107
     108(** Below are some helper definitions to ease the manipulation of a translation
     109    environment for variables. *)
     110
     111type var_locations = (location * Clight.ctype) StringTools.Map.t
     112
     113let empty_var_locs : var_locations = StringTools.Map.empty
     114
     115let add_var_locs : AST.ident -> (location * Clight.ctype) -> var_locations ->
     116  var_locations =
     117  StringTools.Map.add
     118
     119let mem_var_locs : AST.ident -> var_locations -> bool = StringTools.Map.mem
     120
     121let find_var_locs : AST.ident -> var_locations -> (location * Clight.ctype) =
     122  StringTools.Map.find
     123
     124let fold_var_locs : (AST.ident -> (location * Clight.ctype) -> 'a -> 'a) ->
     125  var_locations -> 'a -> 'a =
     126  StringTools.Map.fold
     127
     128
     129let is_local_or_param id var_locs = match find_var_locs id var_locs with
     130  | (Local, _) | (Param, _) -> true
     131  | _ -> false
     132
     133let get_locals var_locs =
     134  let f id (location, ctype) locals =
     135    let added = match location with
     136      | Local -> [(id, sig_type_of_ctype ctype)]
     137      | _ -> [] in
     138    locals @ added in
     139  fold_var_locs f var_locs []
     140
     141let get_stacksize var_locs =
     142  let f _ (location, _) res = match location with
     143    | LocalStack (stacksize, _) | ParamStack (stacksize, _) ->
     144      max_stacksize res stacksize
     145    | _ -> res in
     146  fold_var_locs f var_locs (AST.SProd [])
     147
     148
     149(* Variables of a function that will go in stack: variables of a complex type
     150   (array, structure or union) and variables whose address is evaluated. *)
     151
     152let is_function_ctype = function
     153  | Clight.Tfunction _ -> true
     154  | _ -> false
     155
     156let is_scalar_ctype : Clight.ctype -> bool = function
     157  | Clight.Tint _ | Clight.Tfloat _ | Clight.Tpointer _ -> true
     158  | _ -> false
     159
     160let is_complex_ctype : Clight.ctype -> bool = function
     161  | Clight.Tarray _ | Clight.Tstruct _ | Clight.Tunion _ | Clight.Tfunction _ ->
     162    true
     163  | _ -> false
     164
     165let complex_ctype_vars cfun =
     166  let f set (x, t) =
     167    if is_complex_ctype t then StringTools.Set.add x set else set in
     168  (* Because of CIL, parameters should not have a complex type, but let's add
     169     them just in case. *)
     170  List.fold_left f StringTools.Set.empty
     171    (cfun.Clight.fn_params @ cfun.Clight.fn_vars)
     172
     173let union_list = List.fold_left StringTools.Set.union StringTools.Set.empty
     174
     175let f_expr (Clight.Expr (ed, _)) sub_exprs_res =
     176  let res_ed = match ed with
     177    | Clight.Eaddrof (Clight.Expr (Clight.Evar id, _)) ->
     178      StringTools.Set.singleton id
     179    | _ -> StringTools.Set.empty in
     180  union_list (res_ed :: sub_exprs_res)
     181
     182let f_stmt _ sub_exprs_res sub_stmts_res =
     183  union_list (sub_exprs_res @ sub_stmts_res)
     184
     185let addr_vars_fun cfun = ClightFold.statement2 f_expr f_stmt cfun.Clight.fn_body
     186
     187let stack_vars cfun =
     188  StringTools.Set.union (complex_ctype_vars cfun) (addr_vars_fun cfun)
     189
     190
     191let sort_stacks stack_location vars var_locs =
     192  let stacksize = get_stacksize var_locs in
     193  let f (current_stacksize, var_locs) (id, t) =
     194    let depth = next_depth current_stacksize in
     195    let current_stacksize = add_stacksize t current_stacksize in
     196    let offset = (current_stacksize, depth) in
     197    let var_locs = add_var_locs id (stack_location offset, t) var_locs in
     198    (current_stacksize, var_locs) in
     199  snd (List.fold_left f (stacksize, var_locs) vars)
     200
     201let sort_normals normal_location vars var_locs =
     202  let f var_locs (id, ctype) =
     203    add_var_locs id (normal_location, ctype) var_locs in
     204  List.fold_left f var_locs vars
     205
     206let sort_vars normal_location stack_location_opt stack_vars vars var_locs =
     207  let f_stack (x, _) = StringTools.Set.mem x stack_vars in
     208  let (f_normal, var_locs) = match stack_location_opt with
     209    | None -> ((fun _ -> true), var_locs)
     210    | Some stack_location ->
     211      ((fun var -> not (f_stack var)),
     212       sort_stacks stack_location (List.filter f_stack vars) var_locs) in
     213  sort_normals normal_location (List.filter f_normal vars) var_locs
     214
     215let sort_locals = sort_vars Local (Some (fun offset -> LocalStack offset))
     216
     217let sort_params = sort_vars Param (Some (fun offset -> ParamStack offset))
     218
     219let sort_globals stack_vars globals var_locs =
     220  let globals = List.map (fun ((id, _), ctype) -> (id, ctype)) globals in
     221  sort_vars Global None stack_vars globals var_locs
     222
     223(* The order of insertion in the sorting environment is important: it follows
     224   the scope conventions of C. Local variables hide parameters that hide
     225   globals. *)
     226
     227let sort_variables globals cfun =
     228  let stack_vars = stack_vars cfun in
     229  let var_locs = empty_var_locs in
     230  let var_locs = sort_globals stack_vars globals var_locs in
     231  let var_locs = sort_params stack_vars cfun.Clight.fn_params var_locs in
     232  let var_locs = sort_locals stack_vars cfun.Clight.fn_vars var_locs in
     233  var_locs
     234
     235
     236(* Translate globals *)
     237
     238let init_to_data = function
     239  | [Clight.Init_space _] -> None
     240  | l -> Some (List.map (
    71241  function
    72     | Init_int8 i       -> Data_int8 i
    73     | Init_int16 i      -> Data_int16 i
    74     | Init_int32 i      -> Data_int32 i
    75     | Init_float32 _
    76     | Init_float64 _    -> assert false (*Not supported*)
    77     | Init_space n      -> Data_reserve n
    78     | Init_addrof (_,_) -> assert false (*TODO*)
    79 ) l
    80 
    81 let rec size_of_ctype t = match t with
    82   | Tvoid                       -> 0
    83   | Tint (I8,_)                 -> 1
    84   | Tint (I16,_)                -> 2
    85   | Tint (I32,_)                -> 4
    86   | Tpointer _                  -> ptr_size     
    87   | Tarray (c,s)                -> s*(size_of_ctype c)
    88   | Tstruct (_,lst)             ->
    89       List.fold_left
    90         (fun n (_,ty) -> n+(size_of_ctype ty)) 0 lst
    91   | Tunion (_,lst)              ->
    92       List.fold_left
    93         (fun n (_,ty) ->
    94            let sz = (size_of_ctype ty) in (if n>sz then n else sz)
    95         ) 0 lst
    96   | Tfloat _ | Tfunction (_,_)  -> assert false (*Not supported*)
    97   | Tcomp_ptr _                 -> ptr_size     
    98 
    99 let translate_global_vars ((id,lst),_) = (id,init_to_data lst)
    100 
    101 let translate_unop t = function
    102   | Onotbool                    -> Op_notbool
    103   | Onotint                     -> Op_notint
    104   | Oneg -> (match t with
    105                | Tint (_,_)     -> Op_negint
    106                | Tfloat _       -> assert false  (*Not supported*)
    107                | _              -> assert false  (*Type error*)
    108     )
    109 
    110 let translate_cmp t1 t2 cmp =
    111   match (t1,t2) with
    112     | (Tint(_,Signed),Tint(_,Signed))           -> Op_cmp cmp
    113     | (Tint(_,Unsigned),Tint(_,Unsigned))       -> Op_cmpu cmp
    114     | (Tpointer _,Tpointer _)                   -> Op_cmpp cmp
    115     | _                                         -> Op_cmp cmp 
    116 
    117 let translate_add e1 e2 = function
    118   | (Tint(_,_),Tint(_,_))       -> Op2 (Op_add,e1,e2)
    119   | (Tfloat _,Tfloat _)         -> assert false (*Not supported*)
    120   | (Tpointer t,Tint(_,_))      ->
    121       Op2 (Op_addp,e1, Op2 (Op_mul,e2,Cst (Cst_int (size_of_ctype t))))
    122   | (Tint(_,_),Tpointer t)      ->
    123       Op2 (Op_addp,e2,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))))
    124   | (Tarray (t,_),Tint(_,_))    ->
    125       Op2 (Op_addp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    126   | (Tint(_,_),Tarray(t,_))     ->
    127       Op2 (Op_addp,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
    128   | _                           -> assert false (*Type error*)
    129 
    130 let translate_sub e1 e2 = function
    131   | (Tint(_,_),Tint(_,_))       -> Op2 (Op_sub,e1,e2)
    132   | (Tfloat _,Tfloat _)         -> assert false (*Not supported*)
    133   | (Tpointer t,Tint(_,_))      ->
    134       Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    135   | (Tarray (t,_),Tint(_,_))    ->
    136       Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    137   | _                           -> assert false (*Type error*)
    138 
    139 let translate_mul e1 e2 = function
    140   | (Tint(_,_),Tint(_,_))       -> Op2 (Op_mul,e1,e2)
    141   | (Tfloat _,Tfloat _)         -> assert false (*Not supported*)
    142   | _                           -> assert false (*Type error*)
    143 
    144 let translate_div e1 e2 = function
    145   | (Tint(_,Signed),Tint(_,Signed))     -> Op2 (Op_div,e1,e2)
    146   | (Tint(_,Unsigned),Tint(_,Unsigned)) -> Op2 (Op_divu,e1,e2)
    147   | (Tfloat _,Tfloat _)                 -> assert false (*Not supported*)
    148   | _                                   -> assert false (*Type error*)
    149 
    150 let translate_binop t1 e1 t2 e2 = function
    151   | Oadd -> translate_add e1 e2 (t1,t2)
    152   | Osub -> translate_sub e1 e2 (t1,t2)
    153   | Omul -> translate_mul e1 e2 (t1,t2)
    154   | Odiv -> translate_div e1 e2 (t1,t2)
    155   | Omod -> Op2 (Op_mod,e1,e2)
    156   | Oand -> Op2 (Op_and,e1,e2)
    157   | Oor  -> Op2 (Op_or,e1,e2)
    158   | Oxor -> Op2 (Op_xor,e1,e2)
    159   | Oshl -> Op2 (Op_shl,e1,e2)
    160   | Oshr -> Op2 (Op_shr,e1,e2)
    161   | Oeq  -> Op2 (translate_cmp t1 t2 Cmp_eq,e1,e2)
    162   | One  -> Op2 (translate_cmp t1 t2 Cmp_ne,e1,e2)
    163   | Olt  -> Op2 (translate_cmp t1 t2 Cmp_lt,e1,e2)
    164   | Ogt  -> Op2 (translate_cmp t1 t2 Cmp_gt,e1,e2)
    165   | Ole  -> Op2 (translate_cmp t1 t2 Cmp_le,e1,e2)
    166   | Oge  -> Op2 (translate_cmp t1 t2 Cmp_ge,e1,e2)
    167 
    168 let make_cast e = function
    169   | (Tint(I8,Signed),Tint(_,_))    -> Op1 (Op_cast8signed,e)
    170   | (Tint(I8,Unsigned),Tint(_,_))  -> Op1 (Op_cast8unsigned,e)
    171   | (Tint(I16,Signed),Tint(_,_))   -> Op1 (Op_cast16signed,e)
    172   | (Tint(I16,Unsigned),Tint(_,_)) -> Op1 (Op_cast16unsigned,e)
    173   | _ -> e
    174 
    175 let get_type (Expr (_,t)) = t
    176 
    177 let rec get_offset_struct e id = function
    178   | [] -> assert false (*Wrong id*)
    179   | (fi,_)::_ when fi=id -> e
    180   | (_,ty)::ll -> get_offset_struct (e+(size_of_ctype ty)) id ll
    181 
    182 let is_struct = function
    183   | Tarray(_,_) | Tstruct (_,_) | Tunion(_,_) -> true
     242    | Clight.Init_int8 i       -> AST.Data_int8 i
     243    | Clight.Init_int16 i      -> AST.Data_int16 i
     244    | Clight.Init_int32 i      -> AST.Data_int32 i
     245    | Clight.Init_float32 _
     246    | Clight.Init_float64 _    -> error_float ()
     247    | Clight.Init_space n      -> error "bad global initialization style."
     248    | Clight.Init_addrof (_,_) -> assert false (*TODO*)
     249) l)
     250
     251let translate_global ((id,lst),t) = (id,global_size_of_ctype t,init_to_data lst)
     252
     253
     254(* Translate expression *)
     255
     256let translate_unop = function
     257  | Clight.Onotbool -> AST.Op_notbool
     258  | Clight.Onotint -> AST.Op_notint
     259  | Clight.Oneg -> AST.Op_negint
     260
     261let esizeof_ctype res_type t =
     262  Cminor.Expr (Cminor.Cst (AST.Cst_sizeof (sizeof_ctype t)), res_type)
     263
     264let translate_add res_type ctype1 ctype2 e1 e2 = match ctype1, ctype2 with
     265  | Clight.Tint _, Clight.Tint _ ->
     266    Cminor.Expr (Cminor.Op2 (AST.Op_add, e1, e2), res_type)
     267  | Clight.Tfloat _, Clight.Tfloat _ -> error_float ()
     268  | Clight.Tpointer t, Clight.Tint _
     269  | Clight.Tarray (t, _), Clight.Tint _ ->
     270    let t2 = cminor_type_of e2 in
     271    let size = esizeof_ctype t2 t in
     272    let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e2, size), t2) in
     273    Cminor.Expr (Cminor.Op2 (AST.Op_addp, e1, index), res_type)
     274  | Clight.Tint _, Clight.Tpointer t
     275  | Clight.Tint _, Clight.Tarray (t, _) ->
     276    let t1 = cminor_type_of e1 in
     277    let size = esizeof_ctype t1 t in
     278    let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e1, size), t1) in
     279    Cminor.Expr (Cminor.Op2 (AST.Op_addp, e2, index), res_type)
     280  | _ -> error "type error."
     281
     282let translate_sub res_type ctype1 ctype2 e1 e2 = match ctype1, ctype2 with
     283  | Clight.Tint _, Clight.Tint _ ->
     284    Cminor.Expr (Cminor.Op2 (AST.Op_sub, e1, e2), res_type)
     285  | Clight.Tfloat _, Clight.Tfloat _ -> error_float ()
     286  | Clight.Tpointer t, Clight.Tint _
     287  | Clight.Tarray (t, _), Clight.Tint _ ->
     288    let t2 = cminor_type_of e2 in
     289    let size = esizeof_ctype t2 t in
     290    let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e2, size), t2) in
     291    Cminor.Expr (Cminor.Op2 (AST.Op_subp, e1, index), res_type)
     292  | Clight.Tpointer _, Clight.Tpointer _
     293  | Clight.Tarray _, Clight.Tpointer _
     294  | Clight.Tpointer _, Clight.Tarray _
     295  | Clight.Tarray _, Clight.Tarray _ ->
     296    Cminor.Expr (Cminor.Op2 (AST.Op_subpp, e1, e2), res_type)
     297  | _ -> error "type error."
     298
     299let is_signed = function
     300  | Clight.Tint (_, AST.Signed) -> true
    184301  | _ -> false
    185302
    186 let is_ptr_to_struct = function
    187   | Tpointer t when is_struct t -> true
    188   | _ -> false 
    189 
    190 let is_function = function
    191   | Tfunction _ -> true
     303let is_pointer = function
     304  | Clight.Tpointer _ | Clight.Tarray _ -> true
    192305  | _ -> false
    193306
    194 let rec translate_expr variables expr =
    195   let Expr(d,c) = expr in match d with
    196     | Econst_int i      -> Cst (Cst_int i)
    197     | Econst_float f    -> assert false (*Not supported*)
    198     | Evar id when is_function c -> Cst (Cst_addrsymbol id)
    199     | Evar id           -> 
    200         (try (match Hashtbl.find variables id with
    201            | (Local,_)          -> Id id
    202            | (Stack o,ty) when is_struct ty     -> Cst (Cst_stackoffset o)
    203            | (Stack o,_)        ->
    204              Mem (quantity_of_ty c,Cst (Cst_stackoffset o))
    205            | (Param,_)          -> Id id
    206            | (Global,ty) when is_struct ty -> Cst (Cst_addrsymbol id)
    207            | (Global,_)         ->
    208              Mem (quantity_of_ty c,Cst (Cst_addrsymbol id))
    209         ) with Not_found -> assert false)
    210     | Ederef e when is_ptr_to_struct (get_type e) ->
    211         translate_expr variables e
    212     | Ederef e          -> Mem (quantity_of_ty c,translate_expr variables e)
    213     | Eaddrof se        ->  (
    214         match se with
    215           | Expr(Evar id,_) ->
    216              (try  (match Hashtbl.find variables id with
    217                  | (Local,_) -> assert false (*Impossible: see sort_variables*)
    218                  | (Stack o,_) -> Cst (Cst_stackoffset o)
    219                  | (Param,_) ->  Cst (Cst_addrsymbol id)
    220                  | (Global,_) -> Cst (Cst_addrsymbol id)
    221               ) with Not_found -> assert false)
    222           | Expr(Ederef ee,_)                              ->
    223               translate_expr variables ee
    224           | Expr(Efield (str,fi),_)  ->
    225               (match str with
    226                  | Expr(_,Tstruct(_,b)) ->
    227                      Op2 (Op_add
    228                           ,translate_expr variables str
    229                           ,Cst (Cst_int (get_offset_struct 0 fi b)))
    230                  | Expr(_,Tunion(_,_)) ->
    231                      translate_expr variables str
    232                  | _ -> assert false (*Type Error*)
    233               )
    234           | _ ->  assert false (*Must be a lvalue*)
    235       )
    236     | Eunop (op,e)      ->
    237         Op1 (translate_unop (get_type e) op ,translate_expr variables e)
    238     | Ebinop (op,e1,e2) ->
    239         translate_binop
    240           (get_type e1) (translate_expr variables e1)
    241           (get_type e2) (translate_expr variables e2) op
    242     | Ecast (ty,e)     -> make_cast (translate_expr variables e) (get_type e,ty)
    243     | Econdition (e1,e2,e3) ->
    244         Cond (translate_expr variables e1,
    245               translate_expr variables e2,
    246               translate_expr variables e3)
    247     | Eandbool (e1,e2) ->
    248         Cond (
    249           translate_expr variables e1,
    250           Cond(translate_expr variables e2,Cst (Cst_int 1),Cst (Cst_int 0)),
    251           Cst (Cst_int 0))
    252     | Eorbool (e1,e2) ->
    253         Cond (
    254           translate_expr variables e1,
    255           Cst (Cst_int 1),
    256           Cond(translate_expr variables e2, Cst (Cst_int 1),Cst (Cst_int 0)) )
    257     | Esizeof cc        -> Cst (Cst_int (size_of_ctype cc))
    258     | Efield (e,id)     ->
    259         (match get_type e with
    260            | Tstruct(_,lst) ->
    261                (try
    262                   Mem (quantity_of_ty (List.assoc id lst)
    263                        ,Op2(Op_add
    264                             ,translate_expr variables e
    265                             , Cst (Cst_int (get_offset_struct 0 id lst))
    266                        )
    267                   )
    268                 with Not_found -> assert false (*field does not exists*)
    269                )
    270            | Tunion(_,lst) ->
    271                (try
    272                   Mem (quantity_of_ty (List.assoc id lst), translate_expr variables e)
    273                 with Not_found -> assert false (*field does not exists*)
    274                )
    275            | _ -> assert false (*Type error*)
    276         )
    277     | Ecost (lbl,e)     -> Exp_cost (lbl,translate_expr variables e)
    278     | Ecall _           -> assert false (* Only for annotations *)
    279 
    280 let translate_assign variables e = function
    281   | Expr (Evar v,t) ->
    282       (try (match Hashtbl.find variables v with
    283          | (Local,_)            -> St_assign (v,translate_expr variables e)
    284          | (Stack o,_)          -> St_store (quantity_of_ty t
    285                                              ,Cst (Cst_stackoffset o)
    286                                              ,translate_expr variables e)
    287          | (Param,_)            -> St_assign (v,translate_expr variables e)
    288          | (Global,_)           -> St_store (quantity_of_ty t
    289                                              ,Cst (Cst_addrsymbol v)
    290                                              ,translate_expr variables e)
    291       ) with Not_found -> assert false)
    292   | Expr (Ederef ee,t)          -> St_store (quantity_of_ty t
    293                                              ,translate_expr variables ee
    294                                              ,translate_expr variables e)
    295   | Expr (Efield (ee,id),t) ->
    296       (match ee with
    297          | Expr (_,Tstruct(_,lst)) ->
    298              St_store (quantity_of_ty t
    299                        ,Op2(Op_add,translate_expr variables ee
    300                             ,Cst(Cst_int (get_offset_struct 0 id lst )))
    301                        ,translate_expr variables e)
    302          | Expr (_,Tunion(_,_)) -> St_store (quantity_of_ty t
    303                                              ,translate_expr variables ee
    304                                              ,translate_expr variables e)
    305          | _ -> assert false (*Type error*)
    306       )
    307   | _                           -> assert false (*lvalue error*)
    308 
    309 let translate_call_name variables = function
    310   | Expr (Evar id,_)    -> Cst (Cst_addrsymbol id)
    311   | _                   -> assert false (*Not supported*)
    312 
    313 let translate_call variables e1 e2 lst =
    314   let st_call f_assign f_res =
    315     St_call (f_assign
    316              ,translate_expr variables e2
    317              ,List.map (translate_expr variables) lst
    318              ,{args=List.map (fun exp ->
    319                                 let Expr(_,t) = exp in ctype_to_sig_type t
    320              )lst;res=f_res}
    321         ) in
    322     match e1 with
    323       | Some (Expr (se,tt)) -> (
    324           match se with
    325             | Evar v ->
    326                 (try (match Hashtbl.find variables v with
    327                    | (Local,_) | (Param,_) ->
    328                        st_call (Some v) (Type_ret (ctype_to_sig_type tt))
    329                    | (Stack o,_) ->
    330                        let tmp = fresh_tmp variables in
    331                          St_seq (
    332                            st_call (Some tmp) (Type_ret (ctype_to_sig_type tt))
    333                            ,St_store (quantity_of_ty tt,Cst (Cst_stackoffset o),Id tmp)
    334                          )
    335                    | (Global,_) ->
    336                        let tmp = fresh_tmp variables in
    337                          St_seq (
    338                            st_call (Some tmp) (Type_ret (ctype_to_sig_type tt))
    339                            ,St_store (quantity_of_ty tt,Cst (Cst_addrsymbol v),Id tmp)
    340                          )
    341                 ) with Not_found -> assert false )
    342             | Ederef ee         -> assert false (*Not supported*)
    343             | Efield (ee,id)    -> assert false (*Not supported*)
    344             | _ -> assert false (*Should be a lvalue*)
    345         )
    346       | None -> st_call None Type_void
    347 
    348 (*TODO rewrite this buggy function*)                 
    349 let translate_switch expr (cases,default) =
    350   let sz = List.length cases in
    351   let sw = St_block (St_switch (
    352     expr, MiscPottier.mapi (fun i (n,_) -> (n,i)) cases, sz)) in
    353   let rec add_block n e = function
    354     | [] -> St_block (St_seq(e,default))
    355     | (_,st)::l ->
    356         add_block (n-1) (St_block (St_seq(e,St_seq(st,St_exit n)))) l
    357   in add_block sz sw cases
    358 
    359 let rec translate_stmt variables = function
    360   | Sskip               -> St_skip
    361   | Sassign (e1,e2)     -> translate_assign variables e2 e1
    362   | Scall (e1,e2,lst)   -> translate_call variables e1 e2 lst
    363   | Ssequence (s1,s2)   ->
    364       St_seq (translate_stmt variables s1,
    365               translate_stmt variables s2)
    366   | Sifthenelse (e,s1,s2) ->
    367       St_ifthenelse (translate_expr variables e,
    368                      translate_stmt variables s1,
    369                      translate_stmt variables s2)
    370   | Swhile (e,s)        ->
    371       St_block(St_loop(St_seq (
    372         St_ifthenelse (
    373           Op1 (Op_notbool,translate_expr variables e),
    374           St_exit 0,St_skip),
    375         St_block (translate_stmt variables s)
    376       )))
    377   | Sdowhile (e,s)      ->
    378       St_block(St_loop(St_seq (
    379         St_block (translate_stmt variables s),
    380         St_ifthenelse (
    381           Op1(Op_notbool, translate_expr variables e),
    382           St_exit 0,St_skip)
    383       )))
    384   | Sfor (s1,e,s2,s3)   ->
    385       let b = St_block (St_loop (St_seq (
    386         St_ifthenelse (
    387           Op1(Op_notbool,translate_expr variables e),
    388           St_exit 0,St_skip),
    389         St_seq (St_block (translate_stmt variables s3),
    390                 translate_stmt variables s2
    391         )))) in
    392         (match (translate_stmt variables s1) with
    393            | St_skip -> b | ss -> St_seq (ss,b))
    394   | Sbreak              -> St_exit(1)           
    395   | Scontinue           -> St_exit(0)
    396   | Sreturn (Some e)    -> St_return (Some(translate_expr variables e))
    397   | Sreturn None        -> St_return None
    398   | Sswitch (e,lbl)     ->
    399       translate_switch (translate_expr variables e) (compute_lbl variables lbl)
    400   | Slabel (lbl,st)     ->
    401       St_label(lbl,translate_stmt variables st)
    402   | Sgoto lbl           -> St_goto lbl
    403   | Scost (lbl,s)       -> St_cost(lbl,translate_stmt variables s)
    404 
    405 and compute_lbl variables = function
    406   | LSdefault s -> ([],translate_stmt variables s)
    407   | LScase (i,s,l) ->
    408       let (ll,def) = (compute_lbl variables l) in
    409         ((i,translate_stmt variables s)::ll,def)
    410 
    411 let rec get_stack_vars_expr (Expr (exp,_)) = match exp with
    412   | Econst_int _  | Evar _ | Esizeof _ -> []
    413   | Ederef e -> (get_stack_vars_expr e)
    414   | Eaddrof Expr(e,_) -> (
    415       match e with
    416         | Evar id                       -> [id]
    417         | Ederef ee | Efield (ee,_)     -> (get_stack_vars_expr ee)
    418         | _                             -> assert false (*Should be a lvalue*)
    419     )
    420   | Eunop (_,e) -> (get_stack_vars_expr e)
    421   | Ebinop (_,e1,e2) -> (get_stack_vars_expr e1)@(get_stack_vars_expr e2)
    422   | Ecast (_,e) -> (get_stack_vars_expr e)
    423   | Econdition (e1,e2,e3) ->
    424       (get_stack_vars_expr e1)@(get_stack_vars_expr e2)
    425       @(get_stack_vars_expr e3)
    426   | Eandbool (e1,e2) -> (get_stack_vars_expr e1)@(get_stack_vars_expr e2)
    427   | Eorbool (e1,e2) -> (get_stack_vars_expr e1)@(get_stack_vars_expr e2)
    428   | Ecost (_,e) -> (get_stack_vars_expr e)
    429   | Efield (e,_) -> (get_stack_vars_expr e)
    430   | Econst_float _ -> assert false (*Not supported*)
    431   | Ecall _ -> assert false (* Should not happen *)
    432