Changeset 1871 for src/Clight
 Timestamp:
 Apr 4, 2012, 1:40:30 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r1631 r1871 1 2 1 include "Clight/Csyntax.ma". 3 2 include "Clight/TypeComparison.ma". … … 6 5 7 6 (* Identify local variables that must be allocated memory. *) 8 7 (* These are the variables whose addresses are taken. *) 9 8 let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝ 10 9 match e with … … 77 76 ]. 78 77 78 (* Defines where a variable should be allocated. *) 79 79 inductive var_type : Type[0] ≝ 80  Global : region → var_type 81  Stack : nat → var_type 82  Local : var_type 80  Global : region → var_type (* A global, allocated statically in a given region (which one ???) *) 81  Stack : nat → var_type (* On the stack, at a given height *) 82  Local : var_type (* Locally (hopefully, in a register) *) 83 83 . 84 84 85 (* A map associating each variable identifier to its allocation mode and its type. *) 85 86 definition var_types ≝ identifier_map SymbolTag (var_type × type). 86 87 … … 99 100 *) 100 101 102 (* Some kind of data is never allocated in registers, even if it fits, typically structured data. *) 101 103 definition always_alloc : type → bool ≝ 102 104 λt. match t with … … 107 109 ]. 108 110 111 (* This builds a [var_types] map characterizing the allocation mode, of variables, 112 * and it returns a stack usage for the function (in bytes, according to [sizeof]) *) 109 113 definition characterise_vars : list (ident×region×type) → function → var_types × nat ≝ 110 114 λglobals, f. 115 (* globals are added into a map, with var_type Global, region π_2(idrt) and type π_3(idrt) *) 111 116 let m ≝ foldr ?? (λidrt,m. add ?? m (\fst (\fst idrt)) 〈Global (\snd (\fst idrt)), \snd idrt〉) (empty_map ??) globals in 117 (* variables in the body of the function are gathered in [mem_vars] *) 112 118 let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in 119 (* iterate on the parameters and local variables of the function, with a tuple (map, stack_high) as an accumulator *) 113 120 let 〈m,stacksize〉 ≝ foldr ?? (λv,ms. 114 let 〈m,stack_high〉 ≝ ms in 115 let 〈id,ty〉 ≝ v in 116 let 〈c,stack_high〉 ≝ if always_alloc ty ∨ mem_set ? mem_vars id 117 then 〈Stack stack_high,stack_high + sizeof ty〉 118 else 〈Local, stack_high〉 in 121 let 〈m,stack_high〉 ≝ ms in 122 let 〈id,ty〉 ≝ v in 123 let 〈c,stack_high〉 ≝ 124 (* if the (local, parameter) variable is of a compound type OR if its adress is taken, we allocate it on the stack. *) 125 if always_alloc ty ∨ mem_set ? mem_vars id then 126 〈Stack stack_high,stack_high + sizeof ty〉 127 else 128 〈Local, stack_high〉 129 in 119 130 〈add ?? m id 〈c, ty〉, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in 120 131 〈m,stacksize〉. 121 132 133 (* A local variable id' status is not modified by the removal of a global variable id : id' is still local *) 122 134 lemma local_id_add_global : ∀vars,id,r,t,id',t'. 123 135 local_id (add ?? vars id 〈Global r, t〉) id' t' → local_id vars id' t'. … … 129 141 ] qed. 130 142 143 (* If I add a variable id ≠ id', then id' is still local *) 131 144 lemma local_id_add_miss : ∀vars,id,vt,id',t'. 132 145 id ≠ id' → local_id (add ?? vars id vt) id' t' → local_id vars id' t'. … … 138 151 qed. 139 152 153 (* After characterise_vars, a variable in the resulting map is either a global or a "local"(register or stack allocated) *) 140 154 lemma characterise_vars_src : ∀gl,f,vars,n. 141 155 characterise_vars gl f = 〈vars,n〉 → 142 ∀id. present ?? vars id → 156 ∀id. present ?? vars id → 143 157 (∃r,ty. lookup' vars id = OK ? 〈Global r,ty〉 ∧ Exists ? (λx.x = 〈〈id,r〉,ty〉) gl) ∨ 144 158 ∃t.local_id vars id t. … … 181 195 ] qed. 182 196 183 197 (* A local variable in a function is either a parameter or a "local" (:=register or stack alloc'd) 198 * variable, with the right type *) 184 199 lemma characterise_vars_all : ∀l,f,vars,n. 185 200 characterise_vars l f = 〈vars,n〉 → … … 215 230 ] qed. 216 231 232 (* The map generated by characterise_vars is "correct" wrt the fresh ident generator of tag [u], 233 i.e. by generating fresh idents with u, we risk no collision with the idents in the map domain. *) 217 234 lemma characterise_vars_fresh : ∀gl,f,vars,n,u. 218 characterise_vars gl f = 〈vars,n〉 → 219 globals_fresh_for_univ ? gl u → 220 fn_fresh_for_univ f u → 221 fresh_map_for_univ … vars u. 235 characterise_vars gl f = 〈vars,n〉 → (* If we generate a map ... *) 236 globals_fresh_for_univ ? gl u → (* and the globals are out of the idents generated by u *) 237 fn_fresh_for_univ f u → (* and the variables of the function f are cool with u too ... *) 238 fresh_map_for_univ … vars u. (* then there won't be collisions between the map and idents made from u *) 222 239 #gl #f #vars #n #u #CH #GL #FN 223 240 #id #H … … 238 255 axiom MissingField : String. 239 256 240 257 (* type_should_eq enforces that two types are equal and eliminates this equality by 258 transporting P ty1 to P ty2. If ty1 != ty2, then Error *) 241 259 definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝ 242 260 λty1,ty2,P,p. 243 261 do E ← assert_type_eq ty1 ty2; 244 OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p). 245 262 OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p). 263 264 (* same gig for regions *) 246 265 definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2). 247 266 * * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) 248 267 qed. 249 268 269 (* same gig for AST typs *) 250 270 definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2). 251 271 * [ #sz1 #sg1  #r1  #sz1 ] … … 257 277 ] qed. 258 278 259 260 279 alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)". 261 280 alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)". … … 264 283 alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,3,0)". 265 284 285 (* Translates a Clight unary operation into a Cminor one, while checking 286 * that the domain and codomain types are consistent. *) 266 287 definition translate_unop : ∀t,t':typ. CLunop → res (CMunop t t') ≝ 267 288 λt,t'.λop:CLunop. … … 294 315 ]. @I qed. 295 316 317 (* Translates a Clight addition into a Cminor one. Four cases to consider : 318  integer/integer add 319  fp/fp add 320  pointer/integer 321  integer/pointer. 322 Consistency of the type is enforced by explicit checks. 323 *) 296 324 definition translate_add ≝ 297 325 λty1,e1,ty2,e2,ty'. … … 315 343  add_default ⇒ Error ? (msg TypeMismatch) 316 344 ]. 345 317 346 318 347 definition translate_sub ≝ … … 408 437 ]. 409 438 439 (* Recall that [expr_vars], defined in Cminor/Syntax.ma, asserts a predicate on 440 all the variables of a program. [translate_binop_vars], given 441 a predicate verified for all variables of subexprs e1 and e2, produces 442 a proof that all variables of [translate_binop op _ e1 _ e2 _] satisfy this 443 predicate. *) 410 444 lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e. 411 445 expr_vars ? e1 P → … … 445 479 (* We'll need to implement proper translation of pointers if we really do memory 446 480 spaces. *) 481 (* This function performs leibnizstyle subst if r1 = r2, and fails otherwise. *) 447 482 definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝ 448 483 λr1,r2,P. … … 456 491 ]. 457 492 493 (* Simple application of [check_region] to translate between terms. *) 458 494 definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝ 459 495 λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e. … … 461 497 axiom FIXME : String. 462 498 463 definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝ 499 (* Given a source and target type, translate an expession of type source to type target *) 500 definition translate_cast : ∀P. ∀ty1:type.∀ty2:type. (Σe:CMexpr (typ_of_type ty1). expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝ 464 501 λP,ty1,ty2. 465 502 match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with … … 496 533 qed. 497 534 535 (* Small inversion lemma : if the access mode of a type is by reference, then it must be a ptr type. *) 498 536 lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r. 499 537 * … … 506 544 ] qed. 507 545 546 (* Translate Clight exprs into Cminor ones. 547 Arguments : 548  vars:var_types, an environment mapping each variable to a couple (allocation mode, type) 549  e:expr, the expression to be converted 550 Result : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) 551 that is, either 552 . an error 553 . an expression e', matching the type of e, such that e' respect the property that all variables 554 in it are not global. In effect, [translate_expr] will replace global variables by constant symbols. 555 *) 508 556 let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝ 509 557 match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with … … 513 561  Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?» 514 562  Evar id ⇒ 515 do 〈c,t〉 as E ← lookup' vars id; 563 do 〈c,t〉 as E ← lookup' vars id; (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *) 516 564 match c return λx.? = ? → res (Σe':CMexpr ?. ?) with 517 [ Global r ⇒ λ_. 565 [ Global r ⇒ λ_. 566 (* We are accessing a global variable in an expression. Its Cminor counterpart also depends on 567 its access mode: 568  By_value q, where q is a memory chunk specification (whitch should match the type of the global) 569  By_reference, and we only take the adress of the variable 570  By_nothing : error 571 *) 518 572 match access_mode ty with 519 [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?» 573 [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *) 520 574  By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?» 521 575  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 522 576 ] 523 577  Stack n ⇒ λE. 578 (* We have decided that the variable should be allocated on the stack, 579 * because its adress was taken somewhere or becauste it's a structured data. *) 524 580 match access_mode ty with 525 581 [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?» … … 527 583  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 528 584 ] 585 (* This is a local variable. Keep it as an identifier in the Cminor code, ensuring that the type of the original expr and of ty match. *) 529 586  Local ⇒ λE. type_should_eq t ty (λt.Σe':CMexpr (typ_of_type t).expr_vars (typ_of_type t) e' (local_id vars)) («Id (typ_of_type t) id, ?») 530 587 ] E 531 588  Ederef e1 ⇒ 532 589 do e1' ← translate_expr vars e1; 590 (* According to the way the data pointed to by e1 is accessed, the generated Cminor code will vary. 591  if e1 is a kind of int* ptr, then we load ("Mem") the ptr returned by e1 592  if e1 is a struct* or a function ptr, then we acess by reference, in which case we : 593 1) check the consistency of the regions in the type of e1 and in the access mode of its type 594 2) return directly the converted CMinor expression "as is" (TODO : what is the strange notation with the ceil function and the mapsto ?) 595 *) 533 596 match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with 534 597 [ ASTptr r ⇒ λe1'. … … 634 697 typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e' 635 698 ] 636 ] and translate_addr (vars:var_types) (e:expr) on e : res (𝚺r. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝ 699 ] 700 701 (* Translate addr takes an expression e1, and returns a Cminor code computing the address of the result of [e1]. *) 702 and translate_addr (vars:var_types) (e:expr) on e : res (𝚺r. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝ 637 703 match e with 638 704 [ Expr ed _ ⇒ … … 685 751  MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars. 686 752 753 (* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a 754 /Clight/ expression, not converted by translate_expr. We thus have to do part of the work 755 of [translate_expr] in this function. [translate_dest] will convert e1 756 into a proper destination for an assignement operation. We proceed by case analysis on e1. 757  if e1 is a variable [id], then we proceed by case analysis on its allocation mode: 758  if [id] is allocated locally (in a register), then id becomes directly 759 the target for the assignement, as (IdDest vars id t H), where t is the type 760 of id, and H asserts that id is indeed a local variable. 761  if [id] is a global variable stored in region [r], then we perform [translate_expr]'s 762 job and return an adress, given as a constant symbol corresponding to [id], with 763 region r and memory chunk specified by the access mode of the rhs type ty2 of [e2]. 764  same thing for stackallocated variables, except that we don't specify any region. 765  if e1 is not a variable, we use [translate_addr] to generate a Cminor expression computing 766 the adres of e1 767 *) 687 768 definition translate_dest ≝ 688 769 λvars,e1,ty2. … … 710 791 qed. 711 792 793 (* [lenv] is the type of maps from Clight labels to Cminor labels. *) 712 794 definition lenv ≝ identifier_map SymbolTag (identifier Label). 713 795 714 796 axiom MissingLabel : String. 715 797 798 (* Find the Cminor label corresponding to [l] or fail. *) 716 799 definition lookup_label ≝ 717 800 λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l). 718 801 802 (* True iff the Cminor label [l] is in the codomain of [lbls] *) 719 803 definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l. 804 805 (* True iff The Clight label [l] is in the domain of [lbls] *) 806 definition label_in_domain ≝ λlbls:lenv. λl. present ?? lbls l. 807 808 let rec fresh_list_for_univ (l:list (identifier Label)) (u:universe Label) ≝ 809 match l with 810 [ nil ⇒ True 811  cons elt tl ⇒ fresh_for_univ ? elt u ∧ fresh_list_for_univ tl u]. 812 813 record labgen : Type[0] ≝ { 814 labuniverse : universe Label; 815 label_genlist : list (identifier Label); 816 genlist_is_fresh : fresh_list_for_univ label_genlist labuniverse 817 }. 818 819 lemma fresh_list_stays_fresh : ∀l,tmp,u,u'. fresh_list_for_univ l u → 〈tmp,u'〉=fresh Label u → fresh_list_for_univ l u'. 820 #l elim l 821 [ 1: normalize // 822  2: #hd #tl #Hind #tmp #u #u' #HA #HB 823 whd 824 @conj 825 [ 1: whd in HA ⊢ ?; 826 elim HA #HAleft #HAright 827 @(fresh_remains_fresh ? hd tmp u u') assumption 828  2: whd in HA ⊢ ?; 829 elim HA #HAleft #HAright 830 @Hind // 831 ] 832 ] 833 qed. 834 835 definition In ≝ λelttype.λelt.λl.Exists elttype (λx.x=elt) l. 836 837 definition generate_fresh_label : 838 ∀ul. Σlul:(identifier Label × labgen). 839 (And (∀lab. In ? lab (label_genlist ul) → In ? lab (label_genlist (snd … lul))) 840 (In ? (fst … lul) (label_genlist (snd … lul)))) ≝ 841 λul. 842 let 〈tmp,u〉 as E ≝ fresh ? (labuniverse ul) in 843 «〈tmp, mk_labgen u (tmp::(label_genlist ul)) ?〉, ?». 844 [ 1: normalize @conj 845 [ 1: @(fresh_is_fresh ? tmp u (labuniverse ul) ?) assumption 846  2: @fresh_list_stays_fresh // ] 847  @conj /2/ 848 ] 849 qed. 720 850 721 851 let rec labels_defined (s:statement) : list ident ≝ … … 739 869 definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s). 740 870 871 (* For each label l in s, there exists a matching label l' = lenv(l) defined in s' *) 741 872 definition labels_translated : lenv → statement → stmt → Prop ≝ 742 873 λlbls,s,s'. ∀l. 743 874 (Exists ? (λl'.l' = l) (labels_defined s)) → 744 ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'. 745 746 definition stmt_inv ≝ 747 λvars. λlbls:lenv. 748 stmt_P (λs.stmt_vars (local_id vars) s ∧ stmt_labels (lpresent lbls) s). 749 750 definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.∀ls. stmt_inv vars ls s) ≝ 875 ∃l'. lookup_label lbls l = (OK ? l') ∧ ldefined s' l'. 876 877 878 (* Invariant on statements, holds during conversion to Cminor *) 879 definition stmt_inv ≝ λvars. stmt_P (stmt_vars (local_id vars)). 880 881 (* I (Ilias) decided to inline the following definition, to make explicit the data constructed. 882 * This was needed to prove some stuff in translate_statement at some point, but it might be 883 * useless now. If needed, I can revert this change. *) 884 definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt. stmt_inv vars s) ≝ 751 885 λvars,e1,e2. 752 do e2' ← translate_expr vars e2; 886 do e2' ← translate_expr vars e2; 753 887 do dest ← translate_dest vars e1 (typeof e2); 754 888 match dest with … … 758 892  MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?» 759 893 ]. 760 #ls whd % 761 [ % // @pi2 762  @I 763  % @pi2 764  @I 765 ] qed. 894 % try (//) try (elim e2' //) elim e1' // 895 qed. 766 896 767 897 definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝ … … 779 909 qed. 780 910 911 (* Add the list of typed variables tmpenv to the environment [var_types] with 912 the allocation mode Local. *) 781 913 definition add_tmps : var_types → list (ident × type) → var_types ≝ 782 914 λvs,tmpenv. … … 787 919 tmp_env : list (ident × type); 788 920 tmp_ok : fresh_map_for_univ … (add_tmps vars tmp_env) tmp_universe; 789 tmp_preserved : 921 tmp_preserved : 790 922 ∀id,ty. local_id vars id ty → local_id (add_tmps vars tmp_env) id ty 791 923 }. … … 814 946 ] qed. 815 947 948 816 949 lemma lookup_label_hit : ∀lbls,l,l'. 817 950 lookup_label lbls l = OK ? l' → … … 821 954 822 955 (* TODO: is this really needed now? *) 956 823 957 definition tmps_preserved : ∀vars:var_types. tmpgen vars → tmpgen vars → Prop ≝ 824 958 λvars,u1,u2. … … 839 973 qed. 840 974 841 definition trans_inv : ∀vars:var_types. lenv → statement → tmpgen vars → (stmt×(tmpgen vars)) → Prop ≝ 842 λvars,lbls,s,u,su'. 843 let 〈s',u'〉 ≝ su' in 844 stmt_inv (add_tmps vars (tmp_env … u')) lbls s' ∧ 845 labels_translated lbls s s' ∧ 846 tmps_preserved vars u u'. 847 848 lemma trans_inv_stmt_inv : ∀vars,lbls,s,u,su. 849 trans_inv vars lbls s u su → stmt_inv (add_tmps vars (tmp_env … (\snd su))) lbls (\fst su). 850 #var #lbls #s #u * #s' #u' * * #H1 #H2 #H3 @H1 851 qed. 852 853 lemma trans_inv_labels : ∀vars,lbls,s,u,su. 854 trans_inv vars lbls s u su → labels_translated lbls s (\fst su). 855 #vars #lbls #s #u * #s' #u' * * #_ #H #_ @H 856 qed. 857 858 (* TODO: still needed? *) 859 lemma local_id_add_local_oblivious : ∀vars,id,ty,id',ty'. 860 fresh_for_map ?? id' vars → 861 local_id vars id ty → local_id (add ?? vars id' 〈Local, ty'〉) id ty. 862 #vars #id #ty #id' #ty' #F #H whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 863 cases (identifier_eq ? id id') 864 [ #E @False_ind >E in H; whd in ⊢ (% → ?); 865 whd in ⊢ (match % with [_⇒ ?_⇒ ?] → ?); cases id' in F ⊢ %; #id' 866 #F whd in F; >F * 867  #NE >lookup_add_miss [ @H  // ] 868 ] qed. 869 870 (* 871 lemma local_id_add_tmps_oblivious : ∀vars,id,ty,u. 872 local_id vars id ty → local_id (add_tmps vars (tmp_env vars u)) id ty. 873 #vars #id #ty * #u #l #F #H elim l 874 [ // 875  * #id' #ty' #tl @local_id_add_local_oblivious @F 876 ] qed. 877 *) 878 879 lemma add_tmps_oblivious : ∀vars,lbls,s,u. 880 stmt_inv vars lbls s → stmt_inv (add_tmps vars (tmp_env vars u)) lbls s. 881 #vars #lbls #s #u #H 975 lemma add_tmps_oblivious : ∀vars,s,u. 976 stmt_inv vars s → stmt_inv (add_tmps vars (tmp_env vars u)) s. 977 #vars #s #u #H 882 978 @(stmt_P_mp … H) 883 #s' * #H1 #H2 % 884 [ @(stmt_vars_mp … H1) 885 #id #t @(tmp_preserved ? u) 886  @H2 887 ] qed. 979 #s' #H1 @(stmt_vars_mp … H1) #id #t #H @(tmp_preserved ? u ?? H) 980 qed. 888 981 889 982 lemma local_id_fresh_tmp : ∀vars,tmp,u,ty,u0. … … 898 991 qed. 899 992 900 let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen vars) (s:statement) on s : res (Σsu:stmt×(tmpgen vars).trans_inv vars lbls s u su) ≝ 901 match s return λs.res (Σsu:stmt×(tmpgen vars).trans_inv vars lbls s u su) with 902 [ Sskip ⇒ OK ? «〈St_skip, u〉, ?» 993 994 let rec mklabels (ul:labgen) : (identifier Label) × (identifier Label) × labgen ≝ 995 match generate_fresh_label ul with 996 [ mk_Sig res1 H1 ⇒ 997 let 〈entry_label, ul1〉 as E1 ≝ res1 in 998 match generate_fresh_label ul1 with 999 [ mk_Sig res2 H2 ⇒ 1000 let 〈exit_label, ul2〉 as E2 ≝ res2 in 1001 〈entry_label, exit_label, ul2〉 1002 ] 1003 ]. 1004 1005 (* When converting loops into gotos, and in order to eliminate blocks, we have 1006 * to convert continues and breaks into goto's, too. We add some "flags" in 1007 * in argument to [translate_statement], meaning that the next encountered break 1008 * or continue has to be converted into a goto to some contained label. 1009 * ConvertTo l1 l2 means "convert continue to goto l1 and convert break to goto l2". 1010 *) 1011 inductive convert_flag : Type[0] ≝ 1012  DoNotConvert : convert_flag 1013  ConvertTo : identifier Label → identifier Label → convert_flag. (* continue, break *) 1014 1015 let rec labels_of_flag (flag : convert_flag) : list (identifier Label) ≝ 1016 match flag with 1017 [ DoNotConvert ⇒ [ ] 1018  ConvertTo continue break ⇒ continue :: break :: [ ] 1019 ]. 1020 1021 (* For a toplevel expression, [labelwf] collapses to "all labels are properly declared" *) 1022 definition label_wf ≝ 1023 λ (s : statement) .λ (s' : stmt) .λ (lbls : lenv). λ (flag : convert_flag). 1024 stmt_P (λs1. stmt_labels (λl.ldefined s' l ∨ lpresent lbls l ∨ In ? l (labels_of_flag flag)) s1) s'. 1025 1026 (* trans_inv is the invariant which is enforced during the translation from Clight to Cminor. 1027 The involved arguments are the following: 1028 . vars:var_types, an environment mapping variables to their types and allocation modes 1029 . lbls:lenv, a mapping from old (Clight) to fresh and new (Cminor) labels, 1030 . s:statement, a Clight statement, 1031 . uv, a fresh variable generator (containing itself some invariants) 1032 . flag, wich maps "break" and "continue" to "gotos" 1033 . su', a couple of a Cminor statement and fresh variable generator. 1034 *) 1035 definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → ((tmpgen vars) × labgen × stmt) → Prop ≝ 1036 λvars,lbls,s,uv,flag,su'. 1037 let 〈uv', ul', s'〉 ≝ su' in 1038 stmt_inv (add_tmps vars (tmp_env … uv')) s' ∧ (* remaining variables in s' are local*) 1039 labels_translated lbls s s' ∧ (* all the labels in s are transformed in label of s' using [lbls] as a map *) 1040 tmps_preserved vars uv uv' ∧ (* the variables generated are local and grows in a monotonic fashion *) 1041 label_wf s s' lbls flag. (* labels are "properly" declared, as defined in [ŀabel_wf].*) 1042 1043 let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (s:statement) on s 1044 : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) ≝ 1045 match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) with 1046 [ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?» 903 1047  Sassign e1 e2 ⇒ 904 do s' ← translate_assign vars e1 e2; 905 OK ? «〈pi1 ?? s', u〉, ?» 1048 do e2' ← translate_expr vars e2; (* rhs *) 1049 do dest ← translate_dest vars e1 (typeof e2); (* e1 *) 1050 match dest with 1051 [ IdDest id ty p ⇒ 1052 do e2' ← type_should_eq (typeof e2) ty ? e2'; 1053 OK ? «〈uv, ul, St_assign ? id e2'〉, ?» 1054  MemDest r q e1' ⇒ 1055 OK ? «〈uv, ul, St_store ? r q e1' e2'〉, ?» 1056 ] 906 1057  Scall ret ef args ⇒ 907 1058 do ef' ← translate_expr vars ef; … … 909 1060 do args' ← mmap_sigma ??? (translate_expr_sigma vars) args; 910 1061 match ret with 911 [ None ⇒ OK ? «〈 St_call (None ?) ef' args', u〉, ?»1062 [ None ⇒ OK ? «〈uv, ul, St_call (None ?) ef' args'〉, ?» 912 1063  Some e1 ⇒ 913 1064 do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *) 914 1065 match dest with 915 [ IdDest id ty p ⇒ OK ? «〈 St_call (Some ? 〈id,typ_of_type ty〉) ef' args', u〉, ?»1066 [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?» 916 1067  MemDest r q e1' ⇒ 917 let 〈tmp, u 〉 as Etmp ≝ alloc_tmp ? (typeof e1) uin918 OK ? «〈 St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r q e1' (Id ? tmp)), u〉, ?»1068 let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in 1069 OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r q e1' (Id ? tmp))〉, ?» 919 1070 ] 920 1071 ] 921 1072  Ssequence s1 s2 ⇒ 922 do «s1', u1, H1» ← translate_statement vars lbls us1;923 do «s2', u2, H2» ← translate_statement vars lbls u1s2;924 OK ? «〈 St_seq s1' s2', u2〉, ?»1073 do «fgens1, s1', H1» ← translate_statement vars uv ul «lbls,?» flag s1; 1074 do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) «lbls,?» flag s2; 1075 OK ? «〈fgens2, St_seq s1' s2'〉, ?» 925 1076  Sifthenelse e1 s1 s2 ⇒ 926 1077 do e1' ← translate_expr vars e1; 927 1078 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 928 1079 [ ASTint _ _ ⇒ λe1'. 929 do « s1', u, H1» ← translate_statement vars lbls us1;930 do « s2', u, H2» ← translate_statement vars lbls us2;931 OK ? «〈 St_ifthenelse ?? e1' s1' s2', u〉, ?»1080 do «fgens1, s1', H1» ← translate_statement vars uv ul «lbls,?» flag s1; 1081 do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) «lbls,?» flag s2; 1082 OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?» 932 1083  _ ⇒ λ_.Error ? (msg TypeMismatch) 933 1084 ] e1' … … 935 1086 do e1' ← translate_expr vars e1; 936 1087 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 937 [ ASTint _ _ ⇒ λe1'. 938 do «s1', u, H1» ← translate_statement vars lbls u s1; 939 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 940 OK ? «〈St_block 941 (St_loop 942 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉, ?» 1088 [ ASTint _ _ ⇒ λe1'. 1089 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 1090 match mklabels ul with 1091 [ mk_Sig result Hmklabels => 1092 let 〈labels, ul1〉 as E1 ≝ result in 1093 let 〈entry, exit〉 as E2 ≝ labels in 1094 do «fgens2, s1',H1» ← translate_statement vars uv ul1 «lbls,?» (ConvertTo entry exit) s1; 1095 let converted_loop ≝ 1096 St_label entry 1097 (St_seq 1098 (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip) 1099 (St_label exit St_skip)) 1100 in 1101 OK ? «〈fgens2, converted_loop〉, ?» 1102 ] 943 1103  _ ⇒ λ_.Error ? (msg TypeMismatch) 944 1104 ] e1' … … 947 1107 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with 948 1108 [ ASTint _ _ ⇒ λe1'. 949 do «s1',u, H1» ← translate_statement vars lbls u s1; 950 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 951 OK ? «〈St_block 952 (St_loop 953 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉, ?» 1109 match mklabels ul with 1110 [ mk_Sig result Hmklabels ⇒ 1111 let 〈labels, ul1〉 as E1 ≝ result in 1112 let 〈entry, exit〉 as E2 ≝ labels in 1113 do «fgens2, s1', H1» ← translate_statement vars uv ul1 «lbls,?» (ConvertTo entry exit) s1; 1114 let converted_loop ≝ 1115 St_label entry 1116 (St_seq 1117 (St_seq 1118 s1' 1119 (St_ifthenelse ?? e1' (St_goto entry) St_skip) 1120 ) 1121 (St_label exit St_skip)) 1122 in 1123 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 1124 OK ? «〈fgens2, converted_loop〉, ?» 1125 ] 954 1126  _ ⇒ λ_.Error ? (msg TypeMismatch) 955 1127 ] e1' … … 958 1130 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with 959 1131 [ ASTint _ _ ⇒ λe1'. 960 do «s1', u, H1» ← translate_statement vars lbls u s1; 961 do «s2', u, H2» ← translate_statement vars lbls u s2; 962 do «s3', u, H3» ← translate_statement vars lbls u s3; 963 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 964 OK ? «〈St_seq s1' 965 (St_block 966 (St_loop 967 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉, ?» 1132 match mklabels ul with 1133 [ mk_Sig result Hmklabels ⇒ 1134 let 〈labels, ul1〉 as E ≝ result in 1135 let 〈entry, exit〉 as E2 ≝ labels in 1136 do «fgens2, s1', H1» ← translate_statement vars uv ul1 «lbls,?» flag s1; 1137 do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) «lbls, ?» (ConvertTo entry exit) s2; 1138 do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) «lbls, ?» (ConvertTo entry exit) s3; 1139 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 1140 let converted_loop ≝ 1141 St_seq 1142 s1' 1143 (St_label entry 1144 (St_seq 1145 (St_ifthenelse ?? e1' (St_seq s3' (St_seq s2' (St_goto entry))) St_skip) 1146 (St_label exit St_skip) 1147 )) 1148 in 1149 OK ? «〈fgens4, converted_loop〉, ?» 1150 ] 968 1151  _ ⇒ λ_.Error ? (msg TypeMismatch) 969 1152 ] e1' 970  Sbreak ⇒ OK ? «〈St_exit 1, u〉, ?» 971  Scontinue ⇒ OK ? «〈St_exit 0, u〉, ?» 1153  Sbreak ⇒ 1154 match flag return λf.flag = f → ? with 1155 [ DoNotConvert ⇒ λEflag. 1156 Error ? (msg FIXME) 1157  ConvertTo continue_label break_label ⇒ λEflag. 1158 OK ? «〈uv, ul, St_goto break_label〉, ?» 1159 ] (refl ? flag) 1160  Scontinue ⇒ 1161 match flag return λf.flag = f → ? with 1162 [ DoNotConvert ⇒ λEflag. 1163 Error ? (msg FIXME) 1164  ConvertTo continue_label break_label ⇒ λEflag. 1165 OK ? «〈uv, ul, St_goto continue_label〉, ?» 1166 ] (refl ? flag) 972 1167  Sreturn ret ⇒ 973 1168 match ret with 974 [ None ⇒ OK ? «〈 St_return (None ?), u〉, ?»1169 [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?» 975 1170  Some e1 ⇒ 976 1171 do e1' ← translate_expr vars e1; 977 OK ? «〈 St_return (Some ? (mk_DPair … e1')), u〉, ?»1172 OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?» 978 1173 ] 979 1174  Sswitch e1 ls ⇒ Error ? (msg FIXME) 980 1175  Slabel l s1 ⇒ 981 1176 do l' as E ← lookup_label lbls l; 982 do «s1', u, H1» ← translate_statement vars lbls us1;983 OK ? «〈 St_label l' s1', u〉, ?»1177 do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1; 1178 OK ? «〈fgens1, St_label l' s1'〉, ?» 984 1179  Sgoto l ⇒ 985 1180 do l' as E ← lookup_label lbls l; 986 OK ? «〈 St_goto l', u〉, ?»1181 OK ? «〈uv, ul, St_goto l'〉, ?» 987 1182  Scost l s1 ⇒ 988 do «s1', u, H1» ← translate_statement vars lbls u s1; 989 OK ? «〈St_cost l s1', u〉, ?» 990 ]. 991 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj 992 try @I 993 try (#l #H @(match H in False with [ ])) 994 try (#id #ty #H @H) 995 [ @add_tmps_oblivious @(pi2 ?? s') 996  @(tmp_preserved … u) @p 997 ] 998 try (@sub_pi2 #x @expr_vars_mp #i #ty @(tmp_preserved … u)) 999 [ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i #ty' @(tmp_preserved … u) 1000  2,4: @(local_id_fresh_tmp … Etmp) 1001  @(alloc_tmp_preserves … Etmp) 1002  7,11: @(stmt_P_mp … (π1 (π1 H1))) #s * #H3 #H4 % [ 1,3: @(stmt_vars_mp … H3) cases H2 #_ #H @H  *: @H4 ] 1003  8,12: @(trans_inv_stmt_inv … H2) 1004  9,13: #l #H cases (Exists_append … H) 1005 [ 1,3: #H3 cases H1 * #S1 #L1 #T1 cases (L1 l H3) #l' * #E1 #D1 1006 %{l'} % [ 1,3: @E1  *: @Exists_append_l @D1 ] 1007  *: #H3 cases H2 * #S2 #L2 #T2 cases (L2 l H3) #l' * #E2 #D2 1008 %{l'} % [ 1,3: @E2  *: @Exists_append_r @D2 ] 1009 ] 1010  10,14: cases H2 #_ #TP2 #id #ty #L @TP2 cases H1 #_ #TP1 @TP1 @L 1011  15,18: @(π1 (π1 H1)) 1012  16,19: cases H1 * #_ #L1 #_ #l #H cases (L1 l H) #l' * #E1 #D1 1013 %{l'} % [ 1,3: @E1  *: @Exists_append_l @D1 ] 1014  17,20: @(π2 H1) 1015 (* Sfor *) 1016  @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #ty #H @(π2 H3) @(π2 H2) @H  @H5 ] 1017  @(π1 (π1 H3)) 1018  @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #ty #H @(π2 H3) @H  @H5 ] 1019  #l #H cases (Exists_append … H) 1020 [ #EX1 cases H1 * #S1 #L1 #_ cases (L1 l EX1) #l' * #E1 #D1 1021 %{l'} % [ @E1  @Exists_append_l @D1 ] 1022  #EX cases (Exists_append … EX) 1023 [ #EX2 cases H2 * #S2 #L2 #_ cases (L2 l EX2) #l' * #E2 #D2 1024 %{l'} % [ @E2  @Exists_append_r @Exists_append_l @Exists_append_r @D2 ] 1025  #EX3 cases H3 * #S3 #L3 #_ cases (L3 l EX3) #l' * #E3 #D3 1026 %{l'} % [ @E3  @Exists_append_r @Exists_append_l @Exists_append_l @D3 ] 1027 ] 1028 ] 1029  #id #ty #H @(π2 H3) @(π2 H2) @(π2 H1) @H 1030 (* Slabel *) 1031  %{l} @E 1032  @(π1 (π1 H1)) 1033  #l'' * [ #E <E %{l'} % // %1 @refl  #EX cases (π2 (π1 H1) l'' EX) #l4 * #LK #LD %{l4} % // %2 @LD ] 1034  @(π2 H1) 1035 (* Sgoto *) 1036  %{l} @E 1037  @(π1 (π1 H1)) 1038 (* Scost *) 1039  @(π2 (π1 H1)) 1040  @(π2 H1) 1183 do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1; 1184 OK ? «〈fgens1, St_cost l s1'〉, ?» 1185 ]. 1186 try @conj try @conj try @conj try @conj try @conj try @conj try @conj 1187 try (@I) 1188 try (#l #H elim H) 1189 try (#size #sign #H assumption) 1190 try (#region #H assumption) 1191 [ 1,5: @(tmp_preserved … p) ] 1192 [ 1,3: elim e2'  2,9: elim e1'  4,7,14: elim ef' ] 1193 [ 1,2,3,4,5,6,7 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ] 1194 [ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ]) 1195  2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp) 1196  3: elim args' // ] 1197  8: (* we should be able to merge this case with the previous ... *) 1198 @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ]) 1199  2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp) 1200  3: elim args' // ] 1201  2: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) 1202  3: @(All_mp (𝚺 t:typ.expr t) (λe. match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars)])) 1203 [ 1: #a #Ha elim a in Ha ⊢ ?; #ta #a #Ha whd @(expr_vars_mp ?? (local_id vars)) 1204 [ 1: #i0 #t0 #H0 @(tmp_preserved vars uv1 i0 t0 H0) 1205  2: assumption ] 1206  2: elim args' // ] 1207  4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ] 1208 [ 1: #size #sign  2: #reg  3: #fsize ] 1209 [ 1,2,3: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ] 1210 try @(match fgens1 return λx.x=fgens1 → ? with 1211 [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1)) 1212 try @(match fgens2 return λx.x=fgens2 → ? with 1213 [ mk_Prod uv2 ul2 ⇒ λHfgens2.? ] (refl ? fgens2)) 1214 try @(match fgens3 return λx.x=fgens3 → ? with 1215 [ mk_Prod uv3 ul3 ⇒ λHfgens3.? ] (refl ? fgens3)) 1216 try @(match fgens4 return λx.x=fgens4 → ? with 1217 [ mk_Prod uv4 ul4 ⇒ λHfgens4.? ] (refl ? fgens4)) 1218 whd in H1 H2 H3 ⊢ ?; destruct whd nodelta in H1 H2 H3; 1219 try (elim H1 H1 * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1) 1220 try (elim H2 H2 * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2) 1221 try (elim H3 H3 * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3) 1222 [ 1,2: #Hind1 #Hind2  3,4,9,11: #Hind  5: #Hind1 #Hind2 #Hind3 ] 1223 try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption 1224 [ 1,7: @(stmt_P_mp … Hstmt_inv1) #e #Hvars @(stmt_vars_mp … Hvars) #i #t #Hlocal @(Htmps_pres2 … Hlocal) 1225  2: #l #H cases (Exists_append ???? H) #Hcase 1226 [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj 1227 [ 1: @(proj1 ?? Hlabel) 1228  2: normalize @Exists_append_l @(proj2 … Hlabel) ] 1229  2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj 1230 [ 1: @(proj1 ?? Hlabel) 1231  2: normalize @Exists_append_r @(proj2 … Hlabel) ] 1232 ] 1233  3,9: #id #ty #H @(Htmps_pres2 … (Htmps_pres1 id ty H)) ] 1234 [ 1: @(stmt_P_mp … Hind2)  2: @(stmt_P_mp … Hind1) ] 1235 [ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1236 #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H) 1237  2,5: #H %1 %2 assumption 1238  3,6: #H %2 assumption ] 1239 (* if/then/else *) 1240  3: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) 1241  4: whd #l #H 1242 cases (Exists_append ???? H) #Hcase 1243 [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj 1244 [ 1: @(proj1 ?? Hlabel) 1245  2: normalize @Exists_append_l @(proj2 … Hlabel) ] 1246  2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj 1247 [ 1: @(proj1 ?? Hlabel) 1248  2: normalize @Exists_append_r @(proj2 … Hlabel) ] 1249 ] 1250 ] 1251 [ 1: 1: @(stmt_P_mp … Hind2)  2: @(stmt_P_mp … Hind1) ] 1252 [ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1253 #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H) 1254  2,5: #H %1 %2 assumption 1255  3,6: #H %2 assumption ] ] 1256 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I 1257 [ 1,9,19,32: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) 1258  2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) // 1259  3,10: whd #l #H normalize in H; 1260 elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label) 1261 @conj 1262 [ 1,3: @(proj1 … Hlabel) 1263  2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l 1264 @(proj2 … Hlabel) ] 1265  30: whd %2 %2 whd /2/ 1266  31: whd %2 whd /2/ 1267  4,16: whd %1 %1 normalize /2/ 1268  5,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1269 #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H 1270  2,6: #H %1 %2 assumption 1271  3,7: #H <H %1 %1 normalize /2/ 1272  4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2 1273 @Exists_append_r normalize /2/ 1274  2,4: * ] 1275 ] 1276  6: normalize %1 %1 %1 // 1277  7,14: normalize %1 %1 %2 @Exists_append_r normalize /2/ 1278  11,13: whd %1 %1 normalize /2/ 1279  15: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct //  whd /2/ ] 1280  2: #H elim (Hlabels_tr1 label H) 1281 #lab * #Hlookup #Hdef @(ex_intro … lab) @conj 1282 [ 1: //  2: whd %2 assumption ] 1283 ] 1284  17: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1285 #l * try * [ 1: #H %1 %1 normalize %2 @H 1286  2: #H %1 %2 assumption 1287  3: #H %2 assumption ] 1288  18: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t 1289 #H @(Htmps_pres3 … (Htmps_pres2 … H)) 1290  20: @(stmt_P_mp … Hstmt_inv3) // 1291  21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t 1292 #H @(Htmps_pres3 … H) 1293  22: whd #l #H normalize in H; 1294 cases (Exists_append … H) #Hcase 1295 [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj 1296 [ 1: @(proj1 … Hlabel) 1297  2: normalize @Exists_append_l @(proj2 … Hlabel) 1298 ] 1299  2: cases (Exists_append … Hcase) #Hcase2 1300 [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj 1301 [ 1: @(proj1 … Hlabel) 1302  2: normalize >append_nil >append_nil >append_cons 1303 @Exists_append_r @Exists_append_l @Exists_append_r 1304 @(proj2 … Hlabel) 1305 ] 1306  2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj 1307 [ 1: @(proj1 … Hlabel) 1308  2: normalize >append_nil >append_nil >append_cons 1309 @Exists_append_r @Exists_append_l @Exists_append_l 1310 @(proj2 … Hlabel) 1311 ] 1312 ] 1313 ] 1314  23: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H))) 1315  24: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1316 #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H 1317  2: #H %1 %2 assumption 1318  3: #H %2 assumption ] 1319  25: whd %1 %1 normalize /2/ 1320  26: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1321 #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?)) 1322 @Exists_append_r @Exists_append_l @Exists_append_l 1323 @Exists_append_l assumption 1324  2: #H %1 %2 assumption 1325  3: #H <H %1 %1 normalize 1326 @Exists_append_r whd %1 // 1327  4: * [ 1: #H <H %1 %1 normalize 1328 @Exists_append_r @(Exists_add ?? (nil ?)) 1329 @Exists_append_r @Exists_append_r 1330 whd %1 // 1331  2: * ] 1332 ] 1333  27: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1334 #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?)) 1335 @Exists_append_r @Exists_append_l @Exists_append_l 1336 @Exists_append_r @Exists_append_l assumption 1337  2: #H %1 %2 assumption 1338  3: #H <H %1 %1 normalize 1339 @Exists_append_r whd %1 // 1340  4: * [ 1: #Eq <Eq %1 %1 whd normalize 1341 @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r 1342 @Exists_append_r whd %1 // 1343  2: * ] 1344 ] 1345  28: whd %1 %1 normalize /2/ 1346  29: whd %1 %1 normalize 1347 @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r 1348 whd %1 // 1349  33: whd %1 %2 whd @(ex_intro … l) @E 1041 1350 ] qed. 1042 1351 1043 1044 1352 axiom ParamGlobalMixup : String. 1045 1353 1046 (* ls and s0 aren't real parameters, they're just there for giving the invariant. *) 1047 definition alloc_params : ∀vars:var_types.∀ls,s0,u. list (ident×type) → (Σsu:stmt×(tmpgen vars). trans_inv vars ls s0 u su) → res (Σsu:stmt×(tmpgen vars).trans_inv vars ls s0 u su) ≝ 1048 λvars,ls,s0,u,params,s. foldl ?? (λsu,it. 1354 (* params and statement aren't real parameters, they're just there for giving the invariant. *) 1355 definition alloc_params : 1356 ∀vars:var_types.∀lbls,statement,uv,flag. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag su) 1357 → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag su) ≝ 1358 λvars,lbls,statement,uv,ul,params,s. foldl ?? (λsu,it. 1049 1359 let 〈id,ty〉 ≝ it in 1050 do «s,u, Is» ← su; 1360 do «result,Is» ← su; 1361 let 〈fgens1, s〉 as Eresult ≝ result in 1051 1362 do 〈t,ty'〉 as E ← lookup' vars id; 1052 match t return λx.? → ?with1053 [ Local ⇒ λE. OK (Σs: stmt×(tmpgen vars).?) «〈s,u〉,Is»1363 match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul su) with 1364 [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is» 1054 1365  Stack n ⇒ λE. 1055 1366 do q ← match access_mode ty with … … 1058 1369  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 1059 1370 ]; 1060 OK ? «〈 St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s, u〉, ?»1371 OK ? «〈fgens1, St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?» 1061 1372  Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id] 1062 1373 ] E) (OK ? s) params. 1063 try @conj try @conj try @conj try @conj try @conj try @conj 1064 try @I 1065 [ @(expr_vars_mp … (tmp_preserved … u)) whd >E @refl 1066  @(π1 (π1 Is)) 1067  @(π2 (π1 Is)) 1068  @(π2 Is) 1069 ] qed. 1070 1071 (* 1072 lemma local_id_add_local : ∀vars,id,id'. 1073 local_id vars id → 1074 local_id (add ?? vars id' Local) id. 1075 #vars #id #id' #H 1076 whd whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ?] cases (identifier_eq ? id id') 1077 [ #E < E >lookup_add_hit // 1078  #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/ 1079 ] qed. 1080 *) 1374 whd 1375 @(match fgens1 return λx.x=fgens1 → ? with 1376 [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1)) 1377 whd in Is ⊢ %; destruct whd in Is; 1378 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I 1379 elim Is * * #Hincl #Hstmt_inv #Hlab_tr #Htmp_pr try assumption 1380 @(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl 1381 qed. 1382 1081 1383 axiom DuplicateLabel : String. 1082 1384 … … 1098 1400 >lookup_add_miss 1099 1401 [ @refl  @NE ] 1100 qed. 1101 1102 let rec populate_lenv (ls:list ident) ( lbls:lenv) (u:universe ?) : res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) ≝1103 match ls return λls. res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) with1104 [ nil ⇒ OK ? «lbls, ?»1402 qed. 1403 1404 let rec populate_lenv (ls:list ident) (ul:labgen) (lbls:lenv): res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) ≝ 1405 match ls return λls.res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) with 1406 [ nil ⇒ OK ? 〈«lbls, ?», ul〉 1105 1407  cons l t ⇒ 1106 match lookup_label lbls l return λx.lookup_label lbls l = x → ? with 1107 [ OK _ ⇒ λ_. Error ? (msg DuplicateLabel) 1108  Error _ ⇒ λLOOK. 1109 let 〈l',u1〉 ≝ fresh … u in 1110 do lbls1 ← populate_lenv t (add … lbls l l') u1; 1111 OK ? «pi1 … lbls1, ?» 1112 ] (refl ? (lookup_label lbls l)) 1113 ]. 1114 [ #l #l' #H %2 @H 1115  cases lbls1 #lbls' #I whd in ⊢ (??%?); 1116 #l1 #l1' #E1 @(eq_identifier_elim … l l1) 1117 [ #E %1 %1 @E 1118  #NE cases (I l1 l1' E1) 1119 [ #H %1 %2 @H 1120  #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H 1121 ] 1122 ] 1123 ] qed. 1124 1125 definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) ≝ 1408 match lookup_label lbls l return λlook. lookup_label lbls l = look → ? with 1409 [ OK _ ⇒ λ_.Error ? (msg DuplicateLabel) 1410  Error _ ⇒ λLOOK. 1411 match generate_fresh_label … ul with 1412 [ mk_Sig ret H ⇒ 1413 do 〈packed_lbls, ul1〉 ← populate_lenv t (snd ?? ret) (add … lbls l (fst ?? ret)); 1414 match packed_lbls with 1415 [ mk_Sig lbls' Hinv ⇒ OK ? 〈«lbls', ?», ul1〉 ] 1416 ] 1417 ] (refl ? (lookup_label lbls l)) 1418 ]. 1419 [ 1: whd #l #l' #Hlookup %2 assumption 1420  2: whd in Hinv; whd #cl_lab #cm_lab #Hlookup 1421 @(eq_identifier_elim … l cl_lab) 1422 [ 1: #Heq %1 >Heq whd %1 // 1423  2: #Hneq cases (Hinv cl_lab cm_lab Hlookup) 1424 [ 1: #H %1 %2 @H 1425  2: #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H ] 1426 ] 1427 ] 1428 qed. 1429 1430 definition build_label_env : 1431 ∀body:statement. res ((Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) × labgen) ≝ 1126 1432 λbody. 1127 do «lbls, H» ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?); 1128 OK ? «lbls, ?». 1129 #l #l' #E cases (H l l' E) // 1130 whd in ⊢ (??%? → ?); #H destruct 1433 let initial_labgen ≝ mk_labgen (new_universe ?) (nil ?) ? in 1434 do 〈label_map, u〉 ← populate_lenv (labels_defined body) initial_labgen (empty_map ??); 1435 let lbls ≝ pi1 ?? label_map in 1436 let H ≝ pi2 ?? label_map in 1437 OK ? 〈«lbls, ?», u〉. 1438 [ 1: #l #l' #E cases (H l l' E) // 1439 whd in ⊢ (??%? → ?); #H destruct 1440  2: whd @I ] 1131 1441 qed. 1132 1442 … … 1158 1468 ] qed. 1159 1469 1470 (* This lemma allows to merge two stmt_P in one. Used in the following parts to merge an invariant on variables 1471 and an invariant on labels. *) 1472 lemma stmt_P_conj : ∀ (P1:stmt → Prop). ∀ (P2:stmt → Prop). ∀ s. stmt_P P1 s → stmt_P P2 s → stmt_P (λs.P1 s ∧ P2 s) s. 1473 #P1 #P2 #s elim s 1474 normalize try @conj try @conj try /3/ 1475 [ #z0 #s #Hind1 #Hind2 * * #HA #HB #HC * * #HD #HE #HF try @conj try @conj try @conj try /2/ 1476  #H5 #H6 #H7 #H8 #H9 #H10 #H11 * * #H15 #H16 #H17 * * #H20 #H21 #H22 1477 try @conj try @conj try @conj try /2/ 1478  3,4: #H24 #H25 * #H29 #H30 * #H33 #H34 try @conj try @conj try @conj try /2/ 1479  5,6: #H36 #H37 #H38 * #H42 #H43 * #H46 #H47 try @conj try @conj try @conj try /2/ ] 1480 qed. 1481 1160 1482 definition translate_function : 1161 1483 ∀tmpuniverse:universe SymbolTag. … … 1166 1488 res internal_function ≝ 1167 1489 λtmpuniverse, globals, f, Fglobals, Ffn. 1168 do «lbls, Ilbls» ← build_label_env (fn_body f); 1169 let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in 1170 let tmp ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in 1171 do s ← translate_statement vartypes lbls tmp (fn_body f); 1172 do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s; 1173 let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in 1174 let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? tmp @ fn_vars f) in 1175 do D ← check_distinct_env ?? (params @ vars); 1176 OK ? (mk_internal_function 1177 (opttyp_of_type (fn_return f)) 1178 params 1179 vars 1180 D 1181 stacksize 1182 s ?). 1183 [ // 1184  @(characterise_vars_fresh … (sym_eq … E)) // 1185  cases Is * #S #L #TP 1186 @(stmt_P_mp ???? S) 1187 #s1 * #H1 #H2 % 1188 [ @(stmt_vars_mp … H1) 1189 #i #t #H 1190 cases (local_id_split … H) 1191 [ #H' >map_append 1192 @Exists_map [ 2: @Exists_squeeze @(characterise_vars_all … (sym_eq ??? E) i t) @H' 1193  skip 1194  * #id #ty * #E1 #E2 <E1 <E2 @refl 1195 ] 1196  #EX @Exists_append_r whd in ⊢ (???%); <map_append @Exists_append_l @Exists_map [2: @EX  skip  * #id #ty * #E1 #E2 <E1 <E2 % @refl ] 1197 ] 1198  @(stmt_labels_mp … H2) 1199 #l * #l' #LOOKUP 1200 lapply (Ilbls l' l LOOKUP) #DEFINED 1201 cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex) 1202 #H @H 1203 ] 1204 ] qed. 1490 do 〈env_pack, ul〉 ← build_label_env (fn_body f); 1491 match env_pack with 1492 [ mk_Sig lbls Ilbls ⇒ 1493 let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in 1494 let uv ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in 1495 do s0 ← translate_statement vartypes uv ul lbls DoNotConvert (fn_body f); 1496 do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert (fn_params f) s0; 1497 let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in 1498 let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? (fst ?? fgens) @ fn_vars f) in 1499 do D ← check_distinct_env ?? (params @ vars); 1500 OK ? (mk_internal_function 1501 (opttyp_of_type (fn_return f)) 1502 params 1503 vars 1504 D 1505 stacksize 1506 s1 ?) 1507 ]. 1508 [ 1: #i #t #Hloc whd @Hloc 1509  2: whd #id #Hpresent normalize in Hpresent:(???%?); whd in Hpresent; 1510 @(characterise_vars_fresh … (sym_eq … E)) // 1511  3: @(match fgens return λx.x=fgens → ? with 1512 [ mk_Prod uv' ul' ⇒ λHfgens.? ] (refl ? fgens)) 1513 whd in Is; <Hfgens in Is; #Is whd in Is ⊢ %; 1514 elim Is * * #Hstmt_inv #Hlab_trans #Htmps_pres #Hlabel_wf 1515 (* merge Hlabel_wf with Hstmt_inv and eliminate right away *) 1516 @(stmt_P_mp … (stmt_P_conj … Hstmt_inv Hlabel_wf)) 1517 #s * #Hstmt_vars #Hstmt_labels @conj 1518 [ 1: (* prove that variables are either parameters or locals *) 1519 @(stmt_vars_mp … Hstmt_vars) #i #t #H 1520 (* Case analysis: (i, t) is either in vartypes, or in (tmp_env vartypes uv) *) 1521 cases (local_id_split … H) 1522 [ 1: #H' >map_append 1523 @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t)) (* * #id #ty @(〈id, typ_of_type ty〉=〈i, t〉)*) 1524  2: whd @Exists_squeeze @(characterise_vars_all globals f ?? (sym_eq ??? E) i t H') 1525  3: * #id #ty * #E1 #E2 <E1 <E2 @refl 1526 ] 1527  2: #EX @Exists_append_r whd in ⊢ (???%); <map_append @Exists_append_l 1528 @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t)) 1529  2: <Hfgens @EX 1530  3: * #id #ty * #E1 #E2 <E1 <E2 % @refl 1531 ] 1532 ] 1533  2: (* prove that labels are properly declared. *) 1534 @(stmt_labels_mp … Hstmt_labels) #l * * 1535 [ 1: #H assumption 1536  2: * #cl_label #Hlookup lapply (Ilbls cl_label l Hlookup) #Hdefined 1537 cases (Hlab_trans … Hdefined) #lx * #LOOKUPx >LOOKUPx in Hlookup; #Ex destruct (Ex) 1538 #H @H 1539 ] 1540 ] 1541 ] qed. 1205 1542 1206 1543 definition translate_fundef :
Note: See TracChangeset
for help on using the changeset viewer.