 Timestamp:
 Sep 23, 2011, 11:49:44 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1258 r1259 295 295 296 296 definition set_param_stack ≝ 297 λglobals. 297 298 λoff. 298 299 λsrcr. 299 300 λstart_lbl: label. 300 301 λdest_lbl: label. 301 λdef: ertl_internal_function .302 let 〈def, addr1〉 ≝ fresh_reg def in303 let 〈def, addr2〉 ≝ fresh_reg def in304 let 〈def, tmpr〉 ≝ fresh_reg def in302 λdef: ertl_internal_function globals. 303 let 〈def, addr1〉 ≝ fresh_reg … def in 304 let 〈def, addr2〉 ≝ fresh_reg … def in 305 let 〈def, tmpr〉 ≝ fresh_reg … def in 305 306 let 〈ignore, int_off〉 ≝ half_add ? off int_size in 306 adds_graph [307 ertl_st_int addr1 int_offstart_lbl;308 ertl_st_get_hdw tmpr RegisterSPLstart_lbl;309 ertl_st_clear_carrystart_lbl;310 ertl_st_op2 Sub addr1 tmpr addr1start_lbl;311 ertl_st_get_hdw tmpr RegisterSPHstart_lbl;312 ertl_st_int addr2 (zero ?) start_lbl;313 ertl_st_op2 Sub addr2 tmpr addr2start_lbl;314 ertl_st_store addr1 addr2 srcrstart_lbl307 adds_graph ? [ 308 joint_st_sequential … (joint_instr_int … addr1 int_off) start_lbl; 309 joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl; 310 joint_st_sequential … (joint_instr_clear_carry …) start_lbl; 311 joint_st_sequential … (joint_instr_op2 … Sub addr1 tmpr addr1) start_lbl; 312 joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl; 313 joint_st_sequential … (joint_instr_int … addr2 (zero ?)) start_lbl; 314 joint_st_sequential … (joint_instr_op2 … Sub addr2 tmpr addr2) start_lbl; 315 joint_st_sequential … (joint_instr_store … addr1 addr2 srcr) start_lbl 315 316 ] start_lbl dest_lbl def. 316 317 317 318 definition set_params_stack ≝ 318 λ params.319 λglobals,params. 319 320 match params with 320 [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skipstart_lbl] start_lbl]321 [ nil ⇒ [ λstart_lbl. adds_graph globals [joint_st_goto … start_lbl] start_lbl] 321 322  _ ⇒ 322 let f ≝ λi. λr. set_param_stack (bitvector_of_nat ? i) r in 323 mapi ? ? f params 324 ]. 325 326 axiom min_fst: 327 ∀m, n: nat. 328 min m n ≤ m. 323 let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in 324 mapi ? ? f params]. 329 325 330 326 definition set_params ≝ 331 λ params.327 λglobals,params. 332 328 let n ≝ min (params) (RegisterParams) in 333 329 let hdw_stack_params ≝ split ? params n ? in 334 330 let hdw_params ≝ \fst hdw_stack_params in 335 331 let stack_params ≝ \snd hdw_stack_params in 336 set_params_hdw hdw_params @ set_params_stackstack_params.337 @min_fst 332 set_params_hdw globals hdw_params @ set_params_stack globals stack_params. 333 /2/ 338 334 qed. 339 335 340 336 definition fetch_result ≝ 337 λglobals. 341 338 λret_regs. 342 339 λstart_lbl: label. … … 345 342 let commonl ≝ \fst (\fst crl) in 346 343 let commonr ≝ \fst (\snd crl) in 347 let f_save ≝ λst. λret. ertl_st_hdw_to_hdw st retstart_lbl in344 let f_save ≝ λst. λret. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware st, hardware ret〉) start_lbl in 348 345 let saves ≝ map2 ? ? ? f_save commonl commonr ? in 349 346 match reduce_strong ? ? ret_regs RegisterSTS with … … 351 348 let commonl ≝ \fst (\fst crl) in 352 349 let commonr ≝ \fst (\snd crl) in 353 let f_restore ≝ λr. λst. ertl_st_get_hdw r ststart_lbl in350 let f_restore ≝ λr. λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈pseudo r, hardware st〉) start_lbl in 354 351 let restores ≝ map2 ? ? ? f_restore commonl commonr ? in 355 adds_graph (saves @ restores) start_lbl 356 ] 357 ]. 358 [ normalize nodelta; @second_crl_proof 359  @first_crl_proof 360 ] 352 adds_graph … (saves @ restores) start_lbl]]. 353 [@second_crl_proof  @first_crl_proof] 361 354 qed. 362 355 363 356 definition translate_call_id ≝ 364 λ f.357 λglobals,f. 365 358 λargs. 366 359 λret_regs. … … 369 362 λdef. 370 363 let nb_args ≝ args in 371 add_translates (372 set_params args @ [373 adds_graph [ ertl_st_call_id f nb_argsstart_lbl ];374 fetch_result ret_regs364 add_translates globals ( 365 set_params … args @ [ 366 adds_graph … [ joint_st_sequential … (joint_instr_call_id … f nb_args) start_lbl ]; 367 fetch_result … ret_regs 375 368 ] 376 369 ) start_lbl dest_lbl def. 377 370 378 371 definition translate_stmt ≝ 372 λglobals. 379 373 λlbl. 380 374 λstmt. 381 375 λdef. 382 376 match stmt with 383 [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def384  rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def385  rtl_st_addr r1 r2 x lbl' ⇒ add_graph lbl (ertl_st_addr r1 r2 x lbl') def377 [ rtl_st_skip lbl' ⇒ add_graph … lbl (ertl_st_skip lbl') def 378  rtl_st_cost cost_lbl lbl' ⇒ add_graph … lbl (ertl_st_cost cost_lbl lbl') def 379  rtl_st_addr r1 r2 x lbl' ⇒ add_graph … lbl (ertl_st_addr r1 r2 x lbl') def 386 380  rtl_st_stack_addr r1 r2 lbl' ⇒ 387 adds_graph [381 adds_graph … [ 388 382 ertl_st_get_hdw r1 RegisterSPL lbl; 389 383 ertl_st_get_hdw r2 RegisterSPH lbl 390 384 ] lbl lbl' def 391  rtl_st_int r i lbl' ⇒ add_graph lbl (ertl_st_int r i lbl') def392  rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def385  rtl_st_int r i lbl' ⇒ add_graph … lbl (ertl_st_int r i lbl') def 386  rtl_st_move r1 r2 lbl' ⇒ add_graph … lbl (ertl_st_move r1 r2 lbl') def 393 387  rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒ 394 add_graph lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def 395 (* XXX: change from o'caml 396 adds_graph [ 397 ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl; 398 ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl 399 ] lbl lbl' def 400 *) 388 add_graph … lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def 401 389  rtl_st_op1 op1 destr srcr lbl' ⇒ 402 add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def390 add_graph … lbl (ertl_st_op1 op1 destr srcr lbl') def 403 391  rtl_st_op2 op2 destr srcr1 srcr2 lbl' ⇒ 404 add_graph lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def392 add_graph … lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def 405 393  rtl_st_clear_carry lbl' ⇒ 406 add_graph lbl (ertl_st_clear_carry lbl') def394 add_graph … lbl (ertl_st_clear_carry lbl') def 407 395  rtl_st_set_carry lbl' ⇒ 408 add_graph lbl (ertl_st_set_carry lbl') def396 add_graph … lbl (ertl_st_set_carry lbl') def 409 397  rtl_st_load destr addr1 addr2 lbl' ⇒ 410 add_graph lbl (ertl_st_load destr addr1 addr2 lbl') def398 add_graph … lbl (ertl_st_load destr addr1 addr2 lbl') def 411 399  rtl_st_store addr1 addr2 srcr lbl' ⇒ 412 add_graph lbl (ertl_st_store addr1 addr2 srcr lbl') def400 add_graph … lbl (ertl_st_store addr1 addr2 srcr lbl') def 413 401  rtl_st_call_id f args ret_regs lbl' ⇒ 414 translate_call_id f args ret_regs lbl lbl' def402 translate_call_id … f args ret_regs lbl lbl' def 415 403  rtl_st_cond srcr lbl_true lbl_false ⇒ 416 add_graph lbl (ertl_st_cond srcr lbl_true lbl_false) def404 add_graph … lbl (ertl_st_cond srcr lbl_true lbl_false) def 417 405  rtl_st_return ⇒ 418 add_graph lbl ertl_st_return def406 add_graph … lbl ertl_st_return def 419 407  _ ⇒ ? (* assert false: not implemented or should not happen *) 420 408 ].
Note: See TracChangeset
for help on using the changeset viewer.