- Timestamp:
- Sep 2, 2011, 2:51:20 PM (10 years ago)
- Location:
- src/ERTL
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTL.ma
r1168 r1171 15 15 definition ertl_params: params ≝ 16 16 mk_params register register register register (move_registers × move_registers) register. 17 18 inductive ertl_statement_extension: Type[0] ≝ 19 | ertl_st_ext_new_frame: label → ertl_statement_extension 20 | ertl_st_ext_del_frame: label → ertl_statement_extension 21 | ertl_st_ext_frame_size: register → label → ertl_statement_extension. 17 22 18 definition pre_ertl_statement ≝ joint_statement label ertl_params. 19 20 inductive ertl_statement (globals: list ident): Type[0] ≝ 21 | ertl_st_lift_pre: pre_ertl_statement globals → ertl_statement globals 22 | ertl_st_new_frame: label → ertl_statement globals 23 | ertl_st_del_frame: label → ertl_statement globals 24 | ertl_st_frame_size: register → label → ertl_statement globals. 23 definition ertl_statement ≝ joint_statement label ertl_statement_extension ertl_params. 25 24 26 25 definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals). -
src/ERTL/ERTLToLTL.ma
r1170 r1171 167 167 λl. 168 168 if eq_nat (stacksize globals int_fun) 0 then 169 〈joint_st_goto ? globals l, graph〉169 〈joint_st_goto … globals l, graph, (ertl_if_luniverse globals int_fun)〉 170 170 else 171 171 let luniv ≝ ertl_if_luniverse globals int_fun in 172 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in173 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals SubRegisterDPH) l) in174 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_intglobals RegisterDPH (zero ?)) l) in175 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in176 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in177 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals SubRegisterDPL) l) in178 let 〈l, graph, luniv e〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_clear_carryglobals) l) in179 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? (stacksizeint_fun))) l) in180 〈joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l, graph, luniv〉.172 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? ? globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in 173 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in 174 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in 175 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in 176 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in 177 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in 178 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) in 179 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in 180 〈joint_st_sequential … globals (joint_instr_move ltl_params … globals (to_acc RegisterSPL)) l, graph, luniv〉. 181 181 182 182 definition delframe ≝ 183 λ int_fun.184 λ globals.183 λglobals. 184 λint_fun. 185 185 λgraph: graph (ltl_statement globals). 186 186 λl. 187 if eq_nat (stacksize int_fun) 0 then188 〈joint_st_goto ? globals l, graph〉187 if eq_nat (stacksize globals int_fun) 0 then 188 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉 189 189 else 190 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in 191 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in 192 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in 193 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in 194 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in 195 〈joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? (stacksize int_fun))) l, graph〉. 190 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 … globals (joint_instr_int ltl_params … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉. 197 198 check joint_st_sequential. 196 199 197 200 definition translate_statement ≝ 198 λ int_fun.199 λ globals: list ident.200 λgraph: graph (ltl_statement globals).201 λstmt: ertl_statement .201 λglobals: list ident. 202 λint_fun. 203 λgraph: ltl_statement_graph globals. 204 λstmt: ertl_statement globals. 202 205 match stmt with 203 [ ertl_st_skip l ⇒ 〈joint_st_goto ? globals l, graph〉 204 | ertl_st_comment s l ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉 206 [ ertl_st_lift_pre pre ⇒ 207 match pre with 208 [ joint_st_sequential seq l ⇒ 209 match seq with 210 [ joint_instr_comment c ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉 211 | _ ⇒ ? 212 ] 213 | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉 214 | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉 215 ] 216 | ertl_st_new_frame l ⇒ newframe globals int_fun graph l 217 | ertl_st_del_frame l ⇒ delframe globals int_fun graph l 218 | ertl_st_frame_size r l ⇒ 219 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in 220 〈joint_st_sequential … globals (joint_instr_int ltl_params … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉 221 ]. 222 223 match stmt with 224 | ertl_st_comment s l ⇒ 205 225 | ertl_st_cost cost_lbl l ⇒ 〈joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l, graph〉 206 226 | ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l … … 209 229 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in 210 230 〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉 211 | ertl_st_new_frame l ⇒ newframe int_fun globals graph l212 | ertl_st_del_frame l ⇒ delframe int_fun globals graph l231 | ertl_st_new_frame l ⇒ 232 | ertl_st_del_frame l ⇒ 213 233 | ertl_st_frame_size r l ⇒ 214 let 〈hdw, l〉 ≝ write int_fun globals graph r l in215 let 〈l, graph〉 ≝ l in216 〈joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? (stacksize int_fun))) l, graph〉217 234 | ertl_st_pop r l ⇒ 218 235 let 〈hdw, l〉 ≝ write int_fun globals graph r l in … … 335 352 let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 336 353 〈joint_st_goto ? globals l, graph〉 337 | ertl_st_return ⇒ 〈joint_st_return ? globals, graph〉338 354 ]. 339 355 cases daemon (* XXX: todo -- proofs regarding gvars *)
Note: See TracChangeset
for help on using the changeset viewer.