Changeset 1179


Ignore:
Timestamp:
Sep 5, 2011, 11:58:58 AM (8 years ago)
Author:
mulligan
Message:

changes to ertl, ltl and lin to use new notion of joint params. ertl to ltl pass in process of being changed

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1175 r1179  
    167167  λl: label.
    168168  if eq_nat (stacksize globals int_fun) 0 then
    169     〈joint_st_goto label unit ltl_params globals l, graph, (ertl_if_luniverse globals int_fun)〉
     169    〈joint_st_goto ltl_params globals l, graph, (ertl_if_luniverse globals int_fun)〉
    170170  else
    171171    let luniv ≝ ertl_if_luniverse globals int_fun in
    172     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    173     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
    174     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
    175     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
    176     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    177     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
    178     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_clear_carry … globals) l) in
    179     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
    180       〈joint_st_sequential label unit ltl_params globals (joint_instr_move ltl_params globals (to_acc RegisterSPL)) l, graph, luniv〉.
     172    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
     173    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
     174    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
     175    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
     176    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
     177    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
     178    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_clear_carry … globals) l) in
     179    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
     180      〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc RegisterSPL)) l, graph, luniv〉.
    181181
    182182definition delframe ≝
     
    186186  λl.
    187187  if eq_nat (stacksize globals int_fun) 0 then
    188     〈joint_st_goto globals l, graph, ertl_if_luniverse globals int_fun〉
     188    〈joint_st_goto ltl_params globals l, graph, ertl_if_luniverse globals int_fun〉
    189189  else
    190190    let luniv ≝ ertl_if_luniverse globals int_fun in
    191     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    192     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
    193     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    194     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    195     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    196       〈joint_st_sequential label unit ltl_params globals (joint_instr_int ltl_params … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
     191    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
     192    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     193    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     194    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
     195    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
     196      〈joint_st_sequential ltl_params globals (joint_instr_int ltl_params globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
    197197
    198198definition translate_statement ≝
     
    206206    match seq with
    207207    [ joint_instr_comment c ⇒
    208       〈joint_st_sequential label unit ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉
     208      〈joint_st_sequential ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉
    209209    | joint_instr_cost_label cost_lbl ⇒
    210210      〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉
     
    217217      let int_fun ≝ set_luniverse globals int_fun luniv in
    218218      let 〈l, graph, luniv〉 ≝ read globals int_fun graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    219         〈joint_st_goto globals l, graph, luniv〉
     219        〈joint_st_goto ltl_params globals l, graph, luniv〉
    220220    | joint_instr_cond srcr lbl_true ⇒
    221221      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
    222222      let int_fun ≝ set_luniverse globals int_fun luniv in
    223223      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    224         〈joint_st_goto globals l, graph, luniv〉
     224        〈joint_st_goto ltl_params globals l, graph, luniv〉
    225225    | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉
    226226    | joint_instr_store addr1 addr2 srcr ⇒
     
    237237      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
    238238      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    239         〈joint_st_goto globals l, graph, luniv〉
     239        〈joint_st_goto ltl_params globals l, graph, luniv〉
    240240    | joint_instr_load destr addr1 addr2 ⇒
    241241      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
     
    250250      let int_fun ≝ set_luniverse globals int_fun luniv in
    251251      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    252         〈joint_st_goto globals l, graph, luniv〉
     252        〈joint_st_goto ltl_params globals l, graph, luniv〉
    253253    | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉
    254254    | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉
     
    262262      let luniv ≝ set_luniverse globals int_fun luniv in
    263263      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    264         〈joint_st_goto globals l, graph, luniv〉
     264        〈joint_st_goto ltl_params globals l, graph, luniv〉
    265265    | joint_instr_op1 op1 acc_a ⇒
    266266      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a l in
     
    269269      let int_fun ≝ set_luniverse globals int_fun luniv in
    270270      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    271         〈joint_st_goto globals l, graph, luniv〉
     271        〈joint_st_goto ltl_params globals l, graph, luniv〉
    272272    | joint_instr_int r i ⇒
    273273      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
    274         〈joint_st_sequential label unit ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉
     274        〈joint_st_sequential ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉
    275275    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
    276276      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a_reg l in
     
    293293      let luniv ≝ set_luniverse globals int_fun luniv in
    294294      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    295         〈joint_st_goto globals l, graph, luniv〉
     295        〈joint_st_goto ltl_params globals l, graph, luniv〉
    296296    | _ ⇒ ?
    297297    ]
     
    304304    | ertl_st_ext_frame_size r l ⇒
    305305      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
    306         〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     306        〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
    307307    ]
    308308  ].
  • src/LIN/LIN.ma

    r1171 r1179  
    22
    33definition lin_params: params ≝
    4  mk_params unit unit unit unit registers_move Register.
     4 mk_params
     5   label unit unit unit unit registers_move Register
     6     unit unit unit unit.
    57
    68definition pre_lin_statement ≝
    7  λglobals: list ident. joint_statement unit unit lin_params globals.
     9 λglobals: list ident. joint_statement lin_params globals.
    810
    911definition lin_statement ≝
  • src/LIN/LINToASM.ma

    r1168 r1179  
    3535      match instr' with
    3636      [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    37       | joint_instr_cond lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     37      | joint_instr_cond acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    3838      | _ ⇒ set_empty ?
    3939      ]
    4040    | joint_st_return ⇒ set_empty ?
    4141    | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     42    | joint_st_extension _ ⇒ set_empty ?
    4243    ]
    4344  in
     
    9091  match statement with
    9192  [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
     93  | joint_st_extension ext ⇒ Instruction (NOP ?) (* XXX: NOP or something else? *)
    9294  | joint_st_return ⇒ Instruction (RET ?)
    9395  | joint_st_sequential instr _ ⇒
  • src/LTL/LTL.ma

    r1171 r1179  
    44
    55definition ltl_params: params ≝
    6  mk_params unit unit unit unit registers_move Register.
     6 mk_params
     7   label unit unit unit unit registers_move Register
     8     unit unit unit unit.
    79
    8 definition ltl_statement ≝ λglobals: list ident. joint_statement label unit ltl_params globals.
     10definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals.
    911 
    1012definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
Note: See TracChangeset for help on using the changeset viewer.