Changeset 1060
 Timestamp:
 Jul 8, 2011, 12:17:14 PM (9 years ago)
 Location:
 src
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/I8051.ma
r777 r1060 15 15 inductive OpAccs: Type[0] ≝ 16 16 Mul: OpAccs 17  Divu: OpAccs 18  Modu: OpAccs. 17  DivuModu: OpAccs. 19 18 20 19 inductive Op1: Type[0] ≝ 
src/ASM/Util.ma
r1059 r1060 12 12 with precedence 10 13 13 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. 14 15 let rec nth_safe 16 (elt_type: Type[0]) (index: nat) (the_list: list elt_type) 17 (proof: index <  the_list ) 18 on index ≝ 19 match index return λs. s <  the_list  → elt_type with 20 [ O ⇒ 21 match the_list return λt. 0 <  t  → elt_type with 22 [ nil ⇒ λnil_absurd. ? 23  cons hd tl ⇒ λcons_proof. hd 24 ] 25  S index' ⇒ 26 match the_list return λt. S index' <  t  → elt_type with 27 [ nil ⇒ λnil_absurd. ? 28  cons hd tl ⇒ 29 λcons_proof. nth_safe elt_type index' tl ? 30 ] 31 ] proof. 32 [ normalize in nil_absurd; 33 cases (not_le_Sn_O 0) 34 #ABSURD 35 elim (ABSURD nil_absurd) 36  normalize in nil_absurd; 37 cases (not_le_Sn_O (S index')) 38 #ABSURD 39 elim (ABSURD nil_absurd) 40  normalize in cons_proof 41 @le_S_S_to_le 42 assumption 43 ] 44 qed. 45 46 definition last_safe ≝ 47 λelt_type: Type[0]. 48 λthe_list: list elt_type. 49 λproof : 0 <  the_list . 50 nth_safe elt_type (the_list  1) the_list ?. 51 normalize /2/ 52 qed. 14 53 15 54 let rec reduce … … 28 67 ]. 29 68 69 axiom reduce_strong: 70 ∀A: Type[0]. 71 ∀left: list A. 72 ∀right: list A. 73 Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret) . 74 30 75 (* 31 76 let rec reduce_strong … … 34 79 [ nil ⇒ 35 80 match right return λy.  [ ]  =  y  → Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  with 36 [ nil ⇒ λnil_nil_prf. dp ? 〈〈[ ], [ ]〉, 〈[ ], [ ]〉〉?37  cons hd tl ⇒ λnil_cons_a srd_prf. ?81 [ nil ⇒ λnil_nil_prf. ? 82  cons hd tl ⇒ λnil_cons_absrd_prf. ? 38 83 ] 39 84  cons hd tl ⇒ 40 85 match right return λy.  hd::tl  =  y  → Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  with 41 86 [ nil ⇒ λcons_nil_absrd_prf. ? 42  cons hd' tl' ⇒ λcons_cons_prf. ? 87  cons hd' tl' ⇒ λcons_cons_prf. 88 let tail_call ≝ reduce_strong A tl tl' ? in ? 43 89 ] 44 90 ] prf. 45 *) 46 91 [ 5: normalize in cons_cons_prf; 92 destruct(cons_cons_prf) 93 assumption 94  2: normalize in nil_cons_absrd_prf; 95 destruct(nil_cons_absrd_prf) 96  3: normalize in cons_nil_absrd_prf; 97 destruct(cons_nil_absrd_prf) 98 ] 99 qed. 100 *) 101 47 102 axiom reduce_length: 48 103 ∀A: Type[0]. 
src/RTL/RTL.ma
r878 r1060 4 4 include "common/Graphs.ma". 5 5 include "common/CostLabel.ma". 6 include "ASM/I8051.ma".7 6 8 7 definition registers ≝ list register. … … 15 14  rtl_st_int: register → Byte → label → rtl_statement 16 15  rtl_st_move: register → register → label → rtl_statement 17  rtl_st_opaccs: OpAccs→ register → register → register → label → rtl_statement18  rtl_st_op1: Op1 → register → register → label → rtl_statement19  rtl_st_op2: Op2 → register → register → register → label → rtl_statement16  rtl_st_opaccs: inter → register → register → register → register → label → rtl_statement 17  rtl_st_op1: intermediate_op1 → register → register → label → rtl_statement 18  rtl_st_op2: intermediate_op2 → register → register → register → label → rtl_statement 20 19  rtl_st_clear_carry: label → rtl_statement 21 20  rtl_st_load: register → register → register → label → rtl_statement … … 26 25  rtl_st_tailcall_ptr: register → register → registers → rtl_statement 27 26  rtl_st_cond_acc: register → label → label → rtl_statement 27  rtl_st_set_carry: label → rtl_statement 28  rtl_st_clear_carry: label → rtl_statement 28 29  rtl_st_return: registers → rtl_statement. 29 30 … … 44 45 }. 45 46 46 47 47 inductive rtl_function_definition: Type[0] ≝ 48 48  rtl_f_internal: rtl_internal_function → rtl_function_definition 
src/RTLabs/RTLAbstoRTL.ma
r1059 r1060 3 3 include "common/AssocList.ma". 4 4 include "common/Graphs.ma". 5 include "common/Maps.ma".6 5 (* include "common/IntValue.ma". *) 7 6 include "common/FrontEndOps.ma". … … 227 226  rtl_st_int r i _ ⇒ rtl_st_int r i lbl 228 227  rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl 229  rtl_st_opaccs opaccs d s1 s2 _ ⇒ rtl_st_opaccs opaccs d s1 s2lbl228  rtl_st_opaccs opaccs d s1 s2 s3 _ ⇒ rtl_st_opaccs opaccs d s1 s2 s3 lbl 230 229  rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl 231 230  rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl … … 238 237  rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a 239 238  rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2 239  rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl 240  rtl_st_set_carry l ⇒ rtl_st_set_carry lbl 240 241  rtl_st_return r ⇒ rtl_st_return r 241 242 ]. … … 299 300 λsrcrs: list register. 300 301 λstart_lbl: label. 302 match reduce_strong register destrs srcrs with 303 [ dp crl_crr len_proof ⇒ 304 let commonl ≝ \fst (\fst crl_crr) in 305 let commonr ≝ \fst (\snd crl_crr) in 306 let restl ≝ \snd (\fst crl_crr) in 307 let restr ≝ \snd (\snd crl_crr) in 308 let f_common ≝ translate_move_internal start_lbl in 309 let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in 310 let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *) 311 add_translates [ translate1 ; translate2 ] start_lbl 312 ]. 313 @len_proof 314 qed. 315 316 let rec make 317 (A: Type[0]) (elt: A) (n: nat) on n ≝ 318 match n with 319 [ O ⇒ [ ] 320  S n' ⇒ elt :: make A elt n' 321 ]. 322 323 lemma make_length: 324 ∀A: Type[0]. 325 ∀elt: A. 326 ∀n: nat. 327 n = length ? (make A elt n). 328 #A #ELT #N 329 elim N 330 [ normalize % 331  #N #IH 332 normalize <IH % 333 ] 334 qed. 335 336 definition translate_cast_unsigned ≝ 337 λdestrs. 338 λstart_lbl. 339 λdest_lbl. 340 λdef. 341 let 〈def, tmp_zero〉 ≝ fresh_reg def in 342 let zeros ≝ make ? tmp_zero (length ? destrs) in 343 add_translates [ 344 adds_graph [ 345 rtl_st_int tmp_zero (bitvector_of_nat ? 0) start_lbl 346 ]; 347 translate_move destrs zeros 348 ] start_lbl dest_lbl def. 349 350 definition translate_cast_signed ≝ 351 λdestrs. 352 λsrcr. 353 λstart_lbl. 354 λdest_lbl. 355 λdef. 356 let 〈def, tmp_128〉 ≝ fresh_reg def in 357 let 〈def, tmp_255〉 ≝ fresh_reg def in 358 let 〈def, tmpr〉 ≝ fresh_reg def in 359 let 〈def, dummy〉 ≝ fresh_reg def in 360 let insts ≝ [ 361 rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl; 362 rtl_st_op2 And tmpr tmp_128 srcr start_lbl; 363 rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl; 364 rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl; 365 rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl 366 ] in 367 let srcrs ≝ make ? tmpr (length ? destrs) in 368 add_translates [ 369 adds_graph insts; 370 translate_move destrs srcrs 371 ] start_lbl dest_lbl def. 372 373 definition translate_cast ≝ 374 λsrc_size. 375 λsrc_sign. 376 λdest_size. 377 λdestrs. 378 λsrcrs. 379 match  srcrs  return λx.  srcrs  = x → ? with 380 [ O ⇒ λzero_prf. adds_graph [ ] 381  S n' ⇒ λsucc_prf. 382 if ltb dest_size src_size then 383 translate_move destrs srcrs 384 else 385 match reduce_strong ? destrs srcrs with 386 [ dp crl len_proof ⇒ 387 let commonl ≝ \fst (\fst crl) in 388 let commonr ≝ \fst (\snd crl) in 389 let restl ≝ \snd (\fst crl) in 390 let restr ≝ \snd (\snd crl) in 391 let insts_common ≝ translate_move commonl commonr in 392 let sign_reg ≝ last_safe ? srcrs ? in 393 let insts_sign ≝ 394 match src_sign with 395 [ Unsigned ⇒ translate_cast_unsigned restl 396  Signed ⇒ translate_cast_signed restl sign_reg 397 ] 398 in 399 add_translates [ insts_common; insts_sign ] 400 ] 401 ] (refl ? (srcrs)). 402 >succ_prf // 403 qed. 404 405 definition translate_negint ≝ 406 λdestrs. 407 λsrcrs. 408 λstart_lbl. 409 λdest_lbl. 410 λdef. 411 λprf:  destrs  =  srcrs . (* assert in caml code *) 412 let 〈def, tmpr〉 ≝ fresh_reg def in 413 let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in 414 let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in 415 let insts_init ≝ [ 416 rtl_st_set_carry start_lbl; 417 rtl_st_int tmpr (zero ?) start_lbl 418 ] in 419 let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in 420 let insts_add ≝ map … f_add destrs in 421 adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def. 422 423 definition translate_notbool ≝ 424 λdestrs. 425 λsrcrs. 426 λstart_lbl. 427 λdest_lbl. 428 λdef. 429 match destrs with 430 [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def 431  cons destr destrs ⇒ 432 let 〈def, tmpr〉 ≝ fresh_reg def in 433 let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in 434 let save_srcrs ≝ translate_move tmp_srcrs srcrs in 435 let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in 436 let f ≝ λtmp_srcr. [ 437 rtl_st_clear_carry start_lbl; 438 rtl_st_int tmpr (zero ?) start_lbl; 439 rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl; 440 rtl_st_int tmpr (zero ?) start_lbl; 441 rtl_st_op2 Addc tmpr tmpr tmpr start_lbl; 442 rtl_st_op2 Xor destr destr tmpr start_lbl 443 ] in 444 let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in 445 let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in 446 add_translates [ 447 save_srcrs; adds_graph insts; epilogue 448 ] start_lbl dest_lbl def 449 ]. 450 451 definition translate_intermediate_op1 ≝ 452 λop1. 453 λdestrs. 454 λsrcrs. 455 λstart_lbl. 456 λdest_lbl. 457 λdef. 301 458 λprf:  destrs  =  srcrs . 302 let 〈crl, crr〉 ≝ reduce register destrs srcrs in 303 let 〈commonl, restl〉 ≝ crl in 304 let 〈commonr, restr〉 ≝ crr in 305 let f_common ≝ translate_move_internal start_lbl in 306 let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in 307 let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *) 308 add_translates [ translate1 ; translate2 ] start_lbl. 309 310 let rec translate_move destrs srcrs start_lbl = 311 let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in 312 let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in 313 let translates1 = adds_graph (List.map2 f_common common1 common2) in 314 let translates2 = translate_cst (AST.Cst_int 0) rest1 in 315 add_translates [translates1 ; translates2] start_lbl 459 match op1 with 460 [ intermediate_op1_cast src_size src_sign dest_size ⇒ 461 translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def 462  intermediate_op1_negint ⇒ 463 translate_negint destrs srcrs start_lbl dest_lbl def prf 464  intermediate_op1_notbool ⇒ 465 translate_notbool destrs srcrs start_lbl dest_lbl def 466  intermediate_op1_notint ⇒ 467 let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in 468 let l ≝ map2 … f destrs srcrs prf in 469 adds_graph l start_lbl dest_lbl def 470  intermediate_op1_ptrofint ⇒ 471 translate_move destrs srcrs start_lbl dest_lbl def 472  intermediate_op1_intofptr ⇒ 473 translate_move destrs srcrs start_lbl dest_lbl def 474  intermediate_op1_id ⇒ 475 translate_move destrs srcrs start_lbl dest_lbl def 476 ]. 316 477 317 478 definition filter_and_to_list_local_env_internal ≝ 
src/common/AST.ma
r1059 r1060 56 56 *) 57 57 58 58 59 (* Memory spaces *) 59 60 … … 102 103  I16: intsize 103 104  I32: intsize. 105 106 (* unary operations used in the backend intermediate languages, there's also a separate 107 type for unary operations at the assembly level in ASM/I8051.ma *) 108 inductive intermediate_op1: Type[0] ≝ 109  intermediate_op1_cast: nat → signedness → nat → intermediate_op1 (**r size in bytes, signedness, to size *) 110  intermediate_op1_negint: intermediate_op1 (**r integer opposite *) 111  intermediate_op1_notbool: intermediate_op1 (**r boolean negation *) 112  intermediate_op1_notint: intermediate_op1 (**r bitwise complement *) 113  intermediate_op1_id: intermediate_op1 (**r identity *) 114  intermediate_op1_ptrofint: intermediate_op1 (**r int to pointer *) 115  intermediate_op1_intofptr: intermediate_op1. (**r pointer to int *) 104 116 105 117 (* * Float types come in two sizes: 32 bits (single precision)
Note: See TracChangeset
for help on using the changeset viewer.