Changeset 2722 for src/common
 Timestamp:
 Feb 23, 2013, 5:05:03 PM (7 years ago)
 Location:
 src/common
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Globalenvs.ma
r2645 r2722 425 425 qed. 426 426 427 427 428 lemma symbol_of_block_rev : ∀F,genv,b,id. 428 429 symbol_for_block F genv b = Some ? id → … … 439 440  #_ * 440 441 ] 442 ] qed. 443 444 lemma symbol_of_block_rev' : ∀F,genv,b. 445 symbol_for_block F genv b = None ? → 446 find_funct_ptr F genv b = None ?. 447 #F #genv * * [ //  // ] #b #H 448 whd in ⊢ (??%?); 449 lapply (functions_inv ? genv b) 450 cases (lookup_opt F b ?) // 451 #f #H' cases (H' ?) 452 [ #id #E whd in H:(??%?); 453 lapply (find_none ?? (symbols … genv) (λid,b'. eq_block (mk_block (neg b)) b') id (mk_block (neg b))) 454 cases (find ????) in H ⊢ %; 455 [ normalize #_ #H lapply (H (refl ??) E) >eqb_n_n * 456  * #id' #b' normalize #E destruct 457 ] 458  % #E destruct 441 459 ] qed. 442 460 … … 459 477  * #id' #b' #_ normalize #_ #E destruct 460 478 ] qed. 479 480 lemma symbol_of_function_block_ok : ∀F,ge,b,FFP,id. 481 symbol_of_function_block F ge b FFP = id → 482 symbol_for_block F ge b = Some ? id. 483 #F #ge #b #FFP #id whd in ⊢ (??%? → ?); 484 generalize in match (refl ? (symbol_for_block F ge b)); 485 lapply (symbol_of_block_rev' F ge b) 486 cases (symbol_for_block F ge b) in ⊢ (% → ???% → ??(match % with [_⇒?_⇒?]?)? → ?); 487 [ #H @⊥ >(H (refl ??)) in FFP; * /2/ 488  #id' #_ #E normalize in ⊢ (% → ?); #E' destruct @E 489 ] qed. 490 491 definition symbol_of_function_block' : ∀F,ge,b,f. find_funct_ptr F ge b = Some ? f → ident ≝ 492 λF,ge,b,f,FFP. symbol_of_function_block F ge b ?. 493 >FFP % #E destruct 494 qed. 495 496 definition find_funct_ptr_id : ∀F:Type[0]. genv_t F → block → option (F × ident) ≝ 497 λF:Type[0].λge:genv_t F.λb:block. 498 match find_funct_ptr F ge b return λx:option F. ? = x → option (F × ident) with 499 [ None ⇒ λ_. None ? 500  Some f ⇒ λFFP. Some ? 〈f,symbol_of_function_block' F ge b f FFP〉 501 ] (refl ??). 502 503 lemma find_funct_ptr_id_drop : ∀F,ge,b,f,id. 504 find_funct_ptr_id F ge b = Some ? 〈f,id〉 → 505 find_funct_ptr F ge b = Some ? f. 506 #F #ge #b #f #id whd in ⊢ (??%? → ?); 507 generalize in match (refl ??); 508 cases (find_funct_ptr F ge b) in ⊢ (???% → ??(match % with [_⇒?_⇒?] ?)? → %); 509 [ #X #E normalize in E; destruct 510  #f' #ID #E whd in E:(??%?); destruct % 511 ] qed. 512 513 coercion ffpi_drop : 514 ∀F,ge,b,f,id. 515 ∀FFP:find_funct_ptr_id F ge b = Some ? 〈f,id〉. 516 find_funct_ptr F ge b = Some ? f ≝ find_funct_ptr_id_drop 517 on _FFP:eq (option ?) ?? to eq (option ?) ??. 518 519 lemma find_funct_ptr_id_inv : ∀F,ge,b,f,id. 520 find_funct_ptr_id F ge b = Some ? 〈f,id〉 → 521 find_funct_ptr F ge b = Some ? f ∧ 522 symbol_for_block F ge b = Some ? id. 523 #F #ge #b #f #id whd in ⊢ (??%? → ?); 524 generalize in match (refl ??); 525 cases (find_funct_ptr F ge b) in ⊢ (???% → ??(match % with [_⇒?_⇒?] ?)? → %); 526 [ #X #E normalize in E; destruct 527  #f' #FFP #E whd in E:(??%?); % 528 [ destruct % 529  @(symbol_of_function_block_ok F ge b ? id) 530 [ >FFP % #E' destruct 531  destruct % 532 ] 533 ] 534 ] qed. 535 536 lemma make_find_funct_ptr_id : ∀F,ge,b,f,id. 537 find_funct_ptr F ge b = Some ? f → 538 symbol_for_block F ge b = Some ? id → 539 find_funct_ptr_id F ge b = Some ? 〈f,id〉. 540 #F #ge #b #f #id #FFP #SYM 541 whd in ⊢ (??%?); generalize in match (refl ??); 542 >FFP in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)?); 543 #FFP' whd in ⊢ (??%?); 544 @eq_f @eq_f 545 whd in ⊢ (??%?); 546 generalize in match (refl ? (symbol_for_block F ge b)); 547 >SYM in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)?); 548 #SYM' whd in ⊢ (??%?); % 549 qed. 550 551 definition symbol_of_function_val : ∀F,ge,v. find_funct F ge v ≠ None ? → ident ≝ 552 λF,ge,v. 553 match v return λv. find_funct F ge v ≠ None ? → ident with 554 [ Vptr p ⇒ λH. symbol_of_function_block F ge (pblock p) ? 555  _ ⇒ λH. ⊥ 556 ]. 557 try (cases H #H' cases (H' (refl ??))) 558 lapply H 559 whd in match (find_funct ???); 560 @eq_offset_elim 561 [ #_ #H' @H' 562  #X * #H' cases (H' (refl ??)) 563 ] qed. 564 565 definition symbol_of_function_val' : ∀F,ge,v,f. find_funct F ge v = Some ? f → ident ≝ 566 λF,ge,v,f,FF. symbol_of_function_val F ge v ?. 567 >FF % #E destruct 568 qed. 569 570 definition find_funct_id : ∀F:Type[0]. genv_t F → val → option (F × ident) ≝ 571 λF:Type[0].λge:genv_t F.λv:val. 572 match find_funct F ge v return λx:option F. ? = x → option (F × ident) with 573 [ None ⇒ λ_. None ? 574  Some f ⇒ λFF. Some ? 〈f,symbol_of_function_val' F ge v f FF〉 575 ] (refl ??). 576 577 lemma find_funct_id_drop : ∀F,ge,v,f,id. 578 find_funct_id F ge v = Some ? 〈f,id〉 → 579 find_funct F ge v = Some ? f. 580 #F #ge #v #f #id whd in ⊢ (??%? → ?); 581 generalize in match (refl ??); 582 cases (find_funct F ge v) in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)? → ?); 583 [ #X #E normalize in E; destruct 584  #f' #ID #E whd in E:(??%?); destruct assumption 585 ] qed. 586 587 coercion ffi_drop : 588 ∀F,ge,v,f,id. 589 ∀FF:find_funct_id F ge v = Some ? 〈f,id〉. 590 find_funct F ge v = Some ? f ≝ find_funct_id_drop 591 on _FF:eq (option ?) ?? to eq (option ?) ??. 592 593 lemma find_funct_id_ptr : ∀F,ge,v,f,id. 594 find_funct_id F ge v = Some ? 〈f,id〉 → 595 ∃b. v = Vptr (mk_pointer b zero_offset) ∧ 596 find_funct_ptr_id F ge b = Some ? 〈f,id〉. 597 #F #ge #v #f #id whd in ⊢ (??%? → ?); 598 generalize in match (refl ??); 599 cases (find_funct F ge v) in ⊢ (???% → ??(match % with [_⇒?_⇒?] ?)? → %); 600 [ #X #E normalize in E; destruct 601  #f' #FF #E whd in E:(??%?); 602 cases (find_funct_find_funct_ptr ???? FF) #b * #E1 #FFP %{b} %{E1} 603 whd in ⊢ (??%?); 604 generalize in match (refl ??); 605 >FFP in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)?); 606 #FFP' whd in ⊢ (??%?); <E 607 @eq_f @eq_f >E1 in FF E ⊢ %; #FF #E % 608 ] qed. 609 610 lemma find_funct_ptr_id_conv : ∀F,ge,b,f,id. 611 find_funct_ptr_id F ge b = Some ? 〈f,id〉 → 612 find_funct_id F ge (Vptr (mk_pointer b zero_offset)) = Some ? 〈f,id〉. 613 #F #ge * * [2,3:#b] #f #id 614 whd in ⊢ (??%? → ??%?); #E destruct 615 @E 616 qed. 461 617 462 618 (* … … 943 1099 qed. 944 1100 1101 lemma symbols_match: 1102 ∀M:matching. 1103 ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → 1104 ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). 1105 match_program … M p p' → 1106 symbols ? (globalenv … initW p') = symbols ? (globalenv … initV p). 1107 * #A #B #V #W #match_fun #match_var #initV #initW #initsize 1108 * #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain 1109 whd in match (globalenv ????); whd in match (globalenv_allocmem ????); 1110 whd in match (globalenv ????); whd in match (globalenv_allocmem ????); 1111 change with (add_globals ?????) in match (foldl ?????); 1112 change with (add_globals ?????) in match (foldl ? (ident×region×V) ???); 1113 @sym_eq 1114 @(proj1 … (add_globals_match … Mvars)) 1115 [ @(matching_fns_get_same_blocks … Mfns) 1116 #f #g @match_funct_entry_id 1117  * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %  @(initsize … MVE) ] 1118 ] qed. 1119 945 1120 lemma 946 1121 find_symbol_match: … … 951 1126 ∀s: ident. 952 1127 find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s. 953 * #A #B #V #W #match_fun #match_var #initV #initW #initsize 954 * #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain #s 955 whd in ⊢ (??%%); 956 @sym_eq 957 @(eq_f ??(λx. lookup SymbolTag block x s)) 958 whd in match (globalenv ????); whd in match (globalenv_allocmem ????); 959 whd in match (globalenv ????); whd in match (globalenv_allocmem ????); 960 change with (add_globals ?????) in match (foldl ?????); 961 change with (add_globals ?????) in match (foldl ? (ident×region×V) ???); 962 @(proj1 … (add_globals_match … Mvars)) 963 [ @(matching_fns_get_same_blocks … Mfns) 964 #f #g @match_funct_entry_id 965  * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %  @(initsize … MVE) ] 966 ] qed. 1128 #M #initV #initW #initsize #p1 #p2 #MATCH #s 1129 whd in ⊢ (??%%); >(symbols_match M … initsize … MATCH) % 1130 qed. 967 1131 968 1132 lemma … … 1118 1282 rg_find_symbol: ∀s. 1119 1283 find_symbol … ge s = find_symbol … ge' s; 1284 rg_symbol_for : ∀b. 1285 symbol_for_block … ge b = symbol_for_block … ge' b; 1120 1286 rg_find_funct: ∀v,f. 1121 1287 find_funct … ge v = Some ? f → … … 1126 1292 }. 1127 1293 1294 lemma rg_find_funct_id : ∀A,B,t,ge,ge'. ∀RG:related_globals A B t ge ge'. ∀v,f,id. 1295 find_funct_id … ge v = Some ? 〈f,id〉 → 1296 find_funct_id … ge' v = Some ? 〈t f,id〉. 1297 #A #B #t #ge #ge' #RG #v #f #id #FFI 1298 cases (find_funct_id_ptr ????? FFI) 1299 #b * #E1 #FFPI 1300 cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM 1301 lapply (rg_find_funct_ptr … RG … FFP) #FFP' 1302 >(rg_symbol_for … RG b) in SYM; #SYM' 1303 lapply (make_find_funct_ptr_id … FFP' SYM') 1304 >E1 @find_funct_ptr_id_conv 1305 qed. 1306 1307 lemma rg_find_funct_ptr_id : ∀A,B,t,ge,ge'. ∀RG:related_globals A B t ge ge'. ∀b,f,id. 1308 find_funct_ptr_id … ge b = Some ? 〈f,id〉 → 1309 find_funct_ptr_id … ge' b = Some ? 〈t f,id〉. 1310 #A #B #t #ge #ge' #RG #b #f #id #FFPI 1311 cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM 1312 lapply (rg_find_funct_ptr … RG … FFP) #FFP' 1313 >(rg_symbol_for … RG b) in SYM; #SYM' 1314 @(make_find_funct_ptr_id … FFP' SYM') 1315 qed. 1316 1317 1318 1128 1319 theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs. 1129 1320 related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)). 1130 1321 #A #B #V #iV #p #tf % 1131 1322 [ #s @sym_eq @(find_symbol_transf A B V iV tf p) 1323  #b whd in ⊢ (??%%); >(symbols_match … (transform_program_match … tf ?)) 1324 [ %  #v #w * #id #r #v1 #v2 #E destruct %  skip ] 1132 1325  @(find_funct_transf A B V iV tf p) 1133 1326  @(find_funct_ptr_transf A B V iV p tf) … … 1137 1330 rgg_find_symbol: ∀s. 1138 1331 find_symbol … ge s = find_symbol … ge' s; 1332 rgg_symbol_for : ∀b. 1333 symbol_for_block … ge b = symbol_for_block … ge' b; 1139 1334 rgg_find_funct_ptr: ∀b,f. 1140 1335 find_funct_ptr … ge b = Some ? f → … … 1145 1340 }. 1146 1341 1342 lemma rgg_find_funct_id : ∀tag,A,B,t,ge,ge'. ∀RG:related_globals_gen tag A B t ge ge'. ∀v,f,id. 1343 find_funct_id … ge v = Some ? 〈f,id〉 → 1344 ∃g. find_funct_id … ge' v = Some ? 〈\fst (t g f),id〉. 1345 #tag #A #B #t #ge #ge' #RG #v #f #id #FFI 1346 cases (find_funct_id_ptr ????? FFI) 1347 #b * #E1 #FFPI 1348 cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM 1349 cases (rgg_find_funct_ptr … RG … FFP) #g #FFP' %{g} 1350 >(rgg_symbol_for … RG b) in SYM; #SYM' 1351 lapply (make_find_funct_ptr_id … FFP' SYM') 1352 >E1 @find_funct_ptr_id_conv 1353 qed. 1354 1355 lemma rgg_find_funct_ptr_id : ∀tag,A,B,t,ge,ge'. ∀RG:related_globals_gen tag A B t ge ge'. ∀b,f,id. 1356 find_funct_ptr_id … ge b = Some ? 〈f,id〉 → 1357 ∃g. find_funct_ptr_id … ge' b = Some ? 〈\fst (t g f),id〉. 1358 #tag #A #B #t #ge #ge' #RG #b #f #id #FFPI 1359 cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM 1360 cases (rgg_find_funct_ptr … RG … FFP) #g #FFP' %{g} 1361 >(rgg_symbol_for … RG b) in SYM; #SYM' 1362 @(make_find_funct_ptr_id … FFP' SYM') 1363 qed. 1364 1147 1365 include "utilities/extra_bool.ma". 1148 1366 … … 1152 1370 [ #s @sym_eq @(find_symbol_match … (transform_program_gen_match … tf p)) 1153 1371 #v #w * // 1372  #b whd in ⊢ (??%%); >(symbols_match … (transform_program_gen_match … tf p)) 1373 [ %  #v #w * #id #r #v1 #v2 #E destruct %  skip ] 1154 1374  #b #f #FFP 1155 1375 cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP) 
src/common/Measurable.ma
r2685 r2722 394 394 *) 395 395 396 definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝ 397 λFE,p,m,n. 398 let trace ≝ exec_inf … FE p in 399 match split_trace … trace m with 400 [ Some x ⇒ 401 let 〈prefix,suffix〉 ≝ x in 402 match split_trace … suffix n with 403 [ Some y ⇒ 404 let interesting ≝ \fst y in 405 Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉 406  _ ⇒ None ? 407 ] 408  _ ⇒ None ? 409 ]. 410 411 definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝ 412 λFE,p,m. 413 let trace ≝ exec_inf … FE p in 414 match split_trace … trace m with 415 [ Some x ⇒ 416 match \snd x with 417 [ e_step _ s _ ⇒ Some ? s 418  e_stop _ _ s ⇒ Some ? s 419  _ ⇒ None ? 420 ] 421  _ ⇒ None ? 422 ]. 396 definition observables : ∀C:preclassified_system. program ?? C → nat → nat → res ((list intensional_event) × (list intensional_event)) ≝ 397 λC,p,m,n. 398 let g ≝ make_global … (pcs_exec … C) p in 399 let C' ≝ pcs_to_cs C g in 400 ! s0 ← make_initial_state … p; 401 ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0; 402 ! 〈interesting,s2〉 ← exec_steps m ?? (cs_exec … C') g s1; 403 let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in 404 return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉. 405
Note: See TracChangeset
for help on using the changeset viewer.