Changeset 2687
 Timestamp:
 Feb 21, 2013, 4:20:19 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semanticsUtils.ma
r2683 r2687 164 164 lapply (opt_eq_from_res ???? H) H #EQ2 165 165 whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2} 166 qed.167 168 lemma symbols_match :169 ∀M:matching.∀initV,initW.170 (∀v,w. match_var_entry M v w →171 size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →172 ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).173 ∀MATCH:match_program … M p p'.174 symbols … (globalenv … initW p') = symbols … (globalenv … initV p).175 * #A #B #V #W #match_fn #match_var #initV #initW #H176 #p #p' * #Mvars #Mfn #Mmain177 whd in match globalenv in ⊢ (???%); normalize nodelta178 whd in match (globalenv_allocmem ????);179 change with (add_globals ?????) in match (foldl ?????);180 >(proj1 … (add_globals_match … initW … Mvars))181 [ % *:]182 [ * #idr #v * #idr' #w #MVE %183 [ inversion MVE184 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %185  @(H … MVE)186 ]187  @(matching_fns_get_same_blocks … Mfn)188 #f #g @match_funct_entry_id189 ]190 qed.191 192 lemma symbols_transf:193 ∀A,B,V,init.∀prog_in : program A V.194 ∀trans : ∀vars.A vars → B vars.195 let prog_out ≝ transform_program … prog_in trans in196 symbols … (globalenv … init prog_out) = symbols … (globalenv … init prog_in).197 #A #B #V #iV #p #tf whd198 @(symbols_match … (transform_program_match … tf ?))199 #v0 #w0 * //200 166 qed. 201 167 … … 220 186 λM,vars.pm_P … (match_fundef M ?). 221 187 222 axiom functions_match: 188 lemma pm_P_insert : 189 ∀A,B,P. 190 ∀p,a1,a2,m1,m2.P a1 a2 → pm_P A B P m1 m2 → 191 pm_P … P (insert … p a1 m1) (insert … p a2 m2). 192 #A #B #P #p #a1 #a2 #m1 #m2 #Pa1a2 #Pm1m2 193 #p' 194 @(eqb_elim p' p) #H destruct 195 [ >lookup_opt_insert_hit >lookup_opt_insert_hit @Pa1a2 196  >(lookup_opt_insert_miss … a1 … H) >(lookup_opt_insert_miss … a2 … H) 197 @Pm1m2 198 ] 199 qed. 200 201 lemma pm_P_set_None : 202 ∀A,B,P. 203 ∀p,m1,m2.pm_P A B P m1 m2 → 204 pm_P … P (pm_set … p (None ?) m1) (pm_set … p (None ?) m2). 205 #A #B #P #p #m1 #m2 #Pm1m2 206 #p' 207 @(eqb_elim p' p) #H destruct 208 [ >lookup_opt_pm_set_hit >lookup_opt_pm_set_hit % 209  >(lookup_opt_pm_set_miss … H) >(lookup_opt_pm_set_miss … H) 210 @Pm1m2 211 ] 212 qed. 213 214 record match_genv_t (M : matching) 215 (vars : list ident) 216 (ge1 : genv_t (m_A M vars)) (ge2 : genv_t (m_B M vars)) : Prop ≝ 217 { symbols_eq : symbols … ge1 = symbols … ge2 218 ; nextfunction_eq : nextfunction … ge1 = nextfunction … ge2 219 ; functions_match : pm_P … (match_fundef M ?) (functions … ge1) (functions … ge2) 220 }. 221 222 lemma add_globals_match : 223 ∀M : matching.∀initV,initW. 224 ∀vars1,vars2. 225 ∀vars. 226 (* let vars1' ≝ map … (λx.\fst (\fst x)) vars1 in 227 let vars2' ≝ map … (λx.\fst (\fst x)) vars2 in *) 228 ∀env_mem1 : genv_t (m_A M vars) × mem. 229 ∀env_mem2 : genv_t (m_B M vars) × mem. 230 All2 (ident×region×(m_V M)) (ident×region×(m_W M)) 231 (match_var_entry M) vars1 vars2 → 232 nextblock … (\snd env_mem1) = nextblock … (\snd env_mem2) → 233 match_genv_t M vars 234 (\fst env_mem1) (\fst env_mem2) → 235 match_genv_t M vars 236 (\fst (add_globals … initV env_mem1 vars1)) 237 (\fst (add_globals … initW env_mem2 vars2)). 238 #M #init1 #init2 #vars1 239 elim vars1 vars1 [2: ** #id1 #r1 #v1 #tl1 #IH ] 240 * [2,4: ** #id2 #r2 #v2 #tl2 ] 241 #vars * #env1 #mem1 * #env2 #mem2 * 242 [2: #_ #H @H ] 243 #H inversion H #id' #r' #v1' #v2' #P #EQ1 #EQ2 #_ destruct H #H 244 #EQnxtbl #G @(IH tl2 … H) 245 cases mem1 in EQnxtbl; mem1 #mem1 #nbl1 #prf1 246 cases mem2 mem2 #mem2 #nbl2 #prf2 #EQ destruct 247 [ % ] 248 normalize nodelta % 249 whd in match add_symbol; 250 whd in match drop_fn; normalize nodelta 251 [ >(symbols_eq … G) % 252  @(nextfunction_eq … G) 253  >(symbols_eq … G) cases (lookup ? block ??) normalize nodelta 254 [2: ** [2,3: #p] normalize nodelta ] 255 try @pm_P_set_None 256 @(functions_match … G) 257 ] 258 qed. 259 260 lemma add_functs_match : 261 ∀M : matching. 262 ∀vars. 263 ∀functs1,functs2. 264 (* let vars1' ≝ map … (λx.\fst (\fst x)) vars1 in 265 let vars2' ≝ map … (λx.\fst (\fst x)) vars2 in *) 266 ∀env1 : genv_t (m_A M vars). 267 ∀env2 : genv_t (m_B M vars). 268 All2 … 269 (match_funct_entry M vars vars) functs1 functs2 → 270 match_genv_t M vars env1 env2 → 271 match_genv_t M vars 272 (add_functs … env1 functs1) 273 (add_functs … env2 functs2). 274 #M #vars #functs1 elim functs1 functs1 [2: * #id1 #f1 #tl1 #IH ] 275 * [2,4: * #id2 #f2 #tl2 ] 276 #env1 #env2 * 277 [2: #H @H ] 278 #H 279 cut (id1 = id2 ∧ match_fundef M … f1 f2) 280 [ @(match_funct_entry_inv M ??????? H) #v #i #f1 #f2 #H %{H} % ] 281 * #EQ destruct #Pf1f2 #Ptl1tl2 #G 282 lapply (IH … Ptl1tl2 G) G #G 283 % 284 whd in 285 match (add_functs ?? (? :: tl1)); 286 whd in 287 match (add_functs ?? (? :: tl2)); 288 change with (add_functs ?? tl1) in match (foldr ???? tl1); 289 change with (add_functs ?? tl2) in match (foldr ???? tl2); 290 whd in match drop_fn; normalize nodelta 291 [ >(nextfunction_eq … G) >(symbols_eq … G) % 292  >(nextfunction_eq … G) % 293  >(symbols_eq … G) cases (lookup ? block ??) normalize nodelta 294 [2: ** [2,3: #p] normalize nodelta ] 295 >(nextfunction_eq … G) 296 @(pm_P_insert … Pf1f2) 297 try @pm_P_set_None @(functions_match … G) 298 ] 299 qed. 300 301 lemma globalenv_match: 223 302 ∀M:matching.∀initV,initW. 303 (∀v,w. match_var_entry M v w → 304 size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → 224 305 ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). 225 306 ∀MATCH:match_program … M p p'. 226 match_funct_map M ? 227 (functions ? (globalenv ?? initV p)) 228 (functions ? (globalenv ?? initW p') ⌈prog_var_names … p' ↦ prog_var_names … p⌉). 229 @sym_eq @(matching_vars … (mp_vars … MATCH)) qed. 307 match_genv_t M ? (globalenv … initV p) 308 (globalenv … initW p' ⌈prog_var_names … p' ↦ prog_var_names … p⌉). 309 [2: @sym_eq @(matching_vars … (mp_vars … MATCH)) ] 310 * #A #B #V #W #Pf #Pv #iV #iW #init_eq 311 * #vars1 #functs1 #main1 312 * #vars2 #functs2 #main2 313 * #Mvars #Mfns #EQmain destruct 314 lapply (sym_eq ????) 315 whd in match prog_var_names in functs2 Mfns ⊢ %; 316 normalize nodelta in functs2 Mfns ⊢ %; #E 317 lapply Mfns lapply functs2 functs2 lapply Mvars Mvars lapply init_eq init_eq 318 whd in match globalenv; whd in match globalenv_allocmem; 319 normalize nodelta 320 cases daemon 321 (* TODO I hate coercions *) 322 qed. 323 324 lemma symbols_transf: 325 ∀A,B,V,init.∀prog_in : program A V. 326 ∀trans : ∀vars.A vars → B vars. 327 let prog_out ≝ transform_program … prog_in trans in 328 symbols … (globalenv … init prog_out) = symbols … (globalenv … init prog_in). 329 #A #B #V #iV #p #tf whd 330 lapply (transform_program_match … tf p) 331 #MATCH 332 >(symbols_eq … (globalenv_match … MATCH)) 333 [2: @iV 3: #v #w * // ] 334 lapply (sym_eq ????) 335 whd in match (prog_var_names ???); whd in match (prog_vars B ??); 336 #E >(K ?? E) normalize nodelta % 337 qed. 338 230 339 231 340 lemma functions_transf: … … 236 345 option_map ?? (trans ?) (lookup_opt … p (functions … (globalenv … init prog_in))). 237 346 #A #B #V #iV #p #tf #n 238 lapply(functions_match … (transform_program_match … tf p) n) try @iV 239 cases (lookup_opt … n ?) [2: #f] normalize nodelta 240 generalize in ⊢ (match (???match % with [ _ ⇒ ?]) with [ _ ⇒ ?  _ ⇒ ? ] → ?); 241 #e >(K ?? e) normalize nodelta 242 cases (lookup_opt ???) [2,4: #f'] normalize nodelta 243 [2,3,4: * % ] 244 #EQ destruct % 347 lapply (transform_program_match … tf p) 348 #MATCH 349 whd in match globalenv; whd in match globalenv_allocmem; 350 normalize nodelta 351 lapply (functions_match … (globalenv_match … MATCH) n) 352 [ @iV  @iV  #v #w * // ] 353 lapply (sym_eq ????) 354 whd in match (prog_var_names ???); whd in match (prog_vars B ??); 355 #E >(K ?? E) normalize nodelta 356 cases (lookup_opt ???) [2: #x ] normalize nodelta 357 cases (lookup_opt ???) [2,4: #y ] normalize nodelta 358 [ #EQ <EQ % *: * % ] 245 359 qed. 246 360 … … 255 369 #bl 256 370 whd in match symbol_for_block; normalize nodelta 257 >(symbols_match … (transform_program_match … tf ?)) 258 [ % *:] 259 #v #w * // 371 >(symbols_transf … tf) % 260 372 qed. 261 373 … … 298 410 include alias "utilities/binary/positive.ma". 299 411 300 lemma pm_map_cases : ∀A.∀P : positive_map A → Prop.∀m : positive_map A.301 ((∀p.lookup_opt … p m = None ?) → P m) →302 (∀p,v.lookup_opt … p m = Some ? v → P m) →303 P m.304 #A #P #m lapply P P elim m m305 [ #P #H1 #_ @H1 #p % ]306 * [2: #x ] #l #r #IHl #IHr #P #H1 #H2 [ @(H2 one x) % ]307 @IHl [2: #p #v #EQ @(H2 (p0 p) v EQ) ]308 #l_empty309 @IHr [2: #p #v #EQ @(H2 (p1 p) v EQ) ]310 #r_empty311 @H1 * normalize //312 qed.313 314 412 lemma pm_map_add_ind : ∀A.∀P : positive_map A → Prop. 315 413 (∀m.(∀p.lookup_opt A p m = None ?) → P m) → … … 338 436 #A #B #impl * #Bf % #At @Bf @impl @At qed. 339 437 438 definition b_graph_transform_program_props ≝ 439 λsrc,dst : sem_graph_params. 440 λdata,prog_in. 441 λinit_regs : block → list register. 442 λf_lbls : block → label → option (list label). 443 λf_regs : block → label → option (list register). 444 let prog_out ≝ b_graph_transform_program src dst data prog_in in 445 let src_genv ≝ globalenv_noinit ? prog_in in 446 let dst_genv ≝ globalenv_noinit ? prog_out in 447 ∀bl,def_in. 448 find_funct_ptr … src_genv bl = return (Internal ? def_in) → 449 ∃init_data,def_out. 450 find_funct_ptr … dst_genv bl = return (Internal ? def_out) ∧ 451 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧ 452 b_graph_translate_props src dst ? init_data (init_regs bl) 453 def_in def_out (f_lbls bl) (f_regs bl). 454 340 455 lemma b_graph_transform_program_find_funct_ptr : 341 456 ∀src,dst:sem_graph_params. … … 349 464 ∃f_lbls : block → label → option (list label). 350 465 ∃f_regs : block → label → option (list register). 351 ∀bl,def_in. 352 find_funct_ptr … src_genv bl = return (Internal ? def_in) → 353 ∃init_data,def_out. 354 find_funct_ptr … dst_genv bl = return (Internal ? def_out) ∧ 355 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧ 356 b_graph_translate_props src dst ? init_data (init_regs bl) 357 def_in def_out (f_lbls bl) (f_regs bl). 466 b_graph_transform_program_props src dst data prog_in init_regs f_lbls f_regs. 358 467 #src #dst #data #prog_in 359 whd 468 whd in match b_graph_transform_program_props; normalize nodelta 360 469 letin prog_out ≝ (b_graph_transform_program … data prog_in) 361 470 letin src_genv ≝ (globalenv_noinit ? prog_in) … … 436 545 bind_new register (b_graph_translate_data src dst globals). 437 546 ∀prog_in : joint_program src. 547 ∀init_regs : block → list register. 548 ∀f_lbls : block → label → option (list label). 549 ∀f_regs : block → label → option (list register). 550 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs → 438 551 let prog_out ≝ b_graph_transform_program … data prog_in in 439 552 let src_genv ≝ globalenv_noinit ? prog_in in 440 553 let dst_genv ≝ globalenv_noinit ? prog_out in 441 let code_block ≝ (Σbl.block_region bl = Code) in442 ∃init_regs : code_block → list register.443 ∃f_lbls : code_block → label → option (list label).444 ∃f_regs : code_block → label → option (list register).445 554 ∀bl,id,def_in. 446 555 fetch_internal_function … src_genv bl = return 〈id, def_in〉 → … … 451 560 def_in def_out (f_lbls bl) (f_regs bl). 452 561 #src #dst #data #prog_in 453 cases (b_graph_transform_program_find_funct_ptr src dst data prog_in) 454 #init_regs * #f_lbls * #f_regs #props 455 %{(λb.init_regs b)} 456 %{(λb.f_lbls b)} 457 %{(λb.f_regs b)} 562 #init_regs #f_lbls #f_regs #props 458 563 #bl #id #def_in 459 564 #H @('bind_inversion H) * #id' * #def_in' H … … 477 582 bind_new register (b_graph_translate_data src dst globals). 478 583 ∀prog_in : joint_program src. 584 ∀init_regs : block → list register. 585 ∀f_lbls : block → label → option (list label). 586 ∀f_regs : block → label → option (list register). 587 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs → 479 588 let prog_out ≝ b_graph_transform_program … data prog_in in 480 589 let src_genv ≝ globalenv_noinit ? prog_in in 481 590 let dst_genv ≝ globalenv_noinit ? prog_out in 482 let code_block ≝ (Σbl.block_region bl = Code) in483 ∃init_regs : code_block → list register.484 ∃f_lbls : code_block → label → option (list label).485 ∃f_regs : code_block → label → option (list register).486 591 ∀pc,id,def_in,s. 487 592 fetch_statement … src_genv pc = return 〈id, def_in, s〉 → … … 490 595 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧ 491 596 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧ 492 b_graph_translate_props src dst ? init_data (init_regs bl)493 def_in def_out (f_lbls bl) (f_regs bl) ∧494 597 let l ≝ point_of_pc dst pc in 495 598 ∃lbls,regs. … … 509 612 ]. 510 613 #src #dst #data #prog_in 511 cases (b_graph_transform_program_fetch_internal_function src dst data prog_in) 512 #init_regs * #f_lbls * #f_regs #props 513 %{init_regs} 514 %{f_lbls} 515 %{f_regs} 614 #init_regs #f_lbls #f_regs #props 516 615 #pc #id #def_in #s 517 616 #H @('bind_inversion H) * #id' #def_in' H … … 520 619 #H lapply (opt_eq_from_res ???? H) H 521 620 #EQstmt_at whd in ⊢ (??%%→?); #EQ destruct 522 cases (props … EQfif) 523 #a * #b #H %{a} %{b} %{H} 524 cases H H #_ #props' 525 @(multi_fetch_ok … props' … EQstmt_at) 526 qed. 621 cases (b_graph_transform_program_fetch_internal_function … props … EQfif) 622 #a * #b ** #H1 #H2 #H3 %{a} %{b} % 623 [ %{H1 H2}  @(multi_fetch_ok … H3 … EQstmt_at) ] 624 qed.
Note: See TracChangeset
for help on using the changeset viewer.