 Timestamp:
 Sep 2, 2011, 5:58:01 PM (9 years ago)
 Location:
 src/ERTL
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTL.ma
r1171 r1175 37 37 }. 38 38 39 definition set_luniverse ≝ 40 λglobals : list ident. 41 λint_fun : ertl_internal_function globals. 42 λluniverse: universe LabelTag. 43 let runiverse ≝ ertl_if_runiverse globals int_fun in 44 let params ≝ ertl_if_params globals int_fun in 45 let locals ≝ ertl_if_locals globals int_fun in 46 let stacksize ≝ ertl_if_stacksize globals int_fun in 47 let graph ≝ ertl_if_graph globals int_fun in 48 let entry ≝ ertl_if_entry globals int_fun in 49 let exit ≝ ertl_if_exit globals int_fun in 50 mk_ertl_internal_function globals 51 luniverse runiverse params locals 52 stacksize graph entry exit. 53 39 54 definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals). 40 55 
src/ERTL/ERTLToLTL.ma
r1172 r1175 202 202 λstmt: ertl_statement globals. 203 203 match stmt with 204 [ ertl_st_lift_pre pre ⇒ 205 match pre with 206 [ joint_st_sequential seq l ⇒ 207 match seq with 208 [ joint_instr_comment c ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉 209  _ ⇒ ? 210 ] 211  joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉 212  joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉 204 [ joint_st_sequential seq l ⇒ 205 let luniv ≝ ertl_if_luniverse globals int_fun in 206 match seq with 207 [ joint_instr_comment c ⇒ 208 〈joint_st_sequential label unit ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉 209  joint_instr_cost_label cost_lbl ⇒ 210 〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉 211  joint_instr_pop r ⇒ 212 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in 213 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 214 〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉 215  joint_instr_push r ⇒ 216 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in 217 let int_fun ≝ set_luniverse globals int_fun luniv in 218 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〉 220  joint_instr_cond srcr lbl_true ⇒ 221 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in 222 let int_fun ≝ set_luniverse globals int_fun luniv in 223 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〉 225  joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉 226  joint_instr_store addr1 addr2 srcr ⇒ 227 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in 228 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST1)) l) in 229 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in 230 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in 231 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 232 let int_fun ≝ set_luniverse globals int_fun luniv in 233 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 234 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in 235 let int_fun ≝ set_luniverse globals int_fun luniv in 236 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 237 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in 238 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〉 240  joint_instr_load destr addr1 addr2 ⇒ 241 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in 242 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 243 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in 244 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in 245 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in 246 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 247 let int_fun ≝ set_luniverse globals int_fun luniv in 248 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 249 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in 250 let int_fun ≝ set_luniverse globals int_fun luniv in 251 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〉 253  joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉 254  joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉 255  joint_instr_op2 op2 destr srcr ⇒ 256 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in 257 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 258 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in 259 let luniv ≝ set_luniverse globals int_fun luniv in 260 let 〈l, graph, luniv〉 ≝ read globals int_fun graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 261 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 262 let luniv ≝ set_luniverse globals int_fun luniv in 263 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〉 265  joint_instr_op1 op1 acc_a ⇒ 266 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a l in 267 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 268 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in 269 let int_fun ≝ set_luniverse globals int_fun luniv in 270 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〉 272  joint_instr_int r i ⇒ 273 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〉 275  joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒ 276 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a_reg l in 277 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 278 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in 279 let luniv ≝ set_luniverse globals int_fun luniv in 280 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 281 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 282 let luniv ≝ set_luniverse globals int_fun luniv in 283 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 284 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in 285 let luniv ≝ set_luniverse globals int_fun luniv in 286 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_b_reg l in 287 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 288 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in 289 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in 290 let luniv ≝ set_luniverse globals int_fun luniv in 291 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 292 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 293 let luniv ≝ set_luniverse globals int_fun luniv in 294 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〉 296  _ ⇒ ? 213 297 ] 214  ertl_st_new_frame l ⇒ newframe globals int_fun graph l 215  ertl_st_del_frame l ⇒ delframe globals int_fun graph l 216  ertl_st_frame_size r l ⇒ 217 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in 218 〈joint_st_sequential … globals (joint_instr_int ltl_params … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉 298  joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉 299  joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉 300  joint_st_extension ext ⇒ 301 match ext with 302 [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l 303  ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l 304  ertl_st_ext_frame_size r l ⇒ 305 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〉 307 ] 219 308 ]. 220 309 221 310 match stmt with 222  ertl_st_comment s l ⇒223  ertl_st_cost cost_lbl l ⇒ 〈joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l, graph〉224 311  ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l 225 312  ertl_st_set_hdw desthwr srcr l ⇒ move int_fun globals graph (decision_colour desthwr) (lookup srcr) l … … 227 314 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in 228 315 〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉 229  ertl_st_new_frame l ⇒230  ertl_st_del_frame l ⇒231  ertl_st_frame_size r l ⇒232  ertl_st_pop r l ⇒233 let 〈hdw, l〉 ≝ write int_fun globals graph r l in234 let 〈l, graph〉 ≝ l in235 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in236 〈joint_st_sequential ? globals (joint_instr_pop globals) l, graph〉237  ertl_st_push r l ⇒238 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_push globals) l) in239 let 〈l, graph〉 ≝ read int_fun globals graph r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in240 〈joint_st_goto ? globals l, graph〉241 316  ertl_st_addr rl rh x l ⇒ 242 317 let 〈hdw1, l〉 ≝ write int_fun globals graph rh l in … … 261 336 ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) 262 337 *) 263  ertl_st_int r i l ⇒264 let 〈hdw, l〉 ≝ write int_fun globals graph r l in265 let 〈l, graph〉 ≝ l in266 〈joint_st_sequential ? globals (joint_instr_int globals hdw i) l, graph〉267 338  ertl_st_move r1 r2 l ⇒ move int_fun globals graph (lookup r1) (lookup r2) l 268  ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒269 let 〈hdw, l〉 ≝ write int_fun globals graph destr1 l in270 let 〈l, graph〉 ≝ l in271 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in272 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in273 let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in274 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in275 let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in276 let 〈l, graph〉 ≝ generate globals graph (joint_st_goto ? globals l) in277 let 〈hdw, l〉 ≝ write int_fun globals graph destr2 l in278 let 〈l, graph〉 ≝ l in279 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in280 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in281 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in282 let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in283 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in284 let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in285 〈joint_st_goto ? globals l, graph〉286 339 (* 287 340  ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒ … … 303 356 joint_st_goto ? globals l 304 357 *) 305  ertl_st_op1 op1 destr srcr l ⇒306 let 〈hdw, l〉 ≝ write int_fun globals graph destr l in307 let 〈l, graph〉 ≝ l in308 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in309 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in310 let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in311 〈joint_st_goto ? globals l, graph〉312  ertl_st_op2 op2 destr srcr1 srcr2 l ⇒313 let 〈hdw, l〉 ≝ write int_fun globals graph destr l in314 let 〈l, graph〉 ≝ l in315 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in316 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in317 let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in318 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in319 let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in320 〈joint_st_goto ? globals l, graph〉321  ertl_st_clear_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_clear_carry globals) l, graph〉322  ertl_st_set_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_set_carry globals) l, graph〉323  ertl_st_load destr addr1 addr2 l ⇒324 let 〈hdw, l〉 ≝ write int_fun globals graph destr l in325 let 〈l, graph〉 ≝ l in326 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in327 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_load globals) l) in328 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in329 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in330 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in331 let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in332 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in333 let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in334 〈joint_st_goto ? globals l, graph〉335  ertl_st_store addr1 addr2 srcr l ⇒336 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_store globals) l) in337 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in338 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in339 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in340 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in341 let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in342 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in343 let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in344 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in345 let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in346 〈joint_st_goto ? globals l, graph〉347  ertl_st_call_id f ignore l ⇒ 〈joint_st_sequential ? globals (joint_instr_call_id globals f) l, graph〉348  ertl_st_cond srcr lbl_true lbl_false ⇒349 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in350 let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in351 〈joint_st_goto ? globals l, graph〉352 358 ]. 353 359 cases daemon (* XXX: todo  proofs regarding gvars *)
Note: See TracChangeset
for help on using the changeset viewer.