Changeset 1083 for src/ERTL


Ignore:
Timestamp:
Jul 21, 2011, 12:28:11 PM (9 years ago)
Author:
mulligan
Message:

ertl --> ltl statement generation nearly complete. required some changes to ltl and below

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTLI.ma

    r1082 r1083  
    2828  λl.
    2929    let off ≝ adjust_off off in
    30     let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r) l)) in
    31     let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_load globals) l)) in
    32     let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l)) in
    33     let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l)) in
    34     let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l)) in
    35     let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l)) in
    36     let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l)) in
     30    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
     31    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
     32    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     33    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     34    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     35    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     36    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    3737      joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
    3838
     
    4343  λl.
    4444  let off ≝ adjust_off off in
    45   let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_store globals) l)) in
    46   let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals r) l)) in
    47   let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l)) in
    48   let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l)) in
    49   let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l)) in
    50   let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l)) in
    51   let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l)) in
     45  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
     46  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
     47  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     48  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     49  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     50  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     51  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    5252    joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
    5353
     
    5555  λglobals.
    5656  λr: register.
    57   λl: ident.
     57  λl: label.
    5858  match lookup r with
    59   [ decision_spill off ⇒ 〈RegisterSST, label_to_ident (generate globals (set_stack globals off RegisterSST l))〉
     59  [ decision_spill off ⇒ 〈RegisterSST, generate globals (set_stack globals off RegisterSST l)〉
    6060  | decision_colour hwr ⇒ 〈hwr, l〉
    6161  ].
     
    7070    let temphwr ≝ RegisterSST in
    7171    let l ≝ generate globals (stmt temphwr) in
    72       generate globals (get_stack globals temphwr off (label_to_ident l))
    73   ].
    74 
     72      generate globals (get_stack globals temphwr off l)
     73  ].
     74
     75definition move ≝
     76  λglobals: list ident.
     77  λdest: decision.
     78  λsrc: decision.
     79  λl: label.
     80  match dest with
     81  [ decision_colour dest_hwr ⇒
     82    match src with
     83    [ decision_colour src_hwr ⇒
     84      if eq_Register dest_hwr src_hwr then
     85        joint_st_sequential ? globals (joint_instr_skip globals) l
     86      else
     87        let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
     88          joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l
     89    | decision_spill src_off ⇒ get_stack globals dest_hwr src_off l
     90    ]
     91  | decision_spill dest_off ⇒
     92    match src with
     93    [ decision_colour src_hwr ⇒ set_stack globals dest_off src_hwr l
     94    | decision_spill src_off ⇒
     95      if eq_bv ? dest_off src_off then
     96        joint_st_sequential ? globals (joint_instr_skip globals) l
     97      else
     98        let temp_hwr ≝ RegisterSST in
     99        let l ≝ generate globals (set_stack globals dest_off temp_hwr l) in
     100          get_stack globals temp_hwr src_off l
     101    ]
     102  ].
     103
     104definition newframe ≝
     105  λglobals.
     106  λl.
     107  if eq_nat stacksize 0 then
     108    joint_st_sequential ? globals (joint_instr_skip globals) l
     109  else
     110    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     111    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
     112    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
     113    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
     114    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
     115    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
     116    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
     117    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? stacksize)) l) in
     118      joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l.
     119
     120definition delframe ≝
     121  λglobals.
     122  λl.
     123  if eq_nat stacksize 0 then
     124    joint_st_sequential ? globals (joint_instr_skip globals) l
     125  else
     126    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     127    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     128    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     129    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
     130    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
     131      joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? stacksize)) l.
     132
     133definition translate_statement ≝
     134  λglobals: list ident.
     135  λstmt: ertl_statement.
     136  match stmt with
     137  [ ertl_st_skip l ⇒ joint_st_sequential ? globals (joint_instr_skip globals) l
     138  | ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l
     139  | ertl_st_cost cost_lbl l ⇒ joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l
     140  | ertl_st_get_hdw destr sourcehwr l ⇒ move globals (lookup destr) (decision_colour sourcehwr) l
     141  | ertl_st_set_hdw desthwr srcr l ⇒ move globals (decision_colour desthwr) (lookup srcr) l
     142  | ertl_st_hdw_to_hdw r1 r2 l ⇒
     143    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
     144      joint_st_sequential ? globals (joint_instr_to_acc globals r2) l
     145  | ertl_st_new_frame l ⇒ newframe globals l
     146  | ertl_st_del_frame l ⇒ delframe globals l
     147  | ertl_st_frame_size r l ⇒
     148    let 〈hdw, l〉 ≝ write globals r l in
     149      joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? stacksize)) l
     150  | ertl_st_pop r l ⇒
     151    let 〈hdw, l〉 ≝ write globals r l in
     152    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     153      joint_st_sequential ? globals (joint_instr_pop globals) l
     154  | ertl_st_push r l ⇒
     155    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_push globals) l) in
     156    let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     157      joint_st_sequential ? globals (joint_instr_skip globals) l
     158  | _ ⇒ ?
     159  ].
     160
     161  let translate_statement (stmt : ERTL.statement) : LTL.statement =
     162    match stmt with
     163
     164      | ERTL.St_addrH (r, x, l) ->
     165        let (hdw, l) = write r l in
     166        let l = generate (LTL.St_from_acc (hdw, l)) in
     167        let l = generate (LTL.St_to_acc (I8051.dph, l)) in
     168        LTL.St_addr (x, l)
     169
     170      | ERTL.St_addrL (r, x, l) ->
     171        let (hdw, l) = write r l in
     172        let l = generate (LTL.St_from_acc (hdw, l)) in
     173        let l = generate (LTL.St_to_acc (I8051.dpl, l)) in
     174        LTL.St_addr (x, l)
     175
     176      | ERTL.St_int (r, i, l) ->
     177        let (hdw, l) = write r l in
     178        LTL.St_int (hdw, i, l)
     179
     180      | ERTL.St_move (r1, r2, l) ->
     181        move (lookup r1) (lookup r2) l
     182
     183      | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) ->
     184        let (hdw, l) = write destr l in
     185        let l = generate (LTL.St_from_acc (hdw, l)) in
     186        let l = generate (LTL.St_opaccs (opaccs, l)) in
     187        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     188        let l = generate (LTL.St_from_acc (I8051.b, l)) in
     189        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     190        LTL.St_skip l
     191
     192      | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) ->
     193        let (hdw, l) = write destr l in
     194        let l = generate (LTL.St_from_acc (hdw, l)) in
     195        let l = generate (LTL.St_to_acc (I8051.b, l)) in
     196        let l = generate (LTL.St_opaccs (opaccs, l)) in
     197        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     198        let l = generate (LTL.St_from_acc (I8051.b, l)) in
     199        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     200        LTL.St_skip l
     201
     202      | ERTL.St_op1 (op1, destr, srcr, l) ->
     203        let (hdw, l) = write destr l in
     204        let l = generate (LTL.St_from_acc (hdw, l)) in
     205        let l = generate (LTL.St_op1 (op1, l)) in
     206        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
     207        LTL.St_skip l
     208
     209      | ERTL.St_op2 (op2, destr, srcr1, srcr2, l) ->
     210        let (hdw, l) = write destr l in
     211        let l = generate (LTL.St_from_acc (hdw, l)) in
     212        let l = generate (LTL.St_op2 (op2, I8051.b, l)) in
     213        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     214        let l = generate (LTL.St_from_acc (I8051.b, l)) in
     215        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     216        LTL.St_skip l
     217
     218      | ERTL.St_clear_carry l ->
     219        LTL.St_clear_carry l
     220
     221      | ERTL.St_set_carry l ->
     222        LTL.St_set_carry l
     223
     224      | ERTL.St_load (destr, addr1, addr2, l) ->
     225        let (hdw, l) = write destr l in
     226        let l = generate (LTL.St_from_acc (hdw, l)) in
     227        let l = generate (LTL.St_load l) in
     228        let l = generate (LTL.St_from_acc (I8051.dph, l)) in
     229        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
     230        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
     231        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     232        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
     233        let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     234        LTL.St_skip l
     235
     236      | ERTL.St_store (addr1, addr2, srcr, l) ->
     237        let l = generate (LTL.St_store l) in
     238        let l = generate (LTL.St_to_acc (I8051.st1, l)) in
     239        let l = generate (LTL.St_from_acc (I8051.dph, l)) in
     240        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
     241        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
     242        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     243        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
     244        let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     245        let l = generate (LTL.St_from_acc (I8051.st1, l)) in
     246        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
     247        LTL.St_skip l
     248
     249      | ERTL.St_call_id (f, _, l) ->
     250        LTL.St_call_id (f, l)
     251
     252      | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
     253        let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
     254        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
     255        LTL.St_skip l
     256
     257      | ERTL.St_return _ ->
     258        LTL.St_return
Note: See TracChangeset for help on using the changeset viewer.