Changeset 1316 for src/Clight/toCminor.ma
 Timestamp:
 Oct 7, 2011, 12:26:39 PM (9 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src

Property
svn:mergeinfo
set to
/Deliverables/D3.3/idlookupbranch merged eligible

Property
svn:mergeinfo
set to

src/Clight/toCminor.ma
r1224 r1316 3 3 include "Clight/TypeComparison.ma". 4 4 include "utilities/lists.ma". 5 include "utilities/deppair.ma". 5 6 6 7 (* Identify local variables that must be allocated memory. *) … … 84 85 definition var_types ≝ identifier_map SymbolTag var_type. 85 86 87 axiom UndeclaredIdentifier : String. 88 89 definition lookup' ≝ 90 λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id). 91 92 definition local_id : var_types → ident → Prop ≝ 93 λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False  _ ⇒ True ]  _ ⇒ False ]. 94 86 95 (* Note that the semantics allows locals to shadow globals. 87 96 Parameters start out as locals, but get stack allocated if their address … … 99 108 definition characterise_vars : list (ident×region) → function → var_types × nat ≝ 100 109 λglobals, f. 101 let m ≝ foldl ?? (λm,idr. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in 102 let m ≝ foldl ?? (λm,v. add ?? m (\fst v) Local) m (fn_params f) in 110 let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in 103 111 let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in 104 let 〈m,stacksize〉 ≝ fold l ?? (λms,v.112 let 〈m,stacksize〉 ≝ foldr ?? (λv,ms. 105 113 let 〈m,stack_high〉 ≝ ms in 106 114 let 〈id,ty〉 ≝ v in … … 111 119 〈m,stacksize〉. 112 120 121 lemma local_id_add_global : ∀vars,id,r,id'. 122 local_id (add ?? vars id (Global r)) id' → local_id vars id'. 123 #var #id #r #id' 124 whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?] → ?) 125 cases (identifier_eq ? id id') 126 [ #E >E >lookup_add_hit whd in ⊢ (% → ?) * 127  #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/ 128 ] qed. 129 130 lemma local_id_add_miss : ∀vars,id,t,id'. 131 id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'. 132 #vars #id #t #id' #NE 133 whd in ⊢ (% → %) 134 whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ] → match % with [ _ ⇒ ?  _ ⇒ ? ]) 135 >lookup_add_miss 136 [ #H @H  @eq_identifier_elim // #E >E in NE * /2/ ] 137 qed. 138 139 include "utilities/extralib.ma". (* for pair_eq1 to work around destruct's excessive normalisation *) 140 141 lemma characterise_vars_all : ∀l,f,vars,n. 142 characterise_vars l f = 〈vars,n〉 → 143 ∀i. local_id vars i → 144 Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f). 145 #globals #f 146 whd in ⊢ (∀_.∀_.??%? → ?) 147 elim (fn_params f @ fn_vars f) 148 [ #vars #n whd in ⊢ (??%? → ?) #E <(pair_eq1 ?????? E) E; #i #H @False_ind 149 elim globals in H 150 [ normalize // 151  * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H) 152 ] 153  * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i 154 cases (identifier_eq ? id i) 155 [ #E' <E' #H % @refl 156  #NE #H whd %2 >(contract_pair var_types nat ?) in E; 157 whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?) 158 cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?) 159 #H' lapply (extract_pair ???????? H') H' * #m0 * #n0 * #EQ #EQ2 160 @(IH m0 n0) 161 [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ 162  2,4: <(pair_eq1 ?????? EQ2) in H #H' @(local_id_add_miss … H') @NE 163 ] 164 ] 165 ] qed. 113 166 114 167 include "Cminor/syntax.ma". … … 117 170 alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)". 118 171 119 axiom UndeclaredIdentifier : String.120 172 axiom BadlyTypedAccess : String. 121 173 axiom BadLvalue : String. … … 255 307 ]. 256 308 309 lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e. 310 expr_vars ? e1 P → 311 expr_vars ? e2 P → 312 translate_binop op ty1 e1 ty2 e2 ty = OK ? e → 313 expr_vars ? e P. 314 #P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2 315 whd in ⊢ (??%? → ?) 316 [ cases (classify_add ty1 ty2) 317 [ 3,4: #z ] whd in ⊢ (??%? → ?) 318 [ generalize in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ])? → ?) 319 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 320 whd in c:(??%?); destruct % [ @H1  % // @H2 ] 321  generalize in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ])? → ?) 322 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 323 whd in c:(??%?); destruct % [ @H2  % // @H1 ] 324  *: #E destruct (E) % try @H1 @H2 325 ] 326  cases (classify_sub ty1 ty2) 327 [ 3,4: #z] whd in ⊢ (??%? → ?) 328 [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ])? → ?) 329 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 330 whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I 331  *: #E destruct (E) % try @H1 try @H2 % // @H2 332 ] 333  cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct 334 % try @H1 @H2 335  cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct 336 % try @H1 @H2 337  cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct 338 % try @H1 @H2 339  6,7,8,9: #E destruct % try @H1 @H2 340  cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2 341  11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2 342 ] qed. 257 343 258 344 (* We'll need to implement proper translation of pointers if we really do memory … … 269 355 ]. 270 356 271 definition translate_ptr : ∀ r1,r2. CMexpr (ASTptr r1) → res (CMexpr (ASTptr r2)) ≝272 λ r1,r2,e. check_region r1 r2 ?e.273 274 definition translate_cast : type → ∀ty2:type. CMexpr ? → res (CMexpr (typ_of_type ty2)) ≝275 λ ty1,ty2.276 match ty1 return λx. CMexpr (typ_of_type x) → ? with357 definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝ 358 λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e. 359 360 definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝ 361 λP,ty1,ty2. 362 match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with 277 363 [ Tint sz1 sg1 ⇒ λe. 278 match ty2 return λx.res ( CMexpr (typ_of_type x)) with364 match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with 279 365 [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e) 280 366  Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu  _ ⇒ Ofloatofint]) e) … … 284 370 ] 285 371  Tfloat sz1 ⇒ λe. 286 match ty2 return λx.res ( CMexpr (typ_of_type x)) with287 [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2  _ ⇒ Ointoffloat sz2 ]) e)288  Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e)(* FIXME *)372 match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with 373 [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2  _ ⇒ Ointoffloat sz2 ]) e, ?» 374  Tfloat sz2 ⇒ OK ? «Op1 ?? Oid e, ?» (* FIXME *) 289 375  _ ⇒ Error ? (msg TypeMismatch) 290 376 ] 291 377  Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *) 292 match ty2 return λx.res ( CMexpr (typ_of_type x)) with293 [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ointofptr sz2) e)294  Tarray r2 _ _ ⇒ translate_ptr r1 r2 e295  Tpointer r2 _ ⇒ translate_ptr r1 r2 e378 match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with 379 [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2) e, ?» 380  Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e 381  Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e 296 382  _ ⇒ Error ? (msg TypeMismatch) 297 383 ] 298 384  Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *) 299 match ty2 return λx.res ( CMexpr (typ_of_type x)) with300 [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e)301  Tarray r2 _ _ ⇒ translate_ptr r1 r2 e302  Tpointer r2 _ ⇒ translate_ptr r1 r2 e385 match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with 386 [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e, ?» 387  Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e 388  Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e 303 389  _ ⇒ Error ? (msg TypeMismatch) 304 390 ] 305 391  _ ⇒ λ_. Error ? (msg TypeMismatch) 306 ]. 392 ]. whd @use_sig qed. 307 393 308 394 definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝ … … 335 421 ] qed. 336 422 337 let rec translate_expr (vars:var_types) (e:expr) on e : res ( CMexpr (typ_of_type (typeof e))) ≝338 match e return λe. res ( CMexpr (typ_of_type (typeof e))) with423 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)) ≝ 424 match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with 339 425 [ Expr ed ty ⇒ 340 426 match ed with 341 [ Econst_int sz i ⇒ OK ? (Cst ? (Ointconst sz i))342  Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))427 [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?» 428  Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?» 343 429  Evar id ⇒ 344 do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);345 match c with346 [ Global r ⇒ 430 do c as E ← lookup' vars id; 431 match c return λx.? = ? → res (Σe':CMexpr ?. ?) with 432 [ Global r ⇒ λ_. 347 433 match access_mode ty with 348 [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id 0)))349  By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id 0))434 [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?» 435  By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?» 350 436  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 351 437 ] 352  Stack n ⇒ 438  Stack n ⇒ λE. 353 439 match access_mode ty with 354 [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack n)))355  By_reference _ ⇒ OK ? (Cst ? (Oaddrstack n))440 [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?» 441  By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?» 356 442  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 357 443 ] 358  Local ⇒ OK ? (Id ? id)359 ] 444  Local ⇒ λE. OK ? «Id ? id, ?» 445 ] E 360 446  Ederef e1 ⇒ 361 447 do e1' ← translate_expr vars e1; 362 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with448 match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with 363 449 [ ASTptr r ⇒ λe1'. 364 match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with 365 [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1') 366  By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉ 450 match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with 451 [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (eject … e1'), ?» 452  By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1'; 453 OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉ 367 454  By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) 368 ] ( refl ? (access_mode ty))455 ] (access_mode_typ ty) 369 456  _ ⇒ λ_. Error ? (msg TypeMismatch) 370 457 ] e1' 371 458  Eaddrof e1 ⇒ 372 459 do e1' ← translate_addr vars e1; 373 match typ_of_type ty return λx.res ( CMexpr x) with460 match typ_of_type ty return λx.res (Σz:CMexpr x.?) with 374 461 [ ASTptr r ⇒ 375 462 match e1' with … … 381 468 do op' ← translate_unop ty op; 382 469 do e1' ← translate_expr vars e1; 383 OK ? (Op1 ?? op' e1')470 OK ? «Op1 ?? op' e1', ?» 384 471  Ebinop op e1 e2 ⇒ 385 472 do e1' ← translate_expr vars e1; 386 473 do e2' ← translate_expr vars e2; 387 translate_binop op (typeof e1) e1' (typeof e2) e2' ty 474 do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty; 475 OK ? «e', ?» 388 476  Ecast ty1 e1 ⇒ 389 477 do e1' ← translate_expr vars e1; 390 do e' ← translate_cast (typeof e1) ty1 e1'; 391 typ_should_eq ? (typ_of_type ty) ? e' 478 do e' ← translate_cast ? (typeof e1) ty1 e1'; 479 do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e'; 480 OK ? e' 392 481  Econdition e1 e2 e3 ⇒ 393 482 do e1' ← translate_expr vars e1; 394 483 do e2' ← translate_expr vars e2; 395 do e2' ← type_should_eq ? ty (λx. CMexpr (typ_of_type x)) e2';484 do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; 396 485 do e3' ← translate_expr vars e3; 397 do e3' ← type_should_eq ? ty (λx. CMexpr (typ_of_type x)) e3';398 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with399 [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' e3')486 do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3'; 487 match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with 488 [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?» 400 489  _ ⇒ λ_.Error ? (msg TypeMismatch) 401 490 ] e1' … … 405 494 match ty with 406 495 [ Tint sz _ ⇒ 407 do e2' ← type_should_eq ? ty (λx. CMexpr (typ_of_type x)) e2';408 match typ_of_type (typeof e1) return λx. CMexpr x → res (CMexpr (typ_of_type ty))with409 [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))))496 do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; 497 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with 498 [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))), ?» 410 499  _ ⇒ λ_.Error ? (msg TypeMismatch) 411 500 ] e1' … … 417 506 match ty with 418 507 [ Tint sz _ ⇒ 419 do e2' ← type_should_eq ? ty (λx. CMexpr (typ_of_type x)) e2';420 match typ_of_type (typeof e1) return λx. CMexpr x → res (CMexpr (typ_of_type ty))with421 [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2')508 do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; 509 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with 510 [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?» 422 511  _ ⇒ λ_.Error ? (msg TypeMismatch) 423 512 ] e1' … … 426 515  Esizeof ty1 ⇒ 427 516 match ty with 428 [ Tint sz _ ⇒ OK ? (Cst ? (Ointconst sz (repr ? (sizeof ty1))))517 [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?» 429 518  _ ⇒ Error ? (msg TypeMismatch) 430 519 ] 431 520  Efield e1 id ⇒ 432 do e' ←match typeof e1 with521 match typeof e1 with 433 522 [ Tstruct _ fl ⇒ 434 523 do e1' ← translate_addr vars e1; … … 437 526 do off ← field_offset id fl; 438 527 match access_mode ty with 439 [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))440  By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))))528 [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?» 529  By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?» 441 530  By_nothing ⇒ Error ? (msg BadlyTypedAccess) 442 531 ] … … 446 535 match e1' with 447 536 [ dp r e1' ⇒ 448 match access_mode ty return λx. access_mode ty = x → res (CMexpr (typ_of_type ty)) with 449 [ By_value q ⇒ λ_. OK ? (Mem ?? q e1') 450  By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈res (CMexpr (ASTptr r')) ↦ res (CMexpr (typ_of_type ty))⌉ 537 match access_mode ty return λx. access_mode ty = x → res ? with 538 [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?» 539  By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1'; 540 OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉ 451 541  By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) 452 542 ] (refl ? (access_mode ty)) 453 543 ] 454 544  _ ⇒ Error ? (msg BadlyTypedAccess) 455 ]; 456 typ_should_eq ? (typ_of_type ty) ? e' 545 ] 457 546  Ecost l e1 ⇒ 458 547 do e1' ← translate_expr vars e1; 459 do e' ← OK ? (Ecost ? l e1');460 typ_should_eq ? (typ_of_type ty) ?e'461 ] 462 ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. CMexpr (ASTptr r)) ≝548 do e' ← OK ? «Ecost ? l e1',?»; 549 typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e' 550 ] 551 ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝ 463 552 match e with 464 553 [ Expr ed _ ⇒ … … 466 555 [ Evar id ⇒ 467 556 do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id); 468 match c return λ_. res (Σr. CMexpr (ASTptr r)) with469 [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0)))470  Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack n)))557 match c return λ_. res (Σr.Σz:CMexpr (ASTptr r).?) with 558 [ Global r ⇒ OK ? «r, «Cst ? (Oaddrsymbol id 0), ?»» 559  Stack n ⇒ OK ? «Any, «Cst ? (Oaddrstack n), ?»» 471 560  Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *) 472 561 ] 473 562  Ederef e1 ⇒ 474 563 do e1' ← translate_expr vars e1; 475 match typ_of_type (typeof e1) return λx. CMexpr x → res (Σr. CMexpr (ASTptr r)) with476 [ ASTptr r ⇒ λe1'.OK ? (dp ?? r e1')564 match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σr. Σz:CMexpr (ASTptr r). ?) with 565 [ ASTptr r ⇒ λe1'.OK ? «r, e1'» 477 566  _ ⇒ λ_.Error ? (msg BadlyTypedAccess) 478 567 ] e1' … … 483 572 do off ← field_offset id fl; 484 573 match e1' with 485 [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))574 [ dp r e1'' ⇒ OK (Σr:region.Σe:CMexpr (ASTptr r).?) («r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» ») 486 575 ] 487 576  Tunion _ _ ⇒ translate_addr vars e1 … … 491 580 ] 492 581 ]. 493 >(access_mode_typ … E) @refl 494 qed. 495 496 inductive destination : Type[0] ≝ 497  IdDest : ident → destination 498  MemDest : ∀r:region. memory_chunk → CMexpr (ASTptr r) → destination. 582 whd try @I 583 [ >E @I 584  >(E ? (refl ??)) @refl 585  3,4: @use_sig 586  @(translate_binop_vars … E) @use_sig 587  % [ % ] @use_sig 588  % [ % @use_sig ] whd @I 589  % [ % [ @use_sig  @I ]  @use_sig ] 590  % [ @use_sig  @I ] 591  % [ @use_sig  @I ] 592  >(access_mode_typ … E) @refl 593  @use_sig 594  @use_sig 595  % [ @use_sig  @I ] 596 ] qed. 597 598 inductive destination (vars:var_types) : Type[0] ≝ 599  IdDest : ∀id:ident. local_id vars id → destination vars 600  MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars. 499 601 500 602 definition translate_dest ≝ … … 509 611 match ed1 with 510 612 [ Evar id ⇒ 511 do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);512 match c with513 [ Local ⇒ OK ? (IdDest id)514  Global r ⇒ OK ? (MemDestr q (Cst ? (Oaddrsymbol id 0)))515  Stack n ⇒ OK ? (MemDestAny q (Cst ? (Oaddrstack n)))516 ] 613 do c as E ← lookup' vars id; 614 match c return λx.? → ? with 615 [ Local ⇒ λE. OK ? (IdDest vars id ?) 616  Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0))) 617  Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n))) 618 ] E 517 619  _ ⇒ 518 620 do e1' ← translate_addr vars e1; 519 match e1' with [ dp r e1' ⇒ OK ? (MemDest r q e1') ]621 match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ] 520 622 ] 521 623 ]. 522 523 definition translate_assign ≝ 624 whd // >E @I 625 qed. 626 627 definition lenv ≝ identifier_map SymbolTag (identifier Label). 628 629 axiom MissingLabel : String. 630 631 definition lookup_label ≝ 632 λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l). 633 634 definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l. 635 636 let rec labels_defined (s:statement) : list ident ≝ 637 match s with 638 [ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2 639  Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2 640  Swhile _ s ⇒ labels_defined s 641  Sdowhile _ s ⇒ labels_defined s 642  Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3 643  Sswitch _ ls ⇒ labels_defined_switch ls 644  Slabel l s ⇒ l::(labels_defined s) 645  Scost _ s ⇒ labels_defined s 646  _ ⇒ [ ] 647 ] 648 and labels_defined_switch (ls:labeled_statements) : list ident ≝ 649 match ls with 650 [ LSdefault s ⇒ labels_defined s 651  LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls 652 ]. 653 654 definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s). 655 656 definition labels_translated : lenv → statement → stmt → Prop ≝ 657 λlbls,s,s'. ∀l. 658 (Exists ? (λl'.l' = l) (labels_defined s)) → 659 ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'. 660 661 definition stmt_inv ≝ 662 λvars. λlbls:lenv. 663 stmt_P (λs.stmt_vars (local_id vars) s ∧ stmt_labels (lpresent lbls) s). 664 665 definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.∀ls. stmt_inv vars ls s) ≝ 524 666 λvars,e1,e2. 525 667 do e2' ← translate_expr vars e2; 526 668 do dest ← translate_dest vars e1 (typeof e2); 527 669 match dest with 528 [ IdDest id ⇒ OK ? (St_assign ? id e2') 529  MemDest r q e1' ⇒ OK ? (St_store ? r q e1' e2') 530 ]. 670 [ IdDest id p ⇒ OK ? «St_assign ? id e2', ?» 671  MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?» 672 ]. 673 #ls whd % 674 [ % // @use_sig 675  @I 676  % @use_sig 677  @I 678 ] qed. 531 679 532 680 definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝ … … 537 685 ]. 538 686 539 definition translate_expr_sigma : var_types → expr → res (Σt:typ.CMexpr t) ≝687 definition translate_expr_sigma : ∀vars:var_types. expr → res (Σe:(Σt:typ.CMexpr t). match e with [ dp t e ⇒ expr_vars t e (local_id vars) ]) ≝ 540 688 λv,e. 541 689 do e' ← translate_expr v e; 542 OK ? (dp ? (λt:typ.CMexpr t) ? e'). 690 OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?». 691 whd @use_sig 692 qed. 543 693 544 694 axiom FIXME : String. … … 554 704 〈tmp, mk_tmpgen u (〈tmp, typ_of_memory_chunk c〉::(tmp_env g))〉. 555 705 556 let rec translate_statement (vars:var_types) (u:tmpgen) (s:statement) on s : res (stmt×tmpgen) ≝ 557 match s with 558 [ Sskip ⇒ OK ? 〈St_skip, u〉 559  Sassign e1 e2 ⇒ do s' ← translate_assign vars e1 e2; OK ? 〈s',u〉 706 lemma lookup_label_hit : ∀lbls,l,l'. 707 lookup_label lbls l = OK ? l' → 708 lpresent lbls l'. 709 #lbls #l #l' #E whd %{l} @E 710 qed. 711 712 definition add_tmps : var_types → tmpgen → var_types ≝ 713 λvs,g. 714 foldr ?? (λidty,vs. add ?? vs (\fst idty) Local) vs (tmp_env g). 715 716 definition tmps_preserved : var_types → tmpgen → tmpgen → Prop ≝ 717 λvars,u1,u2. 718 ∀id. local_id (add_tmps vars u1) id → local_id (add_tmps vars u2) id. 719 720 lemma alloc_tmp_preserves : ∀tmp,u,u',vars,q. 721 〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'. 722 #tmp #g #g' #vars #q 723 whd in ⊢ (???% → ?) 724 generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?) 725 * #tmp' #u whd in ⊢ (???% → ?) #E 726 >(pair_eq2 ?????? E) 727 #id #H 728 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ? ] 729 cases (identifier_eq ? id tmp') 730 [ #E1 >E1 >lookup_add_hit @I 731  * #NE >lookup_add_miss [ @H  @eq_identifier_elim // #E1 cases (NE E1) 732 ] qed. 733 734 definition trans_inv : var_types → lenv → statement → tmpgen → (stmt×tmpgen) → Prop ≝ 735 λvars,lbls,s,u,su'. 736 let 〈s',u'〉 ≝ su' in 737 stmt_inv (add_tmps vars u') lbls s' ∧ 738 labels_translated lbls s s' ∧ 739 tmps_preserved vars u u'. 740 741 lemma trans_inv_stmt_inv : ∀vars,lbls,s,u,su. 742 trans_inv vars lbls s u su → stmt_inv (add_tmps vars (\snd su)) lbls (\fst su). 743 #var #lbls #s #u * #s' #u' * * #H1 #H2 #H3 @H1 744 qed. 745 746 lemma trans_inv_labels : ∀vars,lbls,s,u,su. 747 trans_inv vars lbls s u su → labels_translated lbls s (\fst su). 748 #vars #lbls #s #u * #s' #u' * * #_ #H #_ @H 749 qed. 750 751 lemma local_id_add_local_oblivious : ∀vars,id,id'. 752 local_id vars id → local_id (add ?? vars id' Local) id. 753 #vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) 754 cases (identifier_eq ? id id') 755 [ #E >E >lookup_add_hit @I 756  * #NE >lookup_add_miss [ @H  @eq_identifier_elim // #E cases (NE E) 757 ] qed. 758 759 lemma local_id_add_tmps_oblivious : ∀vars,id,u. 760 local_id vars id → local_id (add_tmps vars u) id. 761 #vars #id * #u #l #H elim l 762 [ // 763  * #id' #ty #tl @local_id_add_local_oblivious 764 ] qed. 765 766 lemma add_tmps_oblivious : ∀vars,lbls,s,u. 767 stmt_inv vars lbls s → stmt_inv (add_tmps vars u) lbls s. 768 #vars #lbls #s #u #H 769 @(stmt_P_mp … H) 770 #s' * #H1 #H2 % 771 [ @(stmt_vars_mp … H1) 772 #id @local_id_add_tmps_oblivious 773  @H2 774 ] qed. 775 776 lemma local_id_fresh_tmp : ∀tmp,u,q,u0,vars. 777 〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp. 778 #tmp #u #q #u0 #vars 779 whd in ⊢ (???% → ?) 780 generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?) 781 * #tmp' #u' whd in ⊢ (???% → ?) #E 782 >(pair_eq1 ?????? E) >(pair_eq2 ?????? E) 783 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ? ] >lookup_add_hit 784 @I 785 qed. 786 787 lemma use_sig' : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' x. 788 #A #P #P' #H1 * #x #H2 @H1 @H2 789 qed. 790 791 definition sigbind2 : ∀A,B,C:Type[0]. ∀P:A×B → Prop. res (Σx:A×B.P x) → (∀a,b. P 〈a,b〉 → res C) → res C ≝ 792 λA,B,C,P,e,f. 793 match e with 794 [ OK v ⇒ match v with [ dp v' p ⇒ match v' return λv'. P v' → res C with [ pair a b ⇒ f a b ] p ] 795  Error msg ⇒ Error ? msg 796 ]. 797 798 notation > "vbox('do' 〈ident v1, ident v2〉 'with' ident H ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}. 799 (* 800 notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. 801 notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}. 802 notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. 803 *) 804 interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f). 805 806 let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen) (s:statement) on s : res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) ≝ 807 match s return λs.res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) with 808 [ Sskip ⇒ OK ? «〈St_skip, u〉, ?» 809  Sassign e1 e2 ⇒ 810 do s' ← translate_assign vars e1 e2; 811 OK ? «〈eject ?? s', u〉, ?» 560 812  Scall ret ef args ⇒ 561 813 do ef' ← translate_expr vars ef; 562 do ef' ← typ_should_eq ?(ASTptr Code) ? ef';563 do args' ← mmap … (translate_expr_sigma vars) args;814 do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef'; 815 do args' ← mmap_sigma … (translate_expr_sigma vars) args; 564 816 match ret with 565 [ None ⇒ OK ? 〈St_call (None ?) ef' args', u〉817 [ None ⇒ OK ? «〈St_call (None ?) ef' args', u〉, ?» 566 818  Some e1 ⇒ 567 819 do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *) 568 820 match dest with 569 [ IdDest id ⇒ OK ? 〈St_call (Some ? id) ef' args', u〉821 [ IdDest id p ⇒ OK ? «〈St_call (Some ? id) ef' args', u〉, ?» 570 822  MemDest r q e1' ⇒ 571 let 〈tmp, u〉 ≝ alloc_tmp q u in572 OK ? 〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉823 let 〈tmp, u〉 as Etmp ≝ alloc_tmp q u in 824 OK ? «〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉, ?» 573 825 ] 574 826 ] 575 827  Ssequence s1 s2 ⇒ 576 do 〈s1', u 〉 ← translate_statement vars u s1;577 do 〈s2', u 〉 ← translate_statement vars us2;578 OK ? 〈St_seq s1' s2', u〉828 do 〈s1', u1〉 with H1 ← translate_statement vars lbls u s1; 829 do 〈s2', u2〉 with H2 ← translate_statement vars lbls u1 s2; 830 OK ? «〈St_seq s1' s2', u2〉, ?» 579 831  Sifthenelse e1 s1 s2 ⇒ 580 832 do e1' ← translate_expr vars e1; 581 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with833 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 582 834 [ ASTint _ _ ⇒ λe1'. 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〉835 do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1; 836 do 〈s2', u〉 with H2 ← translate_statement vars lbls u s2; 837 OK ? «〈St_ifthenelse ?? e1' s1' s2', u〉, ?» 586 838  _ ⇒ λ_.Error ? (msg TypeMismatch) 587 839 ] e1' 588 840  Swhile e1 s1 ⇒ 589 841 do e1' ← translate_expr vars e1; 590 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with842 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 591 843 [ ASTint _ _ ⇒ λe1'. 592 do 〈s1', u〉 ← translate_statement vars u s1;844 do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1; 593 845 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 594 OK ? 〈St_block846 OK ? «〈St_block 595 847 (St_loop 596 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉 848 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉, ?» 597 849  _ ⇒ λ_.Error ? (msg TypeMismatch) 598 850 ] e1' 599 851  Sdowhile e1 s1 ⇒ 600 852 do e1' ← translate_expr vars e1; 601 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with853 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with 602 854 [ ASTint _ _ ⇒ λe1'. 603 do 〈s1',u〉 ← translate_statement vars u s1;855 do 〈s1',u〉 with H1 ← translate_statement vars lbls u s1; 604 856 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 605 OK ? 〈St_block857 OK ? «〈St_block 606 858 (St_loop 607 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉 859 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉, ?» 608 860  _ ⇒ λ_.Error ? (msg TypeMismatch) 609 861 ] e1' 610 862  Sfor s1 e1 s2 s3 ⇒ 611 863 do e1' ← translate_expr vars e1; 612 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with864 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with 613 865 [ ASTint _ _ ⇒ λe1'. 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;866 do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1; 867 do 〈s2', u〉 with H2 ← translate_statement vars lbls u s2; 868 do 〈s3', u〉 with H3 ← translate_statement vars lbls u s3; 617 869 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 618 OK ? 〈St_seq s1'870 OK ? «〈St_seq s1' 619 871 (St_block 620 872 (St_loop 621 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉 873 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉, ?» 622 874  _ ⇒ λ_.Error ? (msg TypeMismatch) 623 875 ] e1' 624  Sbreak ⇒ OK ? 〈St_exit 1, u〉625  Scontinue ⇒ OK ? 〈St_exit 0, u〉876  Sbreak ⇒ OK ? «〈St_exit 1, u〉, ?» 877  Scontinue ⇒ OK ? «〈St_exit 0, u〉, ?» 626 878  Sreturn ret ⇒ 627 879 match ret with 628 [ None ⇒ OK ? 〈St_return (None ?), u〉880 [ None ⇒ OK ? «〈St_return (None ?), u〉, ?» 629 881  Some e1 ⇒ 630 882 do e1' ← translate_expr vars e1; 631 OK ? 〈St_return (Some ? (dp … e1')), u〉883 OK ? «〈St_return (Some ? (dp … e1')), u〉, ?» 632 884 ] 633 885  Sswitch e1 ls ⇒ Error ? (msg FIXME) 634 886  Slabel l s1 ⇒ 635 do 〈s1', u〉 ← translate_statement vars u s1; 636 OK ? 〈St_label l s1', u〉 637  Sgoto l ⇒ OK ? 〈St_goto l, u〉 887 do l' as E ← lookup_label lbls l; 888 do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1; 889 OK ? «〈St_label l' s1', u〉, ?» 890  Sgoto l ⇒ 891 do l' as E ← lookup_label lbls l; 892 OK ? «〈St_goto l', u〉, ?» 638 893  Scost l s1 ⇒ 639 do 〈s1', u〉 ← translate_statement vars u s1; 640 OK ? 〈St_cost l s1', u〉 641 ]. 894 do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1; 895 OK ? «〈St_cost l s1', u〉, ?» 896 ]. 897 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj 898 try @I 899 try (#l #H @(match H in False with [ ])) 900 try (#id #H @H) 901 [ @add_tmps_oblivious @(use_sig ?? s') 902  @local_id_add_tmps_oblivious @p 903 ] 904 try (@use_sig' #x @expr_vars_mp #i @local_id_add_tmps_oblivious) 905 [ 1,3,6: @use_sig' #x @All_mp * #ty #e @expr_vars_mp #i @local_id_add_tmps_oblivious 906  2,4: @(local_id_fresh_tmp … Etmp) 907  @(alloc_tmp_preserves … Etmp) 908  7,11: @(stmt_P_mp … (π1 (π1 H1))) #s * #H3 #H4 % [ 1,3: @(stmt_vars_mp … H3) cases H2 #_ #H @H  *: @H4 ] 909  8,12: @(trans_inv_stmt_inv … H2) 910  9,13: #l #H cases (Exists_append … H) 911 [ 1,3: #H3 cases H1 * #S1 #L1 #T1 cases (L1 l H3) #l' * #E1 #D1 912 %{l'} % [ 1,3: @E1  *: @Exists_append_l @D1 ] 913  *: #H3 cases H2 * #S2 #L2 #T2 cases (L2 l H3) #l' * #E2 #D2 914 %{l'} % [ 1,3: @E2  *: @Exists_append_r @D2 ] 915 ] 916  10,14: cases H2 #_ #TP2 #id #L @TP2 cases H1 #_ #TP1 @TP1 @L 917  15,18: @(π1 (π1 H1)) 918  16,19: cases H1 * #_ #L1 #_ #l #H cases (L1 l H) #l' * #E1 #D1 919 %{l'} % [ 1,3: @E1  *: @Exists_append_l @D1 ] 920  17,20: @(π2 H1) 921 (* Sfor *) 922  @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @(π2 H2) @H  @H5 ] 923  @(π1 (π1 H3)) 924  @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @H  @H5 ] 925  #l #H cases (Exists_append … H) 926 [ #EX1 cases H1 * #S1 #L1 #_ cases (L1 l EX1) #l' * #E1 #D1 927 %{l'} % [ @E1  @Exists_append_l @D1 ] 928  #EX cases (Exists_append … EX) 929 [ #EX2 cases H2 * #S2 #L2 #_ cases (L2 l EX2) #l' * #E2 #D2 930 %{l'} % [ @E2  @Exists_append_r @Exists_append_l @Exists_append_r @D2 ] 931  #EX3 cases H3 * #S3 #L3 #_ cases (L3 l EX3) #l' * #E3 #D3 932 %{l'} % [ @E3  @Exists_append_r @Exists_append_l @Exists_append_l @D3 ] 933 ] 934 ] 935  #id #H @(π2 H3) @(π2 H2) @(π2 H1) @H 936 (* Slabel *) 937  %{l} @E 938  @(π1 (π1 H1)) 939  #l'' * [ #E <E %{l'} % // %1 @refl  #EX cases (π2 (π1 H1) l'' EX) #l4 * #LK #LD %{l4} % // %2 @LD ] 940  @(π2 H1) 941 (* Sgoto *) 942  %{l} @E 943  @(π1 (π1 H1)) 944 (* Scost *) 945  @(π2 (π1 H1)) 946  @(π2 H1) 947 ] qed. 948 642 949 643 950 axiom ParamGlobalMixup : String. 644 951 645 definition alloc_params : var_types → list (ident×type) → stmt → res stmt ≝ 646 λvars,params,s. foldl ?? (λs,it. 952 (* ls and s0 aren't real parameters, they're just there for giving the invariant. *) 953 definition alloc_params : ∀vars:var_types.∀ls,s0,u. list (ident×type) → (Σsu:stmt×tmpgen. trans_inv vars ls s0 u su) → res (Σsu:stmt×tmpgen.trans_inv vars ls s0 u su) ≝ 954 λvars,ls,s0,u,params,s. foldl ?? (λsu,it. 647 955 let 〈id,ty〉 ≝ it in 648 do s ← s;649 do t ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);650 match t with651 [ Local ⇒ OK ? s652  Stack n ⇒ 956 do 〈s,u〉 with Is ← su; 957 do t as E ← lookup' vars id; 958 match t return λx.? → ? with 959 [ Local ⇒ λE. OK (Σs:stmt×tmpgen.?) «〈s,u〉,Is» 960  Stack n ⇒ λE. 653 961 do q ← match access_mode ty with 654 962 [ By_value q ⇒ OK ? q … … 656 964  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 657 965 ]; 658 OK ? (St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s) 659  Global _ ⇒ Error ? [MSG ParamGlobalMixup; CTX ? id] 660 ]) (OK ? s) params. 966 OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, u〉, ?» 967  Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id] 968 ] E) (OK ? s) params. 969 try @conj try @conj try @conj try @conj try @conj try @conj 970 try @I 971 [ @(expr_vars_mp … (λid. local_id_add_tmps_oblivious vars id u)) whd >E @I 972  @(π1 (π1 Is)) 973  @(π2 (π1 Is)) 974  @(π2 Is) 975 ] qed. 976 977 (* 978 lemma local_id_add_local : ∀vars,id,id'. 979 local_id vars id → 980 local_id (add ?? vars id' Local) id. 981 #vars #id #id' #H 982 whd whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ?] cases (identifier_eq ? id id') 983 [ #E < E >lookup_add_hit // 984  #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/ 985 ] qed. 986 *) 987 axiom DuplicateLabel : String. 988 989 definition lenv_list_inv : lenv → lenv → list ident → Prop ≝ 990 λlbls0,lbls,ls. 991 ∀l,l'. lookup_label lbls l = OK ? l' → 992 Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'. 993 994 lemma lookup_label_add : ∀lbls,l,l'. 995 lookup_label (add … lbls l l') l = OK ? l'. 996 #lbls #l #l' whd in ⊢ (??%?) >lookup_add_hit @refl 997 qed. 998 999 lemma lookup_label_miss : ∀lbls,l,l',l0. 1000 l0 ≠ l → 1001 lookup_label (add … lbls l l') l0 = lookup_label lbls l0. 1002 #lbls #l #l' #l0 * #NE 1003 whd in ⊢ (??%%) 1004 >lookup_add_miss 1005 [ @refl  @(eq_identifier_elim ?? l0 l) 1006 [ #E cases (NE E) 1007  #_ @I 1008 ] 1009 ] 1010 qed. 1011 1012 let rec populate_lenv (ls:list ident) (lbls:lenv) (u:universe ?) : res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) ≝ 1013 match ls return λls. res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) with 1014 [ nil ⇒ OK ? «lbls, ?» 1015  cons l t ⇒ 1016 match lookup_label lbls l return λx.lookup_label lbls l = x → ? with 1017 [ OK _ ⇒ λ_. Error ? (msg DuplicateLabel) 1018  Error _ ⇒ λLOOK. 1019 let 〈l',u1〉 ≝ fresh … u in 1020 do lbls1 ← populate_lenv t (add … lbls l l') u1; 1021 OK ? «eject … lbls1, ?» 1022 ] (refl ? (lookup_label lbls l)) 1023 ]. 1024 [ #l #l' #H %2 @H 1025  cases lbls1 #lbls' #I whd in ⊢ (??%?) 1026 #l1 #l1' #E1 @(eq_identifier_elim … l l1) 1027 [ #E %1 %1 @E 1028  #NE cases (I l1 l1' E1) 1029 [ #H %1 %2 @H 1030  #LOOK' %2 >lookup_label_miss in LOOK' /2/ #H @H 1031 ] 1032 ] 1033 ] qed. 1034 1035 definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) ≝ 1036 λbody. 1037 do «lbls, H» ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?); 1038 OK ? «lbls, ?». 1039 #l #l' #E cases (H l l' E) // 1040 whd in ⊢ (??%? → ?) #H destruct 1041 qed. 1042 1043 lemma local_id_split : ∀vars,tmpgen,i. 1044 local_id (add_tmps vars tmpgen) i → 1045 local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen). 1046 #vars #tmpgen #i 1047 whd in ⊢ (?%? → ?) 1048 elim (tmp_env tmpgen) 1049 [ #H %1 @H 1050  * #id #ty #tl #IH 1051 cases (identifier_eq ? i id) 1052 [ #E >E #H %2 whd %1 @refl 1053  * #NE #H cases (IH ?) 1054 [ #H' %1 @H' 1055  #H' %2 %2 @H' 1056  whd in H; whd in H:(match % with [ _ ⇒ ?  _ ⇒ ? ]); 1057 >lookup_add_miss in H; [ #H @H  @eq_identifier_elim // #E cases (NE E) ] 1058 ] 1059 ] 1060 ] qed. 1061 1062 lemma Exists_squeeze : ∀A,P,l1,l2,l3. 1063 Exists A P (l1@l3) → Exists A P (l1@l2@l3). 1064 #A #P #l1 #l2 #l3 #EX 1065 cases (Exists_append … EX) 1066 [ #EX1 @Exists_append_l @EX1 1067  #EX3 @Exists_append_r @Exists_append_r @EX3 1068 ] qed. 661 1069 662 1070 definition translate_function : universe SymbolTag → list (ident×region) → function → res internal_function ≝ 663 1071 λtmpuniverse, globals, f. 664 let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in 1072 do «lbls, Ilbls» ← build_label_env (fn_body f); 1073 let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in 665 1074 let tmp ≝ mk_tmpgen tmpuniverse [ ] in 666 do 〈s,tmp〉 ← translate_statement vartypes tmp (fn_body f);667 do s ← alloc_params vartypes(fn_params f) s;1075 do s ← translate_statement vartypes lbls tmp (fn_body f); 1076 do 〈s,tmp〉 with Is ← alloc_params vartypes lbls ?? (fn_params f) s; 668 1077 OK ? (mk_internal_function 669 1078 (opttyp_of_type (fn_return f)) … … 671 1080 ((tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f))) 672 1081 stacksize 673 s). 1082 s ?). 1083 cases Is * #S #L #TP 1084 @(stmt_P_mp ???? S) 1085 #s1 * #H1 #H2 % 1086 [ @(stmt_vars_mp … H1) 1087 #i #H 1088 cases (local_id_split … H) 1089 [ #H' @Exists_squeeze >map_append 1090 @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i) @H' 1091  skip 1092  * #id #ty #E1 <E1 @refl 1093 ] 1094  #EX @Exists_append_r @Exists_append_l @EX 1095 ] 1096  @(stmt_labels_mp … H2) 1097 #l * #l' #LOOKUP 1098 lapply (Ilbls l' l LOOKUP) #DEFINED 1099 cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex) 1100 #H @H 1101 ] qed. 674 1102 675 1103 definition translate_fundef : universe SymbolTag → list (ident×region) → clight_fundef → res (fundef internal_function) ≝
Note: See TracChangeset
for help on using the changeset viewer.