Changeset 1568 for Deliverables


Ignore:
Timestamp:
Nov 25, 2011, 7:43:39 PM (8 years ago)
Author:
tranquil
Message:
  • Immediates introduced (but not fully used yet in RTLabs to RTL pass)
  • translation streamlined
  • BUGGY: interpretation fails in LTL, trying to fetch a function with incorrect address
Location:
Deliverables/D2.2/8051/src
Files:
29 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml

    r1542 r1568  
    10071007            memory, we must increment by 5, as we added two new instructions. *)
    10081008        let to_ljmp = `REL (vect_of_int 2 `Eight) in
    1009         let offset = 5 in
     1009        (* let offset = 5 in *)
    10101010         let jmp_address, translated_jump =
    10111011           match i with
     
    14521452;;
    14531453
     1454let unopt = function Some x -> x | None -> invalid_arg "None"
     1455
    14541456let serial_port_input status in_cont =
    14551457      (* Serial port input *)
     
    14951497                           serial_v_in       = Some (`Eight b) }
    14961498                     else
    1497                            (* Warning about incomplete case analysis here, but safe as we've already tested for
    1498                               None. *)
    1499                        let Some e = status.serial_epsilon_in in
    1500                        let Some v = status.serial_v_in in
     1499                       (* safe as we've already tested for None. *)
     1500                       let e = unopt status.serial_epsilon_in in
     1501                       let v = unopt status.serial_v_in in
    15011502                       if status.clock >= e then
    15021503                         match v with
     
    15341535                           serial_v_in       = Some (`Nine (b, b')) }
    15351536                     else
    1536                            (* Warning about incomplete case analysis here, but safe as we've already tested for
    1537                               None. *)
    1538                        let Some e = status.serial_epsilon_in in
    1539                        let Some v = status.serial_v_in in
     1537                       (* safe as we've already tested for None. *)
     1538                       let e = unopt status.serial_epsilon_in in
     1539                       let v = unopt status.serial_v_in in
    15401540                       if status.clock >= e then
    15411541                         match v with
  • Deliverables/D2.2/8051/src/ASM/I8051.ml

    r1488 r1568  
    1111  | Cmpl
    1212  | Inc
     13  (* | Dec *)
     14  | Rl
    1315
    1416type op2 =
     
    2729  | Cmpl -> "cmpl"
    2830  | Inc -> "inc"
     31  | Rl -> "rotl"
    2932
    3033let print_op2 = function
     
    5760    | Cmpl -> Val.cmpl
    5861    | Inc -> Val.succ
     62    | Rl -> Val.rotl
    5963
    6064  let op2 carry op2 v1 v2 = match op2 with
  • Deliverables/D2.2/8051/src/ASM/I8051.mli

    r1488 r1568  
    99  | Cmpl
    1010  | Inc
     11  (* | Dec *)
     12  | Rl
    1113
    1214type op2 =
  • Deliverables/D2.2/8051/src/ERTL/ERTL.mli

    r1542 r1568  
    3838type registers = Register.t list
    3939
     40type argument = RTL.argument
     41
    4042type statement =
    4143
     
    6365     are the destination hardware register, the source pseudo register, and the
    6466     label of the next statement. *)
    65   | St_set_hdw of I8051.register * Register.t * Label.t
     67  | St_set_hdw of I8051.register * argument * Label.t
    6668
    6769  (* Assign the content of a hardware register to a hardware
     
    101103  | St_addrL of Register.t * AST.ident * Label.t
    102104
    103   (* Assign an integer constant to a register. Parameters are the destination
    104      register, the integer and the label of the next statement. *)
    105   | St_int of Register.t * int * Label.t
     105  (* (\* Assign an integer constant to a register. Parameters are the destination *)
     106  (*    register, the integer and the label of the next statement. *\) *)
     107  (* | St_int of Register.t * int * Label.t *)
    106108
    107109  (* Move the content of a register to another. Parameters are the destination
    108110     register, the source register, and the label of the next statement. *)
    109   | St_move of Register.t * Register.t * Label.t
     111  | St_move of Register.t * argument * Label.t
    110112
    111113  (* Apply a binary operation that will later be translated in an operation on
     
    127129  (* Apply a binary operation. Parameters are the operation, the destination
    128130     register, the source registers, and the label of the next statement. *)
    129   | St_op2 of I8051.op2 * Register.t * Register.t * Register.t * Label.t
     131  | St_op2 of I8051.op2 * Register.t * Register.t * argument * Label.t
    130132
    131133  (* Set the carry flag to zero. Parameter is the label of the next
  • Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml

    r1542 r1568  
    158158    else error ("Unknown local register " ^ (Register.print r) ^ ".")
    159159
     160let get_arg a st = match a with
     161  | RTL.Imm i -> Val.of_int i
     162  | RTL.Reg r -> get_reg (Psd r) st
     163
    160164let push st v =
    161165  let mem = Mem.store st.mem chunk st.isp v in
     
    282286
    283287    | ERTL.St_set_hdw (destr, srcr, lbl) ->
    284       let st = add_reg (Hdw destr) (get_reg (Psd srcr) st) st in
     288      let st = add_reg (Hdw destr) (get_arg srcr st) st in
    285289      next_pc st lbl
    286290
     
    328332      next_pc st lbl
    329333
    330     | ERTL.St_int (r, i, lbl) ->
     334    | ERTL.St_move (r, RTL.Imm i, lbl) ->
    331335      let st = add_reg (Psd r) (Val.of_int i) st in
    332336      next_pc st lbl
    333337
    334     | ERTL.St_move (destr, srcr, lbl) ->
     338    | ERTL.St_move (destr, RTL.Reg srcr, lbl) ->
    335339      let st = add_reg (Psd destr) (get_reg (Psd srcr) st) st in
    336340      next_pc st lbl
     
    361365        Eval.op2 st.carry op2
    362366          (get_reg (Psd srcr1) st)
    363           (get_reg (Psd srcr2) st) in
     367          (get_arg srcr2 st) in
    364368      let st = change_carry st carry in
    365369      let st = add_reg (Psd destr) v st in
  • Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml

    r1542 r1568  
    3737let print_result rl = print_reg_list "[" "]" " ; " Register.print rl
    3838
     39let print_arg = function
     40  | RTL.Imm i -> string_of_int i
     41  | RTL.Reg r -> Register.print r
    3942
    4043let print_statement = function
     
    5457  | ERTL.St_set_hdw (r1, r2, lbl) ->
    5558    Printf.sprintf "move %s, %s --> %s"
    56       (I8051.print_register r1) (Register.print r2) lbl
     59      (I8051.print_register r1) (print_arg r2) lbl
    5760  | ERTL.St_hdw_to_hdw (r1, r2, lbl) ->
    5861    Printf.sprintf "move %s, %s --> %s"
     
    7275  | ERTL.St_addrL (dstr, id, lbl) ->
    7376    Printf.sprintf "addrL %s, %s --> %s" (Register.print dstr) id lbl
    74   | ERTL.St_int (dstr, i, lbl) ->
    75     Printf.sprintf "imm %s, %d --> %s" (Register.print dstr) i lbl
     77  (* | ERTL.St_int (dstr, i, lbl) -> *)
     78  (*   Printf.sprintf "imm %s, %d --> %s" (Register.print dstr) i lbl *)
    7679  | ERTL.St_move (dstr, srcr, lbl) ->
    7780    Printf.sprintf "move %s, %s --> %s"
    78       (Register.print dstr) (Register.print srcr) lbl
     81      (Register.print dstr) (print_arg srcr) lbl
    7982  | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl) ->
    8083    Printf.sprintf "%sA %s, %s, %s --> %s"
     
    102105      (Register.print dstr)
    103106      (Register.print srcr1)
    104       (Register.print srcr2)
     107      (print_arg srcr2)
    105108      lbl
    106109  | ERTL.St_clear_carry lbl ->
  • Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml

    r1542 r1568  
    4040    let l = generate (LTL.St_load l) in
    4141    let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    42     let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in
     42    let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
    4343    let l = generate (LTL.St_int (I8051.a, 0, l)) in
    4444    let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    45     let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in
     45    let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in
    4646    LTL.St_int (I8051.a, off, l)
    4747
     48  let set_stack_preamble off l =
     49    let off = adjust off in
     50    let l = generate (LTL.St_from_acc (I8051.dph, l)) in
     51    let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
     52    let l = generate (LTL.St_int (I8051.a, 0, l)) in
     53    let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
     54    let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in
     55    LTL.St_int (I8051.a, off, l)
     56
    4857  let set_stack off r l =
    49     let off = adjust off in
    5058    let l = generate (LTL.St_store l) in
    5159    let l = generate (LTL.St_to_acc (r, l)) in
    52     let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    53     let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in
    54     let l = generate (LTL.St_int (I8051.a, 0, l)) in
    55     let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    56     let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in
    57     LTL.St_int (I8051.a, off, l)
    58 
    59 
    60   let write (r : Register.t) (l : Label.t) : (I8051.register * Label.t) =
    61     match lookup r with
    62 
    63       | Color hwr ->
    64         (* Pseudo-register [r] has been mapped to hardware register
    65            [hwr]. Just write into [hwr] and branch to [l]. *)
    66         (hwr, l)
    67 
    68       | Spill off ->
    69         (* Pseudo-register [r] has been mapped to offset [off] in the local zone
    70            of the stack. Then, write into [sst] (never allocated) and transfer
    71            control to an instruction that copies [sst] in the designated
    72            location of the stack before branching to [l]. *)
    73         (I8051.sst, generate (set_stack off I8051.sst l))
    74 
    75 
    76   let read (r : Register.t) (stmt : I8051.register -> LTL.statement) =
    77     match lookup r with
    78       | Color hwr ->
    79         (* Pseudo-register [r] has been mapped to hardware register [hwr]. Just
    80            generate statement [stmt] with a reference to register [hwr]. *)
    81         generate (stmt hwr)
    82 
    83       | Spill off ->
    84         (* Pseudo-register [r] has been mapped to offset [off] in the local zone
    85            of the stack. Issue a statement that copies the designated area in
    86            the stack into the temporary unallocatable hardware register [sst],
    87            then generate statement [stmt] with a reference to register
    88            [sst]. *)
    89         let temphwr = I8051.sst in
    90         let l = generate (stmt temphwr) in
    91         generate (get_stack temphwr off l)
     60    set_stack_preamble off l
     61
     62  let set_stack_int off k l =
     63    let l = generate (LTL.St_store l) in
     64    let l = generate (LTL.St_int (I8051.a, k, l)) in
     65    set_stack_preamble off l
     66
     67  (* let write (r : Register.t) (l : Label.t) : (I8051.register * Label.t) = *)
     68  (*   match lookup r with *)
     69
     70  (*     | Color hwr -> *)
     71  (*       (\* Pseudo-register [r] has been mapped to hardware register *)
     72  (*          [hwr]. Just write into [hwr] and branch to [l]. *\) *)
     73  (*       (hwr, l) *)
     74
     75  (*     | Spill off -> *)
     76  (*       (\* Pseudo-register [r] has been mapped to offset [off] in the local zone *)
     77  (*          of the stack. Then, write into [sst] (never allocated) and transfer *)
     78  (*          control to an instruction that copies [sst] in the designated *)
     79  (*          location of the stack before branching to [l]. *\) *)
     80  (*       (I8051.sst, generate (set_stack off I8051.sst l)) *)
     81
     82
     83  (* let read (r : Register.t) (stmt : I8051.register -> LTL.statement) = *)
     84  (*   match lookup r with *)
     85  (*     | Color hwr -> *)
     86  (*       (\* Pseudo-register [r] has been mapped to hardware register [hwr]. Just *)
     87  (*          generate statement [stmt] with a reference to register [hwr]. *\) *)
     88  (*       generate (stmt hwr) *)
     89
     90  (*     | Spill off -> *)
     91  (*       (\* Pseudo-register [r] has been mapped to offset [off] in the local zone *)
     92  (*          of the stack. Issue a statement that copies the designated area in *)
     93  (*          the stack into the temporary unallocatable hardware register [sst], *)
     94  (*          then generate statement [stmt] with a reference to register *)
     95  (*          [sst]. *\) *)
     96  (*       let temphwr = I8051.sst in *)
     97  (*       let l = generate (stmt temphwr) in *)
     98  (*       generate (get_stack temphwr off l) *)
    9299
    93100
     
    100107      | Color desthwr, Color sourcehwr when I8051.eq_reg desthwr sourcehwr ->
    101108        LTL.St_skip l
     109      | Color desthwr, Color sourcehwr when I8051.eq_reg desthwr I8051.a ->
     110        LTL.St_to_acc (sourcehwr, l)
     111      | Color desthwr, Color sourcehwr when I8051.eq_reg sourcehwr I8051.a ->
     112        LTL.St_from_acc (desthwr, l)
    102113      | Color desthwr, Color sourcehwr ->
    103114        let l = generate (LTL.St_from_acc (desthwr, l)) in
     
    119130        get_stack temphwr off2 l
    120131
     132  let move_int (dest : decision) (k : int) l =
     133    match dest with
     134      | Color desthwr -> LTL.St_int (desthwr, k, l)
     135      | Spill off -> set_stack_int off k l
     136
     137  let op2 op (dest : decision) (src1 : decision) (src2 : decision) l =
     138    let l = generate (move dest (Color I8051.a) l) in
     139    match op, src1, src2 with
     140      | _, _, Color src2hwr ->
     141        let l = generate (LTL.St_op2 (op, LTL.Reg src2hwr, l)) in
     142        move (Color I8051.a) src1 l
     143        (* if op is commutative, we can do as above if first is hwr *)
     144      | (Add | Addc | And | Or | Xor), Color src1hwr, _ ->
     145        let l = generate (LTL.St_op2 (op, LTL.Reg src1hwr, l)) in
     146        move (Color I8051.a) src2 l
     147        (* otherwise we have to use b *)
     148      | _ ->
     149        let l = generate (LTL.St_op2 (op, LTL.Reg I8051.b, l)) in
     150        let l = generate (move (Color I8051.a) src1 l) in
     151        move (Color I8051.b) src2 l
     152
     153  let move_to_dptr (addr1 : decision) (addr2 : decision) l =
     154    match addr1, addr2 with
     155      | Color _, _ ->
     156        (* the following does not change dph, as addr1 is hwr *)
     157        let l = generate (move (Color I8051.dpl) addr1 l) in
     158        move (Color I8051.dph) addr2 l
     159      | _, Color _ ->
     160        (* the following does not change dph, as addr1 is hwr *)
     161        let l = generate (move (Color I8051.dph) addr2 l) in
     162        move (Color I8051.dpl) addr1 l
     163      | _ ->
     164        let l = generate (move (Color I8051.dph) (Color I8051.b) l) in
     165        let l = generate (move (Color I8051.dpl) addr1 l) in
     166        move (Color I8051.b) addr2 l
     167
     168  let store addr1 addr2 srcr l =
     169    let l = generate (LTL.St_store l) in
     170    match srcr with
     171      | Color _ ->
     172        let l = generate (move (Color I8051.a) srcr l) in
     173        move_to_dptr addr1 addr2 l
     174      | _ ->
     175        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
     176        let l = generate (move_to_dptr addr1 addr2 l) in
     177        move (Color I8051.st0) srcr l
    121178
    122179  let newframe l =
     
    124181    else
    125182      let l = generate (LTL.St_from_acc (I8051.sph, l)) in
    126       let l = generate (LTL.St_op2 (I8051.Sub, I8051.dph, l)) in
    127       let l = generate (LTL.St_int (I8051.dph, 0, l)) in
     183      let l = generate (LTL.St_op2 (I8051.Sub, LTL.Imm 0, l)) in
    128184      let l = generate (LTL.St_to_acc (I8051.sph, l)) in
    129185      let l = generate (LTL.St_from_acc (I8051.spl, l)) in
    130       let l = generate (LTL.St_op2 (I8051.Sub, I8051.dpl, l)) in
     186      let l = generate (LTL.St_op2 (I8051.Sub, LTL.Imm stacksize, l)) in
    131187      let l = generate (LTL.St_clear_carry l) in
    132       let l = generate (LTL.St_int (I8051.dpl, stacksize, l)) in
    133188      LTL.St_to_acc (I8051.spl, l)
    134189
     
    137192    else
    138193      let l = generate (LTL.St_from_acc (I8051.sph, l)) in
    139       let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in
     194      let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
    140195      let l = generate (LTL.St_int (I8051.a, 0, l)) in
    141196      let l = generate (LTL.St_from_acc (I8051.spl, l)) in
    142       let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in
    143       LTL.St_int (I8051.a, stacksize, l)
     197      let l = generate (LTL.St_op2 (I8051.Add, LTL.Imm stacksize, l)) in
     198      LTL.St_to_acc (I8051.spl, l)
    144199
    145200
     
    174229        move (lookup destr) (Color sourcehwr) l
    175230
    176       | ERTL.St_set_hdw (desthwr, sourcer, l) ->
     231      | ERTL.St_set_hdw (desthwr, RTL.Reg sourcer, l) ->
    177232        move (Color desthwr) (lookup sourcer) l
    178233
     234      | ERTL.St_set_hdw (desthwr, RTL.Imm k, l) ->
     235        move_int (Color desthwr) k l
     236
    179237      | ERTL.St_hdw_to_hdw (r1, r2, l) ->
    180         let l = generate (LTL.St_from_acc (r1, l)) in
    181         LTL.St_to_acc (r2, l)
     238        move (Color r1) (Color r2) l
    182239
    183240      | ERTL.St_newframe l ->
     
    188245
    189246      | ERTL.St_framesize (r, l) ->
    190         let (hdw, l) = write r l in
    191         LTL.St_int (hdw, stacksize, l)
     247        move_int (lookup r) stacksize l
    192248
    193249      | ERTL.St_pop (r, l) ->
    194         let (hdw, l) = write r l in
    195         let l = generate (LTL.St_from_acc (hdw, l)) in
     250        let l = generate (move (lookup r) (Color I8051.a) l) in
    196251        LTL.St_pop l
    197252
    198253      | ERTL.St_push (r, l) ->
    199254        let l = generate (LTL.St_push l) in
    200         let l = read r (fun hdw -> LTL.St_to_acc (hdw, l)) in
    201         LTL.St_skip l
     255        move (Color I8051.a) (lookup r) l
    202256
    203257      | ERTL.St_addrH (r, x, l) ->
    204         let (hdw, l) = write r l in
    205         let l = generate (LTL.St_from_acc (hdw, l)) in
    206         let l = generate (LTL.St_to_acc (I8051.dph, l)) in
     258        let l = generate (move (lookup r) (Color I8051.dph) l) in
    207259        LTL.St_addr (x, l)
    208260
    209261      | ERTL.St_addrL (r, x, l) ->
    210         let (hdw, l) = write r l in
    211         let l = generate (LTL.St_from_acc (hdw, l)) in
    212         let l = generate (LTL.St_to_acc (I8051.dpl, l)) in
     262        let l = generate (move (lookup r) (Color I8051.dpl) l) in
    213263        LTL.St_addr (x, l)
    214264
    215       | ERTL.St_int (r, i, l) ->
    216         let (hdw, l) = write r l in
    217         LTL.St_int (hdw, i, l)
    218 
    219       | ERTL.St_move (r1, r2, l) ->
     265      | ERTL.St_move (r, RTL.Imm i, l) ->
     266        move_int (lookup r) i l
     267
     268      | ERTL.St_move (r1, RTL.Reg r2, l) ->
    220269        move (lookup r1) (lookup r2) l
    221270
    222271      | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) ->
    223         let (hdw, l) = write destr l in
    224         let l = generate (LTL.St_from_acc (hdw, l)) in
     272        let l = generate (move (lookup destr) (Color I8051.a) l) in
    225273        let l = generate (LTL.St_opaccs (opaccs, l)) in
    226         let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    227         let l = generate (LTL.St_from_acc (I8051.b, l)) in
    228         let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    229         LTL.St_skip l
     274        let l = generate (move (Color I8051.a) (lookup srcr1) l) in
     275        move (Color I8051.b) (lookup srcr2) l
    230276
    231277      | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) ->
    232         let (hdw, l) = write destr l in
    233         let l = generate (LTL.St_from_acc (hdw, l)) in
    234         let l = generate (LTL.St_to_acc (I8051.b, l)) in
     278        let l = generate (move (lookup destr) (Color I8051.b) l) in
    235279        let l = generate (LTL.St_opaccs (opaccs, l)) in
    236         let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    237         let l = generate (LTL.St_from_acc (I8051.b, l)) in
    238         let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    239         LTL.St_skip l
     280        let l = generate (move (Color I8051.a) (lookup srcr1) l) in
     281        move (Color I8051.b) (lookup srcr2) l
    240282
    241283      | ERTL.St_op1 (op1, destr, srcr, l) ->
    242         let (hdw, l) = write destr l in
    243         let l = generate (LTL.St_from_acc (hdw, l)) in
     284        let l = generate (move (lookup destr) (Color I8051.a) l) in
    244285        let l = generate (LTL.St_op1 (op1, l)) in
    245         let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
    246         LTL.St_skip l
    247 
    248       | ERTL.St_op2 (op2, destr, srcr1, srcr2, l) ->
    249         let (hdw, l) = write destr l in
    250         let l = generate (LTL.St_from_acc (hdw, l)) in
    251         let l = generate (LTL.St_op2 (op2, I8051.b, l)) in
    252         let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    253         let l = generate (LTL.St_from_acc (I8051.b, l)) in
    254         let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    255         LTL.St_skip l
     286        move (Color I8051.a) (lookup srcr) l
     287
     288      | ERTL.St_op2 (op, destr, srcr1, RTL.Reg srcr2, l) ->
     289        op2 op (lookup destr) (lookup srcr1) (lookup srcr2) l
     290
     291      | ERTL.St_op2 (op2, destr, srcr1, RTL.Imm k, l) ->
     292        let l = generate (move (lookup destr) (Color I8051.a) l) in
     293        let l = generate (LTL.St_op2 (op2, LTL.Imm k, l)) in
     294        move (Color I8051.a) (lookup srcr1) l
    256295
    257296      | ERTL.St_clear_carry l ->
     
    261300        LTL.St_set_carry l
    262301
     302      (* act differently on hardware registers? if at least one of
     303         the address bytes is hdw use of st0 can be avoided. And in
     304         case of non-hdw, the read could actually target a register
     305         directly *)
    263306      | ERTL.St_load (destr, addr1, addr2, l) ->
    264         let (hdw, l) = write destr l in
    265         let l = generate (LTL.St_from_acc (hdw, l)) in
    266         let l = generate (LTL.St_load l) in
    267         let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    268         let l = generate (LTL.St_to_acc (I8051.st0, l)) in
    269         let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    270         let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    271         let l = generate (LTL.St_from_acc (I8051.st0, l)) in
    272         let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    273         LTL.St_skip l
     307        let l = generate (move (lookup destr) (Color I8051.a) l) in
     308        let l = generate (LTL.St_load l) in
     309        move_to_dptr (lookup addr1) (lookup addr2) l
    274310
    275311      | ERTL.St_store (addr1, addr2, srcr, l) ->
    276         let l = generate (LTL.St_store l) in
    277         let l = generate (LTL.St_to_acc (I8051.st1, l)) in
    278         let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    279         let l = generate (LTL.St_to_acc (I8051.st0, l)) in
    280         let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    281         let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    282         let l = generate (LTL.St_from_acc (I8051.st0, l)) in
    283         let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    284         let l = generate (LTL.St_from_acc (I8051.st1, l)) in
    285         let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
    286         LTL.St_skip l
     312        store (lookup addr1) (lookup addr2) (lookup srcr) l
    287313
    288314      | ERTL.St_call_id (f, _, l) ->
     
    291317      | ERTL.St_call_ptr (f1, f2, _, l) ->
    292318        let l = generate (LTL.St_call_ptr l) in
    293         let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    294         let l = generate (LTL.St_to_acc (I8051.st0, l)) in
    295         let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    296         let l = read f1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    297         let l = generate (LTL.St_from_acc (I8051.st0, l)) in
    298         let l = read f2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    299         LTL.St_skip l
     319        move_to_dptr (lookup f1) (lookup f2) l
    300320
    301321      | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
    302322        let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
    303         let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
    304         LTL.St_skip l
     323        move (Color I8051.a) (lookup srcr) l
    305324
    306325      | ERTL.St_return _ ->
  • Deliverables/D2.2/8051/src/ERTL/build.ml

    r486 r1568  
    7070          let exceptions =
    7171            match stmt with
    72             | St_move (_, sourcer, _)
    73             | St_set_hdw (_, sourcer, _) ->
     72            | St_move (_, RTL.Reg sourcer, _)
     73            | St_set_hdw (_, RTL.Reg sourcer, _) ->
    7474                 Liveness.L.psingleton sourcer
    7575            | St_get_hdw (_, sourcehwr, _) ->
     
    103103          let graph =
    104104            match stmt with
    105             | St_move (r1, r2, _) ->
     105            | St_move (r1, RTL.Reg r2, _) ->
    106106                mkppp graph r1 r2
    107107            | St_get_hdw (r, hwr, _)
    108             | St_set_hdw (hwr, r, _) ->
     108            | St_set_hdw (hwr, RTL.Reg r, _) ->
    109109                mkpph graph r hwr
    110110            | _ ->
  • Deliverables/D2.2/8051/src/ERTL/liveness.ml

    r1542 r1568  
    3030  | St_addrH (_, _, l)
    3131  | St_addrL (_, _, l)
    32   | St_int (_, _, l)
     32  (* | St_int (_, _, l) *)
    3333  | St_move (_, _, l)
    3434  | St_opaccsA (_, _, _, _, l)
     
    112112  | St_framesize (r, _)
    113113  | St_pop (r, _)
    114   | St_int (r, _, _)
     114  (* | St_int (r, _, _) *)
    115115  | St_addrH (r, _, _)
    116116  | St_addrL (r, _, _)
     
    154154  | St_addrH _
    155155  | St_addrL _
    156   | St_int _
     156  (* | St_int _ *)
    157157  | St_clear_carry _
    158   | St_set_carry _ ->
     158  | St_set_carry _
     159  | St_set_hdw (_, RTL.Imm _, _)
     160  | St_move (_, RTL.Imm _, _) ->
    159161    L.bottom
    160162  | St_call_id (_, nparams, _) ->
     
    169171  | St_hdw_to_hdw (_, r, _) ->
    170172    L.hsingleton r
    171   | St_set_hdw (_, r, _)
     173  | St_op2 (I8051.Addc, _, r1, RTL.Reg r2, _) ->
     174    L.join (L.join (L.psingleton r1) (L.psingleton r2))
     175      (L.hsingleton I8051.carry)
     176  | St_op2 (I8051.Addc, _, r1, RTL.Imm _, _) ->
     177    L.join (L.psingleton r1) (L.hsingleton I8051.carry)
     178  | St_set_hdw (_, RTL.Reg r, _)
    172179  | St_push (r, _)
    173   | St_move (_, r, _)
     180  | St_move (_, RTL.Reg r, _)
    174181  | St_op1 (_, _, r, _)
     182  | St_op2 (_, _, r, RTL.Imm _, _)
    175183  | St_cond (r, _, _) ->
    176184    L.psingleton r
    177   | St_op2 (I8051.Addc, _, r1, r2, _) ->
    178     L.join (L.join (L.psingleton r1) (L.psingleton r2))
    179       (L.hsingleton I8051.carry)
    180185  | St_opaccsA (_, _, r1, r2, _)
    181186  | St_opaccsB (_, _, r1, r2, _)
    182   | St_op2 (_, _, r1, r2, _)
     187  | St_op2 (_, _, r1, RTL.Reg r2, _)
    183188  | St_load (_, r1, r2, _) ->
    184189    L.join (L.psingleton r1) (L.psingleton r2)
     
    187192  | St_newframe _
    188193  | St_delframe _ ->
    189     L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)   
     194    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
    190195  | St_return _ ->
    191196    Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved ret_regs
     
    224229  | St_get_hdw (r, _, l)
    225230  | St_framesize (r, l)
    226   | St_int (r, _, l)
     231  (* | St_int (r, _, l) *)
    227232  | St_addrH (r, _, l)
    228233  | St_addrL (r, _, l)
  • Deliverables/D2.2/8051/src/ERTL/uses.ml

    r1542 r1568  
    2323  | St_ind_inc _
    2424  | St_hdw_to_hdw _
     25  | St_set_hdw (_, RTL.Imm _, _)
    2526  | St_newframe _
    2627  | St_delframe _
     
    3132    uses
    3233  | St_get_hdw (r, _, _)
    33   | St_set_hdw (_, r, _)
     34  | St_set_hdw (_, RTL.Reg r, _)
    3435  | St_framesize (r, _)
    3536  | St_pop (r, _)
    3637  | St_push (r, _)
    37   | St_int (r, _, _)
     38  | St_move (r, RTL.Imm _, _)
    3839  | St_addrH (r, _, _)
    3940  | St_addrL (r, _, _)
    4041  | St_cond (r, _, _) ->
    4142    count r uses
    42   | St_move (r1, r2, _)
     43  | St_move (r1, RTL.Reg r2, _)
    4344  | St_op1 (_, r1, r2, _)
     45  | St_op2 (_, r1, r2, RTL.Imm _, _)
    4446  | St_call_ptr (r1, r2, _, _) ->
    4547    count r1 (count r2 uses)
    4648  | St_opaccsA (_, r1, r2, r3, _)
    4749  | St_opaccsB (_, r1, r2, r3, _)
    48   | St_op2 (_, r1, r2, r3, _)
     50  | St_op2 (_, r1, r2, RTL.Reg r3, _)
    4951  | St_load (r1, r2, r3, _)
    5052  | St_store (r1, r2, r3, _) ->
  • Deliverables/D2.2/8051/src/LIN/LIN.mli

    r1542 r1568  
    11
    22(** This module defines the abstract syntax tree of [LIN]. *)
     3
     4type argument = LTL.argument
    35
    46(** Compared to LTL where functions were graphs, the functions of a LIN program
     
    5557  (* Apply a binary operation on the A accumulator. Parameters are the
    5658     operation, and the other source register. *)
    57   | St_op2 of I8051.op2 * I8051.register
     59  | St_op2 of I8051.op2 * argument
    5860
    5961  (* Set the carry flag to zero. *)
  • Deliverables/D2.2/8051/src/LIN/LINInterpret.ml

    r1542 r1568  
    9696  else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
    9797
     98let get_arg a st = match a with
     99  | LTL.Imm i -> Val.of_int i
     100  | LTL.Reg r -> get_reg r st
     101
    98102let push st v =
    99103  let mem = Mem.store st.mem chunk st.isp v in
     
    262266
    263267    | LIN.St_op2 (op2, srcr) ->
    264       let (v, carry) =
    265         Eval.op2 st.carry op2
    266           (get_reg I8051.a st)
    267           (get_reg srcr st) in
     268      let (v, carry) = 
     269        Eval.op2 st.carry op2
     270          (get_reg I8051.a st)
     271          (get_arg srcr st) in
    268272      let st = change_carry st carry in
    269273      let st = add_reg I8051.a v st in
  • Deliverables/D2.2/8051/src/LIN/LINPrinter.ml

    r1542 r1568  
    1919let print_a = print_reg I8051.a
    2020
     21let print_arg = function
     22  | LTL.Imm i -> string_of_int i
     23  | LTL.Reg r -> print_reg r
    2124
    2225let print_statement = function
     
    5154  | LIN.St_op2 (op2, srcr) ->
    5255    Printf.sprintf "%s %s, %s"
    53       (I8051.print_op2 op2) print_a (print_reg srcr)
     56      (I8051.print_op2 op2) print_a (print_arg srcr)
    5457  | LIN.St_clear_carry -> "clear CARRY"
    5558  | LIN.St_set_carry -> "set CARRY"
  • Deliverables/D2.2/8051/src/LIN/LINToASM.ml

    r1542 r1568  
    5555let byte_of_int i = vect_of_int i `Eight
    5656let data_of_int i = `DATA (byte_of_int i)
     57let reg_or_data = function
     58  | LTL.Imm k -> data_of_int k
     59  | LTL.Reg r -> I8051.reg_addr r
    5760let data16_of_int i = `DATA16 (vect_of_int i `Sixteen)
    5861let acc_addr = I8051.reg_addr I8051.a
     
    9598  | LIN.St_op1 I8051.Inc ->
    9699    [`INC `A]
    97   | LIN.St_op2 (I8051.Add, r) ->
    98     [`ADD (`A, I8051.reg_addr r)]
    99   | LIN.St_op2 (I8051.Addc, r) ->
    100     [`ADDC (`A, I8051.reg_addr r)]
    101   | LIN.St_op2 (I8051.Sub, r) ->
    102     [`SUBB (`A, I8051.reg_addr r)]
     100  | LIN.St_op1 I8051.Rl ->
     101    [`RL `A]
     102  | LIN.St_op2 (I8051.Add, a) ->
     103    [`ADD (`A, reg_or_data a)]
     104  | LIN.St_op2 (I8051.Addc, a) ->
     105    [`ADDC (`A, reg_or_data a)]
     106  | LIN.St_op2 (I8051.Sub, a) ->
     107    [`SUBB (`A, reg_or_data a)]
    103108  | LIN.St_op2 (I8051.And, r) ->
    104     [`ANL (`U1 (`A, I8051.reg_addr r))]
     109    [`ANL (`U1 (`A, reg_or_data r))]
    105110  | LIN.St_op2 (I8051.Or, r) ->
    106     [`ORL (`U1 (`A, I8051.reg_addr r))]
     111    [`ORL (`U1 (`A, reg_or_data r))]
    107112  | LIN.St_op2 (I8051.Xor, r) ->
    108     [`XRL (`U1 (`A, I8051.reg_addr r))]
     113    [`XRL (`U1 (`A, reg_or_data r))]
    109114  | LIN.St_clear_carry ->
    110115    [`CLR `C]
  • Deliverables/D2.2/8051/src/LTL/LTL.mli

    r1542 r1568  
    77    algorithm. Actually, this coloring algorithm relies on the result of a
    88    liveness analysis that will also allow to remove dead code. *)
     9
     10type argument =
     11  | Reg of I8051.register
     12  | Imm of int
    913
    1014type statement =
     
    5862
    5963  (* Apply a binary operation on the A accumulator. Parameters are the
    60      operation, the other source register, and the label of the next
     64     operation, the other argument, and the label of the next
    6165     statement. *)
    62   | St_op2 of I8051.op2 * I8051.register * Label.t
     66  | St_op2 of I8051.op2 * argument * Label.t
    6367
    6468  (* Set the carry flag to zero. Parameter is the label of the next
  • Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

    r1542 r1568  
    123123  else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
    124124
     125let get_arg a st = match a with
     126  | LTL.Imm i -> Val.of_int i
     127  | LTL.Reg r -> get_reg r st
     128
    125129let push st v =
    126130  let mem = Mem.store st.mem chunk st.isp v in
     
    294298        Eval.op2 st.carry op2
    295299          (get_reg I8051.a st)
    296           (get_reg srcr st) in
     300          (get_arg srcr st) in
    297301      let st = change_carry st carry in
    298302      let st = add_reg I8051.a v st in
  • Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml

    r1542 r1568  
    1818
    1919let print_a = print_reg I8051.a
     20
     21let print_arg = function
     22  | LTL.Imm i -> string_of_int i
     23  | LTL.Reg r -> print_reg r
    2024
    2125
     
    5054  | LTL.St_op2 (op2, srcr, lbl) ->
    5155    Printf.sprintf "%s %s, %s --> %s"
    52       (I8051.print_op2 op2) print_a (print_reg srcr) lbl
     56      (I8051.print_op2 op2) print_a (print_arg srcr) lbl
    5357  | LTL.St_clear_carry lbl ->
    5458    Printf.sprintf "clear CARRY --> %s" lbl
  • Deliverables/D2.2/8051/src/RTL/RTL.mli

    r1542 r1568  
    99type registers = Register.t list
    1010
     11(* arguments to certain operations: either registers or immediate args *)
     12type argument =
     13  | Reg of Register.t
     14  | Imm of int
     15
    1116type statement =
    1217
     
    1722  | St_cost of CostLabel.t * Label.t
    1823
    19   (* Reset to 0 a loop index *) 
     24  (* Reset to 0 a loop index *)
    2025  | St_ind_0 of CostLabel.index * Label.t
    2126
     
    3237  | St_stackaddr of Register.t * Register.t * Label.t
    3338
    34   (* Assign an integer constant to a register. Parameters are the destination
    35      register, the integer and the label of the next statement. *)
    36   | St_int of Register.t * int * Label.t
     39  (* (\* Assign an integer constant to a register. Parameters are the destination *)
     40  (*    register, the integer and the label of the next statement. *\) *)
     41  (* | St_int of Register.t * int * Label.t *)
    3742
    3843  (* Move the content of a register to another. Parameters are the destination
    39      register, the source register, and the label of the next statement. *)
    40   | St_move of Register.t * Register.t * Label.t
     44     register, the source argument, and the label of the next statement. *)
     45  | St_move of Register.t * argument * Label.t
    4146
    4247  (* Apply a binary operation that will later be translated in an operation on
     
    5257
    5358  (* Apply a binary operation. Parameters are the operation, the destination
    54      register, the source registers, and the label of the next statement. *)
    55   | St_op2 of I8051.op2 * Register.t * Register.t * Register.t * Label.t
     59     register, the source arguments, and the label of the next statement. *)
     60  | St_op2 of I8051.op2 * Register.t * Register.t * argument * Label.t
    5661
    5762  (* Set the carry flag to zero. Parameter is the label of the next
  • Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml

    r1542 r1568  
    8989  if Register.Map.mem r lenv then Register.Map.find r lenv
    9090  else error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
     91
     92let get_local_arg_value (lenv : local_env) : RTL.argument -> Val.t = function
     93  | RTL.Reg r -> get_local_value lenv r
     94  | RTL.Imm i -> Val.of_int i
     95
    9196let get_arg_values lenv args = List.map (get_local_value lenv) args
    9297
     
    159164        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] sp
    160165
    161       | RTL.St_int (r, i, lbl) ->
    162         assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i]
     166      (* | RTL.St_int (r, i, lbl) -> *)
     167      (*   assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i] *)
    163168
    164169      | RTL.St_move (destr, srcr, lbl) ->
    165170        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr]
    166           [get_local_value lenv srcr]
     171          [get_local_arg_value lenv srcr]
    167172
    168173      | RTL.St_opaccs (opaccs, destr1, destr2, srcr1, srcr2, lbl) ->
     
    182187          Eval.op2 carry op2
    183188            (get_local_value lenv srcr1)
    184             (get_local_value lenv srcr2) in
     189            (get_local_arg_value lenv srcr2) in
    185190        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
    186191
  • Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml

    r1542 r1568  
    1616
    1717let print_reg = Register.print
     18
     19let print_arg = function
     20  | RTL.Reg r -> print_reg r
     21  | RTL.Imm i -> string_of_int i
    1822
    1923let reg_set_to_list rs =
     
    4448  | RTL.St_cost (cost_lbl, lbl) ->
    4549    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    46     Printf.sprintf "emit %s --> %s" cost_lbl lbl
     50    Printf.sprintf "_emit %s --> %s" cost_lbl lbl
    4751  | RTL.St_ind_0 (i, lbl) ->
    48     Printf.sprintf "index %d --> %s" i lbl
     52    Printf.sprintf "_index %d --> %s" i lbl
    4953  | RTL.St_ind_inc (i, lbl) ->
    50     Printf.sprintf "increment %d --> %s" i lbl
     54    Printf.sprintf "_increment %d --> %s" i lbl
    5155  | RTL.St_addr (dstr1, dstr2, id, lbl) ->
    52     Printf.sprintf "imm (%s, %s), %s --> %s"
     56    Printf.sprintf "move (%s, %s), %s --> %s"
    5357      (print_reg dstr1) (print_reg dstr2) id lbl
    5458  | RTL.St_stackaddr (dstr1, dstr2, lbl) ->
    55     Printf.sprintf "imm (%s, %s), STACK --> %s"
     59    Printf.sprintf "move (%s, %s), STACK --> %s"
    5660      (print_reg dstr1) (print_reg dstr2) lbl
    57   | RTL.St_int (dstr, i, lbl) ->
    58     Printf.sprintf "imm %s, %d --> %s" (print_reg dstr) i lbl
     61  (* | RTL.St_int (dstr, i, lbl) -> *)
     62  (*   Printf.sprintf "imm %s, %d --> %s" (print_reg dstr) i lbl *)
    5963  | RTL.St_move (dstr, srcr, lbl) ->
    6064    Printf.sprintf "move %s, %s --> %s"
    61       (print_reg dstr) (print_reg srcr) lbl
     65      (print_reg dstr) (print_arg srcr) lbl
    6266  | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl) ->
    6367    Printf.sprintf "%s (%s, %s) %s, %s --> %s"
     
    7680      (print_reg dstr)
    7781      (print_reg srcr1)
    78       (print_reg srcr2)
     82      (print_arg srcr2)
    7983      lbl
    8084  | RTL.St_clear_carry lbl ->
  • Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

    r1542 r1568  
    3434  | ERTL.St_addrH (r, id, _) -> ERTL.St_addrH (r, id, lbl)
    3535  | ERTL.St_addrL (r, id, _) -> ERTL.St_addrL (r, id, lbl)
    36   | ERTL.St_int (r, i, _) -> ERTL.St_int (r, i, lbl)
    37   | ERTL.St_move (r1, r2, _) -> ERTL.St_move (r1, r2, lbl)
     36  | ERTL.St_move (r1, a, _) -> ERTL.St_move (r1, a, lbl)
    3837  | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, _) ->
    3938    ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl)
     
    102101let restore_hdws l =
    103102  let f (destr, srcr) start_lbl =
    104     adds_graph [ERTL.St_set_hdw (destr, srcr, start_lbl)] start_lbl in
     103    adds_graph [ERTL.St_set_hdw (destr, RTL.Reg srcr, start_lbl)] start_lbl in
    105104  List.map f (List.map (fun (x, y) -> (y, x)) l)
    106105
     
    118117  adds_graph
    119118    [ERTL.St_framesize (addr1, start_lbl) ;
    120      ERTL.St_int (tmpr, off+I8051.int_size, start_lbl) ;
    121      ERTL.St_op2 (I8051.Sub, addr1, addr1, tmpr, start_lbl) ;
     119     ERTL.St_op2 (I8051.Sub, addr1, addr1, RTL.Imm (off+I8051.int_size),
     120                 start_lbl) ;
    122121     ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
    123      ERTL.St_op2 (I8051.Add, addr1, addr1, tmpr, start_lbl) ;
    124      ERTL.St_int (addr2, 0, start_lbl) ;
     122     ERTL.St_op2 (I8051.Add, addr1, addr1, RTL.Reg tmpr, start_lbl) ;
    125123     ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
    126      ERTL.St_op2 (I8051.Addc, addr2, addr2, tmpr, start_lbl) ;
     124     ERTL.St_op2 (I8051.Addc, addr2, tmpr, RTL.Imm 0, start_lbl) ;
    127125     ERTL.St_load (destr, addr1, addr2, start_lbl)]
    128126    start_lbl dest_lbl def
     
    176174
    177175let save_return ret_regs start_lbl dest_lbl def =
    178   let (def, tmpr) = fresh_reg def in
    179176  let ((common1, rest1), (common2, _)) =
    180177    MiscPottier.reduce I8051.sts ret_regs in
    181   let init_tmpr = ERTL.St_int (tmpr, 0, start_lbl) in
    182   let f_save st r = ERTL.St_set_hdw (st, r, start_lbl) in
     178  let f_save st r = ERTL.St_set_hdw (st, RTL.Reg r, start_lbl) in
    183179  let saves = List.map2 f_save common1 common2 in
    184   let f_default st = ERTL.St_set_hdw (st, tmpr, start_lbl) in
     180  let f_default st = ERTL.St_set_hdw (st, RTL.Imm 0, start_lbl) in
    185181  let defaults = List.map f_default rest1 in
    186   adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
     182  adds_graph (saves @ defaults) start_lbl dest_lbl def
    187183
    188184let assign_result start_lbl =
     
    252248  let (def, tmpr) = fresh_reg def in
    253249  adds_graph
    254     [ERTL.St_int (addr1, off+I8051.int_size, start_lbl) ;
    255      ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
     250    [ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
    256251     ERTL.St_clear_carry start_lbl ;
    257      ERTL.St_op2 (I8051.Sub, addr1, tmpr, addr1, start_lbl) ;
     252     ERTL.St_op2 (I8051.Sub, addr1, tmpr, RTL.Imm (off+I8051.int_size),
     253                  start_lbl) ;
    258254     ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
    259      ERTL.St_int (addr2, 0, start_lbl) ;
    260      ERTL.St_op2 (I8051.Sub, addr2, tmpr, addr2, start_lbl) ;
     255     ERTL.St_op2 (I8051.Sub, addr2, tmpr, RTL.Imm 0, start_lbl) ;
    261256     ERTL.St_store (addr1, addr2, srcr, start_lbl)]
    262257    start_lbl dest_lbl def
     
    338333      lbl lbl' def
    339334
    340   | RTL.St_int (r, i, lbl') ->
    341     add_graph lbl (ERTL.St_int (r, i, lbl')) def
     335  (* | RTL.St_int (r, i, lbl') -> *)
     336  (*   add_graph lbl (ERTL.St_int (r, i, lbl')) def *)
    342337
    343338  | RTL.St_move (r1, r2, lbl') ->
     
    444439    | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl)
    445440    | ERTL.St_pop (_, lbl) | ERTL.St_push (_, lbl) | ERTL.St_addrH (_, _, lbl)
    446     | ERTL.St_addrL (_, _, lbl) | ERTL.St_int (_, _, lbl)
     441    | ERTL.St_addrL (_, _, lbl) (* | ERTL.St_int (_, _, lbl) *)
    447442    | ERTL.St_move (_, _, lbl) | ERTL.St_opaccsA (_, _, _, _, lbl)
    448443    | ERTL.St_opaccsB (_, _, _, _, lbl)
  • Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli

    r1542 r1568  
    1111
    1212
     13(* arguments to certain operations: either registers or immediate args *)
    1314type argument =
    1415  | Reg of Register.t
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml

    r1542 r1568  
    168168        lbl
    169169  | RTLabs.St_load (q, addr, destr, lbl) ->
    170       Printf.sprintf "%s := *(%s) %s --> %s"
     170      Printf.sprintf "%s := (%s) *%s --> %s"
    171171        (print_reg destr)
    172172        (Memory.string_of_quantity q)
     
    174174        lbl
    175175  | RTLabs.St_store (q, addr, srcr, lbl) ->
    176       Printf.sprintf "*(%s)%s := %s --> %s"
     176      Printf.sprintf "*%s := (%s)%s --> %s"
     177        (print_arg addr)
    177178        (Memory.string_of_quantity q)
    178         (print_arg addr)
    179179        (print_arg srcr)
    180180        lbl
     
    216216        (Primitive.print_sig sg)
    217217  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
    218       Printf.sprintf "%s? --> %s, %s"
     218      Printf.sprintf "if %s --> %s else --> %s"
    219219        (print_reg r)
    220220        lbl_true
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

    r1542 r1568  
    9797  | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl)
    9898  | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl)
    99   | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl)
     99  (* | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl) *)
    100100  | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl)
    101101  | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, _) ->
     
    204204    let module M = IntValue.Make (struct let size = size end) in
    205205    let is = List.map M.to_int (M.break (M.of_int i) size) in
    206     let f r i = RTL.St_int (r, i, dest_lbl) in
     206    let f r i = RTL.St_move (r, RTL.Imm i, dest_lbl) in
    207207    let l = List.map2 f destrs is in
    208208    adds_graph l start_lbl dest_lbl def
     
    229229let rec translate_move destrs srcrs start_lbl =
    230230  let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
    231   let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
     231  let f_common destr srcr = RTL.St_move (destr, RTL.Reg srcr, start_lbl) in
    232232  let translates1 = adds_graph (List.map2 f_common common1 common2) in
    233233  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
    234234  add_translates [translates1 ; translates2] start_lbl
    235235
     236let rec translate_imm destrs vals start_lbl =
     237  let ((common1, rest1), (common2, _)) = MiscPottier.reduce destrs vals in
     238  let f_common destr srcr = RTL.St_move (destr, RTL.Imm srcr, start_lbl) in
     239  let translates1 = adds_graph (List.map2 f_common common1 common2) in
     240  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
     241  add_translates [translates1 ; translates2] start_lbl
     242
    236243
    237244let translate_cast_unsigned destrs start_lbl dest_lbl def =
    238   let (def, tmp_zero) = fresh_reg def in
    239   let zeros = MiscPottier.make tmp_zero (List.length destrs) in
    240   add_translates
    241     [adds_graph [RTL.St_int (tmp_zero, 0, start_lbl)] ;
    242      translate_move destrs zeros]
    243     start_lbl dest_lbl def
     245  translate_cst (AST.Cst_int 0) destrs start_lbl dest_lbl def
    244246
    245247let translate_cast_signed destrs srcr start_lbl dest_lbl def =
    246   let (def, tmp_128) = fresh_reg def in
    247   let (def, tmp_255) = fresh_reg def in
    248248  let (def, tmpr) = fresh_reg def in
    249   let (def, dummy) = fresh_reg def in
    250249  let insts =
    251     [RTL.St_int (tmp_128, 128, start_lbl) ;
    252      RTL.St_op2 (I8051.And, tmpr, tmp_128, srcr, start_lbl) ;
    253      RTL.St_opaccs (I8051.DivuModu, tmpr, dummy, tmpr, tmp_128, start_lbl) ;
    254      RTL.St_int (tmp_255, 255, start_lbl) ;
    255      RTL.St_opaccs (I8051.Mul, tmpr, dummy, tmpr, tmp_255, start_lbl)] in
     250    (* this sets tmpr to 0xFF if s is neg, 0x00 o.w. Done like that:
     251       byte in tmpr if srcr is: neg   |  pos
     252       tmpr ← srcr | 127       11...1 | 01...1
     253       tmpr ← tmpr <rot< 1     1...11 | 1...10
     254       tmpr ← INC tmpr         0....0 | 1....1
     255       tmpr ← CPL tmpr         1....1 | 0....0
     256
     257     *)
     258    [RTL.St_op2 (I8051.Or, tmpr, srcr, RTL.Imm 127, start_lbl) ;
     259     RTL.St_op1 (I8051.Rl, tmpr, tmpr, start_lbl) ;
     260     RTL.St_op1 (I8051.Inc, tmpr, tmpr, start_lbl) ;
     261     RTL.St_op1 (I8051.Cmpl, tmpr, tmpr, start_lbl) ] in
    256262  let srcrs = MiscPottier.make tmpr (List.length destrs) in
    257263  add_translates [adds_graph insts ; translate_move destrs srcrs]
     
    273279
    274280let translate_negint destrs srcrs start_lbl dest_lbl def =
    275   assert (List.length destrs = List.length srcrs) ;
    276   let (def, tmpr) = fresh_reg def in
     281  assert (List.length destrs = List.length srcrs && List.length destrs > 0) ;
    277282  let f_cmpl destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
    278283  let insts_cmpl = List.map2 f_cmpl destrs srcrs in
    279   let insts_init =
    280     [RTL.St_set_carry start_lbl ;
    281      RTL.St_int (tmpr, 0, start_lbl)] in
    282   let f_add destr = RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl) in
    283   let insts_add = List.map f_add destrs in
    284   adds_graph (insts_cmpl @ insts_init @ insts_add)
     284  let first, rest = List.hd destrs, List.tl destrs in
     285  let inst_init =
     286    RTL.St_op2 (I8051.Add, first, first, RTL.Imm 0, start_lbl) in
     287  let f_add destr =
     288    RTL.St_op2 (I8051.Addc, destr, destr, RTL.Imm 0, start_lbl) in
     289  let insts_add = List.map f_add rest in
     290  adds_graph (insts_cmpl @ inst_init :: insts_add)
    285291    start_lbl dest_lbl def
    286292
    287293
    288 let translate_notbool destrs srcrs start_lbl dest_lbl def = match destrs with
    289   | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
    290   | destr :: destrs ->
    291     let (def, tmpr) = fresh_reg def in
    292     let (def, tmp_srcrs) = fresh_regs def (List.length srcrs) in
    293     let save_srcrs = translate_move tmp_srcrs srcrs in
    294     let init_destr = RTL.St_int (destr, 1, start_lbl) in
    295     let f tmp_srcr =
    296       [RTL.St_clear_carry start_lbl ;
    297        RTL.St_int (tmpr, 0, start_lbl) ;
    298        RTL.St_op2 (I8051.Sub, tmpr, tmpr, tmp_srcr, start_lbl) ;
    299        RTL.St_int (tmpr, 0, start_lbl) ;
    300        RTL.St_op2 (I8051.Addc, tmpr, tmpr, tmpr, start_lbl) ;
    301        RTL.St_op2 (I8051.Xor, destr, destr, tmpr, start_lbl)] in
    302     let insts = init_destr :: (List.flatten (List.map f tmp_srcrs)) in
    303     let epilogue = translate_cst (AST.Cst_int 0) destrs in
    304     add_translates [save_srcrs ; adds_graph insts ; epilogue]
    305       start_lbl dest_lbl def
     294let translate_notbool destrs srcrs start_lbl dest_lbl def =
     295  match destrs,srcrs with
     296    | [], _ -> adds_graph [] start_lbl dest_lbl def
     297    | destr :: destrs, srcr :: srcrs ->
     298      let (def, tmpr) = fresh_reg def in
     299      let init_destr = RTL.St_move (destr, RTL.Reg srcr, start_lbl) in
     300      let f r =
     301        RTL.St_op2 (I8051.Or, destr, destr, RTL.Reg r, start_lbl) in
     302      let big_or = List.map f srcrs in
     303      let finalize_destr =
     304        [RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
     305         RTL.St_clear_carry start_lbl ;
     306         RTL.St_op2 (I8051.Sub, tmpr, tmpr, RTL.Reg destr, start_lbl) ;
     307         (* carry bit is set iff destr is non-zero iff destrs was non-zero *)
     308         RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
     309         RTL.St_op2 (I8051.Addc, destr, tmpr, RTL.Reg tmpr, start_lbl) ;
     310         (* destr = carry bit = bigor of old destrs *)
     311         RTL.St_op2 (I8051.Xor, destr, destr, RTL.Imm 1, start_lbl)] in
     312      let epilogue = translate_cst (AST.Cst_int 0) destrs in
     313      add_translates [adds_graph (init_destr :: big_or @ finalize_destr) ;
     314                      epilogue]
     315        start_lbl dest_lbl def
     316    | destr :: destrs, [] ->
     317      translate_cst (AST.Cst_int 1) destrs start_lbl dest_lbl def
    306318
    307319
     
    336348    MiscPottier.reduce destrs_rest srcrs_rest in
    337349  let (def, tmpr) = fresh_reg def in
    338   let insts_init =
    339     [RTL.St_clear_carry start_lbl ;
    340      RTL.St_int (tmpr, 0, start_lbl)] in
     350  let carry_init = match op with
     351    | I8051.Addc | I8051.Sub ->
     352      (* depend on carry bit *)
     353      [RTL.St_clear_carry start_lbl]
     354    | I8051.Add -> assert false (* should not call with add, not correct *)
     355    | _ -> [] in
     356  let inst_init = RTL.St_move (tmpr, RTL.Imm 0, start_lbl) :: carry_init in
    341357  let f_add destr srcr1 srcr2 =
    342     RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
     358    RTL.St_op2 (op, destr, srcr1, RTL.Reg srcr2, start_lbl) in
    343359  let insts_add =
    344360    MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in
    345361  let f_add_cted destr srcr =
    346     RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in
     362    RTL.St_op2 (op, destr, srcr, RTL.Reg tmpr, start_lbl) in
    347363  let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
    348364  let f_rest destr =
    349     RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in
     365    RTL.St_op2 (op, destr, tmpr, RTL.Reg tmpr, start_lbl) in
    350366  let insts_rest = List.map f_rest destrs_rest in
    351   adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest)
     367  adds_graph (inst_init @ insts_add @ insts_add_cted @ insts_rest)
    352368    start_lbl dest_lbl def
    353369
     
    357373    | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl
    358374    | [destr], [] ->
    359       adds_graph [RTL.St_int (tmpr, 0, start_lbl) ;
    360                   RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]
     375      adds_graph [RTL.St_op2 (I8051.Addc, destr, destr, RTL.Imm 0, start_lbl)]
    361376        start_lbl
    362377    | destr1 :: destr2 :: destrs, [] ->
    363378      add_translates
    364         [adds_graph [RTL.St_int (tmpr, 0, start_lbl) ;
    365                      RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl) ;
    366                      RTL.St_op2 (I8051.Addc, destr2, tmpr, tmpr, start_lbl)] ;
     379        [adds_graph
     380            [RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
     381             RTL.St_op2 (I8051.Addc, destr1, destr1, RTL.Imm 0, start_lbl) ;
     382             RTL.St_op2 (I8051.Addc, destr2, tmpr, RTL.Imm 0, start_lbl)] ;
    367383         translate_cst (AST.Cst_int 0) destrs]
    368384        start_lbl
     
    370386      adds_graph
    371387        [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ;
    372          RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]
     388         RTL.St_op2 (I8051.Addc, destr, destr, RTL.Reg tmpr, start_lbl)]
    373389        start_lbl
    374390    | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 ->
     
    377393            [RTL.St_opaccs
    378394                (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ;
    379              RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl)] ;
     395             RTL.St_op2 (I8051.Addc, destr1, destr1, RTL.Reg tmpr, start_lbl)] ;
    380396         translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2]
    381397        start_lbl
     
    389405      | tmp_destr2 :: tmp_destrs2 ->
    390406        [adds_graph [RTL.St_clear_carry dummy_lbl ;
    391                      RTL.St_int (tmp_destr2, 0, dummy_lbl)] ;
     407                     RTL.St_move (tmp_destr2, RTL.Imm 0, dummy_lbl)] ;
    392408         translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
    393409         translate_cst (AST.Cst_int 0) tmp_destrs1 ;
    394          adds_graph [RTL.St_clear_carry dummy_lbl] ;
    395410         translate_op I8051.Addc destrs destrs tmp_destrs])
    396411
     
    422437      add_translates [inst_div ; insts_rest] start_lbl dest_lbl def
    423438
    424 
    425439let translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def =
    426440  match destrs with
    427     | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
     441    | [] -> adds_graph [] start_lbl dest_lbl def
    428442    | destr :: destrs ->
    429443      let (def, tmpr) = fresh_reg def in
    430       let (def, tmp_zero) = fresh_reg def in
    431       let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in
    432       let save_srcrs1 = translate_move tmp_srcrs1 srcrs1 in
    433       let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in
    434       let save_srcrs2 = translate_move tmp_srcrs2 srcrs2 in
    435444      let ((common1, rest1), (common2, rest2)) =
    436         MiscPottier.reduce tmp_srcrs1 tmp_srcrs2 in
     445        MiscPottier.reduce srcrs1 srcrs2 in
    437446      let rest = choose_rest rest1 rest2 in
    438       let inits =
    439         [RTL.St_int (destr, 0, start_lbl) ;
    440          RTL.St_int (tmp_zero, 0, start_lbl)] in
    441       let f_common tmp_srcr1 tmp_srcr2 =
    442         [RTL.St_clear_carry start_lbl ;
    443          RTL.St_op2 (I8051.Sub, tmpr, tmp_srcr1, tmp_srcr2, start_lbl) ;
    444          RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in
    445       let insts_common = List.flatten (List.map2 f_common common1 common2) in
     447      let firsts = match common1, common2 with
     448        | c1hd :: c1tl, c2hd :: c2tl ->
     449          let init =
     450            RTL.St_op2 (I8051.Xor, destr, c1hd, RTL.Reg c2hd, start_lbl) in
     451          let f_common tmp_srcr1 tmp_srcr2 =
     452            [RTL.St_op2 (I8051.Xor, tmpr, tmp_srcr1,
     453                         RTL.Reg tmp_srcr2, start_lbl) ;
     454             RTL.St_op2 (I8051.Or, destr, destr, RTL.Reg tmpr, start_lbl)] in
     455          let insts_common = List.flatten (List.map2 f_common c1tl c2tl) in
     456          init :: insts_common
     457        | [], [] ->
     458          [RTL.St_move (destr, RTL.Imm 0, start_lbl)]
     459        (* common1 and common2 have the same length *)
     460        | _ -> assert false in
    446461      let f_rest tmp_srcr =
    447         [RTL.St_clear_carry start_lbl ;
    448          RTL.St_op2 (I8051.Sub, tmpr, tmp_zero, tmp_srcr, start_lbl) ;
    449          RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in
    450       let insts_rest = List.flatten (List.map f_rest rest) in
    451       let insts = inits @ insts_common @ insts_rest in
     462        RTL.St_op2 (I8051.Xor, destr, destr, RTL.Reg tmp_srcr, start_lbl) in
     463      let insts_rest = List.map f_rest rest in
     464      let insts = firsts @ insts_rest in
    452465      let epilogue = translate_cst (AST.Cst_int 0) destrs in
    453       add_translates [save_srcrs1 ; save_srcrs2 ; adds_graph insts ; epilogue]
    454         start_lbl dest_lbl def
    455 
    456 
    457 let translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl
    458     (srcr1, srcr2) =
    459   [RTL.St_clear_carry dummy_lbl ;
    460    RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ;
    461    RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ;
    462    RTL.St_op2 (I8051.Sub, tmpr2, srcr2, srcr1, dummy_lbl) ;
    463    RTL.St_op2 (I8051.Addc, tmpr2, tmp_zero, tmp_zero, dummy_lbl) ;
    464    RTL.St_op2 (I8051.Or, tmpr1, tmpr1, tmpr2, dummy_lbl) ;
    465    RTL.St_op2 (I8051.Xor, tmpr1, tmpr1, tmp_one, dummy_lbl) ;
    466    RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)]
    467 
    468 let translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 destr leq dummy_lbl =
    469   let f = translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
    470   (RTL.St_int (destr, 1, dummy_lbl)) :: (List.flatten (List.map f leq))
    471 
    472 let translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq
    473     srcr1 srcr2 =
    474   (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @
    475   [RTL.St_clear_carry dummy_lbl ;
    476    RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ;
    477    RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ;
    478    RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ;
    479    RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)]
    480 
    481 let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl
    482     srcrs1 srcrs2 =
    483   let f (insts, leq) srcr1 srcr2 =
    484     let added_insts =
    485       translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq
    486         srcr1 srcr2 in
    487     (insts @ added_insts, leq @ [(srcr1, srcr2)]) in
    488   fst (List.fold_left2 f ([], []) srcrs1 srcrs2)
    489 
    490 let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     466      add_translates [ adds_graph insts ; epilogue] start_lbl dest_lbl def
     467
     468(* this requires destrs to be either 0 or 1 to be truly correct
     469   to be used after translations that ensure this *)
     470let translate_toggle_bool destrs start_lbl =
    491471  match destrs with
    492     | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
    493     | _ ->
    494       let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
    495       let tmp_destr = List.hd tmp_destrs in
    496       let (def, tmp_zero) = fresh_reg def in
    497       let (def, tmp_one) = fresh_reg def in
    498       let (def, tmpr1) = fresh_reg def in
    499       let (def, tmpr2) = fresh_reg def in
    500       let (def, tmpr3) = fresh_reg def in
    501       let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in
    502       let srcrs1 = List.rev srcrs1 in
    503       let srcrs2 = List.rev srcrs2 in
    504       let insts_init =
    505         [translate_cst (AST.Cst_int 0) tmp_destrs ;
    506          translate_cst (AST.Cst_int 0) added ;
    507          adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ;
    508                      RTL.St_int (tmp_one, 1, start_lbl)]] in
    509       let insts_main =
    510         translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl
    511           srcrs1 srcrs2 in
    512       let insts_main = [adds_graph insts_main] in
    513       let insts_exit = [translate_move destrs tmp_destrs] in
    514       add_translates (insts_init @ insts_main @ insts_exit )
    515         start_lbl dest_lbl def
    516 
    517 
    518 let add_128_to_last tmp_128 rs start_lbl = match rs with
    519   | [] -> adds_graph [] start_lbl
    520   | _ ->
    521     let r = MiscPottier.last rs in
    522     adds_graph [RTL.St_op2 (I8051.Add, r, r, tmp_128, start_lbl)] start_lbl
    523 
     472    | [] -> adds_graph [] start_lbl
     473    | destr :: _ ->
     474      adds_graph [RTL.St_op1 (I8051.Cmpl, destr, destr, start_lbl)] start_lbl
     475
     476
     477
     478(* let translate_eq_reg tmp_zero tmpr destr dummy_lbl *)
     479(*     (srcr1, srcr2) = *)
     480(*   [RTL.St_op2 (I8051.Xor, tmpr, srcr1, srcr2, dummy_lbl) ; *)
     481(*    (\* now tmpr = 0 iff srcr1 = srcr2 *\) *)
     482(*    RTL.St_clear_carry dummy_lbl ; *)
     483(*    RTL.St_op2 (I8051.Sub, tmpr, tmp_zero, tmpr, dummy_lbl) ; *)
     484(*    (\* now carry bit = (old tmpr is not zero) = (srcr1 != srcr2) *\) *)
     485(*    RTL.St_op2 (I8051.Addc, tmpr, tmp_zero, tmp_zero, dummy_lbl) ; *)
     486(*    (\* now tmpr = old carry bit = (srcr1 != srcr2) *\) *)
     487(*    RTL.St_op1 (I8051.Cpl, tmpr, tmpr, dummy_lbl)] *)
     488
     489(* let translate_eq_list tmp_zero tmpr destr leq dummy_lbl = match leq with *)
     490(*   | leqhd :: leqtl -> *)
     491(*     let init = translate_eq_reg tmp_zero destr dummy_lbl leqhd in *)
     492(*     let f p = translate_eq_reg tmp_zero tmpr destr dummy_lbl p @ *)
     493(*       [RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)] in *)
     494(*     init @ List.flatten (List.map f leqtl) *)
     495(*   | _ -> [RTL.St_move (destr, RTL.Imm 1, dummy_lbl)] *)
     496
     497(* let translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq *)
     498(*     srcr1 srcr2 = *)
     499(*   (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @ *)
     500(*   [RTL.St_clear_carry dummy_lbl ; *)
     501(*    RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ; *)
     502(*    RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ; *)
     503(*    RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ; *)
     504(*    RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)] *)
     505
     506(* let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl *)
     507(*     srcrs1 srcrs2 = *)
     508(*   let f (insts, leq) srcr1 srcr2 = *)
     509(*     let added_insts = *)
     510(*       translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq *)
     511(*      srcr1 srcr2 in *)
     512(*     (insts @ added_insts, leq @ [(srcr1, srcr2)]) in *)
     513(*   fst (List.fold_left2 f ([], []) srcrs1 srcrs2) *)
     514
     515(* let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def = *)
     516(*   match destrs with *)
     517(*     | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def *)
     518(*     | _ -> *)
     519(*       let (def, tmp_destrs) = fresh_regs def (List.length destrs) in *)
     520(*       let tmp_destr = List.hd tmp_destrs in *)
     521(*       let (def, tmp_zero) = fresh_reg def in *)
     522(*       let (def, tmp_one) = fresh_reg def in *)
     523(*       let (def, tmpr1) = fresh_reg def in *)
     524(*       let (def, tmpr2) = fresh_reg def in *)
     525(*       let (def, tmpr3) = fresh_reg def in *)
     526(*       let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in *)
     527(*       let srcrs1 = List.rev srcrs1 in *)
     528(*       let srcrs2 = List.rev srcrs2 in *)
     529(*       let insts_init = *)
     530(*      [translate_cst (AST.Cst_int 0) tmp_destrs ; *)
     531(*       translate_cst (AST.Cst_int 0) added ; *)
     532(*       adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ; *)
     533(*                   RTL.St_int (tmp_one, 1, start_lbl)]] in *)
     534(*       let insts_main = *)
     535(*      translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl *)
     536(*        srcrs1 srcrs2 in *)
     537(*       let insts_main = [adds_graph insts_main] in *)
     538(*       let insts_exit = [translate_move destrs tmp_destrs] in *)
     539(*       add_translates (insts_init @ insts_main @ insts_exit ) *)
     540(*      start_lbl dest_lbl def *)
     541
     542let rec pad_with p l1 l2 = match l1, l2 with
     543  | [], [] -> ([], [])
     544  | x :: xs, y :: ys ->
     545    let (xs', ys') = pad_with p xs ys in
     546    (x :: xs', y :: ys')
     547  | [], _ -> (MiscPottier.make p (List.length l2), l2)
     548  | _, [] -> (l1, MiscPottier.make p (List.length l1))
     549
     550let translate_ltu desrtrs srcrs1 srcrs2 start_lbl dest_lbl def =
     551  match desrtrs with
     552    | [] -> adds_graph [] start_lbl dest_lbl def
     553    | destr :: destrs ->
     554      let (def, tmpr_zero) = fresh_reg def in
     555      let (srcrs1, srcrs2) = pad_with tmpr_zero srcrs1 srcrs2 in
     556      let init =
     557        [RTL.St_move (tmpr_zero, RTL.Imm 0, start_lbl) ;
     558         RTL.St_clear_carry start_lbl] in
     559      let f srcr1 srcr2 =
     560        RTL.St_op2 (I8051.Sub, destr, srcr1, RTL.Reg srcr2, start_lbl) in
     561      (* not interested in result, just the carry bit
     562         the following is safe even if destrs = srcrsi *)
     563      let iter_sub = List.map2 f srcrs1 srcrs2 in
     564      let extract_carry =
     565        [RTL.St_op2 (I8051.Addc, destr, tmpr_zero,
     566                     RTL.Reg tmpr_zero, start_lbl)] in
     567      let epilogue = translate_cst (AST.Cst_int 0) destrs in
     568      add_translates [adds_graph (init @ iter_sub @ extract_carry);
     569                      epilogue] start_lbl dest_lbl def
     570
     571let rec add_128_to_last
     572    (tmp_128 : Register.t)
     573    (last_subst : Register.t)
     574    (rs : Register.t list)
     575    (dummy_lbl : Label.t) = match rs with
     576  | [] -> ([], adds_graph [])
     577  | [last] ->
     578    let insts =
     579      [RTL.St_move (last_subst, RTL.Reg last, dummy_lbl) ;
     580       RTL.St_op2 (I8051.Add, last_subst, last_subst,
     581                   RTL.Reg tmp_128, dummy_lbl)] in
     582    ([last_subst], adds_graph insts)
     583  | hd :: tail ->
     584    let (tail', trans) = add_128_to_last tmp_128 last_subst tail dummy_lbl in
     585    (hd :: tail', trans)
     586
     587(* what happens if srcrs1 and srcrs2 have different length? seems to me
     588   128 is added at the wrong place then *)
    524589let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def =
    525   let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in
    526   let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in
     590  let (def, tmp_last_srcr1) = fresh_reg def in
     591  let (def, tmp_last_srcr2) = fresh_reg def in
    527592  let (def, tmp_128) = fresh_reg def in
     593  (* I save just the last registers *)
     594  let (srcrs1, add_128_to_srcrs1) =
     595    add_128_to_last tmp_128 tmp_last_srcr1 srcrs1 start_lbl in
     596  let (srcrs2, add_128_to_srcrs2) =
     597    add_128_to_last tmp_128 tmp_last_srcr2 srcrs2 start_lbl in
    528598  add_translates
    529     [translate_move tmp_srcrs1 srcrs1 ;
    530      translate_move tmp_srcrs2 srcrs2 ;
    531      adds_graph [RTL.St_int (tmp_128, 128, start_lbl)] ;
    532      add_128_to_last tmp_128 tmp_srcrs1 ;
    533      add_128_to_last tmp_128 tmp_srcrs2 ;
    534      translate_lt destrs tmp_srcrs1 tmp_srcrs2]
     599    [adds_graph [RTL.St_move (tmp_128, RTL.Imm 128, start_lbl)] ;
     600     add_128_to_srcrs1;
     601     add_128_to_srcrs2;
     602     translate_ltu destrs srcrs1 srcrs2]
    535603    start_lbl dest_lbl def
    536604
    537605
    538 let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     606let translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
    539607  match op2 with
    540608
     
    569637    | AST.Op_cmpp AST.Cmp_eq ->
    570638      add_translates
    571         [translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ;
    572          translate_op1 AST.Op_notbool destrs destrs]
    573         start_lbl dest_lbl def
     639        [translate_ne destrs srcrs1 srcrs2 ;
     640         translate_toggle_bool destrs] start_lbl dest_lbl def
    574641
    575642    | AST.Op_cmp AST.Cmp_ne
     
    582649
    583650    | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
    584       translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def
     651      translate_ltu destrs srcrs1 srcrs2 start_lbl dest_lbl def
    585652
    586653    | AST.Op_cmp AST.Cmp_le ->
    587654      add_translates
    588         [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
    589          translate_op1 AST.Op_notbool destrs destrs]
    590         start_lbl dest_lbl def
    591 
    592     | AST.Op_cmpu AST.Cmp_le ->
     655        [translate_lts destrs srcrs2 srcrs1 ;
     656         translate_toggle_bool destrs] start_lbl dest_lbl def
     657
     658    | AST.Op_cmpu AST.Cmp_le | AST.Op_cmpp AST.Cmp_le ->
    593659      add_translates
    594         [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ;
    595          translate_op1 AST.Op_notbool destrs destrs]
    596         start_lbl dest_lbl def
    597 
    598     | AST.Op_cmpp AST.Cmp_le ->
    599       add_translates
    600         [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
    601          translate_op1 AST.Op_notbool destrs destrs]
    602         start_lbl dest_lbl def
     660        [translate_ltu destrs srcrs2 srcrs1 ;
     661         translate_toggle_bool destrs] start_lbl dest_lbl def
    603662
    604663    | AST.Op_cmp AST.Cmp_gt ->
    605       translate_op2 (AST.Op_cmp AST.Cmp_lt)
    606         destrs srcrs2 srcrs1 start_lbl dest_lbl def
    607 
    608     | AST.Op_cmpu AST.Cmp_gt ->
    609       translate_op2 (AST.Op_cmpu AST.Cmp_lt)
    610         destrs srcrs2 srcrs1 start_lbl dest_lbl def
    611 
    612     | AST.Op_cmpp AST.Cmp_gt ->
    613       translate_op2 (AST.Op_cmpp AST.Cmp_lt)
    614         destrs srcrs2 srcrs1 start_lbl dest_lbl def
     664      translate_lts destrs srcrs2 srcrs1 start_lbl dest_lbl def
     665
     666    | AST.Op_cmpu AST.Cmp_gt | AST.Op_cmpp AST.Cmp_gt ->
     667      translate_ltu destrs srcrs2 srcrs1 start_lbl dest_lbl def
    615668
    616669    | AST.Op_cmp AST.Cmp_ge ->
    617670      add_translates
    618         [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
    619          translate_op1 AST.Op_notbool destrs destrs]
    620         start_lbl dest_lbl def
    621 
    622     | AST.Op_cmpu AST.Cmp_ge ->
     671        [translate_lts destrs srcrs1 srcrs2 ;
     672         translate_toggle_bool destrs] start_lbl dest_lbl def
     673
     674    | AST.Op_cmpu AST.Cmp_ge | AST.Op_cmpp AST.Cmp_ge ->
    623675      add_translates
    624         [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
    625          translate_op1 AST.Op_notbool destrs destrs]
    626         start_lbl dest_lbl def
    627 
    628     | AST.Op_cmpp AST.Cmp_ge ->
    629       add_translates
    630         [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
    631          translate_op1 AST.Op_notbool destrs destrs]
    632         start_lbl dest_lbl def
     676        [translate_ltu destrs srcrs1 srcrs2 ;
     677         translate_toggle_bool destrs] start_lbl dest_lbl def
    633678
    634679    | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
     
    639684
    640685let translate_cond srcrs start_lbl lbl_true lbl_false def =
    641   let (def, tmpr) = fresh_reg def in
    642   let tmp_lbl = fresh_label def in
    643   let init = RTL.St_int (tmpr, 0, start_lbl) in
    644   let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, srcr, start_lbl) in
    645   let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
    646   add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def
     686  match srcrs with
     687    | [] -> add_graph start_lbl (RTL.St_skip lbl_false) def
     688    | srcr :: srcrs ->
     689      let (def, tmpr) = fresh_reg def in
     690      let tmp_lbl = fresh_label def in
     691      let init = RTL.St_move (tmpr, RTL.Reg srcr, start_lbl) in
     692      let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, RTL.Reg srcr, start_lbl) in
     693      let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
     694      add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def
    647695
    648696
     
    656704    let translates =
    657705      translates @
    658         [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
     706        [adds_graph [RTL.St_move (tmpr, RTL.Imm off, start_lbl)] ;
    659707         translate_op2 AST.Op_addp tmp_addr save_addr [tmpr] ;
    660708         adds_graph [RTL.St_load (r, tmp_addr1, tmp_addr2, dest_lbl)]] in
     
    671719    let translates =
    672720      translates @
    673         [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
     721        [adds_graph [RTL.St_move (tmpr, RTL.Imm off, start_lbl)] ;
    674722         translate_op2 AST.Op_addp tmp_addr addr [tmpr] ;
    675723         adds_graph [RTL.St_store (tmp_addr1, tmp_addr2, srcr, dest_lbl)]] in
     
    747795  | RTLabs.St_return (Some r) ->
    748796    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
    749                
     797
    750798  | _ -> assert false (*not possible because of previous removal of immediates*)
    751799
  • Deliverables/D2.2/8051/src/common/intValue.ml

    r818 r1568  
    6666  val logxor  : t -> t -> t
    6767  val shl     : t -> t -> t
     68  val rotl    : t -> t
    6869  val shr     : t -> t -> t
    6970  val shrl    : t -> t -> t
     
    176177    let pow = power_int_positive_big_int 2 (cast b) in
    177178    cast (mult_big_int a pow)
     179
     180  let rotl a =
     181    if ge_big_int a half_bound then
     182      cast (add_big_int (mult_big_int a two) one)
     183    else
     184      cast (mult_big_int a two)
    178185
    179186  let shr a b =
  • Deliverables/D2.2/8051/src/common/intValue.mli

    r818 r1568  
    6262  val logxor  : t -> t -> t
    6363  val shl     : t -> t -> t
     64  val rotl    : t -> t
    6465  val shr     : t -> t -> t
    6566  val shrl    : t -> t -> t
  • Deliverables/D2.2/8051/src/common/memory.ml

    r818 r1568  
    88
    99let error_prefix = "Memory"
    10 let error s = Error.global_error error_prefix s
     10let error s = invalid_arg (error_prefix ^ s)
    1111
    1212
  • Deliverables/D2.2/8051/src/common/value.ml

    r818 r1568  
    113113  val xor        : t -> t -> t
    114114  val shl        : t -> t -> t
     115  val rotl       : t -> t
    115116  val shr        : t -> t -> t
    116117  val shru       : t -> t -> t
     
    376377  let xor    = binary_int_op ValInt.logxor
    377378  let shl    = binary_int_op ValInt.shl
     379  let rotl   = unary_int_op ValInt.rotl
    378380  let shr    = binary_int_op ValInt.shr
    379381  let shru   = binary_int_op ValInt.shrl
  • Deliverables/D2.2/8051/src/common/value.mli

    r818 r1568  
    105105  val xor        : t -> t -> t
    106106  val shl        : t -> t -> t
     107  val rotl       : t -> t
    107108  val shr        : t -> t -> t
    108109  val shru       : t -> t -> t
Note: See TracChangeset for help on using the changeset viewer.