Changeset 1087 for Deliverables/D3.3/idlookupbranch/Clight/toCminor.ma
 Timestamp:
 Jul 25, 2011, 2:58:10 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/Clight/toCminor.ma
r1078 r1087 153 153 definition var_types ≝ identifier_map SymbolTag var_type. 154 154 155 axiom UndeclaredIdentifier : String. 156 157 definition lookup' ≝ 158 λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id). 159 160 definition local_id : var_types → ident → Prop ≝ 161 λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False  _ ⇒ True ]  _ ⇒ False ]. 162 155 163 (* Note that the semantics allows locals to shadow globals. 156 164 Parameters start out as locals, but get stack allocated if their address … … 168 176 definition characterise_vars : list (ident×region) → function → var_types × nat ≝ 169 177 λglobals, f. 170 let m ≝ foldl ?? (λm,idr. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in 171 let m ≝ foldl ?? (λm,v. add ?? m (\fst v) Local) m (fn_params f) in 178 let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in 172 179 let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in 173 let 〈m,stacksize〉 ≝ fold l ?? (λms,v.180 let 〈m,stacksize〉 ≝ foldr ?? (λv,ms. 174 181 let 〈m,stack_high〉 ≝ ms in 175 182 let 〈id,ty〉 ≝ v in … … 180 187 〈m,stacksize〉. 181 188 189 lemma local_id_add_global : ∀vars,id,r,id'. 190 local_id (add ?? vars id (Global r)) id' → local_id vars id'. 191 #var #id #r #id' 192 whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?] → ?) 193 cases (identifier_eq ? id id') 194 [ #E >E >lookup_add_hit whd in ⊢ (% → ?) * 195  #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/ 196 ] qed. 197 198 lemma local_id_add_miss : ∀vars,id,t,id'. 199 id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'. 200 #vars #id #t #id' #NE 201 whd in ⊢ (% → %) 202 whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ] → match % with [ _ ⇒ ?  _ ⇒ ? ]) 203 >lookup_add_miss 204 [ #H @H  @eq_identifier_elim // #E >E in NE * /2/ ] 205 qed. 206 207 lemma contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e. 208 #A #B * // qed. 209 210 lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y. 211 ((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) → 212 ∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉. 213 #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed. 214 215 include "utilities/extralib.ma". (* for pair_eq1 to work around destruct's excessive normalisation *) 216 217 lemma characterise_vars_all : ∀l,f,vars,n. 218 characterise_vars l f = 〈vars,n〉 → 219 ∀i. local_id vars i → 220 Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f). 221 #globals #f 222 whd in ⊢ (∀_.∀_.??%? → ?) 223 elim (fn_params f @ fn_vars f) 224 [ #vars #n whd in ⊢ (??%? → ?) #E <(pair_eq1 ?????? E) E; #i #H @False_ind 225 elim globals in H 226 [ normalize // 227  * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H) 228 ] 229  * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i 230 cases (identifier_eq ? id i) 231 [ #E' <E' #H % @refl 232  #NE #H whd %2 >(contract_pair var_types nat ?) in E; 233 whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?) 234 cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?) 235 #H' lapply (extract_pair ???????? H') H' * #m0 * #n0 * #EQ #EQ2 236 @(IH m0 n0) 237 [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ 238  2,4: <(pair_eq1 ?????? EQ2) in H #H' @(local_id_add_miss … H') @NE 239 ] 240 ] 241 ] qed. 182 242 183 243 include "Cminor/syntax.ma". … … 186 246 alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)". 187 247 188 axiom UndeclaredIdentifier : String.189 248 axiom BadlyTypedAccess : String. 190 249 axiom BadLvalue : String. … … 324 383 ]. 325 384 385 lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e. 386 expr_vars ? e1 P → 387 expr_vars ? e2 P → 388 translate_binop op ty1 e1 ty2 e2 ty = OK ? e → 389 expr_vars ? e P. 390 #P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2 391 whd in ⊢ (??%? → ?) 392 [ cases (classify_add ty1 ty2) 393 [ 3,4: #z ] whd in ⊢ (??%? → ?) 394 [ generalize in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ])? → ?) 395 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 396 whd in c:(??%?); destruct % [ @H1  % // @H2 ] 397  generalize in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ])? → ?) 398 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 399 whd in c:(??%?); destruct % [ @H2  % // @H1 ] 400  *: #E destruct (E) % try @H1 @H2 401 ] 402  cases (classify_sub ty1 ty2) 403 [ 3,4: #z] whd in ⊢ (??%? → ?) 404 [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ])? → ?) 405 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 406 whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I 407  *: #E destruct (E) % try @H1 try @H2 % // @H2 408 ] 409  cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct 410 % try @H1 @H2 411  cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct 412 % try @H1 @H2 413  cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct 414 % try @H1 @H2 415  6,7,8,9: #E destruct % try @H1 @H2 416  cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2 417  11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2 418 ] qed. 326 419 327 420 (* We'll need to implement proper translation of pointers if we really do memory … … 338 431 ]. 339 432 340 definition translate_ptr : ∀r1,r2. CMexpr (ASTptr r1) → res (CMexpr (ASTptr r2)) ≝ 341 λr1,r2,e. check_region r1 r2 ? e. 342 343 definition translate_cast : type → ∀ty2:type. CMexpr ? → res (CMexpr (typ_of_type ty2)) ≝ 344 λty1,ty2. 345 match ty1 return λx.CMexpr (typ_of_type x) → ? with 433 definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝ 434 λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e. 435 436 notation "hvbox(« term 19 a, break term 19 b»)" 437 with precedence 90 for @{ (dp ?? $a $b) }. 438 439 lemma sig_ok : ∀A:Type[0]. ∀P:A → Prop. ∀x:Σx:A.P x. 440 P x. 441 #A #P * #a #p @p 442 qed. 443 444 definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝ 445 λP,ty1,ty2. 446 match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with 346 447 [ Tint sz1 sg1 ⇒ λe. 347 match ty2 return λx.res ( CMexpr (typ_of_type x)) with448 match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with 348 449 [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e) 349 450  Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu  _ ⇒ Ofloatofint]) e) … … 353 454 ] 354 455  Tfloat sz1 ⇒ λe. 355 match ty2 return λx.res ( CMexpr (typ_of_type x)) with356 [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2  _ ⇒ Ointoffloat sz2 ]) e)357  Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e)(* FIXME *)456 match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with 457 [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2  _ ⇒ Ointoffloat sz2 ]) e, ?» 458  Tfloat sz2 ⇒ OK ? «Op1 ?? Oid e, ?» (* FIXME *) 358 459  _ ⇒ Error ? (msg TypeMismatch) 359 460 ] 360 461  Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *) 361 match ty2 return λx.res ( CMexpr (typ_of_type x)) with362 [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ointofptr sz2) e)363  Tarray r2 _ _ ⇒ translate_ptr r1 r2 e364  Tpointer r2 _ ⇒ translate_ptr r1 r2 e462 match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with 463 [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2) e, ?» 464  Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e 465  Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e 365 466  _ ⇒ Error ? (msg TypeMismatch) 366 467 ] 367 468  Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *) 368 match ty2 return λx.res ( CMexpr (typ_of_type x)) with369 [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e)370  Tarray r2 _ _ ⇒ translate_ptr r1 r2 e371  Tpointer r2 _ ⇒ translate_ptr r1 r2 e469 match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with 470 [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e, ?» 471  Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e 472  Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e 372 473  _ ⇒ Error ? (msg TypeMismatch) 373 474 ] 374 475  _ ⇒ λ_. Error ? (msg TypeMismatch) 375 ]. 476 ]. whd @sig_ok qed. 376 477 377 478 definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝ … … 404 505 ] qed. 405 506 406 let rec translate_expr (vars:var_types) (e:expr) on e : res (CMexpr (typ_of_type (typeof e))) ≝ 407 match e return λe. res (CMexpr (typ_of_type (typeof e))) with 507 definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B. 508 match f return λx. f = x → ? with 509 [ OK x ⇒ g x 510  Error msg ⇒ λ_. Error ? msg 511 ] (refl ? f). 512 513 notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}. 514 515 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)) ≝ 516 match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with 408 517 [ Expr ed ty ⇒ 409 518 match ed with 410 [ Econst_int sz i ⇒ OK ? (Cst ? (Ointconst sz i))411  Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))519 [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?» 520  Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?» 412 521  Evar id ⇒ 413 do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);414 match c with415 [ Global r ⇒ 522 do c as E ← lookup' vars id; 523 match c return λx.? = ? → res (Σe':CMexpr ?. ?) with 524 [ Global r ⇒ λ_. 416 525 match access_mode ty with 417 [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id 0)))418  By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id 0))526 [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?» 527  By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?» 419 528  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 420 529 ] 421  Stack n ⇒ 530  Stack n ⇒ λE. 422 531 match access_mode ty with 423 [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack n)))424  By_reference _ ⇒ OK ? (Cst ? (Oaddrstack n))532 [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?» 533  By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?» 425 534  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 426 535 ] 427  Local ⇒ OK ? (Id ? id)428 ] 536  Local ⇒ λE. OK ? «Id ? id, ?» 537 ] E 429 538  Ederef e1 ⇒ 430 539 do e1' ← translate_expr vars e1; 431 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with540 match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with 432 541 [ ASTptr r ⇒ λe1'. 433 match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with 434 [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1') 435  By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉ 542 match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with 543 [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (eject … e1'), ?» 544  By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1'; 545 OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉ 436 546  By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) 437 ] ( refl ? (access_mode ty))547 ] (access_mode_typ ty) 438 548  _ ⇒ λ_. Error ? (msg TypeMismatch) 439 549 ] e1' 440 550  Eaddrof e1 ⇒ 441 551 do e1' ← translate_addr vars e1; 442 match typ_of_type ty return λx.res ( CMexpr x) with552 match typ_of_type ty return λx.res (Σz:CMexpr x.?) with 443 553 [ ASTptr r ⇒ 444 554 match e1' with … … 450 560 do op' ← translate_unop ty op; 451 561 do e1' ← translate_expr vars e1; 452 OK ? (Op1 ?? op' e1')562 OK ? «Op1 ?? op' e1', ?» 453 563  Ebinop op e1 e2 ⇒ 454 564 do e1' ← translate_expr vars e1; 455 565 do e2' ← translate_expr vars e2; 456 translate_binop op (typeof e1) e1' (typeof e2) e2' ty 566 do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty; 567 OK ? «e', ?» 457 568  Ecast ty1 e1 ⇒ 458 569 do e1' ← translate_expr vars e1; 459 do e' ← translate_cast (typeof e1) ty1 e1'; 460 typ_should_eq ? (typ_of_type ty) ? e' 570 do e' ← translate_cast ? (typeof e1) ty1 e1'; 571 do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e'; 572 OK ? e' 461 573  Econdition e1 e2 e3 ⇒ 462 574 do e1' ← translate_expr vars e1; 463 575 do e2' ← translate_expr vars e2; 464 do e2' ← type_should_eq ? ty (λx. CMexpr (typ_of_type x)) e2';576 do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; 465 577 do e3' ← translate_expr vars e3; 466 do e3' ← type_should_eq ? ty (λx. CMexpr (typ_of_type x)) e3';467 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with468 [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' e3')578 do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3'; 579 match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with 580 [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?» 469 581  _ ⇒ λ_.Error ? (msg TypeMismatch) 470 582 ] e1' … … 474 586 match ty with 475 587 [ Tint sz _ ⇒ 476 do e2' ← type_should_eq ? ty (λx. CMexpr (typ_of_type x)) e2';477 match typ_of_type (typeof e1) return λx. CMexpr x → res (CMexpr (typ_of_type ty))with478 [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))))588 do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; 589 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with 590 [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))), ?» 479 591  _ ⇒ λ_.Error ? (msg TypeMismatch) 480 592 ] e1' … … 486 598 match ty with 487 599 [ Tint sz _ ⇒ 488 do e2' ← type_should_eq ? ty (λx. CMexpr (typ_of_type x)) e2';489 match typ_of_type (typeof e1) return λx. CMexpr x → res (CMexpr (typ_of_type ty))with490 [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2')600 do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; 601 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with 602 [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?» 491 603  _ ⇒ λ_.Error ? (msg TypeMismatch) 492 604 ] e1' … … 495 607  Esizeof ty1 ⇒ 496 608 match ty with 497 [ Tint sz _ ⇒ OK ? (Cst ? (Ointconst sz (repr ? (sizeof ty1))))609 [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?» 498 610  _ ⇒ Error ? (msg TypeMismatch) 499 611 ] 500 612  Efield e1 id ⇒ 501 do e' ←match typeof e1 with613 match typeof e1 with 502 614 [ Tstruct _ fl ⇒ 503 615 do e1' ← translate_addr vars e1; … … 506 618 do off ← field_offset id fl; 507 619 match access_mode ty with 508 [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))509  By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))))620 [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?» 621  By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?» 510 622  By_nothing ⇒ Error ? (msg BadlyTypedAccess) 511 623 ] … … 515 627 match e1' with 516 628 [ dp r e1' ⇒ 517 match access_mode ty return λx. access_mode ty = x → res (CMexpr (typ_of_type ty)) with 518 [ By_value q ⇒ λ_. OK ? (Mem ?? q e1') 519  By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈res (CMexpr (ASTptr r')) ↦ res (CMexpr (typ_of_type ty))⌉ 629 match access_mode ty return λx. access_mode ty = x → res ? with 630 [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?» 631  By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1'; 632 OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉ 520 633  By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) 521 634 ] (refl ? (access_mode ty)) 522 635 ] 523 636  _ ⇒ Error ? (msg BadlyTypedAccess) 524 ]; 525 typ_should_eq ? (typ_of_type ty) ? e' 637 ] 526 638  Ecost l e1 ⇒ 527 639 do e1' ← translate_expr vars e1; 528 do e' ← OK ? (Ecost ? l e1');529 typ_should_eq ? (typ_of_type ty) ?e'640 do e' ← OK ? «Ecost ? l e1',?»; 641 typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e' 530 642 ] 531 ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. CMexpr (ASTptr r)) ≝643 ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝ 532 644 match e with 533 645 [ Expr ed _ ⇒ … … 535 647 [ Evar id ⇒ 536 648 do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id); 537 match c return λ_. res (Σr. CMexpr (ASTptr r)) with538 [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0)))539  Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack n)))649 match c return λ_. res (Σr.Σz:CMexpr (ASTptr r).?) with 650 [ Global r ⇒ OK ? «r, «Cst ? (Oaddrsymbol id 0), ?»» 651  Stack n ⇒ OK ? «Any, «Cst ? (Oaddrstack n), ?»» 540 652  Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *) 541 653 ] 542 654  Ederef e1 ⇒ 543 655 do e1' ← translate_expr vars e1; 544 match typ_of_type (typeof e1) return λx. CMexpr x → res (Σr. CMexpr (ASTptr r)) with545 [ ASTptr r ⇒ λe1'.OK ? (dp ?? r e1')656 match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σr. Σz:CMexpr (ASTptr r). ?) with 657 [ ASTptr r ⇒ λe1'.OK ? «r, e1'» 546 658  _ ⇒ λ_.Error ? (msg BadlyTypedAccess) 547 659 ] e1' … … 552 664 do off ← field_offset id fl; 553 665 match e1' with 554 [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))666 [ 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))), ?» ») 555 667 ] 556 668  Tunion _ _ ⇒ translate_addr vars e1 … … 560 672 ] 561 673 ]. 562 >(access_mode_typ … E) @refl 563 qed. 564 565 inductive destination : Type[0] ≝ 566  IdDest : ident → destination 567  MemDest : ∀r:region. memory_chunk → CMexpr (ASTptr r) → destination. 674 whd try @I 675 [ >E @I 676  >(E ? (refl ??)) @refl 677  3,4: @sig_ok 678  @(translate_binop_vars … E) @sig_ok 679  % [ % ] @sig_ok 680  % [ % @sig_ok ] whd @I 681  % [ % [ @sig_ok  @I ]  @sig_ok ] 682  % [ @sig_ok  @I ] 683  % [ @sig_ok  @I ] 684  >(access_mode_typ … E) @refl 685  @sig_ok 686  @sig_ok 687  % [ @sig_ok  @I ] 688 ] qed. 689 690 inductive destination (vars:var_types) : Type[0] ≝ 691  IdDest : ∀id:ident. local_id vars id → destination vars 692  MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars. 568 693 569 694 definition translate_dest ≝ … … 578 703 match ed1 with 579 704 [ Evar id ⇒ 580 do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);581 match c with582 [ Local ⇒ OK ? (IdDest id)583  Global r ⇒ OK ? (MemDestr q (Cst ? (Oaddrsymbol id 0)))584  Stack n ⇒ OK ? (MemDestAny q (Cst ? (Oaddrstack n)))585 ] 705 do c as E ← lookup' vars id; 706 match c return λx.? → ? with 707 [ Local ⇒ λE. OK ? (IdDest vars id ?) 708  Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0))) 709  Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n))) 710 ] E 586 711  _ ⇒ 587 712 do e1' ← translate_addr vars e1; 588 match e1' with [ dp r e1' ⇒ OK ? (MemDest r q e1') ]713 match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ] 589 714 ] 590 715 ]. 716 whd // >E @I 717 qed. 591 718 (* 592 719 definition translate_assign ≝ … … 614 741 ]. 615 742 *) 616 definition translate_assign ≝743 definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.stmt_vars s (local_id vars)) ≝ 617 744 λvars,e1,e2. 618 745 do e2' ← translate_expr vars e2; 619 746 do dest ← translate_dest vars e1 (typeof e2); 620 747 match dest with 621 [ IdDest id ⇒ OK ? (St_assign ? id e2') 622  MemDest r q e1' ⇒ OK ? (St_store ? r q e1' e2') 623 ]. 748 [ IdDest id p ⇒ OK ? «St_assign ? id e2', ?» 749  MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?» 750 ]. 751 whd 752 [ % // @sig_ok 753  % @sig_ok 754 ] qed. 624 755 625 756 definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝ … … 630 761 ]. 631 762 632 definition translate_expr_sigma : var_types → expr → res (Σt:typ.CMexpr t) ≝763 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) ]) ≝ 633 764 λv,e. 634 765 do e' ← translate_expr v e; 635 OK ? (dp ? (λt:typ.CMexpr t) ? e'). 766 OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?». 767 whd @sig_ok 768 qed. 636 769 637 770 axiom FIXME : String. 638 771 639 let rec translate_statement (vars:var_types) (tmp:ident) (tmpp:ident) (s:statement) on s : res stmt ≝ 772 let rec mmap_sigma (A,B:Type[0]) (P:B → Prop) (f:A → res (Σx:B.P x)) (l:list A) on l : res (Σl':list B.All B P l') ≝ 773 match l with 774 [ nil ⇒ OK ? «nil B, ?» 775  cons h t ⇒ 776 do h' ← f h; 777 do t' ← mmap_sigma A B P f t; 778 OK ? «cons B h' t', ?» 779 ]. 780 whd // % 781 [ @(sig_ok B P) 782  cases t' #l' #p @p 783 ] qed. 784 785 let rec translate_statement (vars:var_types) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs:stmt.stmt_vars s (local_id vars)) ≝ 640 786 match s with 641 [ Sskip ⇒ OK ? St_skip787 [ Sskip ⇒ OK ? «St_skip, ?» 642 788  Sassign e1 e2 ⇒ translate_assign vars e1 e2 643 789  Scall ret ef args ⇒ 644 790 do ef' ← translate_expr vars ef; 645 do ef' ← typ_should_eq ?(ASTptr Code) ? ef';646 do args' ← mmap … (translate_expr_sigma vars) args;791 do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef'; 792 do args' ← mmap_sigma … (translate_expr_sigma vars) args; 647 793 match ret with 648 [ None ⇒ OK ? (St_call (None ?) ef' args')794 [ None ⇒ OK ? «St_call (None ?) ef' args', ?» 649 795  Some e1 ⇒ 650 796 do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *) 651 797 match dest with 652 [ IdDest id ⇒ OK ? (St_call (Some ? id) ef' args')798 [ IdDest id p ⇒ OK ? «St_call (Some ? id) ef' args', ?» 653 799  MemDest r q e1' ⇒ 654 800 let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp  _ ⇒ tmp ] in 655 OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)))801 OK ? «St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), ?» 656 802 ] 657 803 ] … … 659 805 do s1' ← translate_statement vars tmp tmpp s1; 660 806 do s2' ← translate_statement vars tmp tmpp s2; 661 OK ? (St_seq s1' s2')807 OK ? «St_seq s1' s2', ?» 662 808  Sifthenelse e1 s1 s2 ⇒ 663 809 do e1' ← translate_expr vars e1; 664 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with810 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 665 811 [ ASTint _ _ ⇒ λe1'. 666 812 do s1' ← translate_statement vars tmp tmpp s1; 667 813 do s2' ← translate_statement vars tmp tmpp s2; 668 OK ? (St_ifthenelse ?? e1' s1' s2')814 OK ? «St_ifthenelse ?? e1' s1' s2', ?» 669 815  _ ⇒ λ_.Error ? (msg TypeMismatch) 670 816 ] e1' 671 817  Swhile e1 s1 ⇒ 672 818 do e1' ← translate_expr vars e1; 673 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with819 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 674 820 [ ASTint _ _ ⇒ λe1'. 675 821 do s1' ← translate_statement vars tmp tmpp s1; 676 822 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 677 OK ? (St_block823 OK ? «St_block 678 824 (St_loop 679 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))) )825 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), ?» 680 826  _ ⇒ λ_.Error ? (msg TypeMismatch) 681 827 ] e1' 682 828  Sdowhile e1 s1 ⇒ 683 829 do e1' ← translate_expr vars e1; 684 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with830 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with 685 831 [ ASTint _ _ ⇒ λe1'. 686 832 do s1' ← translate_statement vars tmp tmpp s1; 687 833 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 688 OK ? (St_block834 OK ? «St_block 689 835 (St_loop 690 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))) )836 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), ?» 691 837  _ ⇒ λ_.Error ? (msg TypeMismatch) 692 838 ] e1' 693 839  Sfor s1 e1 s2 s3 ⇒ 694 840 do e1' ← translate_expr vars e1; 695 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with841 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with 696 842 [ ASTint _ _ ⇒ λe1'. 697 843 do s1' ← translate_statement vars tmp tmpp s1; … … 699 845 do s3' ← translate_statement vars tmp tmpp s3; 700 846 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 701 OK ? (St_seq s1'847 OK ? «St_seq s1' 702 848 (St_block 703 849 (St_loop 704 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))) )850 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), ?» 705 851  _ ⇒ λ_.Error ? (msg TypeMismatch) 706 852 ] e1' 707  Sbreak ⇒ OK ? (St_exit 1)708  Scontinue ⇒ OK ? (St_exit 0)853  Sbreak ⇒ OK ? «St_exit 1, ?» 854  Scontinue ⇒ OK ? «St_exit 0, ?» 709 855  Sreturn ret ⇒ 710 856 match ret with 711 [ None ⇒ OK ? (St_return (None ?))857 [ None ⇒ OK ? «St_return (None ?), ?» 712 858  Some e1 ⇒ 713 859 do e1' ← translate_expr vars e1; 714 OK ? (St_return (Some ? (dp … e1')))860 OK ? «St_return (Some ? (dp … e1')), ?» 715 861 ] 716 862  Sswitch e1 ls ⇒ Error ? (msg FIXME) 717 863  Slabel l s1 ⇒ 718 864 do s1' ← translate_statement vars tmp tmpp s1; 719 OK ? (St_label l s1')720  Sgoto l ⇒ OK ? (St_goto l)865 OK ? «St_label l s1', ?» 866  Sgoto l ⇒ OK ? «St_goto l, ?» 721 867  Scost l s1 ⇒ 722 868 do s1' ← translate_statement vars tmp tmpp s1; 723 OK ? (St_cost l s1') 724 ]. 869 OK ? «St_cost l s1', ?» 870 ]. 871 whd try @I 872 [ % [ % [ @p  @sig_ok ]  @(sig_ok ? (All ??)) ] 873  % [ whd % [ % [ @sig_ok  @sig_ok ]  @(sig_ok ? (All ??)) ]  whd % @sig_ok ] 874  % [ % [ @I  @sig_ok ]  @(sig_ok ? (All ??)) ] 875  % @sig_ok 876  % [ % @sig_ok  @sig_ok ] 877  % [ % @sig_ok  whd @I ] 878  % [ @sig_ok  whd % [ % [ @sig_ok  @I ]  @I ] ] 879  % [ @sig_ok  whd % [ % [ @sig_ok  whd % @sig_ok ]  @I ] ] 880  @sig_ok 881  @sig_ok 882  @sig_ok 883 ] qed. 725 884 726 885 axiom ParamGlobalMixup : String. 727 886 728 definition alloc_params : var_types → list (ident×type) → stmt → res stmt≝887 definition alloc_params : ∀vars:var_types. list (ident×type) → (Σs:stmt.stmt_vars s (local_id vars)) → res (Σs:stmt.stmt_vars s (local_id vars)) ≝ 729 888 λvars,params,s. foldl ?? (λs,it. 730 889 let 〈id,ty〉 ≝ it in 731 890 do s ← s; 732 do t ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);733 match t with734 [ Local ⇒ OK ?s735  Stack n ⇒ 891 do t as E ← lookup' vars id; 892 match t return λx.? → ? with 893 [ Local ⇒ λE. OK (Σs:stmt.?) s 894  Stack n ⇒ λE. 736 895 do q ← match access_mode ty with 737 896 [ By_value q ⇒ OK ? q … … 739 898  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 740 899 ]; 741 OK ? (St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s) 742  Global _ ⇒ Error ? [MSG ParamGlobalMixup; CTX ? id] 743 ]) (OK ? s) params. 900 OK ? «St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, ?» 901  Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id] 902 ] E) (OK ? s) params. 903 whd % [ whd % [ @I  whd >E @I ]  @sig_ok ] 904 qed. 744 905 745 906 definition bigid1 ≝ an_identifier SymbolTag [[ … … 754 915 false;false;false;true]]. 755 916 917 lemma Exists_rm : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2). 918 #A #P #l1 #x #l2 elim l1 919 [ normalize #H %2 @H 920  #h #t #IH normalize * [ #H %1 @H  #H %2 @IH @H ] 921 qed. 922 923 lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2). 924 #A #P #l1 #x #l2 #H elim l1 925 [ %1 @H 926  #h #t #IH %2 @IH 927 ] qed. 928 929 lemma Exists_map : ∀A,B,P,Q,f,l. 930 Exists A P l → 931 (∀a.P a → Q (f a)) → 932 Exists B Q (map A B f l). 933 #A #B #P #Q #f #l elim l // 934 #h #t #IH * [ #H #F %1 @F @H  #H #F %2 @IH [ @H  @F ] ] qed. 935 936 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)" 937 with precedence 10 938 for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒ 939 λ${ident E}.$s ] (refl ? $t) }. 940 941 lemma local_id_add_local : ∀vars,id,id'. 942 local_id vars id → 943 local_id (add ?? vars id' Local) id. 944 #vars #id #id' #H 945 whd whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ?] cases (identifier_eq ? id id') 946 [ #E < E >lookup_add_hit // 947  #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/ 948 ] qed. 949 756 950 (* FIXME: the temporary handling is nonsense, I'm afraid. *) 757 951 definition translate_function : list (ident×region) → function → res internal_function ≝ 758 952 λglobals, f. 759 let 〈vartypes , stacksize〉≝ characterise_vars globals f in953 let 〈vartypes0, stacksize〉 as E ≝ characterise_vars globals f in 760 954 let tmp ≝ bigid1 in (* FIXME *) 761 955 let tmpp ≝ bigid2 in (* FIXME *) 956 let vartypes ≝ add … (add … vartypes0 tmp Local) tmpp Local in 762 957 do s ← translate_statement vartypes tmp tmpp (fn_body f); 763 958 do s ← alloc_params vartypes (fn_params f) s; … … 767 962 (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f))) 768 963 stacksize 769 s). 964 s ?). 965 [ whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) >lookup_add_hit % 966  whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit % % ] 967  @stmt_vars_mp [ 3: @sig_ok  skip ] 968 #i #H cases (identifier_eq ? tmp i) 969 [ #E <E @Exists_mid @refl 970  #NE1 @Exists_rm cases (identifier_eq ? tmpp i) 971 [ #E <E @Exists_mid @refl 972  #NE2 @Exists_rm 973 >map_append 974 @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i) 975 @(local_id_add_miss ?? Local ? NE1) 976 @(local_id_add_miss ?? Local ? NE2) @H 977  skip 978  * #id #ty #E1 <E1 @refl 979 ] 980 ] 981 ] 982 ] qed. 770 983 771 984 definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
Note: See TracChangeset
for help on using the changeset viewer.