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

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

Location:
Deliverables/D2.2/8051/src/ERTL
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • 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, _)
Note: See TracChangeset for help on using the changeset viewer.