Changeset 1206
 Timestamp:
 Sep 12, 2011, 4:20:57 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r1194 r1206 544 544 axiom FIXME : String. 545 545 546 let rec translate_statement (vars:var_types) (tmp:ident) (tmpp:ident) (s:statement) on s : res stmt ≝ 546 record tmpgen : Type[0] ≝ { 547 tmp_universe : universe SymbolTag; 548 tmp_env : list (ident × typ) 549 }. 550 551 definition alloc_tmp : memory_chunk → tmpgen → ident × tmpgen ≝ 552 λc,g. 553 let 〈tmp,u〉 ≝ fresh ? (tmp_universe g) in 554 〈tmp, mk_tmpgen u (〈tmp, typ_of_memory_chunk c〉::(tmp_env g))〉. 555 556 let rec translate_statement (vars:var_types) (u:tmpgen) (s:statement) on s : res (stmt×tmpgen) ≝ 547 557 match s with 548 [ Sskip ⇒ OK ? St_skip549  Sassign e1 e2 ⇒ translate_assign vars e1 e2558 [ Sskip ⇒ OK ? 〈St_skip, u〉 559  Sassign e1 e2 ⇒ do s' ← translate_assign vars e1 e2; OK ? 〈s',u〉 550 560  Scall ret ef args ⇒ 551 561 do ef' ← translate_expr vars ef; … … 553 563 do args' ← mmap … (translate_expr_sigma vars) args; 554 564 match ret with 555 [ None ⇒ OK ? (St_call (None ?) ef' args')565 [ None ⇒ OK ? 〈St_call (None ?) ef' args', u〉 556 566  Some e1 ⇒ 557 567 do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *) 558 568 match dest with 559 [ IdDest id ⇒ OK ? (St_call (Some ? id) ef' args')569 [ IdDest id ⇒ OK ? 〈St_call (Some ? id) ef' args', u〉 560 570  MemDest r q e1' ⇒ 561 let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp  _ ⇒ tmp ]in562 OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)))571 let 〈tmp, u〉 ≝ alloc_tmp q u in 572 OK ? 〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉 563 573 ] 564 574 ] 565 575  Ssequence s1 s2 ⇒ 566 do s1' ← translate_statement vars tmp tmpps1;567 do s2' ← translate_statement vars tmp tmpps2;568 OK ? (St_seq s1' s2')576 do 〈s1', u〉 ← translate_statement vars u s1; 577 do 〈s2', u〉 ← translate_statement vars u s2; 578 OK ? 〈St_seq s1' s2', u〉 569 579  Sifthenelse e1 s1 s2 ⇒ 570 580 do e1' ← translate_expr vars e1; 571 581 match typ_of_type (typeof e1) return λx.CMexpr x → ? with 572 582 [ ASTint _ _ ⇒ λe1'. 573 do s1' ← translate_statement vars tmp tmpps1;574 do s2' ← translate_statement vars tmp tmpps2;575 OK ? (St_ifthenelse ?? e1' s1' s2')583 do 〈s1', u〉 ← translate_statement vars u s1; 584 do 〈s2', u〉 ← translate_statement vars u s2; 585 OK ? 〈St_ifthenelse ?? e1' s1' s2', u〉 576 586  _ ⇒ λ_.Error ? (msg TypeMismatch) 577 587 ] e1' … … 580 590 match typ_of_type (typeof e1) return λx.CMexpr x → ? with 581 591 [ ASTint _ _ ⇒ λe1'. 582 do s1' ← translate_statement vars tmp tmpps1;592 do 〈s1', u〉 ← translate_statement vars u s1; 583 593 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 584 OK ? (St_block594 OK ? 〈St_block 585 595 (St_loop 586 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))) )596 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉 587 597  _ ⇒ λ_.Error ? (msg TypeMismatch) 588 598 ] e1' … … 591 601 match typ_of_type (typeof e1) return λx.CMexpr x → ? with 592 602 [ ASTint _ _ ⇒ λe1'. 593 do s1' ← translate_statement vars tmp tmpps1;603 do 〈s1',u〉 ← translate_statement vars u s1; 594 604 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 595 OK ? (St_block605 OK ? 〈St_block 596 606 (St_loop 597 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))) )607 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉 598 608  _ ⇒ λ_.Error ? (msg TypeMismatch) 599 609 ] e1' … … 602 612 match typ_of_type (typeof e1) return λx.CMexpr x → ? with 603 613 [ ASTint _ _ ⇒ λe1'. 604 do s1' ← translate_statement vars tmp tmpps1;605 do s2' ← translate_statement vars tmp tmpps2;606 do s3' ← translate_statement vars tmp tmpps3;614 do 〈s1', u〉 ← translate_statement vars u s1; 615 do 〈s2', u〉 ← translate_statement vars u s2; 616 do 〈s3', u〉 ← translate_statement vars u s3; 607 617 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 608 OK ? (St_seq s1'618 OK ? 〈St_seq s1' 609 619 (St_block 610 620 (St_loop 611 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))) )621 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉 612 622  _ ⇒ λ_.Error ? (msg TypeMismatch) 613 623 ] e1' 614  Sbreak ⇒ OK ? (St_exit 1)615  Scontinue ⇒ OK ? (St_exit 0)624  Sbreak ⇒ OK ? 〈St_exit 1, u〉 625  Scontinue ⇒ OK ? 〈St_exit 0, u〉 616 626  Sreturn ret ⇒ 617 627 match ret with 618 [ None ⇒ OK ? (St_return (None ?))628 [ None ⇒ OK ? 〈St_return (None ?), u〉 619 629  Some e1 ⇒ 620 630 do e1' ← translate_expr vars e1; 621 OK ? (St_return (Some ? (dp … e1')))631 OK ? 〈St_return (Some ? (dp … e1')), u〉 622 632 ] 623 633  Sswitch e1 ls ⇒ Error ? (msg FIXME) 624 634  Slabel l s1 ⇒ 625 do s1' ← translate_statement vars tmp tmpps1;626 OK ? (St_label l s1')627  Sgoto l ⇒ OK ? (St_goto l)635 do 〈s1', u〉 ← translate_statement vars u s1; 636 OK ? 〈St_label l s1', u〉 637  Sgoto l ⇒ OK ? 〈St_goto l, u〉 628 638  Scost l s1 ⇒ 629 do s1' ← translate_statement vars tmp tmpps1;630 OK ? (St_cost l s1')639 do 〈s1', u〉 ← translate_statement vars u s1; 640 OK ? 〈St_cost l s1', u〉 631 641 ]. 632 642 … … 650 660 ]) (OK ? s) params. 651 661 652 definition big id1 ≝ an_identifierSymbolTag [[662 definition bigu ≝ mk_universe SymbolTag [[ 653 663 false;true;false;false; 654 664 false;false;false;false; 655 665 false;false;false;false; 656 false;false;false;false]]. 657 definition bigid2 ≝ an_identifier SymbolTag [[ 658 false;true;false;false; 659 false;false;false;false; 660 false;false;false;false; 661 false;false;false;true]]. 662 663 (* FIXME: the temporary handling is nonsense, I'm afraid. *) 666 false;false;false;false]] false. 667 668 (* FIXME: the temporary handling is a bit dodgy, I'm afraid. *) 664 669 definition translate_function : list (ident×region) → function → res internal_function ≝ 665 670 λglobals, f. 666 671 let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in 667 let tmp ≝ bigid1 in (* FIXME *) 668 let tmpp ≝ bigid2 in (* FIXME *) 669 do s ← translate_statement vartypes tmp tmpp (fn_body f); 672 let tmp ≝ mk_tmpgen bigu [ ] in (* FIXME *) 673 do 〈s,tmp〉 ← translate_statement vartypes tmp (fn_body f); 670 674 do s ← alloc_params vartypes (fn_params f) s; 671 675 OK ? (mk_internal_function 672 676 (opttyp_of_type (fn_return f)) 673 677 (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f)) 674 ( 〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))678 ((tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f))) 675 679 stacksize 676 680 s).
Note: See TracChangeset
for help on using the changeset viewer.