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
File:
1 edited

Legend:

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