Changeset 2683
 Timestamp:
 Feb 20, 2013, 6:41:46 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semanticsUtils.ma
r2681 r2683 4 4 include "ASM/BitVectorTrie.ma". 5 5 include "joint/TranslateUtils.ma". 6 include "common/ExtraMonads.ma". 7 include "common/extraGlobalenvs.ma". 6 8 7 9 record hw_register_env : Type[0] ≝ … … 164 166 qed. 165 167 166 axiom b_graph_transform_program_props : 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 #H 176 #p #p' * #Mvars #Mfn #Mmain 177 whd in match globalenv in ⊢ (???%); normalize nodelta 178 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 MVE 184 #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_id 189 ] 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 in 196 symbols … (globalenv … init prog_out) = symbols … (globalenv … init prog_in). 197 #A #B #V #iV #p #tf whd 198 @(symbols_match … (transform_program_match … tf ?)) 199 #v0 #w0 * // 200 qed. 201 202 definition pm_P : ∀A,B.∀P : A → B → Prop.positive_map A → positive_map B → Prop ≝ 203 λA,B,P,mA,mB. 204 ∀p. 205 match lookup_opt … p mA with 206 [ Some a ⇒ 207 match lookup_opt … p mB with 208 [ Some b ⇒ P a b 209  _ ⇒ False 210 ] 211  _ ⇒ match lookup_opt … p mB with 212 [ Some _ ⇒ False 213  _ ⇒ True 214 ] 215 ]. 216 217 definition match_funct_map : 218 ∀M : matching. 219 ∀vars.positive_map (m_A M vars) → positive_map (m_B M vars) → Prop ≝ 220 λM,vars.pm_P … (match_fundef M ?). 221 222 axiom functions_match: 223 ∀M:matching.∀initV,initW. 224 ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). 225 ∀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. 230 231 lemma functions_transf: 232 ∀A,B,V,init.∀prog_in : program A V. 233 ∀trans : ∀vars.A vars → B vars. 234 let prog_out ≝ transform_program … prog_in trans in 235 ∀p.lookup_opt … p (functions … (globalenv … init prog_out)) = 236 option_map ?? (trans ?) (lookup_opt … p (functions … (globalenv … init prog_in))). 237 #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 % 245 qed. 246 247 lemma symbol_for_block_transf : 248 ∀A,B,V,init.∀prog_in : program A V. 249 ∀trans : ∀vars.A vars → B vars. 250 let prog_out ≝ transform_program … prog_in trans in 251 ∀bl. 252 symbol_for_block … (globalenv … init prog_out) bl = 253 symbol_for_block … (globalenv … init prog_in) bl. 254 #A #B #V #iV #p #tf whd 255 #bl 256 whd in match symbol_for_block; normalize nodelta 257 >(symbols_match … (transform_program_match … tf ?)) 258 [ % *:] 259 #v #w * // 260 qed. 261 262 include alias "common/Pointers.ma". 263 264 lemma fetch_function_transf : 265 ∀A,B,V,init.∀prog_in : program A V. 266 ∀trans : ∀vars.A vars → B vars. 267 let prog_out ≝ transform_program … prog_in trans in 268 ∀bl. 269 fetch_function … (globalenv … init prog_out) bl = 270 ! 〈i, f〉 ← fetch_function … (globalenv … init prog_in) bl ; 271 return 〈i, trans … f〉. 272 #A #B #V #init #prog_in #trans #bl 273 whd in match fetch_function; normalize nodelta 274 >(symbol_for_block_transf A B V init prog_in trans) 275 cases (symbol_for_block ???) [ % ] #id >m_return_bind >m_return_bind 276 whd in match find_funct_ptr; normalize nodelta 277 whd in match (block_region (pi1 ?? bl)); 278 cases (block_id (pi1 ?? bl)) [2,3: #p] normalize nodelta try % 279 >(functions_transf A B V init prog_in trans p) 280 cases (lookup_opt ???) // 281 qed. 282 283 lemma fetch_internal_function_transf : 284 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ. 285 ∀trans : ∀vars.A vars → B vars. 286 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in 287 ∀bl. 288 fetch_internal_function … (globalenv_noinit … prog_out) bl = 289 ! 〈i, f〉 ← fetch_internal_function … (globalenv_noinit … prog_in) bl ; 290 return 〈i, trans … f〉. 291 #A #B #prog #trans #bl 292 whd in match fetch_internal_function; normalize nodelta 293 >(fetch_function_transf … prog) 294 cases (fetch_function ???) 295 [ * #id * #f %  #e % ] 296 qed. 297 298 include alias "utilities/binary/positive.ma". 299 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 m 305 [ #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_empty 309 @IHr [2: #p #v #EQ @(H2 (p1 p) v EQ) ] 310 #r_empty 311 @H1 * normalize // 312 qed. 313 314 lemma pm_map_add_ind : ∀A.∀P : positive_map A → Prop. 315 (∀m.(∀p.lookup_opt A p m = None ?) → P m) → 316 (∀m,p,v.P m → lookup_opt A p m = None ? → P (insert A p v m)) → 317 ∀m.P m. 318 #A #P #H1 #H2 #m lapply H2 lapply H1 lapply P P elim m m 319 [ #P #H1 #_ @H1 #p % ] 320 #o #l #r #IHl #IHr #P #H1 #H2 321 @IHl #l' 322 [ #empty_l' @IHr #r' 323 [ #empty_r' cases o [ @H1 * try #p normalize // ] 324 #v change with (P (insert ? one v (pm_node ? (None ?) ??))) 325 @H2 [ @H1 * try #p normalize //  % ] 326 ] 327 ] 328 #p #v #H #G 329 [ change with (P (insert ? (p1 p) v (pm_node ? ???))) 330  change with (P (insert ? (p0 p) v (pm_node ? ???))) 331 ] @H2 assumption 332 qed. 333 334 include alias "basics/logic.ma". 335 include alias "common/PositiveMap.ma". 336 337 lemma swap_neg : ∀A,B : Prop.(A → B) → ¬B → ¬A. 338 #A #B #impl * #Bf % #At @Bf @impl @At qed. 339 340 lemma b_graph_transform_program_find_funct_ptr : 167 341 ∀src,dst:sem_graph_params. 168 342 ∀data : ∀globals.joint_closed_internal_function src globals → … … 172 346 let src_genv ≝ globalenv_noinit ? prog_in in 173 347 let dst_genv ≝ globalenv_noinit ? prog_out in 174 ∃init_regs : ident → list register. 175 ∃f_lbls : ident → label → option (list label). 176 ∃f_regs : ident → label → option (list register). 348 ∃init_regs : block → list register. 349 ∃f_lbls : block → label → option (list label). 350 ∃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). 358 #src #dst #data #prog_in 359 whd 360 letin prog_out ≝ (b_graph_transform_program … data prog_in) 361 letin src_genv ≝ (globalenv_noinit ? prog_in) 362 letin dst_genv ≝ (globalenv_noinit ? prog_out) 363 cut (∀p.lookup_opt ? p (functions ? dst_genv) = 364 option_map ?? (transf_fundef … (λf.b_graph_translate … (data … f) f)) 365 (lookup_opt ? p (functions ? src_genv))) 366 [ @functions_transf ] 367 cases dst_genv #functs2 #nextf2 #symbols2 #H2 368 cases src_genv #functs1 #nextf1 #symbols1 #H1 369 lapply H2 lapply H1 lapply functs2 370 @(pm_map_add_ind … functs1) functs1 functs2 #functs1 371 [ #functs1_empty  #p #f #IH #p_not_in ] 372 #functs2 #H1 #H2 #transf 373 [ %{(λ_.[ ])} %{(λ_.λ_.None ?)} %{(λ_.λ_.None ?)} 374 #bl #def_in #ABS @⊥ lapply ABS ABS 375 whd in match find_funct_ptr; 376 normalize nodelta 377 whd in match (block_region bl); 378 cases (block_id bl) normalize nodelta 379 [2,3: #p [2: >functs1_empty ]] 380 normalize #ABS destruct 381 ] 382 cases (IH (pm_set … p (None ?) functs2) ???) 383 [2: @hide_prf #b #G @(H1 b ?) @(swap_neg … G) G @(eqb_elim b p) 384 [ #EQ destruct >lookup_opt_insert_hit #ABS destruct ] 385 #NEQ >(lookup_opt_insert_miss ? f b p … NEQ) #H @H 386 3: @hide_prf #b #G @(H2 b ?) @(swap_neg … G) G @(eqb_elim b p) 387 [ #EQ destruct >lookup_opt_pm_set_hit #_ % ] 388 #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) #H @H 389 4: #b @(eqb_elim b p) 390 [ #EQ destruct >lookup_opt_pm_set_hit >p_not_in % ] 391 #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) >transf 392 >(lookup_opt_insert_miss ? f b p … NEQ) % 393 ] 394 IH cases f in H1 transf; f #f #H1 #transf 395 #init_regs * #f_lbls * #f_regs #props 396 [ (* internal *) 397 letin upd ≝ (λA : Type[0].λf : block → A. 398 λid.λv,id'. 399 if eq_block id id' then v else f id') 400 cases (pi2 ?? (b_graph_translate … (data … f) f)) 401 #loc_data * #loc_init_regs * #loc_f_lbls * #loc_f_regs * 402 #inst_loc_data #loc_props 403 letin bl ≝ (mk_block (neg p)) 404 %{(upd … init_regs bl loc_init_regs)} 405 %{(upd … f_lbls bl loc_f_lbls)} 406 %{(upd … f_regs bl loc_f_regs)} 407  (* external, nothing changes *) 408 %{init_regs} 409 %{f_lbls} 410 %{f_regs} 411 ] 412 * #p' #def_in 413 whd in match find_funct_ptr; normalize nodelta 414 whd in match (block_region (mk_block p')); 415 cases p' p' [2,3,5,6: #p' ] normalize nodelta 416 [1,3,5,6: #ABS normalize in ABS; destruct] 417 @(eqb_elim p' p) #pp' destruct 418 [1,3: >lookup_opt_insert_hit whd in ⊢ (??%%→?); #EQ destruct(EQ) 419 %{loc_data} % 420 [2: % [ % ] 421 [ >transf >lookup_opt_insert_hit % 422 *: >eq_block_b_b assumption 423 ] 424 ] 425 *: >(lookup_opt_insert_miss ???? functs1 … pp') 426 [ @eq_block_elim [ #EQ destruct cases (absurd ?? pp') % ] #_ normalize nodelta] 427 #EQ lapply (props (mk_block (neg p')) def_in EQ) 428 whd in match find_funct_ptr; normalize nodelta 429 >(lookup_opt_pm_set_miss … functs2 … pp') #H @H 430 ] 431 qed. 432 433 lemma b_graph_transform_program_fetch_internal_function : 434 ∀src,dst:sem_graph_params. 435 ∀data : ∀globals.joint_closed_internal_function src globals → 436 bind_new register (b_graph_translate_data src dst globals). 437 ∀prog_in : joint_program src. 438 let prog_out ≝ b_graph_transform_program … data prog_in in 439 let src_genv ≝ globalenv_noinit ? prog_in in 440 let dst_genv ≝ globalenv_noinit ? prog_out in 441 let code_block ≝ (Σbl.block_region bl = Code) in 442 ∃init_regs : code_block → list register. 443 ∃f_lbls : code_block → label → option (list label). 444 ∃f_regs : code_block → label → option (list register). 177 445 ∀bl,id,def_in. 178 fetch_internal_function ?src_genv bl = return 〈id, def_in〉 →446 fetch_internal_function … src_genv bl = return 〈id, def_in〉 → 179 447 ∃init_data,def_out. 180 fetch_internal_function ? dst_genv bl = return 〈id, def_out〉 ∧ 181 bind_new_instantiates … init_data (data … def_in) (init_regs id) ∧ 182 b_graph_translate_props src dst ? init_data (init_regs id) 183 def_in def_out (f_lbls id) (f_regs id). 448 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧ 449 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧ 450 b_graph_translate_props src dst ? init_data (init_regs bl) 451 def_in def_out (f_lbls bl) (f_regs bl). 452 #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)} 458 #bl #id #def_in 459 #H @('bind_inversion H) * #id' * #def_in' H 460 normalize nodelta #H whd in ⊢ (??%%→?); #EQ destruct 461 @('bind_inversion (opt_eq_from_res … H)) H #id' #EQ1 462 #H @('bind_inversion H) H #def_in' #H 463 whd in ⊢ (??%%→?); #EQ destruct 464 cases (props … H) 465 #loc_data * #def_out ** #H1 #H2 #H3 466 %{loc_data} %{def_out} 467 %{H3} %{H2} 468 whd in match fetch_internal_function; 469 whd in match fetch_function; normalize nodelta 470 >symbol_for_block_transf >EQ1 >m_return_bind 471 >H1 % 472 qed. 473 474 lemma b_graph_transform_program_fetch_statement : 475 ∀src,dst:sem_graph_params. 476 ∀data : ∀globals.joint_closed_internal_function src globals → 477 bind_new register (b_graph_translate_data src dst globals). 478 ∀prog_in : joint_program src. 479 let prog_out ≝ b_graph_transform_program … data prog_in in 480 let src_genv ≝ globalenv_noinit ? prog_in in 481 let dst_genv ≝ globalenv_noinit ? prog_out in 482 let code_block ≝ (Σbl.block_region bl = Code) in 483 ∃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 ∀pc,id,def_in,s. 487 fetch_statement … src_genv pc = return 〈id, def_in, s〉 → 488 ∃init_data,def_out. 489 let bl ≝ pc_block pc in 490 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧ 491 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 let l ≝ point_of_pc dst pc in 495 ∃lbls,regs. 496 f_lbls bl l = Some ? lbls ∧ 497 f_regs bl l = Some ? regs ∧ 498 match s with 499 [ sequential s' nxt ⇒ 500 let block ≝ 501 if eq_identifier … (joint_if_entry … def_in) l then 502 append_seq_list … (f_step … init_data l s') (added_prologue … init_data) 503 else 504 f_step … init_data l s' in 505 l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out 506  final s' ⇒ 507 l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out 508  FCOND abs _ _ _ ⇒ Ⓧabs 509 ]. 510 #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} 516 #pc #id #def_in #s 517 #H @('bind_inversion H) * #id' #def_in' H 518 #EQfif 519 #H @('bind_inversion H) H #s 520 #H lapply (opt_eq_from_res ???? H) H 521 #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.
Note: See TracChangeset
for help on using the changeset viewer.